diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala index 996debb8525d94080f4368722ee9b92ff4bd3e40..a713445839ff3622ec0bb3778c57a941edbf09d2 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 }