0 | module Derive.Literal
  1 |
  2 | import public Derive.Refined
  3 | import Language.Reflection.Util
  4 |
  5 | %default total
  6 |
  7 | export
  8 | litImplDef : (impl, fun, con : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl
  9 | litImplDef impl fun con (MkParamTypeInfo ti q ns [c] s) (RI x) =
 10 |   let p    := MkParamTypeInfo ti q ns [c] s
 11 |       arg  := p.applied
 12 |       vfun := var fun
 13 |       res  := appCon (vfun `app` varStr "n") c x
 14 |       prf  := `(fromJust0 (hdec0 {p = ~(proofType ns c.args x)} (~(vfun) n)))
 15 |       pred := `(\v => IsJust0 (hdec0 {p = ~(proofType ns c.args x)} (~(vfun) v)))
 16 |       rhs  := `(~(var con) (~pred) (\n,_ => let 0 prf := ~(prf) in ~(res)))
 17 |
 18 |    in def impl [ patClause (var impl) rhs ]
 19 |
 20 | export
 21 | litDef : (impl, fun, con : Name) -> Con n vs -> Decl
 22 | litDef impl fun con c =
 23 |   let t   := `(~(var fun) n)
 24 |       rhs := `(~(var con) (\n => ~(injArgs explicit (const t) c)))
 25 |    in def impl [patClause (var impl) rhs]
 26 |
 27 | --------------------------------------------------------------------------------
 28 | --          Derive
 29 | --------------------------------------------------------------------------------
 30 |
 31 | litOnly :
 32 |      (iface    : String)
 33 |   -> (smartCon : Name)
 34 |   -> (plainCon : Name)
 35 |   -> (conv     : Name)
 36 |   -> Visibility
 37 |   -> List Name
 38 |   -> ParamTypeInfo
 39 |   -> Res (List TopLevel)
 40 | litOnly iface smartCon plainCon conv vis nms p =
 41 |   case refinedInfo p of
 42 |     Right r => Right $ decls r
 43 |     Left  x => case p.info.cons of
 44 |       [c] =>
 45 |         let impl := implName p iface
 46 |          in Right [TL implClm (litDef impl conv plainCon c)]
 47 |       _   => failRecord "IntegerLit"
 48 |   where
 49 |     implNm  : Name
 50 |     implNm = implName p iface
 51 |
 52 |     implClm : Decl
 53 |     implClm = implClaimVis Public implNm (implType (fromString iface) p)
 54 |
 55 |     decls : RefinedInfo p -> List TopLevel
 56 |     decls x =
 57 |       let fun  := refineName p.getName
 58 |        in [TL implClm (litImplDef implNm conv smartCon p x)]
 59 |
 60 | litVis :
 61 |      (iface    : String)
 62 |   -> (smartCon : Name)
 63 |   -> (plainCon : Name)
 64 |   -> (conv     : Name)
 65 |   -> Visibility
 66 |   -> List Name
 67 |   -> ParamTypeInfo
 68 |   -> Res (List TopLevel)
 69 | litVis iface smartCon plainCon conv vis nms p =
 70 |   case refinedInfo p of
 71 |     Right r => Right $ decls r
 72 |     Left  x => case p.info.cons of
 73 |       [c] =>
 74 |         let impl := implName p iface
 75 |          in Right [TL implClm (litDef impl conv plainCon c)]
 76 |       _   => failRecord "IntegerLit"
 77 |   where
 78 |     implNm  : Name
 79 |     implNm = implName p iface
 80 |
 81 |     implClm : Decl
 82 |     implClm = implClaimVis Public implNm (implType (fromString iface) p)
 83 |
 84 |     decls : RefinedInfo p -> List TopLevel
 85 |     decls x =
 86 |       let fun  := refineName p.getName
 87 |        in [ refineTL fun p x
 88 |           , TL implClm (litImplDef implNm conv smartCon p x)
 89 |           ]
 90 |
 91 | export
 92 | IntegerLitVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 93 | IntegerLitVis = litVis "IntegerLit" "mkIL" "ilPlain" "fromInteger"
 94 |
 95 | export %inline
 96 | IntegerLit : List Name -> ParamTypeInfo -> Res (List TopLevel)
 97 | IntegerLit = IntegerLitVis Export
 98 |
 99 | export
100 | StringLitVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
101 | StringLitVis = litVis "StringLit" "mkSL" "slPlain" "fromString"
102 |
103 | export %inline
104 | StringLit : List Name -> ParamTypeInfo -> Res (List TopLevel)
105 | StringLit = StringLitVis Export
106 |
107 | export
108 | CharLitVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
109 | CharLitVis = litVis "CharLit" "mkCL" "clPlain" "fromChar"
110 |
111 | export %inline
112 | CharLit : List Name -> ParamTypeInfo -> Res (List TopLevel)
113 | CharLit = CharLitVis Export
114 |
115 | export
116 | DoubleLitVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
117 | DoubleLitVis v ns p =
118 |   [| List.(++)
119 |        (litVis "DoubleLit" "mkDL" "dlPlain" "fromDouble" v ns p)
120 |        (litOnly "IntegerLit" "mkIL" "ilPlain" "fromInteger" v ns p)
121 |   |]
122 |
123 | export %inline
124 | DoubleLit : List Name -> ParamTypeInfo -> Res (List TopLevel)
125 | DoubleLit = DoubleLitVis Export
126 |