From b19c478f6016002a96e524a2ba6afc38e9a2ffe6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 22 Oct 2015 16:43:28 +0200
Subject: [PATCH] Added minimal string value Added values for generating
values.
---
src/main/scala/leon/datagen/VanuatooDataGen.scala | 10 ++++++++++
src/main/scala/leon/purescala/ExprOps.scala | 5 +++++
2 files changed, 15 insertions(+)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index e68e21f01..066b411de 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -32,12 +32,19 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val booleans = (for (b <- Set(true, false)) yield {
b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b)
}).toMap
+
+ val strings = (for (b <- Set("", "a", "Abcd")) yield {
+ b -> Constructor[Expr, TypeTree](List(), StringType, s => StringLiteral(b), b)
+ }).toMap
+
def intConstructor(i: Int) = ints(i)
def bigIntConstructor(i: Int) = bigInts(i)
def boolConstructor(b: Boolean) = booleans(b)
+
+ def stringConstructor(s: String) = strings(s)
def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = {
ConstructorPattern[Expr, TypeTree](c, args)
@@ -166,6 +173,9 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case (b: java.lang.Boolean, BooleanType) =>
(cPattern(boolConstructor(b), List()), true)
+ case (b: java.lang.String, StringType) =>
+ (cPattern(stringConstructor(b), List()), true)
+
case (cc: codegen.runtime.CaseClass, ct: ClassType) =>
val r = cc.__getRead()
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c106d1393..9acca4069 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1100,6 +1100,7 @@ object ExprOps {
/** Returns simplest value of a given type */
def simplestValue(tpe: TypeTree) : Expr = tpe match {
+ case StringType => StringLiteral("")
case Int32Type => IntLiteral(0)
case RealType => FractionalLiteral(0, 1)
case IntegerType => InfiniteIntegerLiteral(0)
@@ -1735,6 +1736,10 @@ object ExprOps {
case UnitType =>
// Anything matches ()
ps.nonEmpty
+
+ case StringType =>
+ // Can't possibly pattern match against all Strings one by one
+ ps exists (_.isInstanceOf[WildcardPattern])
case Int32Type =>
// Can't possibly pattern match against all Ints one by one
--
GitLab