summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Core/Parser.cs288
-rw-r--r--Source/Core/Scanner.cs2
2 files changed, 79 insertions, 211 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 1f8d17d6..78823b61 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -24,8 +24,7 @@ public class Parser {
public const int _string = 4;
public const int _decimal = 5;
public const int _float = 6;
- public const int _fp = 97;
- public const int maxT = 98;
+ public const int maxT = 96;
const bool T = true;
const bool x = false;
@@ -118,7 +117,7 @@ private class BvBounds : Expr {
public BigNum Lower;
public BigNum Upper;
public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
- : base(tok, /*immutable=*/ false) {
+ : base(tok, /*immutable*/ false) {
Contract.Requires(tok != null);
this.Lower = lower;
this.Upper = upper;
@@ -133,7 +132,8 @@ private class BvBounds : Expr {
Contract.Assert(false);throw new cce.UnreachableException();
}
public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
- public override int ComputeHashCode() {
+ public override int ComputeHashCode()
+ {
return base.GetHashCode();
}
}
@@ -366,7 +366,7 @@ private class BvBounds : Expr {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(99);
+ } else SynErr(97);
if (la.kind == 27) {
Get();
Expression(out tmp);
@@ -374,7 +374,7 @@ private class BvBounds : Expr {
Expect(28);
} else if (la.kind == 8) {
Get();
- } else SynErr(100);
+ } else SynErr(98);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -665,11 +665,8 @@ private class BvBounds : Expr {
ty = new BasicType(t, SimpleType.Int);
} else if (la.kind == 15) {
Get();
- ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 98) {
- Get();
- ty = FType();
- } else if (la.kind == 16) {
+ ty = new BasicType(t, SimpleType.Real);
+ } else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Bool);
} else if (la.kind == 9) {
@@ -679,39 +676,6 @@ private class BvBounds : Expr {
} else SynErr(101);
}
- FloatType FType() {
- if (t.val.Length > 5) {
- switch (Int32.Parse(t.val.Substring(5))) {
- case 16:
- return new FloatType(t, 5, 11);
- case 32:
- return new FloatType(t, 8, 24);
- case 64:
- return new FloatType(t, 11, 53);
- case 128:
- return new FloatType(t, 15, 113);
- default:
- SynErr(3);
- return new FloatType(t, 0, 0);
- }
- }
- else {
- try {
- Expect(19); //<
- Expect(3); //int
- int exp = Int32.Parse(t.val);
- Expect(12); //,
- Expect(3); //int
- int man = Int32.Parse(t.val);
- Expect(20); //>
- return new FloatType(t, exp, man);
- }
- catch (Exception) {
- return new FloatType(t, 0, 0);
- }
- }
- }
-
void Ident(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
@@ -1656,7 +1620,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get();
} else if (la.kind == 81) {
Get();
- } else SynErr(123);
+ } else SynErr(121);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1680,7 +1644,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(124);
+ } else SynErr(122);
}
}
@@ -1751,7 +1715,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; BigFloat fp;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
List<TypeVariable>/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1776,16 +1740,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new LiteralExpr(t, bn);
break;
}
- case 5: case 6: {
+ case 5: case 6: {
Dec(out bd);
e = new LiteralExpr(t, bd);
break;
}
- case 97: {
- Float(out fp);
- e = new LiteralExpr(t, fp);
- break;
- }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1801,7 +1760,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 10) {
e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
- } else SynErr(125);
+ } else SynErr(123);
Expect(10);
}
break;
@@ -1833,15 +1792,6 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
break;
}
- case 98: {
- Get();
- x = t;
- Expect(19);
- Expression(out e);
- Expect(20);
- e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
- break;
- }
case 9: {
Get();
if (StartOf(9)) {
@@ -1869,7 +1819,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Count + ds.Count > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(126);
+ } else SynErr(124);
Expect(10);
break;
}
@@ -1882,7 +1832,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(127); break;
+ default: SynErr(125); break;
}
}
@@ -1894,7 +1844,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(128);
+ } else SynErr(126);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1904,77 +1854,6 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
- /// <summary>
- /// Creates a floating point from the current token value
- /// </summary>
- /// <param name="n"></param>
- void Float(out BigFloat n)
- {
- try
- {
- if (la.kind == 97) {
- bool negative = false;
- int exp, sig, size;
- BigNum exp_val, sig_val, value;
- //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)
- Get(); //Skip the float token
- if (la.val == "(") {
- Get();
- if (la.val == "false")
- negative = false;
- else if (la.val == "true")
- negative = true;
- else
- throw new FormatException();
- Get();
- Expect(12); //,
- BvLit(out exp_val, out exp);
- Expect(12);
- BvLit(out sig_val, out sig);
- n = new BigFloat(negative, exp_val, sig_val, exp, sig);
- Expect(10); //)
- }
- else if (la.val == "<") {
- Get();
- Expect(3);
- exp = Int32.Parse(t.val);
- Expect(12);
- Expect(3);
- sig = Int32.Parse(t.val);
- Expect(20); //>
- Expect(9); //(
- if (la.kind == 1) { //NaN
- Get();
- n = new BigFloat(t.val, exp, sig);
- }
- else if (la.kind == 74 || la.kind == 75) { //+ or -
- Get();
- String s = t.val;
- Get();
- n = new BigFloat(s + t.val, exp, sig);
- }
- else {
- BvLit(out value, out size);
- n = new BigFloat(value.ToString(), exp, sig);
- }
- Expect(10); //)
- }
- else {
- throw new FormatException();
- }
- }
- else {
- n = BigFloat.ZERO(8, 24);
- SynErr(137);
- }
- }
- catch (FormatException)
- {
- this.SemErr("incorrectly formatted floating point");
- n = BigFloat.ZERO(8, 24);
- }
- }
-
void BvLit(out BigNum n, out int m) {
Expect(2);
int pos = t.val.IndexOf("bv");
@@ -1996,7 +1875,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get();
} else if (la.kind == 89) {
Get();
- } else SynErr(129);
+ } else SynErr(127);
}
void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -2014,7 +1893,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
} else if (la.kind == 1 || la.kind == 27) {
BoundVars(q, out ds);
- } else SynErr(130);
+ } else SynErr(128);
QSep();
while (la.kind == 27) {
AttributeOrTrigger(ref kv, ref trig);
@@ -2027,7 +1906,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 91) {
Get();
- } else SynErr(131);
+ } else SynErr(129);
}
void Lambda() {
@@ -2035,7 +1914,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 93) {
Get();
- } else SynErr(132);
+ } else SynErr(130);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -2105,7 +1984,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(133);
+ } else SynErr(131);
Expect(8);
}
@@ -2162,7 +2041,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(134);
+ } else SynErr(132);
Expect(28);
}
@@ -2177,7 +2056,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(135);
+ } else SynErr(133);
}
void QSep() {
@@ -2185,7 +2064,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 95) {
Get();
- } else SynErr(136);
+ } else SynErr(134);
}
@@ -2200,24 +2079,24 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expect(0);
}
- static readonly bool[,]/*!*/ set = { //grid is 17 x 100
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x}
+ static readonly bool[,]/*!*/ set = {
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}
};
} // end Parser
@@ -2239,12 +2118,6 @@ public class Errors {
count++;
}
- /// <summary>
- /// Returns a string corresponding to the syntax error of the given type
- /// Note that many of these errors (0-98) correspond to token types (e.g. the la token)
- /// </summary>
- /// <param name="n"></param>
- /// <returns></returns>
string GetSyntaxErrorString(int n) {
string s;
switch (n) {
@@ -2345,47 +2218,44 @@ public class Errors {
case 94: s = "\"::\" expected"; break;
case 95: s = "\"\\u2022\" expected"; break;
case 96: s = "??? expected"; break;
- case 97: s = "fp expected"; break;
- case 98: s = "\"float\" expected"; break;
- case 99: s = "invalid Function"; break;
- case 100: s = "invalid Function"; break;
- case 101: s = "invalid Procedure"; break;
- case 102: s = "invalid Type"; break;
- case 103: s = "invalid TypeAtom"; break;
- case 104: s = "invalid TypeArgs"; break;
- case 105: s = "invalid Spec"; break;
- case 106: s = "invalid SpecPrePost"; break;
- case 107: s = "invalid LabelOrCmd"; break;
- case 108: s = "invalid StructuredCmd"; break;
- case 109: s = "invalid TransferCmd"; break;
- case 110: s = "invalid IfCmd"; break;
- case 111: s = "invalid Guard"; break;
- case 112: s = "invalid LabelOrAssign"; break;
- case 113: s = "invalid CallParams"; break;
- case 114: s = "invalid EquivOp"; break;
- case 115: s = "invalid ImpliesOp"; break;
- case 116: s = "invalid ExpliesOp"; break;
- case 117: s = "invalid AndOp"; break;
- case 118: s = "invalid OrOp"; break;
- case 119: s = "invalid RelOp"; break;
- case 120: s = "invalid AddOp"; break;
- case 121: s = "invalid MulOp"; break;
- case 122: s = "invalid UnaryExpression"; break;
- case 123: s = "invalid NegOp"; break;
- case 124: s = "invalid CoercionExpression"; break;
+ case 97: s = "invalid Function"; break;
+ case 98: s = "invalid Function"; break;
+ case 99: s = "invalid Procedure"; break;
+ case 100: s = "invalid Type"; break;
+ case 101: s = "invalid TypeAtom"; break;
+ case 102: s = "invalid TypeArgs"; break;
+ case 103: s = "invalid Spec"; break;
+ case 104: s = "invalid SpecPrePost"; break;
+ case 105: s = "invalid LabelOrCmd"; break;
+ case 106: s = "invalid StructuredCmd"; break;
+ case 107: s = "invalid TransferCmd"; break;
+ case 108: s = "invalid IfCmd"; break;
+ case 109: s = "invalid Guard"; break;
+ case 110: s = "invalid LabelOrAssign"; break;
+ case 111: s = "invalid CallParams"; break;
+ case 112: s = "invalid EquivOp"; break;
+ case 113: s = "invalid ImpliesOp"; break;
+ case 114: s = "invalid ExpliesOp"; break;
+ case 115: s = "invalid AndOp"; break;
+ case 116: s = "invalid OrOp"; break;
+ case 117: s = "invalid RelOp"; break;
+ case 118: s = "invalid AddOp"; break;
+ case 119: s = "invalid MulOp"; break;
+ case 120: s = "invalid UnaryExpression"; break;
+ case 121: s = "invalid NegOp"; break;
+ case 122: s = "invalid CoercionExpression"; break;
+ case 123: s = "invalid AtomExpression"; break;
+ case 124: s = "invalid AtomExpression"; break;
case 125: s = "invalid AtomExpression"; break;
- case 126: s = "invalid AtomExpression"; break;
- case 127: s = "invalid AtomExpression"; break;
- case 128: s = "invalid Dec"; break;
- case 129: s = "invalid Forall"; break;
- case 130: s = "invalid QuantifierBody"; break;
- case 131: s = "invalid Exists"; break;
- case 132: s = "invalid Lambda"; break;
- case 133: s = "invalid SpecBlock"; break;
- case 134: s = "invalid AttributeOrTrigger"; break;
- case 135: s = "invalid AttributeParameter"; break;
- case 136: s = "invalid QSep"; break;
- case 137: s = "invalid Float"; break;
+ case 126: s = "invalid Dec"; break;
+ case 127: s = "invalid Forall"; break;
+ case 128: s = "invalid QuantifierBody"; break;
+ case 129: s = "invalid Exists"; break;
+ case 130: s = "invalid Lambda"; break;
+ case 131: s = "invalid SpecBlock"; break;
+ case 132: s = "invalid AttributeOrTrigger"; break;
+ case 133: s = "invalid AttributeParameter"; break;
+ case 134: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 69023555..e068fc4b 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -508,8 +508,6 @@ public class Scanner {
case "int": t.kind = 14; break;
case "real": t.kind = 15; break;
case "bool": t.kind = 16; break;
- case "fp": t.kind = 97; break;
- case "float": case "float16": case "float32": case "float64": case "float128": t.kind = 98; break;
case "const": t.kind = 21; break;
case "unique": t.kind = 22; break;
case "extends": t.kind = 23; break;