[ derive, test ] Move generator's printer to the main lib + cleanup

buzden · Aug 29, 2024 · 1e06f50 · 1e06f50
1 parent 6e26d52
commit 1e06f50
Show file tree

Hide file tree

Showing 340 changed files with 1,218 additions and 1,393 deletions.
diff --git a/examples/covering-seq/tests/gens/print/DerivedGen.idr b/examples/covering-seq/tests/gens/print/DerivedGen.idr
@@ -1,11 +1,12 @@
 module DerivedGen
 
-import PrintDerivation
-
 import Data.List.Covering
 
+import Deriving.DepTyCheck.Gen
+
 %default total
 
 %language ElabReflection
 
-%runElab printDerived $ Fuel -> {n : Nat} -> (bs : BitMask n) -> Gen MaybeEmpty $ CoveringSequence n bs
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter $ Fuel -> {n : Nat} -> (bs : BitMask n) -> Gen MaybeEmpty $ CoveringSequence n bs
diff --git a/examples/covering-seq/tests/gens/print/PrintDerivation.idr b/examples/covering-seq/tests/gens/print/PrintDerivation.idr
diff --git a/examples/covering-seq/tests/gens/print/expected b/examples/covering-seq/tests/gens/print/expected
@@ -1,7 +1,5 @@
-1/2: Building PrintDerivation (PrintDerivation.idr)
-2/2: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> (bs : BitMask n) -> Gen MaybeEmpty (CoveringSequence n bs)
-LOG gen.auto.derive.infra:0: 
+1/1: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen MaybeEmpty (CoveringSequence n bs)
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> MkArg MW ImplicitArg (Just "outer^<n>") implicitTrue
 .=> MkArg MW ExplicitArg (Just "outer^<bs>") implicitTrue

diff --git a/examples/sorted-list/tests/gens/print/DerivedGen.idr b/examples/sorted-list/tests/gens/print/DerivedGen.idr
@@ -1,11 +1,12 @@
 module DerivedGen
 
-import PrintDerivation
-
 import Data.List.Sorted
 
+import Deriving.DepTyCheck.Gen
+
 %default total
 
 %language ElabReflection
 
-%runElab printDerived $ Fuel -> Gen MaybeEmpty SortedList
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter $ Fuel -> Gen MaybeEmpty SortedList
diff --git a/examples/sorted-list/tests/gens/print/PrintDerivation.idr b/examples/sorted-list/tests/gens/print/PrintDerivation.idr
diff --git a/examples/sorted-list/tests/gens/print/expected b/examples/sorted-list/tests/gens/print/expected
@@ -1,7 +1,5 @@
-1/2: Building PrintDerivation (PrintDerivation.idr)
-2/2: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
-LOG gen.auto.derive.infra:0: 
+1/1: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> local
       { decls =

diff --git a/src/Deriving/DepTyCheck/Gen/Entry.idr b/src/Deriving/DepTyCheck/Gen/Entry.idr
@@ -371,3 +371,18 @@ deriveGenFor a = do
   sig <- quote a
   tt <- deriveGenExpr sig
   check tt
+
+||| Declares `main : IO Unit` function that prints derived generator for the given generator's signature
+export
+deriveGenPrinter : DerivatorCore => Type -> Elab Unit
+deriveGenPrinter ty = do
+  ty <- quote ty
+  logSugaredTerm "deptycheck.derive.print" DefaultLogLevel "type" ty
+  expr <- deriveGenExpr ty
+  expr <- quote expr
+  declare `[
+    main : IO Unit
+    main = do
+      putStr $ interpolate ~(expr)
+      putStrLn ""
+  ]
diff --git a/tests/derivation/_common/PrintDerivation.idr b/tests/derivation/_common/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 001/DerivedGen.idr b/tests/derivation/infra/empty-body print 001/DerivedGen.idr
@@ -1,10 +1,12 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 %default total
 
 %language ElabReflection
 
-%runElab printDerived @{EmptyBody} $ Fuel -> Gen MaybeEmpty Unit
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> Gen MaybeEmpty Unit
diff --git a/tests/derivation/infra/empty-body print 001/PrintDerivation.idr b/tests/derivation/infra/empty-body print 001/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 001/expected b/tests/derivation/infra/empty-body print 001/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty ()
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty ()
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> local
       { decls =

diff --git a/tests/derivation/infra/empty-body print 002/DerivedGen.idr b/tests/derivation/infra/empty-body print 002/DerivedGen.idr
@@ -1,12 +1,14 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 import Data.Vect
 
 %default total
 
 %language ElabReflection
 
-%runElab printDerived @{EmptyBody} $ Fuel -> (n : Nat) -> (a : Type) -> Gen MaybeEmpty (Vect n a)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> (n : Nat) -> (a : Type) -> Gen MaybeEmpty (Vect n a)
diff --git a/tests/derivation/infra/empty-body print 002/PrintDerivation.idr b/tests/derivation/infra/empty-body print 002/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 002/expected b/tests/derivation/infra/empty-body print 002/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> (n : Nat) -> (a : Type) -> Gen MaybeEmpty (Vect n a)
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (a : Type) -> Gen MaybeEmpty (Vect n a)
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> MkArg MW ExplicitArg (Just "outer^<n>") implicitTrue
 .=> MkArg MW ExplicitArg (Just "outer^<a>") implicitTrue

diff --git a/tests/derivation/infra/empty-body print 003/DerivedGen.idr b/tests/derivation/infra/empty-body print 003/DerivedGen.idr
@@ -1,12 +1,14 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 import Data.Vect
 
 %default total
 
 %language ElabReflection
 
-%runElab printDerived @{EmptyBody} $ Fuel -> (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty Bool
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty Bool
diff --git a/tests/derivation/infra/empty-body print 003/PrintDerivation.idr b/tests/derivation/infra/empty-body print 003/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 003/expected b/tests/derivation/infra/empty-body print 003/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel) -> Gen MaybeEmpty Nat)} -> Gen MaybeEmpty Bool
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel) -> Gen MaybeEmpty Nat)} -> Gen MaybeEmpty Bool
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> MkArg
       MW

diff --git a/tests/derivation/infra/empty-body print 004/DerivedGen.idr b/tests/derivation/infra/empty-body print 004/DerivedGen.idr
@@ -1,7 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 %default total
 
@@ -10,4 +11,5 @@ import PrintDerivation
 data X : Nat -> Type where
   MkX : X n
 
-%runElab printDerived @{EmptyBody} $ Fuel -> (n : Nat) -> Gen MaybeEmpty (X n)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> (n : Nat) -> Gen MaybeEmpty (X n)
diff --git a/tests/derivation/infra/empty-body print 004/PrintDerivation.idr b/tests/derivation/infra/empty-body print 004/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 004/expected b/tests/derivation/infra/empty-body print 004/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> (n : Nat) -> Gen MaybeEmpty (X n)
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> Gen MaybeEmpty (X n)
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> MkArg MW ExplicitArg (Just "outer^<n>") implicitTrue
 .=> local

diff --git a/tests/derivation/infra/empty-body print 005/DerivedGen.idr b/tests/derivation/infra/empty-body print 005/DerivedGen.idr
@@ -1,7 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 %default total
 
@@ -10,4 +11,5 @@ import PrintDerivation
 data X : Nat -> Type where
   MkX : X n
 
-%runElab printDerived @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** X n)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** X n)
diff --git a/tests/derivation/infra/empty-body print 005/PrintDerivation.idr b/tests/derivation/infra/empty-body print 005/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 005/expected b/tests/derivation/infra/empty-body print 005/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** X n)
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** X n)
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> local
       { decls =

diff --git a/tests/derivation/infra/empty-body print 006/DerivedGen.idr b/tests/derivation/infra/empty-body print 006/DerivedGen.idr
@@ -1,12 +1,14 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 import Data.Vect
 
 %default total
 
 %language ElabReflection
 
-%runElab printDerived @{EmptyBody} $ Fuel -> (a : Type) -> Gen MaybeEmpty (n : Nat ** Vect n a)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> (a : Type) -> Gen MaybeEmpty (n : Nat ** Vect n a)
diff --git a/tests/derivation/infra/empty-body print 006/PrintDerivation.idr b/tests/derivation/infra/empty-body print 006/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 006/expected b/tests/derivation/infra/empty-body print 006/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> (a : Type) -> Gen MaybeEmpty (n : Nat ** Vect n a)
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Type) -> Gen MaybeEmpty (n : Nat ** Vect n a)
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> MkArg MW ExplicitArg (Just "outer^<a>") implicitTrue
 .=> local

diff --git a/tests/derivation/infra/empty-body print 007/DerivedGen.idr b/tests/derivation/infra/empty-body print 007/DerivedGen.idr
@@ -1,7 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 %default total
 
@@ -11,4 +12,5 @@ data X : Nat -> Bool -> Type where
   X0 : X 0 True
   X1 : X 1 False
 
-%runElab printDerived @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** b : Bool ** X n b)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** b : Bool ** X n b)
diff --git a/tests/derivation/infra/empty-body print 007/PrintDerivation.idr b/tests/derivation/infra/empty-body print 007/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 007/expected b/tests/derivation/infra/empty-body print 007/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** (b : Bool ** X n b))
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** (b : Bool ** X n b))
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> local
       { decls =

diff --git a/tests/derivation/infra/empty-body print 008/DerivedGen.idr b/tests/derivation/infra/empty-body print 008/DerivedGen.idr
@@ -1,12 +1,14 @@
 module DerivedGen
 
 import AlternativeCore
-import PrintDerivation
+
+import Deriving.DepTyCheck.Gen
 
 import Data.Vect
 
 %default total
 
 %language ElabReflection
 
-%runElab printDerived @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** a : Type ** Vect n a)
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{EmptyBody} $ Fuel -> Gen MaybeEmpty (n : Nat ** a : Type ** Vect n a)
diff --git a/tests/derivation/infra/empty-body print 008/PrintDerivation.idr b/tests/derivation/infra/empty-body print 008/PrintDerivation.idr
diff --git a/tests/derivation/infra/empty-body print 008/expected b/tests/derivation/infra/empty-body print 008/expected
@@ -1,8 +1,6 @@
-1/3: Building AlternativeCore (AlternativeCore.idr)
-2/3: Building PrintDerivation (PrintDerivation.idr)
-3/3: Building DerivedGen (DerivedGen.idr)
-LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** (a : Type ** Vect n a))
-LOG gen.auto.derive.infra:0: 
+1/2: Building AlternativeCore (AlternativeCore.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** (a : Type ** Vect n a))
     MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
 .=> local
       { decls =

diff --git a/tests/derivation/infra/empty-body run 001/DerivedGen.idr b/tests/derivation/infra/empty-body run 001/DerivedGen.idr
@@ -1,6 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
+
+import Deriving.DepTyCheck.Gen
 import RunDerivedGen
 
 %default total

diff --git a/tests/derivation/infra/empty-body run 002/DerivedGen.idr b/tests/derivation/infra/empty-body run 002/DerivedGen.idr
@@ -1,6 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
+
+import Deriving.DepTyCheck.Gen
 import RunDerivedGen
 
 %default total

diff --git a/tests/derivation/infra/empty-body run 003/DerivedGen.idr b/tests/derivation/infra/empty-body run 003/DerivedGen.idr
@@ -1,6 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
+
+import Deriving.DepTyCheck.Gen
 import RunDerivedGen
 
 %default total

diff --git a/tests/derivation/infra/empty-body run 004/DerivedGen.idr b/tests/derivation/infra/empty-body run 004/DerivedGen.idr
@@ -1,6 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
+
+import Deriving.DepTyCheck.Gen
 import RunDerivedGen
 
 %default total

diff --git a/tests/derivation/infra/empty-body run 005/DerivedGen.idr b/tests/derivation/infra/empty-body run 005/DerivedGen.idr
@@ -1,6 +1,8 @@
 module DerivedGen
 
 import AlternativeCore
+
+import Deriving.DepTyCheck.Gen
 import RunDerivedGen
 
 %default total