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