0 | module Derive.TSV.Decoder
 1 |
 2 | import public Text.Parse.Manual
 3 | import public Text.Lex.Manual.Syntax
 4 | import Language.Reflection.Util
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          Claims
10 | --------------------------------------------------------------------------------
11 |
12 | ||| Top-level function declaration implementing the `decodeFrom` function for
13 | ||| the given data type.
14 | export
15 | decClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
16 | decClaim vis fun p =
17 |   let arg := p.applied
18 |       tpe := piAll `({0 e : Type} -> Tok False e ~(arg)) (allImplicits p "TSVDecoder")
19 |    in simpleClaim vis fun tpe
20 |
21 | ||| Top-level declaration implementing the `TSVDecoder` interface for
22 | ||| the given data type.
23 | export
24 | decoderImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
25 | decoderImplClaim v impl p = implClaimVis v impl (implType "TSVDecoder" p)
26 |
27 | --------------------------------------------------------------------------------
28 | --          Definitions
29 | --------------------------------------------------------------------------------
30 |
31 | export
32 | decoderImplDef : (fun, impl : Name) -> Decl
33 | decoderImplDef f i =
34 |   def i [patClause (var i) (var "MkTSVDecoder" `app` var f)]
35 |
36 | appArgs : TTImp -> List (BoundArg 0 Explicit) -> TTImp
37 | appArgs t []                = t
38 | appArgs t [BA _ [] _]       = `(Tok.(<*>) ~(t) decodeFrom)
39 | appArgs t (BA _ [] _ :: xs) =
40 |   appArgs `(Tok.(<*>) ~(t) (Tok.(<*) decodeFrom tab)) xs
41 |
42 | decClause : Name -> Con n vs -> Clause
43 | decClause f c =
44 |   let sx := boundArgs explicit c.args []
45 |    in patClause (var f) (appArgs `(Tok.pure ~(c.nameVar)) $ sx <>> [])
46 |
47 | decDef : Name -> Con n vs -> Decl
48 | decDef f c = def f [decClause f c]
49 |
50 | enumClause : Con n vs -> Clause
51 | enumClause c = patClause (c.namePrim) `(Just ~(c.nameVar))
52 |
53 | enumDef : Name -> ParamTypeInfo -> Decl
54 | enumDef f p =
55 |   let catchAll := patClause implicitTrue `(Nothing)
56 |       cls      := map enumClause p.info.cons ++ [catchAll]
57 |    in def f [patClause (var f) `(refine str $ \x => ~(iCase `(x) implicitFalse cls))]
58 |
59 | --------------------------------------------------------------------------------
60 | --          Deriving
61 | --------------------------------------------------------------------------------
62 |
63 | ||| Generate declarations and implementations for `Semigroup` for a given data type.
64 | export
65 | TSVDecoderVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
66 | TSVDecoderVis vis nms p =
67 |   let fun  := funName p "decodeFrom"
68 |       impl := implName p "TSVDecoder"
69 |    in case p.info.cons of
70 |         [c] =>
71 |           Right
72 |             [ TL (decClaim vis fun p) (decDef fun c)
73 |             , TL (decoderImplClaim vis impl p) (decoderImplDef fun impl)
74 |             ]
75 |         _   =>
76 |           case isEnum p.info of
77 |             False => failRecord "TSVDecoder"
78 |             True  =>
79 |               Right
80 |                 [ TL (decClaim vis fun p) (enumDef fun p)
81 |                 , TL (decoderImplClaim vis impl p) (decoderImplDef fun impl)
82 |             ]
83 |
84 | ||| Alias for `SemigroupVis Public`
85 | export %inline
86 | TSVDecoder : List Name -> ParamTypeInfo -> Res (List TopLevel)
87 | TSVDecoder = TSVDecoderVis Public
88 |