Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 1 commit into from
Aug 29, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
7 changes: 4 additions & 3 deletions examples/covering-seq/tests/gens/print/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion examples/covering-seq/tests/gens/print/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

6 changes: 2 additions & 4 deletions examples/covering-seq/tests/gens/print/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
7 changes: 4 additions & 3 deletions examples/sorted-list/tests/gens/print/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion examples/sorted-list/tests/gens/print/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

6 changes: 2 additions & 4 deletions examples/sorted-list/tests/gens/print/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
15 changes: 15 additions & 0 deletions src/Deriving/DepTyCheck/Gen/Entry.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ""
]
20 changes: 0 additions & 20 deletions tests/derivation/_common/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 001/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 001/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 001/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 002/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 002/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 002/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 003/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 003/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 003/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 004/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
module DerivedGen

import AlternativeCore
import PrintDerivation

import Deriving.DepTyCheck.Gen

%default total

Expand All @@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 004/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 004/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 005/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
module DerivedGen

import AlternativeCore
import PrintDerivation

import Deriving.DepTyCheck.Gen

%default total

Expand All @@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 005/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 005/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 006/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 006/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 006/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 007/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
module DerivedGen

import AlternativeCore
import PrintDerivation

import Deriving.DepTyCheck.Gen

%default total

Expand All @@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 007/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 007/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
6 changes: 4 additions & 2 deletions tests/derivation/infra/empty-body print 008/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
1 change: 0 additions & 1 deletion tests/derivation/infra/empty-body print 008/PrintDerivation.idr
View file
Open in desktop

This file was deleted.

8 changes: 3 additions & 5 deletions tests/derivation/infra/empty-body print 008/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
2 changes: 2 additions & 0 deletions tests/derivation/infra/empty-body run 001/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module DerivedGen

import AlternativeCore

import Deriving.DepTyCheck.Gen
import RunDerivedGen

%default total
Expand Down
2 changes: 2 additions & 0 deletions tests/derivation/infra/empty-body run 002/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module DerivedGen

import AlternativeCore

import Deriving.DepTyCheck.Gen
import RunDerivedGen

%default total
Expand Down
2 changes: 2 additions & 0 deletions tests/derivation/infra/empty-body run 003/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module DerivedGen

import AlternativeCore

import Deriving.DepTyCheck.Gen
import RunDerivedGen

%default total
Expand Down
2 changes: 2 additions & 0 deletions tests/derivation/infra/empty-body run 004/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module DerivedGen

import AlternativeCore

import Deriving.DepTyCheck.Gen
import RunDerivedGen

%default total
Expand Down
2 changes: 2 additions & 0 deletions tests/derivation/infra/empty-body run 005/DerivedGen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module DerivedGen

import AlternativeCore

import Deriving.DepTyCheck.Gen
import RunDerivedGen

%default total
Expand Down
Loading