Merge pull request #11 from stefan-hoeck/lenses

[ new ] record lenses

barbies.ipkg

@@ -5,17 +5,20 @@ license = "BSD-3"
 brief = "Barbies: Data types that can change their clothes"
 
 depends = elab-util
+        , monocle
 
 sourcedir = "src"
 modules = Control.Barbie
         , Control.DistributiveB
         , Control.FunctorB
         , Control.ApplicativeB
         , Control.TraversableB
+        , Control.RecordB
 
         , Derive.ApplicativeB
-        , Derive.DistributiveB
         , Derive.Barbie
         , Derive.BarbieInfo
+        , Derive.DistributiveB
         , Derive.FunctorB
+        , Derive.RecordB
         , Derive.TraversableB

docs/src/Main.idr

@@ -6,6 +6,7 @@ import Data.List1
 import Data.String
 import Derive.Barbie
 import Derive.Prelude
+import Monocle
 
 %default total
 %language ElabReflection
@@ -23,13 +24,19 @@ public export
 0 Up : Field -> Type
 Up x = Tpe x -> Tpe x
 
+frstToUpper : String -> String
+frstToUpper s =
+  case unpack s of
+    h::t => pack $ toUpper h :: t
+    []   => ""
+
 record User (f : Field -> Type) where
   constructor U
   id    : f Id
   name  : f Name
   email : f Email
 
-%runElab derive "User" [Show,Eq,Barbie]
+%runElab derive "User" [Show,Eq,Barbie,RecordB frstToUpper]
 
 user : User Tpe
 user = U 12 "Stefan" "gundi@gmail.com"

src/Control/Barbie.idr

@@ -1,6 +1,7 @@
 module Control.Barbie
 
+import public Control.ApplicativeB
 import public Control.DistributiveB
 import public Control.FunctorB
-import public Control.ApplicativeB
+import public Control.RecordB
 import public Control.TraversableB

src/Control/RecordB.idr

@@ -0,0 +1,22 @@
+module Control.RecordB
+
+import Monocle.Lens
+
+%default total
+
+public export
+interface RecordB (0 k : Type) (0 t : (k -> Type) -> Type) | t where
+  constructor MkRecordB
+  field : (0 f : k -> Type) -> (v : k) -> Lens' (t f) (f v)
+
+export %inline
+field' : RecordB k t => (v : k) -> Lens' (t f) (f v)
+field' = field f
+
+export %inline
+getField : RecordB k t => (v : k) -> t f -> f v
+getField v = get_ (field f v)
+
+export %inline
+setField : RecordB k t => (v : k) -> f v -> t f -> t f
+setField v = setL (field f v)

src/Derive/Barbie.idr

@@ -4,6 +4,7 @@ import public Derive.ApplicativeB
 import public Derive.BarbieInfo
 import public Derive.DistributiveB
 import public Derive.FunctorB
+import public Derive.RecordB
 import public Derive.TraversableB
 import Language.Reflection.Util
 

src/Derive/RecordB.idr

@@ -0,0 +1,87 @@
+module Derive.RecordB
+
+import Language.Reflection.Util
+import Derive.BarbieInfo
+
+%default total
+
+--------------------------------------------------------------------------------
+--          Claims
+--------------------------------------------------------------------------------
+
+blensTpe : (k : TTImp) -> TTImp -> TTImp
+blensTpe k arg =
+  `(
+       (0 f : ~(k) -> Type)
+    -> (v : ~(k))
+    -> Lens' (~(arg) f) (f v)
+  )
+
+export
+blensClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
+blensClaim vis fun p =
+  simpleClaim vis fun $ piAll (blensTpe p.kind p.applied) p.implicits
+
+||| Top-level declaration implementing the `Eq` interface for
+||| the given data type.
+export
+recordImplClaim : Visibility -> (impl : Name) -> (p : BarbieInfo) -> Decl
+recordImplClaim vis impl p =
+  let tpe := piAll `(RecordB ~(p.kind) ~(p.applied)) p.implicits
+   in implClaimVis vis impl tpe
+
+--------------------------------------------------------------------------------
+--          Definitions
+--------------------------------------------------------------------------------
+
+export
+recordImplDef : (fld, impl : Name) -> Decl
+recordImplDef fld impl = def impl [patClause (var impl) `(MkRecordB ~(var fld))]
+
+lclause : (String -> String) -> Name -> BoundArg 0 RegularNamed -> Clause
+lclause f fun (BA x _ _) =
+  let fld := argName x
+      nme := UN $ Basic (f $ nameStr fld)
+      u   := update [ISetField [nameStr fld] `(x)] `(y)
+   in patClause `(~(var fun) _ ~(var nme)) `(lens ~(var fld) $ \x,y => ~(u))
+
+export
+lensDef : (String -> String) -> Name -> Con n vs -> Decl
+lensDef f fun c =
+  def fun (lclause f fun <$> (boundArgs regularNamed c.args [] <>> []))
+
+--------------------------------------------------------------------------------
+--          Deriving
+--------------------------------------------------------------------------------
+
+||| Generate declarations and implementations for `RecordB`
+||| for a given data type.
+export
+RecordBVis :
+     (String -> String)
+  -> Visibility
+  -> List Name
+  -> ParamTypeInfo
+  -> Res (List TopLevel)
+RecordBVis f vis nms p = case barbieArgs p.info.args of
+  Just prf => case p.info.cons of
+    [c] =>
+      let nlens := funName p "bfield"
+          impl  := implName p "RecordB"
+          bti   := BI p prf
+       in Right
+            [ TL (blensClaim vis nlens bti) (lensDef f nlens c)
+            , TL (recordImplClaim vis impl bti)
+                 (recordImplDef nlens impl)
+            ]
+    _ => failRecord "RecordB"
+  Nothing => Left $ "Not a barbie type"
+
+||| Alias for `RecordBVis Public`
+export %inline
+RecordB :
+     (String -> String)
+  -> List Name
+  -> ParamTypeInfo
+  -> Res (List TopLevel)
+RecordB f = RecordBVis f Public