0 | module Derive.Sqlite3.FromRow
 1 |
 2 | import Derive.Sqlite3.ToRow
 3 | import Sqlite3.Marshall
 4 | import Sqlite3.Types
 5 | import Language.Reflection.Util
 6 |
 7 | %default total
 8 |
 9 | --------------------------------------------------------------------------------
10 | --          Claims
11 | --------------------------------------------------------------------------------
12 |
13 | flatTypes : Vect n Name -> ParamCon n -> TTImp
14 | flatTypes vs (MkParamCon _ _ args) = foldr acc `(Prelude.Nil) args
15 |   where
16 |     acc : ConArg n -> TTImp -> TTImp
17 |     acc (CArg _ MW _ t) s = `(Prelude.List.(++) (FromRowTypes ~(ttimp vs t)) ~(s))
18 |     acc _               s = s
19 |
20 | rowsTypes : Vect n Name -> ParamCon n -> TTImp
21 | rowsTypes vs (MkParamCon _ _ args) = foldr acc `(Prelude.Nil) args
22 |   where
23 |     acc : ConArg n -> TTImp -> TTImp
24 |     acc (CArg _ MW _ t) s = `(Prelude.(::) (FromRowTypes ~(ttimp vs t)) ~(s))
25 |     acc _               s = s
26 |
27 | ||| Top-level declaration of the `FromCell` implementation for the given data type.
28 | export
29 | fromRowImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
30 | fromRowImplClaim impl p = implClaim impl (implType "FromRow" p)
31 |
32 | --------------------------------------------------------------------------------
33 | --          Definitions
34 | --------------------------------------------------------------------------------
35 |
36 | x : Name
37 | x = "x"
38 |
39 | matchEither : Name -> (res : TTImp) -> Name -> TTImp
40 | matchEither x res y =
41 |   `(case fromRow ~(var x) of
42 |      Right ~(bindVar y) => ~(res)
43 |      Left e             => Left e)
44 |
45 | parameters (nms : List Name)
46 |   fromLHS : SnocList (BoundArg 2 Regular) -> TTImp
47 |   fromLHS = foldr acc `(Data.List.Quantifiers.All.Nil)
48 |     where
49 |       acc : BoundArg 2 Regular -> TTImp -> TTImp
50 |       acc (BA _ [x,_] _) t = `(Data.List.Quantifiers.All.(::) ~(bindVar x) ~(t))
51 |
52 |
53 |   fromRHS : SnocList (BoundArg 2 Regular) -> TTImp -> TTImp
54 |   fromRHS [<]                    res = res
55 |   fromRHS (sx :< (BA a [x,y] _)) res = fromRHS sx (matchEither x res y)
56 |
57 |   fromRowClause : Con n vs -> Clause
58 |   fromRowClause c =
59 |     let xs      := freshNames "x" c.arty
60 |         ys      := freshNames "y" c.arty
61 |         args    := boundArgs regular c.args [xs,ys]
62 |         applied := appAll c.name (map (\(BA _ [_,y] _) => var y) args <>> [])
63 |      in patClause (fromLHS args) (fromRHS args $ app `(Right) applied)
64 |
65 |   from : TTImp -> Con n vs -> TTImp
66 |   from rowTypes c =
67 |     lam (lambdaArg x) $
68 |       iCase
69 |         `(splitAll ~(rowTypes) ~(var x))
70 |         implicitFalse
71 |         [fromRowClause c]
72 |
73 |   fromRowDef : Name -> (ft,rt : TTImp) -> Con n vs -> Decl
74 |   fromRowDef f ft rt c =
75 |     def f [patClause (var f) `(MkFromRow ~(ft) ~(from rt c))]
76 |
77 | --------------------------------------------------------------------------------
78 | --          Deriving
79 | --------------------------------------------------------------------------------
80 |
81 | ||| Generate declarations and implementations for `FromRow` for a given
82 | ||| record type using default settings.
83 | export
84 | FromRow : List Name -> ParamTypeInfo -> Res (List TopLevel)
85 | FromRow nms p =
86 |   case (p.cons, p.info.cons) of
87 |     ([c],[d]) =>
88 |       let impl     := implName p "FromRow"
89 |           ft       := flatTypes p.paramNames c
90 |           rt       := rowsTypes p.paramNames c
91 |        in Right [ TL (fromRowImplClaim impl p) (fromRowDef nms impl ft rt d) ]
92 |     _   => failRecord "FromRow"
93 |