From 1e54fb7a180153ae3cb8fbf8188253ede9b4a23d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 14 Aug 2024 23:13:21 +0300 Subject: [PATCH] [ derive ] Implement a multi-stage (layered) algorithm of order search --- deptycheck.ipkg | 1 + .../tests/gens/covering-seqs-long/Main.idr | 28 ++ .../tests/gens/covering-seqs-long/expected | 65 +++ .../tests/gens/covering-seqs-long/run | 6 + .../tests/gens/covering-seqs-long/test.ipkg | 6 + .../tests/gens/covering-seqs/expected | 80 ++-- .../covering-seq/tests/gens/print/expected | 292 +++++--------- .../tests/gens/sorted/expected | 40 +- .../uniq-list/tests/gens/uniq-list/expected | 16 +- .../tests/gens/uniq-vect-spare/expected | 20 +- .../tests/gens/uniq-vect-tight/expected | 20 +- .../DepTyCheck/Gen/Core/ConsDerive.idr | 127 +++--- .../core/norec nodep noext 002/expected | 2 +- .../core/norec nodep w_ext 002/expected | 12 +- .../core/norec nodep w_ext 003/expected | 12 +- .../core/norec nodep w_ext 004/expected | 2 +- .../core/norec t-..->p. noext 001/expected | 8 +- .../core/norec t-..->p. noext 002/expected | 10 +- .../core/typealias con 001/expected | 2 +- .../core/typealias con 002/expected | 2 +- .../print/adt/004 noparam/expected | 6 +- .../adt/010 right-to-left long-dpair/expected | 4 +- .../adt/011 right-to-left long-dpair/expected | 80 ++-- .../adt/013 right-to-left nondet/expected | 4 +- .../adt/014 right-to-left nondet ext/expected | 8 +- .../print/gadt/004 right-to-left det/expected | 4 +- .../least-effort/print/gadt/005 gadt/expected | 14 +- .../least-effort/print/gadt/006 gadt/expected | 16 +- .../print/order/001 complex order/expected | 256 ++++-------- .../print/order/002 complex order/expected | 377 +++++++----------- .../print/order/003 complex order/expected | 256 ++++-------- .../print/order/004 complex order/expected | 198 +++------ .../print/order/005 complex order/expected | 193 ++++----- .../least-effort/run/adt/004 noparam/expected | 20 +- .../adt/010 right-to-left long-dpair/expected | 20 +- .../run/adt/013 right-to-left nondet/expected | 18 +- .../adt/014 right-to-left nondet ext/expected | 12 +- .../run/gadt/004 right-to-left det/expected | 10 +- .../least-effort/run/gadt/005 gadt/expected | 6 +- .../least-effort/run/gadt/006 gadt/expected | 8 +- .../run/order/001 complex order/expected | 24 ++ .../run/order/002 complex order/expected | 24 ++ .../run/order/003 complex order/expected | 24 ++ .../run/order/004 complex order/expected | 24 ++ .../run/order/005 complex order/expected | 24 ++ .../run/order/006 complex order/expected | 24 ++ 46 files changed, 1147 insertions(+), 1258 deletions(-) create mode 100644 examples/covering-seq/tests/gens/covering-seqs-long/Main.idr create mode 100644 examples/covering-seq/tests/gens/covering-seqs-long/expected create mode 100755 examples/covering-seq/tests/gens/covering-seqs-long/run create mode 100644 examples/covering-seq/tests/gens/covering-seqs-long/test.ipkg create mode 100644 tests/derivation/least-effort/run/order/001 complex order/expected create mode 100644 tests/derivation/least-effort/run/order/002 complex order/expected create mode 100644 tests/derivation/least-effort/run/order/003 complex order/expected create mode 100644 tests/derivation/least-effort/run/order/004 complex order/expected create mode 100644 tests/derivation/least-effort/run/order/005 complex order/expected create mode 100644 tests/derivation/least-effort/run/order/006 complex order/expected diff --git a/deptycheck.ipkg b/deptycheck.ipkg index d6276a38f..af31ffc57 100644 --- a/deptycheck.ipkg +++ b/deptycheck.ipkg @@ -31,6 +31,7 @@ modules = Deriving.DepTyCheck depends = ansi , best-alternative , collection-utils + , cozippable , dependent-vect , elab-pretty , elab-util diff --git a/examples/covering-seq/tests/gens/covering-seqs-long/Main.idr b/examples/covering-seq/tests/gens/covering-seqs-long/Main.idr new file mode 100644 index 000000000..527cfc9bc --- /dev/null +++ b/examples/covering-seq/tests/gens/covering-seqs-long/Main.idr @@ -0,0 +1,28 @@ +import Data.Fuel +import Data.List +import Data.List.Lazy +import Data.List.Covering.Gen +import Data.String + +import System.Random.Pure.StdGen + +%default total + +submain : {n : _} -> BitMask n -> IO () +submain bs = do + putStrLn "-----------------------" + putStrLn "bitmask: \{bs}" + putStrLn "-----------------------" + let vals = unGenTryN 10 someStdGen $ genCoveringSequence (limit $ 2 * n) bs + Lazy.for_ vals $ \v => do + let hits = hits v + let verdict = if sort hits == setBits bs then "ok" else "fail, hits are: \{show hits}, expected: \{show $ setBits bs}" + putStrLn "\{v} (\{verdict})" + +main : IO () +main = do + submain [True, True, True, True, True, True, True, True] + submain [True, False, True, True, True, True, True, True] + submain [True, False, True, False, True, False, True, False] + submain [False, False, True, False, False, False, False, False] + submain [False, False, False, False, False, False, False, False] diff --git a/examples/covering-seq/tests/gens/covering-seqs-long/expected b/examples/covering-seq/tests/gens/covering-seqs-long/expected new file mode 100644 index 000000000..04f37fde9 --- /dev/null +++ b/examples/covering-seq/tests/gens/covering-seqs-long/expected @@ -0,0 +1,65 @@ +----------------------- +bitmask: 11111111 +----------------------- +10 0 [7] 14 [6] 7 6 13 [0] 5 8 [5] [4] [3] [2] [1] (ok) +[6] [7] 3 16 2 11 [5] [4] 2 [3] [2] 1 [1] [0] 3 (ok) +3 10 [7] 15 [6] 2 [5] [4] [3] 5 16 16 13 [2] [1] [0] (ok) +10 [7] 11 7 [3] 6 1 8 2 12 [6] [5] [4] [2] [1] [0] (ok) +[4] [7] [6] 2 [5] [3] [2] 1 [1] 14 15 6 13 3 3 [0] (ok) +[6] [0] [7] [5] 10 [4] [3] [2] [1] 14 7 16 4 15 7 (ok) +[5] [7] 7 7 9 [4] 3 [2] 2 6 [6] [3] 16 9 [1] [0] (ok) +7 3 12 0 [4] [2] 13 [1] 8 4 [0] 2 [6] [7] [5] [3] (ok) +9 [7] 4 [6] [5] [4] 12 12 14 [3] [2] 8 4 [1] [0] 6 (ok) +2 [7] 4 8 11 [3] [6] 13 [5] [4] 10 [2] 0 2 [1] [0] (ok) +----------------------- +bitmask: 10111111 +----------------------- +6 10 [7] 0 [6] 14 7 6 [0] 13 5 [5] [4] 11 [3] [2] (ok) +[7] 16 [6] [5] 2 [4] [3] [2] [0] 11 2 (ok) +16 3 10 15 2 5 16 [7] [4] [6] [5] [3] [2] 16 [0] 13 (ok) +15 4 10 [7] 11 [6] [5] [4] [3] [2] 7 6 1 8 2 [0] (ok) +[7] 1 [6] 14 15 [5] [4] [3] 6 [2] [0] 6 (ok) +10 14 7 [6] [0] [7] [5] 16 [4] 4 15 7 0 [3] [2] 4 (ok) +[5] [7] 0 7 7 [4] 9 [2] 3 2 [6] [3] 6 16 9 [0] (ok) +12 [6] [3] 0 [5] [7] [4] 13 8 [2] 3 [0] (ok) +4 [0] [7] 12 12 [6] 14 [3] 8 4 5 [5] 11 15 [4] [2] (ok) +8 [7] [6] 11 13 10 [3] [5] [4] [2] 0 3 [0] 4 (ok) +----------------------- +bitmask: 10101010 +----------------------- +7 6 [6] 13 5 [4] [2] 11 6 [0] 15 (ok) +1 [6] [4] 6 [2] [0] 5 12 2 11 13 (ok) +[2] [6] 2 5 [4] [0] 16 16 13 14 13 3 15 (ok) +6 1 8 2 12 [6] [4] 12 16 [2] [0] 11 6 (ok) +6 2 [4] 1 14 15 [6] 6 13 [2] 3 6 [0] 14 16 15 (ok) +[0] [6] [4] 15 [2] 7 0 6 6 (ok) +8 16 [0] 12 [6] [4] [2] 4 0 4 2 8 5 14 (ok) +3 [6] 8 [4] [2] [0] 0 7 3 12 (ok) +12 [6] 0 [4] 13 8 4 8 [2] 6 [0] (ok) +14 [0] [6] 8 4 5 [4] 12 [2] 15 9 (ok) +----------------------- +bitmask: 00100000 +----------------------- +7 6 [2] 13 5 11 13 14 0 (ok) +16 [2] 2 11 2 1 6 5 12 2 11 14 7 (ok) +16 11 1 16 3 10 15 [2] 2 5 16 16 13 14 13 (ok) +[2] 6 14 16 15 4 10 11 7 6 1 8 5 (ok) +[2] 6 (ok) +6 [2] 2 1 14 5 (ok) +[2] 15 7 0 6 4 14 6 (ok) +3 2 [2] 6 16 8 16 12 4 0 4 2 8 5 10 13 (ok) +8 8 [2] 15 7 3 4 0 3 8 0 2 (ok) +16 13 15 [2] 10 7 3 12 8 (ok) +----------------------- +bitmask: 00000000 +----------------------- +14 7 6 13 5 11 13 14 5 2 (ok) + (ok) +1 6 5 12 2 0 16 (ok) +2 1 (ok) +16 11 1 16 3 10 15 2 5 16 16 13 14 13 0 16 (ok) +6 14 16 15 4 10 11 7 6 1 8 5 (ok) +15 6 6 (ok) +14 7 16 4 15 7 0 6 4 14 13 6 0 1 (ok) +6 16 8 16 12 4 0 4 2 7 (ok) +7 7 (ok) diff --git a/examples/covering-seq/tests/gens/covering-seqs-long/run b/examples/covering-seq/tests/gens/covering-seqs-long/run new file mode 100755 index 000000000..3445c95bf --- /dev/null +++ b/examples/covering-seq/tests/gens/covering-seqs-long/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps test.ipkg && \ +pack run test.ipkg + +rm -rf build diff --git a/examples/covering-seq/tests/gens/covering-seqs-long/test.ipkg b/examples/covering-seq/tests/gens/covering-seqs-long/test.ipkg new file mode 100644 index 000000000..a094bbec5 --- /dev/null +++ b/examples/covering-seq/tests/gens/covering-seqs-long/test.ipkg @@ -0,0 +1,6 @@ +package a-test + +depends = covering-seq + +executable = a-test +main = Main diff --git a/examples/covering-seq/tests/gens/covering-seqs/expected b/examples/covering-seq/tests/gens/covering-seqs/expected index 19014a5c4..c5b0a61ea 100644 --- a/examples/covering-seq/tests/gens/covering-seqs/expected +++ b/examples/covering-seq/tests/gens/covering-seqs/expected @@ -1,52 +1,52 @@ ----------------------- bitmask: 1111 ----------------------- -3 3 [1] [3] [2] [0] 5 (ok) -[2] [3] [1] [0] (ok) -[3] [2] [1] 1 [0] 2 (ok) -5 3 3 4 [3] [2] [1] [0] (ok) -1 6 4 2 [3] [0] [2] [1] (ok) -0 1 [3] [2] 7 [1] [0] (ok) -8 5 [3] 5 [2] 7 [1] [0] (ok) -[3] 7 [2] [1] 5 [0] 6 (ok) -[3] [2] 5 [1] [0] (ok) -[3] 4 [2] 3 [1] [0] 2 8 (ok) +5 [2] 7 6 5 [1] [3] [0] (ok) +4 [2] [3] [1] 0 [0] 6 6 (ok) +4 [3] 3 [0] [2] 0 3 [1] (ok) +1 [3] 0 8 1 [1] [2] [0] (ok) +4 [3] [2] [1] 1 0 [0] (ok) +[3] [2] 7 7 3 8 [1] [0] (ok) +7 3 7 8 [3] [2] [1] [0] (ok) +[3] 2 6 6 5 [2] [1] [0] (ok) +1 [0] 1 5 7 [3] [2] [1] (ok) +[3] 3 [2] [1] [0] 4 2 (ok) ----------------------- bitmask: 1011 ----------------------- -3 3 [3] 4 [2] [0] 5 (ok) -[2] [3] [0] (ok) -8 6 [0] [3] 2 [2] 6 (ok) -[3] 3 4 6 1 8 [2] [0] (ok) -[3] 5 0 [2] [0] 3 (ok) -[3] 7 7 [2] [0] (ok) -7 [3] 8 3 7 [2] [0] 7 (ok) -[3] 8 [2] 0 0 5 [0] (ok) -7 [3] [2] 3 8 8 [0] 4 (ok) -[3] 4 [2] 5 [0] 4 2 6 (ok) +7 [2] 6 7 5 [3] 0 [0] (ok) +3 0 [3] [2] [0] (ok) +[3] [2] 8 [0] 6 1 4 0 (ok) +[3] 2 [0] 6 [2] 4 0 4 (ok) +1 6 5 1 [3] 4 [2] [0] (ok) +3 7 7 7 [3] 5 [2] [0] (ok) +[3] [2] 5 7 [0] 6 8 (ok) +1 [3] 0 2 6 [2] [0] 5 (ok) +5 1 [3] 1 [2] [0] 5 3 (ok) +8 4 [3] 8 [2] [0] 3 2 (ok) ----------------------- bitmask: 0010 ----------------------- -3 3 [2] 1 4 (ok) -8 7 5 2 [2] 0 3 8 (ok) -[2] 0 4 (ok) -0 8 [2] (ok) -[2] 4 (ok) -6 1 8 1 6 4 2 [2] (ok) -7 1 [2] 5 7 (ok) -8 5 [2] 7 8 7 3 (ok) -8 5 7 8 [2] 8 6 (ok) -[2] 7 5 5 (ok) +7 [2] 6 7 5 4 (ok) +6 8 [2] 3 3 (ok) +[2] 4 3 0 5 8 1 (ok) +8 [2] 2 6 (ok) +7 [2] 4 1 6 5 1 (ok) +5 [2] 3 7 7 7 (ok) +6 2 5 7 [2] 6 8 (ok) +1 0 2 [2] 6 (ok) +5 1 [2] 1 5 3 7 (ok) +4 8 [2] 3 4 2 (ok) ----------------------- bitmask: 0000 ----------------------- -3 3 1 4 4 (ok) -8 7 5 2 2 1 3 8 (ok) -0 4 6 8 5 (ok) -3 4 (ok) -6 1 8 (ok) -4 2 1 2 5 1 2 7 (ok) -5 7 7 7 0 (ok) -7 5 8 6 7 5 (ok) -8 7 6 2 (ok) -8 7 3 5 (ok) +2 (ok) +0 (ok) +5 5 7 6 3 (ok) +0 6 8 3 (ok) +0 5 8 1 (ok) +0 7 2 (ok) +1 0 8 4 (ok) +7 4 1 6 5 1 (ok) +7 5 (ok) +7 6 8 5 7 5 5 (ok) diff --git a/examples/covering-seq/tests/gens/print/expected b/examples/covering-seq/tests/gens/print/expected index 9899c0753..df23ac814 100644 --- a/examples/covering-seq/tests/gens/print/expected +++ b/examples/covering-seq/tests/gens/print/expected @@ -28,28 +28,22 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1, 2, 3]" + { name = "[0, 2, 3]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Basics.Bool") + .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Basics.Bool") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "Data.List.Covering.BitMask.Index.AtIndex" .$ var "n" .$ var "{arg:2}" .$ var "{arg:3}" .$ var "{arg:4}") - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[0]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Data.List.Covering.BitMask.Index.AtIndex" + .$ var "n" + .$ var "{arg:4}" + .$ var "{arg:2}" + .$ var "{arg:3}")) }) , IClaim emptyFC @@ -173,34 +167,37 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.List.Covering.Hit (orders)")) .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1, 2, 3]" - .$ var "^outmost-fuel^" - .$ var "n" - .$ var "i" - .$ var "bs" - .$ var "Prelude.Basics.True") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{conArg:2}") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1]" - .$ var "^cons_fuel^" - .$ var "n" - .$ ( var "Data.List.Covering.BitMask.update" - .! ("n", var "n") - .$ var "i" - .$ var "Prelude.Basics.False" - .$ var "bs")) - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:9}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Data.List.Covering.Hit" - .! ("n", var "n") - .! ("bs", var "bs") - .$ var "i" - .@ var "^bnd^{conArg:2}" - .$ var "^bnd^{arg:9}"))))) + .$ ( var "[0, 2, 3]" + .$ var "^outmost-fuel^" + .$ var "n" + .$ var "bs" + .$ var "Prelude.Basics.True") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "^bnd^{conArg:2}" + .= var ">>=" + .$ ( var "[0, 1]" + .$ var "^cons_fuel^" + .$ var "n" + .$ ( var "Data.List.Covering.BitMask.update" + .! ("n", var "n") + .$ var "i" + .$ var "Prelude.Basics.False" + .$ var "bs")) + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:9}") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Data.List.Covering.Hit" + .! ("n", var "n") + .! ("bs", var "bs") + .$ var "i" + .@ var "^bnd^{conArg:2}" + .$ var "^bnd^{arg:9}")) + ] + })) ] ] , scope = @@ -244,13 +241,12 @@ LOG gen.auto.derive.infra:0: ] , IDef emptyFC - "[0, 1, 2, 3]" - [ var "[0, 1, 2, 3]" + "[0, 2, 3]" + [ var "[0, 2, 3]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:2}>" .$ bindVar "inter^<{arg:3}>" - .$ bindVar "inter^<{arg:4}>" .= local { decls = [ IClaim @@ -263,16 +259,18 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Basics.Bool") + .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Basics.Bool") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Data.List.Covering.BitMask.Index.AtIndex" - .$ var "n" - .$ var "{arg:2}" - .$ var "{arg:3}" - .$ var "{arg:4}") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Data.List.Covering.BitMask.Index.AtIndex" + .$ var "n" + .$ var "{arg:4}" + .$ var "{arg:2}" + .$ var "{arg:3}")) }) , IClaim emptyFC @@ -284,16 +282,18 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") - .-> MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Basics.Bool") + .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Covering.BitMask.BitMask" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Basics.Bool") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Data.List.Covering.BitMask.Index.AtIndex" - .$ var "n" - .$ var "{arg:2}" - .$ var "{arg:3}" - .$ var "{arg:4}") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Data.List.Covering.BitMask.Index.AtIndex" + .$ var "n" + .$ var "{arg:4}" + .$ var "{arg:2}" + .$ var "{arg:3}")) }) , IDef emptyFC @@ -303,7 +303,6 @@ LOG gen.auto.derive.infra:0: var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FZ" .! ("k", implicitTrue)) .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "to_be_deceqed^^b0" , rig = MW @@ -314,7 +313,6 @@ LOG gen.auto.derive.infra:0: [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FZ" .! ("k", implicitTrue)) .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "b" .$ (var "Prelude.Yes" .$ var "Builtin.Refl") @@ -322,23 +320,22 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.Here (orders)")) .$ ( var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.List.Covering.BitMask.Index.Here" .! ("n", var "n") .! ("bs", var "bs") .! ("b", var "b"))) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Data.List.Covering.BitMask.Index.Here" + .! ("n", var "n") + .! ("bs", var "bs") + .! ("b", var "b")))) , var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FZ" .! ("k", implicitTrue)) .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "to_be_deceqed^^b0" .$ (var "Prelude.No" .$ implicitTrue) .= var "empty" ] } - , var "<>" - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef @@ -347,34 +344,36 @@ LOG gen.auto.derive.infra:0: [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "i") .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "v" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.There (orders)")) .$ ( var ">>=" - .$ ( var "[0, 1, 2, 3]" + .$ ( var "[0, 2, 3]" .$ var "^cons_fuel^" .$ var "n" - .$ var "i" .$ var "bs" .$ var "v") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:10}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Data.List.Covering.BitMask.Index.There" - .! ("b", var "b") - .! ("v", var "v") - .! ("n", var "n") - .! ("bs", var "bs") - .! ("i", var "i") - .$ var "^bnd^{arg:10}"))) - , var "<>" - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue - .$ implicitTrue + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "^bnd^{arg:10}" + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Data.List.Covering.BitMask.Index.There" + .! ("b", var "b") + .! ("v", var "v") + .! ("n", var "n") + .! ("bs", var "bs") + .! ("i", var "i") + .$ var "^bnd^{arg:10}")) + ] + })) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] @@ -385,16 +384,15 @@ LOG gen.auto.derive.infra:0: , clauses = [ var "Data.Fuel.Dry" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.AtIndex[0, 1, 2, 3] (dry fuel)")) + .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.AtIndex[0, 2, 3] (dry fuel)")) .$ ( var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^" .$ var "inter^<{arg:2}>" - .$ var "inter^<{arg:3}>" - .$ var "inter^<{arg:4}>") + .$ var "inter^<{arg:3}>") , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.AtIndex[0, 1, 2, 3] (spend fuel)")) + .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.AtIndex[0, 2, 3] (spend fuel)")) .$ ( var "Test.DepTyCheck.Gen.frequency" .$ ( var "::" .$ ( var "Builtin.MkPair" @@ -403,8 +401,7 @@ LOG gen.auto.derive.infra:0: .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>" - .$ var "inter^<{arg:3}>" - .$ var "inter^<{arg:4}>")) + .$ var "inter^<{arg:3}>")) .$ ( var "::" .$ ( var "Builtin.MkPair" .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") @@ -412,94 +409,7 @@ LOG gen.auto.derive.infra:0: .$ var "^sub^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>" - .$ var "inter^<{arg:3}>" - .$ var "inter^<{arg:4}>")) - .$ var "Nil"))) - ] - } - } - ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "Data.Fin.Fin" .$ var "n") - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "Data.Fin.Fin" .$ var "n") - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.FZ (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FZ" .! ("k", var "k"))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) - .$ ( var ">>=" - .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:11}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:11}"))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - ] - , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ var "Data.Nat1.one" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^")) + .$ var "inter^<{arg:3}>")) .$ var "Nil"))) ] } @@ -549,10 +459,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:12}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:11}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:12}"))) + .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:11}"))) ] ] , scope = @@ -666,14 +576,14 @@ LOG gen.auto.derive.infra:0: .$ var "n" .$ var "b" .$ var "bs") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:13}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:12}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Data.List.Covering.BitMask.Index.Continue" .! ("n", var "n") .! ("bs", var "bs") .! ("b", var "b") - .$ var "^bnd^{arg:13}"))) + .$ var "^bnd^{arg:12}"))) , var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") diff --git a/examples/sorted-tree-indexed/tests/gens/sorted/expected b/examples/sorted-tree-indexed/tests/gens/sorted/expected index e75f68e28..c34e9cec8 100644 --- a/examples/sorted-tree-indexed/tests/gens/sorted/expected +++ b/examples/sorted-tree-indexed/tests/gens/sorted/expected @@ -1,40 +1,40 @@ -------------- -min: 0, max: 7, length: 5 -as list: [0, 1, 2, 3, 7] +min: 0, max: 1, length: 2 +as list: [0, 1] sorted: True -------------- -min: 1, max: 6, length: 3 -as list: [1, 2, 6] +min: 1, max: 3, length: 3 +as list: [1, 2, 3] sorted: True -------------- -min: 0, max: 7, length: 4 -as list: [0, 2, 3, 7] +min: 0, max: 4, length: 5 +as list: [0, 1, 2, 3, 4] sorted: True -------------- -min: 0, max: 5, length: 5 -as list: [0, 1, 2, 3, 5] +min: 0, max: 1, length: 2 +as list: [0, 1] sorted: True -------------- -min: 1, max: 5, length: 4 -as list: [1, 2, 3, 5] +min: 2, max: 2, length: 1 +as list: [2] sorted: True -------------- -min: 0, max: 8, length: 3 -as list: [0, 3, 8] +min: 0, max: 4, length: 5 +as list: [0, 1, 2, 3, 4] sorted: True -------------- -min: 2, max: 2, length: 1 -as list: [2] +min: 3, max: 3, length: 1 +as list: [3] sorted: True -------------- -min: 2, max: 7, length: 3 -as list: [2, 3, 7] +min: 4, max: 4, length: 1 +as list: [4] sorted: True -------------- -min: 0, max: 4, length: 3 -as list: [0, 3, 4] +min: 0, max: 4, length: 5 +as list: [0, 1, 2, 3, 4] sorted: True -------------- -min: 2, max: 2, length: 1 -as list: [2] +min: 0, max: 3, length: 4 +as list: [0, 1, 2, 3] sorted: True diff --git a/examples/uniq-list/tests/gens/uniq-list/expected b/examples/uniq-list/tests/gens/uniq-list/expected index 1a51887f2..bb3fa34d6 100644 --- a/examples/uniq-list/tests/gens/uniq-list/expected +++ b/examples/uniq-list/tests/gens/uniq-list/expected @@ -5,26 +5,26 @@ uniq: True list: ["g"] uniq: True ----------- -list: ["a", "d", "c", "h"] +list: ["g", "b", "f"] uniq: True ----------- -list: ["c", "b"] +list: ["f", "g", "a", "d"] uniq: True ----------- -list: ["b", "c", "a", "h", "g", "d", "f"] +list: ["h", "c", "g"] uniq: True ----------- -list: ["c", "a", "b", "f", "d"] +list: ["h", "g", "b", "d", "c"] uniq: True ----------- -list: ["b", "g", "f", "c", "a", "d", "h"] +list: ["c", "b"] uniq: True ----------- -list: ["h", "f", "a"] +list: ["d", "a", "h"] uniq: True ----------- -list: ["h", "c", "a", "d", "g", "b"] +list: ["g", "a", "h", "c", "d", "b", "f"] uniq: True ----------- -list: ["g", "c", "b", "d"] +list: ["g", "c", "b", "h", "d", "f", "a"] uniq: True diff --git a/examples/uniq-list/tests/gens/uniq-vect-spare/expected b/examples/uniq-list/tests/gens/uniq-vect-spare/expected index 0c5203b8b..b14bad6f9 100644 --- a/examples/uniq-list/tests/gens/uniq-vect-spare/expected +++ b/examples/uniq-list/tests/gens/uniq-vect-spare/expected @@ -1,31 +1,31 @@ prenty of spare strings to generate from (7 for vects of length 4) ----------- -vect: ["g", "f", "b", "h"] +vect: ["g", "c", "a", "b"] uniq: True ----------- -vect: ["h", "b", "g", "f"] +vect: ["b", "c", "g", "a"] uniq: True ----------- -vect: ["h", "a", "c", "f"] +vect: ["b", "c", "d", "h"] uniq: True ----------- -vect: ["d", "c", "f", "a"] +vect: ["h", "g", "d", "c"] uniq: True ----------- -vect: ["a", "b", "d", "h"] +vect: ["a", "b", "g", "c"] uniq: True ----------- -vect: ["h", "f", "d", "a"] +vect: ["f", "b", "h", "g"] uniq: True ----------- -vect: ["a", "c", "f", "h"] +vect: ["g", "f", "c", "a"] uniq: True ----------- -vect: ["h", "f", "b", "c"] +vect: ["a", "h", "d", "g"] uniq: True ----------- -vect: ["a", "d", "f", "c"] +vect: ["a", "c", "d", "f"] uniq: True ----------- -vect: ["f", "a", "d", "b"] +vect: ["c", "d", "f", "a"] uniq: True diff --git a/examples/uniq-list/tests/gens/uniq-vect-tight/expected b/examples/uniq-list/tests/gens/uniq-vect-tight/expected index 8b16d9612..c504454fa 100644 --- a/examples/uniq-list/tests/gens/uniq-vect-tight/expected +++ b/examples/uniq-list/tests/gens/uniq-vect-tight/expected @@ -1,31 +1,31 @@ no spare strings to generate from (4 for vects of length 4) ----------- -vect: ["b", "a", "d", "c"] +vect: ["b", "d", "a", "c"] uniq: True ----------- -vect: ["c", "b", "d", "a"] +vect: ["d", "c", "a", "b"] uniq: True ----------- -vect: ["c", "b", "d", "a"] +vect: ["d", "c", "a", "b"] uniq: True ----------- -vect: ["d", "c", "a", "b"] +vect: ["c", "b", "a", "d"] uniq: True ----------- -vect: ["d", "b", "c", "a"] +vect: ["d", "c", "b", "a"] uniq: True ----------- -vect: ["a", "d", "c", "b"] +vect: ["a", "b", "d", "c"] uniq: True ----------- -vect: ["d", "b", "c", "a"] +vect: ["b", "d", "c", "a"] uniq: True ----------- -vect: ["a", "d", "c", "b"] +vect: ["a", "b", "c", "d"] uniq: True ----------- -vect: ["c", "a", "b", "d"] +vect: ["b", "c", "a", "d"] uniq: True ----------- -vect: ["b", "a", "c", "d"] +vect: ["c", "b", "a", "d"] uniq: True diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 8512aed18..58b43e0b6 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -4,6 +4,7 @@ module Deriving.DepTyCheck.Gen.Core.ConsDerive import public Control.Monad.State import public Data.Collections.Analysis +import public Data.Cozippable import public Data.Either import public Data.SortedSet.Extra @@ -13,6 +14,14 @@ import public Deriving.DepTyCheck.Gen.Derive %default total +Foldable Identity where + foldr f init (Id x) = f x init + foldl f init (Id x) = f init x + null _ = False + foldlM f init (Id x) = f init x + toList (Id x) = [x] + foldMap f (Id x) = f x + ------------------------------------------------- --- Derivation of a generator for constructor --- ------------------------------------------------- @@ -30,6 +39,58 @@ interface ConstructorDerivator where --- Particular tactics --- +record Determination (0 con : Con) where + constructor MkDetermination + ||| Args which cannot be determined by this arg, e.g. because it is used in a non-trivial expression. + stronglyDeterminingArgs : SortedSet $ Fin con.args.length + ||| Args which this args depends on, which are not strongly determining. + determinableArgs : SortedSet $ Fin con.args.length + ||| Reverse of `determinableArgs`, i.e. args which depend on this arg, which are not strongly determined by this arg. + weaklyDeterminingArgs : SortedSet $ Fin con.args.length + +mapDetermination : {0 con : Con} -> (SortedSet (Fin con.args.length) -> SortedSet (Fin con.args.length)) -> Determination con -> Determination con +mapDetermination f $ MkDetermination sda da wda = MkDetermination (f sda) (f da) (f wda) + +removeDeeply : Foldable f => + (toRemove : f $ Fin con.args.length) -> + (fromWhat : SortedMap .| Fin con.args.length .| Determination con) -> + SortedMap .| Fin con.args.length .| Determination con +removeDeeply toRemove fromWhat = foldl delete' fromWhat toRemove <&> mapDetermination (\s => foldl delete' s toRemove) + +searchOrder : (left : SortedMap .| Fin con.args.length .| Determination con) -> + List $ Fin con.args.length +searchOrder left = do + -- find all arguments that are not stongly determined by anyone + let nonStronglyDetermined = filter (\(_, det) => null det.stronglyDeterminingArgs) $ SortedMap.toList left + + -- finish is nothing appropriate left + let False = null nonStronglyDetermined | True => [] + + -- among them find all that are not determined even weakly, if any + let notDetermined = filter (\(_, det) => null det.weaklyDeterminingArgs) $ nonStronglyDetermined + + -- choose the group of args that can go next + let curr = if not $ null notDetermined then notDetermined else nonStronglyDetermined + + -- choose the one from the variants + -- It's important to do so, since after discharging one of the selected variable, set of available variants can extend + -- (e.g. because of discharging of strong determination), and new alternative have more priority than current ones. + -- TODO to determine the best among current variants taking into account which indices are more complex (transitively!) + let Just curr = last' curr + | Nothing => [] + + -- compute set of arguments that will be determined by the currently chosen args + let determined = determinableArgs $ snd curr + + -- clean up representation + let curr = fst curr + + -- remove information about all currently chosen args + let next = removeDeeply .| Id curr .| removeDeeply determined left + + -- `next` is smaller than `left` because `curr` must be not empty + curr :: searchOrder (assert_smaller left next) + ||| "Non-obligatory" means that some present external generator of some type ||| may be ignored even if its type is really used in a generated data constructor. namespace NonObligatoryExts @@ -153,61 +214,33 @@ namespace NonObligatoryExts let consExpr = wrapImpls $ sig.targetType.args.length `minus` sig.givenParams.size `(Prelude.pure {f=Test.DepTyCheck.Gen.Gen _} ~consExpr) - -- Get dependencies of constructor's arguments - rawDeps <- argDeps con.args - let deps = downmap ((`difference` givs) . mapIn weakenToSuper) rawDeps - - ------------------------------------------------- - -- Left-to-right generation phase (2nd phase) --- - ------------------------------------------------- - - -- Determine which arguments need to be generated in a left-to-right manner - let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\((MkTypeApp _ _ as), _) => any isRight as) $ toListI argsTypeApps - - -------------------------------------------------------------------------------- - -- Preparation of input for the left-to-right phase (1st right-to-left phase) -- - -------------------------------------------------------------------------------- - - -- Acquire those variables that appear in non-trivial type expressions, i.e. those which needs to be generated before the left-to-right phase - let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ _ as) => rights (toList as) >>= allVarNames - let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR - - -- Find rightmost arguments among `preLTR` - let depsLTR = SortedSet.fromList $ - mapMaybe (\(ds, idx) => whenT .| contains idx preLTR && null ds .| idx) $ - toListI $ deps <&> intersection preLTR + -------------------------------------------- + -- Compute possible orders of generation --- + -------------------------------------------- - --------------------------------------------------------------------------------- - -- Main right-to-left generation phase (3rd phase aka 2nd right-to-left phase) -- - --------------------------------------------------------------------------------- + -- Compute a map of which arguments each argument depends on + let canBeDetermined = concat $ join $ Prelude.toList $ flip mapI argsTypeApps $ \i, tya => + map (\v => singleton v $ SortedSet.singleton i) $ SortedSet.toList $ argsCanDetermine tya - -- Arguments that no other argument depends on - let rightmostArgs = fromFoldable {f=Vect _} range `difference` (givs `union` concat deps) + -- Compute determination map without weak determination information + let determ = insertFrom' empty $ mapI (\i, tya => (i, MkDetermination (argsDeterminedBy tya) (argsCanDetermine tya) empty)) argsTypeApps - --------------------------------------------------------------- - -- Manage different possible variants of generation ordering -- - --------------------------------------------------------------- - - -- Prepare info about which arguments are independent and thus can be ordered arbitrarily - let disjDeps = disjointDepSets rawDeps givs - - -- Acquire order(s) in what we will generate arguments - let allOrders = do - leftmost <- indepPermutations' disjDeps depsLTR - rightmost <- indepPermutations' disjDeps rightmostArgs - pure $ leftmost ++ leftToRightArgs ++ rightmost - - let allOrders = if simplificationHack then take 1 allOrders else allOrders - let allOrders = List.nub $ nub <$> allOrders - - for_ allOrders $ \order => - logPoint {level=10} "least-effort.order" [sig, con] "- one of used final orders: \{show order}" + -- Add weak determination info + let updWeakDeterm : These (Determination con) (SortedSet $ Fin con.args.length) -> Determination con + updWeakDeterm $ This d = d + updWeakDeterm $ That w = MkDetermination empty empty w + updWeakDeterm $ Both d w = {weaklyDeterminingArgs := w} d + let determ = cozipWith updWeakDeterm determ canBeDetermined -------------------------- -- Producing the result -- -------------------------- - callOneOf "\{show con.name} (orders)".label <$> traverse genForOrder allOrders + let theOrder = searchOrder $ removeDeeply givs determ + + logPoint {level=10} "least-effort.order" [sig, con] "- used final order: \{show theOrder}" + + labelGen "\{show con.name} (orders)".label <$> genForOrder theOrder where diff --git a/tests/derivation/core/norec nodep noext 002/expected b/tests/derivation/core/norec nodep noext 002/expected index f24349d0b..e8002ea6f 100644 --- a/tests/derivation/core/norec nodep noext 002/expected +++ b/tests/derivation/core/norec nodep noext 002/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 False True +X2 True False ----- X0 diff --git a/tests/derivation/core/norec nodep w_ext 002/expected b/tests/derivation/core/norec nodep w_ext 002/expected index 41f247885..3b1bbdba5 100644 --- a/tests/derivation/core/norec nodep w_ext 002/expected +++ b/tests/derivation/core/norec nodep w_ext 002/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX "a" "" +MkX "" "a" ----- MkX "" "" ----- -MkX "" "a" +MkX "a" "" ----- MkX "a" "a" ----- -MkX "" "a" +MkX "a" "" ----- -MkX "a" "bc" +MkX "bc" "a" ----- MkX "" "" ----- -MkX "bc" "a" +MkX "a" "bc" ----- MkX "a" "a" ----- -MkX "a" "" +MkX "" "a" diff --git a/tests/derivation/core/norec nodep w_ext 003/expected b/tests/derivation/core/norec nodep w_ext 003/expected index bca5e2eb1..283dfd585 100644 --- a/tests/derivation/core/norec nodep w_ext 003/expected +++ b/tests/derivation/core/norec nodep w_ext 003/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX "a" 0 +MkX "" 10 ----- MkX "" 0 ----- -MkX "" 10 +MkX "a" 0 ----- MkX "a" 10 ----- MkX "" 10 ----- -MkX "a" 0 ------ -MkX "" 10 +MkX "a" 10 ----- MkX "" 0 ----- -MkX "a" 10 +MkX "" 10 +----- +MkX "a" 0 ----- MkX "a" 10 diff --git a/tests/derivation/core/norec nodep w_ext 004/expected b/tests/derivation/core/norec nodep w_ext 004/expected index a598ad771..6da06a116 100644 --- a/tests/derivation/core/norec nodep w_ext 004/expected +++ b/tests/derivation/core/norec nodep w_ext 004/expected @@ -15,7 +15,7 @@ X1 "a" 10 ----- X3 "" ----- -X1 "bc" 10 +X1 "a" 0 ----- X2 10 ----- diff --git a/tests/derivation/core/norec t-..->p. noext 001/expected b/tests/derivation/core/norec t-..->p. noext 001/expected index f285def7a..424ef5e3c 100644 --- a/tests/derivation/core/norec t-..->p. noext 001/expected +++ b/tests/derivation/core/norec t-..->p. noext 001/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -(True ** (False ** MkX True False)) +(False ** (True ** MkX False True)) ----- (False ** (False ** MkX False False)) ----- -(False ** (True ** MkX False True)) +(True ** (False ** MkX True False)) ----- (True ** (True ** MkX True True)) ----- (True ** (True ** MkX True True)) ----- -(False ** (True ** MkX False True)) ------ (True ** (False ** MkX True False)) ----- (False ** (True ** MkX False True)) ----- +(True ** (False ** MkX True False)) +----- (False ** (False ** MkX False False)) ----- (True ** (True ** MkX True True)) diff --git a/tests/derivation/core/norec t-..->p. noext 002/expected b/tests/derivation/core/norec t-..->p. noext 002/expected index 7bb6de6e4..ea06853cc 100644 --- a/tests/derivation/core/norec t-..->p. noext 002/expected +++ b/tests/derivation/core/norec t-..->p. noext 002/expected @@ -5,11 +5,11 @@ Generated values: ----- (False ** (False ** X1)) ----- -(False ** (True ** X0 False True)) +(True ** (False ** X0 True False)) ----- (True ** (True ** X1)) ----- -(True ** (False ** X1)) +(False ** (True ** X1)) ----- (False ** (False ** X1)) ----- @@ -17,8 +17,8 @@ Generated values: ----- (True ** (True ** X1)) ----- -(False ** (True ** X1)) +(True ** (False ** X1)) ----- -(False ** (True ** X0 False True)) +(True ** (False ** X0 True False)) ----- -(False ** (True ** X1)) +(True ** (False ** X1)) diff --git a/tests/derivation/core/typealias con 001/expected b/tests/derivation/core/typealias con 001/expected index f24349d0b..e8002ea6f 100644 --- a/tests/derivation/core/typealias con 001/expected +++ b/tests/derivation/core/typealias con 001/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 False True +X2 True False ----- X0 diff --git a/tests/derivation/core/typealias con 002/expected b/tests/derivation/core/typealias con 002/expected index cd7fee414..db1387033 100644 --- a/tests/derivation/core/typealias con 002/expected +++ b/tests/derivation/core/typealias con 002/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 False 5 +X2 False 6 ----- X0 diff --git a/tests/derivation/least-effort/print/adt/004 noparam/expected b/tests/derivation/least-effort/print/adt/004 noparam/expected index 6b7165e57..edcccca69 100644 --- a/tests/derivation/least-effort/print/adt/004 noparam/expected +++ b/tests/derivation/least-effort/print/adt/004 noparam/expected @@ -71,14 +71,14 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.R (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") + .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:1}") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") + .$ (var "[]" .$ var "^cons_fuel^") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.R" .$ var "^bnd^{arg:1}" .$ var "^bnd^{arg:2}")))) + .$ (var "DerivedGen.R" .$ var "^bnd^{arg:2}" .$ var "^bnd^{arg:1}")))) ] ] , scope = diff --git a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected index e71b4834e..164f042c7 100644 --- a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected @@ -126,10 +126,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected index 0c547800c..14a47ffbc 100644 --- a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected @@ -42,10 +42,10 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" }) , IClaim emptyFC @@ -53,10 +53,10 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" }) , IDef emptyFC @@ -136,11 +136,11 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" @@ -156,38 +156,6 @@ LOG gen.auto.derive.infra:0: .$ (var "<>" .$ var "^fuel_arg^") } ] - , IDef - emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Builtin.MkUnit (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Builtin.MkUnit") - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Builtin.Unit[] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^") - } - ] , IDef emptyFC "[]" @@ -262,6 +230,38 @@ LOG gen.auto.derive.infra:0: } } ] + , IDef + emptyFC + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Builtin.MkUnit (orders)")) + .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Builtin.MkUnit") + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Builtin.Unit[] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^") + } + ] ] , scope = var "[]" .$ var "^outmost-fuel^" } diff --git a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected index b7ecd7eb4..dcc85b6fc 100644 --- a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected @@ -203,10 +203,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected index d2d217c37..4163abae0 100644 --- a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected +++ b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected @@ -201,11 +201,11 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" - .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected index da000ae97..1b4505fb2 100644 --- a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected +++ b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected @@ -454,10 +454,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/gadt/005 gadt/expected b/tests/derivation/least-effort/print/gadt/005 gadt/expected index 79fb99a1f..67280753c 100644 --- a/tests/derivation/least-effort/print/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/005 gadt/expected @@ -121,22 +121,22 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.JJ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse .=> var ">>=" .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.JJ" .! ("b", var "b") - .$ var "^bnd^{arg:4}" - .$ var "^bnd^{arg:5}")))))) + .$ var "^bnd^{arg:5}" + .$ var "^bnd^{arg:4}")))))) ] , IDef emptyFC diff --git a/tests/derivation/least-effort/print/gadt/006 gadt/expected b/tests/derivation/least-effort/print/gadt/006 gadt/expected index a0afbd896..c3e40272c 100644 --- a/tests/derivation/least-effort/print/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/006 gadt/expected @@ -133,7 +133,7 @@ LOG gen.auto.derive.infra:0: .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.JJ" .! ("b", var "b") .$ var "^bnd^{arg:4}" .$ var "^bnd^{arg:5}")))) + .$ (var "DerivedGen.JJ" .! ("b", var "b") .$ var "^bnd^{arg:5}" .$ var "^bnd^{arg:4}")))) ] , IDef emptyFC @@ -319,22 +319,22 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.JJ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse .=> var ">>=" .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.JJ" .! ("b", var "b") - .$ var "^bnd^{arg:4}" - .$ var "^bnd^{arg:5}")))))) + .$ var "^bnd^{arg:5}" + .$ var "^bnd^{arg:4}")))))) ] , IDef emptyFC diff --git a/tests/derivation/least-effort/print/order/001 complex order/expected b/tests/derivation/least-effort/print/order/001 complex order/expected index 16af5eda2..1a9b75c6a 100644 --- a/tests/derivation/least-effort/print/order/001 complex order/expected +++ b/tests/derivation/least-effort/print/order/001 complex order/expected @@ -23,16 +23,14 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0]" + { name = "[0, 1]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -40,25 +38,18 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -96,27 +87,26 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkZ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1]" - .$ var "^outmost-fuel^" - .$ var "n" - .$ (var "Data.Fin.finS" .! ("n", var "n") .$ var "i")) - .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse - .=> var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "y" - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "i" .$ var "x" .$ var "y") - ] - })))) + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "n" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "y") + .= var ">>=" + .$ ( var "[0, 1]" + .$ var "^outmost-fuel^" + .$ var "n" + .$ (var "Data.Fin.finS" .! ("n", var "n") .$ var "i")) + .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "i" .$ var "x" .$ var "y")) + ] + })) ] ] , scope = @@ -125,88 +115,10 @@ LOG gen.auto.derive.infra:0: .$ (var "<>" .$ var "^fuel_arg^") } ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) - .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y0" .! ("i", var "i"))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - , IDef - emptyFC - "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2")) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0] (non-recursive)")) - .$ ( var "Test.DepTyCheck.Gen.oneOf" - .! ("em", var "MaybeEmpty") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") - .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") .$ var "Nil"))) - } - ] , IDef emptyFC "[0, 1]" - [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:2}>" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" .= local { decls = [ IClaim @@ -219,10 +131,10 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -234,10 +146,10 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IDef emptyFC @@ -273,16 +185,16 @@ LOG gen.auto.derive.infra:0: .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>") + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>") + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") .$ var "Nil"))) } ] , IDef emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -291,10 +203,18 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -302,55 +222,55 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) + .$ ( var ">>=" + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y0" .! ("i", var "i")))))) ] , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:3}"))) + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2"))) ] ] , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) - .$ var "Nil"))) - ] - } + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[] (non-recursive)")) + .$ ( var "Test.DepTyCheck.Gen.oneOf" + .! ("em", var "MaybeEmpty") + .$ ( var "::" + .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] , IDef @@ -406,10 +326,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) .$ ( var ">>=" .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:4}"))) + .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:3}"))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/order/002 complex order/expected b/tests/derivation/least-effort/print/order/002 complex order/expected index dfe736cef..0a5c37ba2 100644 --- a/tests/derivation/least-effort/print/order/002 complex order/expected +++ b/tests/derivation/least-effort/print/order/002 complex order/expected @@ -23,19 +23,14 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0]" + { name = "[0, 1]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "Builtin.DPair.DPair" - .$ (var "DerivedGen.BS" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "DerivedGen.BS" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}" .$ var "{arg:2}"))) + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -43,14 +38,21 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:3}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Builtin.DPair.DPair" + .$ (var "DerivedGen.BS" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}" .$ var "{arg:3}")))) }) , IClaim emptyFC @@ -58,10 +60,11 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "DerivedGen.BS" .$ var "n") }) , IClaim emptyFC @@ -75,18 +78,6 @@ LOG gen.auto.derive.infra:0: .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[0]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "DerivedGen.BS" .$ var "n") - }) , IDef emptyFC "[]" @@ -111,34 +102,28 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkZ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1]" - .$ var "^outmost-fuel^" - .$ var "n" - .$ (var "DerivedGen.h" .! ("n", var "n") .$ var "i" .$ var "bs")) - .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse - .=> var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" - .$ bindVar "i" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "bs" .$ bindVar "y") - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "DerivedGen.MkZ" - .$ var "n" - .$ var "i" - .$ var "bs" - .$ var "x" - .$ var "y") - ] - })))) + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "n" + .$ ( var "Builtin.DPair.MkDPair" + .$ bindVar "i" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "bs" .$ bindVar "y")) + .= var ">>=" + .$ ( var "[0, 1]" + .$ var "^outmost-fuel^" + .$ var "n" + .$ (var "DerivedGen.h" .! ("n", var "n") .$ var "i" .$ var "bs")) + .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "i" .$ var "bs" .$ var "x" .$ var "y")) + ] + })) ] ] , scope = @@ -149,8 +134,8 @@ LOG gen.auto.derive.infra:0: ] , IDef emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" + "[0, 1]" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" .= local { decls = [ IClaim @@ -159,19 +144,14 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "Builtin.DPair.DPair" - .$ (var "DerivedGen.BS" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "DerivedGen.BS" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}" .$ var "{arg:2}"))) + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -179,76 +159,57 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "Builtin.DPair.DPair" - .$ (var "DerivedGen.BS" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "DerivedGen.BS" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}" .$ var "{arg:2}"))) + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") .$ bindVar "bs" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) - .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse - .=> var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ (var "DerivedGen.Y0" .! ("bs", var "bs") .! ("i", var "i"))))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "fromString" .$ primVal (Str "DerivedGen.X0 (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.X0" .! ("bs", var "bs"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef emptyFC - "<>" - [ var "<>" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) + .$ bindVar "bs" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) - .$ ( var ">>=" - .$ ( var "[0]" - .$ var "^outmost-fuel^" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) - .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y2" .! ("bs", var "bs")))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "fromString" .$ primVal (Str "DerivedGen.X2 (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.X2" .! ("bs", var "bs"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0] (non-recursive)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.X[0, 1] (non-recursive)")) .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") - .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") .$ var "Nil"))) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") + .$ ( var "::" + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") + .$ var "Nil"))) } ] , IDef emptyFC - "[0, 1]" - [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:3}>" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -257,14 +218,21 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:3}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Builtin.DPair.DPair" + .$ (var "DerivedGen.BS" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}" .$ var "{arg:3}")))) }) , IClaim emptyFC @@ -272,57 +240,80 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:3}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "Builtin.DPair.DPair" + .$ (var "DerivedGen.BS" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:3}") (var "DerivedGen.BS" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}" .$ var "{arg:3}")))) }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") .$ bindVar "bs" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X0 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.X0" .! ("bs", var "bs"))) - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) + .$ ( var ">>=" + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var ">>=" + .$ ( var "[0]" + .$ var "^outmost-fuel^" + .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "DerivedGen.Y0" .! ("bs", var "bs") .! ("i", var "i")))))))) ] , IDef emptyFC - "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) - .$ bindVar "bs" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X2 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.X2" .! ("bs", var "bs"))) - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) + .$ ( var ">>=" + .$ ( var "[0]" + .$ var "^outmost-fuel^" + .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) + .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y2" .! ("bs", var "bs"))))))) ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X[0, 1] (non-recursive)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[] (non-recursive)")) .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:3}>") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:3}>") - .$ var "Nil"))) + .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] , IDef emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .= local { decls = [ IClaim @@ -331,66 +322,29 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ (var "DerivedGen.BS" .$ var "n") }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") - ] - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:4}"))) + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkBS (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkBS" .! ("n", var "n"))) ] ] , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) - .$ var "Nil"))) - ] - } + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.BS[0] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") } ] , IDef @@ -446,10 +400,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) .$ ( var ">>=" .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:5}"))) + .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:4}"))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] @@ -479,43 +433,6 @@ LOG gen.auto.derive.infra:0: } } ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.BS" .$ var "n") - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkBS (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkBS" .! ("n", var "n"))) - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.BS[0] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") - } - ] ] , scope = var "[]" .$ var "^outmost-fuel^" } diff --git a/tests/derivation/least-effort/print/order/003 complex order/expected b/tests/derivation/least-effort/print/order/003 complex order/expected index 16af5eda2..1a9b75c6a 100644 --- a/tests/derivation/least-effort/print/order/003 complex order/expected +++ b/tests/derivation/least-effort/print/order/003 complex order/expected @@ -23,16 +23,14 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0]" + { name = "[0, 1]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -40,25 +38,18 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -96,27 +87,26 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkZ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1]" - .$ var "^outmost-fuel^" - .$ var "n" - .$ (var "Data.Fin.finS" .! ("n", var "n") .$ var "i")) - .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse - .=> var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "y" - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "i" .$ var "x" .$ var "y") - ] - })))) + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "n" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "i" .$ bindVar "y") + .= var ">>=" + .$ ( var "[0, 1]" + .$ var "^outmost-fuel^" + .$ var "n" + .$ (var "Data.Fin.finS" .! ("n", var "n") .$ var "i")) + .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "i" .$ var "x" .$ var "y")) + ] + })) ] ] , scope = @@ -125,88 +115,10 @@ LOG gen.auto.derive.infra:0: .$ (var "<>" .$ var "^fuel_arg^") } ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ (var "Data.Fin.Fin" .$ var "n") - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") - .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) - .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y0" .! ("i", var "i"))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - , IDef - emptyFC - "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2")) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0] (non-recursive)")) - .$ ( var "Test.DepTyCheck.Gen.oneOf" - .! ("em", var "MaybeEmpty") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") - .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") .$ var "Nil"))) - } - ] , IDef emptyFC "[0, 1]" - [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:2}>" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" .= local { decls = [ IClaim @@ -219,10 +131,10 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IClaim emptyFC @@ -234,10 +146,10 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:2}") + .$ (var "DerivedGen.X" .$ var "n" .$ var "{arg:1}") }) , IDef emptyFC @@ -273,16 +185,16 @@ LOG gen.auto.derive.infra:0: .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>") + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:2}>") + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") .$ var "Nil"))) } ] , IDef emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -291,10 +203,18 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -302,55 +222,55 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:2}"))) }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) + .$ ( var ">>=" + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y0" .! ("i", var "i")))))) ] , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:3}"))) + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2"))) ] ] , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) - .$ var "Nil"))) - ] - } + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[] (non-recursive)")) + .$ ( var "Test.DepTyCheck.Gen.oneOf" + .! ("em", var "MaybeEmpty") + .$ ( var "::" + .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] , IDef @@ -406,10 +326,10 @@ LOG gen.auto.derive.infra:0: .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) .$ ( var ">>=" .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:4}"))) + .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:3}"))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/order/004 complex order/expected b/tests/derivation/least-effort/print/order/004 complex order/expected index bfc84c4e0..c1236bd5d 100644 --- a/tests/derivation/least-effort/print/order/004 complex order/expected +++ b/tests/derivation/least-effort/print/order/004 complex order/expected @@ -23,14 +23,18 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}"))) }) , IClaim emptyFC @@ -44,17 +48,6 @@ LOG gen.auto.derive.infra:0: .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" - }) , IDef emptyFC "[]" @@ -79,21 +72,20 @@ LOG gen.auto.derive.infra:0: .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkZ (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var ">>=" - .$ ( var "[0]" - .$ var "^outmost-fuel^" - .$ ( var "Prelude.Types.plus" - .$ var "n" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) - .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse - .=> var ">>=" - .$ (var "[0, 1]" .$ var "^outmost-fuel^" .$ var "n" .$ var "x") - .$ ( MkArg MW ExplicitArg (Just "y") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "x" .$ var "y"))))) + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "n" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "x" .$ bindVar "y") + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "x" .$ var "y") + ] + })) ] ] , scope = @@ -104,8 +96,8 @@ LOG gen.auto.derive.infra:0: ] , IDef emptyFC - "[0, 1]" - [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -117,11 +109,19 @@ LOG gen.auto.derive.infra:0: { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .$ ( MkArg + MW + ExplicitArg + (Just "{arg:1}") + (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}"))) }) , IClaim emptyFC @@ -132,50 +132,58 @@ LOG gen.auto.derive.infra:0: { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .$ ( MkArg + MW + ExplicitArg + (Just "{arg:1}") + (var "Data.Fin.Fin" .$ (var "DerivedGen.f" .$ var "n")) + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}"))) }) , IDef emptyFC "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ var "Prelude.Types.Z" .$ bindVar "i" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.Y0" .! ("i", var "i"))) - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var ">>=" + .$ ( var "[0]" + .$ var "^outmost-fuel^" + .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y0" .! ("i", var "i")))))) ] , IDef emptyFC "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( var "Data.Fin.FS" - .! ("k", var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) - .$ ( var "Data.Fin.FS" - .! ("k", var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ (var "Data.Fin.FZ" .! ("k", var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "DerivedGen.Y2") - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2"))) ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0, 1] (non-recursive)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[] (non-recursive)")) .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") - .$ var "Nil"))) + .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] , IDef @@ -264,80 +272,6 @@ LOG gen.auto.derive.infra:0: } } ] - , IDef - emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") - ] - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:3}"))) - ] - ] - , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) - .$ var "Nil"))) - ] - } - } - ] ] , scope = var "[]" .$ var "^outmost-fuel^" } diff --git a/tests/derivation/least-effort/print/order/005 complex order/expected b/tests/derivation/least-effort/print/order/005 complex order/expected index 04124d411..5f7492677 100644 --- a/tests/derivation/least-effort/print/order/005 complex order/expected +++ b/tests/derivation/least-effort/print/order/005 complex order/expected @@ -23,14 +23,16 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0, 1]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) }) , IClaim emptyFC @@ -38,11 +40,10 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[0]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" }) , IClaim emptyFC @@ -50,10 +51,11 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "[]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") }) , IDef emptyFC @@ -82,23 +84,22 @@ LOG gen.auto.derive.infra:0: .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var ">>=" - .$ ( var "[0]" + .$ ( var "[0]" .$ var "^outmost-fuel^" .$ ( var "Prelude.Types.plus" .$ var "n" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) - .$ ( MkArg MW ExplicitArg (Just "x") implicitFalse - .=> var ">>=" - .$ ( var "[0, 1]" - .$ var "^outmost-fuel^" - .$ ( var "Prelude.Types.plus" - .$ var "n" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))) - .$ var "x") - .$ ( MkArg MW ExplicitArg (Just "y") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "x" .$ var "y"))))) + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "x" .$ bindVar "y" + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkZ" .$ var "n" .$ var "x" .$ var "y") + ] + }))) ] ] , scope = @@ -109,8 +110,8 @@ LOG gen.auto.derive.infra:0: ] , IDef emptyFC - "[0, 1]" - [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .= local { decls = [ IClaim @@ -123,10 +124,12 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) }) , IClaim emptyFC @@ -138,21 +141,26 @@ LOG gen.auto.derive.infra:0: , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}") + .$ ( var "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.Y" .$ var "n" .$ var "{arg:1}")) }) , IDef emptyFC "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") .$ bindVar "i" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.Y1 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.Y1" .! ("i", var "i"))) - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var ">>=" + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.Y1" .! ("i", var "i"))))) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef emptyFC @@ -160,31 +168,28 @@ LOG gen.auto.derive.infra:0: [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( var "Data.Fin.FS" - .! ("k", var "Prelude.Types.S" .$ var "Prelude.Types.Z") - .$ (var "Data.Fin.FZ" .! ("k", var "Prelude.Types.Z"))) .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.Y2 (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "DerivedGen.Y2") - , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.Y2")) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0, 1] (non-recursive)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0] (non-recursive)")) .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") - .$ var "Nil"))) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") .$ var "Nil"))) } ] , IDef emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -193,13 +198,10 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "Data.Fin.Fin" .$ var "n") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" }) , IClaim emptyFC @@ -207,38 +209,31 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "Data.Fin.Fin" .$ var "n") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.FZ (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FZ" .! ("k", var "k"))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) + .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") ] , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) + .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) .$ ( var ">>=" - .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") + .$ (var "[]" .$ var "^cons_fuel^") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:2}"))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:2}"))) ] ] , scope = @@ -248,20 +243,18 @@ LOG gen.auto.derive.infra:0: , clauses = [ var "Data.Fuel.Dry" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^") + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry") , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (spend fuel)")) + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) .$ ( var "Test.DepTyCheck.Gen.frequency" .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ var "Data.Nat1.one" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^")) + .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) .$ ( var "::" .$ ( var "Builtin.MkPair" .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^")) + .$ (var "<>" .$ var "^sub^fuel_arg^")) .$ var "Nil"))) ] } @@ -269,8 +262,8 @@ LOG gen.auto.derive.infra:0: ] , IDef emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .= local { decls = [ IClaim @@ -279,10 +272,13 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ (var "Data.Fin.Fin" .$ var "n") }) , IClaim emptyFC @@ -290,31 +286,38 @@ LOG gen.auto.derive.infra:0: Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ (var "Data.Fin.Fin" .$ var "n") }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") + .$ (var "fromString" .$ primVal (Str "Data.Fin.FZ (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Data.Fin.FZ" .! ("k", var "k"))) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "k") .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) + .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") + .$ (var "[0]" .$ var "^cons_fuel^" .$ var "k") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:3}"))) + .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:3}"))) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] , scope = @@ -324,18 +327,20 @@ LOG gen.auto.derive.infra:0: , clauses = [ var "Data.Fuel.Dry" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") + .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^") , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) + .$ (var "fromString" .$ primVal (Str "Data.Fin.Fin[0] (spend fuel)")) .$ ( var "Test.DepTyCheck.Gen.frequency" .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) + .$ ( var "Builtin.MkPair" + .$ var "Data.Nat1.one" + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^")) .$ ( var "::" .$ ( var "Builtin.MkPair" .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) + .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^")) .$ var "Nil"))) ] } diff --git a/tests/derivation/least-effort/run/adt/004 noparam/expected b/tests/derivation/least-effort/run/adt/004 noparam/expected index 94044733a..d995870d9 100644 --- a/tests/derivation/least-effort/run/adt/004 noparam/expected +++ b/tests/derivation/least-effort/run/adt/004 noparam/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 4) 17) 10) 10) 17) 5) 4) 12) 11) 8) 15) 4) 14) 7) 4) 10 +R (R (R (R (R (R (R (R (R (R E 4) 10) 11) 12) 17) 8) 10) 17) 4) 16 ----- -R E 15 +R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 16) 14) 9) 12) 19) 5) 20) 14) 20) 17) 17) 15) 0) 6) 1) 7) 14) 4) 14 ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 0) 17) 13) 17) 17) 12) 2) 18) 13) 10) 14) 16) 16) 11) 1) 3) 3) 10) 12) 17 +R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 1) 15) 12) 6) 16) 3) 7) 19) 17) 12) 6) 2) 2) 0) 8) 16 ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 7) 3) 16) 6) 12) 18) 2) 8) 1) 18) 15) 1) 7) 0) 5) 15) 19) 3) 19 +R (R (R (R E 15) 17) 0) 5 ----- -R (R (R (R (R (R (R (R (R E 6) 4) 0) 3) 13) 19) 5) 20) 3 +R E 6 ----- -R E 13 +R (R (R (R (R (R (R E 3) 14) 18) 1) 20) 1) 19 ----- -R (R (R (R (R (R (R (R (R E 5) 0) 7) 4) 7) 6) 16) 3) 6 +R (R (R (R (R (R (R (R (R E 4) 8) 13) 1) 3) 20) 15) 13) 2 ----- -R (R (R (R E 5) 10) 11) 2 +R (R (R (R (R (R (R (R (R E 5) 2) 4) 2) 16) 5) 6) 3) 7 ----- -R (R (R (R (R (R (R (R (R (R (R E 12) 13) 19) 15) 5) 7) 10) 18) 2) 14) 9 +R (R (R (R (R (R (R (R E 15) 19) 13) 11) 10) 1) 10) 4 ----- -R (R (R (R (R (R (R E 20) 13) 3) 10) 17) 7) 6 +R (R (R (R (R (R (R (R (R (R (R (R (R (R E 19) 6) 13) 17) 2) 13) 20) 6) 8) 13) 1) 17) 8) 12 diff --git a/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected b/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected index c2745099d..00bda4bbf 100644 --- a/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkY (MkX {n=16} {m=4}) ------ -MkY (MkX {n=17} {m=10}) +MkY (MkX {n=4} {m=16}) ----- MkY (MkX {n=10} {m=17}) ----- -MkY (MkX {n=5} {m=4}) +MkY (MkX {n=17} {m=10}) +----- +MkY (MkX {n=4} {m=5}) ----- -MkY (MkX {n=12} {m=11}) +MkY (MkX {n=11} {m=12}) ----- -MkY (MkX {n=8} {m=15}) +MkY (MkX {n=15} {m=8}) ----- -MkY (MkX {n=4} {m=14}) +MkY (MkX {n=14} {m=4}) ----- -MkY (MkX {n=7} {m=4}) +MkY (MkX {n=4} {m=7}) ----- -MkY (MkX {n=10} {m=1}) +MkY (MkX {n=1} {m=10}) ----- -MkY (MkX {n=15} {m=20}) +MkY (MkX {n=20} {m=15}) diff --git a/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected b/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected index a13c85e9c..ac9849693 100644 --- a/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected +++ b/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkY (MkX {n=16} {m=17}) (MkX {n=16} {m=4}) +MkY (MkX {n=4} {m=17}) (MkX {n=4} {m=16}) ----- MkY (MkX {n=10} {m=17}) (MkX {n=10} {m=10}) ----- -MkY (MkX {n=5} {m=12}) (MkX {n=5} {m=4}) +MkY (MkX {n=4} {m=12}) (MkX {n=4} {m=5}) ----- -MkY (MkX {n=11} {m=15}) (MkX {n=11} {m=8}) +MkY (MkX {n=8} {m=15}) (MkX {n=8} {m=11}) ----- -MkY (MkX {n=4} {m=7}) (MkX {n=4} {m=14}) +MkY (MkX {n=14} {m=7}) (MkX {n=14} {m=4}) ----- -MkY (MkX {n=4} {m=1}) (MkX {n=4} {m=10}) +MkY (MkX {n=10} {m=1}) (MkX {n=10} {m=4}) ----- -MkY (MkX {n=15} {m=0}) (MkX {n=15} {m=20}) +MkY (MkX {n=20} {m=0}) (MkX {n=20} {m=15}) ----- -MkY (MkX {n=17} {m=17}) (MkX {n=17} {m=13}) +MkY (MkX {n=13} {m=17}) (MkX {n=13} {m=17}) ----- -MkY (MkX {n=17} {m=2}) (MkX {n=17} {m=12}) +MkY (MkX {n=12} {m=2}) (MkX {n=12} {m=17}) ----- -MkY (MkX {n=18} {m=10}) (MkX {n=18} {m=13}) +MkY (MkX {n=13} {m=10}) (MkX {n=13} {m=18}) diff --git a/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected b/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected index c9c0f80c0..0a472f403 100644 --- a/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected +++ b/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected @@ -3,7 +3,7 @@ Generated values: ----- ----- -MkY (MkX "a" 0) (MkX "a" 0) +MkY (MkX "" 0) (MkX "" 10) ----- MkY (MkX "" 10) (MkX "" 0) ----- @@ -11,14 +11,14 @@ MkY (MkX "a" 10) (MkX "a" 10) ----- MkY (MkX "" 10) (MkX "" 10) ----- -MkY (MkX "bc" 10) (MkX "bc" 0) +MkY (MkX "bc" 0) (MkX "bc" 10) ----- -MkY (MkX "" 10) (MkX "" 0) +MkY (MkX "" 0) (MkX "" 10) ----- MkY (MkX "a" 10) (MkX "a" 10) ----- -MkY (MkX "a" 0) (MkX "a" 0) +MkY (MkX "a" 0) (MkX "a" 10) ----- -MkY (MkX "" 10) (MkX "" 10) +MkY (MkX "" 10) (MkX "" 0) ----- -MkY (MkX "a" 0) (MkX "a" 0) +MkY (MkX "a" 0) (MkX "a" 10) diff --git a/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected b/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected index 46545db4e..8ca257b11 100644 --- a/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected +++ b/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected @@ -5,19 +5,19 @@ Generated values: ----- MkY_RL (MkX 4 16) (MkXG_4) ----- -MkY_LR (MkXG_5) (MkX 5 19) +MkY_LR (MkXG_5) (MkX 5 4) ----- -MkY_LR (MkXG_5) (MkX 5 2) +MkY_LR (MkXG_5) (MkX 5 8) ----- MkY_RL (MkX 4 11) (MkXG_4) ----- MkY_RL (MkX 4 11) (MkXG_4) ----- -MkY_LR (MkXG_5) (MkX 5 10) +MkY_LR (MkXG_4) (MkX 4 10) ----- -MkY_LR (MkXG_5) (MkX 5 14) +MkY_RL (MkX 5 4) (MkXG_5) ----- -MkY_RL (MkX 4 2) (MkXG_4) +MkY_LR (MkXG_5) (MkX 5 14) ----- MkY_RL (MkX 4 6) (MkXG_4) ----- diff --git a/tests/derivation/least-effort/run/gadt/005 gadt/expected b/tests/derivation/least-effort/run/gadt/005 gadt/expected index edf2e8216..3e012d742 100644 --- a/tests/derivation/least-effort/run/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/run/gadt/005 gadt/expected @@ -13,12 +13,12 @@ Generated values: ----- (True ** TR "a" (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (JJ 0 10))))))) ----- -(True ** TR "bc" (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 10)))))))))) +(True ** TR "bc" (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 0)))))))))) ----- (False ** FN 0 (FN 10 (FN 0 (TR "a" (FN 10 (FN 0 (FN 10 (FN 0 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (FN 0 (FN 10 (FN 0 (FN 10 (JJ 10 0)))))))))))))))))) ----- (True ** TR "a" (TR "bc" (FN 0 (FN 10 (TR "" (FN 0 (FN 10 (TR "" (TR "bc" (FN 10 (JJ 10 10))))))))))) ----- -(True ** TR "a" (FN 10 (TR "" (TR "bc" (TR "a" (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (TR "" (FN 10 (FN 0 (JJ 10 0)))))))))))))) +(True ** TR "a" (FN 10 (TR "" (TR "bc" (TR "a" (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (TR "" (FN 10 (FN 0 (JJ 10 10)))))))))))))) ----- -(True ** TR "bc" (TR "a" (FN 0 (TR "" (JJ 0 10))))) +(True ** TR "bc" (TR "a" (FN 0 (TR "" (JJ 0 0))))) diff --git a/tests/derivation/least-effort/run/gadt/006 gadt/expected b/tests/derivation/least-effort/run/gadt/006 gadt/expected index 915727902..4badde148 100644 --- a/tests/derivation/least-effort/run/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/run/gadt/006 gadt/expected @@ -17,7 +17,7 @@ TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (TR "a" (TR "a" (TR "" (FN 10 (TR "a" (TL "a"))) ----- TR "bc" (TR "bc" (FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (FN 10 (TR "a" (FN 10 (JJ 0 10)))))))))) ----- -TR "bc" (FN 10 (TR "" (FN 0 (JJ 10 10)))) +TR "bc" (FN 10 (TR "" (FN 0 (JJ 10 0)))) ----- TR "bc" (FN 0 (FN 0 (FN 0 (TR "a" (TL ""))))) ----- @@ -34,12 +34,12 @@ FN 0 (FN 0 (TR "a" (FN 10 (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (FN 0 (TR "a" (TR "a ----- FN 10 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (JJ 0 10)))))) ----- -FN 0 (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 10))))))))) +FN 0 (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 0))))))))) ----- FN 0 (FN 10 (FN 0 (TR "a" (FN 10 (FN 0 (FN 10 (FN 0 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (FN 0 (FN 10 (FN 0 (FN 10 (JJ 10 0))))))))))))))))) ----- FN 10 (TR "bc" (FN 0 (FN 10 (TR "" (FN 0 (FN 10 (TR "" (TR "bc" (FN 10 (JJ 10 10)))))))))) ----- -JJ 10 0 +JJ 0 10 ----- -FN 0 (FN 10 (FN 10 (FN 0 (JJ 10 10)))) +FN 0 (FN 10 (FN 10 (FN 0 (JJ 10 0)))) diff --git a/tests/derivation/least-effort/run/order/001 complex order/expected b/tests/derivation/least-effort/run/order/001 complex order/expected new file mode 100644 index 000000000..b3e964294 --- /dev/null +++ b/tests/derivation/least-effort/run/order/001 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 diff --git a/tests/derivation/least-effort/run/order/002 complex order/expected b/tests/derivation/least-effort/run/order/002 complex order/expected new file mode 100644 index 000000000..dfc25930c --- /dev/null +++ b/tests/derivation/least-effort/run/order/002 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 1 0 MkBS X0 Y0 +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 1 0 MkBS X0 Y0 +----- +MkZ 1 0 MkBS X0 Y0 +----- +MkZ 3 2 MkBS X2 Y2 +----- +MkZ 3 2 MkBS X2 Y2 diff --git a/tests/derivation/least-effort/run/order/003 complex order/expected b/tests/derivation/least-effort/run/order/003 complex order/expected new file mode 100644 index 000000000..b3e964294 --- /dev/null +++ b/tests/derivation/least-effort/run/order/003 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 +----- +MkZ 1 0 X0 Y0 diff --git a/tests/derivation/least-effort/run/order/004 complex order/expected b/tests/derivation/least-effort/run/order/004 complex order/expected new file mode 100644 index 000000000..0c958fc04 --- /dev/null +++ b/tests/derivation/least-effort/run/order/004 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 2 2 Y2 +----- +MkZ 0 1 Y0 +----- +MkZ 0 1 Y0 +----- +MkZ 2 2 Y2 +----- +MkZ 2 2 Y2 +----- +MkZ 2 2 Y2 +----- +MkZ 0 1 Y0 +----- +MkZ 0 1 Y0 +----- +MkZ 0 1 Y0 +----- +MkZ 2 2 Y2 diff --git a/tests/derivation/least-effort/run/order/005 complex order/expected b/tests/derivation/least-effort/run/order/005 complex order/expected new file mode 100644 index 000000000..4953ad378 --- /dev/null +++ b/tests/derivation/least-effort/run/order/005 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 +----- +MkZ 0 1 Y2 diff --git a/tests/derivation/least-effort/run/order/006 complex order/expected b/tests/derivation/least-effort/run/order/006 complex order/expected new file mode 100644 index 000000000..7cff7e440 --- /dev/null +++ b/tests/derivation/least-effort/run/order/006 complex order/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2 +----- +MkZ 2 1 Y2