diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 504 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 9 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/DafnyPipeline.csproj | 1 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 10 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 830 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 322 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 52 |
10 files changed, 874 insertions, 883 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs new file mode 100644 index 00000000..3db69fba --- /dev/null +++ b/Source/Dafny/Cloner.cs @@ -0,0 +1,504 @@ +
+using System;
+using System.Collections.Generic;
+using System.Numerics;
+using System.Diagnostics.Contracts;
+using IToken = Microsoft.Boogie.IToken;
+
+namespace Microsoft.Dafny
+{
+ class Cloner
+ {
+ public ModuleDefinition CloneModuleDefinition(ModuleDefinition m, string name) {
+ ModuleDefinition nw;
+ if (m is DefaultModuleDecl) {
+ nw = new DefaultModuleDecl();
+ } else {
+ nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, null, true);
+ }
+ foreach (var d in m.TopLevelDecls) {
+ nw.TopLevelDecls.Add(CloneDeclaration(d, nw));
+ }
+ nw.RefinementBase = m.RefinementBase;
+ nw.Height = m.Height;
+ return nw;
+ }
+ public TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
+ Contract.Requires(d != null);
+ Contract.Requires(m != null);
+
+ if (d is ArbitraryTypeDecl) {
+ var dd = (ArbitraryTypeDecl)d;
+ return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);
+ } else if (d is IndDatatypeDecl) {
+ var dd = (IndDatatypeDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ return dt;
+ } else if (d is CoDatatypeDecl) {
+ var dd = (CoDatatypeDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ return dt;
+ } else if (d is ClassDecl) {
+ if (d is DefaultClassDecl) {
+ var dd = (ClassDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new DefaultClassDecl(m, mm);
+ return cl;
+ } else {
+ var dd = (ClassDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
+ return cl;
+ }
+ } else if (d is ModuleDecl) {
+ if (d is LiteralModuleDecl) {
+ var l = new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
+ l.Signature = ((ModuleDecl)d).Signature;
+ return l;
+ } else if (d is AliasModuleDecl) {
+ var a = (AliasModuleDecl)d;
+ var alias = new AliasModuleDecl(a.Path, a.tok, m);
+ alias.ModuleReference = a.ModuleReference;
+ alias.Signature = a.Signature;
+ return alias;
+ } else if (d is AbstractModuleDecl) {
+ var a = (AbstractModuleDecl)d;
+ var abs = new AbstractModuleDecl(a.Path, a.tok, m, a.CompilePath);
+ abs.Signature = a.Signature;
+ abs.OriginalSignature = a.OriginalSignature;
+ return abs;
+ } else {
+ Contract.Assert(false); // unexpected declaration
+ return null; // to please compiler
+ }
+ } else {
+ Contract.Assert(false); // unexpected declaration
+ return null; // to please compiler
+ }
+ }
+
+ public DatatypeCtor CloneCtor(DatatypeCtor ct) {
+ return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
+ }
+
+ public TypeParameter CloneTypeParam(TypeParameter tp) {
+ return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);
+ }
+
+ public MemberDecl CloneMember(MemberDecl member) {
+ if (member is Field) {
+ var f = (Field)member;
+ return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
+ } else if (member is Function) {
+ var f = (Function)member;
+ return CloneFunction(f);
+ } else {
+ var m = (Method)member;
+ return CloneMethod(m);
+ }
+ }
+
+ public Type CloneType(Type t) {
+ if (t is BasicType) {
+ return t;
+ } else if (t is SetType) {
+ var tt = (SetType)t;
+ return new SetType(CloneType(tt.Arg));
+ } else if (t is SeqType) {
+ var tt = (SeqType)t;
+ return new SeqType(CloneType(tt.Arg));
+ } else if (t is MultiSetType) {
+ var tt = (MultiSetType)t;
+ return new MultiSetType(CloneType(tt.Arg));
+ } else if (t is MapType) {
+ var tt = (MapType)t;
+ return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
+ } else if (t is UserDefinedType) {
+ var tt = (UserDefinedType)t;
+ return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => Tok(x)));
+ } else if (t is InferredTypeProxy) {
+ return new InferredTypeProxy();
+ } else if (t is ParamTypeProxy) {
+ return new ParamTypeProxy(((ParamTypeProxy)t).orig); // todo: this is not right, as when cloning the type parameter declartion changes.
+ } else {
+ Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
+ return null; // to please compiler
+ }
+ }
+
+ public Formal CloneFormal(Formal formal) {
+ return new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ }
+
+ public BoundVar CloneBoundVar(BoundVar bv) {
+ return new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
+ }
+
+ public Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
+ var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
+ return new Specification<Expression>(ee, null);
+ }
+
+ public Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
+ var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
+ return new Specification<FrameExpression>(ee, null);
+ }
+
+ public FrameExpression CloneFrameExpr(FrameExpression frame) {
+ return new FrameExpression(CloneExpr(frame.E), frame.FieldName);
+ }
+ public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {
+ if (aa.E != null) {
+ return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));
+ } else {
+ return new Attributes.Argument(Tok(aa.Tok), aa.S);
+ }
+ }
+
+ public MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
+ return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
+ }
+
+ public virtual Expression CloneExpr(Expression expr) {
+ if (expr == null) {
+ return null;
+ } else if (expr is LiteralExpr) {
+ var e = (LiteralExpr)expr;
+ if (e.Value == null) {
+ return new LiteralExpr(Tok(e.tok));
+ } else if (e.Value is bool) {
+ return new LiteralExpr(Tok(e.tok), (bool)e.Value);
+ } else {
+ return new LiteralExpr(Tok(e.tok), (BigInteger)e.Value);
+ }
+
+ } else if (expr is ThisExpr) {
+ if (expr is ImplicitThisExpr) {
+ return new ImplicitThisExpr(Tok(expr.tok));
+ } else {
+ return new ThisExpr(Tok(expr.tok));
+ }
+
+ } else if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ return new IdentifierExpr(Tok(e.tok), e.Name);
+
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ return new DatatypeValue(Tok(e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));
+
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ if (expr is SetDisplayExpr) {
+ return new SetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
+ } else if (expr is MultiSetDisplayExpr) {
+ return new MultiSetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
+ } else {
+ Contract.Assert(expr is SeqDisplayExpr);
+ return new SeqDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
+ }
+
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ List<ExpressionPair> pp = new List<ExpressionPair>();
+ foreach (ExpressionPair p in e.Elements) {
+ pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));
+ }
+ return new MapDisplayExpr(Tok(expr.tok), pp);
+ } else if (expr is ExprDotName) {
+ var e = (ExprDotName)expr;
+ return new ExprDotName(Tok(e.tok), CloneExpr(e.Obj), e.SuffixName);
+
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ return new FieldSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.FieldName);
+
+ } else if (expr is SeqSelectExpr) {
+ var e = (SeqSelectExpr)expr;
+ return new SeqSelectExpr(Tok(e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));
+
+ } else if (expr is MultiSelectExpr) {
+ var e = (MultiSelectExpr)expr;
+ return new MultiSelectExpr(Tok(e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));
+
+ } else if (expr is SeqUpdateExpr) {
+ var e = (SeqUpdateExpr)expr;
+ return new SeqUpdateExpr(Tok(e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));
+
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ return new FunctionCallExpr(Tok(e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : Tok(e.OpenParen), e.Args.ConvertAll(CloneExpr));
+
+ } else if (expr is OldExpr) {
+ var e = (OldExpr)expr;
+ return new OldExpr(Tok(e.tok), CloneExpr(e.E));
+
+ } else if (expr is MultiSetFormingExpr) {
+ var e = (MultiSetFormingExpr)expr;
+ return new MultiSetFormingExpr(Tok(e.tok), CloneExpr(e.E));
+
+ } else if (expr is FreshExpr) {
+ var e = (FreshExpr)expr;
+ return new FreshExpr(Tok(e.tok), CloneExpr(e.E));
+
+ } else if (expr is AllocatedExpr) {
+ var e = (AllocatedExpr)expr;
+ return new AllocatedExpr(Tok(e.tok), CloneExpr(e.E));
+
+ } else if (expr is UnaryExpr) {
+ var e = (UnaryExpr)expr;
+ return new UnaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E));
+
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ return new BinaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
+
+ } else if (expr is ChainingExpression) {
+ var e = (ChainingExpression)expr;
+ return CloneExpr(e.E); // just clone the desugaring, since it's already available
+
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));
+
+ } else if (expr is NamedExpr) {
+ var e = (NamedExpr)expr;
+ return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var tk = Tok(e.tok);
+ var bvs = e.BoundVars.ConvertAll(CloneBoundVar);
+ var range = CloneExpr(e.Range);
+ var term = CloneExpr(e.Term);
+ if (e is ForallExpr) {
+ return new ForallExpr(tk, bvs, range, term, null);
+ } else if (e is ExistsExpr) {
+ return new ExistsExpr(tk, bvs, range, term, null);
+ } else if (e is MapComprehension) {
+ return new MapComprehension(tk, bvs, range, term);
+ } else {
+ Contract.Assert(e is SetComprehension);
+ return new SetComprehension(tk, bvs, range, term);
+ }
+
+ } else if (expr is WildcardExpr) {
+ return new WildcardExpr(Tok(expr.tok));
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ if (e is AssertExpr) {
+ return new AssertExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
+ } else {
+ Contract.Assert(e is AssumeExpr);
+ return new AssumeExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
+ }
+
+ } else if (expr is ITEExpr) {
+ var e = (ITEExpr)expr;
+ return new ITEExpr(Tok(e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));
+
+ } else if (expr is ParensExpression) {
+ var e = (ParensExpression)expr;
+ return CloneExpr(e.E); // skip the parentheses in the clone
+
+ } else if (expr is IdentifierSequence) {
+ var e = (IdentifierSequence)expr;
+ var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);
+ return new IdentifierSequence(e.Tokens.ConvertAll(tk => Tok(tk)), e.OpenParen == null ? null : Tok(e.OpenParen), aa);
+
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),
+ e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
+ }
+
+ public AssignmentRhs CloneRHS(AssignmentRhs rhs) {
+ if (rhs is ExprRhs) {
+ var r = (ExprRhs)rhs;
+ return new ExprRhs(CloneExpr(r.Expr));
+ } else if (rhs is HavocRhs) {
+ return new HavocRhs(Tok(rhs.Tok));
+ } else {
+ var r = (TypeRhs)rhs;
+ if (r.ArrayDimensions != null) {
+ return new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));
+ } else if (r.InitCall != null) {
+ return new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));
+ } else {
+ return new TypeRhs(Tok(r.Tok), CloneType(r.EType));
+ }
+ }
+ }
+
+ public BlockStmt CloneBlockStmt(BlockStmt stmt) {
+ if (stmt == null) {
+ return null;
+ } else {
+ return new BlockStmt(Tok(stmt.Tok), stmt.Body.ConvertAll(CloneStmt));
+ }
+ }
+
+ public Statement CloneStmt(Statement stmt) {
+ if (stmt == null) {
+ return null;
+ }
+
+ Statement r;
+ if (stmt is AssertStmt) {
+ var s = (AssertStmt)stmt;
+ r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
+
+ } else if (stmt is AssumeStmt) {
+ var s = (AssumeStmt)stmt;
+ r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
+
+ } else if (stmt is PrintStmt) {
+ var s = (PrintStmt)stmt;
+ r = new PrintStmt(Tok(s.Tok), s.Args.ConvertAll(CloneAttrArg));
+
+ } else if (stmt is BreakStmt) {
+ var s = (BreakStmt)stmt;
+ if (s.TargetLabel != null) {
+ r = new BreakStmt(Tok(s.Tok), s.TargetLabel);
+ } else {
+ r = new BreakStmt(Tok(s.Tok), s.BreakCount);
+ }
+
+ } else if (stmt is ReturnStmt) {
+ var s = (ReturnStmt)stmt;
+ r = new ReturnStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));
+
+ } else if (stmt is AssignStmt) {
+ var s = (AssignStmt)stmt;
+ r = new AssignStmt(Tok(s.Tok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));
+
+ } else if (stmt is VarDecl) {
+ var s = (VarDecl)stmt;
+ r = new VarDecl(Tok(s.Tok), s.Name, CloneType(s.OptionalType), s.IsGhost);
+
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ r = new CallStmt(Tok(s.Tok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName, s.Args.ConvertAll(CloneExpr));
+
+ } else if (stmt is BlockStmt) {
+ r = CloneBlockStmt((BlockStmt)stmt);
+
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ r = new IfStmt(Tok(s.Tok), CloneExpr(s.Guard), CloneBlockStmt(s.Thn), CloneStmt(s.Els));
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ r = new AlternativeStmt(Tok(s.Tok), s.Alternatives.ConvertAll(CloneGuardedAlternative));
+
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ r = new WhileStmt(Tok(s.Tok), CloneExpr(s.Guard), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), CloneBlockStmt(s.Body));
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ r = new AlternativeLoopStmt(Tok(s.Tok), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), s.Alternatives.ConvertAll(CloneGuardedAlternative));
+
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
+
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source),
+ s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));
+
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));
+
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ r = new UpdateStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), s.Rhss.ConvertAll(CloneRHS), s.CanMutateKnownState);
+
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ r = new VarDeclStmt(Tok(s.Tok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (ConcreteUpdateStatement)CloneStmt(s.Update));
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
+ }
+
+ // add labels to the cloned statement
+ AddStmtLabels(r, stmt.Labels);
+
+ return r;
+ }
+
+ public void AddStmtLabels(Statement s, LList<Label> node) {
+ if (node != null) {
+ AddStmtLabels(s, node.Next);
+ if (node.Data.Name == null) {
+ // this indicates an implicit-target break statement that has been resolved; don't add it
+ } else {
+ s.Labels = new LList<Label>(new Label(Tok(node.Data.Tok), node.Data.Name), s.Labels);
+ }
+ }
+ }
+
+ public GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) {
+ return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt));
+ }
+
+ public Function CloneFunction(Function f) {
+
+ var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
+ var formals = f.Formals.ConvertAll(CloneFormal);
+ var req = f.Req.ConvertAll(CloneExpr);
+ var reads = f.Reads.ConvertAll(CloneFrameExpr);
+ var decreases = CloneSpecExpr(f.Decreases);
+ var ens = f.Ens.ConvertAll(CloneExpr);
+ var body = CloneExpr(f.Body);
+
+ if (f is Predicate) {
+ return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals,
+ req, reads, ens, decreases, body, false, null, false);
+ } else if (f is CoPredicate) {
+ return new CoPredicate(Tok(f.tok), f.Name, f.IsStatic, tps, f.OpenParen, formals,
+ req, reads, ens, body, null, false);
+ } else {
+ return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
+ req, reads, ens, decreases, body, null, false);
+ }
+ }
+
+ public Method CloneMethod(Method m) {
+ Contract.Requires(m != null);
+
+ var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
+ var ins = m.Ins.ConvertAll(CloneFormal);
+ var req = m.Req.ConvertAll(CloneMayBeFreeExpr);
+ var mod = CloneSpecFrameExpr(m.Mod);
+ var decreases = CloneSpecExpr(m.Decreases);
+
+ var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);
+
+ var body = CloneBlockStmt(m.Body);
+ if (m is Constructor) {
+ return new Constructor(Tok(m.tok), m.Name, tps, ins,
+ req, mod, ens, decreases, body, null, false);
+ } else {
+ return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ req, mod, ens, decreases, body, null, false);
+ }
+ }
+ public virtual IToken Tok(IToken tok) {
+ return tok;
+ }
+ }
+}
\ No newline at end of file diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 3864df8b..4544a01b 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny { ReadRuntimeSystem();
CompileBuiltIns(program.BuiltIns);
- foreach (ModuleDefinition m in program.Modules) {
+ foreach (ModuleDefinition m in program.CompileModules) {
if (m.IsGhost) {
// the purpose of a ghost module is to skip compilation
continue;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5efbd57b..52639f07 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -172,7 +172,7 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
Attributes attrs = null; IToken/*!*/ id;
List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
- List<IToken> idRefined = null, idPath = null;
+ List<IToken> idRefined = null, idPath = null, idAssignment = null;
bool isGhost = false;
ModuleDefinition module;
ModuleDecl sm;
@@ -202,7 +202,10 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl ) |
"=" QualifiedName<out idPath> ";" (. submodule = new AliasModuleDecl(idPath, id, parent); .)
|
- "as" QualifiedName<out idPath> ";" (.submodule = new AbstractModuleDecl(idPath, id, parent); .)
+ ( "as" QualifiedName<out idPath>
+ ["=" QualifiedName<out idAssignment> ]
+ ";" (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment); .)
+ )
)
.
@@ -700,7 +703,7 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe> )
.
FrameExpression<out FrameExpression/*!*/ fe>
-= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null; .)
(( Expression<out e>
[ "`" Ident<out id> (. fieldName = id.val; .)
]
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index e9a4ce4b..ae7e1a4c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -20,8 +20,11 @@ namespace Microsoft.Dafny { public readonly string Name;
public List<ModuleDefinition/*!*/>/*!*/ Modules; // filled in during resolution.
- // Resolution essentially flattens the module heirarchy, for
- // purposes of translation and compilation.
+ // Resolution essentially flattens the module heirarchy, for
+ // purposes of translation and compilation.
+ public List<ModuleDefinition> CompileModules; // filled in during resolution.
+ // Contains the definitions to be used for compilation.
+
public readonly ModuleDecl DefaultModule;
public readonly ModuleDefinition DefaultModuleDef;
public readonly BuiltIns BuiltIns;
@@ -34,6 +37,7 @@ namespace Microsoft.Dafny { DefaultModuleDef = (DefaultModuleDecl)((LiteralModuleDecl)module).ModuleDef;
BuiltIns = builtIns;
Modules = new List<ModuleDefinition>();
+ CompileModules = new List<ModuleDefinition>();
}
}
@@ -601,7 +605,7 @@ namespace Microsoft.Dafny { /// This proxy stands for any type, but it originates from an instantiated type parameter.
/// </summary>
public class ParamTypeProxy : UnrestrictedTypeProxy {
- TypeParameter orig;
+ public TypeParameter orig;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(orig != null);
@@ -819,16 +823,20 @@ namespace Microsoft.Dafny { ModuleReference = null;
}
}
- // Represents "module name as path;", where name is a identifier and path is a possibly qualified name.
+ // Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name.
public class AbstractModuleDecl : ModuleDecl
{
public ModuleDecl Root;
public readonly List<IToken> Path;
+ public ModuleDecl CompileRoot;
+ public readonly List<IToken> CompilePath;
public ModuleSignature OriginalSignature;
- public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent)
+
+ public AbstractModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, List<IToken> compilePath)
: base(name, name.val, parent) {
Path = path;
Root = null;
+ CompilePath = compilePath;
}
}
@@ -837,9 +845,10 @@ namespace Microsoft.Dafny { public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();
public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();
public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();
- public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.
- // it is abstract). Otherwise, it points to that definition.
- public ModuleSignature Refines;
+ public ModuleDefinition ModuleDef = null; // Note: this is null if this signature does not correspond to a specific definition (i.e.
+ // it is abstract). Otherwise, it points to that definition.
+ public ModuleSignature CompileSignature = null; // This is the version of the signature that should be used at compile time.
+ public ModuleSignature Refines = null;
public bool IsGhost = false;
public ModuleSignature() {}
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 14ff3348..f572f419 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -151,6 +151,7 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="Cloner.cs" />
<Compile Include="Util.cs" />
<Compile Include="Compiler.cs" />
<Compile Include="DafnyAst.cs" />
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 73724b28..ad2009c2 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -233,7 +233,7 @@ bool IsAttribute() { ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
Attributes attrs = null; IToken/*!*/ id;
List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
- List<IToken> idRefined = null, idPath = null;
+ List<IToken> idRefined = null, idPath = null, idAssignment = null;
bool isGhost = false;
ModuleDefinition module;
ModuleDecl sm;
@@ -289,8 +289,12 @@ bool IsAttribute() { } else if (la.kind == 13) {
Get();
QualifiedName(out idPath);
+ if (la.kind == 11) {
+ Get();
+ QualifiedName(out idAssignment);
+ }
Expect(12);
- submodule = new AbstractModuleDecl(idPath, id, parent);
+ submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment);
} else SynErr(112);
}
@@ -962,7 +966,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void FrameExpression(out FrameExpression/*!*/ fe) {
- Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
+ Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null;
if (StartOf(10)) {
Expression(out e);
if (la.kind == 50) {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 30fac1cc..56063442 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -18,13 +18,13 @@ using System.Numerics; using System.Diagnostics.Contracts;
using IToken = Microsoft.Boogie.IToken;
-namespace Microsoft.Dafny {
+namespace Microsoft.Dafny
+{
public class RefinementToken : TokenWrapper
{
public readonly ModuleDefinition InheritingModule;
public RefinementToken(IToken tok, ModuleDefinition m)
- : base(tok)
- {
+ : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(m != null);
this.InheritingModule = m;
@@ -53,23 +53,27 @@ namespace Microsoft.Dafny { public class RefinementTransformer : IRewriter
{
ResolutionErrorReporter reporter;
+ Cloner rawCloner; // This cloner just gives exactly the same thing back.
+ RefinementCloner refinementCloner; // This cloner wraps things in a RefinementTransformer
public RefinementTransformer(ResolutionErrorReporter reporter) {
Contract.Requires(reporter != null);
this.reporter = reporter;
+ rawCloner = new Cloner();
}
private ModuleDefinition moduleUnderConstruction; // non-null for the duration of Construct calls
private Queue<Action> postTasks = new Queue<Action>(); // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
public void PreResolve(ModuleDefinition m) {
-
+
if (m.RefinementBase == null) return;
if (moduleUnderConstruction != null) {
postTasks.Clear();
}
moduleUnderConstruction = m;
- var prev = m.RefinementBase;
+ refinementCloner = new RefinementCloner(moduleUnderConstruction);
+ var prev = m.RefinementBase;
// Create a simple name-to-decl dictionary. Ignore any duplicates at this time.
var declaredNames = new Dictionary<string, int>();
@@ -84,7 +88,7 @@ namespace Microsoft.Dafny { foreach (var d in prev.TopLevelDecls) {
int index;
if (!declaredNames.TryGetValue(d.Name, out index)) {
- m.TopLevelDecls.Add(CloneDeclaration(d, m));
+ m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m));
} else {
var nw = m.TopLevelDecls[index];
if (d is ModuleDecl) {
@@ -104,14 +108,7 @@ namespace Microsoft.Dafny { }
if (derived != null) {
// check that the new module refines the previous declaration
- while (derived != null) {
- if (derived == original)
- break;
- derived = derived.Refines;
- }
- if (derived != original) {
- reporter.Error(nw, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);
- }
+ CheckIsRefinement(derived, original, nw.tok, "a module (" + d.Name + ") can only be replaced by a refinement of the original module");
}
}
} else if (d is ArbitraryTypeDecl) {
@@ -167,6 +164,18 @@ namespace Microsoft.Dafny { Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method
}
+ public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original, IToken errorTok, string errorMsg) {
+ while (derived != null) {
+ if (derived == original)
+ break;
+ derived = derived.Refines;
+ }
+ if (derived != original) {
+ reporter.Error(errorTok, errorMsg);
+ return false;
+ } else return true;
+ }
+
public void PostResolve(ModuleDefinition m) {
if (m == moduleUnderConstruction) {
while (this.postTasks.Count != 0) {
@@ -178,453 +187,20 @@ namespace Microsoft.Dafny { }
moduleUnderConstruction = null;
}
-
- IToken Tok(IToken tok) {
- if (moduleUnderConstruction == null) {
- return tok;
- } else {
- return new RefinementToken(tok, moduleUnderConstruction);
- }
- }
-
- // -------------------------------------------------- Cloning ---------------------------------------------------------------
-
- // Clone a toplevel, specifying that its parent module should be m (i.e. it will be added to m.TopLevelDecls).
- TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
- Contract.Requires(d != null);
- Contract.Requires(m != null);
-
- if (d is ArbitraryTypeDecl) {
- var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);
- } else if (d is IndDatatypeDecl) {
- var dd = (IndDatatypeDecl)d;
- var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
- var ctors = dd.Ctors.ConvertAll(CloneCtor);
- var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
- return dt;
- } else if (d is CoDatatypeDecl) {
- var dd = (CoDatatypeDecl)d;
- var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
- var ctors = dd.Ctors.ConvertAll(CloneCtor);
- var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
- return dt;
- } else if (d is ClassDecl) {
- var dd = (ClassDecl)d;
- var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
- var mm = dd.Members.ConvertAll(CloneMember);
- var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
- return cl;
- } else if (d is ModuleDecl) {
- if (d is LiteralModuleDecl) {
- return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef,m);
- } else if (d is AliasModuleDecl) {
- var a = (AliasModuleDecl)d;
- var alias = new AliasModuleDecl(a.Path, a.tok, m);
- alias.ModuleReference = a.ModuleReference;
- alias.Signature = a.Signature;
- return alias;
- } else if (d is AbstractModuleDecl) {
- var a = (AbstractModuleDecl)d;
- var abs = new AbstractModuleDecl(a.Path, a.tok, m);
- abs.Signature = a.Signature;
- abs.OriginalSignature = a.OriginalSignature;
- return abs;
- } else {
- Contract.Assert(false); // unexpected declaration
- return null; // to please compiler
- }
- } else {
- Contract.Assert(false); // unexpected declaration
- return null; // to please compiler
- }
- }
-
- DatatypeCtor CloneCtor(DatatypeCtor ct) {
- return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
- }
-
- TypeParameter CloneTypeParam(TypeParameter tp) {
- return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);
- }
-
- MemberDecl CloneMember(MemberDecl member) {
- if (member is Field) {
- var f = (Field)member;
- return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
- } else if (member is Function) {
- var f = (Function)member;
- return CloneFunction(Tok(f.tok), f, f.IsGhost, null, null, null);
- } else {
- var m = (Method)member;
- return CloneMethod(m, null, null);
- }
- }
-
- Type CloneType(Type t) {
- if (t is BasicType) {
- return t;
- } else if (t is SetType) {
- var tt = (SetType)t;
- return new SetType(CloneType(tt.Arg));
- } else if (t is SeqType) {
- var tt = (SeqType)t;
- return new SeqType(CloneType(tt.Arg));
- } else if (t is MultiSetType) {
- var tt = (MultiSetType)t;
- return new MultiSetType(CloneType(tt.Arg));
- } else if (t is MapType) {
- var tt = (MapType)t;
- return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
- } else if (t is UserDefinedType) {
- var tt = (UserDefinedType)t;
- return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => Tok(x)));
- } else if (t is InferredTypeProxy) {
- return new InferredTypeProxy();
- } else {
- Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
- return null; // to please compiler
- }
- }
-
- Formal CloneFormal(Formal formal) {
- return new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
- }
-
- BoundVar CloneBoundVar(BoundVar bv) {
- return new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
- }
-
- Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
- var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
- return new Specification<Expression>(ee, null);
- }
-
- Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
- var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
- return new Specification<FrameExpression>(ee, null);
- }
-
- FrameExpression CloneFrameExpr(FrameExpression frame) {
- return new FrameExpression(CloneExpr(frame.E), frame.FieldName);
- }
-
- Attributes.Argument CloneAttrArg(Attributes.Argument aa) {
- if (aa.E != null) {
- return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));
- } else {
- return new Attributes.Argument(Tok(aa.Tok), aa.S);
- }
- }
-
- MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
- return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
- }
-
- Expression CloneExpr(Expression expr) {
- if (expr == null) {
- return null;
- } else if (expr is LiteralExpr) {
- var e = (LiteralExpr)expr;
- if (e.Value == null) {
- return new LiteralExpr(Tok(e.tok));
- } else if (e.Value is bool) {
- return new LiteralExpr(Tok(e.tok), (bool)e.Value);
- } else {
- return new LiteralExpr(Tok(e.tok), (BigInteger)e.Value);
- }
-
- } else if (expr is ThisExpr) {
- if (expr is ImplicitThisExpr) {
- return new ImplicitThisExpr(Tok(expr.tok));
- } else {
- return new ThisExpr(Tok(expr.tok));
- }
-
- } else if (expr is IdentifierExpr) {
- var e = (IdentifierExpr)expr;
- return new IdentifierExpr(Tok(e.tok), e.Name);
-
- } else if (expr is DatatypeValue) {
- var e = (DatatypeValue)expr;
- return new DatatypeValue(Tok(e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));
-
- } else if (expr is DisplayExpression) {
- DisplayExpression e = (DisplayExpression)expr;
- if (expr is SetDisplayExpr) {
- return new SetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
- } else if (expr is MultiSetDisplayExpr) {
- return new MultiSetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
- } else {
- Contract.Assert(expr is SeqDisplayExpr);
- return new SeqDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));
- }
-
- } else if (expr is MapDisplayExpr) {
- MapDisplayExpr e = (MapDisplayExpr)expr;
- List<ExpressionPair> pp = new List<ExpressionPair>();
- foreach(ExpressionPair p in e.Elements) {
- pp.Add(new ExpressionPair(CloneExpr(p.A),CloneExpr(p.B)));
- }
- return new MapDisplayExpr(Tok(expr.tok), pp);
- } else if (expr is ExprDotName) {
- var e = (ExprDotName)expr;
- return new ExprDotName(Tok(e.tok), CloneExpr(e.Obj), e.SuffixName);
-
- } else if (expr is FieldSelectExpr) {
- var e = (FieldSelectExpr)expr;
- return new FieldSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.FieldName);
-
- } else if (expr is SeqSelectExpr) {
- var e = (SeqSelectExpr)expr;
- return new SeqSelectExpr(Tok(e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));
-
- } else if (expr is MultiSelectExpr) {
- var e = (MultiSelectExpr)expr;
- return new MultiSelectExpr(Tok(e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));
-
- } else if (expr is SeqUpdateExpr) {
- var e = (SeqUpdateExpr)expr;
- return new SeqUpdateExpr(Tok(e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));
-
- } else if (expr is FunctionCallExpr) {
- var e = (FunctionCallExpr)expr;
- return new FunctionCallExpr(Tok(e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : Tok(e.OpenParen), e.Args.ConvertAll(CloneExpr));
-
- } else if (expr is OldExpr) {
- var e = (OldExpr)expr;
- return new OldExpr(Tok(e.tok), CloneExpr(e.E));
-
- } else if (expr is MultiSetFormingExpr) {
- var e = (MultiSetFormingExpr)expr;
- return new MultiSetFormingExpr(Tok(e.tok), CloneExpr(e.E));
-
- } else if (expr is FreshExpr) {
- var e = (FreshExpr)expr;
- return new FreshExpr(Tok(e.tok), CloneExpr(e.E));
-
- } else if (expr is AllocatedExpr) {
- var e = (AllocatedExpr)expr;
- return new AllocatedExpr(Tok(e.tok), CloneExpr(e.E));
-
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- return new UnaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E));
-
- } else if (expr is BinaryExpr) {
- var e = (BinaryExpr)expr;
- return new BinaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
-
- } else if (expr is ChainingExpression) {
- var e = (ChainingExpression)expr;
- return CloneExpr(e.E); // just clone the desugaring, since it's already available
-
- } else if (expr is LetExpr) {
- var e = (LetExpr)expr;
- return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));
-
- } else if (expr is NamedExpr) {
- var e = (NamedExpr) expr;
- return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));
- } else if (expr is ComprehensionExpr) {
- var e = (ComprehensionExpr)expr;
- var tk = Tok(e.tok);
- var bvs = e.BoundVars.ConvertAll(CloneBoundVar);
- var range = CloneExpr(e.Range);
- var term = CloneExpr(e.Term);
- if (e is ForallExpr) {
- return new ForallExpr(tk, bvs, range, term, null);
- } else if (e is ExistsExpr) {
- return new ExistsExpr(tk, bvs, range, term, null);
- } else if (e is MapComprehension) {
- return new MapComprehension(tk, bvs, range, term);
- } else {
- Contract.Assert(e is SetComprehension);
- return new SetComprehension(tk, bvs, range, term);
- }
-
- } else if (expr is WildcardExpr) {
- return new WildcardExpr(Tok(expr.tok));
-
- } else if (expr is PredicateExpr) {
- var e = (PredicateExpr)expr;
- if (e is AssertExpr) {
- return new AssertExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
- } else {
- Contract.Assert(e is AssumeExpr);
- return new AssumeExpr(Tok(e.tok), CloneExpr(e.Guard), CloneExpr(e.Body));
- }
-
- } else if (expr is ITEExpr) {
- var e = (ITEExpr)expr;
- return new ITEExpr(Tok(e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));
-
- } else if (expr is ParensExpression) {
- var e = (ParensExpression)expr;
- return CloneExpr(e.E); // skip the parentheses in the clone
-
- } else if (expr is IdentifierSequence) {
- var e = (IdentifierSequence)expr;
- var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);
- return new IdentifierSequence(e.Tokens.ConvertAll(tk => Tok(tk)), e.OpenParen == null ? null : Tok(e.OpenParen), aa);
-
- } else if (expr is MatchExpr) {
- var e = (MatchExpr)expr;
- return new MatchExpr(Tok(e.tok), CloneExpr(e.Source),
- e.Cases.ConvertAll(c => new MatchCaseExpr(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
-
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
- }
- }
-
- AssignmentRhs CloneRHS(AssignmentRhs rhs) {
- if (rhs is ExprRhs) {
- var r = (ExprRhs)rhs;
- return new ExprRhs(CloneExpr(r.Expr));
- } else if (rhs is HavocRhs) {
- return new HavocRhs(Tok(rhs.Tok));
- } else {
- var r = (TypeRhs)rhs;
- if (r.ArrayDimensions != null) {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));
- } else if (r.InitCall != null) {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));
- } else {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType));
- }
- }
- }
-
- BlockStmt CloneBlockStmt(BlockStmt stmt) {
- if (stmt == null) {
- return null;
- } else {
- return new BlockStmt(Tok(stmt.Tok), stmt.Body.ConvertAll(CloneStmt));
- }
- }
-
- Statement CloneStmt(Statement stmt) {
- if (stmt == null) {
- return null;
- }
-
- Statement r;
- if (stmt is AssertStmt) {
- var s = (AssertStmt)stmt;
- r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
-
- } else if (stmt is AssumeStmt) {
- var s = (AssumeStmt)stmt;
- r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
-
- } else if (stmt is PrintStmt) {
- var s = (PrintStmt)stmt;
- r = new PrintStmt(Tok(s.Tok), s.Args.ConvertAll(CloneAttrArg));
-
- } else if (stmt is BreakStmt) {
- var s = (BreakStmt)stmt;
- if (s.TargetLabel != null) {
- r = new BreakStmt(Tok(s.Tok), s.TargetLabel);
- } else {
- r = new BreakStmt(Tok(s.Tok), s.BreakCount);
- }
-
- } else if (stmt is ReturnStmt) {
- var s = (ReturnStmt)stmt;
- r = new ReturnStmt(Tok(s.Tok), s.rhss == null ? null : s.rhss.ConvertAll(CloneRHS));
-
- } else if (stmt is AssignStmt) {
- var s = (AssignStmt)stmt;
- r = new AssignStmt(Tok(s.Tok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));
-
- } else if (stmt is VarDecl) {
- var s = (VarDecl)stmt;
- r = new VarDecl(Tok(s.Tok), s.Name, CloneType(s.OptionalType), s.IsGhost);
-
- } else if (stmt is CallStmt) {
- var s = (CallStmt)stmt;
- r = new CallStmt(Tok(s.Tok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName, s.Args.ConvertAll(CloneExpr));
-
- } else if (stmt is BlockStmt) {
- r = CloneBlockStmt((BlockStmt)stmt);
-
- } else if (stmt is IfStmt) {
- var s = (IfStmt)stmt;
- r = new IfStmt(Tok(s.Tok), CloneExpr(s.Guard), CloneBlockStmt(s.Thn), CloneStmt(s.Els));
-
- } else if (stmt is AlternativeStmt) {
- var s = (AlternativeStmt)stmt;
- r = new AlternativeStmt(Tok(s.Tok), s.Alternatives.ConvertAll(CloneGuardedAlternative));
-
- } else if (stmt is WhileStmt) {
- var s = (WhileStmt)stmt;
- r = new WhileStmt(Tok(s.Tok), CloneExpr(s.Guard), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), CloneBlockStmt(s.Body));
-
- } else if (stmt is AlternativeLoopStmt) {
- var s = (AlternativeLoopStmt)stmt;
- r = new AlternativeLoopStmt(Tok(s.Tok), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), s.Alternatives.ConvertAll(CloneGuardedAlternative));
-
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
-
- } else if (stmt is MatchStmt) {
- var s = (MatchStmt)stmt;
- r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source),
- s.Cases.ConvertAll(c => new MatchCaseStmt(Tok(c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), c.Body.ConvertAll(CloneStmt))));
-
- } else if (stmt is AssignSuchThatStmt) {
- var s = (AssignSuchThatStmt)stmt;
- r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));
-
- } else if (stmt is UpdateStmt) {
- var s = (UpdateStmt)stmt;
- r = new UpdateStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), s.Rhss.ConvertAll(CloneRHS), s.CanMutateKnownState);
-
- } else if (stmt is VarDeclStmt) {
- var s = (VarDeclStmt)stmt;
- r = new VarDeclStmt(Tok(s.Tok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (ConcreteUpdateStatement)CloneStmt(s.Update));
-
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
- }
-
- // add labels to the cloned statement
- AddStmtLabels(r, stmt.Labels);
-
- return r;
- }
-
- void AddStmtLabels(Statement s, LList<Label> node) {
- if (node != null) {
- AddStmtLabels(s, node.Next);
- if (node.Data.Name == null) {
- // this indicates an implicit-target break statement that has been resolved; don't add it
- } else {
- s.Labels = new LList<Label>(new Label(Tok(node.Data.Tok), node.Data.Name), s.Labels);
- }
- }
- }
-
- GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) {
- return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt));
- }
-
Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody) {
Contract.Requires(moreBody == null || f is Predicate);
Contract.Requires(moreBody == null || replacementBody == null);
- var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
- var formals = f.Formals.ConvertAll(CloneFormal);
- var req = f.Req.ConvertAll(CloneExpr);
- var reads = f.Reads.ConvertAll(CloneFrameExpr);
- var decreases = CloneSpecExpr(f.Decreases);
+ var tps = f.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam);
+ var formals = f.Formals.ConvertAll(refinementCloner.CloneFormal);
+ var req = f.Req.ConvertAll(refinementCloner.CloneExpr);
+ var reads = f.Reads.ConvertAll(refinementCloner.CloneFrameExpr);
+ var decreases = refinementCloner.CloneSpecExpr(f.Decreases);
- var previousModuleUnderConstruction = moduleUnderConstruction;
- if (moreBody != null || replacementBody != null) { moduleUnderConstruction = null; }
- var ens = f.Ens.ConvertAll(CloneExpr);
- moduleUnderConstruction = previousModuleUnderConstruction;
+ List<Expression> ens;
+ if (moreBody != null || replacementBody != null)
+ ens = f.Ens.ConvertAll(rawCloner.CloneExpr);
+ else ens = f.Ens.ConvertAll(refinementCloner.CloneExpr);
if (moreEnsures != null) {
ens.AddRange(moreEnsures);
}
@@ -636,10 +212,10 @@ namespace Microsoft.Dafny { if (f.Body == null) {
body = moreBody;
} else {
- body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, CloneExpr(f.Body), moreBody);
+ body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, refinementCloner.CloneExpr(f.Body), moreBody);
}
} else {
- body = CloneExpr(f.Body);
+ body = refinementCloner.CloneExpr(f.Body);
}
if (f is Predicate) {
@@ -649,7 +225,7 @@ namespace Microsoft.Dafny { return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
req, reads, ens, body, null, false);
} else {
- return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
+ return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, refinementCloner.CloneType(f.ResultType),
req, reads, ens, decreases, body, null, false);
}
}
@@ -657,26 +233,26 @@ namespace Microsoft.Dafny { Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, BlockStmt replacementBody) {
Contract.Requires(m != null);
- var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
- var ins = m.Ins.ConvertAll(CloneFormal);
- var req = m.Req.ConvertAll(CloneMayBeFreeExpr);
- var mod = CloneSpecFrameExpr(m.Mod);
- var decreases = CloneSpecExpr(m.Decreases);
+ var tps = m.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam);
+ var ins = m.Ins.ConvertAll(refinementCloner.CloneFormal);
+ var req = m.Req.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
+ var mod = refinementCloner.CloneSpecFrameExpr(m.Mod);
+ var decreases = refinementCloner.CloneSpecExpr(m.Decreases);
- var previousModuleUnderConstruction = moduleUnderConstruction;
- if (replacementBody != null) { moduleUnderConstruction = null; }
- var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);
- if (replacementBody != null) { moduleUnderConstruction = previousModuleUnderConstruction; }
+ List<MaybeFreeExpression> ens;
+ if (replacementBody != null)
+ ens = m.Ens.ConvertAll(rawCloner.CloneMayBeFreeExpr);
+ else ens = m.Ens.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
if (moreEnsures != null) {
ens.AddRange(moreEnsures);
}
- var body = replacementBody ?? CloneBlockStmt(m.Body);
+ var body = replacementBody ?? refinementCloner.CloneBlockStmt(m.Body);
if (m is Constructor) {
- return new Constructor(Tok(m.tok), m.Name, tps, ins,
+ return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
req, mod, ens, decreases, body, null, false);
} else {
- return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, null, false);
}
}
@@ -699,7 +275,7 @@ namespace Microsoft.Dafny { foreach (var member in prev.Members) {
int index;
if (!declaredNames.TryGetValue(member.Name, out index)) {
- nw.Members.Add(CloneMember(member));
+ nw.Members.Add(refinementCloner.CloneMember(member));
} else {
var nwMember = nw.Members[index];
if (nwMember is Field) {
@@ -809,229 +385,6 @@ namespace Microsoft.Dafny { return nw;
}
- private Statement SubstituteNamedExpr(Statement s, Dictionary<string, Expression> sub, SortedSet<string> subs) {
- if (s == null) {
- return null;
- } else if (s is AssertStmt) {
- AssertStmt stmt = (AssertStmt)s;
- return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);
- } else if (s is AssumeStmt) {
- AssumeStmt stmt = (AssumeStmt)s;
- return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, sub, subs), null);
- } else if (s is PrintStmt) {
- throw new NotImplementedException();
- } else if (s is BreakStmt) {
- return s;
- } else if (s is ReturnStmt) {
- return s;
- } else if (s is VarDeclStmt) {
- return s;
- } else if (s is AssignSuchThatStmt) {
- return s;
- } else if (s is UpdateStmt) {
- UpdateStmt stmt = (UpdateStmt)s;
- List<Expression> lhs = new List<Expression>();
- List<AssignmentRhs> rhs = new List<AssignmentRhs>();
- foreach (Expression l in stmt.Lhss) {
- lhs.Add(SubstituteNamedExpr(l, sub, subs));
- }
- foreach (AssignmentRhs r in stmt.Rhss) {
- if (r is HavocRhs) {
- rhs.Add(r); // no substitution on Havoc (*);
- } else if (r is ExprRhs) {
- rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, sub, subs)));
- } else if (r is CallRhs) {
- CallRhs rr = (CallRhs)r;
- rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, sub, subs), rr.MethodName, SubstituteNamedExprList(rr.Args, sub, subs)));
- } else if (r is TypeRhs) {
- rhs.Add(r);
- } else {
- Contract.Assert(false); // unexpected AssignmentRhs
- throw new cce.UnreachableException();
- }
- }
- return new UpdateStmt(stmt.Tok, lhs, rhs);
- } else if (s is AssignStmt) {
- Contract.Assert(false); // AssignStmt is not generated by the parser
- throw new cce.UnreachableException();
- } else if (s is VarDecl) {
- return s;
- } else if (s is CallStmt) {
- return s;
- } else if (s is BlockStmt) {
- BlockStmt stmt = (BlockStmt)s;
- List<Statement> res = new List<Statement>();
- foreach (Statement ss in stmt.Body) {
- res.Add(SubstituteNamedExpr(ss, sub, subs));
- }
- return new BlockStmt(stmt.Tok, res);
- } else if (s is IfStmt) {
- IfStmt stmt = (IfStmt)s;
- return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs),
- (BlockStmt)SubstituteNamedExpr(stmt.Thn, sub, subs),
- SubstituteNamedExpr(stmt.Els, sub, subs));
- } else if (s is AlternativeStmt) {
- return s;
- } else if (s is WhileStmt) {
- WhileStmt stmt = (WhileStmt)s;
- return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, sub, subs), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, sub, subs));
- } else if (s is AlternativeLoopStmt) {
- return s;
- } else if (s is ParallelStmt) {
- return s;
- } else if (s is MatchStmt) {
- return s;
- } else if (s is SkeletonStatement) {
- return s;
- } else {
- Contract.Assert(false); // unexpected statement
- throw new cce.UnreachableException();
- }
-
- }
- private Expression SubstituteNamedExpr(Expression expr, Dictionary<string, Expression> sub, SortedSet<string> subs) {
- if (expr == null) {
- return null;
- }
- if (expr is NamedExpr) {
- NamedExpr n = (NamedExpr)expr;
- Expression E;
- if (sub.TryGetValue(n.Name, out E)) {
- subs.Add(n.Name);
- return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), E.tok);
- } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, sub, subs));
- } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {
- return expr;
- } else if (expr is DisplayExpression) {
- DisplayExpression e = (DisplayExpression)expr;
- List<Expression> newElements = SubstituteNamedExprList(e.Elements, sub, subs);
- if (expr is SetDisplayExpr) {
- return new SetDisplayExpr(expr.tok, newElements);
- } else if (expr is MultiSetDisplayExpr) {
- return new MultiSetDisplayExpr(expr.tok, newElements);
- } else {
- return new SeqDisplayExpr(expr.tok, newElements);
- }
- } else if (expr is FieldSelectExpr) {
- FieldSelectExpr fse = (FieldSelectExpr)expr;
- Expression substE = SubstituteNamedExpr(fse.Obj, sub, subs);
- return new FieldSelectExpr(fse.tok, substE, fse.FieldName);
- } else if (expr is SeqSelectExpr) {
- SeqSelectExpr sse = (SeqSelectExpr)expr;
- Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);
- Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, sub, subs);
- Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, sub, subs);
- return new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
- } else if (expr is SeqUpdateExpr) {
- SeqUpdateExpr sse = (SeqUpdateExpr)expr;
- Expression seq = SubstituteNamedExpr(sse.Seq, sub, subs);
- Expression index = SubstituteNamedExpr(sse.Index, sub, subs);
- Expression val = SubstituteNamedExpr(sse.Value, sub, subs);
- return new SeqUpdateExpr(sse.tok, seq, index, val);
- } else if (expr is MultiSelectExpr) {
- MultiSelectExpr mse = (MultiSelectExpr)expr;
- Expression array = SubstituteNamedExpr(mse.Array, sub, subs);
- List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, sub, subs);
- return new MultiSelectExpr(mse.tok, array, newArgs);
- } else if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
- Expression receiver = SubstituteNamedExpr(e.Receiver, sub, subs);
- List<Expression> newArgs = SubstituteNamedExprList(e.Args, sub, subs);
- return new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);
- } else if (expr is DatatypeValue) {
- DatatypeValue dtv = (DatatypeValue)expr;
- List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, sub, subs);
- return new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
- } else if (expr is OldExpr) {
- OldExpr e = (OldExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, sub, subs);
- return new OldExpr(expr.tok, se);
- } else if (expr is FreshExpr) {
- FreshExpr e = (FreshExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, sub, subs);
- return new FreshExpr(expr.tok, se);
- } else if (expr is AllocatedExpr) {
- AllocatedExpr e = (AllocatedExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, sub, subs);
- return new AllocatedExpr(expr.tok, se);
- } else if (expr is UnaryExpr) {
- UnaryExpr e = (UnaryExpr)expr;
- Expression se = SubstituteNamedExpr(e.E, sub, subs);
- return new UnaryExpr(expr.tok, e.Op, se);
- } else if (expr is BinaryExpr) {
- BinaryExpr e = (BinaryExpr)expr;
- Expression e0 = SubstituteNamedExpr(e.E0, sub, subs);
- Expression e1 = SubstituteNamedExpr(e.E1, sub, subs);
- return new BinaryExpr(expr.tok, e.Op, e0, e1);
- } else if (expr is LetExpr) {
- var e = (LetExpr)expr;
- var rhss = SubstituteNamedExprList(e.RHSs, sub, subs);
- var body = SubstituteNamedExpr(e.Body, sub, subs);
- return new LetExpr(e.tok, e.Vars, rhss, body);
- } else if (expr is ComprehensionExpr) {
- var e = (ComprehensionExpr)expr;
- Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, sub, subs);
- Expression newTerm = SubstituteNamedExpr(e.Term, sub, subs);
- Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, sub, ref subCount);
- if (e is SetComprehension) {
- return new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
- } else if (e is MapComprehension) {
- return new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);
- } else if (e is QuantifierExpr) {
- var q = (QuantifierExpr)e;
- if (expr is ForallExpr) {
- return new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
- } else {
- return new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
- }
- } else {
- Contract.Assert(false); // unexpected ComprehensionExpr
- throw new cce.UnreachableException();
- }
-
- } else if (expr is PredicateExpr) {
- var e = (PredicateExpr)expr;
- Expression g = SubstituteNamedExpr(e.Guard, sub, subs);
- Expression b = SubstituteNamedExpr(e.Body, sub, subs);
- if (expr is AssertExpr) {
- return new AssertExpr(e.tok, g, b);
- } else {
- return new AssumeExpr(e.tok, g, b);
- }
- } else if (expr is ITEExpr) {
- ITEExpr e = (ITEExpr)expr;
- Expression test = SubstituteNamedExpr(e.Test, sub, subs);
- Expression thn = SubstituteNamedExpr(e.Thn, sub, subs);
- Expression els = SubstituteNamedExpr(e.Els, sub, subs);
- return new ITEExpr(expr.tok, test, thn, els);
- } else if (expr is ConcreteSyntaxExpression) {
- if (expr is ParensExpression) {
- return SubstituteNamedExpr(((ParensExpression)expr).E, sub, subs);
- } else if (expr is IdentifierSequence) {
- return expr;
- } else if (expr is ExprDotName) {
- ExprDotName edn = (ExprDotName)expr;
- return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, sub, subs), edn.SuffixName);
- } else if (expr is ChainingExpression) {
- ChainingExpression ch = (ChainingExpression)expr;
- return SubstituteNamedExpr(ch.E, sub, subs);
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
-
- private List<Expression> SubstituteNamedExprList(List<Expression> list, Dictionary<string, Expression> sub, SortedSet<string> subCount) {
- List<Expression> res = new List<Expression>();
- foreach (Expression e in list) {
- res.Add(SubstituteNamedExpr(e, sub, subCount));
- }
- return res;
- }
void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {
Contract.Requires(tok != null);
Contract.Requires(old != null);
@@ -1158,39 +511,38 @@ namespace Microsoft.Dafny { */
if (cur is SkeletonStatement) {
var S = ((SkeletonStatement)cur).S;
- var c = (SkeletonStatement) cur;
+ var c = (SkeletonStatement)cur;
if (S == null) {
- var nxt = i + 1 == skeleton.Body.Count ? null : skeleton.Body[i+1];
+ var nxt = i + 1 == skeleton.Body.Count ? null : skeleton.Body[i + 1];
if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {
// "...; ...;" is the same as just "...;", so skip this one
} else {
- SortedSet<string> substitutions = null;
- Dictionary<string, Expression> subExprs = null;
+ SubstitutionCloner subber = null;
if (c.NameReplacements != null) {
- subExprs = new Dictionary<string, Expression>();
- substitutions = new SortedSet<string>();
+ var subExprs = new Dictionary<string, Expression>();
Contract.Assert(c.NameReplacements.Count == c.ExprReplacements.Count);
for (int k = 0; k < c.NameReplacements.Count; k++) {
if (subExprs.ContainsKey(c.NameReplacements[k].val)) {
reporter.Error(c.NameReplacements[k], "replacement definition must contain at most one definition for a given label");
} else subExprs.Add(c.NameReplacements[k].val, c.ExprReplacements[k]);
}
+ subber = new SubstitutionCloner(subExprs, rawCloner);
}
// skip up until the next thing that matches "nxt"
while (nxt == null || !PotentialMatch(nxt, oldS)) {
// loop invariant: oldS == oldStmt.Body[j]
- var s = CloneStmt(oldS);
- if (subExprs != null)
- s = SubstituteNamedExpr(s, subExprs, substitutions);
+ var s = refinementCloner.CloneStmt(oldS);
+ if (subber != null)
+ s = subber.CloneStmt(s);
body.Add(s);
j++;
if (j == oldStmt.Body.Count) { break; }
oldS = oldStmt.Body[j];
}
- if (subExprs != null && substitutions.Count < subExprs.Count) {
- foreach (var s in substitutions)
- subExprs.Remove(s);
- reporter.Error(c.Tok, "could not find labeled expression(s): " + Util.Comma(", ", subExprs.Keys, x => x));
+ if (subber != null && subber.SubstitutionsMade.Count < subber.Exprs.Count) {
+ foreach (var s in subber.SubstitutionsMade)
+ subber.Exprs.Remove(s);
+ reporter.Error(c.Tok, "could not find labeled expression(s): " + Util.Comma(", ", subber.Exprs.Keys, x => x));
}
}
i++;
@@ -1207,8 +559,8 @@ namespace Microsoft.Dafny { // that this assertion is supposed to be translated into a check. That is,
// it is not allowed to be just assumed in the translation, despite the fact
// that the condition is inherited.
- var e = CloneExpr(oldAssume.Expr);
- body.Add(new AssertStmt(skel.Tok, e, new Attributes("prependAssertToken", new List<Attributes.Argument>(), null)));
+ var e = refinementCloner.CloneExpr(oldAssume.Expr);
+ body.Add(new AssertStmt(new Translator.ForceCheckToken(skel.Tok), e, new Attributes("prependAssertToken", new List<Attributes.Argument>(), null)));
i++; j++;
}
@@ -1220,7 +572,7 @@ namespace Microsoft.Dafny { reporter.Error(cur.Tok, "assume template does not match inherited statement");
i++;
} else {
- var e = CloneExpr(oldAssume.Expr);
+ var e = refinementCloner.CloneExpr(oldAssume.Expr);
body.Add(new AssumeStmt(skel.Tok, e, null));
i++; j++;
}
@@ -1235,7 +587,7 @@ namespace Microsoft.Dafny { } else {
var resultingThen = MergeBlockStmt(skel.Thn, oldIf.Thn);
var resultingElse = MergeElse(skel.Els, oldIf.Els);
- var r = new IfStmt(skel.Tok, CloneExpr(oldIf.Guard), resultingThen, resultingElse);
+ var r = new IfStmt(skel.Tok, refinementCloner.CloneExpr(oldIf.Guard), resultingThen, resultingElse);
body.Add(r);
i++; j++;
}
@@ -1249,7 +601,7 @@ namespace Microsoft.Dafny { } else {
Expression guard;
if (((SkeletonStatement)cur).ConditionOmitted) {
- guard = CloneExpr(oldWhile.Guard);
+ guard = refinementCloner.CloneExpr(oldWhile.Guard);
} else {
if (oldWhile.Guard != null) {
reporter.Error(skel.Guard.tok, "a skeleton while statement with a guard can only replace a while statement with a non-deterministic guard");
@@ -1285,7 +637,7 @@ namespace Microsoft.Dafny { doMerge = true;
} else if (cOld.Update is AssignSuchThatStmt) {
doMerge = true;
- addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);
+ addedAssert = refinementCloner.CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);
} else {
var updateOld = (UpdateStmt)cOld.Update; // if cast fails, there are more ConcreteUpdateStatement subclasses than expected
doMerge = true;
@@ -1344,7 +696,7 @@ namespace Microsoft.Dafny { if (LeftHandSidesAgree(s.Lhss, nw.Lhss)) {
doMerge = true;
stmtGenerated.Add(nw);
- foreach(var rhs in s.Rhss) {
+ foreach (var rhs in s.Rhss) {
if (!(rhs is HavocRhs))
doMerge = false;
}
@@ -1354,7 +706,7 @@ namespace Microsoft.Dafny { if (LeftHandSidesAgree(s.Lhss, nw.Lhss)) {
doMerge = true;
stmtGenerated.Add(nw);
- var addedAssert = CloneExpr(s.Expr);
+ var addedAssert = refinementCloner.CloneExpr(s.Expr);
stmtGenerated.Add(new AssertStmt(new Translator.ForceCheckToken(addedAssert.tok), addedAssert, null));
}
}
@@ -1410,7 +762,7 @@ namespace Microsoft.Dafny { }
// implement the implicit "...;" at the end of each block statement skeleton
for (; j < oldStmt.Body.Count; j++) {
- body.Add(CloneStmt(oldStmt.Body[j]));
+ body.Add(refinementCloner.CloneStmt(oldStmt.Body[j]));
}
return new BlockStmt(skeleton.Tok, body);
}
@@ -1507,12 +859,12 @@ namespace Microsoft.Dafny { if (cNew.Decreases.Expressions.Count != 0) {
reporter.Error(cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'");
}
- decr = CloneSpecExpr(cOld.Decreases);
+ decr = refinementCloner.CloneSpecExpr(cOld.Decreases);
}
- var invs = cOld.Invariants.ConvertAll(CloneMayBeFreeExpr);
+ var invs = cOld.Invariants.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
invs.AddRange(cNew.Invariants);
- var r = new RefinedWhileStmt(cNew.Tok, guard, invs, decr, CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body));
+ var r = new RefinedWhileStmt(cNew.Tok, guard, invs, decr, refinementCloner.CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body));
return r;
}
@@ -1521,7 +873,7 @@ namespace Microsoft.Dafny { Contract.Requires(oldStmt == null || oldStmt is BlockStmt || oldStmt is IfStmt || oldStmt is SkeletonStatement);
if (skeleton == null) {
- return CloneStmt(oldStmt);
+ return refinementCloner.CloneStmt(oldStmt);
} else if (skeleton is IfStmt || skeleton is SkeletonStatement) {
// wrap a block statement around the if statement
skeleton = new BlockStmt(skeleton.Tok, new List<Statement>() { skeleton });
@@ -1656,4 +1008,38 @@ namespace Microsoft.Dafny { return false;
}
}
-}
+
+ class RefinementCloner : Cloner {
+ ModuleDefinition moduleUnderConstruction;
+ public RefinementCloner(ModuleDefinition m) {
+ moduleUnderConstruction = m;
+ }
+ override public IToken Tok(IToken tok) {
+ return new RefinementToken(tok, moduleUnderConstruction);
+ }
+ }
+ class SubstitutionCloner : Cloner {
+ public Dictionary<string, Expression> Exprs;
+ public SortedSet<string> SubstitutionsMade;
+ Cloner c;
+ public SubstitutionCloner(Dictionary<string, Expression> subs, Cloner c) {
+ Exprs = subs;
+ SubstitutionsMade = new SortedSet<string>();
+ this.c = c;
+ }
+ new public Expression CloneExpr(Expression expr) {
+ if (expr is NamedExpr) {
+ NamedExpr n = (NamedExpr)expr;
+ Expression E;
+ if (Exprs.TryGetValue(n.Name, out E)) {
+ SubstitutionsMade.Add(n.Name);
+ return new NamedExpr(n.tok, n.Name, E, c.CloneExpr(n.Body), E.tok);
+ }
+ }
+ return base.CloneExpr(expr); // in all other cases, just do what the base class would.
+ // note that when we get a named expression that is not in
+ // our substitution list, then we call the base class, which
+ // recurses on the body of the named expression.
+ }
+ }
+}
\ No newline at end of file diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f45c3dfa..74ddb08b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -9,7 +9,8 @@ using System.Numerics; using System.Diagnostics.Contracts;
using Microsoft.Boogie;
-namespace Microsoft.Dafny {
+namespace Microsoft.Dafny
+{
public class ResolutionErrorReporter
{
public int ErrorCount = 0;
@@ -60,7 +61,8 @@ namespace Microsoft.Dafny { }
}
- public class Resolver : ResolutionErrorReporter {
+ public class Resolver : ResolutionErrorReporter
+ {
readonly BuiltIns builtIns;
//Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes; // can map to AmbiguousTopLevelDecl
@@ -97,7 +99,9 @@ namespace Microsoft.Dafny { readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();
readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
- ModuleSignature systemNameInfo = null;
+ private ModuleSignature systemNameInfo = null;
+ private bool useCompileSignatures = false;
+
public Resolver(Program prog) {
Contract.Requires(prog != null);
builtIns = prog.BuiltIns;
@@ -115,9 +119,9 @@ namespace Microsoft.Dafny { Contract.Requires(prog != null);
var bindings = new ModuleBindings(null);
var b = BindModuleNames(prog.DefaultModuleDef, bindings);
- bindings.BindName("_module", prog.DefaultModule , b);
+ bindings.BindName("_module", prog.DefaultModule, b);
if (ErrorCount > 0) { return; } // if there were errors, then the implict ModuleBindings data structure invariant
- // is violated, so Processing dependencies will not succeed.
+ // is violated, so Processing dependencies will not succeed.
ProcessDependencies(prog.DefaultModule, b, dependencies);
// check for cycles in the import graph
List<ModuleDecl> cycle = dependencies.TryFindCycle();
@@ -141,7 +145,7 @@ namespace Microsoft.Dafny { }
var refinementTransformer = new RefinementTransformer(this);
-
+
IRewriter rewriter = new AutoContractsRewriter();
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
foreach (var decl in sortedDecls) {
@@ -156,6 +160,8 @@ namespace Microsoft.Dafny { // by the bodies.
var literalDecl = (LiteralModuleDecl)decl;
var m = (literalDecl).ModuleDef;
+
+ var errorCount = ErrorCount;
rewriter.PreResolve(m);
ModuleSignature refinedSig = null;
if (m.RefinementBaseRoot != null) {
@@ -174,14 +180,24 @@ namespace Microsoft.Dafny { literalDecl.Signature.Refines = refinedSig;
var sig = literalDecl.Signature;
// set up environment
- var errorCount = ErrorCount;
+ var preResolveErrorCount = ErrorCount;
+ useCompileSignatures = false;
ResolveModuleDefinition(m, sig);
-
- if (ErrorCount == errorCount) {
+ if (ErrorCount == preResolveErrorCount) {
refinementTransformer.PostResolve(m);
// give rewriter a chance to do processing
rewriter.PostResolve(m);
}
+ if (ErrorCount == errorCount && !m.IsGhost) {
+ // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include);
+ var nw = (new Cloner()).CloneModuleDefinition(m, m.CompileName + "_Compile");
+ var compileSig = RegisterTopLevelDecls(nw);
+ compileSig.Refines = refinedSig;
+ sig.CompileSignature = compileSig;
+ useCompileSignatures = true;
+ ResolveModuleDefinition(nw, compileSig);
+ prog.CompileModules.Add(nw);
+ }
} else if (decl is AliasModuleDecl) {
var alias = (AliasModuleDecl)decl;
// resolve the path
@@ -197,7 +213,16 @@ namespace Microsoft.Dafny { if (ResolvePath(abs.Root, abs.Path, out p)) {
abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules);
abs.OriginalSignature = p;
- // resolve
+ ModuleSignature compileSig;
+ if (abs.CompilePath != null) {
+ if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig)) {
+ if (refinementTransformer.CheckIsRefinement(compileSig, p, abs.CompilePath[0],
+ "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val))) {
+ abs.Signature.CompileSignature = compileSig;
+ abs.Signature.IsGhost = compileSig.IsGhost;
+ }
+ }
+ }
} else {
abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
}
@@ -229,7 +254,8 @@ namespace Microsoft.Dafny { }
- public class ModuleBindings {
+ public class ModuleBindings
+ {
private ModuleBindings parent;
private Dictionary<string, ModuleDecl> modules;
private Dictionary<string, ModuleBindings> bindings;
@@ -326,7 +352,7 @@ namespace Microsoft.Dafny { var alias = moduleDecl as AliasModuleDecl;
ModuleDecl root;
if (!bindings.TryLookup(alias.Path[0], out root))
- Error(alias.tok, "module {0} does not exist", Util.Comma(".", alias.Path, x => x.val));
+ Error(alias.tok, ModuleNotFoundErrorMessage(0, alias.Path));
else {
dependencies.AddEdge(moduleDecl, root);
alias.Root = root;
@@ -335,14 +361,27 @@ namespace Microsoft.Dafny { var abs = moduleDecl as AbstractModuleDecl;
ModuleDecl root;
if (!bindings.TryLookup(abs.Path[0], out root))
- Error(abs.tok, "module {0} does not exist", Util.Comma(".", abs.Path, x => x.val));
+ Error(abs.tok, ModuleNotFoundErrorMessage(0, abs.Path));
else {
dependencies.AddEdge(moduleDecl, root);
abs.Root = root;
}
+ if (abs.CompilePath != null) {
+ if (!bindings.TryLookup(abs.CompilePath[0], out root))
+ Error(abs.tok, ModuleNotFoundErrorMessage(0, abs.CompilePath));
+ else {
+ dependencies.AddEdge(moduleDecl, root);
+ abs.CompileRoot = root;
+ }
+ }
}
}
+ private string ModuleNotFoundErrorMessage(int i, List<IToken> path) {
+ return "module " + path[i].val + " does not exist" +
+ (1 < path.Count ? " (position " + i.ToString() + " in path " + Util.Comma(".", path, x => x.val) + ")" : "");
+ }
+
public static ModuleSignature MergeSignature(ModuleSignature m, ModuleSignature system) {
var info = new ModuleSignature();
// add the system-declared information, among which we know there are no duplicates
@@ -415,7 +454,7 @@ namespace Microsoft.Dafny { DatatypeDecl dt = (DatatypeDecl)d;
// register the names of the constructors
- Dictionary<string,DatatypeCtor> ctors = new Dictionary<string,DatatypeCtor>();
+ Dictionary<string, DatatypeCtor> ctors = new Dictionary<string, DatatypeCtor>();
datatypeCtors.Add(dt, ctors);
// ... and of the other members
Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();
@@ -424,7 +463,7 @@ namespace Microsoft.Dafny { foreach (DatatypeCtor ctor in dt.Ctors) {
if (ctor.Name.EndsWith("?")) {
Error(ctor, "a datatype constructor name is not allowed to end with '?'");
- } else if (ctors.ContainsKey(ctor.Name)) {
+ } else if (ctors.ContainsKey(ctor.Name)) {
Error(ctor, "Duplicate datatype constructor name: {0}", ctor.Name);
} else {
ctors.Add(ctor.Name, ctor);
@@ -469,13 +508,15 @@ namespace Microsoft.Dafny { }
private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> mods) {
- var mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null, false);
+ var mod = new ModuleDefinition(Token.NoToken, Name + ".Abs", true, true, null, null, false);
mod.Height = Height;
foreach (var kv in p.TopLevels) {
mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));
}
var sig = RegisterTopLevelDecls(mod);
sig.Refines = p.Refines;
+ sig.CompileSignature = p;
+ sig.IsGhost = p.IsGhost;
mods.Add(mod);
ResolveModuleDefinition(mod, sig);
return sig;
@@ -505,7 +546,7 @@ namespace Microsoft.Dafny { var mm = dd.Members.ConvertAll(CloneMember);
if (dd is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
- } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
+ } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
@@ -518,7 +559,7 @@ namespace Microsoft.Dafny { } else if (d is AbstractModuleDecl) {
var abs = (AbstractModuleDecl)d;
var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);
- var a = new AbstractModuleDecl(abs.Path, abs.tok, m);
+ var a = new AbstractModuleDecl(abs.Path, abs.tok, m, abs.CompilePath);
a.Signature = sig;
a.OriginalSignature = abs.OriginalSignature;
return a;
@@ -554,7 +595,7 @@ namespace Microsoft.Dafny { return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
}
Type CloneType(Type t) {
- if (t is BasicType) {
+ if (t is BasicType) {
return t;
} else if (t is SetType) {
var tt = (SetType)t;
@@ -589,7 +630,7 @@ namespace Microsoft.Dafny { var ens = f.Ens.ConvertAll(CloneExpr);
Expression body = CloneExpr(f.Body);
-
+
if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
req, reads, ens, decreases, body, false, null, false);
@@ -611,7 +652,7 @@ namespace Microsoft.Dafny { var decreases = CloneSpecExpr(m.Decreases);
var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);
-
+
if (m is Constructor) {
return new Constructor(m.tok, m.Name, tps, ins,
req, mod, ens, decreases, null, null, false);
@@ -800,7 +841,7 @@ namespace Microsoft.Dafny { p = pp;
i++;
} else {
- Error(Path[i], "module {0} does not exist", Path[i].val);
+ Error(Path[i], ModuleNotFoundErrorMessage(i, Path));
break;
}
}
@@ -820,13 +861,14 @@ namespace Microsoft.Dafny { } else if (d is ModuleDecl) {
var decl = (ModuleDecl)d;
if (!def.IsGhost) {
- if (decl.Signature.IsGhost) {
- if (!(def.IsDefaultModule)) // _module is allowed to contain ghost modules, but not by ghost itself. Note this presents a challenge to
- // trusted verification, as toplevels can't be trusted if they invoke ghost module members.
+ if (decl.Signature.IsGhost)
+ {
+ if (!(def.IsDefaultModule)) // _module is allowed to contain ghost modules, but not be ghost itself. Note this presents a challenge to
+ // trusted verification, as toplevels can't be trusted if they invoke ghost module members.
Error(d.tok, "ghost modules can only be imported into other ghost modules, not physical ones.");
- } else {
- // physical modules are allowed everywhere
- }
+ } else {
+ // physical modules are allowed everywhere
+ }
} else {
// everything is allowed in a ghost module
}
@@ -853,7 +895,7 @@ namespace Microsoft.Dafny { }
allTypeParameters.PopMarker();
}
-
+
foreach (TopLevelDecl d in declarations) {
if (d is ClassDecl) {
foreach (var member in ((ClassDecl)d).Members) {
@@ -863,9 +905,9 @@ namespace Microsoft.Dafny { CheckTypeInference(m.Body);
} else if (member is Function) {
var f = (Function)member;
- if (f.Body !=null)
+ if (f.Body != null)
CheckTypeInference(f.Body);
- }
+ }
}
}
}
@@ -1049,7 +1091,7 @@ namespace Microsoft.Dafny { var e = (ConcreteSyntaxExpression)expr;
CoPredicateChecks(e.Resolved, context, cp);
return;
- } else if (expr is FunctionCallExpr) {
+ } else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
var moduleCaller = context.EnclosingClass.Module;
var moduleCallee = e.Function.EnclosingClass.Module;
@@ -1420,7 +1462,7 @@ namespace Microsoft.Dafny { type = type.Normalize();
if (type is BasicType) {
- } else if (type is SetType) {
+ } else if (type is SetType) {
var st = (SetType)type;
return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);
} else if (type is MultiSetType) {
@@ -1459,13 +1501,12 @@ namespace Microsoft.Dafny { Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
-
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
- void ResolveClassMemberTypes(ClassDecl/*!*/ cl)
- {
+ void ResolveClassMemberTypes(ClassDecl/*!*/ cl) {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
@@ -1500,8 +1541,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Assumes type parameters have already been pushed, and that all types in class members have been resolved
/// </summary>
- void ResolveClassMemberBodies(ClassDecl cl)
- {
+ void ResolveClassMemberBodies(ClassDecl cl) {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
@@ -1536,8 +1576,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
- void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies)
- {
+ void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
Contract.Requires(dt != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
foreach (DatatypeCtor ctor in dt.Ctors) {
@@ -1589,8 +1628,7 @@ namespace Microsoft.Dafny { /// would still work if "dependencies" consisted of one large SCC containing all the inductive
/// datatypes in the module.
/// </summary>
- void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies)
- {
+ void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
@@ -1649,7 +1687,7 @@ namespace Microsoft.Dafny { dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
}
return true;
- NEXT_OUTER_ITERATION: {}
+ NEXT_OUTER_ITERATION: { }
}
// no constructor satisfied the requirements, so this is an illegal datatype declaration
return false;
@@ -1775,8 +1813,7 @@ namespace Microsoft.Dafny { void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter much for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
- if (attrs.Args != null)
- {
+ if (attrs.Args != null) {
ResolveAttributeArgs(attrs.Args, twoState, true);
}
}
@@ -1835,7 +1872,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
- void ResolveFunction(Function f){
+ void ResolveFunction(Function f) {
Contract.Requires(f != null);
Contract.Requires(currentFunction == null);
Contract.Ensures(currentFunction == null);
@@ -1865,8 +1902,7 @@ namespace Microsoft.Dafny { Error(r, "Postcondition must be a boolean (got {0})", r.Type);
}
}
- foreach (Expression r in f.Decreases.Expressions)
- {
+ foreach (Expression r in f.Decreases.Expressions) {
ResolveExpression(r, false);
// any type is fine
}
@@ -1975,8 +2011,7 @@ namespace Microsoft.Dafny { ResolveFrameExpression(fe, "modifies");
}
- foreach (Expression e in m.Decreases.Expressions)
- {
+ foreach (Expression e in m.Decreases.Expressions) {
ResolveExpression(e, false);
// any type is fine
}
@@ -2046,7 +2081,7 @@ namespace Microsoft.Dafny { if (argType.IsSubrangeType) {
Error(tok, "sorry, cannot instantiate collection type with a subrange type");
}
- } else if (type is UserDefinedType) {
+ } else if (type is UserDefinedType) {
UserDefinedType t = (UserDefinedType)type;
foreach (Type tt in t.TypeArgs) {
ResolveType(t.tok, tt, defaultTypeArguments, allowAutoTypeArguments);
@@ -2069,8 +2104,9 @@ namespace Microsoft.Dafny { while (j < t.Path.Count) {
if (sig.FindSubmodule(t.Path[j].val, out sig)) {
j++;
+ sig = GetSignature(sig);
} else {
- Error(t.Path[j], "module {0} does not exist", t.Path[j].val);
+ Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path));
break;
}
}
@@ -2185,7 +2221,7 @@ namespace Microsoft.Dafny { return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
} else if (a is MultiSetType) {
return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
- }else if (a is MapType) {
+ } else if (a is MapType) {
return b is MapType && UnifyTypes(((MapType)a).Domain, ((MapType)b).Domain) && UnifyTypes(((MapType)a).Range, ((MapType)b).Range);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
@@ -2219,7 +2255,7 @@ namespace Microsoft.Dafny { }
}
- bool AssignProxy(TypeProxy proxy, Type t){
+ bool AssignProxy(TypeProxy proxy, Type t) {
Contract.Requires(proxy != null);
Contract.Requires(t != null);
Contract.Requires(proxy.T == null);
@@ -2234,9 +2270,9 @@ namespace Microsoft.Dafny { // it's fine to redirect proxy to t (done below)
} else if (t is UnrestrictedTypeProxy) {
- // merge proxy and t by redirecting t to proxy, rather than the other way around
- ((TypeProxy)t).T = proxy;
- return true;
+ // merge proxy and t by redirecting t to proxy, rather than the other way around
+ ((TypeProxy)t).T = proxy;
+ return true;
} else if (t is RestrictedTypeProxy) {
// Both proxy and t are restricted type proxies. To simplify unification, order proxy and t
@@ -2249,7 +2285,7 @@ namespace Microsoft.Dafny { return AssignRestrictedProxies(r1, r0);
}
- // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
+ // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
if (t.IsIndDatatype) {
// all is fine, proxy can be redirected to t
@@ -2323,8 +2359,8 @@ namespace Microsoft.Dafny { return true;
}
- bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)
- { Contract.Requires(a != null);
+ bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b) {
+ Contract.Requires(a != null);
Contract.Requires(b != null);
Contract.Requires(a != b);
Contract.Requires(a.T == null && b.T == null);
@@ -2466,7 +2502,7 @@ namespace Microsoft.Dafny { // disallowed from a ghost if or while in a non-ghost method, which is not what this says.
Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
- ReturnStmt s = (ReturnStmt) stmt;
+ ReturnStmt s = (ReturnStmt)stmt;
if (s.rhss != null) {
if (method.Outs.Count != s.rhss.Count)
Error(s, "number of return parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, method.Outs.Count);
@@ -2494,8 +2530,7 @@ namespace Microsoft.Dafny { // resolving the update statement will check for return statement specifics.
ResolveStatement(s.hiddenUpdate, specContextOnly, method);
}
- }
- else {// this is a regular return statement.
+ } else {// this is a regular return statement.
s.hiddenUpdate = null;
}
} else if (stmt is ConcreteUpdateStatement) {
@@ -2686,8 +2721,7 @@ namespace Microsoft.Dafny { }
}
- foreach (MaybeFreeExpression inv in s.Invariants)
- {
+ foreach (MaybeFreeExpression inv in s.Invariants) {
ResolveExpression(inv.E, true);
Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(inv.E.Type, Type.Bool)) {
@@ -2695,8 +2729,7 @@ namespace Microsoft.Dafny { }
}
- foreach (Expression e in s.Decreases.Expressions)
- {
+ foreach (Expression e in s.Decreases.Expressions) {
ResolveExpression(e, true);
if (bodyMustBeSpecOnly && e is WildcardExpr) {
Error(e, "'decreases *' is not allowed on ghost loops");
@@ -2705,8 +2738,7 @@ namespace Microsoft.Dafny { }
if (s.Mod.Expressions != null) {
- foreach (FrameExpression fe in s.Mod.Expressions)
- {
+ foreach (FrameExpression fe in s.Mod.Expressions) {
ResolveFrameExpression(fe, "modifies");
}
}
@@ -2717,7 +2749,7 @@ namespace Microsoft.Dafny { }
ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
- loopStack.RemoveAt(loopStack.Count-1); // pop
+ loopStack.RemoveAt(loopStack.Count - 1); // pop
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
@@ -2730,8 +2762,7 @@ namespace Microsoft.Dafny { }
}
- foreach (Expression e in s.Decreases.Expressions)
- {
+ foreach (Expression e in s.Decreases.Expressions) {
ResolveExpression(e, true);
if (s.IsGhost && e is WildcardExpr) {
Error(e, "'decreases *' is not allowed on ghost loops");
@@ -2826,12 +2857,12 @@ namespace Microsoft.Dafny { }
UserDefinedType sourceType = null;
DatatypeDecl dtd = null;
- Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
if (s.Source.Type.IsDatatype) {
sourceType = (UserDefinedType)s.Source.Type;
dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
}
- Dictionary<string,DatatypeCtor> ctors;
+ Dictionary<string, DatatypeCtor> ctors;
if (dtd == null) {
Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);
ctors = null;
@@ -2847,7 +2878,7 @@ namespace Microsoft.Dafny { }
s.IsGhost = bodyIsSpecOnly;
- Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>(); // this is really a set
+ Dictionary<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
foreach (MatchCaseStmt mc in s.Cases) {
DatatypeCtor ctor = null;
if (ctors != null) {
@@ -2914,8 +2945,7 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException();
}
}
- private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, Method method)
- {
+ private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, Method method) {
int prevErrorCount = ErrorCount;
// First, resolve all LHS's and expression-looking RHS's.
SeqSelectExpr arrayRangeLhs = null;
@@ -2948,11 +2978,10 @@ namespace Microsoft.Dafny { foreach (var lhs in s.Lhss) {
if (!(lhs.Resolved is IdentifierExpr)) {
Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
- }
- else {
+ } else {
var ie = (IdentifierExpr)lhs.Resolved;
if (lhsNames.ContainsKey(ie.Name)) {
- // disallow same LHS.
+ // disallow same LHS.
Error(s, "duplicate variable in left-hand side of assign-such-that statement: {0}", ie.Name);
} else {
lhsNames.Add(ie.Name, null);
@@ -3270,8 +3299,7 @@ namespace Microsoft.Dafny { }
}
- void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method)
- {
+ void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method) {
Contract.Requires(blockStmt != null);
Contract.Requires(method != null);
@@ -3485,8 +3513,7 @@ namespace Microsoft.Dafny { return rr.Type;
}
- MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out NonProxyType nptype)
- {
+ MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out NonProxyType nptype) {
Contract.Requires(tok != null);
Contract.Requires(receiverType != null);
Contract.Requires(memberName != null);
@@ -3530,7 +3557,7 @@ namespace Microsoft.Dafny { return null;
}
- public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/,Type/*!*/>/*!*/ subst) {
+ public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/, Type/*!*/>/*!*/ subst) {
Contract.Requires(type != null);
Contract.Requires(cce.NonNullDictionaryAndValues(subst));
Contract.Ensures(Contract.Result<Type>() != null);
@@ -3779,7 +3806,7 @@ namespace Microsoft.Dafny { Error(expr, "a field must be selected via an object, not just a class name");
}
// build the type substitution map
- Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]);
}
@@ -3964,8 +3991,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Lt:
case BinaryExpr.Opcode.Le:
- case BinaryExpr.Opcode.Add:
- {
+ case BinaryExpr.Opcode.Add: {
if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
@@ -3998,8 +4024,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Sub:
case BinaryExpr.Opcode.Mul:
case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- {
+ case BinaryExpr.Opcode.Ge: {
if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
@@ -4077,7 +4102,7 @@ namespace Microsoft.Dafny { ResolveExpression(e.Body, twoState);
if (e.Contract != null) ResolveExpression(e.Contract, twoState);
e.Type = e.Body.Type;
- }else if (expr is QuantifierExpr) {
+ } else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
int prevErrorCount = ErrorCount;
scope.PushMarker();
@@ -4183,7 +4208,7 @@ namespace Microsoft.Dafny { ResolveAttributes(e.Attributes, twoState);
scope.PopMarker();
- expr.Type = new MapType(e.BoundVars[0].Type,e.Term.Type);
+ expr.Type = new MapType(e.BoundVars[0].Type, e.Term.Type);
if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
@@ -4238,12 +4263,12 @@ namespace Microsoft.Dafny { Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
UserDefinedType sourceType = null;
DatatypeDecl dtd = null;
- Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
if (me.Source.Type.IsDatatype) {
sourceType = (UserDefinedType)me.Source.Type;
dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
}
- Dictionary<string,DatatypeCtor> ctors;
+ Dictionary<string, DatatypeCtor> ctors;
IVariable goodMatchVariable = null;
if (dtd == null) {
Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);
@@ -4268,7 +4293,7 @@ namespace Microsoft.Dafny { }
}
- Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>(); // this is really a set
+ Dictionary<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
expr.Type = new InferredTypeProxy();
foreach (MatchCaseExpr mc in me.Cases) {
DatatypeCtor ctor = null;
@@ -4353,7 +4378,7 @@ namespace Microsoft.Dafny { }
// Construct a resolved type directly, as we know the declaration is dt.
dtv.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, dt, gt);
-
+
DatatypeCtor ctor;
if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
Error(dtv.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);
@@ -4384,24 +4409,24 @@ namespace Microsoft.Dafny { Type a = UserDefinedType.ArrayElementType(A);
Type b = UserDefinedType.ArrayElementType(B);
return CouldPossiblyBeSameType(a, b);
- } else
- if (A is UserDefinedType && B is UserDefinedType) {
- UserDefinedType a = (UserDefinedType)A;
- UserDefinedType b = (UserDefinedType)B;
- if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) {
- if (a.TypeArgs.Count != b.TypeArgs.Count) {
- return false; // this probably doesn't happen if the classes are the same.
- }
- for (int i = 0; i < a.TypeArgs.Count; i++) {
- if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
- return false;
+ } else
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
}
- // all parameters could be the same
- return true;
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
}
- // either we don't know what class it is yet, or the classes mismatch
- return false;
- }
return false;
}
private bool CouldPossiblyBeSameType(Type A, Type B) {
@@ -4522,7 +4547,7 @@ namespace Microsoft.Dafny { return;
}
} else if (expr is NamedExpr) {
- if (!moduleInfo.IsGhost)
+ if (!moduleInfo.IsGhost)
CheckIsNonGhost(((NamedExpr)expr).Body);
return;
}
@@ -4584,7 +4609,7 @@ namespace Microsoft.Dafny { }
}
// build the type substitution map
- e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
+ e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
@@ -4635,7 +4660,7 @@ namespace Microsoft.Dafny { // - imported module name
// - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
// - static function or method in the enclosing module.
-
+
Expression r = null; // resolved version of e
CallRhs call = null;
@@ -4653,7 +4678,7 @@ namespace Microsoft.Dafny { } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
- } else if (e.Tokens.Count == 1 && e.Arguments == null) {
+ } else if (e.Tokens.Count == 1 && e.Arguments == null) {
Error(id, "name of type ('{0}') is used as a variable", id.val);
} else if (e.Tokens.Count == 1 && e.Arguments != null) {
Error(id, "name of type ('{0}') is used as a function", id.val);
@@ -4746,6 +4771,7 @@ namespace Microsoft.Dafny { MemberDecl member;
Tuple<DatatypeCtor, bool> pair;
var id = e.Tokens[p];
+ sig = GetSignature(sig);
if (sig.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
@@ -4765,7 +4791,7 @@ namespace Microsoft.Dafny { var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();
r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);
- ResolveDatatypeValue(twoState, (DatatypeValue) r, dt);
+ ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);
if (e.Tokens.Count != p + 2) {
r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);
}
@@ -4777,11 +4803,11 @@ namespace Microsoft.Dafny { Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
} else {
var dt = pair.Item1.EnclosingDatatype;
- var args = (e.Tokens.Count == p+1 ? e.Arguments : null) ?? new List<Expression>();
+ var args = (e.Tokens.Count == p + 1 ? e.Arguments : null) ?? new List<Expression>();
r = new DatatypeValue(id, dt.Name, id.val, args);
ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);
- if (e.Tokens.Count != p+1) {
- r = ResolveSuffix(r, e, p+1, twoState, allowMethodCall, out call);
+ if (e.Tokens.Count != p + 1) {
+ r = ResolveSuffix(r, e, p + 1, twoState, allowMethodCall, out call);
}
}
} else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.
@@ -4809,6 +4835,13 @@ namespace Microsoft.Dafny { return call;
}
+ private ModuleSignature GetSignature(ModuleSignature sig) {
+ if (useCompileSignatures) {
+ while (sig.CompileSignature != null)
+ sig = sig.CompileSignature;
+ }
+ return sig;
+ }
/// <summary>
/// Given resolved expression "r" and unresolved expressions e.Tokens[p..] and e.Arguments.
/// Returns a resolved version of the expression:
@@ -5004,8 +5037,7 @@ namespace Microsoft.Dafny { /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
/// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.
/// </summary>
- int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)
- {
+ int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
Contract.Requires(boundVars != null);
@@ -5256,7 +5288,7 @@ namespace Microsoft.Dafny { var e = (IdentifierExpr)expr;
return new HashSet<IVariable>() { e.Var };
- } else if (expr is QuantifierExpr) {
+ } else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
var s = FreeVariables(e.LogicalBody());
foreach (var bv in e.BoundVars) {
@@ -5290,8 +5322,7 @@ namespace Microsoft.Dafny { }
}
- void ResolveReceiver(Expression expr, bool twoState)
- {
+ void ResolveReceiver(Expression expr, bool twoState) {
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
Contract.Ensures(expr.Type != null);
@@ -5317,7 +5348,7 @@ namespace Microsoft.Dafny { Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
Type domainType = new InferredTypeProxy();
-
+
IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);
if (!UnifyTypes(e.Seq.Type, expectedType)) {
Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);
@@ -5366,10 +5397,10 @@ namespace Microsoft.Dafny { BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) {
Contract.Requires(operandType != null);
switch (op) {
- case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff;
- case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp;
- case BinaryExpr.Opcode.And: return BinaryExpr.ResolvedOpcode.And;
- case BinaryExpr.Opcode.Or: return BinaryExpr.ResolvedOpcode.Or;
+ case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff;
+ case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp;
+ case BinaryExpr.Opcode.And: return BinaryExpr.ResolvedOpcode.And;
+ case BinaryExpr.Opcode.Or: return BinaryExpr.ResolvedOpcode.Or;
case BinaryExpr.Opcode.Eq:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetEq;
@@ -5397,7 +5428,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Disjoint:
if (operandType is MultiSetType) {
return BinaryExpr.ResolvedOpcode.MultiSetDisjoint;
- } else if(operandType is MapType) {
+ } else if (operandType is MapType) {
return BinaryExpr.ResolvedOpcode.MapDisjoint;
} else {
return BinaryExpr.ResolvedOpcode.Disjoint;
@@ -5490,8 +5521,8 @@ namespace Microsoft.Dafny { } else {
return BinaryExpr.ResolvedOpcode.NotInSeq;
}
- case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
- case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod;
+ case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
+ case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator
}
@@ -5502,8 +5533,7 @@ namespace Microsoft.Dafny { /// that is allowed only in specification contexts.
/// Requires 'expr' to be a successfully resolved expression.
/// </summary>
- bool UsesSpecFeatures(Expression expr)
- {
+ bool UsesSpecFeatures(Expression expr) {
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
@@ -5561,8 +5591,8 @@ namespace Microsoft.Dafny { return true;
}
return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);
- } else if (expr is NamedExpr) {
- return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
+ } else if (expr is NamedExpr) {
+ return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
} else if (expr is ComprehensionExpr) {
if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {
return true; // the quantifier cannot be compiled if the resolver found no bounds
@@ -5708,7 +5738,7 @@ namespace Microsoft.Dafny { // this call is disqualified from being a co-call, because of side effects
if (!dealsWithCodatatypes) {
e.CoCall = FunctionCallExpr.CoCallResolution.No;
- } else if (coContext != null) {
+ } else if (coContext != null) {
e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects;
} else {
e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
@@ -5776,12 +5806,14 @@ namespace Microsoft.Dafny { }
}
- class Scope<Thing> where Thing : class {
- [Rep] readonly List<string> names = new List<string>(); // a null means a marker
- [Rep] readonly List<Thing> things = new List<Thing>();
+ class Scope<Thing> where Thing : class
+ {
+ [Rep]
+ readonly List<string> names = new List<string>(); // a null means a marker
+ [Rep]
+ readonly List<Thing> things = new List<Thing>();
[ContractInvariantMethod]
- void ObjectInvariant()
- {
+ void ObjectInvariant() {
Contract.Invariant(names != null);
Contract.Invariant(things != null);
Contract.Invariant(names.Count == things.Count);
@@ -5792,8 +5824,8 @@ namespace Microsoft.Dafny { public bool AllowInstance {
get { return scopeSizeWhereInstancesWereDisallowed == -1; }
- set
- {Contract.Requires(AllowInstance && !value); // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction
+ set {
+ Contract.Requires(AllowInstance && !value); // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction
scopeSizeWhereInstancesWereDisallowed = names.Count;
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 41a42319..cfa79f1a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1917,5 +1917,5 @@ Execution trace: Dafny program verifier finished with 19 verified, 2 errors
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 23 verified, 0 errors
Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index bf21432f..fe6eda47 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -57,3 +57,55 @@ module CoRecursion { }
}
}
+
+ghost module S {
+ class C {
+ var f: int;
+ method m()
+ }
+}
+
+module T refines S {
+ class C {
+ method m() {
+ print "in T.C.m()";
+ }
+ }
+}
+module A {
+ module X as S = T;
+ module Y as S = T;
+ module Z = T;
+ static method run() {
+ var x := new X.C;
+ x.m();
+ var y := new Y.C;
+ y.m();
+ var z := new Z.C;
+ z.m();
+ }
+}
+
+method NotMain() {
+ A.run();
+}
+
+
+ghost module S1 {
+ module B as S = T;
+ static method do()
+}
+
+module T1 refines S1 {
+ static method do() {
+ var x := 3;
+ }
+}
+module A1 {
+ module X as S1 = T1;
+ static method run() {
+ X.do();
+ var x := new X.B.C;
+ x.m();
+ }
+}
|