Add elaboration scripts for creating lenses

Thanks to Stefan Hoeck for providing the code for this!
This commit is contained in:
Kiana Sheibani 2023-10-19 16:13:23 -04:00
parent 451d7b2233
commit 63814e7809
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
5 changed files with 186 additions and 2 deletions

View file

@ -10,7 +10,8 @@ sourcedir = "src"
readme = "README.md"
langversion >= 0.6.0
depends = profunctors >= 1.1.2
depends = profunctors >= 1.1.2,
elab-util >= 0.6.0
modules = Control.Applicative.Backwards,
Control.Applicative.Indexing,
@ -41,4 +42,8 @@ modules = Control.Applicative.Backwards,
Data.SortedSet.Lens,
Data.String.Lens,
Data.Tuple.Lens,
Data.Vect.Lens
Data.Vect.Lens,
Derive.Lens.Options,
Derive.Lens,
Derive.Prism,
Derive.Iso

52
src/Derive/Iso.idr Normal file
View file

@ -0,0 +1,52 @@
module Derive.Iso
import public Derive.Lens.Options
import public Language.Reflection.Util
%default total
isoErr : Either String a
isoErr = Left "Isomorphisms can only be derived for newtypes"
parameters (o : LensOptions)
iname : ParamTypeInfo -> Name
iname p = UN $ Basic (o.dataTypeName $ nameStr p.info.name)
iclaim : Visibility -> ParamTypeInfo -> Name -> TTImp -> Decl
iclaim vis p con rtpe =
let arg := p.applied
tpe := piAll `(Iso' ~(arg) ~(rtpe)) p.implicits
in simpleClaim vis (iname p) tpe
idef : ParamTypeInfo -> Name -> Decl
idef p con =
let nme := iname p
get := `(\case ~(var con) x => x)
in def nme [patClause (var nme) `(iso ~(get) ~(var con))]
itl : Visibility -> ParamTypeInfo -> Con n vs -> Res (List TopLevel)
itl vis p (MkCon con _ args _) = case boundArgs regular args [] of
[<arg] => Right [TL (iclaim vis p con arg.arg.type) (idef p con)]
_ => isoErr
||| Generate an isomorphism for a newtype
export
IsoVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
IsoVisO vis nms p = case p.info.cons of
[c] => itl vis p c
_ => isoErr
||| Alias for `IsoVisO Public`
export %inline
IsoO : List Name -> ParamTypeInfo -> Res (List TopLevel)
IsoO = IsoVisO Public
||| Alias for `IsoVisO defaultOptions`
export %inline
IsoVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
IsoVis = IsoVisO defaultOptions
||| Alias for `IsoVis Public`
export %inline
Iso : List Name -> ParamTypeInfo -> Res (List TopLevel)
Iso = IsoVis Public

51
src/Derive/Lens.idr Normal file
View file

@ -0,0 +1,51 @@
module Derive.Lens
import public Derive.Lens.Options
import public Language.Reflection.Util
%default total
parameters (o : LensOptions)
lname : Name -> Name
lname n = UN $ Basic (o.fieldName $ nameStr n)
lclaim : Visibility -> ParamTypeInfo -> BoundArg 0 RegularNamed -> Decl
lclaim vis p (BA x _ _) =
let arg := p.applied
tpe := piAll `(Lens' ~(arg) ~(x.type)) p.implicits
in simpleClaim vis (lname $ argName x) tpe
ldef : BoundArg 0 RegularNamed -> Decl
ldef (BA x _ _) =
let fld := argName x
nme := lname fld
u := update [ISetField [nameStr fld] `(y)] `(x)
in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]
||| Generate monomorphic lenses for a record type.
export
LensesVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
LensesVisO vis nms p = case p.info.cons of
[c] => Right (lenses c.args)
_ => Left "Lenses can only be derived for record types"
where
lenses : Vect n Arg -> List TopLevel
lenses args =
map (\x => TL (lclaim vis p x) (ldef x)) (boundArgs regularNamed args []) <>> []
||| Alias for `LensesVisO Public`
export %inline
LensesO : List Name -> ParamTypeInfo -> Res (List TopLevel)
LensesO = LensesVisO Public
||| Alias for `LensesVisO defaultOptions`
export %inline
LensesVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
LensesVis = LensesVisO defaultOptions
||| Alias for `LensesVis Public`
export %inline
Lenses : List Name -> ParamTypeInfo -> Res (List TopLevel)
Lenses = LensesVis Public

View file

@ -0,0 +1,22 @@
module Derive.Lens.Options
import Data.String
%default total
public export
record LensOptions where
constructor MkLensOptions
fieldName : String -> String
constructorName : String -> String
dataTypeName : String -> String
export
toLowerHead : String -> String
toLowerHead s = case strUncons s of
Nothing => s
Just (x, xs) => singleton (toLower x) ++ xs
export
defaultOptions : LensOptions
defaultOptions = MkLensOptions (++ "_") (++ "_") (\x => toLowerHead x ++ "Iso")

54
src/Derive/Prism.idr Normal file
View file

@ -0,0 +1,54 @@
module Derive.Prism
import public Derive.Lens.Options
import public Language.Reflection.Util
%default total
parameters (o : LensOptions)
pname : Name -> Name
pname n = UN $ Basic (o.constructorName $ nameStr n)
pclaim : Visibility -> ParamTypeInfo -> Name -> TTImp -> Decl
pclaim vis p con rtpe =
let arg := p.applied
tpe := piAll `(Prism' ~(arg) ~(rtpe)) p.implicits
in simpleClaim vis (pname con) tpe
pdef0 : Name -> Decl
pdef0 con =
let nme := pname con
get := `(\case ~(var con) => Just (); _ => Nothing)
in def nme [patClause (var nme) `(prism' (const ~(var con)) ~(get))]
pdef1 : Name -> Decl
pdef1 con =
let nme := pname con
get := `(\case ~(var con) x => Just x; _ => Nothing)
in def nme [patClause (var nme) `(prism' ~(var con) ~(get))]
ptl : Visibility -> ParamTypeInfo -> Con n vs -> Maybe TopLevel
ptl vis p (MkCon con _ args _) = case boundArgs regular args [] of
[<] => Just (TL (pclaim vis p con `(Unit)) (pdef0 con))
[<arg] => Just (TL (pclaim vis p con arg.arg.type) (pdef1 con))
_ => Nothing
||| Generate monomorphic prisms for a sum type.
export
PrismsVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
PrismsVisO vis nms p = Right $ mapMaybe (ptl vis p) p.info.cons
||| Alias for `PrismsVisO Public`
export %inline
PrismsO : List Name -> ParamTypeInfo -> Res (List TopLevel)
PrismsO = PrismsVisO Public
||| Alias for `PrismVisO defaultOptions`
export %inline
PrismsVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
PrismsVis = PrismsVisO defaultOptions
||| Alias for `PrismsVis Public`
export %inline
Prisms : List Name -> ParamTypeInfo -> Res (List TopLevel)
Prisms = PrismsVis Public