Merge pull request #927 from matwojcik/feature-917-inference

Add inference for #917
fthomas · May 19, 2021 · 758d3ff · 758d3ff
2 parents f041655 + ea46a0a
commit 758d3ff
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 0 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
@@ -245,6 +245,15 @@ 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)")
 

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
@@ -273,6 +273,15 @@ 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)")
 

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
@@ -5,6 +5,8 @@ import eu.timepit.refined.api.Inference
 import eu.timepit.refined.boolean._
 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 org.scalacheck.Prop._
 import org.scalacheck.Properties
 import shapeless.test.illTyped
@@ -20,6 +22,14 @@ class BooleanInferenceSpec extends Properties("BooleanInference") {
     Inference[Not[Not[UpperCase]], UpperCase].isValid
   }
 
+  property("substitution in conjunction") = secure {
+    Inference[NonEmpty And ValidLong, NonEmpty And (ValidLong Or ValidDouble)].isValid
+  }
+
+  property("elimination of tautology in disjunction") = secure {
+    Inference[(NonEmpty And ValidLong) Or (NonEmpty And ValidDouble), NonEmpty].isValid
+  }
+
   property("double negation elimination 2x") = secure {
     Inference[Not[Not[Not[Not[UpperCase]]]], UpperCase].isValid
   }