0 | module Derive.Refined.JSON
 1 |
 2 | import public Derive.Refined
 3 | import public JSON.Simple.Derive
 4 | import Language.Reflection.Util
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          ToJSON
10 | --------------------------------------------------------------------------------
11 |
12 | export
13 | refinedToJsonDef : (fun : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl
14 | refinedToJsonDef fun (MkParamTypeInfo _ _ _ [c] _) (RI x) =
15 |   def fun [patClause (var fun) `(toJSON . ~(var $ valName c.args x))]
16 |
17 | ||| Generate declarations and implementations for
18 | ||| `FromJSON` for a given refinement type.
19 | export
20 | RefinedToJSONVis :
21 |      Visibility
22 |   -> List Name
23 |   -> ParamTypeInfo
24 |   -> Res (List TopLevel)
25 | RefinedToJSONVis vis ns p = map decls $ refinedInfo p
26 |
27 |   where
28 |     decls : RefinedInfo p -> List TopLevel
29 |     decls ri =
30 |       let fun  := funName p "toJson"
31 |           impl := implName p "ToJSON"
32 |        in [ TL (toJsonClaim vis fun p)
33 |                (refinedToJsonDef fun p ri)
34 |           , TL (toJsonImplClaim vis impl p) (toJsonImplDef fun impl)
35 |             ]
36 |
37 | export %inline
38 | RefinedToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
39 | RefinedToJSON = RefinedToJSONVis Export
40 |
41 | --------------------------------------------------------------------------------
42 | --          FromJSON
43 | --------------------------------------------------------------------------------
44 |
45 | public export
46 | refineFromJSON : FromJSON a => String -> (a -> Maybe b) -> Parser JSON b
47 | refineFromJSON str f v = case fromJSON v of
48 |   Right va => case f va of
49 |     Just vb => Right vb
50 |     Nothing => fail "refining \{str} failed: \{show v}"
51 |   Left s   => prependContext str $ Left s
52 |
53 | export
54 | refinedFromJsonDef : (fun,typeName, refineName : Name) -> Decl
55 | refinedFromJsonDef fun tn rn =
56 |   def fun [patClause (var fun) `(refineFromJSON ~(tn.namePrim) ~(var rn))]
57 |
58 | ||| Generate declarations and implementations for
59 | ||| `FromJSON` for a given refinement type.
60 | export
61 | RefinedFromJSONVis :
62 |      Visibility
63 |   -> List Name
64 |   -> ParamTypeInfo
65 |   -> Res (List TopLevel)
66 | RefinedFromJSONVis vis ns p = map decls $ refinedInfo p
67 |
68 |   where
69 |     decls : RefinedInfo p -> List TopLevel
70 |     decls _ =
71 |       let fun  := funName p "fromJson"
72 |           impl := implName p "FromJSON"
73 |           refn := refineName p
74 |        in [ TL (fromJsonClaim vis fun p)
75 |                (refinedFromJsonDef fun p.getName refn)
76 |           , TL (fromJsonImplClaim vis impl p) (fromJsonImplDef fun impl)
77 |             ]
78 |
79 | export %inline
80 | RefinedFromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
81 | RefinedFromJSON = RefinedFromJSONVis Export
82 |
83 | --------------------------------------------------------------------------------
84 | --          JSON
85 | --------------------------------------------------------------------------------
86 |
87 | ||| Generate declarations and implementations for
88 | ||| `FromJSON` and `ToJSON` for a given refinement type.
89 | export %inline
90 | RefinedJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
91 | RefinedJSON ns p = sequenceJoin [RefinedToJSON ns p, RefinedFromJSON ns p]
92 |