2 | module Language.Reflection.Refined

  4 | import public Language.Reflection.Refined.Util

  5 | import Language.Reflection.Util

  7 | %default total

 32 | refinedEq : (type : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()

 33 | refinedEq dt t accessor =

 34 |   let eqFun := UN $ Basic $ "implEq" ++ dt

 35 |       acc   := var accessor

 37 |    in declare

 38 |         [ interfaceHint Public eqFun `(Eq ~(t))

 39 |         , def eqFun [patClause (var eqFun) `(mkEq ((==) `on` ~(acc)))]

 40 |         ]

 57 | refinedOrd : (dataType : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()

 58 | refinedOrd dt t accessor =

 59 |   let ordFun := UN $ Basic $ "implOrd"  ++ dt

 60 |       acc    := var accessor

 62 |    in declare

 63 |         [ interfaceHint Public ordFun `(Ord ~(t))

 64 |         , def ordFun [patClause (var ordFun) `(mkOrd (compare `on` ~(acc)))]

 65 |         ]

 82 | refinedShow : (type : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()

 83 | refinedShow dt t accessor =

 84 |   let showFun := UN $ Basic $ "implShow" ++ dt

 85 |       acc     := var accessor

 87 |    in declare

 88 |         [ interfaceHint Public showFun `(Show ~(t))

 89 |         , def showFun

 90 |             [patClause (var showFun) `(mkShowPrec (\p => showPrec p . ~(acc)))]

 91 |         ]

 96 | refinedEqOrdShow :

 97 |      (type : String)

 98 |   -> (dt : TTImp)

 99 |   -> (accessor : Name)

100 |   -> Elab ()

101 | refinedEqOrdShow dt t acc = do

102 |   refinedEq dt t acc

103 |   refinedOrd dt t acc

104 |   refinedShow dt t acc

149 | refinedIntegral :

150 |      (type : String)

151 |   -> (dt       : TTImp)

152 |   -> (con      : Name)

153 |   -> (accessor : Name)

154 |   -> (tpe      : TTImp)

155 |   -> Elab ()

156 | refinedIntegral dt t con acc tpe =

157 |   let ns := MkNS [dt]

159 |       -- this has to be namespaced

160 |       -- to avoid disambiguities when being used

161 |       -- in fromInteger

162 |       refineNS := var $ NS ns (UN $ Basic "refine")

164 |    in refinedEqOrdShow dt t acc >>

165 |       declare

166 |         [ INamespace EmptyFC ns

167 |           `[ public export

168 |              refine : ~(tpe) -> Maybe ~(t)

169 |              refine = refineSo ~(var con)

171 |              public export

172 |              fromInteger :

173 |                   (n : Integer)

174 |                -> {auto 0 _: IsJust (~(refineNS) $ fromInteger n)}

175 |                -> ~(t)

176 |              fromInteger n = fromJust (refine $ fromInteger n)

177 |            ]

178 |         ]

181 | refinedIntegralDflt : (type : String) -> (tpe : TTImp) -> Elab ()

182 | refinedIntegralDflt dt tpe =

183 |   refinedIntegral dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value} tpe

201 | refinedInt : (type : String) -> Elab ()

202 | refinedInt dt = refinedIntegralDflt dt `(Int)

211 | refinedBits8 : (type : String) -> Elab ()

212 | refinedBits8 dt = refinedIntegralDflt dt `(Bits8)

221 | refinedBits16 : (type : String) -> Elab ()

222 | refinedBits16 dt = refinedIntegralDflt dt `(Bits16)

231 | refinedBits32 : (type : String) -> Elab ()

232 | refinedBits32 dt = refinedIntegralDflt dt `(Bits32)

241 | refinedBits64 : (type : String) -> Elab ()

242 | refinedBits64 dt = refinedIntegralDflt dt `(Bits64)

251 | refinedInt8 : (type : String) -> Elab ()

252 | refinedInt8 dt = refinedIntegralDflt dt `(Int8)

261 | refinedInt16 : (type : String) -> Elab ()

262 | refinedInt16 dt = refinedIntegralDflt dt `(Int16)

271 | refinedInt32 : (type : String) -> Elab ()

272 | refinedInt32 dt = refinedIntegralDflt dt `(Int32)

281 | refinedInt64 : (type : String) -> Elab ()

282 | refinedInt64 dt = refinedIntegralDflt dt `(Int64)

323 | refinedFloating :

324 |      (type : String)

325 |   -> (dt       : TTImp)

326 |   -> (con      : Name)

327 |   -> (accessor : Name)

328 |   -> Elab ()

329 | refinedFloating dt t con acc =

330 |   let ns := MkNS [dt]

332 |       -- this has to be namespaced

333 |       -- to avoid disambiguities when being used

334 |       -- in fromInteger

335 |       refineNS := var $ NS ns (UN $ Basic "refine")

337 |    in refinedEqOrdShow dt t acc >>

338 |       declare

339 |         [ INamespace EmptyFC ns

340 |           `[ public export

341 |              refine : Double -> Maybe ~(t)

342 |              refine = refineSo ~(var con)

344 |              public export

345 |              fromDouble :

346 |                   (n : Double)

347 |                -> {auto 0 _: IsJust (~(refineNS) n)}

348 |                -> ~(t)

349 |              fromDouble n = fromJust (refine n)

350 |            ]

351 |         ]

360 | refinedDouble : (type : String) -> Elab ()

361 | refinedDouble dt =

362 |   refinedFloating dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}

402 | refinedText :

403 |      (type : String)

404 |   -> (dt       : TTImp)

405 |   -> (con      : Name)

406 |   -> (accessor : Name)

407 |   -> Elab ()

408 | refinedText dt t con acc =

409 |   let ns := MkNS [dt]

411 |       -- this has to be namespaced

412 |       -- to avoid disambiguities when being used

413 |       -- in fromInteger

414 |       refineNS := var $ NS ns (UN $ Basic "refine")

416 |    in refinedEqOrdShow dt t acc >>

417 |       declare

418 |         [ INamespace EmptyFC ns

419 |           `[ public export

420 |              refine : String -> Maybe ~(t)

421 |              refine = refineSo ~(var con)

423 |              public export

424 |              fromString :

425 |                   (n : String)

426 |                -> {auto 0 _: IsJust (~(refineNS) n)}

427 |                -> ~(t)

428 |              fromString n = fromJust (refine n)

429 |            ]

430 |         ]

439 | refinedString : (type : String) -> Elab ()

440 | refinedString dt = refinedText dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}

480 | refinedCharacter :

481 |      (type : String)

482 |   -> (dt       : TTImp)

483 |   -> (con      : Name)

484 |   -> (accessor : Name)

485 |   -> Elab ()

486 | refinedCharacter dt t con acc =

487 |   let ns := MkNS [dt]

489 |       -- this has to be namespaced

490 |       -- to avoid disambiguities when being used

491 |       -- in fromInteger

492 |       refineNS := var $ NS ns (UN $ Basic "refine")

494 |    in refinedEqOrdShow dt t acc >>

495 |       declare

496 |         [ INamespace EmptyFC ns

497 |           `[ public export

498 |              refine : Char -> Maybe ~(t)

499 |              refine = refineSo ~(var con)

501 |              public export

502 |              fromChar :

503 |                   (n : Char)

504 |                -> {auto 0 _: IsJust (~(refineNS) n)}

505 |                -> ~(t)

506 |              fromChar n = fromJust (refine n)

507 |            ]

508 |         ]

517 | refinedChar : (type : String) -> Elab ()

518 | refinedChar dt =

519 |   refinedCharacter dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}