0 | module Derive.Neg
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | export
11 | minusClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | minusClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll `(~(arg) -> ~(arg) -> ~(arg)) (allImplicits p "Neg")
15 |    in simpleClaim vis fun tpe
16 |
17 | export
18 | negClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
19 | negClaim vis fun p =
20 |   let arg := p.applied
21 |       tpe := piAll `(~(arg) -> ~(arg)) (allImplicits p "Neg")
22 |    in simpleClaim vis fun tpe
23 |
24 | export
25 | negImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
26 | negImplClaim v impl p = implClaimVis v impl (implType "Neg" p)
27 |
28 | --------------------------------------------------------------------------------
29 | --          Definitions
30 | --------------------------------------------------------------------------------
31 |
32 | negImplDef : (neg, min, impl : Name) -> Decl
33 | negImplDef neg min impl =
34 |   def impl [patClause (var impl) (appNames "MkNeg" [neg, min])]
35 |
36 | minus : BoundArg 2 Explicit -> TTImp
37 | minus (BA arg [x,y] _)  = `(~(var x) - ~(var y))
38 |
39 | neg : BoundArg 1 Explicit -> TTImp
40 | neg (BA arg [x] _)  = `(negate ~(var x))
41 |
42 | export
43 | minusDef : Name -> Con n vs -> Decl
44 | minusDef fun c =
45 |   let clause := mapArgs2 explicit (\x,y => `(~(var fun) ~(x) ~(y))) minus c
46 |    in def fun [clause]
47 |
48 | export
49 | negDef : Name -> Con n vs -> Decl
50 | negDef fun c =
51 |   let clause := mapArgs explicit (var fun `app`) neg c
52 |    in def fun [clause]
53 |
54 | --------------------------------------------------------------------------------
55 | --          Deriving
56 | --------------------------------------------------------------------------------
57 |
58 | ||| Generate declarations and implementations for `Neg` for a
59 | ||| single-constructor data type.
60 | export
61 | NegVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
62 | NegVis vis nms p = case p.info.cons of
63 |   [c] =>
64 |     let neg   := funName p "negate"
65 |         minus := funName p "minus"
66 |         impl  := implName p "Neg"
67 |      in Right
68 |         [ TL (negClaim vis neg p) (negDef neg c)
69 |         , TL (minusClaim vis minus p) (minusDef minus c)
70 |         , TL (negImplClaim vis impl p) (negImplDef neg minus impl)
71 |         ]
72 |   _   => failRecord "Neg"
73 |
74 | ||| Alias for `NegVis Public`
75 | export %inline
76 | Neg : List Name -> ParamTypeInfo -> Res (List TopLevel)
77 | Neg = NegVis Public
78 |