0 | module Derive.Sqlite3.ToCell
 1 |
 2 | import Sqlite3.Marshall
 3 | import Sqlite3.Types
 4 | import Language.Reflection.Util
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          Claims
10 | --------------------------------------------------------------------------------
11 |
12 | cellType : Vect n Name -> ParamCon n -> Maybe TTImp
13 | cellType vs (MkParamCon _ _ args) =
14 |   case mapMaybe convert $ toList args of
15 |     [t] => Just `(ToCellType ~(t))
16 |     _   => Nothing
17 |   where
18 |     convert : ConArg n -> Maybe TTImp
19 |     convert (CArg _ MW _ t) = Just $ ttimp vs t
20 |     convert _               = Nothing
21 |
22 | ||| Top-level declaration of the `ToCell` implementation for the given
23 | ||| data type.
24 | export
25 | toCellImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
26 | toCellImplClaim impl p = implClaim impl (implType "ToCell" p)
27 |
28 | --------------------------------------------------------------------------------
29 | --          Definitions
30 | --------------------------------------------------------------------------------
31 |
32 | x : Name
33 | x = "x"
34 |
35 | parameters (nms : List Name)
36 |   encEnumClause : Con n vs -> Clause
37 |   encEnumClause c = patClause (var c.name) `(Just ~(c.namePrim))
38 |
39 |   encEnum : TypeInfo -> TTImp
40 |   encEnum ti =
41 |     lam (lambdaArg x) $ iCase (var x) (var ti.name) (map encEnumClause ti.cons)
42 |
43 |   toCellEnumDef : Name -> TypeInfo -> Decl
44 |   toCellEnumDef f ti =
45 |     def f [patClause (var f) `(MkToCell TEXT ~(encEnum ti))]
46 |
47 |   encNT : ParamCon n -> TTImp
48 |   encNT c =
49 |     lam (lambdaArg x) $ iCase (var x) implicitFalse
50 |       [patClause `(~(var c.name) y) `(toCell y)]
51 |
52 |   toCellNewtypeDef : Name -> TTImp -> ParamCon n -> Decl
53 |   toCellNewtypeDef f ct c =
54 |     def f [patClause (var f) `(MkToCell ~(ct) ~(encNT c))]
55 |
56 | --------------------------------------------------------------------------------
57 | --          Deriving
58 | --------------------------------------------------------------------------------
59 |
60 | ||| Generate declarations and implementations for `ToJSON` for a given data type
61 | ||| using default settings.
62 | export %inline
63 | ToCell : List Name -> ParamTypeInfo -> Res (List TopLevel)
64 | ToCell nms p =
65 |  let impl := implName p "ToCell"
66 |   in if isEnum p.info
67 |         then
68 |           Right [ TL (toCellImplClaim impl p) (toCellEnumDef nms impl p.info) ]
69 |      else
70 |        case p.cons of
71 |          [c] =>
72 |             case cellType p.paramNames c of
73 |               Just ct => Right [ TL (toCellImplClaim impl p) (toCellNewtypeDef nms impl ct c) ]
74 |               Nothing => Left "Interface ToCell can only be derived for enumerations and newtypes."
75 |          _   => Left "Interface ToCell can only be derived for enumerations and newtypes."
76 |