0 | module Node.Internal.Elab
  1 |
  2 | import public Language.Reflection
  3 | import Node.Internal.Support
  4 |
  5 | %language ElabReflection
  6 | %default total
  7 |
  8 | export
  9 | field : String -> Name
 10 | field = UN . Field
 11 |
 12 | export
 13 | basic : String -> Name
 14 | basic = UN . Basic
 15 |
 16 | isVar : String -> TTImp -> Bool
 17 | isVar expected (IVar _ name) = hasName name
 18 |   where
 19 |     hasName : Name -> Bool
 20 |     hasName (UN $ Basic n) = n == expected
 21 |     hasName (UN $ Field n) = n == expected
 22 |     hasName (NS ns name) = hasName name
 23 |     hasName _ = False
 24 | isVar _ _ = False
 25 |
 26 | isMaybe : TTImp -> (Bool, TTImp)
 27 | isMaybe (IApp _ name expr) = (isVar "Maybe" name, expr)
 28 | isMaybe x = (False, x)
 29 |
 30 | fieldConvert : TTImp -> String -> String
 31 | fieldConvert tti var with (isMaybe tti)
 32 |   _ | (True, inner) with (isVar "Bool" inner)
 33 |     _ | True = """
 34 |       {
 35 |         const v = \{var}
 36 |         if (v === undefined || v === null) {
 37 |           return _nothing()
 38 |         }
 39 |         return _just(v ? _true() : _false())
 40 |       }
 41 |       """
 42 |     _ | False = """
 43 |       {
 44 |         const v = \{var}
 45 |         if (v === undefined || v === null) {
 46 |           return _nothing()
 47 |         }
 48 |         return _just(v)
 49 |       }
 50 |       """
 51 |   _ | (False, inner) with (isVar "Bool" inner)
 52 |     _ | True = "\{var} ? _true() : _false()"
 53 |     _ | False = var
 54 |
 55 | export
 56 | nodeFieldDecl : (fnName : Name) -> (fieldName : String) -> (fieldType : TTImp) -> List Decl
 57 | nodeFieldDecl fnName fieldName fieldType = [ foreignDecl, fnDecl, fnDef ]
 58 |   where
 59 |     nodeCode : String
 60 |     nodeCode = "node:lambda: (tyx, x) => \{fieldConvert fieldType $ "x." <+> fieldName}"
 61 |
 62 |     foreignFnOpt : FnOpt
 63 |     foreignFnOpt = ForeignFn [ IApp EmptyFC (IVar EmptyFC (basic "fromString")) (IPrimVal EmptyFC $ Str nodeCode) ]
 64 |
 65 |     foreignName : Name
 66 |     foreignName = basic "ffi_\{fieldName}"
 67 |
 68 |     foreignDecl : Decl
 69 |     foreignDecl = IClaim $ NoFC $ MkIClaimData MW Private [foreignFnOpt]
 70 |                     $ MkTy EmptyFC (NoFC foreignName)
 71 |                     $ IPi EmptyFC MW ExplicitArg Nothing (IBindVar EmptyFC $ basic "a") fieldType
 72 |
 73 |     fnDecl : Decl
 74 |     fnDecl = IClaim $ NoFC $ MkIClaimData MW Export []
 75 |                $ MkTy EmptyFC (NoFC fnName)
 76 |                $ IPi EmptyFC MW ExplicitArg Nothing (IBindVar EmptyFC $ basic "a") fieldType
 77 |
 78 |     fnDef : Decl
 79 |     fnDef = IDef EmptyFC fnName
 80 |               [ PatClause EmptyFC
 81 |                   (IApp EmptyFC (IVar EmptyFC fnName) (IBindVar EmptyFC $ basic "a"))
 82 |                   (IApp EmptyFC (IVar EmptyFC foreignName) (IVar EmptyFC (basic "a")))
 83 |               ]
 84 |
 85 | export
 86 | mkNodeField : (fnName : Name) -> (fieldName : String) -> (fieldType: TTImp) -> Elab ()
 87 | mkNodeField fnName fName fType = declare $ nodeFieldDecl fnName fName fType
 88 |
 89 | export
 90 | nodeFieldIODecl : (fnName : Name) -> (fieldName : String) -> (fieldType : TTImp) -> List Decl
 91 | nodeFieldIODecl fnName fieldName fieldType = [ foreignDecl, fnDecl, fnDef ]
 92 |   where
 93 |     nodeCode : String
 94 |     nodeCode = "node:lambda: (tyx, x) => \{fieldConvert fieldType $ "x." <+> fieldName}"
 95 |
 96 |     foreignFnOpt : FnOpt
 97 |     foreignFnOpt = ForeignFn [ IApp EmptyFC (IVar EmptyFC (basic "fromString")) (IPrimVal EmptyFC $ Str nodeCode) ]
 98 |
 99 |     foreignName : Name
100 |     foreignName = basic "ffi_\{fieldName}"
101 |
102 |     foreignDecl : Decl
103 |     foreignDecl = IClaim $ NoFC $ MkIClaimData MW Private [foreignFnOpt]
104 |                     $ MkTy EmptyFC (NoFC foreignName)
105 |                     $ IPi EmptyFC MW ExplicitArg Nothing (IBindVar EmptyFC $ basic "a")
106 |                       $ IApp EmptyFC (IVar EmptyFC $ basic "PrimIO") fieldType
107 |
108 |     fnDecl : Decl
109 |     fnDecl = IClaim $ NoFC $ MkIClaimData MW Export []
110 |                $ MkTy EmptyFC (NoFC fnName)
111 |                $ IPi EmptyFC MW AutoImplicit Nothing (IApp EmptyFC (IVar EmptyFC $ basic "HasIO") (IBindVar EmptyFC $ basic "io"))
112 |                  $ IPi EmptyFC MW ExplicitArg Nothing (IBindVar EmptyFC $ basic "a")
113 |                    $ IApp EmptyFC (IBindVar EmptyFC $ basic "io") fieldType
114 |
115 |     fnDef : Decl
116 |     fnDef = IDef EmptyFC fnName
117 |               [ PatClause EmptyFC
118 |                   (IApp EmptyFC (IVar EmptyFC fnName) (IBindVar EmptyFC $ basic "a"))
119 |                   (IApp EmptyFC (IVar EmptyFC $ basic "primIO") $ IApp EmptyFC (IVar EmptyFC foreignName) (IVar EmptyFC (basic "a")))
120 |               ]
121 |
122 | export
123 | mkNodeFieldIO : (fnName : Name) -> (fieldName : String) -> (fieldType : TTImp) -> Elab ()
124 | mkNodeFieldIO fnName fieldName fieldType = declare $ nodeFieldIODecl fnName fieldName fieldType
125 |
126 |