Skip to content

Commit

Permalink
[ experim ] Use implicitFalse where it's better to be used
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden committed Sep 2, 2024
1 parent 71df745 commit db0d75f
Show file tree
Hide file tree
Showing 13 changed files with 67 additions and 65 deletions.
22 changes: 11 additions & 11 deletions examples/covering-seq/tests/gens/print/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,8 +301,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
var "<<Data.List.Covering.BitMask.Index.Here>>"
.$ 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"
Expand All @@ -312,8 +312,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
[ var "<<Data.List.Covering.BitMask.Index.Here>>"
.$ 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"
Expand All @@ -324,8 +324,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
, var "<<Data.List.Covering.BitMask.Index.Here>>"
.$ 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"
Expand All @@ -345,8 +345,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (bs : BitMask n) -> Gen May
[ var "<<Data.List.Covering.BitMask.Index.There>>"
.$ 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)"))
Expand Down Expand Up @@ -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
Expand All @@ -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)"))
Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions tests/derivation/least-effort/print/regression/dependent-givens-expl-big/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe
[ var "<<DerivedGen.VectMaybeAnyType.Here>>"
.$ 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"
Expand All @@ -110,7 +110,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (v : VectMaybe
[ var "<<DerivedGen.VectMaybeAnyType.There>>"
.$ 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 ">>="
Expand Down
4 changes: 2 additions & 2 deletions tests/derivation/least-effort/print/regression/dependent-givens-expl-small-deep/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/regression/dependent-givens-expl-small-shallow/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) ->
[ var "<<DerivedGen.MkX>>"
.$ 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"
Expand Down
4 changes: 2 additions & 2 deletions tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) ->
[ var "<<DerivedGen.VectMaybeAnyType.Here>>"
.$ 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"
Expand All @@ -113,7 +113,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) ->
[ var "<<DerivedGen.VectMaybeAnyType.There>>"
.$ 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 ">>="
Expand Down
4 changes: 2 additions & 2 deletions tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) ->
[ var "<<DerivedGen.MkX>>"
.$ 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"
Expand Down
2 changes: 1 addition & 1 deletion tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Loading

0 comments on commit db0d75f

Please sign in to comment.