0 | module Derive.Finite
 1 |
 2 | import public Data.Finite
 3 | import public Derive.Prelude
 4 | import Language.Reflection.Util
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          Claims
10 | --------------------------------------------------------------------------------
11 |
12 | ||| Top-level function declaration implementing the `values` function for
13 | ||| the given data type.
14 | export
15 | valuesClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
16 | valuesClaim vis fun p =
17 |   let arg := p.applied
18 |       tpe := piAll `(List ~(arg)) (allImplicits p "Finite")
19 |    in simpleClaim vis fun tpe
20 |
21 | ||| Top-level declaration implementing the `Finite` interface for
22 | ||| the given data type.
23 | export
24 | finiteImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
25 | finiteImplClaim v impl p = implClaimVis v impl (implType "Finite" p)
26 |
27 | --------------------------------------------------------------------------------
28 | --          Definitions
29 | --------------------------------------------------------------------------------
30 |
31 | export
32 | finiteImplDef : (fun, impl : Name) -> Decl
33 | finiteImplDef f i = def i [patClause (var i) (var "MkFinite" `app` var f)]
34 |
35 | app : TTImp -> List (BoundArg 0 Explicit) -> TTImp
36 | app s []        = s
37 | app s (_ :: xs) = app `(Prelude.(<*>) ~(s) values) xs
38 |
39 | add : SnocList TTImp -> TTImp -> TTImp
40 | add [<]       s = s
41 | add (sx :< x) s = add sx `(Prelude.List.(++) ~(x) ~(s))
42 |
43 | cons : SnocList TTImp -> TTImp -> TTImp
44 | cons [<]       s = s
45 | cons (sx :< x) s = cons sx `(Prelude.(::) ~(x) ~(s))
46 |
47 | rhs : {0 as : _} -> SnocList TTImp -> SnocList TTImp -> List (Con n as) -> TTImp
48 | rhs ss st []      = cons ss (add st `(Prelude.Nil))
49 | rhs ss st (c::cs) = case boundArgs explicit c.args [] <>> [] of
50 |   [] => rhs (ss :< c.nameVar) st cs
51 |   as => rhs ss (st :< app `(Prelude.pure ~(c.nameVar)) as) cs
52 |
53 | ||| Definition of a (local or top-level) function implementing
54 | ||| the values operation.
55 | export
56 | valuesDef : Name -> ParamTypeInfo -> Decl
57 | valuesDef fun p = def fun [patClause (var fun) (rhs [<] [<] p.info.cons)]
58 |
59 | --------------------------------------------------------------------------------
60 | --          Deriving
61 | --------------------------------------------------------------------------------
62 |
63 | ||| Generate declarations and implementations for `Finite` for a given data type.
64 | export
65 | FiniteVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
66 | FiniteVis vis nms p =
67 |   let fun  := funName p "values"
68 |       impl := implName p "Finite"
69 |    in Right
70 |         [ TL (valuesClaim vis fun p) (valuesDef fun p)
71 |         , TL (finiteImplClaim vis impl p) (finiteImplDef fun impl)
72 |         ]
73 |
74 | ||| Alias for `FiniteVis Public`
75 | export %inline
76 | Finite : List Name -> ParamTypeInfo -> Res (List TopLevel)
77 | Finite = FiniteVis Public
78 |