diff --git a/examples/covering-seq/tests/gens/print/expected b/examples/covering-seq/tests/gens/print/expected index 5c91b882b..7c819d0d5 100644 --- a/examples/covering-seq/tests/gens/print/expected +++ b/examples/covering-seq/tests/gens/print/expected @@ -301,8 +301,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May 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") + .$ (var "Data.Fin.FZ" .! ("k", implicitFalse)) + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "to_be_deceqed^^b0" , rig = MW , wval = var "Decidable.Equality.decEq" .$ var "to_be_deceqed^^b0" .$ var "b" @@ -312,8 +312,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May [ 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") + .$ (var "Data.Fin.FZ" .! ("k", implicitFalse)) + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "b" .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .= var "Test.DepTyCheck.Gen.label" @@ -324,8 +324,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May , 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") + .$ (var "Data.Fin.FZ" .! ("k", implicitFalse)) + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "to_be_deceqed^^b0" .$ (var "Prelude.No" .$ implicitTrue) .= var "empty" @@ -345,8 +345,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May [ 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") + .$ (var "Data.Fin.FS" .! ("k", implicitFalse) .$ bindVar "i") + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "b" .$ bindVar "bs") .$ bindVar "v" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.There (orders)")) @@ -644,7 +644,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") .$ bindVar "b" - .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "to_be_deceqed^^b0" .$ bindVar "bs") + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "to_be_deceqed^^b0" .$ bindVar "bs") , rig = MW , wval = var "Decidable.Equality.decEq" .$ var "to_be_deceqed^^b0" .$ var "b" , prf = Nothing @@ -654,7 +654,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") .$ bindVar "b" - .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitTrue) .$ bindVar "b" .$ bindVar "bs") + .$ (var "Data.List.Covering.BitMask.(::)" .! ("n", implicitFalse) .$ bindVar "b" .$ bindVar "bs") .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.List.Covering.BitMask.Index.Continue (orders)")) @@ -677,7 +677,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May .$ (var "Prelude.Types.S" .$ bindVar "n") .$ bindVar "b" .$ ( var "Data.List.Covering.BitMask.(::)" - .! ("n", implicitTrue) + .! ("n", implicitFalse) .$ bindVar "to_be_deceqed^^b0" .$ bindVar "bs") .$ (var "Prelude.No" .$ implicitTrue) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr index 1cc7e3e0b..37265f3eb 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr @@ -62,7 +62,7 @@ canonicConsBody sig name con = do renamedAppliedNames <- for appliedNames.asVect $ \(name, typeDetermined) => do let bindName = bindNameRenamer name if cast typeDetermined - then pure $ const `(_) -- no need to match type-determined parameter by hand + then pure $ const implicitFalse -- no need to match type-determined parameter by hand else if contains name !get then do -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-expl-big/expected b/tests/derivation/least-effort/print/regression/dependent-givens-expl-big/expected index a144b90b0..6638cf052 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-expl-big/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-expl-big/expected @@ -92,7 +92,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitTrue) .$ bindVar "x" .$ bindVar "xs") + .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitFalse) .$ bindVar "x" .$ bindVar "xs") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.VectMaybeAnyType.Here (orders)")) .$ ( var "Prelude.pure" @@ -110,7 +110,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitTrue) .$ bindVar "z" .$ bindVar "zs") + .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitFalse) .$ bindVar "z" .$ bindVar "zs") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.VectMaybeAnyType.There (orders)")) .$ ( var ">>=" diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-deep/expected b/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-deep/expected index 0d43d457f..ef59fe474 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-deep/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-deep/expected @@ -48,8 +48,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ bindVar "n")) .$ ( var "Data.Fin.FS" - .! ("k", var "Prelude.Types.S" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "f")) + .! ("k", var "Prelude.Types.S" .$ implicitFalse) + .$ (var "Data.Fin.FS" .! ("k", implicitFalse) .$ bindVar "f")) .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-shallow/expected b/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-shallow/expected index 12b4e1578..c106f6a79 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-shallow/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-expl-small-shallow/expected @@ -47,7 +47,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "f") + .$ (var "Data.Fin.FS" .! ("k", implicitFalse) .$ bindVar "f") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected index ea2ce22cf..1e1e8a558 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected @@ -92,7 +92,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) -> [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "^bnd^{n:4022}") - .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitTrue) .$ bindVar "x" .$ bindVar "xs") + .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitFalse) .$ bindVar "x" .$ bindVar "xs") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.VectMaybeAnyType.Here (orders)")) .$ ( var "Prelude.pure" @@ -113,7 +113,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) -> [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitTrue) .$ bindVar "z" .$ bindVar "zs") + .$ (var "DerivedGen.VectMaybeAnyType.(::)" .! ("n", implicitFalse) .$ bindVar "z" .$ bindVar "zs") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.VectMaybeAnyType.There (orders)")) .$ ( var ">>=" diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected index 024b352f1..d7fefd5f8 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected @@ -48,8 +48,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ bindVar "n")) .$ ( var "Data.Fin.FS" - .! ("k", var "Prelude.Types.S" .$ implicitTrue) - .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "f")) + .! ("k", var "Prelude.Types.S" .$ implicitFalse) + .$ (var "Data.Fin.FS" .! ("k", implicitFalse) .$ bindVar "f")) .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected index c34b30a21..cf61efdc6 100644 --- a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected +++ b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected @@ -47,7 +47,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) -> [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "n") - .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "f") + .$ (var "Data.Fin.FS" .! ("k", implicitFalse) .$ bindVar "f") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var "Prelude.pure" diff --git a/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr b/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr index e8a337d19..28cbdbfc0 100644 --- a/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr +++ b/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr @@ -11,5 +11,5 @@ record FinInc n where %language ElabReflection -%logging "deptycheck.derive.print" 5 +%logging "deptycheck.derive.print" 15 %runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> Gen MaybeEmpty (n ** FinInc n) diff --git a/tests/derivation/least-effort/print/regression/too-early-rename-multiple-complex/expected b/tests/derivation/least-effort/print/regression/too-early-rename-multiple-complex/expected index 982aa6d11..3f52301f0 100644 --- a/tests/derivation/least-effort/print/regression/too-early-rename-multiple-complex/expected +++ b/tests/derivation/least-effort/print/regression/too-early-rename-multiple-complex/expected @@ -52,13 +52,13 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.False") .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" - , var "DerivedGen.MkY" .! ("m", implicitTrue) .! ("b", var "Prelude.Basics.False") .! ("n", implicitTrue) + , var "DerivedGen.MkY" .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.False") .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^m1" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" - , var "DerivedGen.MkY" .! ("m", implicitTrue) .! ("b", var "Prelude.Basics.True") .! ("n", implicitTrue) + , var "DerivedGen.MkY" .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.True") .! ("n", implicitFalse) )) , rig = MW , wval = var "Decidable.Equality.decEq" .$ var "to_be_deceqed^^m1" .$ var "m" @@ -74,18 +74,18 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.False") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.True") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") , rig = MW @@ -100,18 +100,18 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.False") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.True") .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.True") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .$ (var "Prelude.Yes" .$ var "Builtin.Refl") @@ -127,18 +127,18 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.False") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.True") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .$ (var "Prelude.No" .$ implicitTrue) @@ -152,18 +152,18 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ (var "DerivedGen.MkX" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.False") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^m1" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" - .! ("m", implicitTrue) + .! ("m", implicitFalse) .! ("b", var "Prelude.Basics.True") - .! ("n", implicitTrue) + .! ("n", implicitFalse) )) .$ (var "Prelude.No" .$ implicitTrue) .= var "empty" diff --git a/tests/derivation/least-effort/print/regression/too-early-rename-multiple-simple/expected b/tests/derivation/least-effort/print/regression/too-early-rename-multiple-simple/expected index 35aa68636..0df9e136a 100644 --- a/tests/derivation/least-effort/print/regression/too-early-rename-multiple-simple/expected +++ b/tests/derivation/least-effort/print/regression/too-early-rename-multiple-simple/expected @@ -51,7 +51,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ bindVar "m" .$ var "Prelude.Basics.False") .! ( "{conArg:1}" - , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("m", implicitTrue) .! ("n", implicitTrue) + , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("m", implicitFalse) .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ ( var "DerivedGen.MkX" @@ -59,7 +59,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ bindVar "to_be_deceqed^^m1" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" - , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("m", implicitTrue) .! ("n", implicitTrue) + , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("m", implicitFalse) .! ("n", implicitFalse) )) , rig = MW , wval = var "Decidable.Equality.decEq" .$ var "to_be_deceqed^^m1" .$ var "m" @@ -75,16 +75,16 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ bindVar "m" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") , rig = MW @@ -99,16 +99,16 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ bindVar "m" .$ var "Prelude.Basics.True") .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .$ (var "Prelude.Yes" .$ var "Builtin.Refl") @@ -124,8 +124,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ ( var "DerivedGen.MkX" @@ -135,8 +135,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .$ (var "Prelude.No" .$ implicitTrue) @@ -150,8 +150,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ ( var "DerivedGen.MkZ" .$ ( var "DerivedGen.MkX" @@ -161,8 +161,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .! ( "{conArg:1}" , var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") - .! ("m", implicitTrue) - .! ("n", implicitTrue) + .! ("m", implicitFalse) + .! ("n", implicitFalse) )) .$ (var "Prelude.No" .$ implicitTrue) .= var "empty" diff --git a/tests/derivation/least-effort/print/regression/too-early-rename-single-dependency/expected b/tests/derivation/least-effort/print/regression/too-early-rename-single-dependency/expected index 450dadd17..0384f6e63 100644 --- a/tests/derivation/least-effort/print/regression/too-early-rename-single-dependency/expected +++ b/tests/derivation/least-effort/print/regression/too-early-rename-single-dependency/expected @@ -50,10 +50,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ bindVar "^cons_fuel^" .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.False") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitFalse))) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitFalse))) , rig = MW , wval = var "Decidable.Equality.decEq" .$ var "to_be_deceqed^^n0" .$ var "n" , prf = Nothing @@ -63,10 +63,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ bindVar "^cons_fuel^" .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.False") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitFalse))) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.True") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitFalse))) .$ (var "Prelude.Yes" .$ var "Builtin.Refl") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkW (orders)")) @@ -77,10 +77,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (a : Z) -> (b : Z) -> Gen M .$ bindVar "^cons_fuel^" .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "n" .$ var "Prelude.Basics.False") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.False") .! ("n", implicitFalse))) .$ ( var "DerivedGen.MkZ" .$ (var "DerivedGen.MkX" .$ bindVar "to_be_deceqed^^n0" .$ var "Prelude.Basics.True") - .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitTrue))) + .! ("{conArg:1}", var "DerivedGen.MkY" .! ("b", var "Prelude.Basics.True") .! ("n", implicitFalse))) .$ (var "Prelude.No" .$ implicitTrue) .= var "empty" ] diff --git a/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr b/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr index 4d656ea01..6b52563ba 100644 --- a/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr +++ b/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr @@ -12,6 +12,8 @@ record FinInc n where Show (FinInc n) where show (MkFinInc v p) = "MkFinInc \{show v} prf" +%logging "deptycheck" 15 + checkedGen : Fuel -> Gen MaybeEmpty (n ** FinInc n) checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}