summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.ssc1051
-rw-r--r--Source/Dafny/Dafny.atg28
-rw-r--r--Source/Dafny/DafnyAst.ssc34
-rw-r--r--Source/Dafny/DafnyPipeline.sscproj4
-rw-r--r--Source/Dafny/Parser.ssc464
-rw-r--r--Source/Dafny/Printer.ssc32
-rw-r--r--Source/Dafny/Resolver.ssc69
-rw-r--r--Source/Dafny/Scanner.ssc85
-rw-r--r--Source/Dafny/Translator.ssc9
9 files changed, 1466 insertions, 310 deletions
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc
new file mode 100644
index 00000000..decbcdaa
--- /dev/null
+++ b/Source/Dafny/Compiler.ssc
@@ -0,0 +1,1051 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections.Generic;
+using System.Numerics;
+using System.IO;
+using Microsoft.Contracts;
+using Bpl = Microsoft.Boogie;
+using System.Text;
+
+namespace Microsoft.Dafny {
+ public class Compiler {
+ public Compiler(TextWriter! wr) {
+ this.wr = wr;
+ }
+
+ TextWriter! wr;
+
+ public int ErrorCount;
+ void Error(string! msg, params object[] args) {
+ string s = string.Format("Compilation error: " + msg, args);
+ Console.WriteLine(s);
+ wr.WriteLine("/* {0} */", s);
+ ErrorCount++;
+ }
+
+ void ReadRuntimeSystem() {
+ string! codebase = (!) System.IO.Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ string! path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
+ using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))
+ {
+ while (true) {
+ string s = rd.ReadLine();
+ if (s == null)
+ return;
+ wr.WriteLine(s);
+ }
+ }
+ }
+
+ readonly int IndentAmount = 2;
+ void Indent(int ind) {
+ string spaces = " ";
+ for (; spaces.Length < ind; ind -= spaces.Length) {
+ wr.Write(spaces);
+ }
+ wr.Write(spaces.Substring(0, ind));
+ }
+
+ public void Compile(Program! program) {
+ wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
+ wr.WriteLine();
+ ReadRuntimeSystem();
+
+ foreach (ModuleDecl m in program.Modules) {
+ int indent = 0;
+ if (!m.IsDefaultModule) {
+ wr.WriteLine("namespace {0} {{", m.Name);
+ indent += IndentAmount;
+ }
+ foreach (TopLevelDecl d in m.TopLevelDecls) {
+ wr.WriteLine();
+ if (d is DatatypeDecl) {
+ DatatypeDecl dt = (DatatypeDecl)d;
+ Indent(indent);
+ wr.Write("public abstract class Base_{0}", dt.Name);
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
+ }
+ wr.WriteLine(" { }");
+ CompileDatatypeConstructors(dt, indent);
+ CompileDatatypeStruct(dt, indent);
+ } else {
+ ClassDecl cl = (ClassDecl)d;
+ Indent(indent);
+ wr.Write("public class {0}", cl.IsDefaultClass ? "_DefaultClass" : cl.Name);
+ if (cl.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
+ }
+ wr.WriteLine(" {");
+ CompileClassMembers(cl, indent+IndentAmount);
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+ if (!m.IsDefaultModule) {
+ wr.WriteLine("}} // end of namespace {0}", m.Name);
+ }
+ }
+ }
+
+ void CompileDatatypeConstructors(DatatypeDecl! dt, int indent)
+ {
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ // class Dt_Ctor<T,U> : Base_Dt<T> {
+ // Fields;
+ // public Dt_Ctor(arguments) {
+ // Fields = arguments;
+ // }
+ // }
+ Indent(indent);
+ wr.Write("public class {0}", DtCtorName(ctor));
+ if (dt.TypeArgs.Count != 0 || ctor.TypeArgs.Count != 0) {
+ wr.Write("<");
+ string sep = "";
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("{0}", TypeParameters(dt.TypeArgs));
+ sep = ",";
+ }
+ if (ctor.TypeArgs.Count != 0) {
+ wr.Write("{0}{1}", sep, TypeParameters(ctor.TypeArgs));
+ }
+ wr.Write(">");
+ }
+ wr.Write(" : Base_{0}", dt.Name);
+ wr.WriteLine(" {");
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
+ }
+ int ind = indent + IndentAmount;
+
+ int i = 0;
+ foreach (Formal arg in ctor.Formals) {
+ if (!arg.IsGhost) {
+ Indent(ind);
+ wr.WriteLine("public readonly {0} {1};", TypeName(arg.Type), FormalName(arg, i));
+ i++;
+ }
+ }
+
+ Indent(ind);
+ wr.Write("public {0}(", DtCtorName(ctor));
+ WriteFormals(ctor.Formals);
+ wr.WriteLine(") {");
+ i = 0;
+ foreach (Formal arg in ctor.Formals) {
+ if (!arg.IsGhost) {
+ Indent(ind + IndentAmount);
+ wr.WriteLine("this.{0} = {0};", FormalName(arg, i));
+ i++;
+ }
+ }
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+
+ void CompileDatatypeStruct(DatatypeDecl! dt, int indent) {
+ // public struct Dt<T> {
+ // Base_Dt<T> d;
+ // public Base_Dt<T> D {
+ // get { if (d == null) { d = Default; } return d; }
+ // }
+ // public Dt(Base_Dt<T> d) { this.d = d; }
+ // public static Base_Dt<T> Default {
+ // get { return ...; }
+ // }
+ // public override bool Equals(object other) {
+ // return other is Dt<T> && D.Equals(((Dt<T>)other).D);
+ // }
+ // public override int GetHashCode() { return D.GetHashCode(); }
+ // }
+ string DtT = dt.Name;
+ if (dt.TypeArgs.Count != 0) {
+ DtT += "<" + TypeParameters(dt.TypeArgs) + ">";
+ }
+
+ Indent(indent);
+ wr.WriteLine("public struct {0} {{", DtT);
+ int ind = indent + IndentAmount;
+
+ Indent(ind);
+ wr.WriteLine("Base_{0} d;", DtT);
+
+ Indent(ind);
+ wr.WriteLine("public Base_{0} D {{", DtT);
+ Indent(ind + IndentAmount);
+ wr.WriteLine("get { if (d == null) { d = Default; } return d; }");
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind);
+ wr.WriteLine("public {0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
+
+ Indent(ind);
+ wr.WriteLine("public static Base_{0} Default {{", DtT);
+ Indent(ind + IndentAmount);
+ wr.Write("get { return ");
+ wr.Write("new {0}", DtCtorName((!)dt.DefaultCtor));
+ // todo: type parameters
+ wr.Write("(");
+ string sep = "";
+ foreach (Formal f in dt.DefaultCtor.Formals) {
+ if (!f.IsGhost) {
+ wr.Write("{0}{1}", sep, DefaultValue(f.Type));
+ sep = ", ";
+ }
+ }
+ wr.Write(")");
+ wr.WriteLine("; }");
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
+ Indent(ind + IndentAmount);
+ wr.WriteLine("return other is {0} && D.Equals((({0})other).D);", DtT);
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind);
+ wr.WriteLine("public override int GetHashCode() { return D.GetHashCode(); }");
+
+ Indent(indent);
+ wr.WriteLine("}");
+ }
+
+ void WriteFormals(List<Formal!>! formals)
+ {
+ int i = 0;
+ string sep = "";
+ foreach (Formal arg in formals) {
+ if (!arg.IsGhost) {
+ string name = FormalName(arg, i);
+ wr.Write("{0}{1}{2} {3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);
+ sep = ", ";
+ i++;
+ }
+ }
+ }
+
+ string! FormalName(Formal! formal, int i) {
+ return formal.Name.StartsWith("#") ? "a" + i : formal.Name;
+ }
+
+ string! DtCtorName(DatatypeCtor! ctor) {
+ return ((!)ctor.EnclosingDatatype).Name + "_" + ctor.Name;
+ }
+
+ void CompileClassMembers(ClassDecl! c, int indent)
+ {
+ foreach (MemberDecl member in c.Members) {
+ if (member is Field) {
+ Field f = (Field)member;
+ if (!f.IsGhost) {
+ Indent(indent);
+ wr.WriteLine("public {0} {1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
+ }
+
+ } else if (member is Function) {
+ Function f = (Function)member;
+ if (f.IsGhost) {
+ // nothing to compile
+ } else if (f.Body == null) {
+ Error("Function {0} has no body", f.FullName);
+ } else {
+ Indent(indent);
+ wr.Write("public {0}{1} {2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);
+ if (f.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(f.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals(f.Formals);
+ wr.WriteLine(") {");
+ if (f.Body is MatchExpr) {
+ MatchExpr me = (MatchExpr)f.Body;
+ // Type source = e;
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ // return Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName((!)me.Source.Type), source);
+ TrExpr(me.Source);
+ wr.WriteLine(";");
+
+ int i = 0;
+ foreach (MatchCaseExpr mc in me.Cases) {
+ MatchCasePrelude(source, (!)mc.Ctor, mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
+
+ Indent(indent + 2*IndentAmount);
+ wr.Write("return ");
+ TrExpr(mc.Body);
+ wr.WriteLine(";");
+ i++;
+ }
+
+ Indent(indent); wr.WriteLine("}");
+
+ } else {
+ Indent(indent + IndentAmount);
+ wr.Write("return ");
+ TrExpr(f.Body);
+ wr.WriteLine(";");
+ }
+ Indent(indent); wr.WriteLine("}");
+ }
+
+ } else if (member is Method) {
+ Method m = (Method)member;
+ if (!m.IsGhost) {
+ Indent(indent);
+ wr.Write("public {0}void {1}", m.IsStatic ? "static " : "", m.Name);
+ if (m.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(m.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals(m.Ins);
+ if (m.Ins.Count != 0 && m.Outs.Count != 0) {
+ wr.Write(", ");
+ }
+ WriteFormals(m.Outs);
+ wr.WriteLine(")");
+ Indent(indent); wr.WriteLine("{");
+ foreach (Formal p in m.Outs) {
+ if (!p.IsGhost) {
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0} = {1};", p.Name, DefaultValue(p.Type));
+ }
+ }
+ if (m.Body == null) {
+ Error("Method {0} has no body", m.FullName);
+ } else {
+ TrStmtList(m.Body.Body, indent);
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ // allow the Main method to be an instance method
+ if (m.Name == "Main" && m.Ins.Count == 0 && m.Outs.Count == 0) {
+ Indent(indent);
+ wr.WriteLine("public static void Main(string[] args) {");
+ ClassDecl cl = (!)m.EnclosingClass;
+ Indent(indent + IndentAmount);
+ wr.Write("{0} b = new {0}", cl.Name);
+ if (cl.TypeArgs.Count != 0) {
+ // instantiate every parameter, it doesn't particularly matter how
+ wr.Write("<");
+ string sep = "";
+ for (int i = 0; i < cl.TypeArgs.Count; i++) {
+ wr.Write("{0}int", sep);
+ sep = ", ";
+ }
+ wr.Write(">");
+ }
+ wr.WriteLine("();");
+ Indent(indent + IndentAmount); wr.WriteLine("b.Main();");
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+
+ } else {
+ assert false; // unexpected member
+ }
+ }
+ }
+
+ // ----- Type ---------------------------------------------------------------------------------
+
+ readonly string! DafnySetClass = "Dafny.Set";
+ readonly string! DafnySeqClass = "Dafny.Sequence";
+
+ string! TypeName(Type! type)
+ {
+ while (true) {
+ TypeProxy tp = type as TypeProxy;
+ if (tp == null) {
+ break;
+ } else if (tp.T == null) {
+ // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
+ return "object";
+ } else {
+ type = tp.T;
+ }
+ }
+
+ if (type is BoolType) {
+ return "bool";
+ } else if (type is IntType) {
+ return "BigInteger";
+ } else if (type is ObjectType) {
+ return "object";
+ } else if (type is UserDefinedType) {
+ UserDefinedType udt = (UserDefinedType)type;
+ string s = udt.Name;
+ if (udt.TypeArgs.Count != 0) {
+ if (exists{Type argType in udt.TypeArgs; argType is ObjectType}) {
+ Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
+ }
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s;
+ } else if (type is SetType) {
+ Type argType = ((SetType)type).Arg;
+ if (argType is ObjectType) {
+ Error("compilation of set<object> is not supported; consider introducing a ghost");
+ }
+ return DafnySetClass + "<" + TypeName(argType) + ">";
+ } else if (type is SeqType) {
+ Type argType = ((SeqType)type).Arg;
+ if (argType is ObjectType) {
+ Error("compilation of seq<object> is not supported; consider introducing a ghost");
+ }
+ return DafnySeqClass + "<" + TypeName(argType) + ">";
+ } else {
+ assert false; // unexpected type
+ }
+ }
+
+ string! TypeNames(List<Type!>! types) {
+ string s = "";
+ string sep = "";
+ foreach (Type t in types) {
+ s += sep + TypeName(t);
+ sep = ",";
+ }
+ return s;
+ }
+
+ string! TypeParameters(List<TypeParameter!>! targs) {
+ string s = "";
+ string sep = "";
+ foreach (TypeParameter tp in targs) {
+ s += sep + tp.Name;
+ sep = ",";
+ }
+ return s;
+ }
+
+ string! DefaultValue(Type! type)
+ {
+ while (true) {
+ TypeProxy tp = type as TypeProxy;
+ if (tp == null) {
+ break;
+ } else if (tp.T == null) {
+ // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
+ return "null";
+ } else {
+ type = tp.T;
+ }
+ }
+
+ if (type is BoolType) {
+ return "false";
+ } else if (type is IntType) {
+ return "new BigInteger(0)";
+ } else if (type.IsRefType) {
+ return "null";
+ } else if (type.IsDatatype) {
+ UserDefinedType udt = (UserDefinedType)type;
+ string s = udt.Name;
+ if (udt.TypeArgs.Count != 0) {
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s + ".Default";
+ } else if (type.IsTypeParameter) {
+ UserDefinedType udt = (UserDefinedType)type;
+ return "default(" + udt.Name + ")";
+ } else if (type is SetType) {
+ return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";
+ } else if (type is SeqType) {
+ return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";
+ } else {
+ assert false; // unexpected type
+ }
+ }
+
+ // ----- Stmt ---------------------------------------------------------------------------------
+
+ void TrStmt(Statement! stmt, int indent)
+ {
+ if (stmt.IsGhost) {
+ return;
+ }
+
+ if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ foreach (Attributes.Argument arg in s.Args) {
+ Indent(indent);
+ wr.Write("System.Console.Write(");
+ if (arg.S != null) {
+ wr.Write("\"{0}\"", arg.S);
+ } else {
+ assert arg.E != null;
+ TrExpr(arg.E);
+ }
+ wr.WriteLine(");");
+ }
+ } else if (stmt is BreakStmt) {
+ BreakStmt s = (BreakStmt)stmt;
+ Indent(indent);
+ if (s.TargetLabel == null) {
+ // use the scoping rules of C#
+ wr.WriteLine("break;");
+ } else {
+ wr.WriteLine("goto after_{0};", s.TargetLabel);
+ }
+ } else if (stmt is ReturnStmt) {
+ Indent(indent);
+ wr.WriteLine("return;");
+ } else if (stmt is AssignStmt) {
+ AssignStmt s = (AssignStmt)stmt;
+ Indent(indent);
+ TrExpr(s.Lhs);
+ if (!(s.Rhs is HavocRhs)) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ }
+ wr.WriteLine(";");
+
+ } else if (stmt is VarDecl) {
+ TrVarDecl((VarDecl)stmt, true, indent);
+
+ } else if (stmt is CallStmt) {
+ CallStmt s = (CallStmt)stmt;
+
+ foreach (VarDecl local in s.NewVars) {
+ TrVarDecl(local, false, indent);
+ }
+
+ assert s.Method != null; // follows from the fact that stmt has been successfully resolved
+ Indent(indent);
+ if (s.Method.IsStatic) {
+ wr.Write(TypeName((!)s.Receiver.Type));
+ } else {
+ TrParenExpr(s.Receiver);
+ }
+ wr.Write(".{0}(", s.Method.Name);
+
+ string sep = "";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ wr.Write(sep);
+ TrExpr(s.Args[i]);
+ sep = ", ";
+ }
+ }
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ wr.Write("{0}out ", sep);
+ TrExpr(s.Lhs[i]);
+ sep = ", ";
+ }
+ }
+
+ wr.WriteLine(");");
+
+ } else if (stmt is BlockStmt) {
+ Indent(indent); wr.WriteLine("{");
+ TrStmtList(((BlockStmt)stmt).Body, indent);
+ Indent(indent); wr.WriteLine("}");
+
+ } else if (stmt is IfStmt) {
+ IfStmt s = (IfStmt)stmt;
+ Indent(indent);
+ if (s.Guard == null) {
+ wr.WriteLine("if (true)");
+ } else {
+ wr.Write("if (");
+ TrExpr(s.Guard);
+ wr.WriteLine(")");
+ }
+
+ TrStmt(s.Thn, indent);
+ if (s.Els != null) {
+ Indent(indent); wr.WriteLine("else");
+ TrStmt(s.Els, indent);
+ }
+
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ if (s.Guard == null) {
+ Indent(indent);
+ wr.WriteLine("while (false) { }");
+ } else {
+ Indent(indent);
+ wr.Write("while (");
+ TrExpr(s.Guard);
+ wr.WriteLine(")");
+ TrStmt(s.Body, indent);
+ }
+
+ } else if (stmt is ForeachStmt) {
+ ForeachStmt s = (ForeachStmt)stmt;
+ // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
+ // foreach (TType x in S) {
+ // if (Range(x)) {
+ // assert/assume ...;
+ // pendingUpdates.Add(new Pair(x,RHS));
+ // }
+ // }
+ // foreach (Pair<TType,RhsType> p in pendingUpdates) {
+ // p.Car.m = p.Cdr;
+ // }
+ string pu = "_pendingUpdates" + tmpVarCount;
+ string pr = "_pair" + tmpVarCount;
+ tmpVarCount++;
+ string TType = TypeName(s.BoundVar.Type);
+ string RhsType = TypeName((!)s.BodyAssign.Lhs.Type);
+
+ Indent(indent);
+ wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
+
+ Indent(indent);
+ wr.Write("foreach ({0} {1} in (", TType, s.BoundVar.Name);
+ TrExpr(s.Collection);
+ wr.WriteLine(").Elements) {");
+
+ Indent(indent + IndentAmount);
+ wr.Write("if (");
+ TrExpr(s.Range);
+ wr.WriteLine(") {");
+
+ foreach (PredicateStmt p in s.BodyPrefix) {
+ TrStmt(p, indent + 2*IndentAmount);
+ }
+ Indent(indent + 2*IndentAmount);
+ wr.Write("{0}.Add(new Pair<{1},{2}>({3}, ", pu, TType, RhsType, s.BoundVar.Name);
+ ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
+ if (rhsExpr != null) {
+ TrExpr(rhsExpr.Expr);
+ } else {
+ wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
+ }
+ wr.WriteLine("))");
+
+ Indent(indent + IndentAmount); wr.WriteLine("}");
+ Indent(indent); wr.WriteLine("}");
+
+ Indent(indent); wr.WriteLine("foreach (Pair<{0},{1}> {2} in {3}) {{", TType, RhsType, pr, pu);
+ Indent(indent + IndentAmount);
+ FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
+ wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
+ Indent(indent); wr.WriteLine("}");
+
+ } else if (stmt is MatchStmt) {
+ MatchStmt s = (MatchStmt)stmt;
+ // Type source = e;
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ // Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName((!)s.Source.Type), source);
+ TrExpr(s.Source);
+ wr.WriteLine(";");
+
+ int i = 0;
+ foreach (MatchCaseStmt mc in s.Cases) {
+ MatchCasePrelude(source, (!)mc.Ctor, mc.Arguments, i, s.Cases.Count, indent);
+ TrStmtList(mc.Body, indent);
+ i++;
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ } else {
+ assert false; // unexpected statement
+ }
+ }
+
+ int tmpVarCount = 0;
+
+ void TrAssignmentRhs(AssignmentRhs! rhs)
+ requires !(rhs is HavocRhs);
+ {
+ if (rhs is ExprRhs) {
+ ExprRhs e = (ExprRhs)rhs;
+ TrExpr(e.Expr);
+
+ } else {
+ TypeRhs tp = (TypeRhs)rhs;
+ wr.Write("new {0}()", TypeName(tp.Type));
+ }
+ }
+
+ void TrStmtList(List<Statement!>! stmts, int indent) {
+ List<string!> currentLabels = null;
+ foreach (Statement ss in stmts) {
+ if (ss is LabelStmt) {
+ LabelStmt s = (LabelStmt)ss;
+ if (currentLabels == null) {
+ currentLabels = new List<string!>();
+ }
+ currentLabels.Add(s.Label);
+ } else {
+ TrStmt(ss, indent + IndentAmount);
+ SpillLabels(currentLabels, indent);
+ currentLabels = null;
+ }
+ }
+ SpillLabels(currentLabels, indent);
+ }
+
+ void SpillLabels(List<string!> labels, int indent) {
+ if (labels != null) {
+ foreach (string label in labels) {
+ Indent(indent);
+ wr.WriteLine("after_{0}: ;", label);
+ }
+ }
+ }
+
+ void TrVarDecl(VarDecl! s, bool alwaysInitialize, int indent) {
+ Indent(indent);
+ wr.Write("{0} {1}", TypeName(s.Type), s.Name);
+ if (s.Rhs != null) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ } else if (alwaysInitialize) {
+ // produce a default value
+ wr.Write(" = {0}", DefaultValue(s.Type));
+ }
+ wr.WriteLine(";");
+ }
+
+ void MatchCasePrelude(string! source, DatatypeCtor! ctor, List<BoundVar!>! arguments, int caseIndex, int caseCount, int indent) {
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ Indent(indent);
+ wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");
+ if (caseIndex == caseCount - 1) {
+ wr.Write("true");
+ } else {
+ wr.Write("{0}.D is {1}", source, DtCtorName(ctor));
+ }
+ wr.WriteLine(") {");
+
+ int k = 0; // number of processed non-ghost arguments
+ for (int m = 0; m < ctor.Formals.Count; m++) {
+ Formal arg = ctor.Formals[m];
+ if (!arg.IsGhost) {
+ BoundVar bv = arguments[m];
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0} {1} = (({2}){3}.D).{4};",
+ TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k));
+ k++;
+ }
+ }
+ }
+
+ // ----- Expression ---------------------------------------------------------------------------
+
+ void TrParenExpr(string! prefix, Expression! expr) {
+ wr.Write(prefix);
+ TrParenExpr(expr);
+ }
+
+ void TrParenExpr(Expression! expr) {
+ wr.Write("(");
+ TrExpr(expr);
+ wr.Write(")");
+ }
+
+ void TrExprList(List<Expression!>! exprs) {
+ wr.Write("(");
+ string sep = "";
+ foreach (Expression e in exprs) {
+ wr.Write(sep);
+ TrExpr(e);
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+
+ void TrExpr(Expression! expr)
+ {
+ if (expr is LiteralExpr) {
+ LiteralExpr e = (LiteralExpr)expr;
+ if (e.Value == null) {
+ wr.Write("null");
+ } else if (e.Value is bool) {
+ wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is BigInteger) {
+ BigInteger i = (BigInteger)e.Value;
+ if (new BigInteger(int.MinValue) <= i && i <= new BigInteger(int.MaxValue)) {
+ wr.Write("new BigInteger({0})", i);
+ } else {
+ wr.Write("BigInteger.Parse(\"{0}\")", i);
+ }
+ } else {
+ assert false; // unexpected literal
+ }
+
+ } else if (expr is ThisExpr) {
+ wr.Write("this");
+
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ wr.Write(((!)e.Var).Name);
+
+ } else if (expr is SetDisplayExpr) {
+ SetDisplayExpr e = (SetDisplayExpr)expr;
+ Type elType = ((SetType!)e.Type).Arg;
+ wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
+ TrExprList(e.Elements);
+
+ } else if (expr is SeqDisplayExpr) {
+ SeqDisplayExpr e = (SeqDisplayExpr)expr;
+ Type elType = ((SeqType!)e.Type).Arg;
+ wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
+ TrExprList(e.Elements);
+
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr e = (FieldSelectExpr)expr;
+ TrParenExpr(e.Obj);
+ wr.Write(".{0}", e.FieldName);
+
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr e = (SeqSelectExpr)expr;
+ TrParenExpr(e.Seq);
+ if (e.SelectOne) {
+ assert e.E0 != null;
+ assert e.E1 == null;
+ TrParenExpr(".Select", e.E0);
+ } else {
+ if (e.E1 != null) {
+ TrParenExpr(".Take", e.E1);
+ }
+ if (e.E0 != null) {
+ TrParenExpr(".Drop", e.E0);
+ }
+ }
+
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ TrParenExpr(e.Seq);
+ wr.Write(".Update(");
+ TrExpr(e.Index);
+ wr.Write(", ");
+ TrExpr(e.Value);
+ wr.Write(")");
+
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ Function f = (!)e.Function;
+ if (f.IsStatic) {
+ wr.Write(TypeName((!)e.Receiver.Type));
+ } else {
+ TrParenExpr(e.Receiver);
+ }
+ wr.Write(".{0}", f.Name);
+ wr.Write("(");
+ string sep = "";
+ for (int i = 0; i < e.Args.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost) {
+ wr.Write(sep);
+ TrExpr(e.Args[i]);
+ sep = ", ";
+ }
+ }
+ wr.Write(")");
+
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ assert dtv.Ctor != null; // since dtv has been successfully resolved
+ wr.Write("new {0}(new {0}", dtv.DatatypeName, DtCtorName(dtv.Ctor));
+ if (dtv.InferredTypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));
+ }
+ wr.Write("(");
+ string sep = "";
+ for (int i = 0; i < dtv.Arguments.Count; i++) {
+ Formal formal = dtv.Ctor.Formals[i];
+ if (!formal.IsGhost) {
+ wr.Write(sep);
+ TrExpr(dtv.Arguments[i]);
+ sep = ", ";
+ }
+ }
+ wr.Write("))");
+
+ } else if (expr is OldExpr) {
+ assert false; // 'old' is always a ghost (right?)
+
+ } else if (expr is FreshExpr) {
+ assert false; // 'fresh' is always a ghost
+
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ switch (e.Op) {
+ case UnaryExpr.Opcode.Not:
+ wr.Write("!");
+ TrParenExpr(e.E);
+ break;
+ case UnaryExpr.Opcode.SeqLength:
+ TrParenExpr(e.E);
+ wr.Write(".Length");
+ break;
+ default:
+ assert false; // unexpected unary expression
+ }
+
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ string opString = null;
+ string preOpString = "";
+ string callString = null;
+
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Iff:
+ opString = "=="; break;
+ case BinaryExpr.ResolvedOpcode.Imp:
+ preOpString = "!"; opString = "||"; break;
+ case BinaryExpr.ResolvedOpcode.Or:
+ opString = "||"; break;
+ case BinaryExpr.ResolvedOpcode.And:
+ opString = "&&"; break;
+
+ case BinaryExpr.ResolvedOpcode.EqCommon: {
+ Type t = (!)e.E0.Type;
+ if (t.IsDatatype || t.IsTypeParameter) {
+ callString = "Equals";
+ } else {
+ opString = "==";
+ }
+ break;
+ }
+ case BinaryExpr.ResolvedOpcode.NeqCommon: {
+ Type t = (!)e.E0.Type;
+ if (t.IsDatatype || t.IsTypeParameter) {
+ preOpString = "!";
+ callString = "Equals";
+ } else {
+ opString = "!=";
+ }
+ break;
+ }
+
+ case BinaryExpr.ResolvedOpcode.Lt:
+ opString = "<"; break;
+ case BinaryExpr.ResolvedOpcode.Le:
+ opString = "<="; break;
+ case BinaryExpr.ResolvedOpcode.Ge:
+ opString = ">="; break;
+ case BinaryExpr.ResolvedOpcode.Gt:
+ opString = ">"; break;
+ case BinaryExpr.ResolvedOpcode.Add:
+ opString = "+"; break;
+ case BinaryExpr.ResolvedOpcode.Sub:
+ opString = "-"; break;
+ case BinaryExpr.ResolvedOpcode.Mul:
+ opString = "*"; break;
+ case BinaryExpr.ResolvedOpcode.Div:
+ opString = "/"; break;
+ case BinaryExpr.ResolvedOpcode.Mod:
+ opString = "%"; break;
+
+ case BinaryExpr.ResolvedOpcode.SetEq:
+ case BinaryExpr.ResolvedOpcode.SeqEq:
+ callString = "Equals"; break;
+ case BinaryExpr.ResolvedOpcode.SetNeq:
+ case BinaryExpr.ResolvedOpcode.SeqNeq:
+ preOpString = "!"; callString = "Equals"; break;
+
+ case BinaryExpr.ResolvedOpcode.ProperSubset:
+ callString = "IsProperSubsetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Subset:
+ callString = "IsSubsetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Superset:
+ callString = "IsSupersetOf"; break;
+ case BinaryExpr.ResolvedOpcode.ProperSuperset:
+ callString = "IsProperSupersetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Disjoint:
+ callString = "IsDisjointFrom"; break;
+ case BinaryExpr.ResolvedOpcode.InSet:
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+ case BinaryExpr.ResolvedOpcode.Union:
+ callString = "Union"; break;
+ case BinaryExpr.ResolvedOpcode.Intersection:
+ callString = "Intersect"; break;
+ case BinaryExpr.ResolvedOpcode.SetDifference:
+ callString = "Difference"; break;
+
+ case BinaryExpr.ResolvedOpcode.ProperPrefix:
+ callString = "IsProperPrefixOf"; break;
+ case BinaryExpr.ResolvedOpcode.Prefix:
+ callString = "IsPrefixOf"; break;
+ case BinaryExpr.ResolvedOpcode.Concat:
+ callString = "Concat"; break;
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ wr.Write("!");
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+
+ default:
+ assert false; // unexpected binary expression
+ }
+ if (opString != null) {
+ wr.Write(preOpString);
+ TrParenExpr(e.E0);
+ wr.Write(" {0} ", opString);
+ TrParenExpr(e.E1);
+ } else if (callString != null) {
+ wr.Write(preOpString);
+ TrParenExpr(e.E0);
+ wr.Write(".{0}(", callString);
+ TrExpr(e.E1);
+ wr.Write(")");
+ }
+
+ } else if (expr is QuantifierExpr) {
+ assert false; // a quantifier is always a ghost
+
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ wr.Write("(");
+ TrExpr(e.Test);
+ wr.Write(") ? (");
+ TrExpr(e.Thn);
+ wr.Write(") : (");
+ TrExpr(e.Els);
+ wr.Write(")");
+
+ } else {
+ assert false; // unexpected expression
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3d07af57..351905e1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -252,8 +252,10 @@ 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; .)
+TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool isGhost>
+= (. string name = null; isGhost = false; .)
+ [ "ghost" (. isGhost = true; .)
+ ]
TypeAndToken<out id, out ty>
[ ":"
(. /* try to convert ty to an identifier */
@@ -297,7 +299,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
- Statement! bb; Statement body = null;
+ Statement! bb; BlockStmt body = null;
.)
"method"
(. if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
@@ -312,7 +314,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
]
( ";" { MethodSpec<req, mod, ens, dec> }
- | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb> (. body = bb; .)
+ | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb> (. body = (BlockStmt)bb; .)
)
(. parseVarScope.PopMarker();
@@ -349,11 +351,11 @@ Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals>
.
FormalsOptionalIds<List<Formal!\>! formals>
-= (. Token! id; Type! ty; string! name; .)
+= (. Token! id; Type! ty; string! name; bool isGhost; .)
"("
[
- TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
- { "," TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
+ TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
+ { "," TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
}
]
")"
@@ -549,6 +551,7 @@ OneStmt<out Statement! s>
( AssertStmt<out s>
| AssumeStmt<out s>
| UseStmt<out s>
+ | PrintStmt<out s>
| AssignStmt<out s>
| HavocStmt<out s>
| CallStmt<out s>
@@ -828,6 +831,17 @@ UseStmt<out Statement! s>
Expression<out e> ";" (. s = new UseStmt(x, e); .)
.
+PrintStmt<out Statement! s>
+= (. Token! x; Attributes.Argument! arg;
+ List<Attributes.Argument!> args = new List<Attributes.Argument!>();
+ .)
+ "print" (. x = token; .)
+ AttributeArg<out arg> (. args.Add(arg); .)
+ { "," AttributeArg<out arg> (. args.Add(arg); .)
+ }
+ ";" (. s = new PrintStmt(x, args); .)
+ .
+
/*------------------------------------------------------------------------*/
Expression<out Expression! e>
= (. Token! x; Expression! e0; Expression! e1 = dummyExpr;
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index a317155c..ae07c84a 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -353,7 +353,7 @@ namespace Microsoft.Dafny
public class DefaultModuleDecl : ModuleDecl {
public DefaultModuleDecl() {
- base(Token.NoToken, "$default", new List<string!>(), null);
+ base(Token.NoToken, "_default", new List<string!>(), null);
}
public override bool IsDefaultModule {
get { return true; }
@@ -385,7 +385,7 @@ namespace Microsoft.Dafny
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(DefaultModuleDecl! module, [Captured] List<MemberDecl!>! members) {
- base(Token.NoToken, "$default", module, new List<TypeParameter!>(), members, null);
+ base(Token.NoToken, "_default", module, new List<TypeParameter!>(), members, null);
}
public override bool IsDefaultClass {
get { return true; }
@@ -394,6 +394,7 @@ namespace Microsoft.Dafny
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor!>! Ctors;
+ public DatatypeCtor DefaultCtor; // set during resolution
public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
Ctors = ctors;
@@ -483,8 +484,11 @@ namespace Microsoft.Dafny
}
} }
public abstract bool IsMutable { get; }
- readonly bool isGhost;
- public bool IsGhost { get { return isGhost; } }
+ bool isGhost; // readonly, except for BoundVar's of match expressions/statements during resolution
+ public bool IsGhost {
+ get { return isGhost; }
+ set { isGhost = value; }
+ }
public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) {
this.tok = tok;
@@ -552,7 +556,7 @@ namespace Microsoft.Dafny
public readonly List<Expression!>! Mod;
public readonly List<MaybeFreeExpression!>! Ens;
public readonly List<Expression!>! Decreases;
- public readonly Statement Body;
+ public readonly BlockStmt Body;
public Method(Token! tok, string! name,
bool isStatic, bool isGhost,
@@ -560,7 +564,7 @@ namespace Microsoft.Dafny
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
[Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
[Captured] List<Expression!>! decreases,
- [Captured] Statement body,
+ [Captured] BlockStmt body,
Attributes attributes) {
this.IsStatic = isStatic;
this.IsGhost = isGhost;
@@ -580,6 +584,7 @@ namespace Microsoft.Dafny
public abstract class Statement {
public readonly Token! Tok;
+ public bool IsGhost; // filled in by resolution
public Statement(Token! tok) {
this.Tok = tok;
}
@@ -653,6 +658,15 @@ namespace Microsoft.Dafny
}
}
+ public class PrintStmt : Statement {
+ public readonly List<Attributes.Argument!>! Args;
+ public PrintStmt(Token! tok, List<Attributes.Argument!>! args)
+ {
+ base(tok);
+ Args = args;
+ }
+ }
+
public class LabelStmt : Statement {
public readonly string! Label;
public LabelStmt(Token! tok, string! label) {
@@ -746,8 +760,7 @@ namespace Microsoft.Dafny
}
} }
public bool IsMutable { get { return true; } }
- protected bool isGhost;
- public bool IsGhost { get { return isGhost; } }
+ bool IVariable.IsGhost { get { return base.IsGhost; } }
public readonly DeterminedAssignmentRhs Rhs;
invariant OptionalType != null || Rhs != null;
@@ -757,7 +770,7 @@ namespace Microsoft.Dafny
{
this.name = name;
this.OptionalType = type;
- this.isGhost = isGhost;
+ this.IsGhost = isGhost;
this.Rhs = rhs;
base(tok);
}
@@ -774,7 +787,7 @@ namespace Microsoft.Dafny
/// This method retrospectively makes the VarDecl a ghost. It is to be used only during resolution.
/// </summary>
public void MakeGhost() {
- isGhost = true;
+ base.IsGhost = true;
}
}
@@ -968,6 +981,7 @@ namespace Microsoft.Dafny
public readonly string! MemberName;
public readonly List<Expression!>! Arguments;
public DatatypeCtor Ctor; // filled in by resolution
+ public List<Type!>! InferredTypeArgs = new List<Type!>(); // filled in by resolution
public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {
this.DatatypeName = datatypeName;
diff --git a/Source/Dafny/DafnyPipeline.sscproj b/Source/Dafny/DafnyPipeline.sscproj
index 18653957..3bbf5366 100644
--- a/Source/Dafny/DafnyPipeline.sscproj
+++ b/Source/Dafny/DafnyPipeline.sscproj
@@ -131,6 +131,10 @@
SubType="Code"
RelPath="SccGraph.ssc"
/>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Compiler.ssc"
+ />
</Include>
</Files>
</XEN>
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 9551f031..0792f6bb 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -6,7 +6,7 @@ using Microsoft.Contracts;
namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 96;
+ const int maxT = 97;
const bool T = true;
const bool x = false;
@@ -285,7 +285,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
} else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(97);
+ } else Error(98);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -363,7 +363,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
FunctionBody(out bb);
body = bb;
- } else Error(98);
+ } else Error(99);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -379,7 +379,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
- Statement! bb; Statement body = null;
+ Statement! bb; BlockStmt body = null;
Expect(19);
if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
@@ -407,8 +407,8 @@ public static int Parse (List<ModuleDecl!>! modules) {
MethodSpec(req, mod, ens, dec);
}
BlockStmt(out bb);
- body = bb;
- } else Error(99);
+ body = (BlockStmt)bb;
+ } else Error(100);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -438,15 +438,15 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
static void FormalsOptionalIds(List<Formal!>! formals) {
- Token! id; Type! ty; string! name;
+ Token! id; Type! ty; string! name; bool isGhost;
Expect(26);
if (StartOf(6)) {
- TypeIdentOptional(out id, out name, out ty);
- formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
+ TypeIdentOptional(out id, out name, out ty, out isGhost);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
while (t.kind == 15) {
Get();
- TypeIdentOptional(out id, out name, out ty);
- formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
+ TypeIdentOptional(out id, out name, out ty, out isGhost);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
}
}
Expect(27);
@@ -484,8 +484,12 @@ public static int Parse (List<ModuleDecl!>! modules) {
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;
+ static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty, out bool isGhost) {
+ string name = null; isGhost = false;
+ if (t.kind == 9) {
+ Get();
+ isGhost = true;
+ }
TypeAndToken(out id, out ty);
if (t.kind == 16) {
Get();
@@ -536,7 +540,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
} else if (t.kind == 1 || t.kind == 32) {
ReferenceType(out tok, out ty);
- } else Error(100);
+ } else Error(101);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -585,12 +589,12 @@ List<Expression!>! decreases) {
Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(101);
+ } else Error(102);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(102);
+ } else Error(103);
}
static void BlockStmt(out Statement! block) {
@@ -617,14 +621,14 @@ List<Expression!>! decreases) {
Get();
x = token;
Expression(out e);
- Expect(55);
+ Expect(56);
Expression(out e0);
Expect(46);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(103);
+ } else Error(104);
}
static void Expressions(List<Expression!>! args) {
@@ -665,7 +669,7 @@ List<Expression!>! decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(104);
+ } else Error(105);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
@@ -685,7 +689,7 @@ List<Expression!>! decreases) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(105);
+ } else Error(106);
}
static void FunctionBody(out Expression! e) {
@@ -695,7 +699,7 @@ List<Expression!>! decreases) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(106);
+ } else Error(107);
Expect(7);
}
@@ -717,7 +721,7 @@ List<Expression!>! decreases) {
e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(107);
+ } else Error(108);
}
static void MatchExpression(out Expression! e) {
@@ -772,7 +776,7 @@ List<Expression!>! decreases) {
ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(108);
+ } else Error(109);
}
static void OneStmt(out Statement! s) {
@@ -792,7 +796,11 @@ List<Expression!>! decreases) {
UseStmt(out s);
break;
}
- case 1: case 26: case 88: case 89: {
+ case 55: {
+ PrintStmt(out s);
+ break;
+ }
+ case 1: case 26: case 89: case 90: {
AssignStmt(out s);
break;
}
@@ -846,7 +854,7 @@ List<Expression!>! decreases) {
s = new ReturnStmt(x);
break;
}
- default: Error(109); break;
+ default: Error(110); break;
}
}
@@ -894,6 +902,23 @@ List<Expression!>! decreases) {
s = new UseStmt(x, e);
}
+ static void PrintStmt(out Statement! s) {
+ Token! x; Attributes.Argument! arg;
+ List<Attributes.Argument!> args = new List<Attributes.Argument!>();
+
+ Expect(55);
+ x = token;
+ AttributeArg(out arg);
+ args.Add(arg);
+ while (t.kind == 15) {
+ Get();
+ AttributeArg(out arg);
+ args.Add(arg);
+ }
+ Expect(13);
+ s = new PrintStmt(x, args);
+ }
+
static void AssignStmt(out Statement! s) {
Token! x;
Expression! lhs;
@@ -998,7 +1023,7 @@ List<Expression!>! decreases) {
} else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(110);
+ } else Error(111);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1098,7 +1123,7 @@ List<Expression!>! decreases) {
} else if (t.kind == 44) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(111);
+ } else Error(112);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1124,7 +1149,7 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(112);
+ } else Error(113);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1132,10 +1157,10 @@ List<Expression!>! decreases) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
+ } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
ObjectExpression(out e);
- } else Error(113);
- while (t.kind == 83 || t.kind == 85) {
+ } else Error(114);
+ while (t.kind == 84 || t.kind == 86) {
SelectOrCallSuffix(ref e);
}
}
@@ -1176,7 +1201,7 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(114);
+ } else Error(115);
Expect(27);
}
@@ -1215,19 +1240,30 @@ List<Expression!>! decreases) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
+ } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(115);
- while (t.kind == 83 || t.kind == 85) {
+ } else Error(116);
+ while (t.kind == 84 || t.kind == 86) {
SelectOrCallSuffix(ref e);
}
}
+ static void AttributeArg(out Attributes.Argument! arg) {
+ Expression! e; arg = dummyAttrArg;
+ if (t.kind == 3) {
+ Get();
+ arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
+ } else if (StartOf(7)) {
+ Expression(out e);
+ arg = new Attributes.Argument(e);
+ } else Error(117);
+ }
+
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 56 || t.kind == 57) {
+ while (t.kind == 57 || t.kind == 58) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1238,7 +1274,7 @@ List<Expression!>! decreases) {
static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 58 || t.kind == 59) {
+ if (t.kind == 59 || t.kind == 60) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1247,23 +1283,23 @@ List<Expression!>! decreases) {
}
static void EquivOp() {
- if (t.kind == 56) {
+ if (t.kind == 57) {
Get();
- } else if (t.kind == 57) {
+ } else if (t.kind == 58) {
Get();
- } else Error(116);
+ } else Error(118);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 60 || t.kind == 61) {
+ if (t.kind == 61 || t.kind == 62) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 60 || t.kind == 61) {
+ while (t.kind == 61 || t.kind == 62) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1274,7 +1310,7 @@ List<Expression!>! decreases) {
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 62 || t.kind == 63) {
+ while (t.kind == 63 || t.kind == 64) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1285,11 +1321,11 @@ List<Expression!>! decreases) {
}
static void ImpliesOp() {
- if (t.kind == 58) {
+ if (t.kind == 59) {
Get();
- } else if (t.kind == 59) {
+ } else if (t.kind == 60) {
Get();
- } else Error(117);
+ } else Error(119);
}
static void RelationalExpression(out Expression! e0) {
@@ -1303,25 +1339,25 @@ List<Expression!>! decreases) {
}
static void AndOp() {
- if (t.kind == 60) {
+ if (t.kind == 61) {
Get();
- } else if (t.kind == 61) {
+ } else if (t.kind == 62) {
Get();
- } else Error(118);
+ } else Error(120);
}
static void OrOp() {
- if (t.kind == 62) {
+ if (t.kind == 63) {
Get();
- } else if (t.kind == 63) {
+ } else if (t.kind == 64) {
Get();
- } else Error(119);
+ } else Error(121);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 73 || t.kind == 74) {
+ while (t.kind == 74 || t.kind == 75) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1331,7 +1367,7 @@ List<Expression!>! decreases) {
static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 64: {
+ case 65: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1346,22 +1382,22 @@ List<Expression!>! decreases) {
x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 65: {
+ case 66: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 66: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 67: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 68: {
+ case 69: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
@@ -1371,34 +1407,34 @@ List<Expression!>! decreases) {
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 69: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 70: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 71: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 72: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(120); break;
+ default: Error(122); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 75 || t.kind == 76) {
+ while (t.kind == 35 || t.kind == 76 || t.kind == 77) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1407,23 +1443,23 @@ List<Expression!>! decreases) {
static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 73) {
+ if (t.kind == 74) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 74) {
+ } else if (t.kind == 75) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(121);
+ } else Error(123);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 74) {
+ if (t.kind == 75) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 77 || t.kind == 78) {
+ } else if (t.kind == 78 || t.kind == 79) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1432,7 +1468,7 @@ List<Expression!>! decreases) {
SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(122);
+ } else Error(124);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
@@ -1440,21 +1476,21 @@ List<Expression!>! decreases) {
if (t.kind == 35) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 75) {
+ } else if (t.kind == 76) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 76) {
+ } else if (t.kind == 77) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(123);
+ } else Error(125);
}
static void NegOp() {
- if (t.kind == 77) {
+ if (t.kind == 78) {
Get();
- } else if (t.kind == 78) {
+ } else if (t.kind == 79) {
Get();
- } else Error(124);
+ } else Error(126);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1462,17 +1498,17 @@ List<Expression!>! decreases) {
e = dummyExpr;
switch (t.kind) {
- case 79: {
+ case 80: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 80: {
+ case 81: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 81: {
+ case 82: {
Get();
e = new LiteralExpr(token);
break;
@@ -1482,11 +1518,11 @@ List<Expression!>! decreases) {
e = new LiteralExpr(token, n);
break;
}
- case 82: {
+ case 83: {
Get();
x = token;
Ident(out dtName);
- Expect(83);
+ Expect(84);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1499,7 +1535,7 @@ List<Expression!>! decreases) {
e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 84: {
+ case 85: {
Get();
x = token;
Expect(26);
@@ -1526,17 +1562,17 @@ List<Expression!>! decreases) {
Expect(7);
break;
}
- case 85: {
+ case 86: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(86);
+ Expect(87);
break;
}
- default: Error(125); break;
+ default: Error(127); break;
}
}
@@ -1575,10 +1611,10 @@ List<Expression!>! decreases) {
static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 88) {
+ if (t.kind == 89) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 89) {
+ } else if (t.kind == 90) {
Get();
x = token;
Expect(26);
@@ -1591,9 +1627,9 @@ List<Expression!>! decreases) {
QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(126);
+ } else Error(128);
Expect(27);
- } else Error(127);
+ } else Error(129);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1601,7 +1637,7 @@ List<Expression!>! decreases) {
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 83) {
+ if (t.kind == 84) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1614,14 +1650,14 @@ List<Expression!>! decreases) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 85) {
+ } else if (t.kind == 86) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 42 || t.kind == 87) {
- if (t.kind == 87) {
+ if (t.kind == 42 || t.kind == 88) {
+ if (t.kind == 88) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1634,11 +1670,11 @@ List<Expression!>! decreases) {
e1 = ee;
}
}
- } else if (t.kind == 87) {
+ } else if (t.kind == 88) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(128);
+ } else Error(130);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1651,8 +1687,8 @@ List<Expression!>! decreases) {
e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(86);
- } else Error(129);
+ Expect(87);
+ } else Error(131);
}
static void QuantifierGuts(out Expression! q) {
@@ -1665,13 +1701,13 @@ List<Expression!>! decreases) {
Triggers trigs = null;
Expression! body;
- if (t.kind == 90 || t.kind == 91) {
+ if (t.kind == 91 || t.kind == 92) {
Forall();
x = token; univ = true;
- } else if (t.kind == 92 || t.kind == 93) {
+ } else if (t.kind == 93 || t.kind == 94) {
Exists();
x = token;
- } else Error(130);
+ } else Error(132);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1695,19 +1731,19 @@ List<Expression!>! decreases) {
}
static void Forall() {
- if (t.kind == 90) {
+ if (t.kind == 91) {
Get();
- } else if (t.kind == 91) {
+ } else if (t.kind == 92) {
Get();
- } else Error(131);
+ } else Error(133);
}
static void Exists() {
- if (t.kind == 92) {
+ if (t.kind == 93) {
Get();
- } else if (t.kind == 93) {
+ } else if (t.kind == 94) {
Get();
- } else Error(132);
+ } else Error(134);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1720,16 +1756,16 @@ List<Expression!>! decreases) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(133);
+ } else Error(135);
Expect(7);
}
static void QSep() {
- if (t.kind == 94) {
+ if (t.kind == 95) {
Get();
- } else if (t.kind == 95) {
+ } else if (t.kind == 96) {
Get();
- } else Error(134);
+ } else Error(136);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1752,17 +1788,6 @@ List<Expression!>! decreases) {
attrs = new Attributes(aName, aArgs, attrs);
}
- static void AttributeArg(out Attributes.Argument! arg) {
- Expression! e; arg = dummyAttrArg;
- if (t.kind == 3) {
- Get();
- arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
- } else if (StartOf(7)) {
- Expression(out e);
- arg = new Attributes.Argument(e);
- } else Error(135);
- }
-
public static void Parse() {
@@ -1834,87 +1859,88 @@ List<Expression!>! decreases) {
case 52: s = "| expected"; break;
case 53: s = "assert expected"; break;
case 54: s = "assume expected"; break;
- case 55: s = "then expected"; break;
- case 56: s = "<==> expected"; break;
- case 57: s = "\\u21d4 expected"; break;
- case 58: s = "==> expected"; break;
- case 59: s = "\\u21d2 expected"; break;
- case 60: s = "&& expected"; break;
- case 61: s = "\\u2227 expected"; break;
- case 62: s = "|| expected"; break;
- case 63: s = "\\u2228 expected"; break;
- case 64: s = "== 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 = "!in expected"; break;
- case 70: s = "\\u2260 expected"; break;
- case 71: s = "\\u2264 expected"; break;
- case 72: s = "\\u2265 expected"; break;
- case 73: s = "+ expected"; break;
- case 74: s = "- expected"; break;
- case 75: s = "/ expected"; break;
- case 76: s = "% expected"; break;
- case 77: s = "! expected"; break;
- case 78: s = "\\u00ac expected"; break;
- case 79: s = "false expected"; break;
- case 80: s = "true expected"; break;
- case 81: s = "null expected"; break;
- case 82: s = "# expected"; break;
- case 83: s = ". expected"; break;
- case 84: s = "fresh expected"; break;
- case 85: s = "[ expected"; break;
- case 86: s = "] expected"; break;
- case 87: s = ".. expected"; break;
- case 88: s = "this expected"; break;
- case 89: s = "old expected"; break;
- case 90: s = "forall expected"; break;
- case 91: s = "\\u2200 expected"; break;
- case 92: s = "exists expected"; break;
- case 93: s = "\\u2203 expected"; break;
- case 94: s = ":: expected"; break;
- case 95: s = "\\u2022 expected"; break;
- case 96: s = "??? expected"; break;
- case 97: s = "invalid ClassMemberDecl"; break;
- case 98: s = "invalid FunctionDecl"; break;
- case 99: s = "invalid MethodDecl"; break;
- case 100: s = "invalid TypeAndToken"; break;
- case 101: s = "invalid MethodSpec"; break;
+ case 55: s = "print expected"; break;
+ case 56: s = "then expected"; break;
+ case 57: s = "<==> expected"; break;
+ case 58: s = "\\u21d4 expected"; break;
+ case 59: s = "==> expected"; break;
+ case 60: s = "\\u21d2 expected"; break;
+ case 61: s = "&& expected"; break;
+ case 62: s = "\\u2227 expected"; break;
+ case 63: s = "|| expected"; break;
+ case 64: s = "\\u2228 expected"; break;
+ case 65: s = "== expected"; break;
+ case 66: s = "<= expected"; break;
+ case 67: s = ">= expected"; break;
+ case 68: s = "!= expected"; break;
+ case 69: s = "!! expected"; break;
+ case 70: s = "!in expected"; break;
+ case 71: s = "\\u2260 expected"; break;
+ case 72: s = "\\u2264 expected"; break;
+ case 73: s = "\\u2265 expected"; break;
+ case 74: s = "+ expected"; break;
+ case 75: s = "- expected"; break;
+ case 76: s = "/ expected"; break;
+ case 77: s = "% expected"; break;
+ case 78: s = "! expected"; break;
+ case 79: s = "\\u00ac expected"; break;
+ case 80: s = "false expected"; break;
+ case 81: s = "true expected"; break;
+ case 82: s = "null expected"; break;
+ case 83: s = "# expected"; break;
+ case 84: s = ". expected"; break;
+ case 85: s = "fresh expected"; break;
+ case 86: s = "[ expected"; break;
+ case 87: s = "] expected"; break;
+ case 88: s = ".. expected"; break;
+ case 89: s = "this expected"; break;
+ case 90: s = "old expected"; break;
+ case 91: s = "forall expected"; break;
+ case 92: s = "\\u2200 expected"; break;
+ case 93: s = "exists expected"; break;
+ case 94: s = "\\u2203 expected"; break;
+ case 95: s = ":: expected"; break;
+ case 96: s = "\\u2022 expected"; break;
+ case 97: s = "??? expected"; break;
+ case 98: s = "invalid ClassMemberDecl"; break;
+ case 99: s = "invalid FunctionDecl"; break;
+ case 100: s = "invalid MethodDecl"; break;
+ case 101: s = "invalid TypeAndToken"; break;
case 102: s = "invalid MethodSpec"; break;
- case 103: s = "invalid Expression"; break;
- case 104: s = "invalid ReferenceType"; break;
- case 105: s = "invalid FunctionSpec"; break;
- case 106: s = "invalid FunctionBody"; break;
- case 107: s = "invalid PossiblyWildExpression"; break;
- case 108: s = "invalid Stmt"; break;
- case 109: s = "invalid OneStmt"; break;
- case 110: s = "invalid IfStmt"; break;
- case 111: s = "invalid ForeachStmt"; break;
- case 112: s = "invalid AssignRhs"; break;
- case 113: s = "invalid SelectExpression"; break;
- case 114: s = "invalid Guard"; break;
- case 115: s = "invalid CallStmtSubExpr"; break;
- case 116: s = "invalid EquivOp"; break;
- case 117: s = "invalid ImpliesOp"; break;
- case 118: s = "invalid AndOp"; break;
- case 119: s = "invalid OrOp"; break;
- case 120: s = "invalid RelOp"; break;
- case 121: s = "invalid AddOp"; break;
- case 122: s = "invalid UnaryExpression"; break;
- case 123: s = "invalid MulOp"; break;
- case 124: s = "invalid NegOp"; break;
- case 125: s = "invalid ConstAtomExpression"; break;
- case 126: s = "invalid ObjectExpression"; break;
- case 127: s = "invalid ObjectExpression"; break;
- case 128: s = "invalid SelectOrCallSuffix"; break;
- case 129: s = "invalid SelectOrCallSuffix"; break;
- case 130: s = "invalid QuantifierGuts"; break;
- case 131: s = "invalid Forall"; break;
- case 132: s = "invalid Exists"; break;
- case 133: s = "invalid AttributeOrTrigger"; break;
- case 134: s = "invalid QSep"; break;
- case 135: s = "invalid AttributeArg"; break;
+ case 103: s = "invalid MethodSpec"; break;
+ case 104: s = "invalid Expression"; break;
+ case 105: s = "invalid ReferenceType"; break;
+ case 106: s = "invalid FunctionSpec"; break;
+ case 107: s = "invalid FunctionBody"; break;
+ case 108: s = "invalid PossiblyWildExpression"; break;
+ case 109: s = "invalid Stmt"; break;
+ case 110: s = "invalid OneStmt"; break;
+ case 111: s = "invalid IfStmt"; break;
+ case 112: s = "invalid ForeachStmt"; break;
+ case 113: s = "invalid AssignRhs"; break;
+ case 114: s = "invalid SelectExpression"; break;
+ case 115: s = "invalid Guard"; break;
+ case 116: s = "invalid CallStmtSubExpr"; break;
+ case 117: s = "invalid AttributeArg"; break;
+ case 118: s = "invalid EquivOp"; break;
+ case 119: s = "invalid ImpliesOp"; break;
+ case 120: s = "invalid AndOp"; break;
+ case 121: s = "invalid OrOp"; break;
+ case 122: s = "invalid RelOp"; break;
+ case 123: s = "invalid AddOp"; break;
+ case 124: s = "invalid UnaryExpression"; break;
+ case 125: s = "invalid MulOp"; break;
+ case 126: s = "invalid NegOp"; break;
+ case 127: s = "invalid ConstAtomExpression"; break;
+ case 128: s = "invalid ObjectExpression"; break;
+ case 129: s = "invalid ObjectExpression"; break;
+ case 130: s = "invalid SelectOrCallSuffix"; break;
+ case 131: s = "invalid SelectOrCallSuffix"; break;
+ case 132: s = "invalid QuantifierGuts"; break;
+ case 133: s = "invalid Forall"; break;
+ case 134: s = "invalid Exists"; break;
+ case 135: s = "invalid AttributeOrTrigger"; break;
+ case 136: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1922,24 +1948,24 @@ List<Expression!>! decreases) {
}
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, x,x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, 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, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, 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, 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,T, x,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,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,T,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,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, 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,T,T,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,T,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,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,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,T, x,x,x,x, x,x,x,x, x,T,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,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T, x,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},
- {x,x,T,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, 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,T, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,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,x, x,T,T,T, T,T,T,x, T,T,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},
+ {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, 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, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, 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, 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,T, x,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,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,T,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,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,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,T,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, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,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,T, x,x,x,x, x,x,x,x, x,T,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, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T, x,x,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},
+ {x,x,T,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, 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, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,T,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, x,x,T,T, T,T,T,T, x,T,T,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 6f3629d6..1779f46b 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -143,21 +143,25 @@ namespace Microsoft.Dafny {
PrintAttributes(a.Prev);
wr.Write("{ :{0}", a.Name);
- string prefix = " ";
- foreach (Attributes.Argument arg in a.Args) {
- wr.Write(prefix);
- prefix = ", ";
- if (arg.S != null) {
- wr.Write("\"{0}\"", arg.S);
- } else {
- assert arg.E != null;
- PrintExpression(arg.E);
- }
- }
+ PrintAttributeArgs(a.Args);
wr.Write(" } ");
}
}
+ public void PrintAttributeArgs(List<Attributes.Argument!>! args) {
+ string prefix = " ";
+ foreach (Attributes.Argument arg in args) {
+ wr.Write(prefix);
+ prefix = ", ";
+ if (arg.S != null) {
+ wr.Write("\"{0}\"", arg.S);
+ } else {
+ assert arg.E != null;
+ PrintExpression(arg.E);
+ }
+ }
+ }
+
public void PrintField(Field! field, int indent) {
Indent(indent);
if (field.IsGhost) {
@@ -333,6 +337,12 @@ namespace Microsoft.Dafny {
PrintExpression(((UseStmt)stmt).Expr);
wr.Write(";");
+ } else if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ wr.Write("print");
+ PrintAttributeArgs(s.Args);
+ wr.Write(";");
+
} else if (stmt is LabelStmt) {
wr.Write("label {0}:", ((LabelStmt)stmt).Label);
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 430714d3..db6e667a 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -303,7 +303,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// Check that the datatype has some constructor all whose argument types go to a lower stratum, which means
/// go to a different SCC or to a type in 'goodOnes'.
- /// Returns 'true' if that is the case.
+ /// Returns 'true' and sets dt.DefaultCtor if that is the case.
/// </summary>
bool StratosphereCheck(DatatypeDecl! dt, Graph<DatatypeDecl!>! dependencies, List<DatatypeDecl!>! goodOnes) {
// Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
@@ -324,6 +324,7 @@ namespace Microsoft.Dafny {
}
}
// this constructor satisfies the requirements, so the datatype is allowed
+ dt.DefaultCtor = ctor;
return true;
NEXT_OUTER_ITERATION: {}
}
@@ -334,10 +335,14 @@ namespace Microsoft.Dafny {
void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
- foreach (Attributes.Argument aa in attrs.Args) {
- if (aa.E != null) {
- ResolveExpression(aa.E, twoState, true);
- }
+ ResolveAttributeArgs(attrs.Args, twoState, true);
+ }
+ }
+
+ void ResolveAttributeArgs(List<Attributes.Argument!>! args, bool twoState, bool specContext) {
+ foreach (Attributes.Argument aa in args) {
+ if (aa.E != null) {
+ ResolveExpression(aa.E, twoState, specContext);
}
}
}
@@ -792,6 +797,7 @@ namespace Microsoft.Dafny {
{
if (stmt is UseStmt) {
UseStmt s = (UseStmt)stmt;
+ s.IsGhost = true;
ResolveExpression(s.Expr, true, true);
assert s.Expr.Type != null; // follows from postcondition of ResolveExpression
Expression expr = s.Expr;
@@ -808,12 +814,17 @@ namespace Microsoft.Dafny {
}
} else if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
+ s.IsGhost = true;
ResolveExpression(s.Expr, true, true);
assert s.Expr.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
}
-
+
+ } else if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ ResolveAttributeArgs(s.Args, false, false);
+
} else if (stmt is BreakStmt) {
BreakStmt s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
@@ -852,15 +863,17 @@ namespace Microsoft.Dafny {
Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable");
} else {
FieldSelectExpr fse = (FieldSelectExpr)s.Lhs;
- lvalueIsGhost = ((!)fse.Field).IsGhost;
- if (!lvalueIsGhost) {
- if (specContextOnly) {
- Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
- } else {
- // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
- // the next best thing.
- if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
- Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
+ if (fse.Field != null) { // otherwise, an error was reported above
+ lvalueIsGhost = fse.Field.IsGhost;
+ if (!lvalueIsGhost) {
+ if (specContextOnly) {
+ Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ } else {
+ // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
+ // the next best thing.
+ if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
+ Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
+ }
}
}
}
@@ -869,6 +882,7 @@ namespace Microsoft.Dafny {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
+ s.IsGhost = lvalueIsGhost;
if (s.Rhs is ExprRhs) {
ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, true, lvalueIsGhost);
@@ -941,6 +955,7 @@ namespace Microsoft.Dafny {
} else {
callee = (Method)member;
s.Method = callee;
+ s.IsGhost = callee.IsGhost;
if (specContextOnly && !callee.IsGhost) {
Error(s, "only ghost methods can be called from this context");
}
@@ -1062,6 +1077,7 @@ namespace Microsoft.Dafny {
branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
}
}
+ s.IsGhost = branchesAreSpecOnly;
ResolveStatement(s.Thn, branchesAreSpecOnly, method);
if (s.Els != null) {
ResolveStatement(s.Els, branchesAreSpecOnly, method);
@@ -1093,6 +1109,7 @@ namespace Microsoft.Dafny {
ResolveExpression(e, true, true);
// any type is fine
}
+ s.IsGhost = bodyIsSpecOnly;
ResolveStatement(s.Body, bodyIsSpecOnly, method);
} else if (stmt is ForeachStmt) {
@@ -1123,6 +1140,7 @@ namespace Microsoft.Dafny {
bool specOnly = specContextOnly ||
(successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
+ s.IsGhost = specOnly;
ResolveStatement(s.BodyAssign, specOnly, method);
// check for correct usage of BoundVar in LHS and RHS of this assignment
FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
@@ -1166,6 +1184,7 @@ namespace Microsoft.Dafny {
subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
}
+ s.IsGhost = bodyIsSpecOnly;
Dictionary<string!,object> memberNamesUsed = new Dictionary<string!,object>(); // this is really a set
foreach (MatchCaseStmt mc in s.Cases) {
@@ -1201,10 +1220,12 @@ namespace Microsoft.Dafny {
}
ResolveType(v.Type);
if (ctor != null && i < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[i].Type, subst);
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(v.Type, st)) {
Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
+ v.IsGhost = formal.IsGhost;
}
i++;
}
@@ -1378,6 +1399,7 @@ namespace Microsoft.Dafny {
for (int i = 0; i < dt.TypeArgs.Count; i++) {
Type t = new InferredTypeProxy();
gt.Add(t);
+ dtv.InferredTypeArgs.Add(t);
subst.Add(dt.TypeArgs[i], t);
}
expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
@@ -1394,15 +1416,18 @@ namespace Microsoft.Dafny {
}
// add the constructor's own type parameters to the substitution map
foreach (TypeParameter p in ctor.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ Type t = new ParamTypeProxy(p);
+ dtv.InferredTypeArgs.Add(t);
+ subst.Add(p, t);
}
}
int j = 0;
foreach (Expression arg in dtv.Arguments) {
- ResolveExpression(arg, twoState, specContext);
+ Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;
+ ResolveExpression(arg, twoState, specContext || (formal != null && formal.IsGhost));
assert arg.Type != null; // follows from postcondition of ResolveExpression
- if (ctor != null && j < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[j].Type, subst);
+ if (formal != null) {
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(arg.Type, st)) {
Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
}
@@ -1841,10 +1866,12 @@ namespace Microsoft.Dafny {
}
ResolveType(v.Type);
if (ctor != null && i < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[i].Type, subst);
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(v.Type, st)) {
Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
+ v.IsGhost = formal.IsGhost;
}
i++;
}
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc
index 8c7a1b15..7e954005 100644
--- a/Source/Dafny/Scanner.ssc
+++ b/Source/Dafny/Scanner.ssc
@@ -133,7 +133,7 @@ public class Scanner {
start[8804] = 38;
start[8805] = 39;
}
- const int noSym = 96;
+ const int noSym = 97;
static short[] start = new short[16385];
@@ -313,15 +313,16 @@ public class Scanner {
case "in": t.kind = 51; break;
case "assert": t.kind = 53; break;
case "assume": t.kind = 54; break;
- case "then": t.kind = 55; break;
- case "false": t.kind = 79; break;
- case "true": t.kind = 80; break;
- case "null": t.kind = 81; break;
- case "fresh": t.kind = 84; break;
- case "this": t.kind = 88; break;
- case "old": t.kind = 89; break;
- case "forall": t.kind = 90; break;
- case "exists": t.kind = 92; break;
+ case "print": t.kind = 55; break;
+ case "then": t.kind = 56; break;
+ case "false": t.kind = 80; break;
+ case "true": t.kind = 81; break;
+ case "null": t.kind = 82; break;
+ case "fresh": t.kind = 85; break;
+ case "this": t.kind = 89; break;
+ case "old": t.kind = 90; break;
+ case "forall": t.kind = 91; break;
+ case "exists": t.kind = 93; break;
default: break;
}
@@ -387,83 +388,83 @@ public class Scanner {
else {t.kind = 52; goto done;}
case 19:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 65; goto done;}
+ else {t.kind = 66; goto done;}
case 20:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
else {t.kind = noSym; goto done;}
case 21:
- {t.kind = 56; goto done;}
- case 22:
{t.kind = 57; goto done;}
+ case 22:
+ {t.kind = 58; goto done;}
case 23:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 64; goto done;}
+ else {t.kind = 65; goto done;}
case 24:
- {t.kind = 58; goto done;}
- case 25:
{t.kind = 59; goto done;}
+ case 25:
+ {t.kind = 60; goto done;}
case 26:
if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
else {t.kind = noSym; goto done;}
case 27:
- {t.kind = 60; goto done;}
- case 28:
{t.kind = 61; goto done;}
- case 29:
+ case 28:
{t.kind = 62; goto done;}
- case 30:
+ case 29:
{t.kind = 63; goto done;}
+ case 30:
+ {t.kind = 64; goto done;}
case 31:
- {t.kind = 66; goto done;}
+ {t.kind = 67; goto done;}
case 32:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 77; goto done;}
+ else {t.kind = 78; goto done;}
case 33:
- {t.kind = 67; goto done;}
- case 34:
{t.kind = 68; goto done;}
+ case 34:
+ {t.kind = 69; goto done;}
case 35:
if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
else {t.kind = noSym; goto done;}
case 36:
- {t.kind = 69; goto done;}
- case 37:
{t.kind = 70; goto done;}
- case 38:
+ case 37:
{t.kind = 71; goto done;}
- case 39:
+ case 38:
{t.kind = 72; goto done;}
- case 40:
+ case 39:
{t.kind = 73; goto done;}
- case 41:
+ case 40:
{t.kind = 74; goto done;}
- case 42:
+ case 41:
{t.kind = 75; goto done;}
- case 43:
+ case 42:
{t.kind = 76; goto done;}
+ case 43:
+ {t.kind = 77; goto done;}
case 44:
- {t.kind = 78; goto done;}
+ {t.kind = 79; goto done;}
case 45:
- {t.kind = 82; goto done;}
+ {t.kind = 83; goto done;}
case 46:
if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 83; goto done;}
+ else {t.kind = 84; goto done;}
case 47:
- {t.kind = 85; goto done;}
- case 48:
{t.kind = 86; goto done;}
- case 49:
+ case 48:
{t.kind = 87; goto done;}
+ case 49:
+ {t.kind = 88; goto done;}
case 50:
- {t.kind = 91; goto done;}
+ {t.kind = 92; goto done;}
case 51:
- {t.kind = 93; goto done;}
- case 52:
{t.kind = 94; goto done;}
- case 53:
+ case 52:
{t.kind = 95; goto done;}
+ case 53:
+ {t.kind = 96; goto done;}
case 54: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 58350c24..763ed8c9 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1797,6 +1797,15 @@ namespace Microsoft.Dafny {
// Skip the totality check. This makes the 'use' statement easier to use and it has no executable analog anyhow
// builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined")); // totality check
builder.Add(new Bpl.AssumeCmd(stmt.Tok, (s.EvalInOld ? etran.Old : etran).TrUseExpr(s.FunctionCallExpr)));
+ } else if (stmt is PrintStmt) {
+ AddComment(builder, stmt, "print statement");
+ PrintStmt s = (PrintStmt)stmt;
+ foreach (Attributes.Argument arg in s.Args) {
+ if (arg.E != null) {
+ builder.Add(AssertNS(stmt.Tok, IsTotal(arg.E, etran), "print expression must be well defined")); // totality check
+ }
+ }
+
} else if (stmt is LabelStmt) {
AddComment(builder, stmt, "label statement"); // TODO: ouch, comments probably mess up what the label labels in the Boogie program
builder.AddLabelCmd(((LabelStmt)stmt).Label);
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 22:53:41 +0000