diff options
author | Adriaan Moors <adriaan.moors@typesafe.com> | 2013-03-05 09:08:58 -0800 |
---|---|---|
committer | Adriaan Moors <adriaan.moors@typesafe.com> | 2013-03-05 09:08:58 -0800 |
commit | 1176035f271821021c36d1b3cab6b2888e99524d (patch) | |
tree | 03008bb9d5ecc30512c54145a48e1dd045578480 /src/compiler | |
parent | 773f6a8df9ef95852918a706f3f19ebf0431baa8 (diff) | |
parent | f482d5bdd0722e54cb3cfc2219df93da5f435bac (diff) | |
download | scala-1176035f271821021c36d1b3cab6b2888e99524d.tar.gz scala-1176035f271821021c36d1b3cab6b2888e99524d.tar.bz2 scala-1176035f271821021c36d1b3cab6b2888e99524d.zip |
Merge pull request #2193 from adriaanm/patmat-refactor
merge 2.10.1 into 2.10.x
Diffstat (limited to 'src/compiler')
9 files changed, 342 insertions, 303 deletions
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala index 9af4800a70..22eabb6d6f 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala @@ -287,236 +287,9 @@ trait Logic extends Debugging { def findModelFor(f: Formula): Model def findAllModelsFor(f: Formula): List[Model] } - - trait CNF extends PropositionalLogic { - - /** Override Array creation for efficiency (to not go through reflection). */ - private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] { - def runtimeClass: java.lang.Class[Clause] = classOf[Clause] - final override def newArray(len: Int): Array[Clause] = new Array[Clause](len) - } - - import scala.collection.mutable.ArrayBuffer - type FormulaBuilder = ArrayBuffer[Clause] - def formulaBuilder = ArrayBuffer[Clause]() - def formulaBuilderSized(init: Int) = new ArrayBuffer[Clause](init) - def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f - def toFormula(buff: FormulaBuilder): Formula = buff - - // CNF: a formula is a conjunction of clauses - type Formula = FormulaBuilder - def formula(c: Clause*): Formula = ArrayBuffer(c: _*) - - type Clause = Set[Lit] - // a clause is a disjunction of distinct literals - def clause(l: Lit*): Clause = l.toSet - - type Lit - def Lit(sym: Sym, pos: Boolean = true): Lit - - def andFormula(a: Formula, b: Formula): Formula = a ++ b - def simplifyFormula(a: Formula): Formula = a.distinct - - private def merge(a: Clause, b: Clause) = a ++ b - - // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big - // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding) - def eqFreePropToSolvable(p: Prop): Formula = { - def negationNormalFormNot(p: Prop, budget: Int): Prop = - if (budget <= 0) throw AnalysisBudget.exceeded - else p match { - case And(a, b) => Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Or(a, b) => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Not(p) => negationNormalForm(p, budget - 1) - case True => False - case False => True - case s: Sym => Not(s) - } - - def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop = - if (budget <= 0) throw AnalysisBudget.exceeded - else p match { - case And(a, b) => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Or(a, b) => Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Not(negated) => negationNormalFormNot(negated, budget - 1) - case True - | False - | (_ : Sym) => p - } - - val TrueF = formula() - val FalseF = formula(clause()) - def lit(s: Sym) = formula(clause(Lit(s))) - def negLit(s: Sym) = formula(clause(Lit(s, false))) - - def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = { - def distribute(a: Formula, b: Formula, budget: Int): Formula = - if (budget <= 0) throw AnalysisBudget.exceeded - else - (a, b) match { - // true \/ _ = true - // _ \/ true = true - case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF - // lit \/ lit - case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0))) - // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) - // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) - case (cs, ds) => - val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs) - big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size))) - } - - if (budget <= 0) throw AnalysisBudget.exceeded - - p match { - case True => TrueF - case False => FalseF - case s: Sym => lit(s) - case Not(s: Sym) => negLit(s) - case And(a, b) => - val cnfA = conjunctiveNormalForm(a, budget - 1) - val cnfB = conjunctiveNormalForm(b, budget - cnfA.size) - cnfA ++ cnfB - case Or(a, b) => - val cnfA = conjunctiveNormalForm(a) - val cnfB = conjunctiveNormalForm(b) - distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size)) - } - } - - val start = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null - val res = conjunctiveNormalForm(negationNormalForm(p)) - - if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start) - - // - if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1 - -// debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res)) - res - } - } - - trait DPLLSolver extends CNF { - // a literal is a (possibly negated) variable - def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos) - class Lit(val sym: Sym, val pos: Boolean) { - override def toString = if (!pos) "-"+ sym.toString else sym.toString - override def equals(o: Any) = o match { - case o: Lit => (o.sym eq sym) && (o.pos == pos) - case _ => false - } - override def hashCode = sym.hashCode + pos.hashCode - - def unary_- = Lit(sym, !pos) - } - - def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n") - - // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat) - val EmptyModel = Map.empty[Sym, Boolean] - val NoModel: Model = null - - // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??) - def findAllModelsFor(f: Formula): List[Model] = { - val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet - // debug.patmat("vars "+ vars) - // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True) - def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*) - - def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]= - if (recursionDepthAllowed == 0) models - else { - debug.patmat("find all models for\n"+ cnfString(f)) - val model = findModelFor(f) - // if we found a solution, conjunct the formula with the model's negation and recurse - if (model ne NoModel) { - val unassigned = (vars -- model.keySet).toList - debug.patmat("unassigned "+ unassigned +" in "+ model) - def force(lit: Lit) = { - val model = withLit(findModelFor(dropUnit(f, lit)), lit) - if (model ne NoModel) List(model) - else Nil - } - val forced = unassigned flatMap { s => - force(Lit(s, true)) ++ force(Lit(s, false)) - } - debug.patmat("forced "+ forced) - val negated = negateModel(model) - findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) - } - else models - } - - findAllModels(f, Nil) - } - - private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) - private def dropUnit(f: Formula, unitLit: Lit): Formula = { - val negated = -unitLit - // drop entire clauses that are trivially true - // (i.e., disjunctions that contain the literal we're making true in the returned model), - // and simplify clauses by dropping the negation of the literal we're making true - // (since False \/ X == X) - val dropped = formulaBuilderSized(f.size) - for { - clause <- f - if !(clause contains unitLit) - } dropped += (clause - negated) - dropped - } - - def findModelFor(f: Formula): Model = { - @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b - - debug.patmat("DPLL\n"+ cnfString(f)) - - val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null - - val satisfiableWithModel: Model = - if (f isEmpty) EmptyModel - else if(f exists (_.isEmpty)) NoModel - else f.find(_.size == 1) match { - case Some(unitClause) => - val unitLit = unitClause.head - // debug.patmat("unit: "+ unitLit) - withLit(findModelFor(dropUnit(f, unitLit)), unitLit) - case _ => - // partition symbols according to whether they appear in positive and/or negative literals - val pos = new mutable.HashSet[Sym]() - val neg = new mutable.HashSet[Sym]() - f.foreach{_.foreach{ lit => - if (lit.pos) pos += lit.sym else neg += lit.sym - }} - // appearing in both positive and negative - val impures = pos intersect neg - // appearing only in either positive/negative positions - val pures = (pos ++ neg) -- impures - - if (pures nonEmpty) { - val pureSym = pures.head - // turn it back into a literal - // (since equality on literals is in terms of equality - // of the underlying symbol and its positivity, simply construct a new Lit) - val pureLit = Lit(pureSym, pos(pureSym)) - // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) - val simplified = f.filterNot(_.contains(pureLit)) - withLit(findModelFor(simplified), pureLit) - } else { - val split = f.head.head - // debug.patmat("split: "+ split) - orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) - } - } - - if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start) - - satisfiableWithModel - } - } } -trait ScalaLogic extends Logic { self: PatternMatching => +trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis { trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis { type Type = global.Type type Tree = global.Tree diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala index ed990105fd..d9f93f27b6 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala @@ -125,23 +125,15 @@ trait TreeAndTypeAnalysis extends Debugging { } } -trait MatchAnalysis extends TreeAndTypeAnalysis { self: PatternMatching => - import PatternMatchingStats._ - import global.{Tree, Type, Symbol, CaseDef, atPos, - Select, Block, ThisType, SingleType, NoPrefix, NoType, definitions, needsOuterTest, - ConstantType, Literal, Constant, gen, This, analyzer, EmptyTree, map2, NoSymbol, Traverser, - Function, Typed, treeInfo, DefTree, ValDef, nme, appliedType, Name, WildcardType, Ident, TypeRef, - UniqueType, RefinedType, currentUnit, SingletonType, singleType, ModuleClassSymbol, - nestedMemberType, TypeMap, EmptyScope, Apply, If, Bind, lub, Alternative, deriveCaseDef, Match, MethodType, LabelDef, TypeTree, Throw, newTermName} - - import definitions._ - import analyzer.{Typer, ErrorUtils, formalTypes} +trait MatchApproximation extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking { + import global.{Tree, Type, NoType, Symbol, NoSymbol, ConstantType, Literal, Constant, Ident, UniqueType, RefinedType, EmptyScope} + import global.definitions.{ListClass, NilModule} /** * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types) * */ - trait TreeMakerApproximation extends TreeMakers with PropositionalLogic with TreesAndTypesDomain with CheckableTreeAndTypeAnalysis { self: CodegenCore => + trait MatchApproximator extends TreeMakers with TreesAndTypesDomain { object Test { var currId = 0 } @@ -348,7 +340,14 @@ trait MatchAnalysis extends TreeAndTypeAnalysis { self: PatternMatching => } } - trait SymbolicMatchAnalysis extends TreeMakerApproximation { self: CodegenCore => +} + +trait MatchAnalysis extends MatchApproximation { + import PatternMatchingStats._ + import global.{Tree, Type, Symbol, NoSymbol, Ident, Select} + import global.definitions.{isPrimitiveValueClass, ConsClass, isTupleSymbol} + + trait MatchAnalyzer extends MatchApproximator { def uncheckedWarning(pos: Position, msg: String) = global.currentUnit.uncheckedWarning(pos, msg) def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}") @@ -498,7 +497,7 @@ trait MatchAnalysis extends TreeAndTypeAnalysis { self: PatternMatching => // a way to construct a value that will make the match fail: a constructor invocation, a constant, an object of some type) class CounterExample { - protected[SymbolicMatchAnalysis] def flattenConsArgs: List[CounterExample] = Nil + protected[MatchAnalyzer] def flattenConsArgs: List[CounterExample] = Nil def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample } case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString } @@ -513,11 +512,11 @@ trait MatchAnalysis extends TreeAndTypeAnalysis { self: PatternMatching => } } case class ListExample(ctorArgs: List[CounterExample]) extends CounterExample { - protected[SymbolicMatchAnalysis] override def flattenConsArgs: List[CounterExample] = ctorArgs match { + protected[MatchAnalyzer] override def flattenConsArgs: List[CounterExample] = ctorArgs match { case hd :: tl :: Nil => hd :: tl.flattenConsArgs case _ => Nil } - protected[SymbolicMatchAnalysis] lazy val elems = flattenConsArgs + protected[MatchAnalyzer] lazy val elems = flattenConsArgs override def coveredBy(other: CounterExample): Boolean = other match { @@ -691,5 +690,18 @@ trait MatchAnalysis extends TreeAndTypeAnalysis { self: PatternMatching => // this is the variable we want a counter example for VariableAssignment(scrutVar).toCounterExample() } + + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = { + if (!suppression.unreachable) { + unreachableCase(prevBinder, cases, pt) foreach { caseIndex => + reportUnreachable(cases(caseIndex).last.pos) + } + } + if (!suppression.exhaustive) { + val counterExamples = exhaustive(prevBinder, cases, pt) + if (counterExamples.nonEmpty) + reportMissingCases(prevBinder.pos, counterExamples) + } + } } } diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchCodeGen.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchCodeGen.scala index ce19d9cba8..57fab4eafa 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchCodeGen.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchCodeGen.scala @@ -17,7 +17,7 @@ import scala.reflect.internal.util.NoPosition * We have two modes in which to emit trees: optimized (the default) * and pure (aka "virtualized": match is parametric in its monad). */ -trait MatchCodeGen { self: PatternMatching => +trait MatchCodeGen extends Interface { import PatternMatchingStats._ import global.{nme, treeInfo, definitions, gen, Tree, Type, Symbol, NoSymbol, appliedType, NoType, MethodType, newTermName, Name, diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala index c14b4ebc3b..dcf2413b15 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala @@ -19,7 +19,7 @@ import scala.reflect.internal.util.NoPosition * * TODO: split out match analysis */ -trait MatchOptimization { self: PatternMatching => +trait MatchOptimization extends MatchTreeMaking with MatchAnalysis { import PatternMatchingStats._ import global.{Tree, Type, Symbol, NoSymbol, CaseDef, atPos, ConstantType, Literal, Constant, gen, EmptyTree, @@ -30,7 +30,7 @@ trait MatchOptimization { self: PatternMatching => //// - trait CommonSubconditionElimination extends TreeMakerApproximation { self: OptimizedCodegen => + trait CommonSubconditionElimination extends OptimizedCodegen with MatchApproximator { /** a flow-sensitive, generalised, common sub-expression elimination * reuse knowledge from performed tests * the only sub-expressions we consider are the conditions and results of the three tests (type, type&equality, equality) @@ -205,19 +205,19 @@ trait MatchOptimization { self: PatternMatching => //// DCE - trait DeadCodeElimination extends TreeMakers { self: CodegenCore => - // TODO: non-trivial dead-code elimination - // e.g., the following match should compile to a simple instanceof: - // case class Ident(name: String) - // for (Ident(name) <- ts) println(name) - def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = { - // do minimal DCE - cases - } - } +// trait DeadCodeElimination extends TreeMakers { +// // TODO: non-trivial dead-code elimination +// // e.g., the following match should compile to a simple instanceof: +// // case class Ident(name: String) +// // for (Ident(name) <- ts) println(name) +// def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = { +// // do minimal DCE +// cases +// } +// } //// SWITCHES -- TODO: operate on Tests rather than TreeMakers - trait SwitchEmission extends TreeMakers with OptimizedMatchMonadInterface { self: CodegenCore => + trait SwitchEmission extends TreeMakers with OptimizedMatchMonadInterface { import treeInfo.isGuardedCase abstract class SwitchMaker { @@ -589,26 +589,12 @@ trait MatchOptimization { self: PatternMatching => } } - - - - trait MatchOptimizations extends CommonSubconditionElimination - with DeadCodeElimination - with SwitchEmission - with OptimizedCodegen - with SymbolicMatchAnalysis - with DPLLSolver { self: TreeMakers => - override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = { - unreachableCase(prevBinder, cases, pt) foreach { caseIndex => - reportUnreachable(cases(caseIndex).last.pos) - } - if (!unchecked) { - val counterExamples = exhaustive(prevBinder, cases, pt) - if (counterExamples.nonEmpty) - reportMissingCases(prevBinder.pos, counterExamples) - } - - val optCases = doCSE(prevBinder, doDCE(prevBinder, cases, pt), pt) + trait MatchOptimizer extends OptimizedCodegen + with SwitchEmission + with CommonSubconditionElimination { + override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree]) = { + // TODO: do CSE on result of doDCE(prevBinder, cases, pt) + val optCases = doCSE(prevBinder, cases, pt) val toHoist = ( for (treeMakers <- optCases) yield treeMakers.collect{case tm: ReusedCondTreeMaker => tm.treesToHoist} diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTranslation.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTranslation.scala index 5d11fb6459..90c52e3eb6 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTranslation.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTranslation.scala @@ -24,7 +24,7 @@ trait MatchTranslation { self: PatternMatching => repeatedToSeq, isRepeatedParamType, getProductArgs} import global.analyzer.{ErrorUtils, formalTypes} - trait MatchTranslator extends MatchMonadInterface { self: TreeMakers with CodegenCore => + trait MatchTranslator extends TreeMakers { import typer.context // Why is it so difficult to say "here's a name and a context, give me any diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala index c9285f9229..202f3444f8 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala @@ -18,21 +18,26 @@ import scala.reflect.internal.util.NoPosition * The IR is mostly concerned with sequencing, substitution, and rendering all necessary conditions, * mostly agnostic to whether we're in optimized/pure (virtualized) mode. */ -trait MatchTreeMaking { self: PatternMatching => +trait MatchTreeMaking extends MatchCodeGen with Debugging { import PatternMatchingStats._ import global.{Tree, Type, Symbol, CaseDef, atPos, settings, Select, Block, ThisType, SingleType, NoPrefix, NoType, needsOuterTest, ConstantType, Literal, Constant, gen, This, EmptyTree, map2, NoSymbol, Traverser, - Function, Typed, treeInfo, TypeRef, DefTree} + Function, Typed, treeInfo, TypeRef, DefTree, Ident, nme} import global.definitions.{SomeClass, AnyRefClass, UncheckedClass, BooleanClass} + final case class Suppression(exhaustive: Boolean, unreachable: Boolean) + object Suppression { + val NoSuppression = Suppression(false, false) + } + /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// // the making of the trees /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// - trait TreeMakers extends TypedSubstitution { self: CodegenCore => - def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = - (cases, Nil) + trait TreeMakers extends TypedSubstitution with CodegenCore { + def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree]) + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit def emitSwitch(scrut: Tree, scrutSym: Symbol, cases: List[List[TreeMaker]], pt: Type, matchFailGenOverride: Option[Tree => Tree], unchecked: Boolean): Option[Tree] = None @@ -522,18 +527,24 @@ trait MatchTreeMaking { self: PatternMatching => def matchFailGen = (matchFailGenOverride orElse Some(CODE.MATCHERROR(_: Tree))) debug.patmat("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}"))) - val (unchecked, requireSwitch) = - if (settings.XnoPatmatAnalysis.value) (true, false) + val (suppression, requireSwitch): (Suppression, Boolean) = + if (settings.XnoPatmatAnalysis.value) (Suppression.NoSuppression, false) else scrut match { - case Typed(_, tpt) => - (tpt.tpe hasAnnotation UncheckedClass, - // matches with two or fewer cases need not apply for switchiness (if-then-else will do) - treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0) + case Typed(tree, tpt) => + val suppressExhaustive = tpt.tpe hasAnnotation UncheckedClass + val supressUnreachable = tree match { + case Ident(name) if name startsWith nme.CHECK_IF_REFUTABLE_STRING => true // SI-7183 don't warn for withFilter's that turn out to be irrefutable. + case _ => false + } + val suppression = Suppression(suppressExhaustive, supressUnreachable) + // matches with two or fewer cases need not apply for switchiness (if-then-else will do) + val requireSwitch = treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0 + (suppression, requireSwitch) case _ => - (false, false) + (Suppression.NoSuppression, false) } - emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, unchecked).getOrElse{ + emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, suppression.exhaustive).getOrElse{ if (requireSwitch) typer.context.unit.warning(scrut.pos, "could not emit switch for @switch annotated match") if (casesNoSubstOnly nonEmpty) { @@ -550,7 +561,9 @@ trait MatchTreeMaking { self: PatternMatching => }) None else matchFailGen - val (cases, toHoist) = optimizeCases(scrutSym, casesNoSubstOnly, pt, unchecked) + analyzeCases(scrutSym, casesNoSubstOnly, pt, suppression) + + val (cases, toHoist) = optimizeCases(scrutSym, casesNoSubstOnly, pt) val matchRes = codegen.matcher(scrut, scrutSym, pt)(cases map combineExtractors, synthCatchAll) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala index 07eed2cd94..df4e699620 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala @@ -34,13 +34,14 @@ import scala.reflect.internal.util.Position * - recover GADT typing by locally inserting implicit witnesses to type equalities derived from the current case, and considering these witnesses during subtyping (?) * - recover exhaustivity/unreachability of user-defined extractors by partitioning the types they match on using an HList or similar type-level structure */ -trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL +trait PatternMatching extends Transform with TypingTransformers with Debugging with Interface with MatchTranslation with MatchTreeMaking with MatchCodeGen with ScalaLogic + with Solving with MatchAnalysis with MatchOptimization { import global._ @@ -78,15 +79,20 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - class PureMatchTranslator(val typer: analyzer.Typer, val matchStrategy: Tree) extends MatchTranslator with TreeMakers with PureCodegen - class OptimizingMatchTranslator(val typer: analyzer.Typer) extends MatchTranslator with TreeMakers with MatchOptimizations + class PureMatchTranslator(val typer: analyzer.Typer, val matchStrategy: Tree) extends MatchTranslator with PureCodegen { + def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type) = (cases, Nil) + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = {} + } + + class OptimizingMatchTranslator(val typer: analyzer.Typer) extends MatchTranslator + with MatchOptimizer + with MatchAnalyzer + with Solver } -trait HasGlobal { +trait Debugging { val global: Global -} -trait Debugging extends HasGlobal { // TODO: the inliner fails to inline the closures to debug.patmat unless the method is nested in an object object debug { val printPatmat = global.settings.Ypatmatdebug.value @@ -94,7 +100,7 @@ trait Debugging extends HasGlobal { } } -trait Interface { self: ast.TreeDSL with HasGlobal => +trait Interface extends ast.TreeDSL { import global.{newTermName, analyzer, Type, ErrorType, Symbol, Tree} import analyzer.Typer diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala new file mode 100644 index 0000000000..843f831ea1 --- /dev/null +++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala @@ -0,0 +1,242 @@ +/* NSC -- new Scala compiler + * + * Copyright 2011-2013 LAMP/EPFL + * @author Adriaan Moors + */ + +package scala.tools.nsc.transform.patmat + +import scala.collection.mutable +import scala.reflect.internal.util.Statistics + +// naive CNF translation and simple DPLL solver +trait Solving extends Logic { + import PatternMatchingStats._ + trait CNF extends PropositionalLogic { + + /** Override Array creation for efficiency (to not go through reflection). */ + private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] { + def runtimeClass: java.lang.Class[Clause] = classOf[Clause] + final override def newArray(len: Int): Array[Clause] = new Array[Clause](len) + } + + import scala.collection.mutable.ArrayBuffer + type FormulaBuilder = ArrayBuffer[Clause] + def formulaBuilder = ArrayBuffer[Clause]() + def formulaBuilderSized(init: Int) = new ArrayBuffer[Clause](init) + def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f + def toFormula(buff: FormulaBuilder): Formula = buff + + // CNF: a formula is a conjunction of clauses + type Formula = FormulaBuilder + def formula(c: Clause*): Formula = ArrayBuffer(c: _*) + + type Clause = Set[Lit] + // a clause is a disjunction of distinct literals + def clause(l: Lit*): Clause = l.toSet + + type Lit + def Lit(sym: Sym, pos: Boolean = true): Lit + + def andFormula(a: Formula, b: Formula): Formula = a ++ b + def simplifyFormula(a: Formula): Formula = a.distinct + + private def merge(a: Clause, b: Clause) = a ++ b + + // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big + // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding) + def eqFreePropToSolvable(p: Prop): Formula = { + def negationNormalFormNot(p: Prop, budget: Int): Prop = + if (budget <= 0) throw AnalysisBudget.exceeded + else p match { + case And(a, b) => Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) + case Or(a, b) => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) + case Not(p) => negationNormalForm(p, budget - 1) + case True => False + case False => True + case s: Sym => Not(s) + } + + def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop = + if (budget <= 0) throw AnalysisBudget.exceeded + else p match { + case And(a, b) => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) + case Or(a, b) => Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) + case Not(negated) => negationNormalFormNot(negated, budget - 1) + case True + | False + | (_ : Sym) => p + } + + val TrueF = formula() + val FalseF = formula(clause()) + def lit(s: Sym) = formula(clause(Lit(s))) + def negLit(s: Sym) = formula(clause(Lit(s, false))) + + def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = { + def distribute(a: Formula, b: Formula, budget: Int): Formula = + if (budget <= 0) throw AnalysisBudget.exceeded + else + (a, b) match { + // true \/ _ = true + // _ \/ true = true + case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF + // lit \/ lit + case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0))) + // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) + // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) + case (cs, ds) => + val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs) + big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size))) + } + + if (budget <= 0) throw AnalysisBudget.exceeded + + p match { + case True => TrueF + case False => FalseF + case s: Sym => lit(s) + case Not(s: Sym) => negLit(s) + case And(a, b) => + val cnfA = conjunctiveNormalForm(a, budget - 1) + val cnfB = conjunctiveNormalForm(b, budget - cnfA.size) + cnfA ++ cnfB + case Or(a, b) => + val cnfA = conjunctiveNormalForm(a) + val cnfB = conjunctiveNormalForm(b) + distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size)) + } + } + + val start = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null + val res = conjunctiveNormalForm(negationNormalForm(p)) + + if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start) + + // + if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1 + +// debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res)) + res + } + } + + // simple solver using DPLL + trait Solver extends CNF { + // a literal is a (possibly negated) variable + def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos) + class Lit(val sym: Sym, val pos: Boolean) { + override def toString = if (!pos) "-"+ sym.toString else sym.toString + override def equals(o: Any) = o match { + case o: Lit => (o.sym eq sym) && (o.pos == pos) + case _ => false + } + override def hashCode = sym.hashCode + pos.hashCode + + def unary_- = Lit(sym, !pos) + } + + def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n") + + // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat) + val EmptyModel = Map.empty[Sym, Boolean] + val NoModel: Model = null + + // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??) + def findAllModelsFor(f: Formula): List[Model] = { + val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet + // debug.patmat("vars "+ vars) + // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True) + def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*) + + def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]= + if (recursionDepthAllowed == 0) models + else { + debug.patmat("find all models for\n"+ cnfString(f)) + val model = findModelFor(f) + // if we found a solution, conjunct the formula with the model's negation and recurse + if (model ne NoModel) { + val unassigned = (vars -- model.keySet).toList + debug.patmat("unassigned "+ unassigned +" in "+ model) + def force(lit: Lit) = { + val model = withLit(findModelFor(dropUnit(f, lit)), lit) + if (model ne NoModel) List(model) + else Nil + } + val forced = unassigned flatMap { s => + force(Lit(s, true)) ++ force(Lit(s, false)) + } + debug.patmat("forced "+ forced) + val negated = negateModel(model) + findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) + } + else models + } + + findAllModels(f, Nil) + } + + private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) + private def dropUnit(f: Formula, unitLit: Lit): Formula = { + val negated = -unitLit + // drop entire clauses that are trivially true + // (i.e., disjunctions that contain the literal we're making true in the returned model), + // and simplify clauses by dropping the negation of the literal we're making true + // (since False \/ X == X) + val dropped = formulaBuilderSized(f.size) + for { + clause <- f + if !(clause contains unitLit) + } dropped += (clause - negated) + dropped + } + + def findModelFor(f: Formula): Model = { + @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b + + debug.patmat("DPLL\n"+ cnfString(f)) + + val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null + + val satisfiableWithModel: Model = + if (f isEmpty) EmptyModel + else if(f exists (_.isEmpty)) NoModel + else f.find(_.size == 1) match { + case Some(unitClause) => + val unitLit = unitClause.head + // debug.patmat("unit: "+ unitLit) + withLit(findModelFor(dropUnit(f, unitLit)), unitLit) + case _ => + // partition symbols according to whether they appear in positive and/or negative literals + val pos = new mutable.HashSet[Sym]() + val neg = new mutable.HashSet[Sym]() + f.foreach{_.foreach{ lit => + if (lit.pos) pos += lit.sym else neg += lit.sym + }} + // appearing in both positive and negative + val impures = pos intersect neg + // appearing only in either positive/negative positions + val pures = (pos ++ neg) -- impures + + if (pures nonEmpty) { + val pureSym = pures.head + // turn it back into a literal + // (since equality on literals is in terms of equality + // of the underlying symbol and its positivity, simply construct a new Lit) + val pureLit = Lit(pureSym, pos(pureSym)) + // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) + val simplified = f.filterNot(_.contains(pureLit)) + withLit(findModelFor(simplified), pureLit) + } else { + val split = f.head.head + // debug.patmat("split: "+ split) + orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) + } + } + + if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start) + + satisfiableWithModel + } + } +} diff --git a/src/compiler/scala/tools/nsc/typechecker/Typers.scala b/src/compiler/scala/tools/nsc/typechecker/Typers.scala index 9dde952d25..60e50b517e 100644 --- a/src/compiler/scala/tools/nsc/typechecker/Typers.scala +++ b/src/compiler/scala/tools/nsc/typechecker/Typers.scala @@ -222,8 +222,13 @@ trait Typers extends Modes with Adaptations with Tags { new SubstWildcardMap(tparams).apply(tp) case TypeRef(_, sym, _) if sym.isAliasType => val tp0 = tp.dealias - val tp1 = dropExistential(tp0) - if (tp1 eq tp0) tp else tp1 + if (tp eq tp0) { + debugwarn(s"dropExistential did not progress dealiasing $tp, see SI-7126") + tp + } else { + val tp1 = dropExistential(tp0) + if (tp1 eq tp0) tp else tp1 + } case _ => tp } @@ -1818,7 +1823,9 @@ trait Typers extends Modes with Adaptations with Tags { def pkgObjectWarning(m : Symbol, mdef : ModuleDef, restricted : String) = { val pkgName = mdef.symbol.ownerChain find (_.isPackage) map (_.decodedName) getOrElse mdef.symbol.toString - context.warning(if (m.pos.isDefined) m.pos else mdef.pos, s"${m} should be placed directly in package ${pkgName} instead of package object ${pkgName}. Under some circumstances companion objects and case classes in package objects can fail to recompile. See https://issues.scala-lang.org/browse/SI-5954.") + val pos = if (m.pos.isDefined) m.pos else mdef.pos + debugwarn(s"${m} should be placed directly in package ${pkgName} instead of package object ${pkgName}. Under some circumstances companion objects and case classes in package objects can fail to recompile. See https://issues.scala-lang.org/browse/SI-5954.") + debugwarn(pos.lineContent + (if (pos.isDefined) " " * (pos.column - 1) + "^" else "")) } } |