From 031b564bbc327813cfe706df258dbcd0cac8c50d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 2 May 2016 12:35:51 +0200
Subject: [PATCH] Add a few types to ValueGrammar
---
.../scala/leon/grammars/ValueGrammar.scala | 21 +++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
index 996debb85..a71344583 100644
--- a/src/main/scala/leon/grammars/ValueGrammar.scala
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -3,6 +3,8 @@
package leon
package grammars
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Definitions.ValDef
import purescala.Types._
import purescala.Expressions._
@@ -26,6 +28,19 @@ case object ValueGrammar extends SimpleExpressionGrammar {
terminal(InfiniteIntegerLiteral(1), Tags.One),
terminal(InfiniteIntegerLiteral(5), Tags.Constant)
)
+ case CharType =>
+ List(
+ terminal(CharLiteral('a'), Tags.Constant),
+ terminal(CharLiteral('b'), Tags.Constant),
+ terminal(CharLiteral('0'), Tags.Constant)
+ )
+ case RealType =>
+ List(
+ terminal(FractionalLiteral(0, 1), Tags.Zero),
+ terminal(FractionalLiteral(1, 1), Tags.One),
+ terminal(FractionalLiteral(-1, 2), Tags.Constant),
+ terminal(FractionalLiteral(555, 42), Tags.Constant)
+ )
case StringType =>
List(
terminal(StringLiteral(""), Tags.Constant),
@@ -66,6 +81,12 @@ case object ValueGrammar extends SimpleExpressionGrammar {
terminal(UnitLiteral(), Tags.Constant)
)
+ case FunctionType(from, to) =>
+ val args = from map (tp => ValDef(FreshIdentifier("x", tp, true)))
+ List(
+ nonTerminal(Seq(to), { case Seq(e) => Lambda(args, e) })
+ )
+
case _ =>
Nil
}
--
GitLab