0 | module Derive.TSV.Encoder
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | ||| Top-level function declaration implementing the `encodeOnto` function for
11 | ||| the given data type.
12 | export
13 | encClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
14 | encClaim vis fun p =
15 |   let arg := p.applied
16 |       tpe := piAll `(SnocList String -> ~(arg) -> SnocList String) (allImplicits p "TSVEncoder")
17 |    in simpleClaim vis fun tpe
18 |
19 | ||| Top-level declaration implementing the `TSVEncoder` interface for
20 | ||| the given data type.
21 | export
22 | encoderImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
23 | encoderImplClaim v impl p = implClaimVis v impl (implType "TSVEncoder" p)
24 |
25 | --------------------------------------------------------------------------------
26 | --          Definitions
27 | --------------------------------------------------------------------------------
28 |
29 | export
30 | encoderImplDef : (fun, impl : Name) -> Decl
31 | encoderImplDef f i =
32 |   def i [patClause (var i) (var "MkTSVEncoder" `app` var f)]
33 |
34 | appArgs : TTImp -> List (BoundArg 1 Explicit) -> TTImp
35 | appArgs t []                 = t
36 | appArgs t (BA _ [x] _ :: xs) = appArgs `(encodeOnto ~(t) ~(var x)) xs
37 |
38 | encClause : Name -> Con n vs -> Clause
39 | encClause f c =
40 |   let xs := freshNames "x" c.arty
41 |       cx := bindCon c xs
42 |       sx := boundArgs explicit c.args [xs]
43 |    in patClause `(~(var f) sc ~(cx)) (appArgs `(sc) $ sx <>> [])
44 |
45 | enumClause : Name -> Con n vs -> Clause
46 | enumClause f c = patClause `(~(var f) sc ~(c.nameVar)) `(sc :< ~(c.namePrim))
47 |
48 | export
49 | encDef : Name -> Con n vs -> Decl
50 | encDef f c = def f [encClause f c]
51 |
52 | export
53 | enumDef : Name -> ParamTypeInfo -> Decl
54 | enumDef f c = def f (map (enumClause f) c.info.cons)
55 |
56 | --------------------------------------------------------------------------------
57 | --          Deriving
58 | --------------------------------------------------------------------------------
59 |
60 | ||| Generate declarations and implementations for `Semigroup` for a given data type.
61 | export
62 | TSVEncoderVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
63 | TSVEncoderVis vis nms p =
64 |   let fun  := funName p "encodeOnto"
65 |       impl := implName p "TSVEncoder"
66 |    in case p.info.cons of
67 |         [c] =>
68 |            Right
69 |              [ TL (encClaim vis fun p) (encDef fun c)
70 |              , TL (encoderImplClaim vis impl p) (encoderImplDef fun impl)
71 |              ]
72 |         _   =>
73 |           case isEnum p.info of
74 |             False => failRecord "TSVEncoder"
75 |             True  =>
76 |               Right
77 |                 [ TL (encClaim vis fun p) (enumDef fun p)
78 |                 , TL (encoderImplClaim vis impl p) (encoderImplDef fun impl)
79 |                 ]
80 |
81 | ||| Alias for `SemigroupVis Public`
82 | export %inline
83 | TSVEncoder : List Name -> ParamTypeInfo -> Res (List TopLevel)
84 | TSVEncoder = TSVEncoderVis Public
85 |