0 | module Derive.Monoid
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | --------------------------------------------------------------------------------
 5 | --          Claims
 6 | --------------------------------------------------------------------------------
 7 |
 8 | ||| Top-level function declaration implementing the `neutral` function for
 9 | ||| the given data type.
10 | export
11 | neutralClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | neutralClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll arg (allImplicits p "Monoid")
15 |    in simpleClaim vis fun tpe
16 |
17 | ||| Top-level declaration implementing the `Semigroup` interface for
18 | ||| the given data type.
19 | export
20 | monoidImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
21 | monoidImplClaim v impl p = implClaimVis v impl (implType "Monoid" p)
22 |
23 | --------------------------------------------------------------------------------
24 | --          Definitions
25 | --------------------------------------------------------------------------------
26 |
27 | export
28 | monoidImplDef : (fun, impl : Name) -> Decl
29 | monoidImplDef f i = def i [patClause (var i) (var "MkMonoid" `app` var f)]
30 |
31 | rhs : Con n vs -> TTImp
32 | rhs = injArgs explicit (const `(neutral))
33 |
34 | ||| Definition of a (local or top-level) function implementing
35 | ||| the neutral operation.
36 | export
37 | neutralDef : Name -> Con n vs -> Decl
38 | neutralDef f c = def f [patClause (var f) (rhs c)]
39 |
40 | --------------------------------------------------------------------------------
41 | --          Deriving
42 | --------------------------------------------------------------------------------
43 |
44 | ||| Generate declarations and implementations for `Semigroup` for a given data type.
45 | export
46 | MonoidVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
47 | MonoidVis vis nms p = case p.info.cons of
48 |   [c] =>
49 |     let fun  := funName p "neutral"
50 |         impl := implName p "Monoid"
51 |      in Right
52 |           [ TL (neutralClaim vis fun p) (neutralDef fun c)
53 |           , TL (monoidImplClaim vis impl p) (monoidImplDef fun impl)
54 |           ]
55 |   _   => failRecord "Monoid"
56 |
57 | ||| Alias for `MonoidVis Public`
58 | export %inline
59 | Monoid : List Name -> ParamTypeInfo -> Res (List TopLevel)
60 | Monoid = MonoidVis Public
61 |