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