0 | module Derive.Sqlite3.ToRow
 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 | rowsTypes : Vect n Name -> ParamCon n -> TTImp
13 | rowsTypes vs (MkParamCon _ _ args) = foldr acc `(Prelude.Nil) args
14 |   where
15 |     acc : ConArg n -> TTImp -> TTImp
16 |     acc (CArg _ MW _ t) s = `(Prelude.List.(++) (ToRowTypes ~(ttimp vs t)) ~(s))
17 |     acc _               s = s
18 |
19 | ||| Top-level declaration of the `ToCell` implementation for the given data type.
20 | export
21 | toRowImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
22 | toRowImplClaim impl p = implClaim impl (implType "ToRow" p)
23 |
24 | --------------------------------------------------------------------------------
25 | --          Definitions
26 | --------------------------------------------------------------------------------
27 |
28 | appList : SnocList TTImp -> TTImp
29 | appList = foldr acc `(Data.List.Quantifiers.All.Nil)
30 |   where
31 |     acc : TTImp -> TTImp -> TTImp
32 |     acc t s = `(Data.List.Quantifiers.All.(++) ~(t) ~(s))
33 |
34 | x : Name
35 | x = "x"
36 |
37 | matchEither : String -> (res : TTImp) -> Name -> TTImp
38 | matchEither x res y =
39 |   `(case fromCell ~(varStr x) of
40 |      Right ~(bindVar y) => ~(res)
41 |      Left e             => Left e)
42 |
43 | parameters (nms : List Name)
44 |
45 |   toRowClause : Con n vs -> Clause
46 |   toRowClause =
47 |     accumArgs regular id appList (\(BA _ [x] _) => `(toRow ~(var x)))
48 |
49 |   to : Con n vs -> TTImp
50 |   to c =
51 |     lam (lambdaArg x) $ iCase (var x) implicitFalse [toRowClause c]
52 |
53 |   toRowDef : Name -> (rowTypes : TTImp) -> Con n vs -> Decl
54 |   toRowDef f rowTypes c =
55 |     def f [patClause (var f) `(MkToRow ~(rowTypes) ~(to c))]
56 |
57 | --------------------------------------------------------------------------------
58 | --          Deriving
59 | --------------------------------------------------------------------------------
60 |
61 | ||| Generate declarations and implementations for `ToRow` for a given
62 | ||| record type using default settings.
63 | export
64 | ToRow : List Name -> ParamTypeInfo -> Res (List TopLevel)
65 | ToRow nms p =
66 |   case (p.cons, p.info.cons) of
67 |     ([c],[d]) =>
68 |       let impl     := implName p "ToRow"
69 |           rowTypes := rowsTypes p.paramNames c
70 |        in Right [ TL (toRowImplClaim impl p) (toRowDef nms impl rowTypes d) ]
71 |     _   => failRecord "ToRow"
72 |