toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Merge pull request #2 from crumbtoo/main

Browse source 
Use postfix field projections in elab script
This commit is contained in:
Kiana Sheibani 2024-06-28 21:00:42 -04:00 committed by GitHub
parent 253467ebae 61acb58a22
commit 6d7153496d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Derive/Lens.idr
View file

@ -5,6 +5,11 @@ import public Language.Reflection.Util
%default total %default total
toField : Name -> Name
toField (NS ns nm) = NS ns (toField nm)
toField (UN (Basic nm)) = UN (Field nm)
toField nm = nm
parameters (o : LensOptions) parameters (o : LensOptions)
lname : Name -> Name lname : Name -> Name
lname n = UN $ Basic (o.fieldName $ nameStr n) lname n = UN $ Basic (o.fieldName $ nameStr n)
@ -17,7 +22,7 @@ parameters (o : LensOptions)
ldef : BoundArg 0 RegularNamed -> Decl ldef : BoundArg 0 RegularNamed -> Decl
ldef (BA x _ _) = ldef (BA x _ _) =
let fld := argName x let fld := toField $ argName x
nme := lname fld nme := lname fld
u := update [ISetField [nameStr fld] `(y)] `(x) u := update [ISetField [nameStr fld] `(y)] `(x)
in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))] in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]