0 | module Derive.Semigroup
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | ||| Top-level function declaration implementing the append function for
11 | ||| the given data type.
12 | export
13 | appClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
14 | appClaim vis fun p =
15 |   let arg := p.applied
16 |       tpe := piAll `(~(arg) -> ~(arg) -> ~(arg)) (allImplicits p "Semigroup")
17 |    in simpleClaim vis fun tpe
18 |
19 | ||| Top-level declaration implementing the `Semigroup` interface for
20 | ||| the given data type.
21 | export
22 | semigroupImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
23 | semigroupImplClaim v impl p = implClaimVis v impl (implType "Semigroup" p)
24 |
25 | --------------------------------------------------------------------------------
26 | --          Definitions
27 | --------------------------------------------------------------------------------
28 |
29 | export
30 | semigroupImplDef : (fun, impl : Name) -> Decl
31 | semigroupImplDef f i =
32 |   def i [patClause (var i) (var "MkSemigroup" `app` var f)]
33 |
34 | app : BoundArg 2 Explicit -> TTImp
35 | app (BA _ [x,y] _) = `(~(var x) <+> ~(var y))
36 |
37 | appClause : Name -> Con n vs -> Clause
38 | appClause f = mapArgs2 explicit (\x,y => `(~(var f) ~(x) ~(y))) app
39 |
40 | export
41 | appDef : Name -> Con n vs -> Decl
42 | appDef f c = def f [appClause f c]
43 |
44 | --------------------------------------------------------------------------------
45 | --          Deriving
46 | --------------------------------------------------------------------------------
47 |
48 | ||| Generate declarations and implementations for `Semigroup` for a given data type.
49 | export
50 | SemigroupVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
51 | SemigroupVis vis nms p = case p.info.cons of
52 |   [c] =>
53 |     let fun  := funName p "append"
54 |         impl := implName p "Semigroup"
55 |      in Right
56 |           [ TL (appClaim vis fun p) (appDef fun c)
57 |           , TL (semigroupImplClaim vis impl p) (semigroupImplDef fun impl)
58 |           ]
59 |   _   => failRecord "Semigroup"
60 |
61 | ||| Alias for `SemigroupVis Public`
62 | export %inline
63 | Semigroup : List Name -> ParamTypeInfo -> Res (List TopLevel)
64 | Semigroup = SemigroupVis Public
65 |