0 | module Derive.Num
  1 |
  2 | import Language.Reflection.Util
  3 |
  4 | %default total
  5 |
  6 | --------------------------------------------------------------------------------
  7 | --          Claims
  8 | --------------------------------------------------------------------------------
  9 |
 10 | ||| Top-level declaration implementing used for `(+)` and `(*)` functions for
 11 | ||| the given data type.
 12 | export
 13 | pmClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 14 | pmClaim vis fun p =
 15 |   let arg := p.applied
 16 |       tpe := piAll `(~(arg) -> ~(arg) -> ~(arg)) (allImplicits p "Num")
 17 |    in simpleClaim vis fun tpe
 18 |
 19 | ||| Top-level declaration implementing used for the `fromInteger` function for
 20 | ||| the given data type.
 21 | export
 22 | fromIntClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 23 | fromIntClaim vis fun p =
 24 |   let arg := p.applied
 25 |       tpe := piAll `(Integer -> ~(arg)) (allImplicits p "Num")
 26 |    in simpleClaim vis fun tpe
 27 |
 28 | ||| Top-level declaration implementing the `Eq` interface for
 29 | ||| the given data type.
 30 | export
 31 | numImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
 32 | numImplClaim v impl p = implClaimVis v impl (implType "Num" p)
 33 |
 34 | --------------------------------------------------------------------------------
 35 | --          Definitions
 36 | --------------------------------------------------------------------------------
 37 |
 38 | numImplDef : (p, m, fi, impl : Name) -> Decl
 39 | numImplDef p m fi impl =
 40 |   def impl [patClause (var impl) (appNames "MkNum" [p,m,fi])]
 41 |
 42 | plus : BoundArg 2 Explicit -> TTImp
 43 | plus (BA arg [x,y] _)  = `(~(var x) + ~(var y))
 44 |
 45 | mult : BoundArg 2 Explicit -> TTImp
 46 | mult (BA arg [x,y] _)  = `(~(var x) * ~(var y))
 47 |
 48 | fromInt : BoundArg 0 Explicit -> TTImp
 49 | fromInt _ = `(fromInteger n)
 50 |
 51 | export
 52 | plusDef : Name -> Con n vs -> Decl
 53 | plusDef fun c =
 54 |   let clause := mapArgs2 explicit (\x,y => `(~(var fun) ~(x) ~(y))) plus c
 55 |    in def fun [clause]
 56 |
 57 | export
 58 | multDef : Name -> Con n vs -> Decl
 59 | multDef fun c =
 60 |   let clause := mapArgs2 explicit (\x,y => `(~(var fun) ~(x) ~(y))) mult c
 61 |    in def fun [clause]
 62 |
 63 | export
 64 | fromIntDef : Name -> Con n vs -> Decl
 65 | fromIntDef f c =
 66 |   def f [patClause `(~(var f) n) (injArgs explicit fromInt c)]
 67 |
 68 | --------------------------------------------------------------------------------
 69 | --          Deriving
 70 | --------------------------------------------------------------------------------
 71 |
 72 | ||| Generate declarations and implementations for `Num` for a
 73 | ||| single-constructor data type.
 74 | export
 75 | NumVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 76 | NumVis vis nms p = case p.info.cons of
 77 |   [c] =>
 78 |     let mult    := funName p "mult"
 79 |         plus    := funName p "plus"
 80 |         fromInt := funName p "fromInt"
 81 |         impl    := implName p "Num"
 82 |      in Right
 83 |           [ TL (pmClaim vis plus p) (plusDef plus c)
 84 |           , TL (pmClaim vis mult p) (multDef mult c)
 85 |           , TL (fromIntClaim vis fromInt p) (fromIntDef fromInt c)
 86 |           , TL (numImplClaim vis impl p) (numImplDef plus mult fromInt impl)
 87 |           ]
 88 |   _   => failRecord "Num"
 89 |
 90 | ||| Alias for `NumVis Public`
 91 | export %inline
 92 | Num : List Name -> ParamTypeInfo -> Res (List TopLevel)
 93 | Num = NumVis Public
 94 |
 95 | ||| Generate a single `fromInteger` function for the given type
 96 | export
 97 | FromIntegerVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 98 | FromIntegerVis vis nms p = case p.info.cons of
 99 |   [c] =>
100 |     let fun := the Name "fromInteger"
101 |      in Right [ TL (fromIntClaim vis fun p) (fromIntDef fun c) ]
102 |   _   => failRecord "fromInteger"
103 |
104 | ||| Generate a single `fromInteger` function with `public export`
105 | ||| visibility for the given type
106 | export %inline
107 | FromInteger : List Name -> ParamTypeInfo -> Res (List TopLevel)
108 | FromInteger = FromIntegerVis Public
109 |