From 14a918e4ae69465e401ad443417f79d17965e2ad Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 13 Jul 2010 10:07:25 +0000
Subject: [PATCH] added XP flag
---
src/funcheck/FunCheckPlugin.scala | 4 +++-
src/purescala/Settings.scala | 1 +
src/purescala/Trees.scala | 4 ++--
src/purescala/Z3Solver.scala | 2 +-
4 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 0b998ad30..3e8f65605 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -26,7 +26,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" -P:funcheck:noaxioms Don't generate forall axioms for recursive functions" + "\n" +
" -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
- " -P:funcheck:quiet No info and warning messages from the extensions"
+ " -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
+ " -P:funcheck:XP Enable weird transformations and other bug-producing features"
)
/** Processes the command-line options. */
@@ -41,6 +42,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "quiet" => purescala.Settings.quietExtensions = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "noaxioms" => purescala.Settings.noForallAxioms = true
+ case "XP" => purescala.Settings.experimental = true
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 1bd8fac03..b0e2bcab5 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -2,6 +2,7 @@ package purescala
// typically these settings can be changed through some command-line switch.
object Settings {
+ var experimental : Boolean = false
var showIDs: Boolean = false
var quietExtensions: Boolean = false
var functionsToAnalyse: Set[String] = Set.empty
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index a4405a67c..fbe596910 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -654,7 +654,7 @@ object Trees {
}
}
- def unapply(pm : MatchExpr) : Option[MatchExpr] = pm match {
+ def unapply(pm : MatchExpr) : Option[MatchExpr] = if(!Settings.experimental) None else (pm match {
case MatchExpr(scrutinee, cases) if cases.forall(_.isInstanceOf[SimpleCase]) => {
val allPatterns = cases.map(_.pattern)
Settings.reporter.info("This might be a complete pattern-matching expression:")
@@ -663,7 +663,7 @@ object Trees {
None
}
case _ => None
- }
+ })
}
// we use this when debugging our tree transformations...
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index eb25332cc..c828fcd5e 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -139,7 +139,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
}
// universally quantifies all functions !
- if(!Settings.noForallAxioms) {
+ if(Settings.experimental && !Settings.noForallAxioms) {
for(funDef <- program.definedFunctions) if(funDef.hasImplementation && program.isRecursive(funDef) && funDef.args.size > 0) {
funDef.body.get match {
case SimplePatternMatching(scrutinee,_,infos) if (
--
GitLab