0 | module Derive.Lens
 1 |
 2 | import public Derive.Lens.Options
 3 | import public Language.Reflection.Util
 4 |
 5 | %default total
 6 |
 7 | toField : Name -> Name
 8 | toField (NS ns nm)      = NS ns (toField nm)
 9 | toField (UN (Basic nm)) = UN (Field nm)
10 | toField nm              = nm
11 |
12 | parameters (o : LensOptions)
13 |   lname : Name -> Name
14 |   lname n = UN $ Basic (o.fieldName $ nameStr n)
15 |
16 |   lclaim : Visibility -> ParamTypeInfo -> BoundArg 0 RegularNamed -> Decl
17 |   lclaim vis p (BA x _ _) =
18 |     let arg := p.applied
19 |         tpe := piAll `(Lens' ~(arg) ~(x.type)) p.implicits
20 |      in simpleClaim vis (lname $ argName x) tpe
21 |
22 |   ldef : BoundArg 0 RegularNamed -> Decl
23 |   ldef (BA x _ _) =
24 |     let fld := toField $ argName x
25 |         nme := lname fld
26 |         u   := update [ISetField [nameStr fld] `(y)] `(x)
27 |      in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]
28 |
29 |
30 |   ||| Generate monomorphic lenses for a record type.
31 |   export
32 |   LensesVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
33 |   LensesVisO vis nms p = case p.info.cons of
34 |     [c] => Right (lenses c.args)
35 |     _   => Left "Lenses can only be derived for record types"
36 |     where
37 |       lenses : Vect n Arg -> List TopLevel
38 |       lenses args =
39 |         map (\x => TL (lclaim vis p x) (ldef x)) (boundArgs regularNamed args []) <>> []
40 |
41 |   ||| Alias for `LensesVisO Public`
42 |   export %inline
43 |   LensesO : List Name -> ParamTypeInfo -> Res (List TopLevel)
44 |   LensesO = LensesVisO Public
45 |
46 | ||| Alias for `LensesVisO defaultOptions`
47 | export %inline
48 | LensesVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
49 | LensesVis = LensesVisO defaultOptions
50 |
51 | ||| Alias for `LensesVis Public`
52 | export %inline
53 | Lenses : List Name -> ParamTypeInfo -> Res (List TopLevel)
54 | Lenses = LensesVis Public
55 |
56 |