From db9821ac440cdfa817049ab83c2e94f861ff429d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 17 Aug 2015 09:37:47 -0700 Subject: Review preceding commit with Rustan --- Source/Dafny/Cloner.cs | 9 ++------- Source/Dafny/Compiler.cs | 7 ++----- Source/Dafny/DafnyAst.cs | 23 +++++++++-------------- Source/Dafny/Printer.cs | 3 +-- Source/Dafny/Translator.cs | 1 + 5 files changed, 15 insertions(+), 28 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 961d4d14..e89a385f 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -374,18 +374,13 @@ namespace Microsoft.Dafny if (e is QuantifierExpr) { var q = (QuantifierExpr)e; var tvs = q.TypeArgs.ConvertAll(CloneTypeParam); - QuantifierExpr cloned; if (e is ForallExpr) { - cloned = new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + return new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); } else if (e is ExistsExpr) { - cloned = new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + return new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected quantifier expression } - if (q.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Should we clone the quantifier as a quantifier in this case? Or should we just replace entirely? - cloned.SplitQuantifier = q.SplitQuantifier.Select(CloneExpr).ToList(); - } - return cloned; } else if (e is MapComprehension) { return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term, CloneAttributes(e.Attributes)); } else if (e is LambdaExpr) { diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d19d2bed..c969ac1f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -2817,10 +2817,7 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; - if (e.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Do we compile a split quantifier in its original form, or in its split form? - TrExpr(e.SplitQuantifierExpression); - return; - } + // Compilation does not check whether a quantifier was split. Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds var n = e.BoundVars.Count; @@ -2864,7 +2861,7 @@ namespace Microsoft.Dafny { wr.Write("{0}, ", expr is ForallExpr ? "true" : "false"); wr.Write("@{0} => ", bv.CompileName); } - TrExpr(e.LogicalBody()); + TrExpr(e.LogicalBody(true)); for (int i = 0; i < n; i++) { wr.Write(")"); } diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 05548f38..a902a18c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1552,11 +1552,6 @@ namespace Microsoft.Dafny { set { Contract.Requires(Parent == null); // set it only once Contract.Requires(value != null); - // BUGBUG: The following line is a workaround to tell the verifier that 'value' is not of an Immutable type. - // A proper solution would be to be able to express that in the program (in a specification or attribute) or - // to be able to declare 'parent' as [PeerOrImmutable]. - Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor || (value is QuantifierExpr && ((QuantifierExpr)value).SplitQuantifier == null)); - //modifies parent; parent = value; } } @@ -6816,8 +6811,7 @@ namespace Microsoft.Dafny { Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any()); Expression accumulator = SplitQuantifier[0]; for (int tid = 1; tid < SplitQuantifier.Count; tid++) { - var newAcc = new BinaryExpr(Term.tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]); - accumulator = newAcc; + accumulator = new BinaryExpr(Term.tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]); } return accumulator; } @@ -6835,7 +6829,11 @@ namespace Microsoft.Dafny { internal Expression SplitQuantifierExpression { get; private set; } - public abstract Expression LogicalBody(); + public virtual Expression LogicalBody(bool bypassSplitQuantifier = false) { + // Don't call this on a quantifier with a Split clause: it's not a real quantifier. The only exception is the Compiler. + Contract.Requires(bypassSplitQuantifier || SplitQuantifier == null); + throw new cce.UnreachableException(); // This body is just here for the "Requires" clause + } public override IEnumerable SubExpressions { get { @@ -6847,9 +6845,8 @@ namespace Microsoft.Dafny { } } } - + public class ForallExpr : QuantifierExpr { - protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.And; } } protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.And; } } public ForallExpr(IToken tok, List bvars, Expression range, Expression term, Attributes attrs) @@ -6864,8 +6861,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null); Contract.Requires(term != null); } - public override Expression LogicalBody() { - Contract.Assert(SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + public override Expression LogicalBody(bool bypassSplitQuantifier = false) { if (Range == null) { return Term; } @@ -6877,7 +6873,6 @@ namespace Microsoft.Dafny { } public class ExistsExpr : QuantifierExpr { - protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.Or; } } protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } } public ExistsExpr(IToken tok, List bvars, Expression range, Expression term, Attributes attrs) @@ -6892,7 +6887,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null); Contract.Requires(term != null); } - public override Expression LogicalBody() { + public override Expression LogicalBody(bool bypassSplitQuantifier = false) { if (Range == null) { return Term; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 43b69bbb..7c684fde 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1730,8 +1730,7 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; - if (e.SplitQuantifier != null) { - // CLEMENT TODO TRIGGERS: Should (do) we have a setting to print the original forms instead of rewritten forms? + if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) { PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count); return; } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index f0b7f276..df816b6d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5306,6 +5306,7 @@ namespace Microsoft.Dafny { if (q != null && q.SplitQuantifier != null) { CheckWellformedWithResult(q.SplitQuantifierExpression, options, result, resultType, locals, builder, etran); + return; } var typeMap = new Dictionary(); -- cgit v1.2.3