Skip to content

Commit

Permalink
Fix #755 - expose Implies[P,C] variation of Inference[P,C]
Browse files Browse the repository at this point in the history
  • Loading branch information
erikerlandson committed Apr 8, 2020
1 parent b7b52a2 commit 18a5077
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -33,3 +33,27 @@ object Inference {
): Inference[P, C] =
Inference(i1.isValid && i2.isValid, show.format(i1.show, i2.show))
}

/**
* Similar to `Inference[P, C]` but will not implicitly manifest if `C` cannot be
* inferred from `P`.
*
* It is intended to be used with chained implicit definitions that require proof that `P ==> C`
*/
case class Implies[P, C](show: String)

object Implies {
import scala.reflect.macros.blackbox
import eu.timepit.refined.macros.InferMacro
import Inference.==>

implicit def autoImply[A, B](
implicit
ir: A ==> B
): Implies[A, B] = macro InferMacro.implies[A, B]

def manifest[A: c.WeakTypeTag, B: c.WeakTypeTag](
c: blackbox.Context
)(ir: c.Expr[A ==> B]): c.Expr[Implies[A, B]] =
c.universe.reify(Implies[A, B]((ir.splice).show))
}
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package eu.timepit.refined.macros

import eu.timepit.refined.api.Implies
import eu.timepit.refined.api.Inference.==>
import eu.timepit.refined.api.RefType
import eu.timepit.refined.internal.Resources
Expand All @@ -20,4 +21,12 @@ class InferMacro(val c: blackbox.Context) extends MacroUtils {

refTypeInstance(rt).unsafeRewrapM(c)(ta)
}

def implies[A: c.WeakTypeTag, B: c.WeakTypeTag](ir: c.Expr[A ==> B]): c.Expr[Implies[A, B]] = {
val inference = eval(ir)
if (inference.notValid) {
abort(Resources.invalidInference(weakTypeOf[A].toString, weakTypeOf[B].toString))
}
Implies.manifest(c)(ir)
}
}
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
package eu.timepit.refined

import eu.timepit.refined.api.Refined
import eu.timepit.refined.api.{Implies, Refined}
import eu.timepit.refined.auto._
import eu.timepit.refined.char.{Digit, Letter}
import eu.timepit.refined.generic._
import eu.timepit.refined.numeric.{Greater}
import eu.timepit.refined.types.numeric.PosInt
import org.scalacheck.Prop._
import org.scalacheck.Properties
Expand All @@ -22,6 +23,15 @@ class AutoSpec extends Properties("auto") {
a == b
}

property("autoImply") = secure {
val t = implicitly[Implies[Greater[W.`1`.T], Greater[W.`0`.T]]]
illTyped(
"implicitly[Implies[Greater[W.`-1`.T], Greater[W.`0`.T]]]",
"""type mismatch \(invalid inference\):\s*eu.timepit.refined.numeric.Greater\[Int\(-1\)\] does not imply\s*eu.timepit.refined.numeric.Greater\[Int\(0\)\]"""
)
t.show == "greaterInference(1, 0)"
}

property("autoUnwrap: PosInt: Int") = secure {
val a: PosInt = PosInt.unsafeFrom(1)
val b: Int = a
Expand Down

0 comments on commit 18a5077

Please sign in to comment.