0 | module Derive.FromString
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | export
11 | fromStrClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | fromStrClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll `(String -> ~(arg)) (allImplicits p "FromString")
15 |    in simpleClaim vis fun tpe
16 |
17 | ||| Top-level declaration implementing the `FromString` interface for
18 | ||| the given data type.
19 | export
20 | strImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
21 | strImplClaim v impl p = implClaimVis v impl (implType "FromString" p)
22 |
23 | --------------------------------------------------------------------------------
24 | --          Definitions
25 | --------------------------------------------------------------------------------
26 |
27 | strImplDef : (fd, impl : Name) -> Decl
28 | strImplDef fd impl =
29 |   def impl [patClause (var impl) (appNames "MkFromString" [fd])]
30 |
31 | export
32 | fromStrDef : Name -> Con n vs -> Decl
33 | fromStrDef f c =
34 |   let t := `(fromString 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 `FromString` 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 | ||| `fromString 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 | FromStringVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
50 | FromStringVis vis nms p = case p.info.cons of
51 |   [c] =>
52 |     let fun  := funName p "fromString"
53 |         impl := implName p "FromString"
54 |      in Right
55 |           [ TL (fromStrClaim vis fun p) (fromStrDef fun c)
56 |           , TL (strImplClaim vis impl p) (strImplDef fun impl)
57 |           ]
58 |   _   => failRecord "FromString"
59 |
60 | ||| Alias for `FromStringVis Public`
61 | export %inline
62 | FromString : List Name -> ParamTypeInfo -> Res (List TopLevel)
63 | FromString = FromStringVis Public
64 |