From a07b43ac03b38d4af575d1a1df48339ad228751a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 14 Aug 2015 17:38:08 -0700 Subject: Start committing split quantifiers This requires rewriting the parts of the AST that contain these quantifiers. We unfortunately don't have facilities to do such rewrites at the moment (and there are loops in the AST, so it would be hard to write such a facility). As a workaround, this commit introduces a field in quantifier expressions, SplitQuantifiers. Code that manipulate triggers is expected to look for this field, and ignore the other fields if that one is found. --- Source/Dafny/Cloner.cs | 10 ++- Source/Dafny/Compiler.cs | 6 ++ Source/Dafny/DafnyAst.cs | 54 +++++++++++- Source/Dafny/Printer.cs | 7 ++ Source/Dafny/Resolver.cs | 16 +++- Source/Dafny/Rewriter.cs | 4 +- Source/Dafny/Translator.cs | 125 +++++++++++++++++----------- Source/Dafny/Triggers/QuantifierSplitter.cs | 26 ++++-- Source/Dafny/Triggers/TriggerExtensions.cs | 8 ++ Source/Dafny/Triggers/TriggerGenerator.cs | 10 ++- Source/Dafny/Triggers/TriggerUtils.cs | 1 + Source/Dafny/Triggers/TriggersCollector.cs | 5 +- 12 files changed, 203 insertions(+), 69 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 323abc70..961d4d14 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -4,6 +4,7 @@ using System.Collections.Generic; using System.Numerics; using System.Diagnostics.Contracts; using IToken = Microsoft.Boogie.IToken; +using System.Linq; namespace Microsoft.Dafny { @@ -373,13 +374,18 @@ namespace Microsoft.Dafny if (e is QuantifierExpr) { var q = (QuantifierExpr)e; var tvs = q.TypeArgs.ConvertAll(CloneTypeParam); + QuantifierExpr cloned; if (e is ForallExpr) { - return new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + cloned = new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); } else if (e is ExistsExpr) { - return new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + cloned = 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 4fdd34f6..d19d2bed 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -2816,6 +2816,12 @@ 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; + } + Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds var n = e.BoundVars.Count; Contract.Assert(e.Bounds.Count == n); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index efe94c66..05548f38 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1555,7 +1555,7 @@ namespace Microsoft.Dafny { // 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); + 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; } @@ -6552,6 +6552,15 @@ namespace Microsoft.Dafny { } } + /// + /// Returns a resolved binary expression + /// + public BinaryExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) + : this(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1) { + ResolvedOp = rop; + Type = Type.Bool; + } + public override IEnumerable SubExpressions { get { yield return E0; @@ -6770,6 +6779,8 @@ namespace Microsoft.Dafny { public List TypeArgs; private static int currentQuantId = -1; + protected abstract BinaryExpr.ResolvedOpcode SplitResolvedOp { get; } + static int FreshQuantId() { return System.Threading.Interlocked.Increment(ref currentQuantId); } @@ -6800,10 +6811,47 @@ namespace Microsoft.Dafny { this.TypeArgs = tvars; this.UniqueId = FreshQuantId(); } + + private Expression SplitQuantifierToExpression() { + 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; + } + return accumulator; + } + + private List _SplitQuantifier; + public List SplitQuantifier { + get { + return _SplitQuantifier; + } + set { + _SplitQuantifier = value; + SplitQuantifierExpression = SplitQuantifierToExpression(); + } + } + + internal Expression SplitQuantifierExpression { get; private set; } + public abstract Expression LogicalBody(); + + public override IEnumerable SubExpressions { + get { + if (SplitQuantifier == null) { + return base.SubExpressions; + } else { + return SplitQuantifier; + } + } + } } 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) : this(tok, new List(), bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); @@ -6817,6 +6865,7 @@ namespace Microsoft.Dafny { 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 if (Range == null) { return Term; } @@ -6828,6 +6877,9 @@ 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) : this(tok, new List(), bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1c7508eb..43b69bbb 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1729,6 +1729,13 @@ 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? + PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count); + return; + } + bool parensNeeded = !isRightmost; if (parensNeeded) { wr.Write("("); } wr.Write(e is ForallExpr ? "forall" : "exists"); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7bf085f9..e1c3c63b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -305,7 +305,7 @@ namespace Microsoft.Dafny Contract.Assert(!useCompileSignatures); useCompileSignatures = true; // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature var oldErrorsOnly = reporter.ErrorsOnly; - reporter.ErrorsOnly = true; // turn off warning reporting for the clone + reporter.ErrorsOnly = true; // turn off warning reporter for the clone var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile"); var compileSig = RegisterTopLevelDecls(nw, true); compileSig.Refines = refinementTransformer.RefinedSig; @@ -338,7 +338,7 @@ namespace Microsoft.Dafny if (refinementTransformer.CheckIsRefinement(compileSig, p)) { abs.Signature.CompileSignature = compileSig; } else { - reporter.Error(MessageSource.Resolver, + reporter.Error(MessageSource.Resolver, abs.CompilePath[0], "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val)); @@ -2438,6 +2438,7 @@ namespace Microsoft.Dafny return false; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution var cpos = IsCoContext ? cp : Invert(cp); if ((cpos == CallingPosition.Positive && e is ExistsExpr) || (cpos == CallingPosition.Negative && e is ForallExpr)) { if (e.MissingBounds != null && e.MissingBounds.Count != 0) { @@ -6962,7 +6963,7 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, expr, "'this' is not allowed in a 'static' context"); } if (currentClass != null) { - expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporting + expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporter } } else if (expr is IdentifierExpr) { @@ -7605,6 +7606,7 @@ namespace Microsoft.Dafny e.Type = e.Body.Type; } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution int prevErrorCount = reporter.Count(ErrorLevel.Error); bool _val = true; bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val; @@ -9177,6 +9179,7 @@ namespace Microsoft.Dafny return; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution if (e.MissingBounds != null) { foreach (var bv in e.MissingBounds) { reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); @@ -9774,10 +9777,13 @@ namespace Microsoft.Dafny if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; + return new HashSet() { e.Var }; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution + var s = FreeVariables(e.LogicalBody()); foreach (var bv in e.BoundVars) { s.Remove(bv); @@ -10139,7 +10145,9 @@ namespace Microsoft.Dafny } 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) { + var q = expr as QuantifierExpr; + Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution + if (q != null && q.Bounds == null) { return true; // the quantifier cannot be compiled if the resolver found no bounds } return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se)); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 0798510a..2c00e203 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -43,9 +43,9 @@ namespace Microsoft.Dafny Contract.Requires(reporter != null); } - internal override void PostResolve(ModuleDefinition m) { + internal override void PostCyclicityResolve(ModuleDefinition m) { var finder = new Triggers.QuantifierCollectionsFinder(reporter); - + foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Function) { var function = (Function)decl; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 14fca463..f0b7f276 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4465,6 +4465,11 @@ namespace Microsoft.Dafny { var e = (ComprehensionExpr)expr; var canCall = CanCallAssumption(e.Term, etran); var q = e as QuantifierExpr; + + if (q != null && q.SplitQuantifier != null) { + return CanCallAssumption(q.SplitQuantifierExpression, etran); + } + var tyvars = MkTyParamBinders(q != null ? q.TypeArgs : new List()); if (e.Range != null) { canCall = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), canCall)); @@ -4758,6 +4763,12 @@ namespace Microsoft.Dafny { // If the quantifier is universal, then continue as: // assume (\forall x :: body(x)); // Create local variables corresponding to the type arguments: + + if (e.SplitQuantifier != null) { + CheckWellformedAndAssume(e.SplitQuantifierExpression, options, locals, builder, etran); + return; + } + var typeArgumentCopies = Map(e.TypeArgs, tp => e.Refresh(tp, CurrentIdGenerator)); var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp))); var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty))); @@ -5293,6 +5304,10 @@ namespace Microsoft.Dafny { var q = e as QuantifierExpr; var lam = e as LambdaExpr; + if (q != null && q.SplitQuantifier != null) { + CheckWellformedWithResult(q.SplitQuantifierExpression, options, result, resultType, locals, builder, etran); + } + var typeMap = new Dictionary(); var copies = new List(); if (q != null) { @@ -11534,56 +11549,60 @@ namespace Microsoft.Dafny { return TrExpr(((NamedExpr)expr).Body); } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; - List tyvars = translator.MkTyParamBinders(e.TypeArgs); - List bvars = new List(); - - var initEtran = this; - var bodyEtran = this; - bool _scratch = true; - Bpl.Expr antecedent = Bpl.Expr.True; - - if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) { - // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body - var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars); - bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits); - } - if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) { - var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars); - bodyEtran = new ExpressionTranslator(bodyEtran, h); - antecedent = BplAnd(new List { - antecedent, - translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h), - translator.HeapSameOrSucc(initEtran.HeapExpr, h) - }); - } + if (e.SplitQuantifier != null) { + return TrExpr(e.SplitQuantifierExpression); + } else { + List tyvars = translator.MkTyParamBinders(e.TypeArgs); + List bvars = new List(); + + var initEtran = this; + var bodyEtran = this; + bool _scratch = true; + + Bpl.Expr antecedent = Bpl.Expr.True; + + if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) { + // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body + var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars); + bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits); + } + if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) { + var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars); + bodyEtran = new ExpressionTranslator(bodyEtran, h); + antecedent = BplAnd(new List { + antecedent, + translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h), + translator.HeapSameOrSucc(initEtran.HeapExpr, h) + }); + } - antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); + antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); - Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); - Bpl.Trigger tr = null; - var argsEtran = bodyEtran.WithNoLits(); - foreach (var aa in e.Attributes.AsEnumerable()) { - if (aa.Name == "trigger") { - List tt = new List(); - foreach (var arg in aa.Args) { - tt.Add(argsEtran.TrExpr(arg)); + Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); + Bpl.Trigger tr = null; + var argsEtran = bodyEtran.WithNoLits(); + foreach (var aa in e.Attributes.AsEnumerable()) { + if (aa.Name == "trigger") { + List tt = new List(); + foreach (var arg in aa.Args) { + tt.Add(argsEtran.TrExpr(arg)); + } + tr = new Bpl.Trigger(expr.tok, true, tt, tr); } - tr = new Bpl.Trigger(expr.tok, true, tt, tr); } - } - if (e.Range != null) { - antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); - } - Bpl.Expr body = bodyEtran.TrExpr(e.Term); + if (e.Range != null) { + antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); + } + Bpl.Expr body = bodyEtran.TrExpr(e.Term); - if (e is ForallExpr) { - return new Bpl.ForallExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body)); - } else { - Contract.Assert(e is ExistsExpr); - return new Bpl.ExistsExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body)); + if (e is ForallExpr) { + return new Bpl.ForallExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body)); + } else { + Contract.Assert(e is ExistsExpr); + return new Bpl.ExistsExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body)); + } } - } else if (expr is SetComprehension) { var e = (SetComprehension)expr; // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))". @@ -12966,9 +12985,11 @@ namespace Microsoft.Dafny { } } + } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) { + return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran); } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) - /* NB: only for type arg less quantifiers for now: */ - && ((QuantifierExpr)expr).TypeArgs.Count == 0) { + /* NB: only for type arg less quantifiers for now: */ + && ((QuantifierExpr)expr).TypeArgs.Count == 0) { var e = (QuantifierExpr)expr; var inductionVariables = ApplyInduction(e); if (apply_induction && 2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) { @@ -13138,8 +13159,11 @@ namespace Microsoft.Dafny { protected override void VisitOneExpr(Expression expr) { if (expr is QuantifierExpr) { - foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) { - collector.Visit(trigger); + var e = (QuantifierExpr)expr; + if (e.SplitQuantifier == null) { + foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) { + collector.Visit(trigger); + } } } } @@ -13173,6 +13197,7 @@ namespace Microsoft.Dafny { } List ApplyInduction(QuantifierExpr e) { + Contract.Requires(e.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier Contract.Requires(e.TypeArgs.Count == 0); return ApplyInduction(e.BoundVars, e.Attributes, new List() { e.LogicalBody() }, delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); }); @@ -13946,6 +13971,12 @@ namespace Microsoft.Dafny { var e = (ComprehensionExpr)expr; // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with // the enclosing scopes. + + var q = e as QuantifierExpr; + if (q != null && q.SplitQuantifier != null) { + return Substitute(q.SplitQuantifierExpression); + } + var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension); Expression newRange = e.Range == null ? null : Substitute(e.Range); Expression newTerm = Substitute(e.Term); diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 33be0da2..80381f0a 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -21,30 +21,37 @@ namespace Microsoft.Dafny.Triggers { // Unfortunately, this would cause ill-behaved quantifiers to produce // exponentially many smaller quantifiers. + private static UnaryOpExpr Not(Expression expr) { + var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; + return not; + } + internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { expr = expr.Resolved; var unary = expr as UnaryOpExpr; var binary = expr as BinaryExpr; if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) { - foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); } + foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); } } else if (binary != null && binary.Op == separator) { foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; } foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) { - foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; } + foreach (var e in SplitExpr(Not(binary.E0), separator)) { yield return e; } foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } + } else { + yield return expr; } } internal static IEnumerable SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) { - foreach (var e1 in SplitExpr(pair.E1, separator)) { - yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1); + foreach (var e1 in SplitExpr(pair.E1, separator)) { + yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type }; } } internal static IEnumerable SplitQuantifier(QuantifierExpr quantifier) { - var body = quantifier.LogicalBody(); + var body = quantifier.Term; var binary = body as BinaryExpr; if (quantifier is ForallExpr) { @@ -55,7 +62,7 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.And); } foreach (var e in stream) { - yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else if (quantifier is ExistsExpr) { IEnumerable stream; @@ -65,17 +72,18 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.Or); } foreach (var e in stream) { - yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else { yield return quantifier; } } - protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier + protected override void VisitOneExpr(Expression expr) { var quantifier = expr as QuantifierExpr; if (quantifier != null) { - var rew = SplitQuantifier(quantifier); + var split = SplitQuantifier(quantifier).ToList(); + quantifier.SplitQuantifier = split; //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); } } diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index da43abcc..9fbc8a8a 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -272,6 +272,14 @@ namespace Microsoft.Dafny.Triggers { } private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful? + if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) { + return false; + } + + if (expr1.SplitQuantifier != null && expr2.SplitQuantifier != null) { + return ShallowEq_Top(expr1.SplitQuantifierExpression, expr2.SplitQuantifierExpression); + } + if (expr1.TypeArgs.Count != expr2.TypeArgs.Count || !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) { return false; diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/TriggerGenerator.cs index de4b212b..e218ad7b 100644 --- a/Source/Dafny/Triggers/TriggerGenerator.cs +++ b/Source/Dafny/Triggers/TriggerGenerator.cs @@ -19,9 +19,13 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file protected override bool VisitOneExpr(Expression expr, ref object st) { var quantifier = expr as QuantifierExpr; if (quantifier != null) { - quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); - } //FIXME handle the case of groups of quantifiers resulting from a split - + if (quantifier.SplitQuantifier != null) { + var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null); + quantifierCollections.Add(new QuantifiersCollection(collection, reporter)); + } else { + quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); + } + } return true; } } diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index dedbcbb1..6c6eede2 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -101,6 +101,7 @@ namespace Microsoft.Dafny.Triggers { } internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier return quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger"); } } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index e1f8a013..9f721d9a 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -44,11 +44,13 @@ namespace Microsoft.Dafny.Triggers { } internal IEnumerable LoopingSubterms(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier var matchingSubterms = MatchingSubterms(quantifier); return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); } internal List MatchingSubterms(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against. return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); } @@ -139,7 +141,7 @@ namespace Microsoft.Dafny.Triggers { (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944 (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) { annotation = AnnotatePotentialCandidate(expr); - } else if (expr is QuantifierExpr) { + } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier == null) { annotation = AnnotateQuantifier((QuantifierExpr)expr); } else if (expr is LetExpr) { annotation = AnnotateLetExpr((LetExpr)expr); @@ -259,6 +261,7 @@ namespace Microsoft.Dafny.Triggers { // FIXME document that this will contain duplicates internal List CollectTriggers(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions return Annotate(quantifier).PrivateTerms; } -- cgit v1.2.3