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