summaryrefslogtreecommitdiff
path: root/Source/Core/Parser.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/Parser.cs')
-rw-r--r--Source/Core/Parser.cs887
1 files changed, 454 insertions, 433 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 793bb96e..c91de177 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -23,8 +23,9 @@ public class Parser {
public const int _digits = 3;
public const int _string = 4;
public const int _decimal = 5;
- public const int _float = 6;
- public const int maxT = 96;
+ public const int _dec_float = 6;
+ public const int _float = 7;
+ public const int maxT = 97;
const bool T = true;
const bool x = false;
@@ -132,7 +133,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();
}
}
@@ -219,7 +221,7 @@ private class BvBounds : Expr {
while (StartOf(1)) {
switch (la.kind) {
- case 21: {
+ case 22: {
Consts(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -228,7 +230,7 @@ private class BvBounds : Expr {
break;
}
- case 25: {
+ case 26: {
Function(out ds);
foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
@@ -237,12 +239,12 @@ private class BvBounds : Expr {
break;
}
- case 29: {
+ case 30: {
Axiom(out ax);
Pgm.AddTopLevelDeclaration(ax);
break;
}
- case 30: {
+ case 31: {
UserDefinedTypes(out ts);
foreach(Declaration/*!*/ td in ts){
Contract.Assert(td != null);
@@ -251,7 +253,7 @@ private class BvBounds : Expr {
break;
}
- case 7: {
+ case 8: {
GlobalVars(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -260,7 +262,7 @@ private class BvBounds : Expr {
break;
}
- case 32: {
+ case 33: {
Procedure(out pr, out im);
Pgm.AddTopLevelDeclaration(pr);
if (im != null) {
@@ -269,7 +271,7 @@ private class BvBounds : Expr {
break;
}
- case 33: {
+ case 34: {
Implementation(out nnim);
Pgm.AddTopLevelDeclaration(nnim);
break;
@@ -285,17 +287,17 @@ private class BvBounds : Expr {
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
List<ConstantParent/*!*/> Parents = null;
- Expect(21);
+ Expect(22);
y = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
u = true;
}
IdsType(out xs);
- if (la.kind == 23) {
+ if (la.kind == 24) {
OrderSpec(out ChildrenComplete, out Parents);
}
bool makeClone = false;
@@ -319,7 +321,7 @@ private class BvBounds : Expr {
ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
}
- Expect(8);
+ Expect(9);
}
void Function(out List<Declaration>/*!*/ ds) {
@@ -336,44 +338,44 @@ private class BvBounds : Expr {
Expr definition = null;
Expr/*!*/ tmp;
- Expect(25);
- while (la.kind == 27) {
+ Expect(26);
+ while (la.kind == 28) {
Attribute(ref kv);
}
Ident(out z);
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out typeParamTok, out typeParams);
}
- Expect(9);
+ Expect(10);
if (StartOf(2)) {
VarOrType(out tyd, out argKv);
arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
VarOrType(out tyd, out argKv);
arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
}
}
- Expect(10);
+ Expect(11);
argKv = null;
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
- Expect(9);
- VarOrType(out retTyd, out argKv);
Expect(10);
- } else if (la.kind == 11) {
+ VarOrType(out retTyd, out argKv);
+ Expect(11);
+ } else if (la.kind == 12) {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(97);
- if (la.kind == 27) {
+ } else SynErr(98);
+ if (la.kind == 28) {
Get();
Expression(out tmp);
definition = tmp;
- Expect(28);
- } else if (la.kind == 8) {
+ Expect(29);
+ } else if (la.kind == 9) {
Get();
- } else SynErr(98);
+ } else SynErr(99);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -428,30 +430,30 @@ private class BvBounds : Expr {
void Axiom(out Axiom/*!*/ m) {
Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null;
- Expect(29);
- while (la.kind == 27) {
+ Expect(30);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IToken/*!*/ x = t;
Proposition(out e);
- Expect(8);
+ Expect(9);
m = new Axiom(x,e, null, kv);
}
void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> ();
- Expect(30);
- while (la.kind == 27) {
+ Expect(31);
+ while (la.kind == 28) {
Attribute(ref kv);
}
UserDefinedType(out decl, kv);
ts.Add(decl);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
UserDefinedType(out decl, kv);
ts.Add(decl);
}
- Expect(8);
+ Expect(9);
}
void GlobalVars(out List<Variable>/*!*/ ds) {
@@ -460,12 +462,12 @@ private class BvBounds : Expr {
ds = new List<Variable>();
var dsx = ds;
- Expect(7);
- while (la.kind == 27) {
+ Expect(8);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
+ Expect(9);
}
void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
@@ -481,9 +483,9 @@ private class BvBounds : Expr {
QKeyValue kv = null;
impl = null;
- Expect(32);
+ Expect(33);
ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
while (StartOf(3)) {
Spec(pre, mods, post);
@@ -496,7 +498,7 @@ private class BvBounds : Expr {
impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
- } else SynErr(99);
+ } else SynErr(100);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -508,7 +510,7 @@ private class BvBounds : Expr {
StmtList/*!*/ stmtList;
QKeyValue kv;
- Expect(33);
+ Expect(34);
ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
@@ -522,7 +524,7 @@ private class BvBounds : Expr {
void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
IdsTypeWhere(allowWhereClauses, context, action);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
IdsTypeWhere(allowWhereClauses, context, action);
}
@@ -532,12 +534,12 @@ private class BvBounds : Expr {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
QKeyValue kv = null;
- Expect(7);
- while (la.kind == 27) {
+ Expect(8);
+ while (la.kind == 28) {
Attribute(ref kv);
}
IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
+ Expect(9);
}
void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {
@@ -546,16 +548,16 @@ private class BvBounds : Expr {
var dsx = ds;
var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
- Expect(9);
- if (la.kind == 1 || la.kind == 27) {
+ Expect(10);
+ if (la.kind == 1 || la.kind == 28) {
AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
}
- Expect(10);
+ Expect(11);
}
void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
}
@@ -574,7 +576,7 @@ private class BvBounds : Expr {
void IdsType(out List<TypedIdent>/*!*/ tyds) {
Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty;
Idents(out ids);
- Expect(11);
+ Expect(12);
Type(out ty);
tyds = new List<TypedIdent>();
foreach(Token/*!*/ id in ids){
@@ -588,7 +590,7 @@ private class BvBounds : Expr {
Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
Ident(out id);
xs.Add(id);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out id);
xs.Add(id);
@@ -606,14 +608,14 @@ private class BvBounds : Expr {
TypeArgs(args);
}
ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
- } else if (la.kind == 17 || la.kind == 19) {
+ } else if (la.kind == 18 || la.kind == 20) {
MapType(out ty);
- } else SynErr(100);
+ } else SynErr(101);
}
void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
QKeyValue kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
if (!allowAttributes) {
kv = null;
@@ -627,9 +629,9 @@ private class BvBounds : Expr {
void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne;
Idents(out ids);
- Expect(11);
+ Expect(12);
Type(out ty);
- if (la.kind == 13) {
+ if (la.kind == 14) {
Get();
Expression(out nne);
if (!allowWhereClauses) {
@@ -649,7 +651,7 @@ private class BvBounds : Expr {
void Expression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
ImpliesExpression(false, out e0);
- while (la.kind == 55 || la.kind == 56) {
+ while (la.kind == 56 || la.kind == 57) {
EquivOp();
x = t;
ImpliesExpression(false, out e1);
@@ -659,20 +661,20 @@ private class BvBounds : Expr {
void TypeAtom(out Bpl.Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType;
- if (la.kind == 14) {
+ if (la.kind == 15) {
Get();
ty = new BasicType(t, SimpleType.Int);
- } else if (la.kind == 15) {
+ } else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 16) {
+ } else if (la.kind == 17) {
Get();
ty = new BasicType(t, SimpleType.Bool);
- } else if (la.kind == 9) {
+ } else if (la.kind == 10) {
Get();
Type(out ty);
- Expect(10);
- } else SynErr(101);
+ Expect(11);
+ } else SynErr(102);
}
void Ident(out IToken/*!*/ x) {
@@ -699,10 +701,10 @@ private class BvBounds : Expr {
if (StartOf(6)) {
TypeArgs(ts);
}
- } else if (la.kind == 17 || la.kind == 19) {
+ } else if (la.kind == 18 || la.kind == 20) {
MapType(out ty);
ts.Add(ty);
- } else SynErr(102);
+ } else SynErr(103);
}
void MapType(out Bpl.Type/*!*/ ty) {
@@ -712,16 +714,16 @@ private class BvBounds : Expr {
Bpl.Type/*!*/ result;
List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out nnTok, out typeParameters);
tok = nnTok;
}
- Expect(17);
+ Expect(18);
if (tok == null) tok = t;
if (StartOf(6)) {
Types(arguments);
}
- Expect(18);
+ Expect(19);
Type(out result);
ty = new MapType(tok, typeParameters, arguments, result);
@@ -729,10 +731,10 @@ private class BvBounds : Expr {
void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks;
- Expect(19);
+ Expect(20);
tok = t;
Idents(out typeParamToks);
- Expect(20);
+ Expect(21);
typeParams = new List<TypeVariable> ();
foreach(Token/*!*/ id in typeParamToks){
Contract.Assert(id != null);
@@ -744,7 +746,7 @@ private class BvBounds : Expr {
Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
Type(out ty);
ts.Add(ty);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Type(out ty);
ts.Add(ty);
@@ -756,21 +758,21 @@ private class BvBounds : Expr {
Parents = null;
bool u;
IToken/*!*/ parent;
- Expect(23);
+ Expect(24);
Parents = new List<ConstantParent/*!*/> ();
u = false;
- if (la.kind == 1 || la.kind == 22) {
- if (la.kind == 22) {
+ if (la.kind == 1 || la.kind == 23) {
+ if (la.kind == 23) {
Get();
u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
new IdentifierExpr(parent, parent.val), u));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
u = false;
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
u = true;
}
@@ -779,7 +781,7 @@ private class BvBounds : Expr {
new IdentifierExpr(parent, parent.val), u));
}
}
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
ChildrenComplete = true;
}
@@ -792,12 +794,12 @@ private class BvBounds : Expr {
IToken/*!*/ tok;
kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Type(out ty);
tok = ty.tok;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
var uti = ty as UnresolvedTypeIdentifier;
if (uti != null && uti.Arguments.Count == 0) {
@@ -823,7 +825,7 @@ private class BvBounds : Expr {
if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
}
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
Type(out body);
synonym = true;
@@ -855,15 +857,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);
IToken/*!*/ typeParamTok; typeParams = new List<TypeVariable>();
outs = new List<Variable>(); kv = null;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Ident(out name);
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out typeParamTok, out typeParams);
}
ProcFormals(true, allowWhereClausesOnFormals, out ins);
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
ProcFormals(false, allowWhereClausesOnFormals, out outs);
}
@@ -871,7 +873,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms;
- if (la.kind == 34) {
+ if (la.kind == 35) {
Get();
if (la.kind == 1) {
Idents(out ms);
@@ -881,19 +883,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
}
- Expect(8);
- } else if (la.kind == 35) {
+ Expect(9);
+ } else if (la.kind == 36) {
Get();
SpecPrePost(true, pre, post);
- } else if (la.kind == 36 || la.kind == 37) {
+ } else if (la.kind == 37 || la.kind == 38) {
SpecPrePost(false, pre, post);
- } else SynErr(103);
+ } else SynErr(104);
}
void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>();
- Expect(27);
- while (la.kind == 7) {
+ Expect(28);
+ while (la.kind == 8) {
LocalVars(locals);
}
StmtList(out stmtList);
@@ -901,25 +903,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
- if (la.kind == 36) {
+ if (la.kind == 37) {
Get();
tok = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(8);
+ Expect(9);
pre.Add(new Requires(tok, free, e, null, kv));
- } else if (la.kind == 37) {
+ } else if (la.kind == 38) {
Get();
tok = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(8);
+ Expect(9);
post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(104);
+ } else SynErr(105);
}
void StmtList(out StmtList/*!*/ stmtList) {
@@ -956,7 +958,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
cs = new List<Cmd>();
}
- } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
+ } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) {
StructuredCmd(out ecn);
ec = ecn;
if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
@@ -976,7 +978,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
}
- Expect(28);
+ Expect(29);
IToken/*!*/ endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
startToken = t; cs = new List<Cmd>();
@@ -1004,33 +1006,33 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
LabelOrAssign(out c, out label);
break;
}
- case 46: {
+ case 47: {
Get();
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssertCmd(x, e, kv);
- Expect(8);
+ Expect(9);
break;
}
- case 47: {
+ case 48: {
Get();
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssumeCmd(x, e, kv);
- Expect(8);
+ Expect(9);
break;
}
- case 48: {
+ case 49: {
Get();
x = t;
Idents(out xs);
- Expect(8);
+ Expect(9);
ids = new List<IdentifierExpr>();
foreach(IToken/*!*/ y in xs){
Contract.Assert(y != null);
@@ -1040,25 +1042,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
break;
}
- case 35: case 51: case 52: {
+ case 36: case 52: case 53: {
CallCmd(out cn);
- Expect(8);
+ Expect(9);
c = cn;
break;
}
- case 53: {
+ case 54: {
ParCallCmd(out cn);
c = cn;
break;
}
- case 49: {
+ case 50: {
Get();
x = t;
- Expect(8);
+ Expect(9);
c = new YieldCmd(x);
break;
}
- default: SynErr(105); break;
+ default: SynErr(106); break;
}
}
@@ -1066,16 +1068,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec));
IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd;
- if (la.kind == 40) {
+ if (la.kind == 41) {
IfCmd(out ifcmd);
ec = ifcmd;
- } else if (la.kind == 42) {
+ } else if (la.kind == 43) {
WhileCmd(out wcmd);
ec = wcmd;
- } else if (la.kind == 45) {
+ } else if (la.kind == 46) {
BreakCmd(out bcmd);
ec = bcmd;
- } else SynErr(106);
+ } else SynErr(107);
}
void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1083,7 +1085,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Token y; List<IToken>/*!*/ xs;
List<String> ss = new List<String>();
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
y = t;
Idents(out xs);
@@ -1092,11 +1094,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
ss.Add(s.val); }
tc = new GotoCmd(y, ss);
- } else if (la.kind == 39) {
+ } else if (la.kind == 40) {
Get();
tc = new ReturnCmd(t);
- } else SynErr(107);
- Expect(8);
+ } else SynErr(108);
+ Expect(9);
}
void IfCmd(out IfCmd/*!*/ ifcmd) {
@@ -1106,21 +1108,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
IfCmd/*!*/ elseIf; IfCmd elseIfOption = null;
StmtList/*!*/ els; StmtList elseOption = null;
- Expect(40);
+ Expect(41);
x = t;
Guard(out guard);
- Expect(27);
+ Expect(28);
StmtList(out thn);
- if (la.kind == 41) {
+ if (la.kind == 42) {
Get();
- if (la.kind == 40) {
+ if (la.kind == 41) {
IfCmd(out elseIf);
elseIfOption = elseIf;
- } else if (la.kind == 27) {
+ } else if (la.kind == 28) {
Get();
StmtList(out els);
elseOption = els;
- } else SynErr(108);
+ } else SynErr(109);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1132,18 +1134,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
StmtList/*!*/ body;
QKeyValue kv = null;
- Expect(42);
+ Expect(43);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 35 || la.kind == 43) {
+ while (la.kind == 36 || la.kind == 44) {
isFree = false; z = la/*lookahead token*/;
- if (la.kind == 35) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(43);
- while (la.kind == 27) {
+ Expect(44);
+ while (la.kind == 28) {
Attribute(ref kv);
}
Expression(out e);
@@ -1154,9 +1156,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
kv = null;
- Expect(8);
+ Expect(9);
}
- Expect(27);
+ Expect(28);
StmtList(out body);
wcmd = new WhileCmd(x, guard, invariants, body);
}
@@ -1165,27 +1167,27 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
string breakLabel = null;
- Expect(45);
+ Expect(46);
x = t;
if (la.kind == 1) {
Ident(out y);
breakLabel = y.val;
}
- Expect(8);
+ Expect(9);
bcmd = new BreakCmd(x, breakLabel);
}
void Guard(out Expr e) {
Expr/*!*/ ee; e = null;
- Expect(9);
- if (la.kind == 44) {
+ Expect(10);
+ if (la.kind == 45) {
Get();
e = null;
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(109);
- Expect(10);
+ } else SynErr(110);
+ Expect(11);
}
void LabelOrAssign(out Cmd c, out IToken label) {
@@ -1198,40 +1200,40 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Ident(out id);
x = t;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
c = null; label = x;
- } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
+ } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) {
lhss = new List<AssignLhs/*!*/>();
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
+ while (la.kind == 18) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out id);
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
+ while (la.kind == 18) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
}
- Expect(50);
+ Expect(51);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr/*!*/> ();
rhss.Add(e0);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e0);
rhss.Add(e0);
}
- Expect(8);
+ Expect(9);
c = new AssignCmd(x, lhss, rhss);
- } else SynErr(110);
+ } else SynErr(111);
}
void CallCmd(out Cmd c) {
@@ -1242,17 +1244,17 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
QKeyValue kv = null;
c = null;
- if (la.kind == 51) {
+ if (la.kind == 52) {
Get();
isAsync = true;
}
- if (la.kind == 35) {
+ if (la.kind == 36) {
Get();
isFree = true;
}
- Expect(52);
+ Expect(53);
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
CallParams(isAsync, isFree, kv, x, out c);
@@ -1266,19 +1268,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Cmd c = null;
List<CallCmd> callCmds = new List<CallCmd>();
- Expect(53);
+ Expect(54);
x = t;
- while (la.kind == 27) {
+ while (la.kind == 28) {
Attribute(ref kv);
}
CallParams(false, false, kv, x, out c);
callCmds.Add((CallCmd)c);
- while (la.kind == 54) {
+ while (la.kind == 55) {
Get();
CallParams(false, false, kv, x, out c);
callCmds.Add((CallCmd)c);
}
- Expect(8);
+ Expect(9);
d = new ParCallCmd(x, callCmds, kv);
}
@@ -1286,18 +1288,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
Expr/*!*/ e;
- Expect(17);
+ Expect(18);
x = t;
if (StartOf(9)) {
Expression(out e);
indexes.Add(e);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
indexes.Add(e);
}
}
- Expect(18);
+ Expect(19);
}
void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) {
@@ -1309,53 +1311,53 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
c = null;
Ident(out first);
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
if (StartOf(9)) {
Expression(out en);
es.Add(en);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out en);
es.Add(en);
}
}
- Expect(10);
+ Expect(11);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else if (la.kind == 12 || la.kind == 50) {
+ } else if (la.kind == 13 || la.kind == 51) {
ids.Add(new IdentifierExpr(first, first.val));
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
Ident(out p);
ids.Add(new IdentifierExpr(p, p.val));
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Ident(out p);
ids.Add(new IdentifierExpr(p, p.val));
}
}
- Expect(50);
+ Expect(51);
Ident(out first);
- Expect(9);
+ Expect(10);
if (StartOf(9)) {
Expression(out en);
es.Add(en);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out en);
es.Add(en);
}
}
- Expect(10);
+ Expect(11);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else SynErr(111);
+ } else SynErr(112);
}
void Expressions(out List<Expr>/*!*/ es) {
Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>();
Expression(out e);
es.Add(e);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
es.Add(e);
@@ -1366,7 +1368,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
if (StartOf(10)) {
- if (la.kind == 57 || la.kind == 58) {
+ if (la.kind == 58 || la.kind == 59) {
ImpliesOp();
x = t;
ImpliesExpression(true, out e1);
@@ -1378,7 +1380,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
x = t;
LogicalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 59 || la.kind == 60) {
+ while (la.kind == 60 || la.kind == 61) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -1389,23 +1391,23 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void EquivOp() {
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
- } else SynErr(112);
+ } else SynErr(113);
}
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(11)) {
- if (la.kind == 61 || la.kind == 62) {
+ if (la.kind == 62 || la.kind == 63) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 61 || la.kind == 62) {
+ while (la.kind == 62 || la.kind == 63) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1416,7 +1418,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 63 || la.kind == 64) {
+ while (la.kind == 64 || la.kind == 65) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1427,19 +1429,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void ImpliesOp() {
- if (la.kind == 57) {
+ if (la.kind == 58) {
Get();
- } else if (la.kind == 58) {
+ } else if (la.kind == 59) {
Get();
- } else SynErr(113);
+ } else SynErr(114);
}
void ExpliesOp() {
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
Get();
- } else SynErr(114);
+ } else SynErr(115);
}
void RelationalExpression(out Expr/*!*/ e0) {
@@ -1453,25 +1455,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void AndOp() {
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
Get();
- } else SynErr(115);
+ } else SynErr(116);
}
void OrOp() {
- if (la.kind == 63) {
+ if (la.kind == 64) {
Get();
- } else if (la.kind == 64) {
+ } else if (la.kind == 65) {
Get();
- } else SynErr(116);
+ } else SynErr(117);
}
void BvTerm(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
Term(out e0);
- while (la.kind == 73) {
+ while (la.kind == 74) {
Get();
x = t;
Term(out e1);
@@ -1482,64 +1484,64 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 65: {
+ case 66: {
Get();
x = t; op=BinaryOperator.Opcode.Eq;
break;
}
- case 19: {
+ case 20: {
Get();
x = t; op=BinaryOperator.Opcode.Lt;
break;
}
- case 20: {
+ case 21: {
Get();
x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 66: {
+ case 67: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 67: {
+ case 68: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 68: {
+ case 69: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 69: {
+ case 70: {
Get();
x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 70: {
+ case 71: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 71: {
+ case 72: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 72: {
+ case 73: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(117); break;
+ default: SynErr(118); break;
}
}
void Term(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Factor(out e0);
- while (la.kind == 74 || la.kind == 75) {
+ while (la.kind == 75 || la.kind == 76) {
AddOp(out x, out op);
Factor(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1558,19 +1560,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 74) {
+ if (la.kind == 75) {
Get();
x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(118);
+ } else SynErr(119);
}
void Power(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
UnaryExpression(out e0);
- if (la.kind == 79) {
+ if (la.kind == 80) {
Get();
x = t;
Power(out e1);
@@ -1580,46 +1582,46 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
Get();
x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 77) {
+ } else if (la.kind == 78) {
Get();
x = t; op=BinaryOperator.Opcode.Mod;
- } else if (la.kind == 78) {
+ } else if (la.kind == 79) {
Get();
x = t; op=BinaryOperator.Opcode.RealDiv;
- } else SynErr(119);
+ } else SynErr(120);
}
void UnaryExpression(out Expr/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
e = dummyExpr;
- if (la.kind == 75) {
+ if (la.kind == 76) {
Get();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
- } else if (la.kind == 80 || la.kind == 81) {
+ } else if (la.kind == 81 || la.kind == 82) {
NegOp();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(14)) {
CoercionExpression(out e);
- } else SynErr(120);
+ } else SynErr(121);
}
void NegOp() {
- if (la.kind == 80) {
+ if (la.kind == 81) {
Get();
- } else if (la.kind == 81) {
+ } else if (la.kind == 82) {
Get();
- } else SynErr(121);
+ } else SynErr(122);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1628,7 +1630,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
BigNum bn;
ArrayExpression(out e);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
x = t;
if (StartOf(6)) {
@@ -1643,7 +1645,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(122);
+ } else SynErr(123);
}
}
@@ -1654,7 +1656,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
List<Expr>/*!*/ allArgs = dummyExprSeq;
AtomExpression(out e);
- while (la.kind == 17) {
+ while (la.kind == 18) {
Get();
x = t; allArgs = new List<Expr> ();
allArgs.Add(e);
@@ -1667,7 +1669,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
else
allArgs.Add(index0);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1675,7 +1677,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
allArgs.Add(e1);
}
- if (la.kind == 50) {
+ if (la.kind == 51) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1689,7 +1691,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
allArgs.Add(e1); store = true;
}
}
- Expect(18);
+ Expect(19);
if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
else if (bvExtract)
@@ -1714,7 +1716,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; BigFloat bf;
List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
List<TypeVariable>/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1724,12 +1726,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
List<Block/*!*/>/*!*/ blocks;
switch (la.kind) {
- case 82: {
+ case 83: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 83: {
+ case 84: {
Get();
e = new LiteralExpr(t, true);
break;
@@ -1744,6 +1746,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new LiteralExpr(t, bd);
break;
}
+ case 7: {
+ Float(out bf);
+ e = new LiteralExpr(t, bf);
+ break;
+ }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1752,65 +1759,65 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
case 1: {
Ident(out x);
id = new IdentifierExpr(x, x.val); e = id;
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
if (StartOf(9)) {
Expressions(out es);
e = new NAryExpr(x, new FunctionCall(id), es);
- } else if (la.kind == 10) {
+ } else if (la.kind == 11) {
e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
- } else SynErr(123);
- Expect(10);
+ } else SynErr(124);
+ Expect(11);
}
break;
}
- case 84: {
+ case 85: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new OldExpr(x, e);
break;
}
- case 14: {
+ case 15: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e });
break;
}
- case 15: {
+ case 16: {
Get();
x = t;
- Expect(9);
- Expression(out e);
Expect(10);
+ Expression(out e);
+ Expect(11);
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
break;
}
- case 9: {
+ case 10: {
Get();
if (StartOf(9)) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (la.kind == 88 || la.kind == 89) {
+ } else if (la.kind == 89 || la.kind == 90) {
Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Count + ds.Count > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 90 || la.kind == 91) {
+ } else if (la.kind == 91 || la.kind == 92) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Count + ds.Count > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 92 || la.kind == 93) {
+ } else if (la.kind == 93 || la.kind == 94) {
Lambda();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1818,20 +1825,20 @@ 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(124);
- Expect(10);
+ } else SynErr(125);
+ Expect(11);
break;
}
- case 40: {
+ case 41: {
IfThenElseExpression(out e);
break;
}
- case 85: {
+ case 86: {
CodeExpression(out locals, out blocks);
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(125); break;
+ default: SynErr(126); break;
}
}
@@ -1843,7 +1850,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(126);
+ } else SynErr(127);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1853,6 +1860,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
+ void Float(out BigFloat n) {
+ string s = "";
+ Expect(7);
+ s = t.val;
+ try {
+ n = BigFloat.FromString(s);
+ } catch (FormatException e) {
+ this.SemErr("incorrectly formatted floating point, " + e.Message);
+ n = BigFloat.ZERO;
+ }
+
+ }
+
void BvLit(out BigNum n, out int m) {
Expect(2);
int pos = t.val.IndexOf("bv");
@@ -1870,11 +1890,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void Forall() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(127);
+ } else SynErr(128);
}
void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -1885,35 +1905,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
kv = null;
ds = new List<Variable> ();
- if (la.kind == 19) {
+ if (la.kind == 20) {
TypeParams(out tok, out typeParams);
- if (la.kind == 1 || la.kind == 27) {
+ if (la.kind == 1 || la.kind == 28) {
BoundVars(q, out ds);
}
- } else if (la.kind == 1 || la.kind == 27) {
+ } else if (la.kind == 1 || la.kind == 28) {
BoundVars(q, out ds);
- } else SynErr(128);
+ } else SynErr(129);
QSep();
- while (la.kind == 27) {
+ while (la.kind == 28) {
AttributeOrTrigger(ref kv, ref trig);
}
Expression(out body);
}
void Exists() {
- if (la.kind == 90) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(129);
+ } else SynErr(130);
}
void Lambda() {
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 94) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1921,12 +1941,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
IToken/*!*/ tok;
Expr/*!*/ e0, e1, e2;
e = dummyExpr;
- Expect(40);
+ Expect(41);
tok = t;
Expression(out e0);
- Expect(87);
+ Expect(88);
Expression(out e1);
- Expect(41);
+ Expect(42);
Expression(out e2);
e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 });
}
@@ -1935,8 +1955,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- Expect(85);
- while (la.kind == 7) {
+ Expect(86);
+ while (la.kind == 8) {
LocalVars(locals);
}
SpecBlock(out b);
@@ -1945,7 +1965,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
SpecBlock(out b);
blocks.Add(b);
}
- Expect(86);
+ Expect(87);
}
void SpecBlock(out Block/*!*/ b) {
@@ -1958,7 +1978,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expr/*!*/ e;
Ident(out x);
- Expect(11);
+ Expect(12);
while (StartOf(8)) {
LabelOrCmd(out c, out label);
if (c != null) {
@@ -1970,7 +1990,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
}
- if (la.kind == 38) {
+ if (la.kind == 39) {
Get();
y = t;
Idents(out xs);
@@ -1979,12 +1999,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
ss.Add(s.val); }
b = new Block(x,x.val,cs,new GotoCmd(y,ss));
- } else if (la.kind == 39) {
+ } else if (la.kind == 40) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(131);
- Expect(8);
+ } else SynErr(132);
+ Expect(9);
}
void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1992,16 +2012,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
string key;
List<object/*!*/> parameters; object/*!*/ param;
- Expect(27);
+ Expect(28);
tok = t;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
Expect(1);
key = t.val; parameters = new List<object/*!*/>();
if (StartOf(16)) {
AttributeParameter(out param);
parameters.Add(param);
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
AttributeParameter(out param);
parameters.Add(param);
@@ -2029,7 +2049,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
es = new List<Expr> { e };
- while (la.kind == 12) {
+ while (la.kind == 13) {
Get();
Expression(out e);
es.Add(e);
@@ -2040,8 +2060,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(132);
- Expect(28);
+ } else SynErr(133);
+ Expect(29);
}
void AttributeParameter(out object/*!*/ o) {
@@ -2055,15 +2075,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(133);
+ } else SynErr(134);
}
void QSep() {
- if (la.kind == 94) {
+ if (la.kind == 95) {
Get();
- } else if (la.kind == 95) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(134);
+ } else SynErr(135);
}
@@ -2079,23 +2099,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
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}
+ {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,T,x,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,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, 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,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,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,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,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,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,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,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, 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,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,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,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,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
@@ -2126,135 +2146,136 @@ public class Errors {
case 3: s = "digits expected"; break;
case 4: s = "string expected"; break;
case 5: s = "decimal expected"; break;
- case 6: s = "float expected"; break;
- case 7: s = "\"var\" expected"; break;
- case 8: s = "\";\" expected"; break;
- case 9: s = "\"(\" expected"; break;
- case 10: s = "\")\" expected"; break;
- case 11: s = "\":\" expected"; break;
- case 12: s = "\",\" expected"; break;
- case 13: s = "\"where\" expected"; break;
- case 14: s = "\"int\" expected"; break;
- case 15: s = "\"real\" expected"; break;
- case 16: s = "\"bool\" expected"; break;
- case 17: s = "\"[\" expected"; break;
- case 18: s = "\"]\" expected"; break;
- case 19: s = "\"<\" expected"; break;
- case 20: s = "\">\" expected"; break;
- case 21: s = "\"const\" expected"; break;
- case 22: s = "\"unique\" expected"; break;
- case 23: s = "\"extends\" expected"; break;
- case 24: s = "\"complete\" expected"; break;
- case 25: s = "\"function\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"{\" expected"; break;
- case 28: s = "\"}\" expected"; break;
- case 29: s = "\"axiom\" expected"; break;
- case 30: s = "\"type\" expected"; break;
- case 31: s = "\"=\" expected"; break;
- case 32: s = "\"procedure\" expected"; break;
- case 33: s = "\"implementation\" expected"; break;
- case 34: s = "\"modifies\" expected"; break;
- case 35: s = "\"free\" expected"; break;
- case 36: s = "\"requires\" expected"; break;
- case 37: s = "\"ensures\" expected"; break;
- case 38: s = "\"goto\" expected"; break;
- case 39: s = "\"return\" expected"; break;
- case 40: s = "\"if\" expected"; break;
- case 41: s = "\"else\" expected"; break;
- case 42: s = "\"while\" expected"; break;
- case 43: s = "\"invariant\" expected"; break;
- case 44: s = "\"*\" expected"; break;
- case 45: s = "\"break\" expected"; break;
- case 46: s = "\"assert\" expected"; break;
- case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\"yield\" expected"; break;
- case 50: s = "\":=\" expected"; break;
- case 51: s = "\"async\" expected"; break;
- case 52: s = "\"call\" expected"; break;
- case 53: s = "\"par\" expected"; break;
- case 54: s = "\"|\" expected"; break;
- case 55: s = "\"<==>\" expected"; break;
- case 56: s = "\"\\u21d4\" expected"; break;
- case 57: s = "\"==>\" expected"; break;
- case 58: s = "\"\\u21d2\" expected"; break;
- case 59: s = "\"<==\" expected"; break;
- case 60: s = "\"\\u21d0\" expected"; break;
- case 61: s = "\"&&\" expected"; break;
- case 62: s = "\"\\u2227\" expected"; break;
- case 63: s = "\"||\" expected"; break;
- case 64: s = "\"\\u2228\" expected"; break;
- case 65: s = "\"==\" expected"; break;
- case 66: s = "\"<=\" expected"; break;
- case 67: s = "\">=\" expected"; break;
- case 68: s = "\"!=\" expected"; break;
- case 69: s = "\"<:\" expected"; break;
- case 70: s = "\"\\u2260\" expected"; break;
- case 71: s = "\"\\u2264\" expected"; break;
- case 72: s = "\"\\u2265\" expected"; break;
- case 73: s = "\"++\" expected"; break;
- case 74: s = "\"+\" expected"; break;
- case 75: s = "\"-\" expected"; break;
- case 76: s = "\"div\" expected"; break;
- case 77: s = "\"mod\" expected"; break;
- case 78: s = "\"/\" expected"; break;
- case 79: s = "\"**\" expected"; break;
- case 80: s = "\"!\" expected"; break;
- case 81: s = "\"\\u00ac\" expected"; break;
- case 82: s = "\"false\" expected"; break;
- case 83: s = "\"true\" expected"; break;
- case 84: s = "\"old\" expected"; break;
- case 85: s = "\"|{\" expected"; break;
- case 86: s = "\"}|\" expected"; break;
- case 87: s = "\"then\" expected"; break;
- case 88: s = "\"forall\" expected"; break;
- case 89: s = "\"\\u2200\" expected"; break;
- case 90: s = "\"exists\" expected"; break;
- case 91: s = "\"\\u2203\" expected"; break;
- case 92: s = "\"lambda\" expected"; break;
- case 93: s = "\"\\u03bb\" expected"; break;
- case 94: s = "\"::\" expected"; break;
- case 95: s = "\"\\u2022\" expected"; break;
- case 96: s = "??? expected"; break;
- case 97: s = "invalid Function"; break;
+ case 6: s = "dec_float expected"; break;
+ case 7: s = "float expected"; break;
+ case 8: s = "\"var\" expected"; break;
+ case 9: s = "\";\" expected"; break;
+ case 10: s = "\"(\" expected"; break;
+ case 11: s = "\")\" expected"; break;
+ case 12: s = "\":\" expected"; break;
+ case 13: s = "\",\" expected"; break;
+ case 14: s = "\"where\" expected"; break;
+ case 15: s = "\"int\" expected"; break;
+ case 16: s = "\"real\" expected"; break;
+ case 17: s = "\"bool\" expected"; break;
+ case 18: s = "\"[\" expected"; break;
+ case 19: s = "\"]\" expected"; break;
+ case 20: s = "\"<\" expected"; break;
+ case 21: s = "\">\" expected"; break;
+ case 22: s = "\"const\" expected"; break;
+ case 23: s = "\"unique\" expected"; break;
+ case 24: s = "\"extends\" expected"; break;
+ case 25: s = "\"complete\" expected"; break;
+ case 26: s = "\"function\" expected"; break;
+ case 27: s = "\"returns\" expected"; break;
+ case 28: s = "\"{\" expected"; break;
+ case 29: s = "\"}\" expected"; break;
+ case 30: s = "\"axiom\" expected"; break;
+ case 31: s = "\"type\" expected"; break;
+ case 32: s = "\"=\" expected"; break;
+ case 33: s = "\"procedure\" expected"; break;
+ case 34: s = "\"implementation\" expected"; break;
+ case 35: s = "\"modifies\" expected"; break;
+ case 36: s = "\"free\" expected"; break;
+ case 37: s = "\"requires\" expected"; break;
+ case 38: s = "\"ensures\" expected"; break;
+ case 39: s = "\"goto\" expected"; break;
+ case 40: s = "\"return\" expected"; break;
+ case 41: s = "\"if\" expected"; break;
+ case 42: s = "\"else\" expected"; break;
+ case 43: s = "\"while\" expected"; break;
+ case 44: s = "\"invariant\" expected"; break;
+ case 45: s = "\"*\" expected"; break;
+ case 46: s = "\"break\" expected"; break;
+ case 47: s = "\"assert\" expected"; break;
+ case 48: s = "\"assume\" expected"; break;
+ case 49: s = "\"havoc\" expected"; break;
+ case 50: s = "\"yield\" expected"; break;
+ case 51: s = "\":=\" expected"; break;
+ case 52: s = "\"async\" expected"; break;
+ case 53: s = "\"call\" expected"; break;
+ case 54: s = "\"par\" expected"; break;
+ case 55: s = "\"|\" expected"; break;
+ case 56: s = "\"<==>\" expected"; break;
+ case 57: s = "\"\\u21d4\" expected"; break;
+ case 58: s = "\"==>\" expected"; break;
+ case 59: s = "\"\\u21d2\" expected"; break;
+ case 60: s = "\"<==\" expected"; break;
+ case 61: s = "\"\\u21d0\" expected"; break;
+ case 62: s = "\"&&\" expected"; break;
+ case 63: s = "\"\\u2227\" expected"; break;
+ case 64: s = "\"||\" expected"; break;
+ case 65: s = "\"\\u2228\" expected"; break;
+ case 66: s = "\"==\" expected"; break;
+ case 67: s = "\"<=\" expected"; break;
+ case 68: s = "\">=\" expected"; break;
+ case 69: s = "\"!=\" expected"; break;
+ case 70: s = "\"<:\" expected"; break;
+ case 71: s = "\"\\u2260\" expected"; break;
+ case 72: s = "\"\\u2264\" expected"; break;
+ case 73: s = "\"\\u2265\" expected"; break;
+ case 74: s = "\"++\" expected"; break;
+ case 75: s = "\"+\" expected"; break;
+ case 76: s = "\"-\" expected"; break;
+ case 77: s = "\"div\" expected"; break;
+ case 78: s = "\"mod\" expected"; break;
+ case 79: s = "\"/\" expected"; break;
+ case 80: s = "\"**\" expected"; break;
+ case 81: s = "\"!\" expected"; break;
+ case 82: s = "\"\\u00ac\" expected"; break;
+ case 83: s = "\"false\" expected"; break;
+ case 84: s = "\"true\" expected"; break;
+ case 85: s = "\"old\" expected"; break;
+ case 86: s = "\"|{\" expected"; break;
+ case 87: s = "\"}|\" expected"; break;
+ case 88: s = "\"then\" expected"; break;
+ case 89: s = "\"forall\" expected"; break;
+ case 90: s = "\"\\u2200\" expected"; break;
+ case 91: s = "\"exists\" expected"; break;
+ case 92: s = "\"\\u2203\" expected"; break;
+ case 93: s = "\"lambda\" expected"; break;
+ case 94: s = "\"\\u03bb\" expected"; break;
+ case 95: s = "\"::\" expected"; break;
+ case 96: s = "\"\\u2022\" expected"; break;
+ case 97: s = "??? expected"; 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 99: s = "invalid Function"; break;
+ case 100: s = "invalid Procedure"; break;
+ case 101: s = "invalid Type"; break;
+ case 102: s = "invalid TypeAtom"; break;
+ case 103: s = "invalid TypeArgs"; break;
+ case 104: s = "invalid Spec"; break;
+ case 105: s = "invalid SpecPrePost"; break;
+ case 106: s = "invalid LabelOrCmd"; break;
+ case 107: s = "invalid StructuredCmd"; break;
+ case 108: s = "invalid TransferCmd"; break;
+ case 109: s = "invalid IfCmd"; break;
+ case 110: s = "invalid Guard"; break;
+ case 111: s = "invalid LabelOrAssign"; break;
+ case 112: s = "invalid CallParams"; break;
+ case 113: s = "invalid EquivOp"; break;
+ case 114: s = "invalid ImpliesOp"; break;
+ case 115: s = "invalid ExpliesOp"; break;
+ case 116: s = "invalid AndOp"; break;
+ case 117: s = "invalid OrOp"; break;
+ case 118: s = "invalid RelOp"; break;
+ case 119: s = "invalid AddOp"; break;
+ case 120: s = "invalid MulOp"; break;
+ case 121: s = "invalid UnaryExpression"; break;
+ case 122: s = "invalid NegOp"; break;
+ case 123: s = "invalid CoercionExpression"; break;
case 124: s = "invalid AtomExpression"; break;
case 125: s = "invalid AtomExpression"; 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;
+ case 126: s = "invalid AtomExpression"; break;
+ case 127: s = "invalid Dec"; break;
+ case 128: s = "invalid Forall"; break;
+ case 129: s = "invalid QuantifierBody"; break;
+ case 130: s = "invalid Exists"; break;
+ case 131: s = "invalid Lambda"; break;
+ case 132: s = "invalid SpecBlock"; break;
+ case 133: s = "invalid AttributeOrTrigger"; break;
+ case 134: s = "invalid AttributeParameter"; break;
+ case 135: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 05:50:47 +0000