@@ -710,29 +710,26 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
710
710
711
711
/** Whether the counterexample is satisfiable. The space is flattened and non-empty. */
712
712
def satisfiable (sp : Space ): Boolean = {
713
+ def impossible : Nothing = throw new AssertionError (" `satisfiable` only accepts flattened space." )
714
+
713
715
def genConstraint (space : Space ): List [(Type , Type )] = space match {
714
716
case Prod (tp, unappTp, unappSym, ss, _) =>
715
717
val tps = signature(unappTp, unappSym, ss.length)
716
718
ss.zip(tps).flatMap {
717
719
case (sp : Prod , tp) => sp.tp -> tp :: genConstraint(sp)
718
720
case (Typ (tp1, _), tp2) => tp1 -> tp2 :: Nil
719
- case _ => ??? // impossible
721
+ case _ => impossible
720
722
}
721
723
case Typ (_, _) => Nil
722
- case _ => ??? // impossible
724
+ case _ => impossible
723
725
}
724
726
725
727
def checkConstraint (constrs : List [(Type , Type )])(implicit ctx : Context ): Boolean = {
726
728
val tvarMap = collection.mutable.Map .empty[Symbol , TypeVar ]
727
729
val typeParamMap = new TypeMap () {
728
730
override def apply (tp : Type ): Type = tp match {
729
731
case tref : TypeRef if tref.symbol.is(TypeParam ) =>
730
- if (tvarMap.contains(tref.symbol)) tvarMap(tref.symbol)
731
- else {
732
- val tvar = newTypeVar(tref.underlying.bounds)
733
- tvarMap(tref.symbol) = tvar
734
- tvar
735
- }
732
+ tvarMap.getOrElseUpdate(tref.symbol, newTypeVar(tref.underlying.bounds))
736
733
case tp => mapOver(tp)
737
734
}
738
735
}
@@ -810,10 +807,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
810
807
res
811
808
}
812
809
813
- def checkGADT (tp : Type ): Boolean = {
810
+ /** Whehter counter-examples should be further checked? True for GADTs. */
811
+ def shouldCheckExamples (tp : Type ): Boolean = {
814
812
new TypeAccumulator [Boolean ] {
815
813
override def apply (b : Boolean , tp : Type ): Boolean = tp match {
816
- case tref : TypeRef if tref.symbol.is(TypeParam ) && variance == 0 => true
814
+ case tref : TypeRef if tref.symbol.is(TypeParam ) && variance != 1 => true
817
815
case tp => b || foldOver(b, tp)
818
816
}
819
817
}.apply(false , tp)
@@ -830,7 +828,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
830
828
space
831
829
}).reduce((a, b) => Or (List (a, b)))
832
830
833
- val checkGADTSAT = checkGADT (selTyp)
831
+ val checkGADTSAT = shouldCheckExamples (selTyp)
834
832
835
833
val uncovered =
836
834
flatten(simplify(minus(Typ (selTyp, true ), patternSpace), aggressive = true ))
0 commit comments