diff options
| author |  rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
| commit | fdef447cce5bdc57851cad1427f2a8e7cd7df35f (patch) | |
| tree | 0ba65512e599e44cb883d027a945375994bdc975 | |
| parent | c9c423ce3bde91f736266f8c9ae883b9e44acc70 (diff) | |
Start (some parsing and resolution) of adding algebraic datatypes to Dafny.
Included VSI-Benchmarks in standard tests.
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 122 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 76 | ||||
| -rw-r--r-- | Source/Dafny/DafnyMain.ssc | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 926 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 34 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 168 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 161 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 79 | ||||
| -rw-r--r-- | Test/alltests.txt | 1 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 18 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.bpl | 306 | ||||
| -rw-r--r-- | Test/dafny0/Simple.dfy | 21 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 4 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 4 |
15 files changed, 1295 insertions, 631 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 4eee233b..4e524175 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -190,6 +190,10 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } // ---------------------------------------------------------------
+type DatatypeType;
+
+// ---------------------------------------------------------------
+
type Field alpha;
type HeapType = <alpha>[ref,Field alpha]alpha;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5da2b44b..f68b59e1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -17,13 +17,14 @@ COMPILER Dafny /*--------------------------------------------------------------------------*/
-static List<ClassDecl!>! theClasses = new List<ClassDecl!>();
+static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope<string>! parseVarScope = new Scope<string>();
+static int anonymousIds = 0;
// helper routine for parsing call statements
private static void RecordCallLhs(IdentifierExpr! e,
@@ -52,7 +53,7 @@ private static Expression! ConvertToLocal(Expression! e) /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string! filename, List<ClassDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
@@ -61,12 +62,12 @@ public static int Parse (string! filename, List<ClassDecl!>! classes) /* throws }
///<summary>
-/// Parses top level declarations and appends them to "classes".
+/// Parses top-level declarations and appends them to "classes" [sic].
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<ClassDecl!>! classes) {
- List<ClassDecl!> oldClasses = theClasses;
+public static int Parse (List<TopLevelDecl!>! classes) {
+ List<TopLevelDecl!> oldClasses = theClasses;
theClasses = classes;
Parse();
theClasses = oldClasses;
@@ -107,8 +108,9 @@ IGNORE cr + lf + tab PRODUCTIONS
Dafny
-= (. ClassDecl! c; .)
+= (. ClassDecl! c; DatatypeDecl! dt; .)
{ ClassDecl<out c> (. theClasses.Add(c); .)
+ | DatatypeDecl<out dt> (. theClasses.Add(dt); .)
}
EOF
.
@@ -140,6 +142,39 @@ ClassMemberDecl<List<MemberDecl!\>! mm> )
.
+DatatypeDecl<out DatatypeDecl! dt>
+= (. Token! id;
+ Attributes attrs = null;
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
+ .)
+ "datatype"
+ { Attribute<ref attrs> }
+ Ident<out id>
+ [ GenericParameters<typeArgs> ]
+ "{"
+ { DatatypeMemberDecl<ctors>
+ }
+ "}" (. dt = new DatatypeDecl(id, id.val, typeArgs, ctors, attrs); .)
+ .
+
+DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
+= (. Attributes attrs = null;
+ Token! id;
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ List<Formal!> formals = new List<Formal!>();
+ .)
+ { Attribute<ref attrs> }
+ Ident<out id>
+ [ GenericParameters<typeArgs> ]
+ (. parseVarScope.PushMarker(); .)
+ [ FormalsOptionalIds<formals> ]
+ (. parseVarScope.PopMarker();
+ ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
+ .)
+ ";"
+ .
+
FieldDecl<List<MemberDecl!\>! mm>
= (. Attributes attrs = null;
Token! id; Type! ty;
@@ -167,6 +202,28 @@ IdentTypeOptional<out BoundVar! var> (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
+TypeIdentOptional<out Token! id, out string! identName, out Type! ty>
+= (. string name = null; .)
+ TypeAndToken<out id, out ty>
+ [ ":"
+ (. /* try to convert ty to an identifier */
+ UserDefinedType udt = ty as UserDefinedType;
+ if (udt != null && udt.TypeArgs.Count == 0) {
+ name = udt.Name;
+ } else {
+ SemErr(id, "invalid formal-parameter name in datatype constructor");
+ }
+ .)
+ Type<out ty>
+ ]
+ (. if (name != null) {
+ identName = name;
+ } else {
+ identName = "#" + anonymousIds++;
+ }
+ .)
+ .
+
/*------------------------------------------------------------------------*/
GenericParameters<List<TypeParameter!\>! typeArgs>
@@ -248,43 +305,54 @@ Formals<bool incoming, List<Formal!\>! formals> ")"
.
+FormalsOptionalIds<List<Formal!\>! formals>
+= (. Token! id; Type! ty; string! name; .)
+ "("
+ [
+ TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .)
+ { "," TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .)
+ }
+ ]
+ ")"
+ .
+
/*------------------------------------------------------------------------*/
Type<out Type! ty>
-= (. ty = new BoolType(); /*keep compiler happy*/
- .)
- ( "bool" (. /* yeah, that's it! */ .)
- | "int" (. ty = new IntType(); .)
- | ReferenceType<out ty>
- )
+= (. Token! tok; .)
+ TypeAndToken<out tok, out ty>
.
-ReferenceType<out Type! ty>
-= (. Token! x;
- ty = new BoolType(); /*keep compiler happy*/
+TypeAndToken<out Token! tok, out Type! ty>
+= (. tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
.)
- ( "object" (. ty = new ObjectType(); .)
-
- | (. gt = new List<Type!>(); .)
- Ident<out x>
- [ GenericInstantiation<gt> ] (. ty = new ClassType(x, x.val, gt); .)
-
- | (. gt = new List<Type!>(); .)
- "set"
+ ( "bool" (. tok = token; .)
+ | "int" (. tok = token; ty = new IntType(); .)
+ | "set" (. tok = token; gt = new List<Type!>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
}
ty = new SetType(gt[0]);
.)
- | (. gt = new List<Type!>(); .)
- "seq"
+ | "seq" (. tok = token; gt = new List<Type!>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
ty = new SeqType(gt[0]);
.)
+ | ReferenceType<out tok, out ty>
+ )
+ .
+
+ReferenceType<out Token! tok, out Type! ty>
+= (. tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type!>! gt;
+ .)
+ ( "object" (. tok = token; ty = new ObjectType(); .)
+ | Ident<out tok> (. gt = new List<Type!>(); .)
+ [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
.
@@ -434,10 +502,10 @@ AssignStmt<out Statement! s> AssignRhs<out Expression e, out Type ty>
/* ensures e == null <==> ty == null; */
-= (. Expression! ee; Type! tt;
+= (. Token! x; Expression! ee; Type! tt;
e = null; ty = null;
.)
- ( "new" ReferenceType<out tt> (. ty = tt; .)
+ ( "new" ReferenceType<out x, out tt> (. ty = tt; .)
| Expression<out ee> (. e = ee; .)
) (. if (e == null && ty == null) { e = dummyExpr; } .)
.
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index f50ded86..92854bc5 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -11,8 +11,8 @@ namespace Microsoft.Dafny {
public class Program {
public readonly string! Name;
- public readonly List<ClassDecl!>! Classes;
- public Program(string! name, [Captured] List<ClassDecl!>! classes) {
+ public readonly List<TopLevelDecl!>! Classes;
+ public Program(string! name, [Captured] List<TopLevelDecl!>! classes) {
Name = name;
Classes = classes;
}
@@ -62,16 +62,22 @@ namespace Microsoft.Dafny if (this is ObjectType) {
return true;
} else {
- ClassType ct = this as ClassType;
- return ct != null && ct.ResolvedParam == null;
+ UserDefinedType udt = this as UserDefinedType;
+ return udt != null && udt.ResolvedParam == null && !(udt.ResolvedClass is DatatypeDecl);
}
}
}
+ public bool IsDatatype {
+ get {
+ UserDefinedType udt = this as UserDefinedType;
+ return udt != null && udt.ResolvedClass is DatatypeDecl;
+ }
+ }
public bool IsTypeParameter {
get
- ensures result ==> this is ClassType && ((ClassType)this).ResolvedParam != null;
+ ensures result ==> this is UserDefinedType && ((UserDefinedType)this).ResolvedParam != null;
{
- ClassType ct = this as ClassType;
+ UserDefinedType ct = this as UserDefinedType;
return ct != null && ct.ResolvedParam != null;
}
}
@@ -125,15 +131,15 @@ namespace Microsoft.Dafny }
}
- public class ClassType : Type {
+ public class UserDefinedType : Type {
public readonly Token! tok;
public readonly string! Name;
[Rep] public readonly List<Type!>! TypeArgs;
- public ClassDecl ResolvedClass; // filled in by resolution, if Name denotes a class and TypeArgs match the type parameters of that class
+ public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public ClassType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {
+ public UserDefinedType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
@@ -142,7 +148,7 @@ namespace Microsoft.Dafny /// <summary>
/// This constructor constructs a resolved class type
/// </summary>
- public ClassType(Token! tok, string! name, ClassDecl! cd, [Captured] List<Type!>! typeArgs) {
+ public UserDefinedType(Token! tok, string! name, TopLevelDecl! cd, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
@@ -152,7 +158,7 @@ namespace Microsoft.Dafny /// <summary>
/// This constructor constructs a resolved type parameter
/// </summary>
- public ClassType(Token! tok, string! name, TypeParameter! tp) {
+ public UserDefinedType(Token! tok, string! name, TypeParameter! tp) {
this.tok = tok;
this.Name = name;
this.TypeArgs = new List<Type!>();
@@ -163,8 +169,8 @@ namespace Microsoft.Dafny /// If type denotes a resolved class type, then return that class type.
/// Otherwise, return null.
/// </summary>
- public static ClassType DenotesClass(Type! type)
- ensures result != null ==> result.ResolvedClass != null;
+ public static UserDefinedType DenotesClass(Type! type)
+ ensures result != null ==> result.ResolvedClass is ClassDecl;
{
while (true)
invariant type.IsPeerConsistent;
@@ -177,8 +183,8 @@ namespace Microsoft.Dafny break;
}
}
- ClassType ct = type as ClassType;
- if (ct != null && ct.ResolvedClass != null) {
+ UserDefinedType ct = type as UserDefinedType;
+ if (ct != null && ct.ResolvedClass is ClassDecl) {
return ct;
} else {
return null;
@@ -305,7 +311,7 @@ namespace Microsoft.Dafny // BUGBUG: The following line is a workaround to tell the verifier that 'value' is not of an Immutable type.
// A proper solution would be to be able to express that in the program (in a specification or attribute) or
// to be able to declare 'parent' as [PeerOrImmutable].
- requires value is ClassDecl || value is Function || value is Method;
+ requires value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor;
modifies parent;
{
parent = value;
@@ -316,13 +322,43 @@ namespace Microsoft.Dafny }
}
- public class ClassDecl : Declaration, TypeParameter.ParentType {
- public List<TypeParameter!>! TypeArgs;
- public List<MemberDecl!>! Members;
+ public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
+ public readonly List<TypeParameter!>! TypeArgs;
- public ClassDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
+ public TopLevelDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, Attributes attributes) {
TypeArgs = typeArgs;
+ base(tok, name, attributes);
+ }
+ }
+
+ public class ClassDecl : TopLevelDecl {
+ public readonly List<MemberDecl!>! Members;
+
+ public ClassDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
Members = members;
+ base(tok, name, typeArgs, attributes);
+ }
+ }
+
+ public class DatatypeDecl : TopLevelDecl {
+ public readonly List<DatatypeCtor!>! Ctors;
+
+ public DatatypeDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
+ Ctors = ctors;
+ base(tok, name, typeArgs, attributes);
+ }
+ }
+
+ public class DatatypeCtor : Declaration, TypeParameter.ParentType {
+ public readonly List<TypeParameter!>! TypeArgs;
+ public readonly List<Formal!>! Formals;
+ // Todo: One could imagine having a precondition on datatype constructors
+ public DatatypeDecl EnclosingDatatype; // filled in during resolution
+
+ public DatatypeCtor(Token! tok, string! name, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals,
+ Attributes attributes) {
+ this.TypeArgs = typeArgs;
+ this.Formals = formals;
base(tok, name, attributes);
}
}
diff --git a/Source/Dafny/DafnyMain.ssc b/Source/Dafny/DafnyMain.ssc index 84e366e2..9bf132d3 100644 --- a/Source/Dafny/DafnyMain.ssc +++ b/Source/Dafny/DafnyMain.ssc @@ -19,7 +19,7 @@ namespace Microsoft.Dafny { {
program = null;
Dafny.Errors.count = 0;
- List<ClassDecl!> classes = new List<ClassDecl!>();
+ List<TopLevelDecl!> classes = new List<TopLevelDecl!>();
foreach (string! dafnyFileName in fileNames){
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 6b12d796..83665027 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -5,7 +5,7 @@ using Microsoft.Contracts; namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 87;
+ const int maxT = 88;
const bool T = true;
const bool x = false;
@@ -15,13 +15,14 @@ public class Parser { static Token/*!*/ t; // lookahead token
static int errDist = minErrDist;
- static List<ClassDecl!>! theClasses = new List<ClassDecl!>();
+ static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope<string>! parseVarScope = new Scope<string>();
+static int anonymousIds = 0;
// helper routine for parsing call statements
private static void RecordCallLhs(IdentifierExpr! e,
@@ -50,7 +51,7 @@ private static Expression! ConvertToLocal(Expression! e) /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string! filename, List<ClassDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
@@ -59,12 +60,12 @@ public static int Parse (string! filename, List<ClassDecl!>! classes) /* throws }
///<summary>
-/// Parses top level declarations and appends them to "classes".
+/// Parses top-level declarations and appends them to "classes" [sic].
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<ClassDecl!>! classes) {
- List<ClassDecl!> oldClasses = theClasses;
+public static int Parse (List<TopLevelDecl!>! classes) {
+ List<TopLevelDecl!> oldClasses = theClasses;
theClasses = classes;
Parse();
theClasses = oldClasses;
@@ -130,10 +131,15 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void Dafny() {
- ClassDecl! c;
- while (t.kind == 4) {
- ClassDecl(out c);
- theClasses.Add(c);
+ ClassDecl! c; DatatypeDecl! dt;
+ while (t.kind == 4 || t.kind == 7) {
+ if (t.kind == 4) {
+ ClassDecl(out c);
+ theClasses.Add(c);
+ } else {
+ DatatypeDecl(out dt);
+ theClasses.Add(dt);
+ }
}
Expect(0);
}
@@ -149,7 +155,7 @@ public static int Parse (List<ClassDecl!>! classes) { Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 11) {
+ if (t.kind == 12) {
GenericParameters(typeArgs);
}
Expect(5);
@@ -160,6 +166,28 @@ public static int Parse (List<ClassDecl!>! classes) { c = new ClassDecl(id, id.val, typeArgs, members, attrs);
}
+ static void DatatypeDecl(out DatatypeDecl! dt) {
+ Token! id;
+ Attributes attrs = null;
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
+
+ Expect(7);
+ while (t.kind == 5) {
+ Attribute(ref attrs);
+ }
+ Ident(out id);
+ if (t.kind == 12) {
+ GenericParameters(typeArgs);
+ }
+ Expect(5);
+ while (t.kind == 1 || t.kind == 5) {
+ DatatypeMemberDecl(ctors);
+ }
+ Expect(6);
+ dt = new DatatypeDecl(id, id.val, typeArgs, ctors, attrs);
+ }
+
static void Attribute(ref Attributes attrs) {
Expect(5);
AttributeBody(ref attrs);
@@ -173,50 +201,50 @@ public static int Parse (List<ClassDecl!>! classes) { static void GenericParameters(List<TypeParameter!>! typeArgs) {
Token! id;
- Expect(11);
+ Expect(12);
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
}
- Expect(12);
+ Expect(13);
}
static void ClassMemberDecl(List<MemberDecl!>! mm) {
Method! m;
Function! f;
- if (t.kind == 7) {
+ if (t.kind == 9) {
FieldDecl(mm);
- } else if (t.kind == 27) {
+ } else if (t.kind == 28) {
FunctionDecl(out f);
mm.Add(f);
- } else if (t.kind == 14) {
+ } else if (t.kind == 15) {
MethodDecl(out m);
mm.Add(m);
- } else if (t.kind == 13) {
+ } else if (t.kind == 14) {
FrameDecl();
- } else Error(88);
+ } else Error(89);
}
static void FieldDecl(List<MemberDecl!>! mm) {
Attributes attrs = null;
Token! id; Type! ty;
- Expect(7);
+ Expect(9);
while (t.kind == 5) {
Attribute(ref attrs);
}
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, ty, attrs));
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, ty, attrs));
}
- Expect(9);
+ Expect(8);
}
static void FunctionDecl(out Function! f) {
@@ -230,34 +258,34 @@ public static int Parse (List<ClassDecl!>! classes) { Expression! bb; Expression body = null;
bool use = false;
- Expect(27);
+ Expect(28);
while (t.kind == 5) {
Attribute(ref attrs);
}
- if (t.kind == 28) {
+ if (t.kind == 29) {
Get();
use = true;
}
Ident(out id);
- if (t.kind == 11) {
+ if (t.kind == 12) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, formals);
- Expect(10);
+ Expect(11);
Type(out returnType);
- if (t.kind == 9) {
+ if (t.kind == 8) {
Get();
- while (t.kind == 18 || t.kind == 29) {
+ while (t.kind == 19 || t.kind == 30) {
FunctionSpec(reqs, reads);
}
- } else if (t.kind == 5 || t.kind == 18 || t.kind == 29) {
- while (t.kind == 18 || t.kind == 29) {
+ } else if (t.kind == 5 || t.kind == 19 || t.kind == 30) {
+ while (t.kind == 19 || t.kind == 30) {
FunctionSpec(reqs, reads);
}
ExtendedExpr(out bb);
body = bb;
- } else Error(89);
+ } else Error(90);
parseVarScope.PopMarker();
f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
@@ -274,21 +302,21 @@ public static int Parse (List<ClassDecl!>! classes) { List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
Statement! bb; Statement body = null;
- Expect(14);
+ Expect(15);
while (t.kind == 5) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 11) {
+ if (t.kind == 12) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, ins);
- if (t.kind == 15) {
+ if (t.kind == 16) {
Get();
Formals(false, outs);
}
- if (t.kind == 9) {
+ if (t.kind == 8) {
Get();
while (StartOf(2)) {
MethodSpec(req, mod, ens);
@@ -299,7 +327,7 @@ public static int Parse (List<ClassDecl!>! classes) { }
BlockStmt(out bb);
body = bb;
- } else Error(90);
+ } else Error(91);
parseVarScope.PopMarker();
m = new Method(id, id.val, typeArgs, ins, outs, req, mod, ens, body, attrs);
@@ -309,7 +337,7 @@ public static int Parse (List<ClassDecl!>! classes) { Token! id;
Attributes attrs = null;
- Expect(13);
+ Expect(14);
while (t.kind == 5) {
Attribute(ref attrs);
}
@@ -318,31 +346,60 @@ public static int Parse (List<ClassDecl!>! classes) { Expect(6);
}
+ static void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {
+ Attributes attrs = null;
+ Token! id;
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ List<Formal!> formals = new List<Formal!>();
+
+ while (t.kind == 5) {
+ Attribute(ref attrs);
+ }
+ Ident(out id);
+ if (t.kind == 12) {
+ GenericParameters(typeArgs);
+ }
+ parseVarScope.PushMarker();
+ if (t.kind == 21) {
+ FormalsOptionalIds(formals);
+ }
+ parseVarScope.PopMarker();
+ ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
+
+ Expect(8);
+ }
+
+ static void FormalsOptionalIds(List<Formal!>! formals) {
+ Token! id; Type! ty; string! name;
+ Expect(21);
+ if (StartOf(4)) {
+ TypeIdentOptional(out id, out name, out ty);
+ formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name);
+ while (t.kind == 10) {
+ Get();
+ TypeIdentOptional(out id, out name, out ty);
+ formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name);
+ }
+ }
+ Expect(22);
+ }
+
static void IdentType(out Token! id, out Type! ty) {
Ident(out id);
- Expect(10);
+ Expect(11);
Type(out ty);
}
static void Type(out Type! ty) {
- ty = new BoolType(); /*keep compiler happy*/
-
- if (t.kind == 22) {
- Get();
-
- } else if (t.kind == 23) {
- Get();
- ty = new IntType();
- } else if (StartOf(4)) {
- ReferenceType(out ty);
- } else Error(91);
+ Token! tok;
+ TypeAndToken(out tok, out ty);
}
static void IdentTypeOptional(out BoundVar! var) {
Token! id; Type! ty; Type optType = null;
Ident(out id);
- if (t.kind == 10) {
+ if (t.kind == 11) {
Get();
Type(out ty);
optType = ty;
@@ -350,53 +407,108 @@ public static int Parse (List<ClassDecl!>! classes) { var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
}
+ static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty) {
+ string name = null;
+ TypeAndToken(out id, out ty);
+ if (t.kind == 11) {
+ Get();
+ UserDefinedType udt = ty as UserDefinedType;
+ if (udt != null && udt.TypeArgs.Count == 0) {
+ name = udt.Name;
+ } else {
+ SemErr(id, "invalid formal-parameter name in datatype constructor");
+ }
+
+ Type(out ty);
+ }
+ if (name != null) {
+ identName = name;
+ } else {
+ identName = "#" + anonymousIds++;
+ }
+
+ }
+
+ static void TypeAndToken(out Token! tok, out Type! ty) {
+ tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type!>! gt;
+
+ if (t.kind == 23) {
+ Get();
+ tok = token;
+ } else if (t.kind == 24) {
+ Get();
+ tok = token; ty = new IntType();
+ } else if (t.kind == 25) {
+ Get();
+ tok = token; gt = new List<Type!>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("set type expects exactly one type argument");
+ }
+ ty = new SetType(gt[0]);
+
+ } else if (t.kind == 26) {
+ Get();
+ tok = token; gt = new List<Type!>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("seq type expects exactly one type argument");
+ }
+ ty = new SeqType(gt[0]);
+
+ } else if (t.kind == 1 || t.kind == 27) {
+ ReferenceType(out tok, out ty);
+ } else Error(92);
+ }
+
static void Formals(bool incoming, List<Formal!>! formals) {
Token! id; Type! ty;
- Expect(20);
+ Expect(21);
if (t.kind == 1) {
IdentType(out id, out ty);
formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
IdentType(out id, out ty);
formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val);
}
}
- Expect(21);
+ Expect(22);
}
static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens) {
Expression! e; bool isFree = false;
- if (t.kind == 16) {
+ if (t.kind == 17) {
Get();
if (StartOf(5)) {
Expression(out e);
mod.Add(e);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Expression(out e);
mod.Add(e);
}
}
- Expect(9);
- } else if (t.kind == 17 || t.kind == 18 || t.kind == 19) {
- if (t.kind == 17) {
+ Expect(8);
+ } else if (t.kind == 18 || t.kind == 19 || t.kind == 20) {
+ if (t.kind == 18) {
Get();
isFree = true;
}
- if (t.kind == 18) {
+ if (t.kind == 19) {
Get();
Expression(out e);
- Expect(9);
+ Expect(8);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (t.kind == 19) {
+ } else if (t.kind == 20) {
Get();
Expression(out e);
- Expect(9);
+ Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(92);
- } else Error(93);
+ } else Error(93);
+ } else Error(94);
}
static void BlockStmt(out Statement! block) {
@@ -418,7 +530,7 @@ public static int Parse (List<ClassDecl!>! classes) { static void Expression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 48 || t.kind == 49) {
+ while (t.kind == 49 || t.kind == 50) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -426,91 +538,72 @@ public static int Parse (List<ClassDecl!>! classes) { }
}
- static void ReferenceType(out Type! ty) {
- Token! x;
- ty = new BoolType(); /*keep compiler happy*/
- List<Type!>! gt;
-
- if (t.kind == 24) {
- Get();
- ty = new ObjectType();
- } else if (t.kind == 1) {
- gt = new List<Type!>();
- Ident(out x);
- if (t.kind == 11) {
- GenericInstantiation(gt);
- }
- ty = new ClassType(x, x.val, gt);
- } else if (t.kind == 25) {
- gt = new List<Type!>();
- Get();
- GenericInstantiation(gt);
- if (gt.Count != 1) {
- SemErr("set type expects exactly one type argument");
- }
- ty = new SetType(gt[0]);
-
- } else if (t.kind == 26) {
- gt = new List<Type!>();
- Get();
- GenericInstantiation(gt);
- if (gt.Count != 1) {
- SemErr("seq type expects exactly one type argument");
- }
- ty = new SeqType(gt[0]);
-
- } else Error(94);
- }
-
static void GenericInstantiation(List<Type!>! gt) {
Type! ty;
- Expect(11);
+ Expect(12);
Type(out ty);
gt.Add(ty);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(12);
+ Expect(13);
+ }
+
+ static void ReferenceType(out Token! tok, out Type! ty) {
+ tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type!>! gt;
+
+ if (t.kind == 27) {
+ Get();
+ tok = token; ty = new ObjectType();
+ } else if (t.kind == 1) {
+ Ident(out tok);
+ gt = new List<Type!>();
+ if (t.kind == 12) {
+ GenericInstantiation(gt);
+ }
+ ty = new UserDefinedType(tok, tok.val, gt);
+ } else Error(95);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads) {
Expression! e;
- if (t.kind == 18) {
+ if (t.kind == 19) {
Get();
Expression(out e);
- Expect(9);
+ Expect(8);
reqs.Add(e);
- } else if (t.kind == 29) {
+ } else if (t.kind == 30) {
ReadsClause(reads);
- } else Error(95);
+ } else Error(96);
}
static void ExtendedExpr(out Expression! e) {
e = dummyExpr;
Expect(5);
- if (t.kind == 30) {
+ if (t.kind == 31) {
IfThenElseExpr(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(96);
+ } else Error(97);
Expect(6);
}
static void ReadsClause(List<Expression!>! reads) {
- Expect(29);
+ Expect(30);
if (StartOf(5)) {
Expressions(reads);
}
- Expect(9);
+ Expect(8);
}
static void Expressions(List<Expression!>! args) {
Expression! e;
Expression(out e);
args.Add(e);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Expression(out e);
args.Add(e);
@@ -519,18 +612,18 @@ public static int Parse (List<ClassDecl!>! classes) { static void IfThenElseExpr(out Expression! e) {
Token! x; Expression! e0; Expression! e1 = dummyExpr;
- Expect(30);
+ Expect(31);
x = token;
- Expect(20);
- Expression(out e);
Expect(21);
+ Expression(out e);
+ Expect(22);
ExtendedExpr(out e0);
- Expect(31);
- if (t.kind == 30) {
+ Expect(32);
+ if (t.kind == 31) {
IfThenElseExpr(out e1);
} else if (t.kind == 5) {
ExtendedExpr(out e1);
- } else Error(97);
+ } else Error(98);
e = new ITEExpr(x, e, e0, e1);
}
@@ -543,9 +636,9 @@ public static int Parse (List<ClassDecl!>! classes) { if (StartOf(7)) {
OneStmt(out s);
ss.Add(s);
- } else if (t.kind == 7) {
+ } else if (t.kind == 9) {
VarDeclStmts(ss);
- } else Error(98);
+ } else Error(99);
}
static void OneStmt(out Statement! s) {
@@ -553,109 +646,109 @@ public static int Parse (List<ClassDecl!>! classes) { s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 46: {
+ case 47: {
AssertStmt(out s);
break;
}
- case 47: {
+ case 48: {
AssumeStmt(out s);
break;
}
- case 28: {
+ case 29: {
UseStmt(out s);
break;
}
- case 1: case 2: case 5: case 20: case 45: case 66: case 69: case 70: case 71: case 72: case 73: case 74: case 75: case 79: case 80: {
+ case 1: case 2: case 5: case 21: case 46: case 67: case 70: case 71: case 72: case 73: case 74: case 75: case 76: case 80: case 81: {
AssignStmt(out s);
break;
}
- case 37: {
+ case 38: {
HavocStmt(out s);
break;
}
- case 42: {
+ case 43: {
CallStmt(out s);
break;
}
- case 30: {
+ case 31: {
IfStmt(out s);
break;
}
- case 38: {
+ case 39: {
WhileStmt(out s);
break;
}
- case 43: {
+ case 44: {
ForeachStmt(out s);
break;
}
- case 32: {
+ case 33: {
Get();
x = token;
Ident(out id);
- Expect(10);
+ Expect(11);
s = new LabelStmt(x, id.val);
break;
}
- case 33: {
+ case 34: {
Get();
x = token;
if (t.kind == 1) {
Ident(out id);
label = id.val;
}
- Expect(9);
+ Expect(8);
s = new BreakStmt(x, label);
break;
}
- case 34: {
+ case 35: {
Get();
x = token;
- Expect(9);
+ Expect(8);
s = new ReturnStmt(x);
break;
}
- default: Error(99); break;
+ default: Error(100); break;
}
}
static void VarDeclStmts(List<Statement!>! ss) {
VarDecl! d;
- Expect(7);
+ Expect(9);
IdentTypeRhs(out d);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
IdentTypeRhs(out d);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
}
- Expect(9);
+ Expect(8);
}
static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(46);
+ Expect(47);
x = token;
Expression(out e);
- Expect(9);
+ Expect(8);
s = new AssertStmt(x, e);
}
static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(47);
+ Expect(48);
x = token;
Expression(out e);
- Expect(9);
+ Expect(8);
s = new AssumeStmt(x, e);
}
static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(28);
+ Expect(29);
x = token;
Expression(out e);
- Expect(9);
+ Expect(8);
s = new UseStmt(x, e);
}
@@ -667,7 +760,7 @@ public static int Parse (List<ClassDecl!>! classes) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(35);
+ Expect(36);
x = token;
AssignRhs(out rhs, out ty);
if (rhs != null) {
@@ -677,15 +770,15 @@ public static int Parse (List<ClassDecl!>! classes) { s = new AssignStmt(x, lhs, ty);
}
- Expect(9);
+ Expect(8);
}
static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(37);
+ Expect(38);
x = token;
LhsExpr(out lhs);
- Expect(9);
+ Expect(8);
s = new AssignStmt(x, lhs);
}
@@ -695,11 +788,11 @@ public static int Parse (List<ClassDecl!>! classes) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<VarDecl!> newVars = new List<VarDecl!>();
- Expect(42);
+ Expect(43);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 8 || t.kind == 35) {
- if (t.kind == 8) {
+ if (t.kind == 10 || t.kind == 36) {
+ if (t.kind == 10) {
Get();
e = ConvertToLocal(e);
if (e is IdentifierExpr) {
@@ -712,12 +805,12 @@ public static int Parse (List<ClassDecl!>! classes) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(35);
+ Expect(36);
CallStmtSubExpr(out e);
} else {
Get();
@@ -733,7 +826,7 @@ public static int Parse (List<ClassDecl!>! classes) { CallStmtSubExpr(out e);
}
}
- Expect(9);
+ Expect(8);
if (e is FunctionCallExpr) {
FunctionCallExpr fce = (FunctionCallExpr)e;
s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args); // this actually does an ownership transfer of fce.Args
@@ -751,19 +844,19 @@ public static int Parse (List<ClassDecl!>! classes) { Statement! s;
Statement els = null;
- Expect(30);
+ Expect(31);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 31) {
+ if (t.kind == 32) {
Get();
- if (t.kind == 30) {
+ if (t.kind == 31) {
IfStmt(out s);
els = s;
} else if (t.kind == 5) {
BlockStmt(out s);
els = s;
- } else Error(100);
+ } else Error(101);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -776,31 +869,31 @@ public static int Parse (List<ClassDecl!>! classes) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(38);
+ Expect(39);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 17 || t.kind == 39 || t.kind == 40) {
- if (t.kind == 17 || t.kind == 39) {
+ while (t.kind == 18 || t.kind == 40 || t.kind == 41) {
+ if (t.kind == 18 || t.kind == 40) {
isFree = false;
- if (t.kind == 17) {
+ if (t.kind == 18) {
Get();
isFree = true;
}
- Expect(39);
+ Expect(40);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
- Expect(9);
+ Expect(8);
} else {
Get();
Expression(out e);
decreases.Add(e);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
Expression(out e);
decreases.Add(e);
}
- Expect(9);
+ Expect(8);
}
}
BlockStmt(out body);
@@ -816,31 +909,31 @@ public static int Parse (List<ClassDecl!>! classes) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(43);
+ Expect(44);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(20);
+ Expect(21);
Ident(out boundVar);
- if (t.kind == 10) {
+ if (t.kind == 11) {
Get();
Type(out ty);
}
- Expect(44);
+ Expect(45);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 45) {
+ if (t.kind == 46) {
Get();
Expression(out range);
}
- Expect(21);
+ Expect(22);
Expect(5);
- while (t.kind == 28 || t.kind == 46 || t.kind == 47) {
- if (t.kind == 46) {
+ while (t.kind == 29 || t.kind == 47 || t.kind == 48) {
+ if (t.kind == 47) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 47) {
+ } else if (t.kind == 48) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -851,10 +944,10 @@ public static int Parse (List<ClassDecl!>! classes) { if (StartOf(5)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 37) {
+ } else if (t.kind == 38) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(101);
+ } else Error(102);
Expect(6);
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
parseVarScope.PopMarker();
@@ -865,17 +958,17 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void AssignRhs(out Expression e, out Type ty) {
- Expression! ee; Type! tt;
+ Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 36) {
+ if (t.kind == 37) {
Get();
- ReferenceType(out tt);
+ ReferenceType(out x, out tt);
ty = tt;
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(102);
+ } else Error(103);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -885,12 +978,12 @@ public static int Parse (List<ClassDecl!>! classes) { Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
Ident(out id);
- if (t.kind == 10) {
+ if (t.kind == 11) {
Get();
Type(out ty);
optionalType = ty;
}
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -908,26 +1001,26 @@ public static int Parse (List<ClassDecl!>! classes) { static void Guard(out Expression e) {
Expression! ee; e = null;
- Expect(20);
- if (t.kind == 41) {
+ Expect(21);
+ if (t.kind == 42) {
Get();
e = null;
} else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(103);
- Expect(21);
+ } else Error(104);
+ Expect(22);
}
static void CallStmtSubExpr(out Expression! e) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 20 || t.kind == 79 || t.kind == 80) {
+ } else if (t.kind == 21 || t.kind == 80 || t.kind == 81) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(104);
- while (t.kind == 75 || t.kind == 77) {
+ } else Error(105);
+ while (t.kind == 76 || t.kind == 78) {
SelectOrCallSuffix(ref e);
}
}
@@ -935,7 +1028,7 @@ public static int Parse (List<ClassDecl!>! classes) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 50 || t.kind == 51) {
+ if (t.kind == 51 || t.kind == 52) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -944,23 +1037,23 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void EquivOp() {
- if (t.kind == 48) {
+ if (t.kind == 49) {
Get();
- } else if (t.kind == 49) {
+ } else if (t.kind == 50) {
Get();
- } else Error(105);
+ } else Error(106);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(8)) {
- if (t.kind == 52 || t.kind == 53) {
+ if (t.kind == 53 || t.kind == 54) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 52 || t.kind == 53) {
+ while (t.kind == 53 || t.kind == 54) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -971,7 +1064,7 @@ public static int Parse (List<ClassDecl!>! classes) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 54 || t.kind == 55) {
+ while (t.kind == 55 || t.kind == 56) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -982,11 +1075,11 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void ImpliesOp() {
- if (t.kind == 50) {
+ if (t.kind == 51) {
Get();
- } else if (t.kind == 51) {
+ } else if (t.kind == 52) {
Get();
- } else Error(106);
+ } else Error(107);
}
static void RelationalExpression(out Expression! e0) {
@@ -1000,25 +1093,25 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void AndOp() {
- if (t.kind == 52) {
+ if (t.kind == 53) {
Get();
- } else if (t.kind == 53) {
+ } else if (t.kind == 54) {
Get();
- } else Error(107);
+ } else Error(108);
}
static void OrOp() {
- if (t.kind == 54) {
+ if (t.kind == 55) {
Get();
- } else if (t.kind == 55) {
+ } else if (t.kind == 56) {
Get();
- } else Error(108);
+ } else Error(109);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 65 || t.kind == 66) {
+ while (t.kind == 66 || t.kind == 67) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1028,74 +1121,74 @@ public static int Parse (List<ClassDecl!>! classes) { static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 56: {
+ case 57: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
}
- case 11: {
+ case 12: {
Get();
x = token; op = BinaryExpr.Opcode.Lt;
break;
}
- case 12: {
+ case 13: {
Get();
x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 57: {
+ case 58: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 58: {
+ case 59: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 59: {
+ case 60: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 60: {
+ case 61: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 44: {
+ case 45: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 61: {
+ case 62: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 62: {
+ case 63: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 63: {
+ case 64: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 64: {
+ case 65: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(109); break;
+ default: Error(110); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 41 || t.kind == 67 || t.kind == 68) {
+ while (t.kind == 42 || t.kind == 68 || t.kind == 69) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1104,23 +1197,23 @@ public static int Parse (List<ClassDecl!>! classes) { static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 65) {
+ if (t.kind == 66) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 66) {
+ } else if (t.kind == 67) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(110);
+ } else Error(111);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 66) {
+ if (t.kind == 67) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 69 || t.kind == 70) {
+ } else if (t.kind == 70 || t.kind == 71) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1129,39 +1222,39 @@ public static int Parse (List<ClassDecl!>! classes) { SelectExpression(out e);
} else if (StartOf(11)) {
ConstAtomExpression(out e);
- } else Error(111);
+ } else Error(112);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 41) {
+ if (t.kind == 42) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 67) {
+ } else if (t.kind == 68) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 68) {
+ } else if (t.kind == 69) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(112);
+ } else Error(113);
}
static void NegOp() {
- if (t.kind == 69) {
+ if (t.kind == 70) {
Get();
- } else if (t.kind == 70) {
+ } else if (t.kind == 71) {
Get();
- } else Error(113);
+ } else Error(114);
}
static void SelectExpression(out Expression! e) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 20 || t.kind == 79 || t.kind == 80) {
+ } else if (t.kind == 21 || t.kind == 80 || t.kind == 81) {
ObjectExpression(out e);
- } else Error(114);
- while (t.kind == 75 || t.kind == 77) {
+ } else Error(115);
+ while (t.kind == 76 || t.kind == 78) {
SelectOrCallSuffix(ref e);
}
}
@@ -1171,17 +1264,17 @@ public static int Parse (List<ClassDecl!>! classes) { e = dummyExpr;
switch (t.kind) {
- case 71: {
+ case 72: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 72: {
+ case 73: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 73: {
+ case 74: {
Get();
e = new LiteralExpr(token);
break;
@@ -1191,21 +1284,21 @@ public static int Parse (List<ClassDecl!>! classes) { e = new LiteralExpr(token, n);
break;
}
- case 74: {
+ case 75: {
Get();
x = token;
- Expect(20);
- Expression(out e);
Expect(21);
+ Expression(out e);
+ Expect(22);
e = new FreshExpr(x, e);
break;
}
- case 45: {
+ case 46: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(45);
+ Expect(46);
break;
}
case 5: {
@@ -1218,17 +1311,17 @@ public static int Parse (List<ClassDecl!>! classes) { Expect(6);
break;
}
- case 75: {
+ case 76: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(5)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(76);
+ Expect(77);
break;
}
- default: Error(115); break;
+ default: Error(116); break;
}
}
@@ -1246,13 +1339,13 @@ public static int Parse (List<ClassDecl!>! classes) { static void IdentOrFuncExpression(out Expression! e) {
Token! id; e = dummyExpr; List<Expression!>! args;
Ident(out id);
- if (t.kind == 20) {
+ if (t.kind == 21) {
Get();
args = new List<Expression!>();
if (StartOf(5)) {
Expressions(args);
}
- Expect(21);
+ Expect(22);
e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
@@ -1267,25 +1360,25 @@ public static int Parse (List<ClassDecl!>! classes) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 79) {
+ if (t.kind == 80) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 80) {
+ } else if (t.kind == 81) {
Get();
x = token;
- Expect(20);
- Expression(out e);
Expect(21);
+ Expression(out e);
+ Expect(22);
e = new OldExpr(x, e);
- } else if (t.kind == 20) {
+ } else if (t.kind == 21) {
Get();
if (StartOf(12)) {
QuantifierGuts(out e);
} else if (StartOf(5)) {
Expression(out e);
- } else Error(116);
- Expect(21);
- } else Error(117);
+ } else Error(117);
+ Expect(22);
+ } else Error(118);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1293,27 +1386,27 @@ public static int Parse (List<ClassDecl!>! classes) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 77) {
+ if (t.kind == 78) {
Get();
Ident(out id);
- if (t.kind == 20) {
+ if (t.kind == 21) {
Get();
args = new List<Expression!>(); func = true;
if (StartOf(5)) {
Expressions(args);
}
- Expect(21);
+ Expect(22);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 75) {
+ } else if (t.kind == 76) {
Get();
x = token;
if (StartOf(5)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 35 || t.kind == 78) {
- if (t.kind == 78) {
+ if (t.kind == 36 || t.kind == 79) {
+ if (t.kind == 79) {
Get();
anyDots = true;
if (StartOf(5)) {
@@ -1326,11 +1419,11 @@ public static int Parse (List<ClassDecl!>! classes) { e1 = ee;
}
}
- } else if (t.kind == 78) {
+ } else if (t.kind == 79) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(118);
+ } else Error(119);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1343,8 +1436,8 @@ public static int Parse (List<ClassDecl!>! classes) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(76);
- } else Error(119);
+ Expect(77);
+ } else Error(120);
}
static void QuantifierGuts(out Expression! q) {
@@ -1357,17 +1450,17 @@ public static int Parse (List<ClassDecl!>! classes) { Triggers trigs = null;
Expression! body;
- if (t.kind == 81 || t.kind == 82) {
+ if (t.kind == 82 || t.kind == 83) {
Forall();
x = token; univ = true;
- } else if (t.kind == 83 || t.kind == 84) {
+ } else if (t.kind == 84 || t.kind == 85) {
Exists();
x = token;
- } else Error(120);
+ } else Error(121);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1387,40 +1480,40 @@ public static int Parse (List<ClassDecl!>! classes) { }
static void Forall() {
- if (t.kind == 81) {
+ if (t.kind == 82) {
Get();
- } else if (t.kind == 82) {
+ } else if (t.kind == 83) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void Exists() {
- if (t.kind == 83) {
+ if (t.kind == 84) {
Get();
- } else if (t.kind == 84) {
+ } else if (t.kind == 85) {
Get();
- } else Error(122);
+ } else Error(123);
}
static void QSep() {
- if (t.kind == 85) {
+ if (t.kind == 86) {
Get();
- } else if (t.kind == 86) {
+ } else if (t.kind == 87) {
Get();
- } else Error(123);
+ } else Error(124);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
List<Expression!> es = new List<Expression!>();
Expect(5);
- if (t.kind == 10) {
+ if (t.kind == 11) {
AttributeBody(ref attrs);
} else if (StartOf(5)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(124);
+ } else Error(125);
Expect(6);
}
@@ -1429,13 +1522,13 @@ public static int Parse (List<ClassDecl!>! classes) { List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
Attributes.Argument! aArg;
- Expect(10);
+ Expect(11);
Expect(1);
aName = token.val;
if (StartOf(13)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (t.kind == 8) {
+ while (t.kind == 10) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -1452,7 +1545,7 @@ public static int Parse (List<ClassDecl!>! classes) { } else if (StartOf(5)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(125);
+ } else Error(126);
}
@@ -1478,125 +1571,126 @@ public static int Parse (List<ClassDecl!>! classes) { case 4: s = "class expected"; break;
case 5: s = "{ expected"; break;
case 6: s = "} 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 = "frame expected"; break;
- case 14: s = "method expected"; break;
- case 15: s = "returns expected"; break;
- case 16: s = "modifies expected"; break;
- case 17: s = "free expected"; break;
- case 18: s = "requires expected"; break;
- case 19: s = "ensures expected"; break;
- case 20: s = "( expected"; break;
- case 21: s = ") expected"; break;
- case 22: s = "bool expected"; break;
- case 23: s = "int expected"; break;
- case 24: s = "object expected"; break;
+ case 7: s = "datatype expected"; break;
+ case 8: s = "; expected"; break;
+ case 9: s = "var 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 = "frame expected"; break;
+ case 15: s = "method expected"; break;
+ case 16: s = "returns expected"; break;
+ case 17: s = "modifies expected"; break;
+ case 18: s = "free expected"; break;
+ case 19: s = "requires expected"; break;
+ case 20: s = "ensures expected"; break;
+ case 21: s = "( expected"; break;
+ case 22: s = ") expected"; break;
+ case 23: s = "bool expected"; break;
+ case 24: s = "int expected"; break;
case 25: s = "set expected"; break;
case 26: s = "seq expected"; break;
- case 27: s = "function expected"; break;
- case 28: s = "use expected"; break;
- case 29: s = "reads expected"; break;
- case 30: s = "if expected"; break;
- case 31: s = "else expected"; break;
- case 32: s = "label expected"; break;
- case 33: s = "break expected"; break;
- case 34: s = "return expected"; break;
- case 35: s = ":= expected"; break;
- case 36: s = "new expected"; break;
- case 37: s = "havoc expected"; break;
- case 38: s = "while expected"; break;
- case 39: s = "invariant expected"; break;
- case 40: s = "decreases expected"; break;
- case 41: s = "* expected"; break;
- case 42: s = "call expected"; break;
- case 43: s = "foreach expected"; break;
- case 44: s = "in expected"; break;
- case 45: s = "| expected"; break;
- case 46: s = "assert expected"; break;
- case 47: s = "assume expected"; break;
- case 48: s = "<==> expected"; break;
- case 49: s = "\\u21d4 expected"; break;
- case 50: s = "==> expected"; break;
- case 51: s = "\\u21d2 expected"; break;
- case 52: s = "&& expected"; break;
- case 53: s = "\\u2227 expected"; break;
- case 54: s = "|| expected"; break;
- case 55: s = "\\u2228 expected"; break;
- case 56: s = "== expected"; break;
- case 57: s = "<= expected"; break;
- case 58: s = ">= expected"; break;
- case 59: s = "!= expected"; break;
- case 60: s = "!! expected"; break;
- case 61: s = "!in expected"; break;
- case 62: s = "\\u2260 expected"; break;
- case 63: s = "\\u2264 expected"; break;
- case 64: s = "\\u2265 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 = "\\u00ac expected"; break;
- case 71: s = "false expected"; break;
- case 72: s = "true expected"; break;
- case 73: s = "null expected"; break;
- case 74: s = "fresh expected"; break;
- case 75: s = "[ expected"; break;
- case 76: s = "] expected"; break;
- case 77: s = ". expected"; break;
- case 78: s = ".. expected"; break;
- case 79: s = "this expected"; break;
- case 80: s = "old expected"; break;
- case 81: s = "forall expected"; break;
- case 82: s = "\\u2200 expected"; break;
- case 83: s = "exists expected"; break;
- case 84: s = "\\u2203 expected"; break;
- case 85: s = ":: expected"; break;
- case 86: s = "\\u2022 expected"; break;
- case 87: s = "??? expected"; break;
- case 88: s = "invalid ClassMemberDecl"; break;
- case 89: s = "invalid FunctionDecl"; break;
- case 90: s = "invalid MethodDecl"; break;
- case 91: s = "invalid Type"; break;
- case 92: s = "invalid MethodSpec"; break;
+ case 27: s = "object expected"; break;
+ case 28: s = "function expected"; break;
+ case 29: s = "use expected"; break;
+ case 30: s = "reads expected"; break;
+ case 31: s = "if expected"; break;
+ case 32: s = "else expected"; break;
+ case 33: s = "label expected"; break;
+ case 34: s = "break expected"; break;
+ case 35: s = "return expected"; break;
+ case 36: s = ":= expected"; break;
+ case 37: s = "new expected"; break;
+ case 38: s = "havoc expected"; break;
+ case 39: s = "while expected"; break;
+ case 40: s = "invariant expected"; break;
+ case 41: s = "decreases expected"; break;
+ case 42: s = "* expected"; break;
+ case 43: s = "call expected"; break;
+ case 44: s = "foreach expected"; break;
+ case 45: s = "in expected"; break;
+ case 46: s = "| expected"; break;
+ case 47: s = "assert expected"; break;
+ case 48: s = "assume expected"; break;
+ case 49: s = "<==> expected"; break;
+ case 50: s = "\\u21d4 expected"; break;
+ case 51: s = "==> expected"; break;
+ case 52: s = "\\u21d2 expected"; break;
+ case 53: s = "&& expected"; break;
+ case 54: s = "\\u2227 expected"; break;
+ case 55: s = "|| expected"; break;
+ case 56: s = "\\u2228 expected"; break;
+ case 57: s = "== expected"; break;
+ case 58: s = "<= expected"; break;
+ case 59: s = ">= expected"; break;
+ case 60: s = "!= expected"; break;
+ case 61: s = "!! expected"; break;
+ case 62: s = "!in expected"; break;
+ case 63: s = "\\u2260 expected"; break;
+ case 64: s = "\\u2264 expected"; break;
+ case 65: s = "\\u2265 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 = "\\u00ac expected"; break;
+ case 72: s = "false expected"; break;
+ case 73: s = "true expected"; break;
+ case 74: s = "null expected"; break;
+ case 75: s = "fresh expected"; break;
+ case 76: s = "[ expected"; break;
+ case 77: s = "] expected"; break;
+ case 78: s = ". expected"; break;
+ case 79: s = ".. expected"; break;
+ case 80: s = "this expected"; break;
+ case 81: s = "old expected"; break;
+ case 82: s = "forall expected"; break;
+ case 83: s = "\\u2200 expected"; break;
+ case 84: s = "exists expected"; break;
+ case 85: s = "\\u2203 expected"; break;
+ case 86: s = ":: expected"; break;
+ case 87: s = "\\u2022 expected"; break;
+ case 88: s = "??? expected"; break;
+ case 89: s = "invalid ClassMemberDecl"; break;
+ case 90: s = "invalid FunctionDecl"; break;
+ case 91: s = "invalid MethodDecl"; break;
+ case 92: s = "invalid TypeAndToken"; break;
case 93: s = "invalid MethodSpec"; break;
- case 94: s = "invalid ReferenceType"; break;
- case 95: s = "invalid FunctionSpec"; break;
- case 96: s = "invalid ExtendedExpr"; break;
- case 97: s = "invalid IfThenElseExpr"; break;
- case 98: s = "invalid Stmt"; break;
- case 99: s = "invalid OneStmt"; break;
- case 100: s = "invalid IfStmt"; break;
- case 101: s = "invalid ForeachStmt"; break;
- case 102: s = "invalid AssignRhs"; break;
- case 103: s = "invalid Guard"; break;
- case 104: s = "invalid CallStmtSubExpr"; break;
- case 105: s = "invalid EquivOp"; break;
- case 106: s = "invalid ImpliesOp"; break;
- case 107: s = "invalid AndOp"; break;
- case 108: s = "invalid OrOp"; break;
- case 109: s = "invalid RelOp"; break;
- case 110: s = "invalid AddOp"; break;
- case 111: s = "invalid UnaryExpression"; break;
- case 112: s = "invalid MulOp"; break;
- case 113: s = "invalid NegOp"; break;
- case 114: s = "invalid SelectExpression"; break;
- case 115: s = "invalid ConstAtomExpression"; break;
- case 116: s = "invalid ObjectExpression"; break;
+ case 94: s = "invalid MethodSpec"; break;
+ case 95: s = "invalid ReferenceType"; break;
+ case 96: s = "invalid FunctionSpec"; break;
+ case 97: s = "invalid ExtendedExpr"; break;
+ case 98: s = "invalid IfThenElseExpr"; break;
+ case 99: s = "invalid Stmt"; break;
+ case 100: s = "invalid OneStmt"; break;
+ case 101: s = "invalid IfStmt"; break;
+ case 102: s = "invalid ForeachStmt"; break;
+ case 103: s = "invalid AssignRhs"; break;
+ case 104: s = "invalid Guard"; break;
+ case 105: s = "invalid CallStmtSubExpr"; break;
+ case 106: s = "invalid EquivOp"; break;
+ case 107: s = "invalid ImpliesOp"; break;
+ case 108: s = "invalid AndOp"; break;
+ case 109: s = "invalid OrOp"; break;
+ case 110: s = "invalid RelOp"; break;
+ case 111: s = "invalid AddOp"; break;
+ case 112: s = "invalid UnaryExpression"; break;
+ case 113: s = "invalid MulOp"; break;
+ case 114: s = "invalid NegOp"; break;
+ case 115: s = "invalid SelectExpression"; break;
+ case 116: s = "invalid ConstAtomExpression"; break;
case 117: s = "invalid ObjectExpression"; break;
- case 118: s = "invalid SelectOrCallSuffix"; break;
+ case 118: s = "invalid ObjectExpression"; break;
case 119: s = "invalid SelectOrCallSuffix"; break;
- case 120: s = "invalid QuantifierGuts"; break;
- case 121: s = "invalid Forall"; break;
- case 122: s = "invalid Exists"; break;
- case 123: s = "invalid QSep"; break;
- case 124: s = "invalid AttributeOrTrigger"; break;
- case 125: s = "invalid AttributeArg"; break;
+ case 120: s = "invalid SelectOrCallSuffix"; break;
+ case 121: s = "invalid QuantifierGuts"; break;
+ case 122: s = "invalid Forall"; break;
+ case 123: s = "invalid Exists"; break;
+ case 124: s = "invalid QSep"; break;
+ case 125: s = "invalid AttributeOrTrigger"; break;
+ case 126: s = "invalid AttributeArg"; break;
default: s = "error " + n; break;
}
@@ -1604,20 +1698,20 @@ public static int Parse (List<ClassDecl!>! classes) { }
static 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,T, x,x,x,x, x,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, 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,T,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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,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,T,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, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,T,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, 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, 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,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, T,x,x,x, x,x,x,x, x,x,x,x, T,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,T,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,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,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,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,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,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,T,T,T, x,T,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,T,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, T,T,T,T, x,x,x,T, T,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,T,x,x, x,x,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,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,T,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,T,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,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,T,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,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,T,T,T, x,x,T,T, x,x,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,T,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,T, x,T,T,T, x,x,T,T, x,x,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, T,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, 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, 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,T,x,x, x,x,x,x, x,x,x,x, x,T,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,T,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,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,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,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, 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,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,T,T,T, x,T,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,T,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,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 68b9e132..24ccb44e 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -22,9 +22,13 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);
}
wr.WriteLine("// {0}", prog.Name);
- foreach (ClassDecl c in prog.Classes) {
+ foreach (TopLevelDecl d in prog.Classes) {
wr.WriteLine();
- PrintClass(c);
+ if (d is ClassDecl) {
+ PrintClass((ClassDecl)d);
+ } else {
+ PrintDatatype((DatatypeDecl)d);
+ }
}
}
@@ -57,7 +61,9 @@ namespace Microsoft.Dafny { }
void PrintClassMethodHelper(string! kind, Attributes attrs, string! modifiers, string! name, List<TypeParameter!>! typeArgs) {
- wr.Write("{0} ", kind);
+ if (kind.Length != 0) {
+ wr.Write("{0} ", kind);
+ }
PrintAttributes(attrs);
wr.Write(modifiers);
wr.Write(name);
@@ -72,6 +78,19 @@ namespace Microsoft.Dafny { }
}
+ public void PrintDatatype(DatatypeDecl! dt) {
+ PrintClassMethodHelper("datatype", dt.Attributes, "", dt.Name, dt.TypeArgs);
+ if (dt.Ctors.Count == 0) {
+ wr.WriteLine(" { }");
+ } else {
+ wr.WriteLine(" {");
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ PrintCtor(ctor);
+ }
+ wr.WriteLine("}");
+ }
+ }
+
public void PrintAttributes(Attributes a) {
if (a != null) {
PrintAttributes(a.Prev);
@@ -129,6 +148,15 @@ namespace Microsoft.Dafny { }
}
+ public void PrintCtor(DatatypeCtor! ctor) {
+ Indent(IndentAmount);
+ PrintClassMethodHelper("", ctor.Attributes, "", ctor.Name, ctor.TypeArgs);
+ if (ctor.Formals.Count != 0) {
+ PrintFormals(ctor.Formals);
+ }
+ wr.WriteLine(";");
+ }
+
// ----------------------------- PrintMethod -----------------------------
const int IndentAmount = 2;
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 7f1342f1..367c81aa 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -32,42 +32,70 @@ namespace Microsoft.Dafny { Error(e.tok, msg, args);
}
- readonly Dictionary<string!,ClassDecl!>! classes = new Dictionary<string!,ClassDecl!>();
+ readonly Dictionary<string!,TopLevelDecl!>! classes = new Dictionary<string!,TopLevelDecl!>();
readonly Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>! classMembers = new Dictionary<ClassDecl!,Dictionary<string!,MemberDecl!>!>();
+ readonly Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>! datatypeCtors = new Dictionary<DatatypeDecl!,Dictionary<string!,DatatypeCtor!>!>();
public void ResolveProgram(Program! prog) {
- foreach (ClassDecl cl in prog.Classes) {
- // register the class name
- if (classes.ContainsKey(cl.Name)) {
- Error(cl, "Duplicate class name: {0}", cl.Name);
+ foreach (TopLevelDecl d in prog.Classes) {
+ // register the class/datatype name
+ if (classes.ContainsKey(d.Name)) {
+ Error(d, "Duplicate name of top-level declaration: {0}", d.Name);
} else {
- classes.Add(cl.Name, cl);
+ classes.Add(d.Name, d);
}
+
+ if (d is ClassDecl) {
+ ClassDecl cl = (ClassDecl)d;
+
+ // register the names of the class members
+ Dictionary<string!,MemberDecl!> members = new Dictionary<string!,MemberDecl!>();
+ classMembers.Add(cl, members);
- // register the names of the class members
- Dictionary<string!,MemberDecl!> members = new Dictionary<string!,MemberDecl!>();
- classMembers.Add(cl, members);
+ foreach (MemberDecl m in cl.Members) {
+ if (members.ContainsKey(m.Name)) {
+ Error(m, "Duplicate member name: {0}", m.Name);
+ } else {
+ members.Add(m.Name, m);
+ }
+ }
+ } else {
+ DatatypeDecl dt = (DatatypeDecl)d;
+
+ // register the names of the constructors
+ Dictionary<string!,DatatypeCtor!> ctors = new Dictionary<string!,DatatypeCtor!>();
+ datatypeCtors.Add(dt, ctors);
- foreach (MemberDecl m in cl.Members) {
- if (members.ContainsKey(m.Name)) {
- Error(m, "Duplicate member name: {0}", m.Name);
- } else {
- members.Add(m.Name, m);
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ if (ctors.ContainsKey(ctor.Name)) {
+ Error(ctor, "Duplicate datatype constructor name: {0}", ctor.Name);
+ } else {
+ ctors.Add(ctor.Name, ctor);
+ }
}
}
}
// resolve each class
- foreach (ClassDecl cl in prog.Classes) {
+ foreach (TopLevelDecl d in prog.Classes) {
allTypeParameters.PushMarker();
- ResolveTypeParameters(cl.TypeArgs, true, cl);
- ResolveClassMemberTypes(cl);
+ ResolveTypeParameters(d.TypeArgs, true, d);
+ if (d is ClassDecl) {
+ ResolveClassMemberTypes((ClassDecl)d);
+ } else {
+ ResolveCtorTypes((DatatypeDecl)d);
+ }
allTypeParameters.PopMarker();
}
- foreach (ClassDecl cl in prog.Classes) {
+ foreach (TopLevelDecl d in prog.Classes) {
allTypeParameters.PushMarker();
- ResolveTypeParameters(cl.TypeArgs, false, cl);
- ResolveClassMemberBodies(cl);
+ ResolveTypeParameters(d.TypeArgs, false, d);
+ if (d is ClassDecl) {
+ ResolveClassMemberBodies((ClassDecl)d);
+ } else {
+ assert d is DatatypeDecl;
+ // nothing else to do (but there will be something to do here if constructors can have preconditions)
+ }
allTypeParameters.PopMarker();
}
}
@@ -146,6 +174,21 @@ namespace Microsoft.Dafny { currentClass = null;
}
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ void ResolveCtorTypes(DatatypeDecl! dt)
+ {
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ ctor.EnclosingDatatype = dt;
+
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(ctor.TypeArgs, true, ctor);
+ ResolveCtorSignature(ctor);
+ allTypeParameters.PopMarker();
+ }
+ }
+
void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
@@ -218,7 +261,7 @@ namespace Microsoft.Dafny { }
if (t is ObjectType) {
// fine
- } else if (ClassType.DenotesClass(t) != null) {
+ } else if (UserDefinedType.DenotesClass(t) != null) {
// fine
} else {
Error(r, "a reads-clause expression must denote an object or a collection of objects (instead got {0})", r.Type);
@@ -283,7 +326,7 @@ namespace Microsoft.Dafny { }
if (t is ObjectType) {
// fine
- } else if (ClassType.DenotesClass(t) != null) {
+ } else if (UserDefinedType.DenotesClass(t) != null) {
// fine
} else {
Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type);
@@ -312,13 +355,27 @@ namespace Microsoft.Dafny { scope.PopMarker();
}
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ void ResolveCtorSignature(DatatypeCtor! ctor) {
+ scope.PushMarker();
+ foreach (Formal p in ctor.Formals) {
+ if (!scope.Push(p.Name, p)) {
+ Error(p, "Duplicate parameter name: {0}", p.Name);
+ }
+ ResolveType(p.Type);
+ }
+ scope.PopMarker();
+ }
+
public void ResolveType(Type! type) {
if (type is BasicType) {
// nothing to resolve
} else if (type is CollectionType) {
ResolveType(((CollectionType)type).Arg);
- } else if (type is ClassType) {
- ClassType t = (ClassType)type;
+ } else if (type is UserDefinedType) {
+ UserDefinedType t = (UserDefinedType)type;
foreach (Type tt in t.TypeArgs) {
ResolveType(tt);
}
@@ -330,13 +387,13 @@ namespace Microsoft.Dafny { Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
} else {
- ClassDecl cl;
- if (!classes.TryGetValue(t.Name, out cl)) {
- Error(t.tok, "Undeclared class type or type parameter: {0}", t.Name);
- } else if (((!)cl).TypeArgs.Count == t.TypeArgs.Count) {
- t.ResolvedClass = cl;
+ TopLevelDecl d;
+ if (!classes.TryGetValue(t.Name, out d)) {
+ Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name);
+ } else if (((!)d).TypeArgs.Count == t.TypeArgs.Count) {
+ t.ResolvedClass = d;
} else {
- Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class: {2}", t.TypeArgs.Count, cl.TypeArgs.Count, t.Name);
+ Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);
}
}
@@ -393,14 +450,14 @@ namespace Microsoft.Dafny { return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
- } else if (a is ClassType) {
- if (!(b is ClassType)) {
+ } else if (a is UserDefinedType) {
+ if (!(b is UserDefinedType)) {
return false;
}
- ClassType aa = (ClassType)a;
- ClassType bb = (ClassType)b;
+ UserDefinedType aa = (UserDefinedType)a;
+ UserDefinedType bb = (UserDefinedType)b;
if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {
- // these are both resolved class types
+ // these are both resolved class/datatype types
assert aa.TypeArgs.Count == bb.TypeArgs.Count;
bool successSoFar = true;
for (int i = 0; i < aa.TypeArgs.Count; i++) {
@@ -454,14 +511,14 @@ namespace Microsoft.Dafny { // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is ObjectTypeProxy) {
- if (t is ObjectType || ClassType.DenotesClass(t) != null) {
+ if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
} else if (proxy is ObjectsTypeProxy) {
- if (t is ObjectType || ClassType.DenotesClass(t) != null) {
+ if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is good
} else if (t is CollectionType) {
proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());
@@ -641,7 +698,9 @@ namespace Microsoft.Dafny { } else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
ResolveType(rr.Type);
- if (!UnifyTypes(s.Lhs.Type, rr.Type)) {
+ if (!rr.Type.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
+ } else if (!UnifyTypes(s.Lhs.Type, rr.Type)) {
Error(stmt, "type {0} is not assignable to LHS (of type {1})", rr.Type, s.Lhs.Type);
}
} else if (s.Rhs is HavocRhs) {
@@ -666,6 +725,9 @@ namespace Microsoft.Dafny { } else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
ResolveType(rr.Type);
+ if (!rr.Type.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
+ }
rhsType = rr.Type;
} else {
assert false; // unexpected RHS
@@ -708,7 +770,7 @@ namespace Microsoft.Dafny { }
// resolve the method name
- ClassType ctype;
+ UserDefinedType ctype;
MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype);
if (member == null) {
// error has already been reported by ResolveMember
@@ -835,17 +897,17 @@ namespace Microsoft.Dafny { }
}
- MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out ClassType ctype)
+ MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)
ensures result != null ==> ctype != null && ctype.ResolvedClass != null;
{
- ctype = ClassType.DenotesClass(receiverType);
+ ctype = UserDefinedType.DenotesClass(receiverType);
if (ctype == null) {
Error(tok, "receiver (of type {0}) must be of a class type", receiverType);
} else {
- assert ctype.ResolvedClass != null; // follows from postcondition of DenotesClass
+ assert ctype.ResolvedClass is ClassDecl; // follows from postcondition of DenotesClass
assert ctype.TypeArgs.Count == ctype.ResolvedClass.TypeArgs.Count; // follows from the fact that ctype was resolved
MemberDecl member;
- if (!classMembers[ctype.ResolvedClass].TryGetValue(memberName, out member)) {
+ if (!classMembers[(ClassDecl)ctype.ResolvedClass].TryGetValue(memberName, out member)) {
Error(tok, "member {0} does not exist in class {1}", memberName, ctype.Name);
} else {
return (!)member;
@@ -870,8 +932,8 @@ namespace Microsoft.Dafny { } else {
assert false; // unexpected collection type
}
- } else if (type is ClassType) {
- ClassType t = (ClassType)type;
+ } else if (type is UserDefinedType) {
+ UserDefinedType t = (UserDefinedType)type;
if (t.ResolvedParam != null) {
assert t.TypeArgs.Count == 0;
Type s;
@@ -900,10 +962,10 @@ namespace Microsoft.Dafny { // there were no substitutions
return type;
} else {
- return new ClassType(t.tok, t.Name, t.ResolvedClass, newArgs);
+ return new UserDefinedType(t.tok, t.Name, t.ResolvedClass, newArgs);
}
} else {
- // there's neither a resolved param nor a resolved class, which means the ClassType wasn't
+ // there's neither a resolved param nor a resolved class, which means the UserDefinedType wasn't
// properly resolved; just return it
return type;
}
@@ -920,12 +982,12 @@ namespace Microsoft.Dafny { }
}
- public static ClassType! GetThisType(Token! tok, ClassDecl! cl) {
+ public static UserDefinedType! GetThisType(Token! tok, ClassDecl! cl) {
List<Type!> args = new List<Type!>();
foreach (TypeParameter tp in cl.TypeArgs) {
- args.Add(new ClassType(tok, tp.Name, tp));
+ args.Add(new UserDefinedType(tok, tp.Name, tp));
}
- return new ClassType(tok, cl.Name, cl, args);
+ return new UserDefinedType(tok, cl.Name, cl, args);
}
/// <summary>
@@ -989,7 +1051,7 @@ namespace Microsoft.Dafny { FieldSelectExpr e = (FieldSelectExpr)expr;
ResolveExpression(e.Obj, twoState);
assert e.Obj.Type != null; // follows from postcondition of ResolveExpression
- ClassType ctype;
+ UserDefinedType ctype;
MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.FieldName, out ctype);
if (member == null) {
// error has already been reported by ResolveMember
@@ -1066,7 +1128,7 @@ namespace Microsoft.Dafny { FunctionCallExpr e = (FunctionCallExpr)expr;
ResolveExpression(e.Receiver, twoState);
assert e.Receiver.Type != null; // follows from postcondition of ResolveExpression
- ClassType ctype;
+ UserDefinedType ctype;
MemberDecl member = ResolveMember(expr.tok, e.Receiver.Type, e.Name, out ctype);
if (member == null) {
// error has already been reported by ResolveMember
@@ -1120,7 +1182,7 @@ namespace Microsoft.Dafny { }
if (t is ObjectType) {
// fine
- } else if (ClassType.DenotesClass(t) != null) {
+ } else if (UserDefinedType.DenotesClass(t) != null) {
// fine
} else {
Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index adbb7e1c..9c5f0886 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -40,7 +40,7 @@ public class Scanner { start[41] = 13;
start[42] = 15;
start[43] = 39;
- start[44] = 7;
+ start[44] = 8;
start[45] = 40;
start[46] = 46;
start[47] = 41;
@@ -55,7 +55,7 @@ public class Scanner { start[56] = 2;
start[57] = 2;
start[58] = 9;
- start[59] = 8;
+ start[59] = 7;
start[60] = 10;
start[61] = 21;
start[62] = 11;
@@ -132,7 +132,7 @@ public class Scanner { start[8804] = 37;
start[8805] = 38;
}
- const int noSym = 87;
+ const int noSym = 88;
static short[] start = new short[16385];
@@ -275,45 +275,46 @@ public class Scanner { static void CheckLiteral() {
switch (t.val) {
case "class": t.kind = 4; break;
- case "var": t.kind = 7; break;
- case "frame": t.kind = 13; break;
- case "method": t.kind = 14; break;
- case "returns": t.kind = 15; break;
- case "modifies": t.kind = 16; break;
- case "free": t.kind = 17; break;
- case "requires": t.kind = 18; break;
- case "ensures": t.kind = 19; break;
- case "bool": t.kind = 22; break;
- case "int": t.kind = 23; break;
- case "object": t.kind = 24; break;
+ case "datatype": t.kind = 7; break;
+ case "var": t.kind = 9; break;
+ case "frame": t.kind = 14; break;
+ case "method": t.kind = 15; break;
+ case "returns": t.kind = 16; break;
+ case "modifies": t.kind = 17; break;
+ case "free": t.kind = 18; break;
+ case "requires": t.kind = 19; break;
+ case "ensures": t.kind = 20; break;
+ case "bool": t.kind = 23; break;
+ case "int": t.kind = 24; break;
case "set": t.kind = 25; break;
case "seq": t.kind = 26; break;
- case "function": t.kind = 27; break;
- case "use": t.kind = 28; break;
- case "reads": t.kind = 29; break;
- case "if": t.kind = 30; break;
- case "else": t.kind = 31; break;
- case "label": t.kind = 32; break;
- case "break": t.kind = 33; break;
- case "return": t.kind = 34; break;
- case "new": t.kind = 36; break;
- case "havoc": t.kind = 37; break;
- case "while": t.kind = 38; break;
- case "invariant": t.kind = 39; break;
- case "decreases": t.kind = 40; break;
- case "call": t.kind = 42; break;
- case "foreach": t.kind = 43; break;
- case "in": t.kind = 44; break;
- case "assert": t.kind = 46; break;
- case "assume": t.kind = 47; break;
- case "false": t.kind = 71; break;
- case "true": t.kind = 72; break;
- case "null": t.kind = 73; break;
- case "fresh": t.kind = 74; break;
- case "this": t.kind = 79; break;
- case "old": t.kind = 80; break;
- case "forall": t.kind = 81; break;
- case "exists": t.kind = 83; break;
+ case "object": t.kind = 27; break;
+ case "function": t.kind = 28; break;
+ case "use": t.kind = 29; break;
+ case "reads": t.kind = 30; break;
+ case "if": t.kind = 31; break;
+ case "else": t.kind = 32; break;
+ case "label": t.kind = 33; break;
+ case "break": t.kind = 34; break;
+ case "return": t.kind = 35; break;
+ case "new": t.kind = 37; break;
+ case "havoc": t.kind = 38; break;
+ case "while": t.kind = 39; break;
+ case "invariant": t.kind = 40; break;
+ case "decreases": t.kind = 41; break;
+ case "call": t.kind = 43; break;
+ case "foreach": t.kind = 44; break;
+ case "in": t.kind = 45; break;
+ case "assert": t.kind = 47; break;
+ case "assume": t.kind = 48; break;
+ case "false": t.kind = 72; break;
+ case "true": t.kind = 73; break;
+ case "null": t.kind = 74; break;
+ case "fresh": t.kind = 75; break;
+ case "this": t.kind = 80; break;
+ case "old": t.kind = 81; break;
+ case "forall": t.kind = 82; break;
+ case "exists": t.kind = 84; break;
default: break;
}
@@ -349,108 +350,108 @@ public class Scanner { case 7:
{t.kind = 8; goto done;}
case 8:
- {t.kind = 9; goto done;}
+ {t.kind = 10; goto done;}
case 9:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 14;}
else if (ch == ':') {buf.Append(ch); NextCh(); goto case 50;}
- else {t.kind = 10; goto done;}
+ else {t.kind = 11; goto done;}
case 10:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
- else {t.kind = 11; goto done;}
+ else {t.kind = 12; goto done;}
case 11:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}
- else {t.kind = 12; goto done;}
+ else {t.kind = 13; goto done;}
case 12:
- {t.kind = 20; goto done;}
- case 13:
{t.kind = 21; goto done;}
+ case 13:
+ {t.kind = 22; goto done;}
case 14:
- {t.kind = 35; goto done;}
+ {t.kind = 36; goto done;}
case 15:
- {t.kind = 41; goto done;}
+ {t.kind = 42; goto done;}
case 16:
if (ch == '|') {buf.Append(ch); NextCh(); goto case 28;}
- else {t.kind = 45; goto done;}
+ else {t.kind = 46; goto done;}
case 17:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}
- else {t.kind = 57; goto done;}
+ else {t.kind = 58; goto done;}
case 18:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 19;}
else {t.kind = noSym; goto done;}
case 19:
- {t.kind = 48; goto done;}
- case 20:
{t.kind = 49; goto done;}
+ case 20:
+ {t.kind = 50; goto done;}
case 21:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}
else {t.kind = noSym; goto done;}
case 22:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = 56; goto done;}
+ else {t.kind = 57; goto done;}
case 23:
- {t.kind = 50; goto done;}
- case 24:
{t.kind = 51; goto done;}
+ case 24:
+ {t.kind = 52; goto done;}
case 25:
if (ch == '&') {buf.Append(ch); NextCh(); goto case 26;}
else {t.kind = noSym; goto done;}
case 26:
- {t.kind = 52; goto done;}
- case 27:
{t.kind = 53; goto done;}
- case 28:
+ case 27:
{t.kind = 54; goto done;}
- case 29:
+ case 28:
{t.kind = 55; goto done;}
+ case 29:
+ {t.kind = 56; goto done;}
case 30:
- {t.kind = 58; goto done;}
+ {t.kind = 59; goto done;}
case 31:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 33;}
else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 34;}
- else {t.kind = 69; goto done;}
+ else {t.kind = 70; goto done;}
case 32:
- {t.kind = 59; goto done;}
- case 33:
{t.kind = 60; goto done;}
+ case 33:
+ {t.kind = 61; goto done;}
case 34:
if (ch == 'n') {buf.Append(ch); NextCh(); goto case 35;}
else {t.kind = noSym; goto done;}
case 35:
- {t.kind = 61; goto done;}
- case 36:
{t.kind = 62; goto done;}
- case 37:
+ case 36:
{t.kind = 63; goto done;}
- case 38:
+ case 37:
{t.kind = 64; goto done;}
- case 39:
+ case 38:
{t.kind = 65; goto done;}
- case 40:
+ case 39:
{t.kind = 66; goto done;}
- case 41:
+ case 40:
{t.kind = 67; goto done;}
- case 42:
+ case 41:
{t.kind = 68; goto done;}
+ case 42:
+ {t.kind = 69; goto done;}
case 43:
- {t.kind = 70; goto done;}
+ {t.kind = 71; goto done;}
case 44:
- {t.kind = 75; goto done;}
- case 45:
{t.kind = 76; goto done;}
+ case 45:
+ {t.kind = 77; goto done;}
case 46:
if (ch == '.') {buf.Append(ch); NextCh(); goto case 47;}
- else {t.kind = 77; goto done;}
+ else {t.kind = 78; goto done;}
case 47:
- {t.kind = 78; goto done;}
+ {t.kind = 79; goto done;}
case 48:
- {t.kind = 82; goto done;}
+ {t.kind = 83; goto done;}
case 49:
- {t.kind = 84; goto done;}
- case 50:
{t.kind = 85; goto done;}
- case 51:
+ case 50:
{t.kind = 86; goto done;}
+ case 51:
+ {t.kind = 87; goto done;}
case 52: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index ae8f03a5..6d586bf3 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -29,7 +29,7 @@ namespace Microsoft.Dafny { }
// translation state
- readonly Dictionary<ClassDecl!,Bpl.Constant!>! classes = new Dictionary<ClassDecl!,Bpl.Constant!>();
+ readonly Dictionary<TopLevelDecl!,Bpl.Constant!>! classes = new Dictionary<TopLevelDecl!,Bpl.Constant!>();
readonly Dictionary<Field!,Bpl.Constant!>! fields = new Dictionary<Field!,Bpl.Constant!>();
readonly Dictionary<Function!,Bpl.Function!>! functions = new Dictionary<Function!,Bpl.Function!>();
readonly Dictionary<Method!,Bpl.Procedure!>! methods = new Dictionary<Method!,Bpl.Procedure!>();
@@ -109,6 +109,7 @@ namespace Microsoft.Dafny { public readonly string! HeapVarName;
public readonly Bpl.Constant! CevHeapName;
public readonly Bpl.Type! ClassNameType;
+ public readonly Bpl.Type! DatatypeType;
public readonly Bpl.Expr! Null;
private readonly Bpl.Constant! allocField;
public Bpl.IdentifierExpr! Alloc(Token! tok) {
@@ -117,7 +118,8 @@ namespace Microsoft.Dafny { public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
- Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
+ Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! datatypeType,
+ Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
@@ -131,6 +133,7 @@ namespace Microsoft.Dafny { this.HeapVarName = heap.Name;
this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
+ this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
}
@@ -150,6 +153,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
+ Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl boxType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
@@ -163,6 +167,8 @@ namespace Microsoft.Dafny { fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
+ } else if (dt.Name == "DatatypeType") {
+ datatypeType = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "BoxType") {
@@ -201,6 +207,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
+ } else if (datatypeType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
} else if (boxType == null) {
@@ -218,7 +226,9 @@ namespace Microsoft.Dafny { } else if (cevHeapNameConst == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
- return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType, setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, allocField, cevHeapNameConst);
+ return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
+ setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType,
+ allocField, cevHeapNameConst);
}
return null;
}
@@ -248,24 +258,35 @@ namespace Microsoft.Dafny { // already been printed, so just return an empty program here (which is non-null)
return new Bpl.Program();
}
- foreach (ClassDecl c in program.Classes) {
- AddClassMembers(c);
- }
- foreach (ClassDecl c in program.Classes) {
- foreach (MemberDecl member in c.Members) {
- if (member is Method) {
- Method m = (Method)member;
- if (m.Body != null) {
- AddMethodImpl(m);
- }
- } else if (member is Function) {
- Function f = (Function)member;
- AddFrameAxiom(f);
- // TODO: also need a well-formedness check for the preconditions
- if (f.Body != null) {
- AddWellformednessCheck(f);
+ foreach (TopLevelDecl d in program.Classes) {
+ if (d is ClassDecl) {
+ AddClassMembers((ClassDecl)d);
+ } else {
+ DatatypeDecl dt = (DatatypeDecl)d;
+ // TODO: handle DatatypeDecl
+ }
+ }
+ foreach (TopLevelDecl d in program.Classes) {
+ if (d is ClassDecl) {
+ ClassDecl c = (ClassDecl)d;
+ foreach (MemberDecl member in c.Members) {
+ if (member is Method) {
+ Method m = (Method)member;
+ if (m.Body != null) {
+ AddMethodImpl(m);
+ }
+ } else if (member is Function) {
+ Function f = (Function)member;
+ AddFrameAxiom(f);
+ // TODO: also need a well-formedness check for the preconditions
+ if (f.Body != null) {
+ AddWellformednessCheck(f);
+ }
}
}
+ } else {
+ DatatypeDecl dt = (DatatypeDecl)d;
+ // TODO: handle DatatypeDecl
}
}
return sink;
@@ -412,6 +433,9 @@ namespace Microsoft.Dafny { } else {
// TODO: should also handle sequences of sequences, etc. This will probably require some extra predicates, and these predicates may even replace the above treatment of sequences.
}
+
+ } else if (f.Type.IsDatatype) {
+ // TODO
} else {
// reference type:
@@ -912,7 +936,7 @@ namespace Microsoft.Dafny { }
}
- Bpl.Constant! GetClass(ClassDecl! cl)
+ Bpl.Constant! GetClass(TopLevelDecl! cl)
requires predef != null;
{
Bpl.Constant cc;
@@ -958,7 +982,7 @@ namespace Microsoft.Dafny { Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType);
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
- ClassType ct = (ClassType)type;
+ UserDefinedType ct = (UserDefinedType)type;
if (ct.ResolvedClass == null) {
return null; // TODO: what to do here?
}
@@ -1217,6 +1241,8 @@ namespace Microsoft.Dafny { } else if (type.IsRefType) {
// object and class types translate to ref
return predef.RefType;
+ } else if (type.IsDatatype) {
+ return predef.DatatypeType;
} else if (type is SetType) {
return predef.SetType(Token.NoToken, predef.BoxType);
} else if (type is SeqType) {
@@ -1793,7 +1819,7 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(nw)));
// assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);
- builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, etran.GoodRef_Class(tok, nw, (ClassType)((TypeRhs)rhs).Type, true))));
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, etran.GoodRef_Class(tok, nw, (UserDefinedType)((TypeRhs)rhs).Type, true))));
// $Heap[$nw, alloc] := true;
Bpl.Expr alloc = predef.Alloc(tok);
Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr, nw, alloc, Bpl.Expr.True);
@@ -1912,7 +1938,6 @@ namespace Microsoft.Dafny { SeqUpdateExpr e = (SeqUpdateExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
Type elmtType = ((SeqType!)e.Seq.Type).Arg;
- Bpl.Type elType = translator.TrType(elmtType);
Bpl.Expr index = TrExpr(e.Index);
Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
@@ -2236,17 +2261,17 @@ namespace Microsoft.Dafny { public Bpl.Expr! GoodRef(Token! tok, Bpl.Expr! e, Type! type) {
Bpl.Expr goodRef;
- if (type is ClassType && ((ClassType)type).ResolvedClass != null) {
+ if (type is UserDefinedType && ((UserDefinedType)type).ResolvedClass != null) {
// Heap[e, alloc] && dtype(e) == T
- return GoodRef_Class(tok, e, (ClassType)type, false);
+ return GoodRef_Class(tok, e, (UserDefinedType)type, false);
} else {
// Heap[e, alloc]
return IsAlloced(tok, e);
}
}
- public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, ClassType! type, bool isNew)
- requires type.ResolvedClass != null;
+ public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
+ requires type.ResolvedClass is ClassDecl;
{
// Heap[e, alloc]
Bpl.Expr r = IsAlloced(tok, e);
diff --git a/Test/alltests.txt b/Test/alltests.txt index 2a7e11bd..359a27f8 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -20,3 +20,4 @@ z3api Postponed Test for Z3 Managed .NET API prover houdini Postponed Test for Houdini decision procedure
dafny0 Use Dafny programs
havoc0 Use HAVOC-generated bpl files
+VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e7f7c4d6..9c74a7ea 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -32,6 +32,24 @@ class MyClass<T, U> { }
}
+datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
+}
+
+datatype WildData {
+ Something;
+ JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);
+ More(List<int>);
+}
+
+datatype Nothing { }
+
+class C {
+ var w: WildData;
+ var list: List<bool>;
+}
+
Dafny program verifier finished with 0 verified, 0 errors
-------------------- BQueue.bpl --------------------
diff --git a/Test/dafny0/Datatypes.bpl b/Test/dafny0/Datatypes.bpl new file mode 100644 index 00000000..0a66ab16 --- /dev/null +++ b/Test/dafny0/Datatypes.bpl @@ -0,0 +1,306 @@ +// Dafny program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
+// Command Line Options: Datatypes.dfy /dprint:- /print:Datatyps.bpl
+
+type ref;
+
+const null: ref;
+
+type Set T = [T]bool;
+
+function Set#Empty<T>() returns (Set T);
+
+axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
+
+function Set#Singleton<T>(T) returns (Set T);
+
+axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
+
+axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
+
+function Set#UnionOne<T>(Set T, T) returns (Set T);
+
+axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a, x)[o] } Set#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+function Set#Union<T>(Set T, Set T) returns (Set T);
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a, b)[o] } Set#Union(a, b)[o] <==> a[o] || b[o]);
+
+function Set#Intersection<T>(Set T, Set T) returns (Set T);
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a, b)[o] } Set#Intersection(a, b)[o] <==> a[o] && b[o]);
+
+function Set#Difference<T>(Set T, Set T) returns (Set T);
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a, b)[o] } Set#Difference(a, b)[o] <==> a[o] && !b[o]);
+
+function Set#Subset<T>(Set T, Set T) returns (bool);
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Subset(a, b) } Set#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
+
+function Set#Equal<T>(Set T, Set T) returns (bool);
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b);
+
+function Set#Disjoint<T>(Set T, Set T) returns (bool);
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a, b) } Set#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
+
+type Seq _;
+
+function Seq#Length<T>(Seq T) returns (int);
+
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() returns (Seq T);
+
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
+
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+function Seq#Singleton<T>(T) returns (Seq T);
+
+axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+
+axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s, i, v, len)) } 0 <= len ==> Seq#Length(Seq#Build(s, i, v, len)) == len);
+
+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0, s1)) } Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+function Seq#Index<T>(Seq T, int) returns (T);
+
+axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0, s1), n) } (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n)) && (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s, i, v, len), n) } 0 <= n && n < len ==> (i == n ==> Seq#Index(Seq#Build(s, i, v, len), n) == v) && (i != n ==> Seq#Index(Seq#Build(s, i, v, len), n) == Seq#Index(s, n)));
+
+function Seq#Update<T>(Seq T, int, T) returns (Seq T);
+
+axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s, i, v)) } 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s, i, v), n) } 0 <= n && n < Seq#Length(s) ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v) && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n)));
+
+function Seq#Contains<T>(Seq T, T) returns (bool);
+
+axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s, x) } Seq#Contains(s, x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall x: ref :: { Seq#Contains(Seq#Empty(), x) } !Seq#Contains(Seq#Empty(), x));
+
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T :: { Seq#Contains(Seq#Append(s0, s1), x) } Seq#Contains(Seq#Append(s0, s1), x) <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));
+
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T :: { Seq#Contains(Seq#Build(s, i, v, len), x) } Seq#Contains(Seq#Build(s, i, v, len), x) <==> (0 <= i && i < len && x == v) || (exists j: int :: { Seq#Index(s, j) } 0 <= j && j < Seq#Length(s) && j < len && j != i && Seq#Index(s, j) == x));
+
+axiom (forall<T> s: Seq T, n: int, x: T :: { Seq#Contains(Seq#Take(s, n), x) } Seq#Contains(Seq#Take(s, n), x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall<T> s: Seq T, n: int, x: T :: { Seq#Contains(Seq#Drop(s, n), x) } Seq#Contains(Seq#Drop(s, n), x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0, s1) } Seq#Equal(s0, s1) <==> Seq#Length(s0) == Seq#Length(s1) && (forall j: int :: { Seq#Index(s0, j) } { Seq#Index(s1, j) } 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0, s1, n) } Seq#SameUntil(s0, s1, n) <==> (forall j: int :: { Seq#Index(s0, j) } { Seq#Index(s1, j) } 0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s, n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s, n)) == Seq#Length(s)));
+
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s, n), j) } 0 <= j && j < n && j < Seq#Length(s) ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s, n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s, n)) == 0));
+
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s, n), j) } 0 <= n && 0 <= j && j < Seq#Length(s) - n ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));
+
+type BoxType;
+
+function $Box<T>(T) returns (BoxType);
+
+function $Unbox<T>(BoxType) returns (T);
+
+axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+
+axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
+
+axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
+
+axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
+
+axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
+
+type ClassName;
+
+const unique class.int: ClassName;
+
+const unique class.bool: ClassName;
+
+const unique class.object: ClassName;
+
+const unique class.set: ClassName;
+
+const unique class.seq: ClassName;
+
+function dtype(ref) returns (ClassName);
+
+function TypeParams(ref, int) returns (ClassName);
+
+function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);
+
+function TypeTupleCar(ClassName) returns (ClassName);
+
+function TypeTupleCdr(ClassName) returns (ClassName);
+
+axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a, b) } TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);
+
+type DatatypeType;
+
+type Field _;
+
+type HeapType = <alpha>[ref,Field alpha]alpha;
+
+function $IsGoodHeap(HeapType) returns (bool);
+
+var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap);
+
+const unique #loc.$Heap: $token;
+
+const unique alloc: Field bool;
+
+function DeclType<T>(Field T) returns (ClassName);
+
+function $HeapSucc(HeapType, HeapType) returns (bool);
+
+axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h, k) } $HeapSucc(h, k) ==> (forall o: ref :: { k[o, alloc] } h[o, alloc] ==> k[o, alloc]));
+
+axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);
+
+axiom (forall x: int, y: int :: { x % y } 0 < y ==> 0 <= x % y && x % y < y);
+
+axiom (forall x: int, y: int :: { x % y } y < 0 ==> y < x % y && x % y <= 0);
+
+axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+
+type $token;
+
+function $file_name_is(id: int, tok: $token) returns (bool);
+
+type cf_event;
+
+type var_locglob;
+
+const unique conditional_moment: cf_event;
+
+const unique took_then_branch: cf_event;
+
+const unique took_else_branch: cf_event;
+
+const unique loop_register: cf_event;
+
+const unique loop_entered: cf_event;
+
+const unique loop_exited: cf_event;
+
+const unique cev_local: var_locglob;
+
+const unique cev_global: var_locglob;
+
+const unique cev_parameter: var_locglob;
+
+const unique cev_implicit: var_locglob;
+
+function #cev_init(n: int) returns (bool);
+
+function #cev_save_position(n: int) returns ($token);
+
+function #cev_var_intro<T,U>(n: int, locorglob: var_locglob, name: $token, val: T, typ: U) returns (bool);
+
+function #cev_var_update<T>(n: int, locorglob: var_locglob, name: $token, val: T) returns (bool);
+
+function #cev_control_flow_event(n: int, tag: cf_event) returns (bool);
+
+function #cev_function_call(n: int) returns (bool);
+
+var #cev_pc: int;
+
+procedure CevVarIntro<T>(pos: $token, locorglob: var_locglob, name: $token, val: T);
+ modifies #cev_pc;
+ ensures #cev_var_intro(old(#cev_pc), locorglob, name, val, 0);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+
+
+procedure CevUpdateHere<T>(name: $token, val: T);
+ ensures #cev_var_update(#cev_pc, cev_local, name, val);
+
+
+
+procedure CevStep(pos: $token);
+ modifies #cev_pc;
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+
+
+procedure CevUpdate<T>(pos: $token, name: $token, val: T);
+ modifies #cev_pc;
+ ensures #cev_var_update(old(#cev_pc), cev_local, name, val);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+
+
+procedure CevUpdateHeap(pos: $token, name: $token, val: HeapType);
+ modifies #cev_pc;
+ ensures #cev_var_update(old(#cev_pc), cev_implicit, name, val);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+
+
+procedure CevEvent(pos: $token, tag: cf_event);
+ modifies #cev_pc;
+ ensures #cev_control_flow_event(old(#cev_pc), tag);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+
+
+procedure CevStepEvent(pos: $token, tag: cf_event);
+ modifies #cev_pc;
+ ensures #cev_control_flow_event(old(#cev_pc) + 1, tag);
+ ensures #cev_save_position(old(#cev_pc) + 1) == pos;
+ ensures #cev_pc == old(#cev_pc) + 2;
+
+
+
+procedure CevPreLoop(pos: $token) returns (oldPC: int);
+ modifies #cev_pc;
+ ensures #cev_control_flow_event(old(#cev_pc), conditional_moment);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures oldPC == old(#cev_pc) && #cev_pc == old(#cev_pc) + 1;
+
+
+
+const unique class.C: ClassName;
+
+axiom DeclType(C.w) == class.C;
+
+const unique C.w: Field DatatypeType;
+
+axiom (forall $h: HeapType, $o: ref :: { $h[$o, C.w] } $IsGoodHeap($h) && $o != null && $h[$o, alloc] ==> $h[$o, C.w] == null || ($h[$h[$o, C.w], alloc] && dtype($h[$o, C.w]) == class.WildData));
+
+axiom DeclType(C.list) == class.C;
+
+const unique C.list: Field DatatypeType;
+
+axiom (forall $h: HeapType, $o: ref :: { $h[$o, C.list] } $IsGoodHeap($h) && $o != null && $h[$o, alloc] ==> $h[$o, C.list] == null || ($h[$h[$o, C.list], alloc] && dtype($h[$o, C.list]) == class.List && TypeParams($h[$o, C.list], 0) == class.bool));
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 5f0bee87..a224ed91 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -28,3 +28,24 @@ class MyClass<T,U> { }
}
}
+
+// some datatype stuff:
+
+datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
+}
+
+datatype WildData {
+ Something();
+ JustAboutAnything<G,H>(G, myName: set<H>, int, WildData);
+ More(List<int>);
+}
+
+datatype Nothing {
+}
+
+class C {
+ var w: WildData;
+ var list: List<bool>;
+}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 508ffbaf..9d3ed5e0 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -30,14 +30,14 @@ ]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "function" "frame" "var" "method"
+ "class" "datatype" "function" "frame" "var" "method"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
- "false" "true" "null")) . font-lock-keyword-face)
+ "match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 69cd6b0a..f334e770 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,13 +5,13 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,bool,int,object,set,seq,%
+ morekeywords={class,datatype,bool,int,object,set,seq,%
function,returns,
var,
method,in,
requires,modifies,ensures,reads,free,
% expressions
- false,true,null,old,fresh,this,
+ match,case,false,true,null,old,fresh,this,
% statements
assert,assume,new,havoc,call,if,else,while,invariant,break,return,foreach,
},
|