target type generator derivation from fused type generator added

buzden · Jun 4, 2024 · 84d7f0a · 84d7f0a
1 parent aca59a3
commit 84d7f0a
Show file tree

Hide file tree

Showing 146 changed files with 1,019 additions and 16 deletions.
diff --git a/src/Deriving/DepTyCheck/Util/Fusion.idr b/src/Deriving/DepTyCheck/Util/Fusion.idr
@@ -5,6 +5,7 @@ import Language.Reflection.TTImp
 import Language.Reflection.Derive
 import Language.Reflection.Pretty
 import Language.Reflection.Compat
+import public Deriving.DepTyCheck.Gen
 import Deriving.DepTyCheck.Util.Collections
 import Deriving.DepTyCheck.Util.Reflection
 import Data.Nat
@@ -86,6 +87,7 @@ splitRhsDef []      = type
 splitRhsDef (t::[]) = t
 splitRhsDef (t::ts) = app (var `{Builtin.MkPair} .$ t) (splitRhsDef ts)
 
+
 splitRhsClaim : List TTImp -> TTImp
 splitRhsClaim []      = type
 splitRhsClaim (t::[]) = t
@@ -114,6 +116,9 @@ record FusionDecl where
   dataType    : Decl
   splitClaim  : Decl
   splitDef    : Decl
+  genFClaim   : Decl
+  genRClaim   : Decl
+  genRDef     : Decl
 
 
 prepareConArgs : TTImp -> List TTImp
@@ -122,14 +127,29 @@ prepareConArgs t = do
   map getExpr tApps
 
 
-fusionTypeName : List Name -> Name
-fusionTypeName = UN . Basic . (joinBy "") . (map nameStr)
+joinNames : List Name -> Name
+joinNames = UN . Basic . (joinBy "") . (map nameStr)
+
+
+genRMkDPair : TTImp -> List Name -> TTImp
+genRMkDPair = foldr (\n, acc => var `{MkDPair} .$ n.bindVar .$ acc)
+
+
+genFDPair : Name -> List (Name, TTImp) -> TTImp
+genFDPair n l = foldr
+  (\(n, tt), acc => var `{DPair} .$ tt .$ (MkArg MW ExplicitArg (Just n) tt `lam` acc))
+  (foldConstructor (var n) (map (var . fst) l))
+  l
+
+
+genFRhsClaim : Name -> List (Name, TTImp) -> TTImp
+genFRhsClaim n l = var `{Gen} .$ var `{MaybeEmpty} .$ genFDPair n l
 
 
 deriveFusion : Vect (2 + n) (TypeInfo, List Name) -> Maybe FusionDecl
 deriveFusion l = do
   let typeNames = toList $ map ((.name) . fst) l
-  let fusionTypeName = fusionTypeName $ typeNames
+  let fusionTypeName = joinNames $ typeNames
 
   let typeArgs = map (\(ti, la) => matchArgs ti.args la) l
   let False = any isNothing typeArgs
@@ -146,7 +166,10 @@ deriveFusion l = do
   let True = all (not . Prelude.null . fst) consPre
     | False => Nothing
   let consML1 = map (\(cons, args) => (toList1' cons, args)) consPre -- how to prove and use toList?
-  let consL1  = map (\(cons, args) => case cons of {Just x => (x, args); Nothing => ((MkCon (UN (Basic "")) [] type):::[], args)}) consML1
+  let consL1  = map (\(cons, args) => case cons of
+                  Just x => (x, args)
+                  Nothing => ((MkCon (UN (Basic "")) [] type):::[], args)
+                ) consML1
   let consAll = map (\(cons, args) => map (\c => (c, args)) cons) consL1
   let consComb = combinations consAll
   let consCombPrepared = map (map (\(con, args) => (con.name, prepareConArgs con.type, args))) consComb
@@ -165,17 +188,57 @@ deriveFusion l = do
                     splitRhsClaim (splitReturnType typeNames argNamesList)
 
   let defDecl = if (not $ null fusedCons)
-                then def splitName $ splitClauses (var splitName) $ toList (map (toList . (map (nameStr . (.name) . fst))) consComb)
+                then def splitName $ splitClauses (var splitName) $
+                  toList (map (toList . (map (nameStr . (.name) . fst))) consComb)
                 else def splitName [impossibleClause (var splitName .$ implicitTrue)]
 
-  Just (MkFusionDecl dataDecl claimDecl defDecl)
+  let stub = ILog Nothing
+  let genFName = UN $ Basic ("gen" ++ (nameStr fusionTypeName))
+  let genFClaim = export' genFName $
+                    (MkArg MW ExplicitArg Nothing (var `{Fuel})) .->
+                    (genFRhsClaim fusionTypeName uniqueArgs)
+
+  let genRClaim = export' (`{genZ_ultimate}) $
+                    (MkArg MW ExplicitArg Nothing (var `{Fuel})) .->
+                    (var `{Gen} .$ var `{MaybeEmpty} .$ var `{Z})
+
+  let fusedVarName = toLower $ nameStr fusionTypeName
+  let typeVarNames = map (toLower . nameStr) typeNames
+  let genRDef = def
+                  `{genZ_ultimate}
+                  [  var `{genZ_ultimate}
+                  .$ bindVar "fl"
+                  .= var `{(>>=)}
+                  .$ (var genFName .$ var `{fl})
+                  .$ (
+                      MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
+                      `lam` iCase {
+                        sc = var "{lamc:0}",
+                        ty = implicitFalse,
+                        clauses =
+                          [ genRMkDPair (bindVar fusedVarName) uniqueNames
+                          .= iCase {
+                              sc = var splitName .$ (var $ UN $ Basic fusedVarName),
+                              ty = implicitTrue,
+                              clauses =
+                                [ (splitRhsDef (map bindVar typeVarNames))
+                                .= var `{pure}
+                                .$ foldConstructor (var `{MkZ}) (map var uniqueNames ++ map (var . UN . Basic) typeVarNames)
+                                ]
+                            }
+                          ]
+                        }
+                      )
+                  ]
+
+  Just (MkFusionDecl dataDecl claimDecl defDecl genFClaim genRClaim genRDef)
 
 
 declareFusion : Vect (2 + n) (TypeInfo, List Name) -> Elab (Maybe FusionDecl)
 declareFusion l = do
   let derived = deriveFusion l
   case derived of
-    Just fd => declare [fd.dataType, fd.splitClaim, fd.splitDef]
+    Just fd => declare [fd.dataType, fd.splitClaim, fd.splitDef, fd.genFClaim, fd.genRClaim, fd.genRDef]
     Nothing => declare []
   pure $ derived
 
@@ -193,11 +256,13 @@ public export
 solveDependencies : List Arg -> List (List (Name, List String))
 solveDependencies l = go l [] where
   go : List Arg -> List (List (Name, List String)) -> List (List (Name, List String))
-  go []      acc = map reverse acc
+  go []      acc = map reverse acc -- SnocList
   go (a::as) acc = go as (merge (prepareArgsSolve a) acc) where
     merge : (Name, List String) -> List (List (Name, List String)) -> List (List (Name, List String))
     merge a []              = [[a]]
-    merge (m, as) (rs::rss) = if (any (not . Prelude.null . (intersect as) . snd) rs) then ((m, as)::rs)::rss else rs::(merge (m, as) rss)
+    merge (m, as) (rs::rss) = if (any (not . Prelude.null . (intersect as) . snd) rs)
+                              then ((m, as)::rs)::rss
+                              else rs::(merge (m, as) rss)
 
 
 public export
@@ -228,7 +293,7 @@ getSplit Nothing   = []
 getSplit (Just fd) = [fd.splitClaim, fd.splitDef]
 
 
--- TODO: what happens with :doc
--- tests for order of dependent arguments
--- preserve order of args from left to right
--- TODO: List Arg -> group and filter which to fuse (argDeps)
+public export
+getGen : Maybe FusionDecl -> List Decl
+getGen Nothing = []
+getGen (Just fd) = [fd.genFClaim, fd.genRClaim, fd.genRDef]
diff --git a/tests/Tests.idr b/tests/Tests.idr
@@ -12,9 +12,9 @@ main = goldenRunner $
   , "Derivation utils: canonic signature" `atDir` "derivation/utils/canonicsig"
   , "Derivation utils: constructors analysis" `atDir` "derivation/utils/cons-analysis"
   , "Derivation utils: argument dependencies" `atDir` "derivation/utils/arg-deps"
-  , "Derivation utils: data types fusion" `atDir` "derivation/utils/fusion/merger"
-  , "Derivation utils: fused data types split" `atDir` "derivation/utils/fusion/splitter"
-  , "Derivation utils: dependency solver for fusion" `atDir` "derivation/utils/fusion/depsolver"
+  , [ "Derivation utils: \{p} fusion \{w}" `atDir` "derivation/utils/fusion/\{p}/\{w}"
+    | p <- ["print", "run"], w <- ["merger", "splitter", "depsolver", "generator"]
+    ]
   , "Reflection utils: involved types" `atDir` "derivation/utils/involved-types"
   , "Derivation: input validation" `atDir` "derivation/inputvalidation"
   , "Derivation: running harness" `atDir` "derivation/infra"

diff --git a/...epsolver/001 one var match/DerivedGen.idr → ...epsolver/001 one var match/DerivedGen.idr b/...epsolver/001 one var match/DerivedGen.idr → ...epsolver/001 one var match/DerivedGen.idr
diff --git a/...n/depsolver/001 one var match/derive.ipkg → ...t/depsolver/001 one var match/derive.ipkg b/...n/depsolver/001 one var match/derive.ipkg → ...t/depsolver/001 one var match/derive.ipkg
diff --git a/...sion/depsolver/001 one var match/expected → ...rint/depsolver/001 one var match/expected b/...sion/depsolver/001 one var match/expected → ...rint/depsolver/001 one var match/expected
diff --git a/...ls/fusion/depsolver/001 one var match/run → ...ion/print/depsolver/001 one var match/run b/...ls/fusion/depsolver/001 one var match/run → ...ion/print/depsolver/001 one var match/run
diff --git a/...olver/002 one var no match/DerivedGen.idr → ...olver/002 one var no match/DerivedGen.idr b/...olver/002 one var no match/DerivedGen.idr → ...olver/002 one var no match/DerivedGen.idr
diff --git a/...epsolver/002 one var no match/derive.ipkg → ...epsolver/002 one var no match/derive.ipkg b/...epsolver/002 one var no match/derive.ipkg → ...epsolver/002 one var no match/derive.ipkg
diff --git a/...n/depsolver/002 one var no match/expected → ...t/depsolver/002 one var no match/expected b/...n/depsolver/002 one var no match/expected → ...t/depsolver/002 one var no match/expected
diff --git a/...fusion/depsolver/002 one var no match/run → .../print/depsolver/002 one var no match/run b/...fusion/depsolver/002 one var no match/run → .../print/depsolver/002 one var no match/run
diff --git a/...ver/003 two vars one match/DerivedGen.idr → ...ver/003 two vars one match/DerivedGen.idr b/...ver/003 two vars one match/DerivedGen.idr → ...ver/003 two vars one match/DerivedGen.idr
diff --git a/...solver/003 two vars one match/derive.ipkg → ...solver/003 two vars one match/derive.ipkg b/...solver/003 two vars one match/derive.ipkg → ...solver/003 two vars one match/derive.ipkg
diff --git a/...depsolver/003 two vars one match/expected → ...depsolver/003 two vars one match/expected b/...depsolver/003 two vars one match/expected → ...depsolver/003 two vars one match/expected
diff --git a/...sion/depsolver/003 two vars one match/run → ...rint/depsolver/003 two vars one match/run b/...sion/depsolver/003 two vars one match/run → ...rint/depsolver/003 two vars one match/run
diff --git a/.../004 three types one match/DerivedGen.idr → .../004 three types one match/DerivedGen.idr b/.../004 three types one match/DerivedGen.idr → .../004 three types one match/DerivedGen.idr
diff --git a/...ver/004 three types one match/derive.ipkg → ...ver/004 three types one match/derive.ipkg b/...ver/004 three types one match/derive.ipkg → ...ver/004 three types one match/derive.ipkg
diff --git a/...solver/004 three types one match/expected → ...solver/004 three types one match/expected b/...solver/004 three types one match/expected → ...solver/004 three types one match/expected
diff --git a/...n/depsolver/004 three types one match/run → ...t/depsolver/004 three types one match/run b/...n/depsolver/004 three types one match/run → ...t/depsolver/004 three types one match/run
diff --git a/...tils/fusion/depsolver/_common/derive.ipkg → ...usion/print/depsolver/_common/derive.ipkg b/...tils/fusion/depsolver/_common/derive.ipkg → ...usion/print/depsolver/_common/derive.ipkg
diff --git a/...vation/utils/fusion/depsolver/_common/run → .../utils/fusion/print/depsolver/_common/run b/...vation/utils/fusion/depsolver/_common/run → .../utils/fusion/print/depsolver/_common/run
diff --git a/tests/derivation/utils/fusion/print/generator/001 one var match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/001 one var match/DerivedGen.idr
@@ -0,0 +1,23 @@
+module DerivedGen
+
+import public Deriving.DepTyCheck.Util.Fusion
+import public Deriving.DepTyCheck.Gen.Core
+
+%default total
+
+data X : Type -> Type where
+    MkX : X n
+
+data Y : Type -> Type where
+    MkY : Y n
+
+data Z : Type where
+  MkZ : (n : Type) -> X n -> Y n -> Z
+
+%language ElabReflection
+
+decl : Maybe FusionDecl
+decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
+
+main : IO ()
+main = putPretty $ getGen decl
diff --git a/...sion/merger/001 one var match/derive.ipkg → ...t/generator/001 one var match/derive.ipkg b/...sion/merger/001 one var match/derive.ipkg → ...t/generator/001 one var match/derive.ipkg
diff --git a/tests/derivation/utils/fusion/print/generator/001 one var match/expected b/tests/derivation/utils/fusion/print/generator/001 one var match/expected
@@ -0,0 +1,58 @@
+1/1: Building DerivedGen (DerivedGen.idr)
+[ IClaim
+    emptyFC
+    MW
+    Export
+    []
+    (mkTy
+       { name = "genXY"
+       , type =
+               MkArg MW ExplicitArg Nothing (var "Fuel")
+           .->    var "Gen"
+               .$ var "MaybeEmpty"
+               .$ (   var "DPair"
+                   .$ type
+                   .$ (    MkArg MW ExplicitArg (Just "n") type
+                       .=> var "XY" .$ var "n"))
+       })
+, IClaim
+    emptyFC
+    MW
+    Export
+    []
+    (mkTy
+       { name = "genZ_ultimate"
+       , type =
+               MkArg MW ExplicitArg Nothing (var "Fuel")
+           .-> var "Gen" .$ var "MaybeEmpty" .$ var "Z"
+       })
+, IDef
+    emptyFC
+    "genZ_ultimate"
+    [    var "genZ_ultimate" .$ bindVar "fl"
+      .=    var ">>="
+         .$ (var "genXY" .$ var "fl")
+         .$ (    MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
+             .=> iCase
+                   { sc = var "{lamc:0}"
+                   , ty = implicitFalse
+                   , clauses =
+                       [    var "MkDPair" .$ bindVar "n" .$ bindVar "xy"
+                         .= iCase
+                              { sc = var "splitXY" .$ var "xy"
+                              , ty = implicitTrue
+                              , clauses =
+                                  [       var "Builtin.MkPair"
+                                       .$ bindVar "x"
+                                       .$ bindVar "y"
+                                    .=    var "pure"
+                                       .$ (   var "MkZ"
+                                           .$ var "n"
+                                           .$ var "x"
+                                           .$ var "y")
+                                  ]
+                              }
+                       ]
+                   })
+    ]
+]
diff --git a/...utils/fusion/merger/001 one var match/run → ...ion/print/generator/001 one var match/run b/...utils/fusion/merger/001 one var match/run → ...ion/print/generator/001 one var match/run
diff --git a/tests/derivation/utils/fusion/print/generator/002 two var ordered match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/002 two var ordered match/DerivedGen.idr
@@ -0,0 +1,26 @@
+module DerivedGen
+
+import public Deriving.DepTyCheck.Util.Fusion
+import public Deriving.DepTyCheck.Gen.Core
+
+
+%default total
+
+data X : Type -> Type -> Type where
+    MkX : X m n
+
+data Y : Type -> Type -> Type where
+    MkY : Y m n
+
+data Z : Type where
+  MkZ : (m : Type) -> (n : Type) -> X m n -> Y m n -> Z
+
+%language ElabReflection
+
+
+decl : Maybe FusionDecl
+decl = %runElab runFusion `{X} [`{m}, `{n}] `{Y} [`{m}, `{n}]
+
+main : IO ()
+main = putPretty $ getGen decl
+
diff --git a/...ger/002 two var ordered match/derive.ipkg → ...tor/002 two var ordered match/derive.ipkg b/...ger/002 two var ordered match/derive.ipkg → ...tor/002 two var ordered match/derive.ipkg
diff --git a/tests/derivation/utils/fusion/print/generator/002 two var ordered match/expected b/tests/derivation/utils/fusion/print/generator/002 two var ordered match/expected
@@ -0,0 +1,64 @@
+1/1: Building DerivedGen (DerivedGen.idr)
+[ IClaim
+    emptyFC
+    MW
+    Export
+    []
+    (mkTy
+       { name = "genXY"
+       , type =
+               MkArg MW ExplicitArg Nothing (var "Fuel")
+           .->    var "Gen"
+               .$ var "MaybeEmpty"
+               .$ (   var "DPair"
+                   .$ type
+                   .$ (    MkArg MW ExplicitArg (Just "m") type
+                       .=>    var "DPair"
+                           .$ type
+                           .$ (    MkArg MW ExplicitArg (Just "n") type
+                               .=> var "XY" .$ var "m" .$ var "n")))
+       })
+, IClaim
+    emptyFC
+    MW
+    Export
+    []
+    (mkTy
+       { name = "genZ_ultimate"
+       , type =
+               MkArg MW ExplicitArg Nothing (var "Fuel")
+           .-> var "Gen" .$ var "MaybeEmpty" .$ var "Z"
+       })
+, IDef
+    emptyFC
+    "genZ_ultimate"
+    [    var "genZ_ultimate" .$ bindVar "fl"
+      .=    var ">>="
+         .$ (var "genXY" .$ var "fl")
+         .$ (    MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
+             .=> iCase
+                   { sc = var "{lamc:0}"
+                   , ty = implicitFalse
+                   , clauses =
+                       [       var "MkDPair"
+                            .$ bindVar "m"
+                            .$ (var "MkDPair" .$ bindVar "n" .$ bindVar "xy")
+                         .= iCase
+                              { sc = var "splitXY" .$ var "xy"
+                              , ty = implicitTrue
+                              , clauses =
+                                  [       var "Builtin.MkPair"
+                                       .$ bindVar "x"
+                                       .$ bindVar "y"
+                                    .=    var "pure"
+                                       .$ (   var "MkZ"
+                                           .$ var "m"
+                                           .$ var "n"
+                                           .$ var "x"
+                                           .$ var "y")
+                                  ]
+                              }
+                       ]
+                   })
+    ]
+]
diff --git a/...sion/merger/002 two var ordered match/run → ...t/generator/002 two var ordered match/run b/...sion/merger/002 two var ordered match/run → ...t/generator/002 two var ordered match/run
diff --git a/tests/derivation/utils/fusion/print/generator/003 two var unordered match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/003 two var unordered match/DerivedGen.idr
@@ -0,0 +1,24 @@
+module DerivedGen
+
+import public Deriving.DepTyCheck.Util.Fusion
+import public Deriving.DepTyCheck.Gen.Core
+
+
+%default total
+
+data X : Type -> Type -> Type where
+    MkX : X m n
+
+data Y : Type -> Type -> Type where
+    MkY : Y m n
+
+data Z : Type where
+  MkZ : (m : Type) -> (n : Type) -> X m n -> Y n m -> Z
+
+%language ElabReflection
+
+decl : Maybe FusionDecl
+decl = %runElab runFusion `{X} [`{m}, `{n}] `{Y} [`{n}, `{m}]
+
+main : IO ()
+main = putPretty $ getGen decl
diff --git a/...r/003 two var unordered match/derive.ipkg → ...r/003 two var unordered match/derive.ipkg b/...r/003 two var unordered match/derive.ipkg → ...r/003 two var unordered match/derive.ipkg