From a2f70f46e1a4dfb513df45657178399269cec67d Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 6 May 2010 20:28:29 +0000 Subject: Dafny: * First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies) * Added "print" statement (to make running compiled programs more interesting) * Changed name of default class from $default to _default Boogie: * Included "lambda" as a keyword in emacs and latex style files --- Source/Dafny/Compiler.ssc | 1051 ++++++++++++++++++++++++++++++++++++ Source/Dafny/Dafny.atg | 28 +- Source/Dafny/DafnyAst.ssc | 34 +- Source/Dafny/DafnyPipeline.sscproj | 4 + Source/Dafny/Parser.ssc | 464 ++++++++-------- Source/Dafny/Printer.ssc | 32 +- Source/Dafny/Resolver.ssc | 69 ++- Source/Dafny/Scanner.ssc | 85 +-- Source/Dafny/Translator.ssc | 9 + 9 files changed, 1466 insertions(+), 310 deletions(-) create mode 100644 Source/Dafny/Compiler.ssc (limited to 'Source/Dafny') 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 : Base_Dt { + // 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 { + // Base_Dt d; + // public Base_Dt D { + // get { if (d == null) { d = Default; } return d; } + // } + // public Dt(Base_Dt d) { this.d = d; } + // public static Base_Dt Default { + // get { return ...; } + // } + // public override bool Equals(object other) { + // return other is Dt && D.Equals(((Dt)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! 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 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 is not supported; consider introducing a ghost"); + } + return DafnySeqClass + "<" + TypeName(argType) + ">"; + } else { + assert false; // unexpected type + } + } + + string! TypeNames(List! types) { + string s = ""; + string sep = ""; + foreach (Type t in types) { + s += sep + TypeName(t); + sep = ","; + } + return s; + } + + string! TypeParameters(List! 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> pendingUpdates = new List>(); + // foreach (TType x in S) { + // if (Range(x)) { + // assert/assume ...; + // pendingUpdates.Add(new Pair(x,RHS)); + // } + // } + // foreach (Pair 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> {2} = new List>();", 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! stmts, int indent) { + List currentLabels = null; + foreach (Statement ss in stmts) { + if (ss is LabelStmt) { + LabelStmt s = (LabelStmt)ss; + if (currentLabels == null) { + currentLabels = new List(); + } + currentLabels.Add(s.Label); + } else { + TrStmt(ss, indent + IndentAmount); + SpillLabels(currentLabels, indent); + currentLabels = null; + } + } + SpillLabels(currentLabels, indent); + } + + void SpillLabels(List 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! 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! 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 (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .) . -TypeIdentOptional -= (. string name = null; .) +TypeIdentOptional += (. string name = null; isGhost = false; .) + [ "ghost" (. isGhost = true; .) + ] TypeAndToken [ ":" (. /* try to convert ty to an identifier */ @@ -297,7 +299,7 @@ MethodDecl List mod = new List(); List ens = new List(); List dec = new List(); - 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 ] ( ";" { MethodSpec } - | { MethodSpec } BlockStmt (. body = bb; .) + | { MethodSpec } BlockStmt (. body = (BlockStmt)bb; .) ) (. parseVarScope.PopMarker(); @@ -349,11 +351,11 @@ Formals! formals> . FormalsOptionalIds! formals> -= (. Token! id; Type! ty; string! name; .) += (. Token! id; Type! ty; string! name; bool isGhost; .) "(" [ - TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .) - { "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .) + TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .) + { "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .) } ] ")" @@ -549,6 +551,7 @@ OneStmt ( AssertStmt | AssumeStmt | UseStmt + | PrintStmt | AssignStmt | HavocStmt | CallStmt @@ -828,6 +831,17 @@ UseStmt Expression ";" (. s = new UseStmt(x, e); .) . +PrintStmt += (. Token! x; Attributes.Argument! arg; + List args = new List(); + .) + "print" (. x = token; .) + AttributeArg (. args.Add(arg); .) + { "," AttributeArg (. args.Add(arg); .) + } + ";" (. s = new PrintStmt(x, args); .) + . + /*------------------------------------------------------------------------*/ Expression = (. 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(), null); + base(Token.NoToken, "_default", new List(), 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! members) { - base(Token.NoToken, "$default", module, new List(), members, null); + base(Token.NoToken, "_default", module, new List(), members, null); } public override bool IsDefaultClass { get { return true; } @@ -394,6 +394,7 @@ namespace Microsoft.Dafny public class DatatypeDecl : TopLevelDecl { public readonly List! Ctors; + public DatatypeCtor DefaultCtor; // set during resolution public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List! typeArgs, [Captured] List! 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! Mod; public readonly List! Ens; public readonly List! 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! ins, [Captured] List! outs, [Captured] List! req, [Captured] List! mod, [Captured] List! ens, [Captured] List! 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! Args; + public PrintStmt(Token! tok, List! 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. /// public void MakeGhost() { - isGhost = true; + base.IsGhost = true; } } @@ -968,6 +981,7 @@ namespace Microsoft.Dafny public readonly string! MemberName; public readonly List! Arguments; public DatatypeCtor Ctor; // filled in by resolution + public List! InferredTypeArgs = new List(); // filled in by resolution public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List! 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" /> + 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! modules) { } else if (t.kind == 19) { MethodDecl(mmod, out m); mm.Add(m); - } else Error(97); + } else Error(98); } static void GenericParameters(List! typeArgs) { @@ -363,7 +363,7 @@ public static int Parse (List! 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! modules) { List mod = new List(); List ens = new List(); List dec = new List(); - 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! 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! modules) { } static void FormalsOptionalIds(List! 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! 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! 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! formals) { @@ -585,12 +589,12 @@ List! 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! 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! args) { @@ -665,7 +669,7 @@ List! decreases) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else Error(104); + } else Error(105); } static void FunctionSpec(List! reqs, List! reads, List! decreases) { @@ -685,7 +689,7 @@ List! decreases) { Get(); Expressions(decreases); Expect(13); - } else Error(105); + } else Error(106); } static void FunctionBody(out Expression! e) { @@ -695,7 +699,7 @@ List! decreases) { MatchExpression(out e); } else if (StartOf(7)) { Expression(out e); - } else Error(106); + } else Error(107); Expect(7); } @@ -717,7 +721,7 @@ List! 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! 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! 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! decreases) { s = new ReturnStmt(x); break; } - default: Error(109); break; + default: Error(110); break; } } @@ -894,6 +902,23 @@ List! decreases) { s = new UseStmt(x, e); } + static void PrintStmt(out Statement! s) { + Token! x; Attributes.Argument! arg; + List args = new List(); + + 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! 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! 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! 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! 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! decreases) { } else if (StartOf(7)) { Expression(out ee); e = ee; - } else Error(114); + } else Error(115); Expect(27); } @@ -1215,19 +1240,30 @@ List! 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! 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! 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! 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! 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! 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! 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! 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! 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! 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! 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! 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! 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! 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(); if (t.kind == 26) { @@ -1499,7 +1535,7 @@ List! 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! decreases) { Expect(7); break; } - case 85: { + case 86: { Get(); x = token; elements = new List(); 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! 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! 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! 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! 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! 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! 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! 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! 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! decreases) { es = new List(); 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! 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! 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! 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! 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 { /// /// 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. /// bool StratosphereCheck(DatatypeDecl! dt, Graph! dependencies, List! 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! 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 memberNamesUsed = new Dictionary(); // 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); -- cgit v1.2.3