From f25f46ef463204059215bc7760bd4e7c6e15583b Mon Sep 17 00:00:00 2001 From: matwojcik Date: Fri, 9 Jul 2021 18:48:04 +0200 Subject: [PATCH 1/3] Move inferences to lower level of implicits, fixes #990 --- .../eu/timepit/refined/boolean.scala | 23 +++++++++++-------- .../eu/timepit/refined/boolean.scala | 22 ++++++++++-------- .../refined/BooleanInferenceSpec.scala | 8 +++++++ 3 files changed, 33 insertions(+), 20 deletions(-) diff --git a/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala b/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala index aca5edcf0..55a71b64e 100644 --- a/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala +++ b/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala @@ -245,15 +245,6 @@ private[refined] trait BooleanInference0 extends BooleanInference1 { implicit def conjunctionCommutativity[A, B]: (A And B) ==> (B And A) = Inference.alwaysValid("conjunctionCommutativity") - implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) = - p1.adapt("substitutionInConjunction(%s)") - - implicit def disjunctionTautologyElimination[A, B, C](implicit - p1: A ==> C, - p2: B ==> C - ): (A Or B) ==> C = - Inference.combine(p1, p2, "disjunctionElimination") - implicit def conjunctionEliminationR[A, B, C](implicit p1: B ==> C): (A And B) ==> C = p1.adapt("conjunctionEliminationR(%s)") @@ -291,7 +282,7 @@ private[refined] trait BooleanInference1 extends BooleanInference2 { p1.adapt("modusTollens(%s)") } -private[refined] trait BooleanInference2 { +private[refined] trait BooleanInference2 extends BooleanInference3 { implicit def conjunctionEliminationL[A, B, C](implicit p1: A ==> C): (A And B) ==> C = p1.adapt("conjunctionEliminationL(%s)") @@ -299,3 +290,15 @@ private[refined] trait BooleanInference2 { implicit def hypotheticalSyllogism[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C = Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)") } + +private[refined] trait BooleanInference3 { + + implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) = + p1.adapt("substitutionInConjunction(%s)") + + implicit def disjunctionTautologyElimination[A, B, C](implicit + p1: A ==> C, + p2: B ==> C + ): (A Or B) ==> C = + Inference.combine(p1, p2, "disjunctionElimination") +} diff --git a/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala b/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala index 3cba9c5c5..d7472b5e7 100644 --- a/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala +++ b/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala @@ -273,15 +273,6 @@ private[refined] trait BooleanInference0 extends BooleanInference1 { implicit def conjunctionCommutativity[A, B]: (A And B) ==> (B And A) = Inference.alwaysValid("conjunctionCommutativity") - implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) = - p1.adapt("substitutionInConjunction(%s)") - - implicit def disjunctionTautologyElimination[A, B, C](implicit - p1: A ==> C, - p2: B ==> C - ): (A Or B) ==> C = - Inference.combine(p1, p2, "disjunctionElimination") - implicit def conjunctionEliminationR[A, B, C](implicit p1: B ==> C): (A And B) ==> C = p1.adapt("conjunctionEliminationR(%s)") @@ -319,7 +310,7 @@ private[refined] trait BooleanInference1 extends BooleanInference2 { p1.adapt("modusTollens(%s)") } -private[refined] trait BooleanInference2 { +private[refined] trait BooleanInference2 extends BooleanInference3 { implicit def conjunctionEliminationL[A, B, C](implicit p1: A ==> C): (A And B) ==> C = p1.adapt("conjunctionEliminationL(%s)") @@ -327,3 +318,14 @@ private[refined] trait BooleanInference2 { implicit def hypotheticalSyllogism[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C = Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)") } +private[refined] trait BooleanInference3 { + + implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) = + p1.adapt("substitutionInConjunction(%s)") + + implicit def disjunctionTautologyElimination[A, B, C](implicit + p1: A ==> C, + p2: B ==> C + ): (A Or B) ==> C = + Inference.combine(p1, p2, "disjunctionElimination") +} diff --git a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala index 99b007acf..1db31b30d 100644 --- a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala +++ b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala @@ -7,6 +7,7 @@ import eu.timepit.refined.char.{Digit, Letter, UpperCase, Whitespace} import eu.timepit.refined.numeric._ import eu.timepit.refined.string._ import eu.timepit.refined.collection._ +import eu.timepit.refined.predicates.all.{Equal, LetterOrDigit} import org.scalacheck.Prop._ import org.scalacheck.Properties import shapeless.test.illTyped @@ -72,6 +73,13 @@ class BooleanInferenceSpec extends Properties("BooleanInference") { Inference[Letter And UpperCase, UpperCase].isValid } + property("complex conjunction elimination") = secure { + type BaseRefinement = And[Size[Equal[10]], Forall[LetterOrDigit]] + type ConcreteRefinement = And[StartsWith[W.`"001"`.T], BaseRefinement] + + Inference[ConcreteRefinement, BaseRefinement].isValid + } + property("conjunction introduction") = wellTyped { illTyped("Inference[UpperCase, UpperCase And Digit]", "could not find.*Inference.*") } From a99a74d4b5a9788ddd4de7ad11efb0a7ee239e60 Mon Sep 17 00:00:00 2001 From: matwojcik Date: Fri, 9 Jul 2021 18:59:55 +0200 Subject: [PATCH 2/3] Compilation fix --- .../scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala index 1db31b30d..5aacb560a 100644 --- a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala +++ b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala @@ -7,7 +7,8 @@ import eu.timepit.refined.char.{Digit, Letter, UpperCase, Whitespace} import eu.timepit.refined.numeric._ import eu.timepit.refined.string._ import eu.timepit.refined.collection._ -import eu.timepit.refined.predicates.all.{Equal, LetterOrDigit} +import eu.timepit.refined.generic.Equal +import eu.timepit.refined.char.LetterOrDigit import org.scalacheck.Prop._ import org.scalacheck.Properties import shapeless.test.illTyped From 64271a74589e11fda6476fe68b05fdbaed542118 Mon Sep 17 00:00:00 2001 From: matwojcik Date: Fri, 9 Jul 2021 19:16:56 +0200 Subject: [PATCH 3/3] Fix Scala 2.12 --- .../scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala index 5aacb560a..29b9752b8 100644 --- a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala +++ b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala @@ -75,7 +75,7 @@ class BooleanInferenceSpec extends Properties("BooleanInference") { } property("complex conjunction elimination") = secure { - type BaseRefinement = And[Size[Equal[10]], Forall[LetterOrDigit]] + type BaseRefinement = And[Size[Equal[W.`10`.T]], Forall[LetterOrDigit]] type ConcreteRefinement = And[StartsWith[W.`"001"`.T], BaseRefinement] Inference[ConcreteRefinement, BaseRefinement].isValid