0 | module Derive.FromChar
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | export
11 | fromChrClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | fromChrClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll `(Char -> ~(arg)) (allImplicits p "FromChar")
15 |    in simpleClaim vis fun tpe
16 |
17 | ||| Top-level declaration implementing the `FromChar` interface for
18 | ||| the given data type.
19 | export
20 | chrImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
21 | chrImplClaim v impl p = implClaimVis v impl (implType "FromChar" p)
22 |
23 | --------------------------------------------------------------------------------
24 | --          Definitions
25 | --------------------------------------------------------------------------------
26 |
27 | chrImplDef : (fd, impl : Name) -> Decl
28 | chrImplDef fd impl =
29 |   def impl [patClause (var impl) (appNames "MkFromChar" [fd])]
30 |
31 | export
32 | fromChrDef : Name -> Con n vs -> Decl
33 | fromChrDef f c =
34 |   let t := `(fromChar 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 `FromChar` for a
42 | ||| single-constructor data type.
43 | |||
44 | ||| All fields of the data type will be filled with the result of a call to
45 | ||| `fromChar s`, where `s` is the string to be used. This makes mostly
46 | ||| sense for newtypes, but is supported for any single-constructor data type
47 | ||| to be consistent with restrictions on `Num` and `FromDouble`.
48 | export
49 | FromCharVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
50 | FromCharVis vis nms p = case p.info.cons of
51 |   [c] =>
52 |     let fun  := funName p "fromChar"
53 |         impl := implName p "FromChar"
54 |      in Right
55 |           [ TL (fromChrClaim vis fun p) (fromChrDef fun c)
56 |           , TL (chrImplClaim vis impl p) (chrImplDef fun impl)
57 |           ]
58 |   _   => failRecord "FromChar"
59 |
60 | ||| Alias for `FromCharVis Public`
61 | export %inline
62 | FromChar : List Name -> ParamTypeInfo -> Res (List TopLevel)
63 | FromChar = FromCharVis Public
64 |