From d47400c8a1ba72497cc145173aa6ad9f6b1b5a85 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 23 Feb 2014 17:27:26 -0800 Subject: Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma") --- Source/Dafny/Resolver.cs | 166 +++++++++++++++++++++++------------------------ 1 file changed, 83 insertions(+), 83 deletions(-) (limited to 'Source/Dafny/Resolver.cs') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 564e4164..2262c4da 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -354,22 +354,22 @@ namespace Microsoft.Dafny foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) { ICallable m; string s; - if (clbl is CoMethod) { - var prefixMethod = ((CoMethod)clbl).PrefixMethod; - m = prefixMethod; - s = prefixMethod.Name + " "; + if (clbl is CoLemma) { + var prefixLemma = ((CoLemma)clbl).PrefixLemma; + m = prefixLemma; + s = prefixLemma.Name + " "; } else { m = clbl; s = ""; } FillInDefaultDecreases(m); - if (m.InferredDecreases || m is PrefixMethod) { + if (m.InferredDecreases || m is PrefixLemma) { bool showIt = false; if (m is Function) { // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive showIt = ((Function)m).IsRecursive; - } else if (m is PrefixMethod) { + } else if (m is PrefixLemma) { // always show the decrease clause, since at the very least it will start with "_k", which the programmer did not write explicitly showIt = true; } else { @@ -386,7 +386,7 @@ namespace Microsoft.Dafny } s += ";"; // always terminate with a semi-colon, even in the case of an empty decreases clause // Note, in the following line, we use the location information for "clbl", not "m". These - // are the same, except in the case where "clbl" is a CoMethod and "m" is a prefix method. + // are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma. ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length); } } @@ -402,7 +402,7 @@ namespace Microsoft.Dafny return; } var decr = clbl.Decreases.Expressions; - if (decr.Count == 0 || (clbl is PrefixMethod && decr.Count == 1)) { + if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) { // The default for a function starts with the function's reads clause, if any if (clbl is Function) { var fn = (Function)clbl; @@ -853,7 +853,7 @@ namespace Microsoft.Dafny foreach (MemberDecl m in cl.Members) { if (!members.ContainsKey(m.Name)) { members.Add(m.Name, m); - if (m is CoPredicate || m is CoMethod) { + if (m is CoPredicate || m is CoLemma) { var extraName = m.Name + "#"; MemberDecl extraMember; var cloner = new Cloner(); @@ -873,24 +873,24 @@ namespace Microsoft.Dafny // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles. moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop); } else { - var com = (CoMethod)m; + var com = (CoLemma)m; // _k has already been added to 'formals', so append the original formals formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal)); // prepend _k to the given decreases clause var decr = new List(); decr.Add(new IdentifierExpr(com.tok, k.Name)); decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr)); - // Create prefix method. Note that the body is not cloned, but simply shared. - com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic, + // Create prefix lemma. Note that the body is not cloned, but simply shared. + com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.IsStatic, com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal), com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod), - new List(), // Note, the postconditions are filled in after the comethod's postconditions have been resolved + new List(), // Note, the postconditions are filled in after the colemma's postconditions have been resolved new Specification(decr, null), - null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known + null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the colemma is known cloner.CloneAttributes(com.Attributes), com); - extraMember = com.PrefixMethod; + extraMember = com.PrefixLemma; // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles. - moduleDef.CallGraph.AddEdge(com.PrefixMethod, com); + moduleDef.CallGraph.AddEdge(com.PrefixLemma, com); } members.Add(extraName, extraMember); } @@ -1119,8 +1119,8 @@ namespace Microsoft.Dafny if (m is Constructor) { return new Constructor(m.tok, m.Name, tps, ins, req, mod, ens, decreases, null, null, null); - } else if (m is CoMethod) { - return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), + } else if (m is CoLemma) { + return new CoLemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, null); } else if (m is Lemma) { return new Lemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), @@ -1414,40 +1414,40 @@ namespace Microsoft.Dafny } if (ErrorCount == prevErrorCount) { - // fill in the postconditions and bodies of prefix methods - foreach (var com in ModuleDefinition.AllCoMethods(declarations)) { - var prefixMethod = com.PrefixMethod; - if (prefixMethod == null) { - continue; // something went wrong during registration of the prefix method (probably a duplicated comethod name) - } - Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null); // there are not supposed have have been filled in before - // compute the postconditions of the prefix method - var k = prefixMethod.Ins[0]; + // fill in the postconditions and bodies of prefix lemmas + foreach (var com in ModuleDefinition.AllCoLemmas(declarations)) { + var prefixLemma = com.PrefixLemma; + if (prefixLemma == null) { + continue; // something went wrong during registration of the prefix lemma (probably a duplicated colemma name) + } + Contract.Assume(prefixLemma.Ens.Count == 0 && prefixLemma.Body == null); // there are not supposed have have been filled in before + // compute the postconditions of the prefix lemma + var k = prefixLemma.Ins[0]; foreach (var p in com.Ens) { var coConclusions = new HashSet(); - CheckCoMethodConclusions(p.E, true, coConclusions); - var subst = new CoMethodPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this); + CheckCoLemmaConclusions(p.E, true, coConclusions); + var subst = new CoLemmaPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this); var post = subst.CloneExpr(p.E); - prefixMethod.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); + prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); } - // Compute the statement body of the prefix method + // Compute the statement body of the prefix lemma if (com.Body != null) { var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1)); - var subst = new CoMethodBodyCloner(com, kMinusOne, this); + var subst = new CoLemmaBodyCloner(com, kMinusOne, this); var mainBody = subst.CloneBlockStmt(com.Body); var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name)); var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null); - prefixMethod.Body = new BlockStmt(com.tok, condBody.EndTok, new List() { condBody }); + prefixLemma.Body = new BlockStmt(com.tok, condBody.EndTok, new List() { condBody }); } - // The prefix method now has all its components, so it's finally time we resolve it - currentClass = (ClassDecl)prefixMethod.EnclosingClass; + // The prefix lemma now has all its components, so it's finally time we resolve it + currentClass = (ClassDecl)prefixLemma.EnclosingClass; allTypeParameters.PushMarker(); ResolveTypeParameters(currentClass.TypeArgs, false, currentClass); - ResolveTypeParameters(prefixMethod.TypeArgs, false, prefixMethod); - ResolveMethod(prefixMethod); + ResolveTypeParameters(prefixLemma.TypeArgs, false, prefixLemma); + ResolveMethod(prefixLemma); allTypeParameters.PopMarker(); currentClass = null; - CheckTypeInference_Member(prefixMethod); + CheckTypeInference_Member(prefixLemma); } } @@ -1666,7 +1666,7 @@ namespace Microsoft.Dafny } } // Check that copredicates are not recursive with non-copredicate functions, and - // check that comethods are not recursive with non-comethod methods. + // check that colemmas are not recursive with non-colemma methods. foreach (var d in declarations) { if (d is ClassDecl) { foreach (var member in ((ClassDecl)d).Members) { @@ -1684,10 +1684,10 @@ namespace Microsoft.Dafny if (fn.Body != null) { CoPredicateChecks(fn.Body, fn, CallingPosition.Positive); } - } else if (member is CoMethod) { - var m = (CoMethod)member; + } else if (member is CoLemma) { + var m = (CoLemma)member; if (m.Body != null) { - CoMethodChecks(m.Body, m); + CoLemmaChecks(m.Body, m); } } } @@ -2160,13 +2160,13 @@ namespace Microsoft.Dafny #endregion CoPredicateChecks // ------------------------------------------------------------------------------------------------------ - // ----- CoMethodChecks --------------------------------------------------------------------------------- + // ----- CoLemmaChecks ---------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ - #region CoMethodChecks - class CoMethodChecks_Visitor : ResolverBottomUpVisitor + #region CoLemmaChecks + class CoLemmaChecks_Visitor : ResolverBottomUpVisitor { - CoMethod context; - public CoMethodChecks_Visitor(Resolver resolver, CoMethod context) + CoLemma context; + public CoLemmaChecks_Visitor(Resolver resolver, CoLemma context) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(context != null); @@ -2175,15 +2175,15 @@ namespace Microsoft.Dafny protected override void VisitOneStmt(Statement stmt) { if (stmt is CallStmt) { var s = (CallStmt)stmt; - if (s.Method is CoMethod || s.Method is PrefixMethod) { + if (s.Method is CoLemma || s.Method is PrefixLemma) { // all is cool } else { - // the call goes from a comethod context to a non-comethod callee + // the call goes from a colemma context to a non-colemma callee var moduleCaller = context.EnclosingClass.Module; var moduleCallee = s.Method.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { - // we're looking at a recursive call (to a non-comethod) - Error(s.Tok, "a recursive call from a comethod can go only to other comethods and prefix methods"); + // we're looking at a recursive call (to a non-colemma) + Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } @@ -2192,23 +2192,23 @@ namespace Microsoft.Dafny { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; - // the call goes from a comethod context to a non-comethod callee + // the call goes from a colemma context to a non-colemma callee var moduleCaller = context.EnclosingClass.Module; var moduleCallee = e.Function.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) { - // we're looking at a recursive call (to a non-comethod) - Error(e.tok, "a recursive call from a comethod can go only to other comethods and prefix methods"); + // we're looking at a recursive call (to a non-colemma) + Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } } - void CoMethodChecks(Statement stmt, CoMethod context) { + void CoLemmaChecks(Statement stmt, CoLemma context) { Contract.Requires(stmt != null); Contract.Requires(context != null); - var v = new CoMethodChecks_Visitor(this, context); + var v = new CoLemmaChecks_Visitor(this, context); v.Visit(stmt); } - #endregion CoMethodChecks + #endregion CoLemmaChecks // ------------------------------------------------------------------------------------------------------ // ----- CheckEqualityTypes ----------------------------------------------------------------------------- @@ -2582,10 +2582,10 @@ namespace Microsoft.Dafny ResolveTypeParameters(m.TypeArgs, true, m); ResolveMethodSignature(m); allTypeParameters.PopMarker(); - var com = m as CoMethod; - if (com != null && com.PrefixMethod != null && ec == ErrorCount) { - var mm = com.PrefixMethod; - // resolve signature of the prefix method + var com = m as CoLemma; + if (com != null && com.PrefixLemma != null && ec == ErrorCount) { + var mm = com.PrefixLemma; + // resolve signature of the prefix lemma mm.EnclosingClass = cl; allTypeParameters.PushMarker(); ResolveTypeParameters(mm.TypeArgs, true, mm); @@ -3091,8 +3091,8 @@ namespace Microsoft.Dafny ResolveFrameExpression(fe, "modifies", m); if (m is Lemma) { Error(fe.tok, "lemmas are not allowed to have modifies clauses"); - } else if (m is CoMethod) { - Error(fe.tok, "comethods are not allowed to have modifies clauses"); + } else if (m is CoLemma) { + Error(fe.tok, "colemmas are not allowed to have modifies clauses"); } } foreach (Expression e in m.Decreases.Expressions) { @@ -3106,8 +3106,8 @@ namespace Microsoft.Dafny // Add out-parameters to a new scope that will also include the outermost-level locals of the body // Don't care about any duplication errors among the out-parameters, since they have already been reported scope.PushMarker(); - if (m is CoMethod && m.Outs.Count != 0) { - Error(m.Outs[0].tok, "comethods are not allowed to have out-parameters"); + if (m is CoLemma && m.Outs.Count != 0) { + Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters"); } else { foreach (Formal p in m.Outs) { scope.Push(p.Name, p); @@ -3125,18 +3125,18 @@ namespace Microsoft.Dafny // Resolve body if (m.Body != null) { - var com = m as CoMethod; - if (com != null && com.PrefixMethod != null) { + var com = m as CoLemma; + if (com != null && com.PrefixLemma != null) { // The body may mentioned the implicitly declared parameter _k. Throw it into the // scope before resolving the body. - var k = com.PrefixMethod.Ins[0]; + var k = com.PrefixLemma.Ins[0]; scope.Push(k.Name, k); // we expect no name conflict for _k } var codeContext = m; ResolveBlockStatement(m.Body, m.IsGhost, codeContext); } - // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods) + // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas) ResolveAttributes(m.Attributes, false, m); scope.PopMarker(); // for the out-parameters and outermost-level locals @@ -7735,35 +7735,35 @@ namespace Microsoft.Dafny /// /// This method adds to "coConclusions" all copredicate calls and codatatype equalities that occur /// in positive positions and not under existential quantification. If "expr" is the postcondition - /// of a comethod, then the "coConclusions" are the subexpressions that need to be replaced in order - /// to create the postcondition of the corresponding prefix method. + /// of a colemma, then the "coConclusions" are the subexpressions that need to be replaced in order + /// to create the postcondition of the corresponding prefix lemma. /// - void CheckCoMethodConclusions(Expression expr, bool position, ISet coConclusions) { + void CheckCoLemmaConclusions(Expression expr, bool position, ISet coConclusions) { Contract.Requires(expr != null); if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - CheckCoMethodConclusions(e.ResolvedExpression, position, coConclusions); + CheckCoLemmaConclusions(e.ResolvedExpression, position, coConclusions); } else if (expr is LetExpr) { var e = (LetExpr)expr; // For simplicity, only look in the body of the let expression, that is, ignoring the RHS of the // binding and ignoring what that binding would expand to in the body. - CheckCoMethodConclusions(e.Body, position, coConclusions); + CheckCoLemmaConclusions(e.Body, position, coConclusions); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; if (e.Op == UnaryExpr.Opcode.Not) { - CheckCoMethodConclusions(e.E, !position, coConclusions); + CheckCoLemmaConclusions(e.E, !position, coConclusions); } } else if (expr is BinaryExpr) { var bin = (BinaryExpr)expr; if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And || bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) { - CheckCoMethodConclusions(bin.E0, position, coConclusions); - CheckCoMethodConclusions(bin.E1, position, coConclusions); + CheckCoLemmaConclusions(bin.E0, position, coConclusions); + CheckCoLemmaConclusions(bin.E1, position, coConclusions); } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) { - CheckCoMethodConclusions(bin.E0, !position, coConclusions); - CheckCoMethodConclusions(bin.E1, position, coConclusions); + CheckCoLemmaConclusions(bin.E0, !position, coConclusions); + CheckCoLemmaConclusions(bin.E1, position, coConclusions); } else if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) { coConclusions.Add(bin); } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon && bin.E0.Type.IsCoDatatype) { @@ -7772,16 +7772,16 @@ namespace Microsoft.Dafny } else if (expr is ITEExpr) { var ite = (ITEExpr)expr; - CheckCoMethodConclusions(ite.Thn, position, coConclusions); - CheckCoMethodConclusions(ite.Els, position, coConclusions); + CheckCoLemmaConclusions(ite.Thn, position, coConclusions); + CheckCoLemmaConclusions(ite.Els, position, coConclusions); } else if (expr is StmtExpr) { var e = (StmtExpr)expr; - CheckCoMethodConclusions(e.E, position, coConclusions); + CheckCoLemmaConclusions(e.E, position, coConclusions); } else if (expr is OldExpr) { var e = (OldExpr)expr; - CheckCoMethodConclusions(e.E, position, coConclusions); + CheckCoLemmaConclusions(e.E, position, coConclusions); } else if (expr is FunctionCallExpr && position) { var fexp = (FunctionCallExpr)expr; -- cgit v1.2.3