From d30cade5a39c7bc2b1ccb62515b693e57b365c7e Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Fri, 13 Sep 2024 16:04:53 +0300 Subject: [PATCH] [ derive ] Do not pass values of arguments on which someone else depends --- .../covering-seq/tests/gens/print/expected | 36 ++- .../sorted-list/tests/gens/print/expected | 18 +- .../DepTyCheck/Gen/Core/ConsDerive.idr | 22 +- .../adt/007 right-to-left simple/expected | 2 +- .../adt/008 right-to-left simple/expected | 2 +- .../print/adt/009 left-to-right/expected | 2 +- .../adt/010 right-to-left long-dpair/expected | 5 +- .../adt/011 right-to-left long-dpair/expected | 5 +- .../adt/012 right-to-left chained/expected | 4 +- .../adt/013 right-to-left nondet/expected | 6 +- .../adt/014 right-to-left nondet ext/expected | 6 +- .../least-effort/print/gadt/001 gadt/expected | 2 +- .../least-effort/print/gadt/002 gadt/expected | 2 +- .../gadt/003 right-to-left nondet/expected | 12 +- .../print/gadt/004 right-to-left det/expected | 12 +- .../least-effort/print/gadt/005 gadt/expected | 4 +- .../least-effort/print/gadt/006 gadt/expected | 8 +- .../print/gadt/011 eq deepcons/expected | 4 +- .../print/gadt/012 eq deepcons/expected | 5 +- .../print/gadt/013 eq deepcons/expected | 5 +- .../print/gadt/014 eq deepcons/expected | 2 +- .../regression/dependent-givens-big/expected | 13 +- .../dependent-givens-small-deep/expected | 2 +- .../dependent-givens-small-shallow/expected | 2 +- .../print/regression/fin-inc/expected | 6 +- .../DerivedGen.idr | 16 + .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../expected | 171 +++++++++++ .../underscore-in-cons-expl-full-gend1/run | 1 + .../DerivedGen.idr | 16 + .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../expected | 280 ++++++++++++++++++ .../underscore-in-cons-expl-full-gend2/run | 1 + .../DerivedGen.idr | 16 + .../RunDerivedGen.idr | 1 + .../underscore-in-cons-expl-full/derive.ipkg | 1 + .../underscore-in-cons-expl-full/expected | 68 +++++ .../underscore-in-cons-expl-full/run | 1 + .../DerivedGen.idr | 16 + .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../underscore-in-cons-expl-partial/expected | 68 +++++ .../underscore-in-cons-expl-partial/run | 1 + .../unification-mismatch-dependent/expected | 2 +- .../unification-name-mismatch/expected | 4 +- .../regression/unnamed-auto-implicit/expected | 6 +- .../DerivedGen.idr | 23 ++ .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../expected | 20 ++ .../underscore-in-cons-expl-full-gend1/run | 1 + .../DerivedGen.idr | 22 ++ .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../expected | 24 ++ .../underscore-in-cons-expl-full-gend2/run | 1 + .../DerivedGen.idr | 23 ++ .../RunDerivedGen.idr | 1 + .../underscore-in-cons-expl-full/derive.ipkg | 1 + .../underscore-in-cons-expl-full/expected | 25 ++ .../underscore-in-cons-expl-full/run | 1 + .../DerivedGen.idr | 23 ++ .../RunDerivedGen.idr | 1 + .../derive.ipkg | 1 + .../underscore-in-cons-expl-partial/expected | 25 ++ .../underscore-in-cons-expl-partial/run | 1 + 68 files changed, 971 insertions(+), 88 deletions(-) create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/derive.ipkg create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/expected create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/run create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/derive.ipkg create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/expected create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/run create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/DerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/derive.ipkg create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/expected create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/run create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/DerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/derive.ipkg create mode 100644 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/expected create mode 120000 tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/run create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/derive.ipkg create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/run create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/derive.ipkg create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/expected create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/run create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/DerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/derive.ipkg create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/expected create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/run create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/DerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/derive.ipkg create mode 100644 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/expected create mode 120000 tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/run diff --git a/examples/covering-seq/tests/gens/print/expected b/examples/covering-seq/tests/gens/print/expected index 5c91b882b..67d9dba1c 100644 --- a/examples/covering-seq/tests/gens/print/expected +++ b/examples/covering-seq/tests/gens/print/expected @@ -142,7 +142,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ ( MkArg MW ExplicitArg (Just "^bnd^{conArg:1}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.List.Covering.End" .! ("n", var "n") .! ("bs", var "bs") .@ var "^bnd^{conArg:1}"))) + .$ ( var "Data.List.Covering.End" + .! ("n", implicitTrue) + .! ("bs", implicitTrue) + .@ var "^bnd^{conArg:1}"))) ] , IDef emptyFC @@ -159,8 +162,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Data.List.Covering.Miss" - .! ("n", var "n") - .! ("bs", var "bs") + .! ("n", implicitTrue) + .! ("bs", implicitTrue) .$ var "^bnd^{arg:7}" .$ var "^bnd^{arg:8}")))) ] @@ -194,9 +197,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Data.List.Covering.Hit" - .! ("n", var "n") - .! ("bs", var "bs") - .$ var "i" + .! ("n", implicitTrue) + .! ("bs", implicitTrue) + .$ implicitTrue .@ var "^bnd^{conArg:2}" .$ var "^bnd^{arg:9}"))))) ] @@ -320,7 +323,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ (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 "Data.List.Covering.BitMask.Index.Here" + .! ("n", implicitTrue) + .! ("bs", var "bs") + .! ("b", var "b"))) , var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") @@ -362,10 +368,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .! ("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") + .! ("v", implicitTrue) + .! ("n", implicitTrue) + .! ("bs", implicitTrue) + .! ("i", implicitTrue) .$ var "^bnd^{arg:10}"))) , var "<>" .$ implicitTrue @@ -473,7 +479,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ ( 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 "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:11}"))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] @@ -668,9 +674,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .=> 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") + .! ("n", implicitTrue) + .! ("bs", implicitTrue) + .! ("b", implicitTrue) .$ var "^bnd^{arg:13}"))) , var "<>" .$ bindVar "^cons_fuel^" diff --git a/examples/sorted-list/tests/gens/print/expected b/examples/sorted-list/tests/gens/print/expected index 898ce62cf..b70dd9866 100644 --- a/examples/sorted-list/tests/gens/print/expected +++ b/examples/sorted-list/tests/gens/print/expected @@ -135,7 +135,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList .$ (var "Builtin.DPair.MkDPair" .$ bindVar "xs" .$ bindVar "^bnd^{conArg:1}") .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.List.Sorted.(::)" .$ var "x" .$ var "xs" .@ var "^bnd^{conArg:1}") + .$ (var "Data.List.Sorted.(::)" .$ implicitTrue .$ implicitTrue .@ var "^bnd^{conArg:1}") ] })) ] @@ -255,10 +255,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "Data.List.Sorted.NE" - .! ("xs", var "xs") - .! ("x", var "x") + .! ("xs", implicitTrue) + .! ("x", implicitTrue) .! ("prf", var "prf") - .! ("n", var "n") + .! ("n", implicitTrue) .$ var "^bnd^{arg:3}"))) ] }) @@ -367,10 +367,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "Data.List.Sorted.NE" - .! ("xs", var "xs") - .! ("x", var "x") + .! ("xs", implicitTrue) + .! ("x", implicitTrue) .! ("prf", var "prf") - .! ("n", var "n") + .! ("n", implicitTrue) .$ var "^bnd^{arg:3}")) ] }) @@ -477,8 +477,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "Data.Nat.LTESucc" - .! ("right", var "right") - .! ("left", var "left") + .! ("right", implicitTrue) + .! ("left", implicitTrue) .$ var "^bnd^{arg:4}")) ] })) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index d9cbac54a..9fcc2c120 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -84,12 +84,17 @@ namespace NonObligatoryExts -- Compute left-to-right need of generation when there are non-trivial types at the left argsTypeApps <- for con.args.asVect $ analyseTypeApp . type + -- Get dependencies of constructor's arguments + let rawDeps' = argDeps con.args + let rawDeps : Vect _ $ SortedSet $ Fin con.args.length := downmap (mapIn weakenToSuper) rawDeps' + let dependees = concat rawDeps -- arguments which any other argument depends on + -- Decide how constructor arguments would be named during generation - let bindNames = fromList con.args <&> bindNameRenamer . argName + let bindNames = withIndex (fromList con.args) <&> map (bindNameRenamer . argName) -- Form the expression of calling the current constructor let callCons = do - let constructorCall = callCon con $ bindNames <&> varStr + let constructorCall = callCon con $ bindNames <&> \(idx, n) => if contains idx dependees then implicitTrue else varStr n let wrapImpls : Nat -> TTImp wrapImpls Z = constructorCall wrapImpls (S n) = var `{Builtin.DPair.MkDPair} .$ implicitTrue .$ wrapImpls n @@ -140,7 +145,7 @@ namespace NonObligatoryExts subgenCall <- callGen subsig subfuel $ snd <$> subgivens -- Form an expression of binding the result of subgen - let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames + let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . snd . flip Vect.index bindNames let bindSubgenResult = foldr (\l, r => var `{Builtin.DPair.MkDPair} .$ l .$ r) genedArg subgeneratedArgs -- Form an expression of the RHS of a bind; simplify lambda if subgeneration result type does not require pattern matching @@ -151,10 +156,6 @@ namespace NonObligatoryExts -- Chain the subgen call with a given continuation pure $ \cont => `(~subgenCall >>= ~(bindRHS cont)) - -- Get dependencies of constructor's arguments - let rawDeps = argDeps con.args - let deps = downmap ((`difference` givs) . mapIn weakenToSuper) rawDeps - ------------------------------------------------- -- Left-to-right generation phase (2nd phase) --- ------------------------------------------------- @@ -171,23 +172,24 @@ namespace NonObligatoryExts let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR -- Find rightmost arguments among `preLTR` + let depsNoGivs = (`difference` givs) <$> rawDeps let depsLTR = SortedSet.fromList $ mapMaybe (\(ds, idx) => whenT .| contains idx preLTR && null ds .| idx) $ - toListI $ deps <&> intersection preLTR + toListI $ depsNoGivs <&> intersection preLTR --------------------------------------------------------------------------------- -- Main right-to-left generation phase (3rd phase aka 2nd right-to-left phase) -- --------------------------------------------------------------------------------- -- Arguments that no other argument depends on - let rightmostArgs = fromFoldable {f=Vect _} range `difference` (givs `union` concat deps) + let rightmostArgs = fromFoldable {f=Vect _} range `difference` (givs `union` dependees) --------------------------------------------------------------- -- 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 + let disjDeps = disjointDepSets rawDeps' givs -- Acquire order(s) in what we will generate arguments let allOrders = do diff --git a/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected b/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected index c64626f3e..710108193 100644 --- a/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected +++ b/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected @@ -73,7 +73,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y [ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:2}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}") + .$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}") ] })) ] diff --git a/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected b/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected index c64626f3e..710108193 100644 --- a/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected +++ b/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected @@ -73,7 +73,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y [ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:2}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}") + .$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}") ] })) ] diff --git a/tests/derivation/least-effort/print/adt/009 left-to-right/expected b/tests/derivation/least-effort/print/adt/009 left-to-right/expected index 3bf59fae0..e6e909f5b 100644 --- a/tests/derivation/least-effort/print/adt/009 left-to-right/expected +++ b/tests/derivation/least-effort/print/adt/009 left-to-right/expected @@ -72,7 +72,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:2}")))) + .$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:2}")))) ] ] , 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 28b3d7ab2..6694c4b8e 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 @@ -79,7 +79,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}") .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("m", var "m") .! ("n", var "n") .$ var "^bnd^{arg:3}") + .$ ( var "DerivedGen.MkY" + .! ("m", implicitTrue) + .! ("n", implicitTrue) + .$ var "^bnd^{arg:3}") ] })) ] 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 4d56d2a43..dbcf6c57f 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 @@ -90,7 +90,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}") .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("m", var "m") .! ("n", var "n") .$ var "^bnd^{arg:3}") + .$ ( var "DerivedGen.MkY" + .! ("m", implicitTrue) + .! ("n", implicitTrue) + .$ var "^bnd^{arg:3}") ] })) ] diff --git a/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected b/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected index b1111e603..9bddb0eec 100644 --- a/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected +++ b/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected @@ -88,7 +88,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y [ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:3}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkY" .! ("n", var "n") .$ var "^bnd^{arg:3}") + .$ (var "DerivedGen.MkY" .! ("n", implicitTrue) .$ var "^bnd^{arg:3}") ] })) ] @@ -139,7 +139,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "DerivedGen.MkX2" .$ var "n" .$ var "^bnd^{arg:4}")) + .$ (var "DerivedGen.MkX2" .$ implicitTrue .$ var "^bnd^{arg:4}")) ] })) ] 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 1c7187032..8f66095cb 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 @@ -105,9 +105,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:4}" .$ var "^bnd^{arg:3}") ] 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 1665558d9..8ea46f840 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 @@ -106,9 +106,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:6}" .$ var "^bnd^{arg:5}") ] diff --git a/tests/derivation/least-effort/print/gadt/001 gadt/expected b/tests/derivation/least-effort/print/gadt/001 gadt/expected index 130d020b3..93235eb8a 100644 --- a/tests/derivation/least-effort/print/gadt/001 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/001 gadt/expected @@ -72,7 +72,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> Gen MaybeEmpty .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:1}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:1}"))) + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:1}"))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/gadt/002 gadt/expected b/tests/derivation/least-effort/print/gadt/002 gadt/expected index 0bfb458f5..f34612b26 100644 --- a/tests/derivation/least-effort/print/gadt/002 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/002 gadt/expected @@ -96,7 +96,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "Data.Fin.FS" .! ("k", var "k") .$ var "^bnd^{arg:1}")) + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:1}")) ] })) ] diff --git a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected index 66e220888..71ee4768c 100644 --- a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected @@ -133,9 +133,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY1" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:4}" .$ var "^bnd^{arg:3}") ] @@ -170,9 +170,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY2" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:6}" .$ var "^bnd^{arg:5}") ] 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 90eac771c..f87e1f13e 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 @@ -152,9 +152,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY_LR" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:6}" .$ var "^bnd^{arg:5}") ] @@ -189,9 +189,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY_RL" - .! ("k", var "k") - .! ("m", var "m") - .! ("n", var "n") + .! ("k", implicitTrue) + .! ("m", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:8}" .$ var "^bnd^{arg:7}") ] diff --git a/tests/derivation/least-effort/print/gadt/005 gadt/expected b/tests/derivation/least-effort/print/gadt/005 gadt/expected index c36018d30..c3afb08ef 100644 --- a/tests/derivation/least-effort/print/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/005 gadt/expected @@ -157,7 +157,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.FN" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:7}" .$ var "^bnd^{arg:6}"))) ] @@ -198,7 +198,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.TR" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:10}" .$ var "^bnd^{arg:9}"))) ] diff --git a/tests/derivation/least-effort/print/gadt/006 gadt/expected b/tests/derivation/least-effort/print/gadt/006 gadt/expected index 69dbcaa47..90554da87 100644 --- a/tests/derivation/least-effort/print/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/006 gadt/expected @@ -152,7 +152,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.FN" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:7}" .$ var "^bnd^{arg:6}")) ] @@ -193,7 +193,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.TR" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:10}" .$ var "^bnd^{arg:9}")) ] @@ -355,7 +355,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.FN" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:7}" .$ var "^bnd^{arg:6}"))) ] @@ -396,7 +396,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.TR" - .! ("b", var "b") + .! ("b", implicitTrue) .$ var "^bnd^{arg:10}" .$ var "^bnd^{arg:9}"))) ] diff --git a/tests/derivation/least-effort/print/gadt/011 eq deepcons/expected b/tests/derivation/least-effort/print/gadt/011 eq deepcons/expected index 192fc7b89..d9860ad11 100644 --- a/tests/derivation/least-effort/print/gadt/011 eq deepcons/expected +++ b/tests/derivation/least-effort/print/gadt/011 eq deepcons/expected @@ -110,8 +110,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.Step" - .! ("y", var "y") - .! ("x", var "x") + .! ("y", implicitTrue) + .! ("x", implicitTrue) .$ var "^bnd^{arg:4}"))) ] })) diff --git a/tests/derivation/least-effort/print/gadt/012 eq deepcons/expected b/tests/derivation/least-effort/print/gadt/012 eq deepcons/expected index d18fbf2e2..ad9cd22e6 100644 --- a/tests/derivation/least-effort/print/gadt/012 eq deepcons/expected +++ b/tests/derivation/least-effort/print/gadt/012 eq deepcons/expected @@ -89,7 +89,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Nat) -> Gen MaybeEmpty .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "DerivedGen.Step" .! ("y", var "y") .! ("x", var "x") .$ var "^bnd^{arg:3}")) + .$ ( var "DerivedGen.Step" + .! ("y", implicitTrue) + .! ("x", implicitTrue) + .$ var "^bnd^{arg:3}")) ] })) ] diff --git a/tests/derivation/least-effort/print/gadt/013 eq deepcons/expected b/tests/derivation/least-effort/print/gadt/013 eq deepcons/expected index 3f1bec753..2e868552d 100644 --- a/tests/derivation/least-effort/print/gadt/013 eq deepcons/expected +++ b/tests/derivation/least-effort/print/gadt/013 eq deepcons/expected @@ -92,7 +92,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (b : Nat) -> Gen MaybeEmpty .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "DerivedGen.Step" .! ("y", var "y") .! ("x", var "x") .$ var "^bnd^{arg:3}")) + .$ ( var "DerivedGen.Step" + .! ("y", implicitTrue) + .! ("x", implicitTrue) + .$ var "^bnd^{arg:3}")) ] })) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" diff --git a/tests/derivation/least-effort/print/gadt/014 eq deepcons/expected b/tests/derivation/least-effort/print/gadt/014 eq deepcons/expected index 2e60bcf52..dbb2af764 100644 --- a/tests/derivation/least-effort/print/gadt/014 eq deepcons/expected +++ b/tests/derivation/least-effort/print/gadt/014 eq deepcons/expected @@ -101,7 +101,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Nat) -> (b : Nat) -> G .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.Step" .! ("y", var "y") .! ("x", var "x") .$ var "^bnd^{arg:3}"))) + .$ (var "DerivedGen.Step" .! ("y", implicitTrue) .! ("x", implicitTrue) .$ var "^bnd^{arg:3}"))) , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-big/expected b/tests/derivation/least-effort/print/regression/dependent-givens-big/expected index a144b90b0..2ed020667 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-big/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-big/expected @@ -101,7 +101,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe .$ implicitTrue .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "DerivedGen.VectMaybeAnyType.Here" .! ("n", var "n") .! ("xs", var "xs") .! ("x", var "x"))))) + .$ ( var "DerivedGen.VectMaybeAnyType.Here" + .! ("n", implicitTrue) + .! ("xs", var "xs") + .! ("x", var "x"))))) , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef @@ -131,10 +134,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe .$ implicitTrue .$ ( var "DerivedGen.VectMaybeAnyType.There" .! ("z", var "z") - .! ("n", var "n") - .! ("zs", var "zs") - .! ("x", var "x") - .! ("i", var "i") + .! ("n", implicitTrue) + .! ("zs", implicitTrue) + .! ("x", implicitTrue) + .! ("i", implicitTrue) .$ var "^bnd^{arg:4}"))) ] })) diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-small-deep/expected b/tests/derivation/least-effort/print/regression/dependent-givens-small-deep/expected index 0d43d457f..44b63a6e3 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-small-deep/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-small-deep/expected @@ -54,7 +54,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkX" .$ var "n" .$ var "f")) + .$ (var "DerivedGen.MkX" .$ implicitTrue .$ var "f")) , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-small-shallow/expected b/tests/derivation/least-effort/print/regression/dependent-givens-small-shallow/expected index 12b4e1578..9db94345c 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-small-shallow/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-small-shallow/expected @@ -52,7 +52,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkX" .$ var "n" .$ var "f")) + .$ (var "DerivedGen.MkX" .$ implicitTrue .$ var "f")) , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] diff --git a/tests/derivation/least-effort/print/regression/fin-inc/expected b/tests/derivation/least-effort/print/regression/fin-inc/expected index c1f8a1dae..f3a0bba56 100644 --- a/tests/derivation/least-effort/print/regression/fin-inc/expected +++ b/tests/derivation/least-effort/print/regression/fin-inc/expected @@ -88,7 +88,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue - .$ (var "DerivedGen.MkFinInc" .! ("n", var "n") .$ var "val" .$ var "prf")) + .$ (var "DerivedGen.MkFinInc" .! ("n", implicitTrue) .$ implicitTrue .$ var "prf")) ] })) ] @@ -183,8 +183,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "Data.Nat.LTESucc" - .! ("right", var "right") - .! ("left", var "left") + .! ("right", implicitTrue) + .! ("left", implicitTrue) .$ var "^bnd^{arg:1}"))) ] })) diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr new file mode 100644 index 000000000..135e0e3e8 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr @@ -0,0 +1,16 @@ +module DerivedGen + +import Data.Fin + +import Deriving.DepTyCheck.Gen + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +%language ElabReflection + +%logging "deptycheck.derive.print" 5 +%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ + Fuel -> (n : Nat) -> Gen MaybeEmpty (v ** IsFS n v) diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/derive.ipkg b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/expected b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/expected new file mode 100644 index 000000000..8eb2c5761 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/expected @@ -0,0 +1,171 @@ +1/1: Building DerivedGen (DerivedGen.idr) +LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> Gen MaybeEmpty (v : Fin n ** IsFS n v) + MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel") +.=> MkArg MW ExplicitArg (Just "outer^") implicitTrue +.=> local + { decls = + [ 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 "Builtin.DPair.DPair" + .$ (var "Data.Fin.Fin" .$ var "n") + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.IsFS" .$ var "n" .$ var "{arg:1}")) + }) + , 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") + }) + , 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.IsFS" .$ var "n" .$ var "{arg:1}")) + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "^bnd^{k:3643}") + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.ItIsFS (orders)")) + .$ ( var ">>=" + .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "{k:3643}") + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "DerivedGen.ItIsFS" .! ("{k:3643}", implicitTrue) .! ("i", var "i"))))) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.IsFS[0] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") + } + ] + , 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:2}") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:2}"))) + , 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 "Nil"))) + ] + } + } + ] + ] + , scope = var "[0]" .$ var "^outmost-fuel^" .$ var "outer^" + } + diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/run b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend1/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr new file mode 100644 index 000000000..d4ab4c4a4 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr @@ -0,0 +1,16 @@ +module DerivedGen + +import Data.Fin + +import Deriving.DepTyCheck.Gen + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +%language ElabReflection + +%logging "deptycheck.derive.print" 5 +%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ + Fuel -> Gen MaybeEmpty (n ** v ** IsFS n v) diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/derive.ipkg b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/expected b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/expected new file mode 100644 index 000000000..3348d8678 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/expected @@ -0,0 +1,280 @@ +1/1: Building DerivedGen (DerivedGen.idr) +LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** (v : Fin n ** IsFS n v)) + MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel") +.=> 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.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:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.IsFS" .$ var "n" .$ var "{arg:1}"))) + }) + , 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.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ (MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") .=> 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 + "[]" + [ 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.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:1}") (var "Data.Fin.Fin" .$ var "n") + .=> var "DerivedGen.IsFS" .$ var "n" .$ var "{arg:1}"))) + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.ItIsFS (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "^bnd^{k:3643}" .$ bindVar "i" + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "DerivedGen.ItIsFS" .! ("{k:3643}", implicitTrue) .! ("i", var "i")))) + ] + })) + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.IsFS[] (non-recursive)")) + .$ (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.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ (MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") .=> 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 "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ (MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") .=> var "Data.Fin.Fin" .$ var "n")) + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Fin.FZ (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "k") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "Data.Fin.FZ" .! ("k", var "k"))))) + ] + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Fin.FS (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:2}" + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ var "^bnd^{arg:2}")) + ] + })) + ] + ] + , 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[] (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[] (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"))) + ] + } + } + ] + , 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/regression/underscore-in-cons-expl-full-gend2/run b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full-gend2/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/DerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/DerivedGen.idr new file mode 100644 index 000000000..7c24533a3 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/DerivedGen.idr @@ -0,0 +1,16 @@ +module DerivedGen + +import Data.Fin + +import Deriving.DepTyCheck.Gen + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +%language ElabReflection + +%logging "deptycheck.derive.print" 5 +%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ + Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS n v diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/derive.ipkg b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/expected b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/expected new file mode 100644 index 000000000..546f1d57f --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/expected @@ -0,0 +1,68 @@ +1/1: Building DerivedGen (DerivedGen.idr) +LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : Fin n) -> Gen MaybeEmpty (IsFS n v) + MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel") +.=> MkArg MW ImplicitArg (Just "outer^") implicitTrue +.=> MkArg MW ExplicitArg (Just "outer^") implicitTrue +.=> local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { 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 "DerivedGen.IsFS" .$ var "n" .$ var "{arg:1}") + }) + , IDef + emptyFC + "[0, 1]" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" + .= 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") + .-> 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.IsFS" .$ var "n" .$ var "{arg:1}") + }) + , IDef + emptyFC + "<>" + [ var "<>" + .$ bindVar "^cons_fuel^" + .$ (var "Prelude.Types.S" .$ bindVar "^bnd^{k:3643}") + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "i") + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.ItIsFS (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.ItIsFS" .! ("{k:3643}", implicitTrue) .! ("i", var "i"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.IsFS[0, 1] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") + } + ] + ] + , scope = var "[0, 1]" .$ var "^outmost-fuel^" .$ var "outer^" .$ var "outer^" + } + diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/run b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-full/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/DerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/DerivedGen.idr new file mode 100644 index 000000000..1b212c923 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/DerivedGen.idr @@ -0,0 +1,16 @@ +module DerivedGen + +import Data.Fin + +import Deriving.DepTyCheck.Gen + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS (S _) (FS i) + +%language ElabReflection + +%logging "deptycheck.derive.print" 5 +%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ + Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS n v diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/derive.ipkg b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/expected b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/expected new file mode 100644 index 000000000..834525554 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/expected @@ -0,0 +1,68 @@ +1/1: Building DerivedGen (DerivedGen.idr) +LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : Fin n) -> Gen MaybeEmpty (IsFS n v) + MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel") +.=> MkArg MW ImplicitArg (Just "outer^") implicitTrue +.=> MkArg MW ExplicitArg (Just "outer^") implicitTrue +.=> local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { 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 "DerivedGen.IsFS" .$ var "n" .$ var "{arg:1}") + }) + , IDef + emptyFC + "[0, 1]" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^<{arg:1}>" + .= 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") + .-> 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.IsFS" .$ var "n" .$ var "{arg:1}") + }) + , IDef + emptyFC + "<>" + [ var "<>" + .$ bindVar "^cons_fuel^" + .$ (var "Prelude.Types.S" .$ bindVar "^bnd^{_:3643}") + .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "i") + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.ItIsFS (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.ItIsFS" .! ("{_:3643}", implicitTrue) .! ("i", var "i"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.IsFS[0, 1] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^<{arg:1}>") + } + ] + ] + , scope = var "[0, 1]" .$ var "^outmost-fuel^" .$ var "outer^" .$ var "outer^" + } + diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/run b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/underscore-in-cons-expl-partial/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/unification-mismatch-dependent/expected b/tests/derivation/least-effort/print/regression/unification-mismatch-dependent/expected index f896d4019..f6e0a1eec 100644 --- a/tests/derivation/least-effort/print/regression/unification-mismatch-dependent/expected +++ b/tests/derivation/least-effort/print/regression/unification-mismatch-dependent/expected @@ -77,7 +77,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (x : X) -> (x' : X) -> Gen .$ (var "fromString" .$ primVal (Str "DerivedGen.MkZ (orders)")) .$ ( var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkZ" .! ("x", var "x") .$ var "prf")) + .$ (var "DerivedGen.MkZ" .! ("x", implicitTrue) .$ var "prf")) , var "<>" .$ bindVar "^cons_fuel^" .$ (var "DerivedGen.Cons" .$ bindVar "x" .$ bindVar "prf") diff --git a/tests/derivation/least-effort/print/regression/unification-name-mismatch/expected b/tests/derivation/least-effort/print/regression/unification-name-mismatch/expected index 051eda979..1008e0bde 100644 --- a/tests/derivation/least-effort/print/regression/unification-name-mismatch/expected +++ b/tests/derivation/least-effort/print/regression/unification-name-mismatch/expected @@ -129,8 +129,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (xs : X) -> (ys : X) -> Gen .$ ( var "DerivedGen.B" .! ("x", var "x") .! ("y", var "y") - .! ("ys", var "ys") - .! ("xs", var "xs") + .! ("ys", implicitTrue) + .! ("xs", implicitTrue) .$ var "^bnd^{arg:1}"))) , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] diff --git a/tests/derivation/least-effort/print/regression/unnamed-auto-implicit/expected b/tests/derivation/least-effort/print/regression/unnamed-auto-implicit/expected index e82c07f60..f2400dae4 100644 --- a/tests/derivation/least-effort/print/regression/unnamed-auto-implicit/expected +++ b/tests/derivation/least-effort/print/regression/unnamed-auto-implicit/expected @@ -107,9 +107,9 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (f : X) -> Gen MaybeEmpty ( .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.B" - .! ("x", var "x") - .! ("xs", var "xs") - .! ("n", var "n") + .! ("x", implicitTrue) + .! ("xs", implicitTrue) + .! ("n", implicitTrue) .$ var "^bnd^{arg:3}" .@ var "^bnd^{conArg:2}")) ] diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr new file mode 100644 index 000000000..932aa877d --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/DerivedGen.idr @@ -0,0 +1,23 @@ +module DerivedGen + +import RunDerivedGen + +import Data.Fin + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +Show (IsFS n vs) where show ItIsFS = "ItIsFS" + +%language ElabReflection + +checkedGen : Fuel -> (n : Nat) -> Gen MaybeEmpty (v ** IsFS n v) +checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + +main : IO () +main = runGs + [ G $ \fl => checkedGen fl 3 + , G $ \fl => checkedGen fl 0 + ] diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/derive.ipkg b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected new file mode 100644 index 000000000..f3c7133f2 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected @@ -0,0 +1,20 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Error: While processing right hand side of checkedGen. Sorry, I can't find any elaboration which works. All errors: +Possible error: + Error during reflection: While processing right hand side of {u:1837},[0]. While processing right hand side of $resolved13832,<>. {k:1755} is not accessible in this context. + +Possible error: + Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present + + DerivedGen:17:14--17:23 + 13 | + 14 | %language ElabReflection + 15 | + 16 | checkedGen : Fuel -> (n : Nat) -> Gen MaybeEmpty (v ** IsFS n v) + 17 | checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + ^^^^^^^^^ + +[ fatal ] Error when executing system command. + Command: "build/exec/_tmppack" + Error code: 127 diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/run b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr new file mode 100644 index 000000000..414bd25f4 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/DerivedGen.idr @@ -0,0 +1,22 @@ +module DerivedGen + +import RunDerivedGen + +import Data.Fin + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +Show (IsFS n vs) where show ItIsFS = "ItIsFS" + +%language ElabReflection + +checkedGen : Fuel -> Gen MaybeEmpty (n ** v ** IsFS n v) +checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + +main : IO () +main = runGs + [ G $ \fl => checkedGen fl + ] diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/derive.ipkg b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/expected new file mode 100644 index 000000000..36e7faec3 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +(22 ** (17 ** ItIsFS)) +----- +(29 ** (18 ** ItIsFS)) +----- +(29 ** (11 ** ItIsFS)) +----- +(11 ** (6 ** ItIsFS)) +----- +(25 ** (13 ** ItIsFS)) +----- +(25 ** (9 ** ItIsFS)) +----- +(20 ** (5 ** ItIsFS)) +----- +(13 ** (8 ** ItIsFS)) +----- +(13 ** (11 ** ItIsFS)) +----- +(37 ** (16 ** ItIsFS)) diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/run b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend2/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/DerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/DerivedGen.idr new file mode 100644 index 000000000..4e95b763c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/DerivedGen.idr @@ -0,0 +1,23 @@ +module DerivedGen + +import RunDerivedGen + +import Data.Fin + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS _ (FS i) + +Show (IsFS n vs) where show ItIsFS = "ItIsFS" + +%language ElabReflection + +checkedGen : Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS n v +checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + +main : IO () +main = runGs + [ G $ \fl => checkedGen fl $ the (Fin 4) 3 + , G $ \fl => checkedGen fl $ the (Fin 3) 0 + ] diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/derive.ipkg b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/expected new file mode 100644 index 000000000..c2be1814b --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/expected @@ -0,0 +1,25 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/run b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/DerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/DerivedGen.idr new file mode 100644 index 000000000..5f2278141 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/DerivedGen.idr @@ -0,0 +1,23 @@ +module DerivedGen + +import RunDerivedGen + +import Data.Fin + +%default total + +data IsFS : (n : _) -> Fin n -> Type where + ItIsFS : IsFS (S _) (FS i) + +Show (IsFS n vs) where show ItIsFS = "ItIsFS" + +%language ElabReflection + +checkedGen : Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS n v +checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + +main : IO () +main = runGs + [ G $ \fl => checkedGen fl $ the (Fin 4) 3 + , G $ \fl => checkedGen fl $ the (Fin 3) 0 + ] diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/derive.ipkg b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/expected new file mode 100644 index 000000000..c2be1814b --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/expected @@ -0,0 +1,25 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- +ItIsFS +----- diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/run b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-partial/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file