From 63814e7809f4a0d868e18f8cb958cd0efad236a8 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 19 Oct 2023 16:13:23 -0400 Subject: [PATCH] Add elaboration scripts for creating lenses Thanks to Stefan Hoeck for providing the code for this! --- lens.ipkg | 9 +++++-- src/Derive/Iso.idr | 52 +++++++++++++++++++++++++++++++++++ src/Derive/Lens.idr | 51 +++++++++++++++++++++++++++++++++++ src/Derive/Lens/Options.idr | 22 +++++++++++++++ src/Derive/Prism.idr | 54 +++++++++++++++++++++++++++++++++++++ 5 files changed, 186 insertions(+), 2 deletions(-) create mode 100644 src/Derive/Iso.idr create mode 100644 src/Derive/Lens.idr create mode 100644 src/Derive/Lens/Options.idr create mode 100644 src/Derive/Prism.idr diff --git a/lens.ipkg b/lens.ipkg index d58b97d..386b8b5 100644 --- a/lens.ipkg +++ b/lens.ipkg @@ -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 diff --git a/src/Derive/Iso.idr b/src/Derive/Iso.idr new file mode 100644 index 0000000..58c03b7 --- /dev/null +++ b/src/Derive/Iso.idr @@ -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 + [ 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 diff --git a/src/Derive/Lens.idr b/src/Derive/Lens.idr new file mode 100644 index 0000000..cd2bbd6 --- /dev/null +++ b/src/Derive/Lens.idr @@ -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 + diff --git a/src/Derive/Lens/Options.idr b/src/Derive/Lens/Options.idr new file mode 100644 index 0000000..d6a5b12 --- /dev/null +++ b/src/Derive/Lens/Options.idr @@ -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") diff --git a/src/Derive/Prism.idr b/src/Derive/Prism.idr new file mode 100644 index 0000000..ec55da1 --- /dev/null +++ b/src/Derive/Prism.idr @@ -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)) + [ 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