diff --git a/src/main/scala/singleton/ops/OpIntercept.scala b/src/main/scala/singleton/ops/OpIntercept.scala new file mode 100644 index 00000000..35a03d64 --- /dev/null +++ b/src/main/scala/singleton/ops/OpIntercept.scala @@ -0,0 +1,9 @@ +package singleton.ops +import impl._ + +import scala.annotation.implicitNotFound +@implicitNotFound("Missing an `OpIntercept` implicit for the operation ${Op}") +trait OpIntercept[Op <: HasOut] extends HasOutValue +object OpIntercept { + type Aux[Op <: HasOut, Out0] = OpIntercept[Op]{type Out = Out0} +} \ No newline at end of file diff --git a/src/main/scala/singleton/ops/impl/GeneralMacros.scala b/src/main/scala/singleton/ops/impl/GeneralMacros.scala index 6679139b..18687b56 100644 --- a/src/main/scala/singleton/ops/impl/GeneralMacros.scala +++ b/src/main/scala/singleton/ops/impl/GeneralMacros.scala @@ -1,13 +1,17 @@ package singleton.ops.impl import singleton.twoface.impl.TwoFaceAny -import scala.reflect.macros.whitebox +import scala.reflect.macros.{TypecheckException, whitebox} private object MacroCache { import scala.collection.mutable val cache = mutable.Map.empty[Any, Any] def get(key : Any) : Option[Any] = cache.get(key) def add[V <: Any](key : Any, value : V) : V = {cache += (key -> value); value} + var errorCache : String = "" + def clearErrorCache() : Unit = errorCache = "" + def setErrorCache(msg : String) : Unit = errorCache = msg + def getErrorMessage : String = errorCache } trait GeneralMacros { val c: whitebox.Context @@ -261,7 +265,7 @@ trait GeneralMacros { def unapply(arg: CalcType): Option[Primitive] = Some(arg.primitive) } - case class CalcUnknown(tpe : Type, treeOption : Option[Tree]) extends Calc { + case class CalcUnknown(tpe : Type, treeOption : Option[Tree], opIntercept : Boolean) extends Calc { override val primitive: Primitive = Primitive.Unknown(tpe, "Unknown") } object NonLiteralCalc { @@ -456,7 +460,7 @@ trait GeneralMacros { def unapply(tp: Type): Option[Calc] = { tp match { case TypeRef(_, sym, ft :: tp :: _) if sym == opMacroSym && ft.typeSymbol == funcTypes.GetType => - Some(CalcUnknown(tp, None)) + Some(CalcUnknown(tp, None, opIntercept = false)) case TypeRef(_, sym, args) if sym == opMacroSym => VerboseTraversal(s"@@OpCalc@@\nTP: $tp\nRAW: ${showRaw(tp)}") val funcType = args.head.typeSymbol.asType @@ -473,7 +477,7 @@ trait GeneralMacros { case (funcTypes.ImplicitFound, _) => setUncachingReason(1) aValue match { - case CalcUnknown(t, _) => try { + case CalcUnknown(t, _, false) => try { c.typecheck(q"implicitly[$t]") Some(CalcLit(true)) } catch { @@ -484,7 +488,7 @@ trait GeneralMacros { } case (funcTypes.EnumCount, _) => aValue match { - case CalcUnknown(t, _) => Some(CalcLit(t.typeSymbol.asClass.knownDirectSubclasses.size)) + case CalcUnknown(t, _, false) => Some(CalcLit(t.typeSymbol.asClass.knownDirectSubclasses.size)) case _ => Some(CalcLit(0)) } case (funcTypes.IsNat, _) => @@ -551,7 +555,8 @@ trait GeneralMacros { case _ => //regular cases opCalc(funcType, aValue, bValue, cValue) match { case (res : CalcVal) => Some(res) - case u @ CalcUnknown(_,Some(_)) => Some(u) //Accept unknown values with a tree + case u @ CalcUnknown(_,Some(_), _) => Some(u) //Accept unknown values with a tree + case oi @ CalcUnknown(_,_, true) => Some(oi) //Accept unknown op interception case _ => None } } @@ -575,7 +580,7 @@ trait GeneralMacros { case Some(t : CalcUnknown) => t case _ => VerboseTraversal(s"@@Unknown@@\nTP: $tp\nRAW: ${showRaw(tp)}") - CalcUnknown(tp, None) + CalcUnknown(tp, None, opIntercept = false) } } @@ -654,10 +659,11 @@ trait GeneralMacros { } //////////////////////////////////////////////////////////////////////// - def abort(msg: String, annotatedSym : Option[TypeSymbol] = defaultAnnotatedSym): Nothing = { + def abort(msg: String, annotatedSym : Option[TypeSymbol] = defaultAnnotatedSym, position : Position = c.enclosingPosition): Nothing = { VerboseTraversal(s"!!!!!!aborted with: $msg at $annotatedSym, $defaultAnnotatedSym") if (annotatedSym.isDefined) setAnnotation(msg, annotatedSym.get) - c.abort(c.enclosingPosition, msg) + MacroCache.setErrorCache(msg) //propagating the error in case this is an inner implicit call for OpIntercept + c.abort(position, msg) } def buildWarningMsgLoc : String = s"${c.enclosingPosition.source.path}:${c.enclosingPosition.line}:${c.enclosingPosition.column}" @@ -734,11 +740,11 @@ trait GeneralMacros { case None => q""" new $opTpe { - type OutWide = Option[$outTpe] - type Out = Option[$outTpe] - final val value: Option[$outTpe] = None + type OutWide = $outTpe + type Out = $outTpe + final lazy val value: $outTpe = throw new IllegalArgumentException("This operation does not produce a value.") final val isLiteral = false - final val valueWide: Option[$outTpe] = None + final lazy val valueWide: $outTpe = throw new IllegalArgumentException("This operation does not produce a value.") } """ } @@ -771,11 +777,11 @@ trait GeneralMacros { } opTree match { - case q"""{ - $mods class $tpname[..$tparams] $ctorMods(...$paramss) extends ..$parents { $self => ..$opClsBlk } - $expr(...$exprss) - }""" => getOut(opClsBlk) - case _ => extractionFailed(opTree) + case q"""{ + $mods class $tpname[..$tparams] $ctorMods(...$paramss) extends ..$parents { $self => ..$opClsBlk } + $expr(...$exprss) + }""" => getOut(opClsBlk) + case _ => extractionFailed(opTree) } } @@ -881,7 +887,7 @@ trait GeneralMacros { val (typedTree, tpe) = GetArgTree(argIdx, lhs) VerboseTraversal(s"@@extractFromArg@@\nTP: $tpe\nRAW: ${showRaw(tpe)}\nTree: $typedTree") TypeCalc(tpe) match { - case _ : CalcUnknown => CalcUnknown(tpe, Some(c.untypecheck(typedTree))) + case _ : CalcUnknown => CalcUnknown(tpe, Some(c.untypecheck(typedTree)), opIntercept = false) case t : CalcNLit => CalcNLit(t, typedTree) case t => t } @@ -899,9 +905,28 @@ trait GeneralMacros { lazy val b = bCalc lazy val cArg = cCalc def unsupported() : Calc = { - (a, b) match { - case (aArg : CalcVal, bArg : CalcVal) => abort(s"Unsupported $funcType[$a, $b, $cArg]") - case _ => CalcUnknown(funcType.toType, None) + val opMacroTpe = typeOf[OpMacro[_,_,_,_]].typeConstructor + val opTpe = appliedType(opMacroTpe, List(funcType.toType, a.tpe, b.tpe, cArg.tpe)) + val interceptTpe = typeOf[singleton.ops.OpIntercept[_]].typeConstructor + MacroCache.clearErrorCache() + try { + val itree = c.inferImplicitValue ( + appliedType(interceptTpe, List(opTpe)), + silent = false + ) + TypeCalc(itree.tpe.decls.head.info) match { + case t : CalcUnknown => t.copy(treeOption = Some(c.untypecheck(q"$itree.value")),opIntercept = true) //the unknown result must be marked properly so we allow it later + case t => t + } + } catch { + case TypecheckException(_, _) => + MacroCache.getErrorMessage match { + case m if m.nonEmpty => abort(m) + case _ => (a, b) match { + case (_ : CalcVal, _ : CalcVal) => abort(s"Unsupported operation $opTpe") + case _ => CalcUnknown(funcType.toType, None, opIntercept = false) + } + } } } @@ -1055,7 +1080,7 @@ trait GeneralMacros { } //directly using the java lib `require` resulted in compiler crash, so we use wrapped require instead case CalcNLit(Primitive.String, msg, _) => cArg match { - case CalcUnknown(t, _) if t.typeSymbol == symbolOf[Warn] => + case CalcUnknown(t, _, false) if t.typeSymbol == symbolOf[Warn] => CalcNLit(Primitive.Boolean, q"""{println(${buildWarningMsg(msg)}); false}""") case _ => CalcNLit(Primitive.Boolean, q"{_root_.singleton.ops.impl._require(false, $msg); false}") @@ -1065,7 +1090,7 @@ trait GeneralMacros { case CalcNLit(Primitive.Boolean, cond, _) => b match { //directly using the java lib `require` resulted in compiler crash, so we use wrapped require instead case CalcVal(msg : String, msgt) => cArg match { - case CalcUnknown(t, _) if t == symbolOf[Warn] => + case CalcUnknown(t, _, false) if t == symbolOf[Warn] => CalcNLit(Primitive.Boolean, q"""{ if ($cond) true @@ -1366,7 +1391,7 @@ trait GeneralMacros { case funcTypes.PrefixMatch => PrefixMatch case funcTypes.ReplaceFirstMatch => ReplaceFirstMatch case funcTypes.ReplaceAllMatches => ReplaceAllMatches - case _ => abort(s"Unsupported $funcType[$a, $b, $cArg]") + case _ => unsupported() } } @@ -1381,6 +1406,7 @@ trait GeneralMacros { else genOpTreeNat(opTpe, t) case (_, CalcLit(_, t)) => genOpTreeLit(opTpe, t) case (funcTypes.AcceptNonLiteral | funcTypes.GetArg, t : CalcNLit) => genOpTreeNLit(opTpe, t) + case (_, t @ CalcUnknown(_,_,true)) => genOpTreeUnknown(opTpe, t) case (funcTypes.GetArg, t : CalcUnknown) => genOpTreeUnknown(opTpe, t) case (_, t: CalcNLit) => abort("Calculation has returned a non-literal type/value.\nTo accept non-literal values, use `AcceptNonLiteral[T]`.") @@ -1500,7 +1526,7 @@ trait GeneralMacros { } } - val reqCalc = opCalc(funcTypes.Require, condCalc, msgCalc, CalcUnknown(typeOf[NoSym], None)) + val reqCalc = opCalc(funcTypes.Require, condCalc, msgCalc, CalcUnknown(typeOf[NoSym], None, opIntercept = false)) q""" (new $chkSym[$condTpe, $msgTpe, $chkArgTpe]($outTree.asInstanceOf[$outTpe])) @@ -1566,7 +1592,7 @@ trait GeneralMacros { } } - val reqCalc = opCalc(funcTypes.Require, condCalc, msgCalc, CalcUnknown(typeOf[NoSym], None)) + val reqCalc = opCalc(funcTypes.Require, condCalc, msgCalc, CalcUnknown(typeOf[NoSym], None, opIntercept = false)) q""" (new $chkSym[$condTpe, $msgTpe, $chkArgTpe, $paramFaceTpe, $paramTpe]($outTree.asInstanceOf[$outTpe])) diff --git a/src/main/scala/singleton/ops/impl/Op.scala b/src/main/scala/singleton/ops/impl/Op.scala index 1544434e..ca400f7c 100644 --- a/src/main/scala/singleton/ops/impl/Op.scala +++ b/src/main/scala/singleton/ops/impl/Op.scala @@ -6,7 +6,11 @@ trait HasOut extends Any with Serializable { type Out } -trait Op extends HasOut { +trait HasOutValue extends HasOut { + val value : Out +} + +trait Op extends HasOutValue { type OutWide type Out type OutNat <: Nat @@ -29,7 +33,7 @@ protected[singleton] object OpGen { implicit def getValue[O <: Op, Out](o : Aux[O, Out]) : Out = o.value } -trait OpCast[T, O <: Op] extends HasOut {type Out <: T; val value : Out} +trait OpCast[T, O <: Op] extends HasOutValue {type Out <: T} @scala.annotation.implicitNotFound(msg = "Unable to prove type argument is a Nat.") diff --git a/src/main/scala/singleton/ops/rational.scala b/src/main/scala/singleton/ops/rational.scala new file mode 100644 index 00000000..c48412ff --- /dev/null +++ b/src/main/scala/singleton/ops/rational.scala @@ -0,0 +1,245 @@ +package singleton.ops + +import singleton.ops._ +import singleton.ops.impl.{OpCast, OpGen, OpInt, OpMacro} + +object rational { + /** Represents a rational number + * + * @tparam N the numerator + * @tparam D the denominator + */ + trait Rational[N, D] { + def n(implicit nv: Id[N]): nv.Out = nv.value + def d(implicit dv: Id[D]): dv.Out = dv.value + def show(implicit nv: Id[N], dv: Id[D]): String = s"Rational(${n}, ${d})" + } + + trait AlignTypeOpId + type AlignType[V, P] = OpMacro[AlignTypeOpId, V, P, W.`0`.T] + implicit def doAlignTypeInt[V, P <: XInt](implicit + v: ToInt[V]): OpIntercept.Aux[AlignType[V, P], v.Out] = ??? + implicit def doAlignTypeLong[V, P <: XLong](implicit + v: ToLong[V]): OpIntercept.Aux[AlignType[V, P], v.Out] = ??? + implicit def doAlignTypeFloat[V, P <: XFloat](implicit + v: ToFloat[V]): OpIntercept.Aux[AlignType[V, P], v.Out] = ??? + implicit def doAlignTypeDouble[V, P <: XDouble](implicit + v: ToDouble[V]): OpIntercept.Aux[AlignType[V, P], v.Out] = ??? + + trait IsPositiveOpId + type IsPositive[P] = OpMacro[IsPositiveOpId, P, W.`0`.T, W.`0`.T] + implicit def doIsPositive[P](implicit + tst: P > AlignType[0, P]): OpIntercept.Aux[IsPositive[P], tst.Out] = ??? + + trait IsNegativeOpId + type IsNegative[P] = OpMacro[IsNegativeOpId, P, W.`0`.T, W.`0`.T] + implicit def doIsNegative[P](implicit + tst: P < AlignType[0, P]): OpIntercept.Aux[IsNegative[P], tst.Out] = ??? + + trait IsZeroOpId + type IsZero[P] = OpMacro[IsZeroOpId, P, W.`0`.T, W.`0`.T] + implicit def doIsZero[P](implicit + tst: P == AlignType[0, P]): OpIntercept.Aux[IsZero[P], tst.Out] = ??? + + trait IsNonZeroOpId + type IsNonZero[P] = OpMacro[IsNonZeroOpId, P, W.`0`.T, W.`0`.T] + implicit def doIsNonZero[P](implicit + tst: P != AlignType[0, P]): OpIntercept.Aux[IsNonZero[P], tst.Out] = ??? + + trait IsIntegralOpId + type IsIntegral[P] = OpMacro[IsIntegralOpId, P, W.`0`.T, W.`0`.T] + implicit def doIsIntegral[P](implicit + tst: IsInt[P] || IsLong[P]): OpIntercept.Aux[IsIntegral[P], tst.Out] = ??? + + private trait IsRationalImpl[P] { + type Out + } + private trait IsRationalImplDefault { + type Aux[P, O] = IsRationalImpl[P] { type Out = O } + implicit def isRationalFalse[P]: Aux[P, false] = + new IsRationalImpl[P] { + type Out = false + } + } + private object IsRationalImpl extends IsRationalImplDefault { + implicit def isRationalTrue[N, D]: Aux[Rational[N, D], true] = + new IsRationalImpl[Rational[N, D]] { + type Out = true + } + } + + trait IsRationalOpId + type IsRational[P] = OpMacro[IsRationalOpId, P, W.`0`.T, W.`0`.T] + + implicit def doIsRational[P, T](implicit + tst: IsRationalImpl.Aux[P, T]): OpIntercept.Aux[IsRational[P], T] = ??? + + trait ToRationalOpId + type ToRational[P] = OpMacro[ToRationalOpId, P, W.`0`.T, W.`0`.T] + + implicit def toRationalFromRat[ + N <: XInt, D <: XInt, + SN <: XInt, SD <: XInt]( + implicit + sim: OpAuxGen[Simplify[Rational[N, D]], Rational[SN, SD]] + ): OpIntercept.Aux[ToRational[Rational[N, D]], Rational[SN, SD]] = + new OpIntercept[ToRational[Rational[N, D]]] { + type Out = Rational[SN, SD] + val value: Out = new Rational[SN, SD] {} + } + + implicit def toRationalFromInt[N, One](implicit + one: OpAuxGen[AlignType[1, N], One]): OpIntercept.Aux[ToRational[N], Rational[N, One]] = + new OpIntercept[ToRational[N]] { + type Out = Rational[N, One] + val value: Out = new Rational[N, One] {} + } + + implicit def doRationalNegate[N, D, NN](implicit + neg: OpAuxGen[Negate[N], NN]): OpIntercept.Aux[Negate[Rational[N, D]], Rational[NN, D]] = + new OpIntercept[Negate[Rational[N, D]]] { + type Out = Rational[NN, D] + val value: Out = new Rational[NN, D] {} + } + + implicit def doRationalAdd[ + LHS, RHS, + LN, LD, + RN, RD, + LNRD, RNLD, + N, D, + SN, SD]( + implicit + rat: Require[IsRational[LHS] || IsRational[RHS]], + lhs: OpAuxGen[ToRational[LHS], Rational[LN, LD]], + rhs: OpAuxGen[ToRational[RHS], Rational[RN, RD]], + ev0: OpAuxGen[LN * RD, LNRD], + ev1: OpAuxGen[RN * LD, RNLD], + ev2: OpAuxGen[LNRD + RNLD, N], + ev3: OpAuxGen[LD * RD, D], + ev4: OpAuxGen[Simplify[Rational[N, D]], Rational[SN, SD]], + ): OpIntercept.Aux[LHS + RHS, Rational[SN, SD]] = + new OpIntercept[LHS + RHS] { + type Out = Rational[SN, SD] + val value: Out = new Rational[SN, SD] {} + } + + implicit def doRationalSubtract[ + LHS, RHS, + LN, LD, + RN, RD, RNN, + SN, SD]( + implicit + rat: Require[IsRational[LHS] || IsRational[RHS]], + lhs: OpAuxGen[ToRational[LHS], Rational[LN, LD]], + rhs: OpAuxGen[ToRational[RHS], Rational[RN, RD]], + neg: OpAuxGen[Negate[RN], RNN], + add: OpAuxGen[Rational[LN, LD] + Rational[RNN, RD], Rational[SN, SD]] + ): OpIntercept.Aux[LHS - RHS, Rational[SN, SD]] = + new OpIntercept[LHS - RHS] { + type Out = Rational[SN, SD] + val value: Out = new Rational[SN, SD] {} + } + + implicit def doRationalMultiply[ + LHS, RHS, + LN, LD, + RN, RD, + N, D, + SN, SD]( + implicit + rat: Require[IsRational[LHS] || IsRational[RHS]], + lhs: OpAuxGen[ToRational[LHS], Rational[LN, LD]], + rhs: OpAuxGen[ToRational[RHS], Rational[RN, RD]], + ev0: OpAuxGen[LN * RN, N], + ev1: OpAuxGen[LD * RD, D], + ev2: OpAuxGen[Simplify[Rational[N, D]], Rational[SN, SD]] + ): OpIntercept.Aux[LHS * RHS, Rational[SN, SD]] = + new OpIntercept[LHS * RHS] { + type Out = Rational[SN, SD] + val value: Out = new Rational[SN, SD] {} + } + + implicit def doRationalDivide[ + LHS, RHS, + LN, LD, + RN, RD, + SN, SD]( + implicit + rat: Require[IsRational[LHS] || IsRational[RHS]], + lhs: OpAuxGen[ToRational[LHS], Rational[LN, LD]], + rhs: OpAuxGen[ToRational[RHS], Rational[RN, RD]], + mul: OpAuxGen[Rational[LN, LD] * Rational[RD, RN], Rational[SN, SD]] + ): OpIntercept.Aux[LHS / RHS, Rational[SN, SD]] = + new OpIntercept[LHS / RHS] { + type Out = Rational[SN, SD] + val value: Out = new Rational[SN, SD] {} + } + + trait GCDOpId + type GCD[A, B] = OpMacro[GCDOpId, A, B, W.`0`.T] + + private type gcdErrorMsg = W.`"GCD requires positive integral arguments"`.T + + implicit def doGCDforBasisCase[A, B, Rem](implicit + ev0: RequireMsg[IsIntegral[A] && IsIntegral[B] && (A >= B) && IsPositive[B], gcdErrorMsg], + ev1: OpAuxGen[A % B, Rem], + ev2: Require[IsZero[Rem]]): OpIntercept.Aux[GCD[A, B], B] = ??? + + implicit def doGCDforAgeB[A, B, Rem, D](implicit + ev0: RequireMsg[IsIntegral[A] && IsIntegral[B] && (A >= B) && IsPositive[B], gcdErrorMsg], + ev1: OpAuxGen[A % B, Rem], + ev2: Require[IsNonZero[Rem]], + ev3: OpAuxGen[GCD[B, Rem], D]): OpIntercept.Aux[GCD[A, B], D] = ??? + + implicit def doGCDforAltB[A, B, Rem, D](implicit + ev0: RequireMsg[IsIntegral[A] && IsIntegral[B] && (A < B) && IsPositive[A], gcdErrorMsg], + ev1: OpAuxGen[GCD[B, A], D]): OpIntercept.Aux[GCD[A, B], D] = ??? + + trait SimplifyOpId + type Simplify[F] = OpMacro[SimplifyOpId, F, W.`0`.T, W.`0`.T] + + private type simplifyErrorMsg = W.`"Simplify requires non-zero denominator"`.T + + implicit def doSimplifyPositive[N, D, C, SN, SD](implicit + pos: RequireMsg[IsPositive[N] && IsPositive[D], simplifyErrorMsg], + gcd: OpAuxGen[GCD[N, D], C], + n: OpAuxGen[N / C, SN], + d: OpAuxGen[D / C, SD] + ): OpIntercept.Aux[Simplify[Rational[N, D]], Rational[SN, SD]] = + new OpIntercept[Simplify[Rational[N, D]]] { + type Out = Rational[SN, SD] + val value = new Rational[SN, SD] {} + } + + implicit def doSimplifyNegative[N, D, F, SNF, SN, SD](implicit + neg: RequireMsg[IsNegative[N] && IsPositive[D], simplifyErrorMsg], + ev1: OpAuxGen[Negate[Rational[N, D]], F], + ev2: OpAuxGen[Simplify[F], SNF], + ev3: OpAuxGen[Negate[SNF], Rational[SN, SD]] + ): OpIntercept.Aux[Simplify[Rational[N, D]], Rational[SN, SD]] = + new OpIntercept[Simplify[Rational[N, D]]] { + type Out = Rational[SN, SD] + val value = new Rational[SN, SD] {} + } + + implicit def doSimplifyZero[Z, D](implicit + zro: RequireMsg[IsZero[Z] && IsPositive[D], simplifyErrorMsg], + v1: AlignType[1, D] + ): OpIntercept.Aux[Simplify[Rational[Z, D]], Rational[Z, v1.Out]] = + new OpIntercept[Simplify[Rational[Z, D]]] { + type Out = Rational[Z, v1.Out] + val value = new Rational[Z, v1.Out] {} + } + + implicit def doSimplifyNegDenom[N, D, NN, ND, SN, SD](implicit + neg: RequireMsg[IsNegative[D], simplifyErrorMsg], + nn: OpAuxGen[Negate[N], NN], + nd: OpAuxGen[Negate[D], ND], + sf: OpAuxGen[Simplify[Rational[NN, ND]], Rational[SN, SD]] + ): OpIntercept.Aux[Simplify[Rational[N, D]], Rational[SN, SD]] = + new OpIntercept[Simplify[Rational[N, D]]] { + type Out = Rational[SN, SD] + val value = new Rational[SN, SD] {} + } +} diff --git a/src/test/scala/singleton/ops/OpInterceptSpec.scala b/src/test/scala/singleton/ops/OpInterceptSpec.scala new file mode 100644 index 00000000..883bda45 --- /dev/null +++ b/src/test/scala/singleton/ops/OpInterceptSpec.scala @@ -0,0 +1,73 @@ +package singleton.ops + +import org.scalacheck.Properties +import shapeless.test.illTyped +import singleton.TestUtils._ + +class OpInterceptSpec extends Properties("OpInterceptSpec") { + + trait Vec[A0, A1] { + def show(implicit a0 : Id[A0], a1 : Id[A1]) : String = s"Vec[${a0.value}, ${a1.value}]" + } + + implicit def `Vec+`[VL0, VL1, VR0, VR1]( + implicit + opL : VL0 + VR0, + opR : VL1 + VR1 + ) : OpIntercept.Aux[Vec[VL0, VL1] + Vec[VR0, VR1], Vec[opL.Out, opR.Out]] = //Vec is not a singleton value, so we need to instantiate OpIntercept + new OpIntercept[Vec[VL0, VL1] + Vec[VR0, VR1]] { + type Out = Vec[opL.Out, opR.Out] + val value : Out = new Vec[opL.Out, opR.Out]{} + } + + implicit def `Vec==`[VL0, VL1, VR0, VR1]( + implicit + op : (VL0 == VR0) && (VL1 == VR1) + ) : OpIntercept.Aux[Vec[VL0, VL1] == Vec[VR0, VR1], op.Out] = ??? //No need to instantiate when a singleton value is returned + + property("Custom Vec Equality OK") = { + val eq1 = shapeless.the[Vec[W.`1`.T, W.`2`.T] == Vec[W.`1`.T, W.`2`.T]] + val eq2 = shapeless.the[Vec[W.`1`.T, W.`2`.T] == Vec[W.`1`.T, W.`1`.T]] + implicitly[eq1.Out =:= W.`true`.T] + implicitly[eq2.Out =:= W.`false`.T] + eq1.value == true + } + + property("Custom Vec Addition OK") = { + val add2 = shapeless.the[Vec[W.`1`.T, W.`2`.T] + Vec[W.`3`.T, W.`8`.T]] + val add3 = shapeless.the[Vec[W.`1`.T, W.`2`.T] + Vec[W.`3`.T, W.`8`.T] + Vec[W.`20`.T, W.`20`.T]] + implicitly[add2.Out =:= Vec[W.`4`.T, W.`10`.T]] + implicitly[add3.Out =:= Vec[W.`24`.T, W.`30`.T]] + val add23 = shapeless.the[add2.Out + add3.Out] + implicitly[add23.Out =:= Vec[W.`28`.T, W.`40`.T]] + add2.value.show == "Vec[4, 10]" + } + + + trait FibId + type Fib[P] = impl.OpMacro[FibId, P, W.`0`.T, W.`0`.T] + implicit def doFib[P]( + implicit + op : ITE[P == W.`0`.T, W.`0`.T, ITE[P == W.`1`.T, W.`1`.T, Fib[P - W.`1`.T] + Fib[P - W.`2`.T]]] + ) : OpIntercept.Aux[Fib[P], op.Out] = ??? //No need to instantiate when a singleton value is returned + + property("Custom Fibonacci Op OK") = { + val fib4 = shapeless.the[Fib[W.`4`.T]] + implicitly[fib4.Out =:= W.`3`.T] + val fib10 = shapeless.the[Fib[W.`10`.T]] + implicitly[fib10.Out =:= W.`55`.T] + fib10.value == 55 + } + + + trait FooOpId + type FooOp[C, M] = impl.OpMacro[FooOpId, C, M, W.`0`.T] + implicit def FooOp[C, M]( + implicit + r : RequireMsg[C, M] + ) : OpIntercept[FooOp[C, M]] = ??? + + property("Error Message Propagation") = wellTyped { + illTyped("""shapeless.the[FooOp[W.`false`.T, W.`"this is a test"`.T]]""", "this is a test") + } +}