Skip to content
Snippets Groups Projects
Commit 4694b353 authored by Emmanouil (Manos) Koukoutos's avatar Emmanouil (Manos) Koukoutos Committed by Etienne Kneuss
Browse files

We don't handle guards, for now

parent 680bd273
Branches
Tags
No related merge requests found
...@@ -86,7 +86,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie ...@@ -86,7 +86,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
def toIOExamples(in: Expr, out : Expr, cs : MatchCase) : Seq[(Expr,Expr)] = { def toIOExamples(in: Expr, out : Expr, cs : MatchCase) : Seq[(Expr,Expr)] = {
import utils.ExpressionGrammars import utils.ExpressionGrammars.ValueGrammar
import leon.utils.StreamUtils.cartesianProduct import leon.utils.StreamUtils.cartesianProduct
import bonsai._ import bonsai._
import bonsai.enumerators._ import bonsai.enumerators._
...@@ -98,10 +98,13 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie ...@@ -98,10 +98,13 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
case (from, (id, to)) => replaceFromIDs(Map(id -> to), from) case (from, (id, to)) => replaceFromIDs(Map(id -> to), from)
} }
// The trivial example if (cs.optGuard.isDefined) {
if (cs.rhs == out) sctx.reporter.error("Cannot handle guards in example extraction. @" + cs.optGuard.get.getPos)
Seq() Seq()
else { } else if (cs.rhs == out) {
// The trivial example
Seq()
} else {
// The pattern as expression (input expression)(may contain free variables) // The pattern as expression (input expression)(may contain free variables)
val (pattExpr, ieMap) = patternToExpression(cs.pattern, in.getType) val (pattExpr, ieMap) = patternToExpression(cs.pattern, in.getType)
val freeVars = variablesOf(pattExpr).toSeq val freeVars = variablesOf(pattExpr).toSeq
...@@ -111,8 +114,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie ...@@ -111,8 +114,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
} else { } else {
// If the input contains free variables, it does not provide concrete examples. // If the input contains free variables, it does not provide concrete examples.
// We will instantiate them according to a simple grammar to get them. // We will instantiate them according to a simple grammar to get them.
val grammar = ExpressionGrammars.ValueGrammar val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions _)
val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions _)
val types = freeVars.map{ _.getType } val types = freeVars.map{ _.getType }
val typesWithValues = types.map { tp => (tp, enum.iterator(tp).toStream) }.toMap val typesWithValues = types.map { tp => (tp, enum.iterator(tp).toStream) }.toMap
val values = freeVars map { v => typesWithValues(v.getType) } val values = freeVars map { v => typesWithValues(v.getType) }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment