0 | module Generics.Derive
3 | import public Generics.SOP
4 | import public Generics.Meta
5 | import public Decidable.Equality
7 | import public Language.Reflection.Util
12 | %language ElabReflection
22 | ConNames = (Name, List Name, List TTImp)
27 | mkGeneric = "MkGeneric"
33 | mkSOP' : (k : Nat) -> (arg : TTImp) -> TTImp
34 | mkSOP' k arg = `(MkSOP ~(run k))
37 | run : (n : Nat) -> TTImp
39 | run (S n) = `(S ~(run n))
42 | mkSOP : (k : Nat) -> (args : List TTImp) -> TTImp
43 | mkSOP k args = mkSOP' k (listOf args)
48 | mkCode : (p : ParamTypeInfo) -> TTImp
49 | mkCode p = listOf $
map (\c => listOf $
explicits c.args) p.cons
52 | explicits : Vect n (ConArg p.numParams) -> List TTImp
54 | explicits (CArg _ _ ExplicitArg t :: as) =
55 | ttimp p.paramNames t :: explicits as
56 | explicits (_ :: as) = explicits as
59 | fromClause : (Nat,ConNames) -> Clause
60 | fromClause (k,(con,ns,vars)) = patClause (bindAll con ns) (mkSOP k vars)
63 | fromToIdClause : (Nat,ConNames) -> Clause
64 | fromToIdClause (k,(con,ns,vars)) = patClause (bindAll con ns) `(Refl)
67 | toClause : (Nat,ConNames) -> Clause
68 | toClause (k,(con,ns,vars)) =
69 | patClause (mkSOP k $
map bindVar ns) (appAll con vars)
72 | impossibleToClause : Nat -> Clause
73 | impossibleToClause k = impossibleClause (mkSOP' k implicitTrue)
76 | toFromIdClause : (Nat,ConNames) -> Clause
77 | toFromIdClause (k,(con,ns,vars)) = patClause (mkSOP k $
map bindVar ns) `(Refl)
80 | zipWithIndex : List a -> List (Nat,a)
81 | zipWithIndex as = run 0 as
84 | run : Nat -> List a -> List (Nat,a)
86 | run k (h::t) = (k,h) :: run (S k) t
89 | conNames : ParamCon n -> ConNames
91 | let ns := toList $
freshNames "x" (count isExplicit c.args)
93 | in (c.name, ns, vars)
98 | GenericVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
99 | GenericVis vis _ p =
100 | let names := zipWithIndex (map conNames p.cons)
101 | fun := UN . Basic $
"implGeneric" ++ camelCase p.info.name
103 | appType := p.applied
104 | genType := `(Generic ~(appType) ~(mkCode p))
105 | funType := piAll genType p.implicits
107 | x := lambdaArg {a = Name} "x"
109 | from := lam x $
iCase varX implicitFalse (map fromClause names)
110 | to := lam x $
iCase varX implicitFalse (map toClause names)
111 | fromToId := lam x $
iCase varX implicitFalse (map fromToIdClause names)
112 | toFromId := lam x $
iCase varX implicitFalse (map toFromIdClause names)
114 | impl := appAll mkGeneric [from,to,fromToId,toFromId]
117 | [ TL (interfaceHint vis fun funType) (def fun [patClause (var fun) impl])]
121 | Generic : List Name -> ParamTypeInfo -> Res (List TopLevel)
122 | Generic = GenericVis Public
130 | str : String -> TTImp
131 | str = primVal . Str
136 | int n = `(fromInteger ~(primVal $
BI (cast n)))
141 | appNSName : Name -> (con,np : TTImp) -> TTImp
142 | appNSName (NS (MkNS ss) (UN $
Basic s)) con np =
143 | let ss' := listOf $
reverse $
map str ss
144 | in `(~(con) ~(ss') ~(str s) ~(np))
145 | appNSName n con np =
146 | let s := str $
nameStr n
147 | in `(~(con) []
~(s) ~(np))
151 | argNameTTImp : (Nat,Maybe Name) -> TTImp
152 | argNameTTImp (k, Just $
UN $
Basic n) = `(NamedArg ~(int k) ~(str n))
153 | argNameTTImp (k, _) = `(UnnamedArg ~(int k))
157 | conTTImp : ParamCon n -> TTImp
159 | let np := listOf $
map argNameTTImp (names 0 c.args)
160 | in appNSName c.name `(MkConInfo) np
163 | names : (k : Nat) -> Vect m (ConArg n) -> List (Nat, Maybe Name)
165 | names k (CArg n _ ExplicitArg t :: as) = (k,n) :: names (S k) as
166 | names k (_ :: as) = names k as
169 | tiTTImp : ParamTypeInfo -> TTImp
171 | let nps := map conTTImp p.cons
172 | in appNSName p.info.name `(MkTypeInfo) (listOf nps)
177 | MetaVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
179 | let genType := `(Meta ~(p.applied) ~(mkCode p))
180 | funType := piAll genType p.implicits
181 | fun := UN . Basic $
"implMeta" ++ camelCase p.info.name
183 | impl := `(MkMeta ~(tiTTImp p))
186 | [TL (interfaceHint vis fun funType) (def fun [patClause (var fun) impl])]
190 | Meta : List Name -> ParamTypeInfo -> Res (List TopLevel)
191 | Meta = MetaVis Public
201 | Eq : List Name -> ParamTypeInfo -> Res (List TopLevel)
203 | let nm := implName p "Eq"
204 | cl := patClause (var nm) `(mkEq genEq
)
205 | in Right [TL (interfaceHint Public nm (implType "Eq" p)) (def nm [cl])]
215 | Ord : List Name -> ParamTypeInfo -> Res (List TopLevel)
217 | let nm := implName p "Ord"
218 | cl := patClause (var nm) `(mkOrd genCompare
)
219 | in Right [TL (interfaceHint Public nm (implType "Ord" p)) (def nm [cl])]
227 | DecEq : List Name -> ParamTypeInfo -> Res (List TopLevel)
229 | let nm := implName p "DecEq"
230 | cl := patClause (var nm) `(mkDecEq genDecEq
)
231 | in Right [TL (interfaceHint Public nm (implType "DecEq" p)) (def nm [cl])]
241 | Show : List Name -> ParamTypeInfo -> Res (List TopLevel)
243 | let nm := implName p "Show"
244 | cl := patClause (var nm) `(mkShowPrec genShowPrec
)
245 | in Right [TL (interfaceHint Public nm (implType "Show" p)) (def nm [cl])]
253 | %runElab derive "Nat" [Generic,Meta]
255 | %runElab derive "Maybe" [Generic,Meta]
258 | %runElab derive "Either" [Generic,Meta]
260 | %runElab derive "List" [Generic,Meta]
262 | %runElab derive "List1" [Generic,Meta]
264 | %runElab derive "Dec" [Generic,Meta]
266 | %runElab derive "Ordering" [Generic,Meta]
268 | %runElab derive "Bool" [Generic,Meta]
270 | %runElab derive "Prec" [Generic,Meta]
274 | %runElab derive "System.File.Mode.Mode" [Generic,Meta]
276 | %runElab derive "FileError" [Generic,Meta]
278 | %runElab derive "File" [Generic,Meta]
280 | %runElab derive "FileMode" [Generic,Meta]
282 | %runElab derive "Permissions" [Generic,Meta]
284 | %runElab derive "ClockType" [Generic,Meta]