0 | module Derive.Refined.TSV
 1 |
 2 | import public Derive.Refined
 3 | import public Derive.TSV
 4 | import Language.Reflection.Util
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          TSVEncoder
10 | --------------------------------------------------------------------------------
11 |
12 | export
13 | refinedEncDef : (fun : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl
14 | refinedEncDef fun (MkParamTypeInfo _ _ _ [c] _) (RI x) =
15 |   def fun [patClause `(~(var fun) sc) `(encodeOnto sc . ~(var $ valName c.args x))]
16 |
17 | ||| Generate declarations and implementations for
18 | ||| `FromJSON` for a given refinement type.
19 | export
20 | RefinedTSVEncoderVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
21 | RefinedTSVEncoderVis vis ns p = map decls $ refinedInfo p
22 |
23 |   where
24 |     decls : RefinedInfo p -> List TopLevel
25 |     decls ri =
26 |       let fun  := funName p "encodeOnto"
27 |           impl := implName p "TSVEncoder"
28 |        in [ TL (encClaim vis fun p) (refinedEncDef fun p ri)
29 |           , TL (encoderImplClaim vis impl p) (encoderImplDef fun impl)
30 |           ]
31 |
32 | ||| Generate declarations and implementations for
33 | ||| `FromJSON` for a given refinement type.
34 | export %inline
35 | RefinedTSVEncoder : List Name -> ParamTypeInfo -> Res (List TopLevel)
36 | RefinedTSVEncoder = RefinedTSVEncoderVis Export
37 |
38 | --------------------------------------------------------------------------------
39 | --          TSVDecoder
40 | --------------------------------------------------------------------------------
41 |
42 | export
43 | refinedDecDef : (fun, refineName : Name) -> Decl
44 | refinedDecDef fun rn =
45 |   def fun [patClause (var fun) `(refine decodeFrom ~(var rn))]
46 |
47 | ||| Generate declarations and implementations for
48 | ||| `TSVDecoder` for a given refinement type.
49 | export
50 | RefinedTSVDecoderVis :
51 |      Visibility
52 |   -> List Name
53 |   -> ParamTypeInfo
54 |   -> Res (List TopLevel)
55 | RefinedTSVDecoderVis vis ns p = map decls $ refinedInfo p
56 |
57 |   where
58 |     decls : RefinedInfo p -> List TopLevel
59 |     decls _ =
60 |       let fun  := funName p "decodeFrom"
61 |           impl := implName p "TSVDecoder"
62 |           refn := refineName p
63 |        in [ TL (decClaim vis fun p) (refinedDecDef fun refn)
64 |           , TL (decoderImplClaim vis impl p) (decoderImplDef fun impl)
65 |           ]
66 |
67 | ||| Generate declarations and implementations for
68 | ||| `TSVDecoder` for a given refinement type.
69 | export %inline
70 | RefinedTSVDecoder : List Name -> ParamTypeInfo -> Res (List TopLevel)
71 | RefinedTSVDecoder = RefinedTSVDecoderVis Export
72 |
73 | --------------------------------------------------------------------------------
74 | --          TSV
75 | --------------------------------------------------------------------------------
76 |
77 | ||| Generate declarations and implementations for
78 | ||| `TSVDecoder` and `TSVEncoder` for a given refinement type.
79 | export %inline
80 | RefinedTSV : List Name -> ParamTypeInfo -> Res (List TopLevel)
81 | RefinedTSV ns p = sequenceJoin [RefinedTSVEncoder ns p, RefinedTSVDecoder ns p]
82 |