diff options
| -rw-r--r-- | Source/Core/Parser.cs | 24 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 1 |
2 files changed, 23 insertions, 2 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 696a72ed..5545d8c4 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1717,7 +1717,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { }
void AtomExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; FP32 fp;
List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
List<TypeVariable>/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1742,11 +1742,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bn);
break;
}
- case 5: case 6: {
+ case 5: {
Dec(out bd);
e = new LiteralExpr(t, bd);
break;
}
+ case 6: {
+ Float(out fp);
+ e = new LiteralExpr(t, fp);
+ break;
+ }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1856,6 +1861,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { }
+ void Float(out FP32 n)
+ {
+ string s = "";
+ if (la.kind == 6) {
+ Get();
+ s = t.val;
+ } else SynErr(126);
+ try {
+ n = FP32.FromString(s);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = FP32.ZERO;
+ }
+ }
+
void BvLit(out BigNum n, out int m) {
Expect(2);
int pos = t.val.IndexOf("bv");
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index b23a46a4..a3c139c8 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -508,6 +508,7 @@ public class Scanner { case "int": t.kind = 14; break;
case "real": t.kind = 15; break;
case "bool": t.kind = 16; break;
+ case "float": t.kind = 135; break;
case "const": t.kind = 21; break;
case "unique": t.kind = 22; break;
case "extends": t.kind = 23; break;
|