0 | module Derive.RecordB
 1 |
 2 | import Language.Reflection.Util
 3 | import Derive.BarbieInfo
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | --          Claims
 9 | --------------------------------------------------------------------------------
10 |
11 | blensTpe : (k : TTImp) -> TTImp -> TTImp
12 | blensTpe k arg =
13 |   `(
14 |        (0 f : ~(k) -> Type)
15 |     -> (v : ~(k))
16 |     -> Lens' (~(arg) f) (f v)
17 |   )
18 |
19 | export
20 | blensClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
21 | blensClaim vis fun p =
22 |   simpleClaim vis fun $ piAll (blensTpe p.kind p.applied) p.implicits
23 |
24 | ||| Top-level declaration implementing the `Eq` interface for
25 | ||| the given data type.
26 | export
27 | recordImplClaim : Visibility -> (impl : Name) -> (p : BarbieInfo) -> Decl
28 | recordImplClaim vis impl p =
29 |   let tpe := piAll `(RecordB ~(p.kind) ~(p.applied)) p.implicits
30 |    in implClaimVis vis impl tpe
31 |
32 | --------------------------------------------------------------------------------
33 | --          Definitions
34 | --------------------------------------------------------------------------------
35 |
36 | export
37 | recordImplDef : (fld, impl : Name) -> Decl
38 | recordImplDef fld impl = def impl [patClause (var impl) `(MkRecordB ~(var fld))]
39 |
40 | lclause : (String -> String) -> Name -> BoundArg 0 RegularNamed -> Clause
41 | lclause f fun (BA x _ _) =
42 |   let fld := argName x
43 |       nme := UN $ Basic (f $ nameStr fld)
44 |       u   := update [ISetField [nameStr fld] `(x)] `(y)
45 |    in patClause `(~(var fun) _ ~(var nme)) `(lens ~(var fld) $ \x,y => ~(u))
46 |
47 | export
48 | lensDef : (String -> String) -> Name -> Con n vs -> Decl
49 | lensDef f fun c =
50 |   def fun (lclause f fun <$> (boundArgs regularNamed c.args [] <>> []))
51 |
52 | --------------------------------------------------------------------------------
53 | --          Deriving
54 | --------------------------------------------------------------------------------
55 |
56 | ||| Generate declarations and implementations for `RecordB`
57 | ||| for a given data type.
58 | export
59 | RecordBVis :
60 |      (String -> String)
61 |   -> Visibility
62 |   -> List Name
63 |   -> ParamTypeInfo
64 |   -> Res (List TopLevel)
65 | RecordBVis f vis nms p = case barbieArgs p.info.args of
66 |   Just prf => case p.info.cons of
67 |     [c] =>
68 |       let nlens := funName p "bfield"
69 |           impl  := implName p "RecordB"
70 |           bti   := BI p prf
71 |        in Right
72 |             [ TL (blensClaim vis nlens bti) (lensDef f nlens c)
73 |             , TL (recordImplClaim vis impl bti)
74 |                  (recordImplDef nlens impl)
75 |             ]
76 |     _ => failRecord "RecordB"
77 |   Nothing => Left $ "Not a barbie type"
78 |
79 | ||| Alias for `RecordBVis Public`
80 | export %inline
81 | RecordB :
82 |      (String -> String)
83 |   -> List Name
84 |   -> ParamTypeInfo
85 |   -> Res (List TopLevel)
86 | RecordB f = RecordBVis f Public
87 |