0 | module Derive.FromDouble
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | export
11 | fromDblClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | fromDblClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll `(Double -> ~(arg)) (allImplicits p "FromDouble")
15 |    in simpleClaim vis fun tpe
16 |
17 | ||| Top-level declaration implementing the `Eq` interface for
18 | ||| the given data type.
19 | export
20 | dblImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
21 | dblImplClaim v impl p = implClaimVis v impl (implType "FromDouble" p)
22 |
23 | --------------------------------------------------------------------------------
24 | --          Definitions
25 | --------------------------------------------------------------------------------
26 |
27 | dblImplDef : (fd, impl : Name) -> Decl
28 | dblImplDef fd impl =
29 |   def impl [patClause (var impl) (appNames "MkFromDouble" [fd])]
30 |
31 | export
32 | fromDblDef : Name -> Con n vs -> Decl
33 | fromDblDef f c =
34 |   let t := `(fromDouble n)
35 |    in def f [patClause (var f `app` bindVar "n") (injArgs explicit (const t) c)]
36 |
37 | --------------------------------------------------------------------------------
38 | --          Deriving
39 | --------------------------------------------------------------------------------
40 |
41 | ||| Generate declarations and implementations for `FromDouble` for a
42 | ||| single-constructor data type.
43 | export
44 | FromDoubleVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
45 | FromDoubleVis vis nms p = case p.info.cons of
46 |   [c] =>
47 |     let fun  := funName p "fromDouble"
48 |         impl := implName p "FromDouble"
49 |      in Right
50 |           [ TL (fromDblClaim vis fun p) (fromDblDef fun c)
51 |           , TL (dblImplClaim vis impl p) (dblImplDef fun impl)
52 |           ]
53 |   _   => failRecord "FromDouble"
54 |
55 | ||| Alias for `FromDoubleVis Public`
56 | export %inline
57 | FromDouble : List Name -> ParamTypeInfo -> Res (List TopLevel)
58 | FromDouble = FromDoubleVis Public
59 |