From e154fc24780204808b2dfd288d841469d0f9ae58 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 16 Mar 2022 19:02:41 -0700 Subject: [PATCH 01/39] Add SeqComprehension and parsing support --- Source/Dafny/AST/DafnyAst.cs | 26 +++++++++++++++++++++----- Source/Dafny/Dafny.atg | 30 ++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+), 5 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 0e7220638f9..3dd8d2477e8 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -11808,10 +11808,7 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) { } } - public class SetComprehension : ComprehensionExpr { - public override string WhatKind => "set comprehension"; - - public readonly bool Finite; + public class CollectionComprehension : ComprehensionExpr { public readonly bool TermIsImplicit; // records the given syntactic form public bool TermIsSimple { get { @@ -11823,7 +11820,7 @@ public bool TermIsSimple { } } - public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + public CollectionComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, endTok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); @@ -11832,9 +11829,28 @@ public SetComprehension(IToken tok, IToken endTok, bool finite, List b Contract.Requires(term != null || bvars.Count == 1); TermIsImplicit = term == null; + } + } + + public class SetComprehension : CollectionComprehension { + public override string WhatKind => "set comprehension"; + + public readonly bool Finite; + + public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression /*?*/ term, Attributes attrs) + : base(tok, endTok, bvars, range, term, attrs) { Finite = finite; } } + + public class SeqComprehension : CollectionComprehension { + public override string WhatKind => "seq comprehension"; + + public SeqComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + : base(tok, endTok, bvars, range, term, attrs) { + } + } + public class MapComprehension : ComprehensionExpr { public override string WhatKind => "map comprehension"; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 544331b95ef..c220a3f2fe9 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4173,6 +4173,7 @@ EndlessExpression | QuantifierExpression /* types are such that we can allow bitwise operations in the quantifier body */ | SetComprehensionExpr + | SeqComprehensionExpr | StmtInExpr Expression (. e = new StmtExpr(s.Tok, s, e); .) | LetExpression @@ -4685,6 +4686,35 @@ SetComprehensionExpr += (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); + BoundVar bv; + List bvars = new List(); + Expression range; + Expression body = null; + Attributes attrs = null; + .) + "seq" (. IToken setToken = t; .) + IdentTypeOptional (. bvars.Add(bv); .) + { "," + IdentTypeOptional (. bvars.Add(bv); .) + } + { Attribute } + "|" Expression + [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ + QSep + Expression + ] + (. if (body == null && bvars.Count != 1) { + SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); + q = dummyExpr; + } else { + q = new SeqComprehension(setToken, t, bvars, range, body, attrs); + } + .) + . /*------------------------------------------------------------------------*/ Expressions<.List args.> From 1f55a85385653728c610a71932d5d694d7f6433b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 17 Mar 2022 09:59:00 -0700 Subject: [PATCH 02/39] First cut of resolution, dummy translation for now --- Source/Dafny/AST/DafnyAst.cs | 8 ++++++-- Source/Dafny/Cloner.cs | 2 ++ Source/Dafny/Resolver.cs | 20 +++++++++++++------ Source/Dafny/Util.cs | 4 ++-- .../Translator.ExpressionTranslator.cs | 4 ++++ Test/dafny0/SeqComprehensions.dfy | 3 +++ 6 files changed, 31 insertions(+), 10 deletions(-) create mode 100644 Test/dafny0/SeqComprehensions.dfy diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 3dd8d2477e8..585e87b1a8a 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -11809,6 +11809,7 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) { } public class CollectionComprehension : ComprehensionExpr { + public virtual bool Finite => true; public readonly bool TermIsImplicit; // records the given syntactic form public bool TermIsSimple { get { @@ -11835,17 +11836,20 @@ public CollectionComprehension(IToken tok, IToken endTok, List bvars, public class SetComprehension : CollectionComprehension { public override string WhatKind => "set comprehension"; - public readonly bool Finite; + public override bool Finite => finite; + private readonly bool finite; public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression /*?*/ term, Attributes attrs) : base(tok, endTok, bvars, range, term, attrs) { - Finite = finite; + this.finite = finite; } } public class SeqComprehension : CollectionComprehension { public override string WhatKind => "seq comprehension"; + public override bool Finite => true; + public SeqComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, endTok, bvars, range, term, attrs) { } diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 76b2e0bb08c..6dedbd73af8 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -433,6 +433,8 @@ public virtual Expression CloneExpr(Expression expr) { return new MapComprehension(tk, tkEnd, mc.Finite, bvs, range, mc.TermLeft == null ? null : CloneExpr(mc.TermLeft), term, CloneAttributes(e.Attributes)); } else if (e is LambdaExpr l) { return new LambdaExpr(tk, tkEnd, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term); + } else if (e is SeqComprehension sc) { + return new SeqComprehension(tk, tkEnd, bvs, range, sc.TermIsImplicit ? null : term, CloneAttributes(e.Attributes)); } else { Contract.Assert(e is SetComprehension); var tt = (SetComprehension)e; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7058d28004a..2f5104a1041 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6711,8 +6711,8 @@ protected override void VisitOneExpr(Expression expr) { if (e is QuantifierExpr quantifierExpr) { whereToLookForBounds = quantifierExpr.LogicalBody(); polarity = quantifierExpr is ExistsExpr; - } else if (e is SetComprehension setComprehension) { - whereToLookForBounds = setComprehension.Range; + } else if (e is CollectionComprehension) { + whereToLookForBounds = e.Range; } else if (e is MapComprehension) { whereToLookForBounds = e.Range; } else { @@ -15208,8 +15208,8 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { allTypeParameters.PopMarker(); expr.Type = Type.Bool; - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is ComprehensionExpr) { + var e = (ComprehensionExpr)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { @@ -15228,8 +15228,16 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveAttributes(e, opts); scope.PopMarker(); - expr.Type = new SetType(e.Finite, e.Term.Type); - + + switch (e) { + case SetComprehension se: + expr.Type = new SetType(se.Finite, se.Term.Type); + break; + case SeqComprehension se: + expr.Type = new SeqType(se.Term.Type); + break; + } + } else if (expr is MapComprehension) { var e = (MapComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index a526cd1f093..a89377ad0fd 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -1149,8 +1149,8 @@ public static bool UsesSpecFeatures(Expression expr) { var e = (QuantifierExpr)expr; Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody()); - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is CollectionComprehension) { + var e = (CollectionComprehension)expr; return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index 3acfc1c8eeb..881c5d235ab 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -400,6 +400,10 @@ public Boogie.Expr TrExpr(Expression expr) { } return s; + } else if (expr is SeqComprehension) { + // TODO + return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType); + } else if (expr is MapDisplayExpr) { MapDisplayExpr e = (MapDisplayExpr)expr; Boogie.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType); diff --git a/Test/dafny0/SeqComprehensions.dfy b/Test/dafny0/SeqComprehensions.dfy new file mode 100644 index 00000000000..e9b27a0c941 --- /dev/null +++ b/Test/dafny0/SeqComprehensions.dfy @@ -0,0 +1,3 @@ +method Foo() { + var s := seq x: int | x == 2; +} \ No newline at end of file From 9c8621605d9cd211cfcc1105aaf370a8b6c87904 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 31 Mar 2022 18:47:47 -0700 Subject: [PATCH 03/39] Fix parsing ambiguity with sequence constructions --- Source/Dafny/Dafny.atg | 87 ++++++++++++++++++++---------------------- 1 file changed, 42 insertions(+), 45 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index c220a3f2fe9..a7b8ab5a90d 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4080,34 +4080,13 @@ SetDisplayExpr SeqDisplayExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken x = null; - Type explicitTypeArg = null; - Expression n, f; - e = dummyExpr; .) - ( - "seq" (. x = t; .) - [ (. var gt = new List(); .) - GenericInstantiation (. if (gt.Count > 1) { - SemErr("seq type expects only one type argument"); - } else { - explicitTypeArg = gt[0]; - } - .) - ] - "(" - Expression - "," - Expression - ")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .) - | - "[" (. List elements = new List(); - x = t; - - .) - [ Expressions ] (. e = new SeqDisplayExpr(x, elements); - .) - "]" - ) + "[" (. List elements = new List(); + x = t; + .) + [ Expressions ] (. e = new SeqDisplayExpr(x, elements); + .) + "]" . /*------------------------------------------------------------------------*/ @@ -4690,30 +4669,48 @@ SetComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); + Type explicitTypeArg = null; + Expression n, f; BoundVar bv; List bvars = new List(); Expression range; Expression body = null; Attributes attrs = null; + q = dummyExpr; .) - "seq" (. IToken setToken = t; .) - IdentTypeOptional (. bvars.Add(bv); .) - { "," - IdentTypeOptional (. bvars.Add(bv); .) - } - { Attribute } - "|" Expression - [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ - QSep - Expression - ] - (. if (body == null && bvars.Count != 1) { - SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); - q = dummyExpr; - } else { - q = new SeqComprehension(setToken, t, bvars, range, body, attrs); - } - .) + "seq" (. IToken seqToken = t; .) + ( + [ (. var gt = new List(); .) + GenericInstantiation (. if (gt.Count > 1) { + SemErr("seq type expects only one type argument"); + } else { + explicitTypeArg = gt[0]; + } + .) + ] + "(" + Expression + "," + Expression + ")" (. q = new SeqConstructionExpr(seqToken, explicitTypeArg, n, f); .) + | + IdentTypeOptional (. bvars.Add(bv); .) + { "," + IdentTypeOptional (. bvars.Add(bv); .) + } + { Attribute } + "|" Expression + [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ + QSep + Expression + ] + (. if (body == null && bvars.Count != 1) { + SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); + } else { + q = new SeqComprehension(seqToken, t, bvars, range, body, attrs); + } + .) + ) . /*------------------------------------------------------------------------*/ From 1d564a5a5f444e04a28fedd823256e2e06fde6e2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 20 May 2022 12:49:55 -0400 Subject: [PATCH 04/39] First try at parsing changes --- Source/Dafny/AST/DafnyAst.cs | 27 +++++++++++++++++++++++++++ Source/Dafny/Dafny.atg | 26 ++++++++++++++++++++------ 2 files changed, 47 insertions(+), 6 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 585e87b1a8a..fb6e1b50791 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6142,6 +6142,33 @@ public BoundVar(IToken tok, string name, Type type) Contract.Requires(type != null); } } + + [DebuggerDisplay("Quantified<{name}>")] + public class QuantifiedVar : BoundVar { + public readonly Expression Domain; + public readonly Expression Range; + + public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expression range) + : base(tok, name, type) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + Domain = domain; + Range = range; + } + + public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { + bvars = new List(); + range = new LiteralExpr(Token.NoToken, true); + foreach(var qvar in qvars) { + BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.Type); + bvars.Add(bvar); + range = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, + new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain)); + range = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); + } + } + } public class ActualBinding { public readonly IToken /*?*/ FormalParameterName; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a7b8ab5a90d..a89ec3cfed5 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4620,20 +4620,34 @@ QuantifierExpression /*------------------------------------------------------------------------*/ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range.> = (. - bvars = new List(); - BoundVar/*!*/ bv; + List qvars = new List(); + QuantifiedVar/*!*/ qv; attrs = null; range = null; .) - IdentTypeOptional (. bvars.Add(bv); .) + QuantifierVariableDecl (. qvars.Add(qv); .) { "," - IdentTypeOptional (. bvars.Add(bv); .) + QuantifierVariableDecl (. qvars.Add(qv); .) } + (. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .) + . + +/*------------------------------------------------------------------------*/ +QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs.> += (. + BoundVar/*!*/ bv; + Expression domain = null; + Expression range = null; + .) + IdentTypeOptional + [ "<-" + Expression + ] { Attribute } - [ IF(la.kind == _verticalbar) /* Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement; I don't see how that's possible, but this IF is good and suppresses the reported ambiguity */ - "|" + [ "|" Expression ] + (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.Type, domain, range); .) . /*------------------------------------------------------------------------*/ From fe946d70a76fbd7966a3ba67ba638c435348b819 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 20 May 2022 17:13:10 -0400 Subject: [PATCH 05/39] Unify QuantifierDomain parsing, bug fix --- Source/Dafny/AST/DafnyAst.cs | 11 +++++++--- Source/Dafny/Dafny.atg | 42 +++++++++++------------------------- 2 files changed, 20 insertions(+), 33 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index fb6e1b50791..a8d1ac65784 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6163,9 +6163,14 @@ public static void ExtractSingleRange(List qvars, out List "forall" (. x = t; tok = x; .) ( IF(la.kind == _openparen) /* disambiguation needed, because of the possibility of a body-less forall statement */ - "(" [ QuantifierDomain ] ")" + "(" [ QuantifierDomain ] ")" | [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */ - QuantifierDomain + QuantifierDomain ] ) (. if (bvars == null) { bvars = new List(); } @@ -4114,7 +4114,6 @@ MapLiteralExpressions<.out List elements.> /*------------------------------------------------------------------------*/ MapComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); - BoundVar bv; List bvars = new List(); Expression range = null; Expression bodyLeft = null; @@ -4123,12 +4122,7 @@ MapComprehensionExpr (. bvars.Add(bv); .) - { "," - IdentTypeOptional (. bvars.Add(bv); .) - } - { Attribute } - [ "|" Expression ] + QuantifierDomain QSep Expression [ IF(IsGets()) /* greedily parse ":=" */ (. bodyLeft = bodyRight; .) @@ -4606,7 +4600,7 @@ QuantifierExpression ( Forall (. x = t; univ = true; .) | Exists (. x = t; .) ) - QuantifierDomain + QuantifierDomain QSep Expression (. if (univ) { @@ -4618,22 +4612,22 @@ QuantifierExpression . /*------------------------------------------------------------------------*/ -QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range.> +QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range, bool allowLemma, bool allowLambda, bool allowBitwiseOps.> = (. List qvars = new List(); QuantifiedVar/*!*/ qv; attrs = null; range = null; .) - QuantifierVariableDecl (. qvars.Add(qv); .) + QuantifierVariableDecl (. qvars.Add(qv); .) { "," - QuantifierVariableDecl (. qvars.Add(qv); .) + QuantifierVariableDecl (. qvars.Add(qv); .) } (. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .) . /*------------------------------------------------------------------------*/ -QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs.> +QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allowLemma, bool allowLambda, bool allowBitwiseOps.> = (. BoundVar/*!*/ bv; Expression domain = null; @@ -4641,11 +4635,11 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs.> .) IdentTypeOptional [ "<-" - Expression + Expression ] { Attribute } [ "|" - Expression + Expression ] (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.Type, domain, range); .) . @@ -4653,7 +4647,6 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs.> /*------------------------------------------------------------------------*/ SetComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); - BoundVar bv; List bvars = new List(); Expression range; Expression body = null; @@ -4661,12 +4654,7 @@ SetComprehensionExpr (. bvars.Add(bv); .) - { "," - IdentTypeOptional (. bvars.Add(bv); .) - } - { Attribute } - "|" Expression + QuantifierDomain [ IF(IsQSep()) /* let any given body bind to the closest enclosing set comprehension */ QSep Expression @@ -4685,7 +4673,6 @@ SeqComprehensionExpr bvars = new List(); Expression range; Expression body = null; @@ -4708,12 +4695,7 @@ SeqComprehensionExpr ")" (. q = new SeqConstructionExpr(seqToken, explicitTypeArg, n, f); .) | - IdentTypeOptional (. bvars.Add(bv); .) - { "," - IdentTypeOptional (. bvars.Add(bv); .) - } - { Attribute } - "|" Expression + QuantifierDomain [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ QSep Expression From d67c1fef9f4ce2329fcafff3cc933bb6b7518d60 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 20 May 2022 17:39:46 -0400 Subject: [PATCH 06/39] Fix precedence issue with | --- Source/Dafny/Dafny.atg | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ccc223a7088..1f65aef69d1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4635,7 +4635,9 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow .) IdentTypeOptional [ "<-" - Expression + /* We can't allow bitwise ops here since otherwise we'll swallow up any + optional "| " suffix */ + Expression ] { Attribute } [ "|" From 529c75e0e3c9074d7977c5e2115c5fbabce817a8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 20 May 2022 17:54:02 -0400 Subject: [PATCH 07/39] Sequence comprehension printing --- Source/Dafny/AST/Printer.cs | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index 1624c53d289..020957757c7 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2613,15 +2613,23 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, } if (parensNeeded) { wr.Write(")"); } - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is CollectionComprehension) { + var e = (CollectionComprehension)expr; bool parensNeeded = !isRightmost; if (parensNeeded) { wr.Write("("); } - if (e.Finite) { - wr.Write("set "); - } else { - wr.Write("iset "); + switch (e) { + case SetComprehension se: + if (e.Finite) { + wr.Write("set "); + } else { + wr.Write("iset "); + } + break; + case SeqComprehension se: + wr.Write("seq "); + break; } + string sep = ""; foreach (BoundVar bv in e.BoundVars) { wr.Write("{0}{1}", sep, bv.DisplayName); From 9eb0cf8954833e4331cb5365d006c77e920b9cea Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 23 May 2022 22:12:02 -0700 Subject: [PATCH 08/39] Partial fix --- Source/Dafny/AST/DafnyAst.cs | 8 ++++---- Source/Dafny/Dafny.atg | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index a8d1ac65784..7d5788f6ea0 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6161,15 +6161,15 @@ public static void ExtractSingleRange(List qvars, out List(); range = new LiteralExpr(Token.NoToken, true); foreach(var qvar in qvars) { - BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.Type); + BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); bvars.Add(bvar); if (qvar.Domain != null) { - range = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, - new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain)); + var inDomainExpr = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain); + range = range == null ? inDomainExpr : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, inDomainExpr); } if (qvar.Range != null) { - range = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); + range = range == null ? qvar.Range : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); } } } diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 1f65aef69d1..f4c678c0c60 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4643,7 +4643,7 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow [ "|" Expression ] - (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.Type, domain, range); .) + (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.SyntacticType, domain, range); .) . /*------------------------------------------------------------------------*/ From fc75a3c69123ffe7310a16a9e27599c186afb48f Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 25 May 2022 11:18:59 -0700 Subject: [PATCH 09/39] Fix lambdas (incorrect type check in resolver) --- Source/Dafny/Resolver.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2f5104a1041..5c6b52b7bea 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -15208,8 +15208,8 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { allTypeParameters.PopMarker(); expr.Type = Type.Bool; - } else if (expr is ComprehensionExpr) { - var e = (ComprehensionExpr)expr; + } else if (expr is CollectionComprehension) { + var e = (CollectionComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { From 36187561de7505926466922e0223652ca2ba95ad Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 25 May 2022 16:12:04 -0700 Subject: [PATCH 10/39] Split off seq construction production to fix suffixes --- Source/Dafny/Dafny.atg | 77 ++++++++++++++++++------------- Test/dafny0/SeqComprehensions.dfy | 19 +++++++- 2 files changed, 62 insertions(+), 34 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f4c678c0c60..f018de085d6 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -378,6 +378,11 @@ bool IsSetDisplay() { return false; } +bool IsSeqConstruction() { + scanner.ResetPeek(); + return la.kind == _seq && scanner.Peek().kind == _openparen; +} + bool IsSuffix() { return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen; } @@ -3882,6 +3887,9 @@ PrimaryExpression { IF(IsSuffix()) Suffix } + | IF(IsSeqConstruction()) /* this alternative must be checked before going into EndlessExpression, where there is another "seq" */ + SeqConstructionExpr + { IF(IsSuffix()) Suffix } | IF(IsLambda(allowLambda)) LambdaExpression /* this is an endless expression */ | EndlessExpression @@ -4089,6 +4097,29 @@ SeqDisplayExpr "]" . +/*------------------------------------------------------------------------*/ +SeqConstructionExpr += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); + IToken x = null; + Type explicitTypeArg = null; + Expression n, f; + .) + "seq" (. x = t; .) + [ (. var gt = new List(); .) + GenericInstantiation (. if (gt.Count > 1) { + SemErr("seq type expects only one type argument"); + } else { + explicitTypeArg = gt[0]; + } + .) + ] + "(" + Expression + "," + Expression + ")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .) + . + /*------------------------------------------------------------------------*/ MapDisplayExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); @@ -4673,43 +4704,25 @@ SetComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); - Type explicitTypeArg = null; - Expression n, f; List bvars = new List(); Expression range; Expression body = null; Attributes attrs = null; - q = dummyExpr; .) - "seq" (. IToken seqToken = t; .) - ( - [ (. var gt = new List(); .) - GenericInstantiation (. if (gt.Count > 1) { - SemErr("seq type expects only one type argument"); - } else { - explicitTypeArg = gt[0]; - } - .) - ] - "(" - Expression - "," - Expression - ")" (. q = new SeqConstructionExpr(seqToken, explicitTypeArg, n, f); .) - | - QuantifierDomain - [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ - QSep - Expression - ] - (. if (body == null && bvars.Count != 1) { - SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); - } else { - q = new SeqComprehension(seqToken, t, bvars, range, body, attrs); - } - .) - ) - . + "seq" (. IToken seqToken = t; .) + QuantifierDomain + [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ + QSep + Expression + ] + (. if (body == null && bvars.Count != 1) { + SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); + q = dummyExpr; + } else { + q = new SeqComprehension(seqToken, t, bvars, range, body, attrs); + } + .) + . /*------------------------------------------------------------------------*/ Expressions<.List args.> diff --git a/Test/dafny0/SeqComprehensions.dfy b/Test/dafny0/SeqComprehensions.dfy index e9b27a0c941..a7e49401415 100644 --- a/Test/dafny0/SeqComprehensions.dfy +++ b/Test/dafny0/SeqComprehensions.dfy @@ -1,3 +1,18 @@ +// RUN: %dafny /compile:0 "%s" > "%t" method Foo() { - var s := seq x: int | x == 2; -} \ No newline at end of file + var myMap := map[1 := [1], 2 := [4], 3 := [9]]; + var s: seq := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]; + var s' := seq i <- s | i > 3, + j <- f(i) + :: j; + var s'' := seq i <- s | i in myMap, + j <- myMap[i] + :: j; + assert forall i <- s :: i > 0; +} + +function f(x: nat): seq + requires x > 3 +{ + [x - 3, x - 2, x - 1, x] +} From 386ea1f4782a0a93731ae54353a23a1f3623ca9f Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 25 May 2022 22:44:23 -0700 Subject: [PATCH 11/39] Default to null range --- Source/Dafny/AST/DafnyAst.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 86f8050dae8..d7cb4578c1a 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6144,7 +6144,7 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { bvars = new List(); - range = new LiteralExpr(Token.NoToken, true); + range = null; foreach(var qvar in qvars) { BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); bvars.Add(bvar); From d819d5940a239bb8a91db8d09f26f1c41e6b47ec Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 26 May 2022 09:25:19 -0700 Subject: [PATCH 12/39] Handle seq constructions with explicit type args too --- Source/Dafny/Dafny.atg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d756ff5af54..3761a07c34b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -417,7 +417,8 @@ bool ExprIsSetDisplay() { bool IsSeqConstruction() { scanner.ResetPeek(); - return la.kind == _seq && scanner.Peek().kind == _openparen; + int k = scanner.Peek().kind; + return la.kind == _seq && (k == _openparen || k == _openAngleBracket); } bool IsSuffix() { From 20eccfc26c5f78a5b576d0d5167e94bfecd09c8a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 26 May 2022 13:37:40 -0700 Subject: [PATCH 13/39] =?UTF-8?q?Fix=20parsing=20of=20=E2=80=9C<-=E2=80=9C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Source/Dafny/Dafny.atg | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 3761a07c34b..5cde9fda2b7 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1671,9 +1671,6 @@ GenericParameters<.List/*!*/ typeArgs, bool allowVariance.> TypeParameter.TPVarianceSyntax variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; // assignment is to please compiler characteristics = new TypeParameter.TypeParameterCharacteristics(false); .) - // If a "<" combined with a Variance symbol could be a new token, then the parser here will need to be more complex, - // since, for example, a < followed immediately by a Variance symbol would scan as the wrong token. - // Fortunately that is not currently the case. "<" [ Variance (. if (!allowVariance) { SemErr(t, "type-parameter variance is not allowed to be specified in this context"); } .) ] @@ -4730,7 +4727,9 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow Expression range = null; .) IdentTypeOptional - [ "<-" + [ // "<-" can also appear in GenericParameters in something like "<-T>", + // so we parse it as two separate tokens. + "<" "-" /* We can't allow bitwise ops here since otherwise we'll swallow up any optional "| " suffix */ Expression From 05258596059ec46b306f1b315db82c5b5cc304cf Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 26 May 2022 16:13:24 -0700 Subject: [PATCH 14/39] Just a spoonful of lookahead makes the medicine go down --- Source/Dafny/Dafny.atg | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5cde9fda2b7..471f542db3c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -219,6 +219,13 @@ bool IsIdentifier(int kind) { return kind == _ident || kind == _least || kind == _greatest || kind == _older; } +bool IsCommaIdentifier() { + scanner.ResetPeek(); + IToken x = scanner.Peek(); + return la.kind == _comma && IsIdentifier(x.kind); +} + + bool IsLabel(bool allowLabel) { if (!allowLabel) { return false; @@ -4713,7 +4720,8 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range = null; .) QuantifierVariableDecl (. qvars.Add(qv); .) - { "," + { IF(IsCommaIdentifier()) + "," QuantifierVariableDecl (. qvars.Add(qv); .) } (. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .) From 53628aa63fd403face4dc5c5f2add90d639568a9 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 26 May 2022 16:33:54 -0700 Subject: [PATCH 15/39] Missing file --- Test/dafny0/ParseErrors.dfy.expect | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect index a95b5d865cf..7a1570040dc 100644 --- a/Test/dafny0/ParseErrors.dfy.expect +++ b/Test/dafny0/ParseErrors.dfy.expect @@ -34,7 +34,6 @@ ParseErrors.dfy(137,19): Error: formal cannot be declared 'ghost' in this contex ParseErrors.dfy(139,23): Error: formal cannot be declared 'ghost' in this context ParseErrors.dfy(142,27): Error: formal cannot be declared 'ghost' in this context ParseErrors.dfy(143,28): Error: formal cannot be declared 'ghost' in this context -ParseErrors.dfy(155,19): Error: verticalbar expected ParseErrors.dfy(155,18): Error: a set comprehension with more than one bound variable must have a term expression ParseErrors.dfy(156,22): Error: a set comprehension with more than one bound variable must have a term expression ParseErrors.dfy(163,2): Error: mutable fields are not allowed in value types @@ -80,4 +79,4 @@ ParseErrors.dfy(255,32): Error: formal cannot be declared 'older' in this contex ParseErrors.dfy(256,11): Error: formal cannot be declared 'older' in this context ParseErrors.dfy(257,17): Error: formal cannot be declared 'older' in this context ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this context -77 parse errors detected in ParseErrors.dfy +76 parse errors detected in ParseErrors.dfy From db8534e56bac8a2b7ac38c4da6cc501b6327b6a8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 30 May 2022 11:22:07 -0700 Subject: [PATCH 16/39] Added IsQuantifierVariableDecl lookahead --- Source/Dafny/Dafny.atg | 37 ++++++++++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 471f542db3c..879cf101a76 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -219,10 +219,31 @@ bool IsIdentifier(int kind) { return kind == _ident || kind == _least || kind == _greatest || kind == _older; } -bool IsCommaIdentifier() { +bool IsQuantifierVariableDecl(bool requireTypeOrDomain) { scanner.ResetPeek(); + + if (la.kind != _comma) { + return false; + } + IToken x = scanner.Peek(); - return la.kind == _comma && IsIdentifier(x.kind); + if (!IsIdentifier(x.kind)) { + return false; + } + + if (!requireTypeOrDomain) { + return true; + } + + x = scanner.Peek(); + if (x.kind == _colon) { + return true; + } else if (x.kind == _openAngleBracket) { + x = scanner.Peek(); + return x.kind == _minus; + } else { + return false; + } } @@ -900,6 +921,7 @@ TOKENS sarrow = "->". qarrow = "~>". larrow = "-->". + minus = "-". COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf IGNORE cr + lf + tab @@ -4720,7 +4742,16 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range = null; .) QuantifierVariableDecl (. qvars.Add(qv); .) - { IF(IsCommaIdentifier()) + { // This predicate requires an explicit domain (<- C) or an explicit type (: T), + // to disambiguate comprehensions with multiple variables from comma-separated lists of expressions. + // The following will be parsed as two arguments to the print statement, as opposed to a single + // comprehension of two variables (and an invalid one to boot, since it would need an explicit term). + // + // print set x: x | E, y; + // + // This is partially due to the ambiguity of | as either a delimiter for a quantified variable range + // or a bitwise "or" operator. + IF(IsQuantifierVariableDecl(qv.Range != null)) "," QuantifierVariableDecl (. qvars.Add(qv); .) } From 09643044c27c337c8d8183d822aae1d10e44a771 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 30 May 2022 11:44:46 -0700 Subject: [PATCH 17/39] Undoing sequence comprehension changes for this branch --- Source/Dafny/AST/DafnyAst.cs | 31 ++----- Source/Dafny/AST/Printer.cs | 19 ++--- Source/Dafny/Cloner.cs | 2 - Source/Dafny/Dafny.atg | 85 ++++++------------- Source/Dafny/Resolver.cs | 18 ++-- Source/Dafny/Util.cs | 4 +- .../Translator.ExpressionTranslator.cs | 4 - Test/dafny0/SeqComprehensions.dfy | 18 ---- 8 files changed, 44 insertions(+), 137 deletions(-) delete mode 100644 Test/dafny0/SeqComprehensions.dfy diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index d7cb4578c1a..e1b572714fc 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -11968,8 +11968,10 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) { } } - public class CollectionComprehension : ComprehensionExpr { - public virtual bool Finite => true; + public class SetComprehension : ComprehensionExpr { + public override string WhatKind => "set comprehension"; + + public readonly bool Finite; public readonly bool TermIsImplicit; // records the given syntactic form public bool TermIsSimple { get { @@ -11981,7 +11983,7 @@ public bool TermIsSimple { } } - public CollectionComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, endTok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); @@ -11990,31 +11992,10 @@ public CollectionComprehension(IToken tok, IToken endTok, List bvars, Contract.Requires(term != null || bvars.Count == 1); TermIsImplicit = term == null; + Finite = finite; } } - public class SetComprehension : CollectionComprehension { - public override string WhatKind => "set comprehension"; - - public override bool Finite => finite; - private readonly bool finite; - - public SetComprehension(IToken tok, IToken endTok, bool finite, List bvars, Expression range, Expression /*?*/ term, Attributes attrs) - : base(tok, endTok, bvars, range, term, attrs) { - this.finite = finite; - } - } - - public class SeqComprehension : CollectionComprehension { - public override string WhatKind => "seq comprehension"; - - public override bool Finite => true; - - public SeqComprehension(IToken tok, IToken endTok, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) - : base(tok, endTok, bvars, range, term, attrs) { - } - } - public class MapComprehension : ComprehensionExpr { public override string WhatKind => "map comprehension"; diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index a5c86c2063c..96048527f18 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2626,21 +2626,14 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, } if (parensNeeded) { wr.Write(")"); } - } else if (expr is CollectionComprehension) { - var e = (CollectionComprehension)expr; + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; bool parensNeeded = !isRightmost; if (parensNeeded) { wr.Write("("); } - switch (e) { - case SetComprehension se: - if (e.Finite) { - wr.Write("set "); - } else { - wr.Write("iset "); - } - break; - case SeqComprehension se: - wr.Write("seq "); - break; + if (e.Finite) { + wr.Write("set "); + } else { + wr.Write("iset "); } string sep = ""; diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index f37c6067d5e..5fc3d1b0530 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -433,8 +433,6 @@ public virtual Expression CloneExpr(Expression expr) { return new MapComprehension(tk, tkEnd, mc.Finite, bvs, range, mc.TermLeft == null ? null : CloneExpr(mc.TermLeft), term, CloneAttributes(e.Attributes)); } else if (e is LambdaExpr l) { return new LambdaExpr(tk, tkEnd, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term); - } else if (e is SeqComprehension sc) { - return new SeqComprehension(tk, tkEnd, bvs, range, sc.TermIsImplicit ? null : term, CloneAttributes(e.Attributes)); } else { Contract.Assert(e is SetComprehension); var tt = (SetComprehension)e; diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 879cf101a76..4914e9a181a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -443,12 +443,6 @@ bool ExprIsSetDisplay() { return false; } -bool IsSeqConstruction() { - scanner.ResetPeek(); - int k = scanner.Peek().kind; - return la.kind == _seq && (k == _openparen || k == _openAngleBracket); -} - bool IsSuffix() { return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen; } @@ -3978,9 +3972,6 @@ PrimaryExpression { IF(IsSuffix()) Suffix } - | IF(IsSeqConstruction()) /* this alternative must be checked before going into EndlessExpression, where there is another "seq" */ - SeqConstructionExpr - { IF(IsSuffix()) Suffix } | IF(IsLambda(allowLambda)) LambdaExpression /* this is an endless expression */ | EndlessExpression @@ -4177,38 +4168,36 @@ SetDisplayExpr /*------------------------------------------------------------------------*/ SeqDisplayExpr -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); - IToken x = null; - .) - "[" (. List elements = new List(); - x = t; - .) - [ Expressions ] (. e = new SeqDisplayExpr(x, elements); - .) - "]" - . - -/*------------------------------------------------------------------------*/ -SeqConstructionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken x = null; Type explicitTypeArg = null; Expression n, f; + e = dummyExpr; .) - "seq" (. x = t; .) - [ (. var gt = new List(); .) - GenericInstantiation (. if (gt.Count > 1) { - SemErr("seq type expects only one type argument"); - } else { - explicitTypeArg = gt[0]; - } - .) - ] - "(" - Expression - "," - Expression - ")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .) + ( + "seq" (. x = t; .) + [ (. var gt = new List(); .) + GenericInstantiation (. if (gt.Count > 1) { + SemErr("seq type expects only one type argument"); + } else { + explicitTypeArg = gt[0]; + } + .) + ] + "(" + Expression + "," + Expression + ")" (. e = new SeqConstructionExpr(x, explicitTypeArg, n, f); .) + | + "[" (. List elements = new List(); + x = t; + + .) + [ Expressions ] (. e = new SeqDisplayExpr(x, elements); + .) + "]" + ) . /*------------------------------------------------------------------------*/ @@ -4268,7 +4257,6 @@ EndlessExpression | QuantifierExpression /* types are such that we can allow bitwise operations in the quantifier body */ | SetComprehensionExpr - | SeqComprehensionExpr | StmtInExpr Expression (. e = new StmtExpr(s.Tok, s, e); .) | LetExpression @@ -4804,29 +4792,6 @@ SetComprehensionExpr -= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); - List bvars = new List(); - Expression range; - Expression body = null; - Attributes attrs = null; - .) - "seq" (. IToken seqToken = t; .) - QuantifierDomain - [ IF(IsQSep()) /* let any given body bind to the closest enclosing seq comprehension */ - QSep - Expression - ] - (. if (body == null && bvars.Count != 1) { - SemErr(t, "a seq comprehension with more than one bound variable must have a term expression"); - q = dummyExpr; - } else { - q = new SeqComprehension(seqToken, t, bvars, range, body, attrs); - } - .) - . - /*------------------------------------------------------------------------*/ Expressions<.List args.> = (. Expression e; .) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3e388b16fac..cc4f758a116 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6718,8 +6718,8 @@ protected override void VisitOneExpr(Expression expr) { if (e is QuantifierExpr quantifierExpr) { whereToLookForBounds = quantifierExpr.LogicalBody(); polarity = quantifierExpr is ExistsExpr; - } else if (e is CollectionComprehension) { - whereToLookForBounds = e.Range; + } else if (e is SetComprehension setComprehension) { + whereToLookForBounds = setComprehension.Range; } else if (e is MapComprehension) { whereToLookForBounds = e.Range; } else { @@ -15239,8 +15239,8 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { scope.PopMarker(); expr.Type = Type.Bool; - } else if (expr is CollectionComprehension) { - var e = (CollectionComprehension)expr; + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { @@ -15259,15 +15259,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveAttributes(e, opts); scope.PopMarker(); - - switch (e) { - case SetComprehension se: - expr.Type = new SetType(se.Finite, se.Term.Type); - break; - case SeqComprehension se: - expr.Type = new SeqType(se.Term.Type); - break; - } + expr.Type = new SetType(e.Finite, e.Term.Type); } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 72c9b9e44a1..0a02ff01db5 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -1150,8 +1150,8 @@ public static bool UsesSpecFeatures(Expression expr) { var e = (QuantifierExpr)expr; Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody()); - } else if (expr is CollectionComprehension) { - var e = (CollectionComprehension)expr; + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index 60005c77ed3..6afc6cd26e0 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -405,10 +405,6 @@ public Boogie.Expr TrExpr(Expression expr) { } return s; - } else if (expr is SeqComprehension) { - // TODO - return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType); - } else if (expr is MapDisplayExpr) { MapDisplayExpr e = (MapDisplayExpr)expr; Boogie.Type maptype = predef.MapType(GetToken(expr), e.Finite, predef.BoxType, predef.BoxType); diff --git a/Test/dafny0/SeqComprehensions.dfy b/Test/dafny0/SeqComprehensions.dfy deleted file mode 100644 index a7e49401415..00000000000 --- a/Test/dafny0/SeqComprehensions.dfy +++ /dev/null @@ -1,18 +0,0 @@ -// RUN: %dafny /compile:0 "%s" > "%t" -method Foo() { - var myMap := map[1 := [1], 2 := [4], 3 := [9]]; - var s: seq := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]; - var s' := seq i <- s | i > 3, - j <- f(i) - :: j; - var s'' := seq i <- s | i in myMap, - j <- myMap[i] - :: j; - assert forall i <- s :: i > 0; -} - -function f(x: nat): seq - requires x > 3 -{ - [x - 3, x - 2, x - 1, x] -} From 5cf115dfb2b24736ce6cda7f530a4fe36af5c876 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 30 May 2022 11:48:42 -0700 Subject: [PATCH 18/39] Whitespace cleanup --- Source/Dafny/AST/DafnyAst.cs | 1 - Source/Dafny/AST/Printer.cs | 1 - Source/Dafny/Dafny.atg | 2 +- Source/Dafny/Resolver.cs | 2 +- 4 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index e1b572714fc..3dfd994b7ee 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -11995,7 +11995,6 @@ public SetComprehension(IToken tok, IToken endTok, bool finite, List b Finite = finite; } } - public class MapComprehension : ComprehensionExpr { public override string WhatKind => "map comprehension"; diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index 96048527f18..f0beb3e4fd6 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2635,7 +2635,6 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, } else { wr.Write("iset "); } - string sep = ""; foreach (BoundVar bv in e.BoundVars) { wr.Write("{0}{1}", sep, bv.DisplayName); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 4914e9a181a..05d167aa394 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4791,7 +4791,7 @@ SetComprehensionExpr args.> = (. Expression e; .) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index cc4f758a116..2c0d804a84f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -15260,7 +15260,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveAttributes(e, opts); scope.PopMarker(); expr.Type = new SetType(e.Finite, e.Term.Type); - + } else if (expr is MapComprehension) { var e = (MapComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); From 5694696e5123eae4206c5412e60671e5bfa3e840 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 31 May 2022 08:00:07 -0700 Subject: [PATCH 19/39] Hook up /quantifierSyntax, copy and modify several test files --- Source/Dafny/Dafny.atg | 70 ++-- Source/Dafny/DafnyOptions.cs | 18 + Test/comp/ForallNewSyntax.dfy | 356 ++++++++++++++++++ Test/comp/ForallNewSyntax.dfy.expect | 176 +++++++++ Test/comp/NewSyntaxComprehensions.dfy | 284 ++++++++++++++ Test/comp/NewSyntaxComprehensions.dfy.expect | 242 ++++++++++++ Test/dafny0/ForallCompilationNewSyntax.dfy | 104 +++++ .../ForallCompilationNewSyntax.dfy.expect | 2 + Test/dafny0/NewSyntaxComprehensions.dfy | 191 ++++++++++ .../dafny0/NewSyntaxComprehensions.dfy.expect | 23 ++ 10 files changed, 1431 insertions(+), 35 deletions(-) create mode 100644 Test/comp/ForallNewSyntax.dfy create mode 100644 Test/comp/ForallNewSyntax.dfy.expect create mode 100644 Test/comp/NewSyntaxComprehensions.dfy create mode 100644 Test/comp/NewSyntaxComprehensions.dfy.expect create mode 100644 Test/dafny0/ForallCompilationNewSyntax.dfy create mode 100644 Test/dafny0/ForallCompilationNewSyntax.dfy.expect create mode 100644 Test/dafny0/NewSyntaxComprehensions.dfy create mode 100644 Test/dafny0/NewSyntaxComprehensions.dfy.expect diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 05d167aa394..dbd5acae14c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -219,31 +219,32 @@ bool IsIdentifier(int kind) { return kind == _ident || kind == _least || kind == _greatest || kind == _older; } -bool IsQuantifierVariableDecl(bool requireTypeOrDomain) { - scanner.ResetPeek(); - - if (la.kind != _comma) { +bool IsQuantifierVariableDecl(QuantifiedVar previousVar) { + // Introducing per-quantified variable ranges creates some ambiguities in the grammar, + // since before that the range would terminate the quantifed domain. For example, the following statement: + // + // print set x: x | E, y; + // + // This would previously parse as two separate arguments to the print statement, but + // could now also be parsed as a single set comprehension argument with two quantified variables + // (and an invalid one since it would need an explicit ":: " section). + // Even worse: + // + // print set x: x | E, y <- C; + // + // This was a valid statement before as well, because "y <- C" would be parsed as the expression + // "y < (-C)". + // + // The /quantifierSyntax option is used to help migrate this otherwise breaking change: + // * /quantifierSyntax:3 keeps the old behaviour where a "| " always terminates the list of quantified variables. + // * /quantifierSyntax:4 instead attempts to parse additional quantified variables. + if (previousVar.Range != null && theOptions.QuantifierSyntax == DafnyOptions.QuantifierSyntaxOptions.Version3) { return false; } - + + scanner.ResetPeek(); IToken x = scanner.Peek(); - if (!IsIdentifier(x.kind)) { - return false; - } - - if (!requireTypeOrDomain) { - return true; - } - - x = scanner.Peek(); - if (x.kind == _colon) { - return true; - } else if (x.kind == _openAngleBracket) { - x = scanner.Peek(); - return x.kind == _minus; - } else { - return false; - } + return la.kind == _comma && IsIdentifier(x.kind); } @@ -1694,6 +1695,10 @@ GenericParameters<.List/*!*/ typeArgs, bool allowVariance.> TypeParameter.TPVarianceSyntax variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; // assignment is to please compiler characteristics = new TypeParameter.TypeParameterCharacteristics(false); .) + // If a "<" combined with a Variance symbol could be a new token, then the parser here will need to be more complex, + // since, for example, a < followed immediately by a Variance symbol would scan as the wrong token. + // Fortunately that is not currently the case. + // (Only because we parse the new "<-" symbol as separate "<" "-" tokens precisely to avoid this issue :) "<" [ Variance (. if (!allowVariance) { SemErr(t, "type-parameter variance is not allowed to be specified in this context"); } .) ] @@ -4730,16 +4735,7 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression range = null; .) QuantifierVariableDecl (. qvars.Add(qv); .) - { // This predicate requires an explicit domain (<- C) or an explicit type (: T), - // to disambiguate comprehensions with multiple variables from comma-separated lists of expressions. - // The following will be parsed as two arguments to the print statement, as opposed to a single - // comprehension of two variables (and an invalid one to boot, since it would need an explicit term). - // - // print set x: x | E, y; - // - // This is partially due to the ambiguity of | as either a delimiter for a quantified variable range - // or a bitwise "or" operator. - IF(IsQuantifierVariableDecl(qv.Range != null)) + { IF(IsQuantifierVariableDecl(qv)) "," QuantifierVariableDecl (. qvars.Add(qv); .) } @@ -4749,11 +4745,15 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression /*------------------------------------------------------------------------*/ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allowLemma, bool allowLambda, bool allowBitwiseOps.> = (. - BoundVar/*!*/ bv; + IToken tok; + IToken id; + Type optType = null; Expression domain = null; Expression range = null; .) - IdentTypeOptional + WildIdent + [ ":" TypeAndToken + ] [ // "<-" can also appear in GenericParameters in something like "<-T>", // so we parse it as two separate tokens. "<" "-" @@ -4765,7 +4765,7 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow [ "|" Expression ] - (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.SyntacticType, domain, range); .) + (. qvar = new QuantifiedVar(id, id.val, optType == null ? new InferredTypeProxy() : optType, domain, range); .) . /*------------------------------------------------------------------------*/ diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 6a3ed8c03d0..e593d634809 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -108,6 +108,7 @@ public enum PrintModes { public bool WarnShadowing = false; public int DefiniteAssignmentLevel = 1; // [0..4] public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version3; + public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version3; public enum FunctionSyntaxOptions { Version3, @@ -117,6 +118,11 @@ public enum FunctionSyntaxOptions { ExperimentalPredicateAlwaysGhost, Version4, } + + public enum QuantifierSyntaxOptions { + Version3, + Version4, + } public bool ForbidNondeterminism { get { return DefiniteAssignmentLevel == 3; } @@ -454,6 +460,18 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { } return true; + case "quantifierSyntax": + if (ps.ConfirmArgumentCount(1)) { + if (args[ps.i] == "3") { + QuantifierSyntax = QuantifierSyntaxOptions.Version3; + } else if (args[ps.i] == "4") { + QuantifierSyntax = QuantifierSyntaxOptions.Version4; + } else { + InvalidArgumentError(name, ps); + } + } + return true; + case "countVerificationErrors": { int countErrors = 1; // defaults to reporting verification errors if (ps.GetIntArgument(ref countErrors, 2)) { diff --git a/Test/comp/ForallNewSyntax.dfy b/Test/comp/ForallNewSyntax.dfy new file mode 100644 index 00000000000..67cd3c24b54 --- /dev/null +++ b/Test/comp/ForallNewSyntax.dfy @@ -0,0 +1,356 @@ +// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t" +// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() { + var arrayTests := new ArrayTests(); + arrayTests.Run(); + + var multiArrayTests := new MultiArrayTests(); + multiArrayTests.Run(); + + var objectTests := new ObjectTests(); + objectTests.Run(); +} + +class ArrayTests { + var a: array + var b: array + + predicate Valid() reads this, a, b { + a.Length == 5 && b.Length == 5 + } + + constructor() ensures fresh(a) && fresh(b) && Valid() { + a := new int[5]; + b := new int[5]; + } + + method Initialize() modifies a, b { + forall i | 0 <= i < a.Length { + a[i] := i; + } + forall i | 0 <= i < b.Length { + b[i] := i; + } + } + + method Run() modifies a, b requires Valid() ensures Valid() { + BasicCases(); + WrongIndex(); + SequenceConversion(); + IndexCollection(); + Functions(); + } + + method BasicCases() modifies a, b requires Valid() ensures Valid() { + print "Arrays: Basic cases\n"; + + // Can sequentialize (compile as single loop): + forall i | 0 <= i < a.Length { + a[i] := i; + } + print a[..], "\n"; // [ 0, 1, 2, 3, 4 ]; + + // Can sequentialize + forall i | 0 <= i < a.Length { + b[i] := a[i]; + } + print b[..], "\n"; // [ 0, 1, 2, 3, 4 ]; + + // Can sequentialize + forall i | 0 <= i < a.Length && a[i] % 2 == 0 { + a[i] := a[i] * 2; + } + print a[..], "\n"; // [ 0, 1, 4, 3, 8 ]; + } + + method WrongIndex() modifies a, b requires Valid() ensures Valid() { + print "\nArrays: Wrong index\n"; + + // Can't sequentialize: different index in RHS + Initialize(); + forall i | 1 <= i < a.Length { + a[i] := a[i - 1]; + } + print a[..], "\n"; // [ 0, 0, 1, 2, 3 ]; + + // Can't sequentialize: different index in LHS + Initialize(); + forall i | 0 <= i < a.Length - 1 { + a[i + 1] := a[i]; + } + print a[..], "\n"; // [ 0, 0, 1, 2, 3 ]; + + // Can't sequentialize: wrong array access in range + Initialize(); + forall i | 0 <= i < a.Length && (i == 0 || i != a[0]) { + a[i] := a[i] + 1; + } + print a[..], "\n"; // [ 1, 2, 3, 4, 5 ] + } + + method SequenceConversion() modifies a, b requires Valid() ensures Valid() { + print "\nArrays: Sequence conversion\n"; + + // Can't sequentialize: sequence conversion in range + Initialize(); + forall i | 0 <= i < a.Length && (i == 0 || i !in a[..2]) { + a[i] := a[i] + 2; + } + print a[..], "\n"; // [ 2, 1, 4, 5, 6 ] + + // Can't sequentialize: sequence conversion in RHS + Initialize(); + forall i | 1 <= i < a.Length - 1 { + a[i] := |a[i-1..i+2]|; + } + print a[..], "\n"; // [ 0, 3, 3, 3, 4 ] + } + + method IndexCollection() modifies a, b requires Valid() ensures Valid() { + print "\nArrays: Index collection\n"; + + // Can sequentialize: range collection passes through UniqueValues() + Initialize(); + forall i <- [ 0, 0, 0 ] { + a[i] := a[i] + 1; + } + print a[..], "\n"; // [ 1, 1, 2, 3, 4 ] + + // Can sequentialize + Initialize(); + forall i <- { 0, 0, 0 } { + a[i] := a[i] + 1; + } + print a[..], "\n"; // [ 1, 1, 2, 3, 4 ] + + // TODO add case that can't be sequentialized + } + + method Functions() modifies a, b requires Valid() ensures Valid() { + print "\nArrays: Functions\n"; + + var f: int -> int := x => x + 1; + + // Can sequentialize: function is pure + Initialize(); + forall i | 0 <= i < a.Length && a[i] != f(0) { + a[i] := f(a[i]); + } + print a[..], "\n"; // [ 1, 1, 3, 4, 5 ]; + + // Can sequentialize: function is pure + Initialize(); + forall i | 0 <= i < a.Length && a[i] != f(0) { + a[i] := f(a[i]); + } + print a[..], "\n"; // [ 1, 1, 3, 4, 5 ]; + + var g: int ~> int := x reads this, a, b requires Valid() => x + a[1]; + + // Can't sequentialize: impure function call in range + Initialize(); + forall i | 0 <= i < a.Length && a[i] != g(2) { + a[i] := i + 1; + } + print a[..], "\n"; // [ 1, 2, 3, 3, 5 ] + + // Can't sequentialize: impure function call in RHS + Initialize(); + forall i | 0 <= i < a.Length { + a[i] := g(i); + } + print a[..], "\n"; // [ 1, 2, 3, 4, 5 ] + } +} + +class MultiArrayTests { + var a: array2 + + predicate Valid() reads this, a { + a.Length0 == 3 && a.Length1 == 3 + } + + constructor() ensures fresh(a) && Valid() { + a := new int[3,3]; + } + + function method StateAsSeq(): seq> reads this, a requires Valid() { + [ [ a[0,0], a[0,1], a[0,2] ], + [ a[1,0], a[1,1], a[1,2] ], + [ a[2,0], a[2,1], a[2,2] ] ] + } + + method Report() requires Valid() ensures Valid() { + print StateAsSeq(), "\n"; + } + + method Run() modifies a requires Valid() ensures Valid() { + print "\nMulti-dimensional arrays\n"; + + // Can sequentialize + forall i | 0 <= i < a.Length0, + j | 0 <= j < a.Length1 + { + a[i,j] := i + 2 * j; + } + Report(); // [[0, 2, 4], [1, 3, 5], [2, 4, 6]] + + // Can't sequentialize + forall i | 0 <= i < a.Length0, + j | 0 <= j < a.Length1 + { + a[i,j] := a[j,i]; + } + Report(); // [[0, 1, 2], [2, 3, 4], [4, 5, 6]]; + } +} + +class Thing { + var i: int + var r: real + var t: Thing? + + constructor(i: int, r: real, t: Thing?) ensures this.i == i && this.r == r && this.t == t { + this.i := i; + this.r := r; + this.t := t; + } + + method Print() { + print "(", i, ", ", r, ")"; + } + + static method PrintMany(things: seq) { + print "["; + var i := 0; + var sep := ""; + while i < |things| decreases |things| - i { + print sep; + things[i].Print(); + i := i + 1; + sep := ", "; + } + print "]"; + } +} + +class ObjectTests { + var thing1: Thing, thing2: Thing, thing3: Thing + + predicate Valid() reads this { + thing1 != thing2 && thing1 != thing3 && thing2 != thing3 + } + + constructor() ensures fresh(thing1) && fresh(thing2) && fresh(thing3) && Valid() { + thing1 := new Thing(1, 1.0, null); + thing2 := new Thing(2, 2.0, null); + thing3 := new Thing(3, 3.0, null); + } + + method Initialize() modifies thing1, thing2, thing3 requires Valid() ensures Valid() { + thing1.i := 1; thing1.r := 1.0; thing1.t := null; + thing2.i := 2; thing2.r := 2.0; thing2.t := null; + thing3.i := 3; thing3.r := 3.0; thing3.t := null; + } + + method Report() { + Thing.PrintMany([ thing1, thing2, thing3 ]); + print "\n"; + } + + method Run() modifies thing1, thing2, thing3 requires Valid() ensures Valid() { + BasicCases(); + BadFieldAccesses(); + Functions(); + } + + method BasicCases() modifies thing1, thing2, thing3 requires Valid() ensures Valid() { + print "\nObjects: Basic cases\n"; + var things: seq := [ thing1, thing2, thing3 ]; + + // Can sequentialize + Initialize(); + forall t <- things { + t.i := 0; + } + Report(); // [(0, 1.0), (0, 2.0), (0, 3.0)] + + // Can sequentialize + Initialize(); + forall t <- things | t.r != 2.0 { + t.i := t.i + 1; + } + Report(); // [(2, 1.0), (2, 2.0), (4, 3.0)] + + // Can sequentialize + Initialize(); + forall t <- things | t.i != 3 { + t.i := t.i + 1; + } + Report(); // [(2, 1.0), (3, 2.0), (3, 3.0)] + } + + method BadFieldAccesses() modifies thing1, thing2, thing3 requires Valid() ensures Valid() { + print "\nObjects: Bad field accesses\n"; + var things: seq := [ thing1, thing2, thing3 ]; + + // Can't sequentialize: bad field access in range + Initialize(); + thing2.t := thing1; + forall t <- things | (t.t == null || t.t.i == 1) { + t.i := t.i + 1; + } + Report(); // [(2, 1.0), (3, 2.0), (4, 3.0)] + + // Can't sequentialize: bad field access in RHS + Initialize(); + forall t <- things { + t.i := thing1.i + 1; + } + Report(); // [(2, 1.0), (2, 2.0), (2, 3.0)] + + // Can't sequentialize: wrong object in update + Initialize(); + thing1.t := thing3; + thing2.t := thing1; + thing3.t := thing2; + forall t <- things { + t.t.i := t.i; + } + Report(); // [(2, 1.0), (3, 2.0), (1, 3.0)] + } + + method Functions() modifies thing1, thing2, thing3 requires Valid() ensures Valid() { + print "\nObjects: Functions\n"; + var things: seq := [ thing1, thing2, thing3 ]; + + var f: int -> int := x => x * 2; + + // Can sequentialize: function is pure + Initialize(); + forall t <- things { + t.i := f(t.i); + } + Report(); // [(2, 1.0), (4, 2.0), (6, 3.0)] + + var g: () ~> int := () reads this, thing2 => thing2.i; + + // Can't sequentialize: impure function call in range + Initialize(); + forall t <- things | t.i + g() != 5 { + t.i := t.i + 1; + } + Report(); // [(2, 1.0), (3, 2.0), (3, 3.0)] + + // Can't sequentialize: impure function call in RHS + Initialize(); + forall t <- things { + t.i := t.i + g(); + } + Report(); // [(3, 1.0), (4, 2.0), (5, 3.0)]; + } +} diff --git a/Test/comp/ForallNewSyntax.dfy.expect b/Test/comp/ForallNewSyntax.dfy.expect new file mode 100644 index 00000000000..b79a345bbc6 --- /dev/null +++ b/Test/comp/ForallNewSyntax.dfy.expect @@ -0,0 +1,176 @@ + +Dafny program verifier finished with 25 verified, 0 errors +Arrays: Basic cases +[0, 1, 2, 3, 4] +[0, 1, 2, 3, 4] +[0, 1, 4, 3, 8] + +Arrays: Wrong index +[0, 0, 1, 2, 3] +[0, 0, 1, 2, 3] +[1, 2, 3, 4, 5] + +Arrays: Sequence conversion +[2, 1, 4, 5, 6] +[0, 3, 3, 3, 4] + +Arrays: Index collection +[1, 1, 2, 3, 4] +[1, 1, 2, 3, 4] + +Arrays: Functions +[1, 1, 3, 4, 5] +[1, 1, 3, 4, 5] +[1, 2, 3, 3, 5] +[1, 2, 3, 4, 5] + +Multi-dimensional arrays +[[0, 2, 4], [1, 3, 5], [2, 4, 6]] +[[0, 1, 2], [2, 3, 4], [4, 5, 6]] + +Objects: Basic cases +[(0, 1.0), (0, 2.0), (0, 3.0)] +[(2, 1.0), (2, 2.0), (4, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] + +Objects: Bad field accesses +[(2, 1.0), (3, 2.0), (4, 3.0)] +[(2, 1.0), (2, 2.0), (2, 3.0)] +[(2, 1.0), (3, 2.0), (1, 3.0)] + +Objects: Functions +[(2, 1.0), (4, 2.0), (6, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] +[(3, 1.0), (4, 2.0), (5, 3.0)] + +Dafny program verifier finished with 25 verified, 0 errors +Arrays: Basic cases +[0, 1, 2, 3, 4] +[0, 1, 2, 3, 4] +[0, 1, 4, 3, 8] + +Arrays: Wrong index +[0, 0, 1, 2, 3] +[0, 0, 1, 2, 3] +[1, 2, 3, 4, 5] + +Arrays: Sequence conversion +[2, 1, 4, 5, 6] +[0, 3, 3, 3, 4] + +Arrays: Index collection +[1, 1, 2, 3, 4] +[1, 1, 2, 3, 4] + +Arrays: Functions +[1, 1, 3, 4, 5] +[1, 1, 3, 4, 5] +[1, 2, 3, 3, 5] +[1, 2, 3, 4, 5] + +Multi-dimensional arrays +[[0, 2, 4], [1, 3, 5], [2, 4, 6]] +[[0, 1, 2], [2, 3, 4], [4, 5, 6]] + +Objects: Basic cases +[(0, 1.0), (0, 2.0), (0, 3.0)] +[(2, 1.0), (2, 2.0), (4, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] + +Objects: Bad field accesses +[(2, 1.0), (3, 2.0), (4, 3.0)] +[(2, 1.0), (2, 2.0), (2, 3.0)] +[(2, 1.0), (3, 2.0), (1, 3.0)] + +Objects: Functions +[(2, 1.0), (4, 2.0), (6, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] +[(3, 1.0), (4, 2.0), (5, 3.0)] + +Dafny program verifier finished with 25 verified, 0 errors +Arrays: Basic cases +[0, 1, 2, 3, 4] +[0, 1, 2, 3, 4] +[0, 1, 4, 3, 8] + +Arrays: Wrong index +[0, 0, 1, 2, 3] +[0, 0, 1, 2, 3] +[1, 2, 3, 4, 5] + +Arrays: Sequence conversion +[2, 1, 4, 5, 6] +[0, 3, 3, 3, 4] + +Arrays: Index collection +[1, 1, 2, 3, 4] +[1, 1, 2, 3, 4] + +Arrays: Functions +[1, 1, 3, 4, 5] +[1, 1, 3, 4, 5] +[1, 2, 3, 3, 5] +[1, 2, 3, 4, 5] + +Multi-dimensional arrays +[[0, 2, 4], [1, 3, 5], [2, 4, 6]] +[[0, 1, 2], [2, 3, 4], [4, 5, 6]] + +Objects: Basic cases +[(0, 1.0), (0, 2.0), (0, 3.0)] +[(2, 1.0), (2, 2.0), (4, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] + +Objects: Bad field accesses +[(2, 1.0), (3, 2.0), (4, 3.0)] +[(2, 1.0), (2, 2.0), (2, 3.0)] +[(2, 1.0), (3, 2.0), (1, 3.0)] + +Objects: Functions +[(2, 1.0), (4, 2.0), (6, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] +[(3, 1.0), (4, 2.0), (5, 3.0)] + +Dafny program verifier finished with 25 verified, 0 errors +Arrays: Basic cases +[0, 1, 2, 3, 4] +[0, 1, 2, 3, 4] +[0, 1, 4, 3, 8] + +Arrays: Wrong index +[0, 0, 1, 2, 3] +[0, 0, 1, 2, 3] +[1, 2, 3, 4, 5] + +Arrays: Sequence conversion +[2, 1, 4, 5, 6] +[0, 3, 3, 3, 4] + +Arrays: Index collection +[1, 1, 2, 3, 4] +[1, 1, 2, 3, 4] + +Arrays: Functions +[1, 1, 3, 4, 5] +[1, 1, 3, 4, 5] +[1, 2, 3, 3, 5] +[1, 2, 3, 4, 5] + +Multi-dimensional arrays +[[0, 2, 4], [1, 3, 5], [2, 4, 6]] +[[0, 1, 2], [2, 3, 4], [4, 5, 6]] + +Objects: Basic cases +[(0, 1.0), (0, 2.0), (0, 3.0)] +[(2, 1.0), (2, 2.0), (4, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] + +Objects: Bad field accesses +[(2, 1.0), (3, 2.0), (4, 3.0)] +[(2, 1.0), (2, 2.0), (2, 3.0)] +[(2, 1.0), (3, 2.0), (1, 3.0)] + +Objects: Functions +[(2, 1.0), (4, 2.0), (6, 3.0)] +[(2, 1.0), (3, 2.0), (3, 3.0)] +[(3, 1.0), (4, 2.0), (5, 3.0)] diff --git a/Test/comp/NewSyntaxComprehensions.dfy b/Test/comp/NewSyntaxComprehensions.dfy new file mode 100644 index 00000000000..23c89021d3c --- /dev/null +++ b/Test/comp/NewSyntaxComprehensions.dfy @@ -0,0 +1,284 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() { + Quantifier(); + MapComprehension(); + OutParamsUnderLambdas(); // white-box testing + SetComprehension(); + Enumerations(); + EnumerationsMaybeNull(); + TestImplicitTypeTests.Test(); +} + +predicate method Thirteen(x: int) { x == 13 } +predicate method Even(y: int) { y % 2 == 1 } +function method FourMore(x: int): int { x + 4 } + +method Quantifier() { + // Note, by making *two* assignments to "s" (instead of the obvious one), the direct translation + // into Java makes "s" NOT be "effectively final". This means that Java does not allow "s" to be + // used in the lambda expression into which the quantifier translates. Compilation into Java + // thus needs to capture the value of "s" into another variable, which these tests check on. + var s := [0, 1, 1, 2]; + s := s + [3, 5, 8, 13]; + print forall x <- s :: x < 20, " "; // true + print forall x <- s :: x < 10, "\n"; // false + print exists x <- s :: x == 3, " "; // true + print exists x <- s :: x == 4, "\n"; // false +} + +method MapComprehension() { + var s := [12, 13, 14]; + var m := map x <- s :: x / 2; + print m, "\n"; + m := map x <- s :: FourMore(x) := x; + print m, "\n"; +} + +method OutParamsUnderLambdas() { + var x, b := XP(); + print "XP returned: ", x, " ", b, "\n"; + var m := XM(); + print "XM returned: ", m, "\n"; +} + +method XP() returns (x: int, b: bool) { + var s := {2, 4}; + b := exists y <- s :: y < x; +} + + +method XM() returns (x: int) { + var before, after; + + var f := () => x; + before := f(); + x := 2; + after := f(); + print "after: ", f(), " ", "before: ", f(), "\n"; + + f := () => x; + before := f(); + x := 16; + after := f(); + print "after: ", f(), " ", "before: ", f(), "\n"; +} + +trait NothingInParticular { } +class ClassA { } +class ClassB extends NothingInParticular { } + +method SetComprehension() { + SetComprehension0(); + SetComprehension1(); + SetComprehension2(); + SetComprehension3(); +} + +method SetComprehension0() { + var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; + var s := {w, x, y, z}; + // The following set comprehension picks att elements in s: + var all := set o: object <- s; + // The next set comprehension picks out 2 of the elements in s: + var aa := set o: ClassA <- s; + // The next set comprehension picks out the other 2 of the elements in s: + var bb := set o: ClassB <- s; + // The following picks out the same elements as in bb: + var nn := set o: NothingInParticular <- s; + + print |s|, " ", |all|, " "; // 4 4 + print |aa|, " ", |bb|, " "; // 2 2 + print |aa * bb|, " ", |aa + bb|, " "; // 0 4 + print |nn|, " ", bb == nn, "\n"; // 2 true +} + +// SetComprehension1 is like SetComprehension0, but also adds "null" to "s". +method SetComprehension1() { + var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; + var s := {w, x, y, z, null}; + // The following set comprehension picks att elements in s: + var all := set o: object <- s; + // The next set comprehension picks out 2 of the elements in s: + var aa := set o: ClassA <- s; + // The next set comprehension picks out the other 2 of the elements in s: + var bb := set o: ClassB <- s; + // The following picks out the same elements as in bb: + var nn := set o: NothingInParticular <- s; + + print |s|, " ", |all|, " "; // 5 4 + print |aa|, " ", |bb|, " "; // 2 2 + print |aa * bb|, " ", |aa + bb|, " "; // 0 4 + print |nn|, " ", bb == nn, "\n"; // 2 true +} + +// SetComprehension2 is like SetComprehension1, but uses maybe-null types in comprehensions +method SetComprehension2() { + var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; + var s := {w, x, y, z, null}; + // The following set comprehension picks att elements in s: + var all := set o: object? <- s; + // The next set comprehension picks out 2 of the elements in s: + var aa := set o: ClassA? <- s; + // The next set comprehension picks out the other 2 of the elements in s: + var bb := set o: ClassB? <- s; + // The following picks out the same elements as in bb: + var nn := set o: NothingInParticular? <- s; + + print |s|, " ", |all|, " "; // 5 5 + print |aa|, " ", |bb|, " "; // 3 3 + print |aa * bb|, " ", |aa + bb|, " "; // 1 5 + print |nn|, " ", bb == nn, "\n"; // 3 true +} + +datatype Color = Red | Green | Blue + +predicate method True(g: G) { true } + +method SetComprehension3() { + var s: set := {false, true}; + // The following set comprehension picks att elements in s: + var all := set o: bool <- s; + var aa := set o: bool <- s | !o; + var bb := set o: bool <- s | o; + + print |s|, " ", |all|, " "; // 2 2 + print |aa|, " ", |bb|, " "; // 1 1 + print |aa * bb|, " ", |aa + bb|, " "; // 0 2 + print aa == all, " ", aa <= all, "\n"; // false true + + var d := set z: Color | True(z); + var e := set z: Color | z in d; + print |d|, " ", |e|, "\n"; // 3 3 +} + +trait ICell { var data: int } +class CellA extends ICell { } +class CellB extends ICell { } + +method Enumerations() { + var c, d, e := new CellA, new CellA, new CellB; + c.data, d.data, e.data := 4, 5, 1; + var s: set := {c, d, e, null}; + print c.data, d.data, e.data, "\n"; // 451 + + // non-sequentialized forall statement + forall a: CellA <- s { + a.data := c.data + a.data - 2; + } + print c.data, d.data, e.data, "\n"; // 671 + + // sequentialized forall statement + forall a: CellA <- s { + a.data := 2; + } + print c.data, d.data, e.data, "\n"; // 221 + + // assign-such-that statement + d.data := 9; + assert d in s; + var u: CellA :| u in s && 7 <= u.data; + u.data := 8; + print c.data, d.data, e.data, "\n"; // 281 + + // set comprehension + var r := set a: CellA <- s | a.data < 6; + print |r|, "\n"; // 1 + + // map comprehension + var m := map a: CellA <- s | a.data < 6 :: 3; + print c in m.Keys, " ", d in m.Keys, " ", |m.Keys|, "\n"; // true false 1 +} + +method EnumerationsMaybeNull() { + var c, d, e := new CellA, new CellA, new CellB; + c.data, d.data, e.data := 4, 5, 1; + var s: set := {c, d, e, null}; + print c.data, d.data, e.data, "\n"; // 451 + + // non-sequentialized forall statement + forall a: CellA? <- s { + (if a == null then c else a).data := c.data + (if a == null then c else a).data - 2; + } + print c.data, d.data, e.data, "\n"; // 671 + + // sequentialized forall statement + forall a: CellA? <- s { + (if a == null then c else a).data := 2; + } + print c.data, d.data, e.data, "\n"; // 221 + + // assign-such-that statement + d.data := 9; + assert d in s; + var u: CellA? :| u in s && u != null && 7 <= u.data; + u.data := 8; + print c.data, d.data, e.data, "\n"; // 281 + + // set comprehension + var r := set a: CellA? <- s | (a == null || a.data < 6); + print |r|, "\n"; // 2 + + // map comprehension + var m := map a: CellA? <- s | (a == null || a.data < 6) :: 3; + print null in m.Keys, " ", c in m.Keys, " ", d in m.Keys, " ", |m.Keys|, "\n"; // true true false 2 +} + +module TestImplicitTypeTests { + trait A {} + trait B extends A {} + class C extends B {} + class A' extends A {} + class B' extends B {} + + method Test() { + var o, a, b, c := new object, new A', new B', new C; + var r: set := {o, a, b, c}; + var s: set := set x: A <- r; + var t: set := set x: B <- s; + var u: set := set x: C <- s; + print |r|, " ", |s|, " ", |t|, " ", |u|, "\n"; // 4 3 2 1 + print r == set x <- r | x is object, " "; // true + print s == set x <- r | x is A, " "; // true + print t == set x <- r | x is B, " "; // true + print u == set x <- r | x is C, "\n"; // true + + var r': set := r; + var s': set := s; + var t': set := t; + var u': set := u; + print |r'|, " ", |s'|, " ", |t'|, " ", |u'|, "\n"; // 4 3 2 1 + print r' == set x <- r | x is object, " "; // true + print s' == set x <- r | x is A, " "; // true + print t' == set x <- r | x is B, " "; // true + print u' == set x <- r | x is C, "\n"; // true + + r', s', t', u' := r' + {null}, s' + {null}, t' + {null}, u' + {null}; + print r' == set x <- r | x is object, " "; // false + print s' == set x <- r | x is A, " "; // false + print t' == set x <- r | x is B, " "; // false + print u' == set x <- r | x is C, "\n"; // false + print r' == set x <- r | x is object?, " "; // false + print s' == set x <- r | x is A?, " "; // false + print t' == set x <- r | x is B?, " "; // false + print u' == set x <- r | x is C?, "\n"; // false + + print r == set x <- r' | x is object, " "; // true + print s == set x <- r' | x is A, " "; // true + print t == set x <- r' | x is B, " "; // true + print u == set x <- r' | x is C, "\n"; // true + print r == set x <- r' | x is object?, " "; // false + print s == set x <- r' | x is A?, " "; // false + print t == set x <- r' | x is B?, " "; // false + print u == set x <- r' | x is C?, "\n"; // false + print r == set x <- r' | x is object? && x != null, " "; // true + print s == set x <- r' | x is A? && x != null, " "; // true + print t == set x <- r' | x is B? && x != null, " "; // true + print u == set x <- r' | x is C? && x != null, "\n"; // true + } +} diff --git a/Test/comp/NewSyntaxComprehensions.dfy.expect b/Test/comp/NewSyntaxComprehensions.dfy.expect new file mode 100644 index 00000000000..744e06331fc --- /dev/null +++ b/Test/comp/NewSyntaxComprehensions.dfy.expect @@ -0,0 +1,242 @@ + +Dafny program verifier finished with 27 verified, 0 errors + +Dafny program verifier did not attempt verification +x=13 y=14 +x=13 y=14 b=yes +true false +true false +map[12 := 6, 13 := 6, 14 := 7] +map[16 := 12, 17 := 13, 18 := 14] +false false false false +true true true true +XP returned: 0 false +after: 0 before: 0 +after: 2 before: 2 +XM returned: 16 +0 12 3 8 +0 12 3 8 +0 12 3 8 +0 12 3 8 +[1, 1, 1, 1] +[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] +[0, 1, 4, 9, 16, 25, 36, 49] +[0, 1, 2, 3, 4, 5, 6, 7] +4 4 2 2 0 4 2 true +5 4 2 2 0 4 2 true +5 5 3 3 1 5 3 true +2 2 1 1 0 2 false true +3 3 +451 +671 +221 +281 +1 +true false 1 +451 +671 +221 +281 +2 +true true false 2 +the intersection is {null} +there are 3 elements in the union +true true true +false false false +true true true +false false false +4 3 2 1 +true true true true +4 3 2 1 +true true true true +false false false false +false false false false +true true true true +false false false false +true true true true +false true +false true +null +false true +true true +3 + +Dafny program verifier did not attempt verification +x=13 y=14 +x=13 y=14 b=yes +true false +true false +map[12 := 6, 13 := 6, 14 := 7] +map[16 := 12, 17 := 13, 18 := 14] +false false false false +true true true true +XP returned: 0 false +after: 0 before: 0 +after: 2 before: 2 +XM returned: 16 +0 12 3 8 +0 12 3 8 +0 12 3 8 +0 12 3 8 +[1, 1, 1, 1] +[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] +[0, 1, 4, 9, 16, 25, 36, 49] +[0, 1, 2, 3, 4, 5, 6, 7] +4 4 2 2 0 4 2 true +5 4 2 2 0 4 2 true +5 5 3 3 1 5 3 true +2 2 1 1 0 2 false true +3 3 +451 +671 +221 +281 +1 +true false 1 +451 +671 +221 +281 +2 +true true false 2 +the intersection is {null} +there are 3 elements in the union +true true true +false false false +true true true +false false false +4 3 2 1 +true true true true +4 3 2 1 +true true true true +false false false false +false false false false +true true true true +false false false false +true true true true +false true +false true +null +false true +true true +3 + +Dafny program verifier did not attempt verification +x=13 y=14 +x=13 y=14 b=yes +true false +true false +map[12 := 6, 13 := 6, 14 := 7] +map[16 := 12, 17 := 13, 18 := 14] +false false false false +true true true true +XP returned: 0 false +after: 0 before: 0 +after: 2 before: 2 +XM returned: 16 +0 12 3 8 +0 12 3 8 +0 12 3 8 +0 12 3 8 +[1, 1, 1, 1] +[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] +[0, 1, 4, 9, 16, 25, 36, 49] +[0, 1, 2, 3, 4, 5, 6, 7] +4 4 2 2 0 4 2 true +5 4 2 2 0 4 2 true +5 5 3 3 1 5 3 true +2 2 1 1 0 2 false true +3 3 +451 +671 +221 +281 +1 +true false 1 +451 +671 +221 +281 +2 +true true false 2 +the intersection is {null} +there are 3 elements in the union +true true true +false false false +true true true +false false false +4 3 2 1 +true true true true +4 3 2 1 +true true true true +false false false false +false false false false +true true true true +false false false false +true true true true +false true +false true +null +false true +true true +3 + +Dafny program verifier did not attempt verification +x=13 y=14 +x=13 y=14 b=yes +true false +true false +map[12 := 6, 13 := 6, 14 := 7] +map[16 := 12, 17 := 13, 18 := 14] +false false false false +true true true true +XP returned: 0 false +after: 0 before: 0 +after: 2 before: 2 +XM returned: 16 +0 12 3 8 +0 12 3 8 +0 12 3 8 +0 12 3 8 +[1, 1, 1, 1] +[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] +[0, 1, 4, 9, 16, 25, 36, 49] +[0, 1, 2, 3, 4, 5, 6, 7] +4 4 2 2 0 4 2 true +5 4 2 2 0 4 2 true +5 5 3 3 1 5 3 true +2 2 1 1 0 2 false true +3 3 +451 +671 +221 +281 +1 +true false 1 +451 +671 +221 +281 +2 +true true false 2 +the intersection is {null} +there are 3 elements in the union +true true true +false false false +true true true +false false false +4 3 2 1 +true true true true +4 3 2 1 +true true true true +false false false false +false false false false +true true true true +false false false false +true true true true +false true +false true +null +false true +true true +3 diff --git a/Test/dafny0/ForallCompilationNewSyntax.dfy b/Test/dafny0/ForallCompilationNewSyntax.dfy new file mode 100644 index 00000000000..9391a7e60c3 --- /dev/null +++ b/Test/dafny0/ForallCompilationNewSyntax.dfy @@ -0,0 +1,104 @@ +// RUN: %dafny /compile:3 /quantifierSyntax:4 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() { + var c := new MyClass; + c.arr := new int[10,20]; + c.K0(3, 12); + c.K1(3, 12); + c.K2(3, 12); + c.K3(3, 12); + c.K4(12); + c.M(); + c.N(); + c.P(); + c.Q(); +} + +class MyClass +{ + var arr: array2 + + method K0(i: int, j: int) + requires 0 <= i < arr.Length0 && 0 <= j < arr.Length1 + modifies arr + { + forall k <- {-3, 4} { + arr[i,j] := 50; + } + } + + method K1(i: int, j: int) + requires 0 <= i < arr.Length0 && 0 <= j < arr.Length1 + // note the absence of a modifies clause + { + forall k <- {} { + arr[i,j] := k; // fine, since control will never reach here + } + } + + method K2(i: int, j: int) + requires 0 <= i < arr.Length0 && 0 <= j < arr.Length1 + modifies arr + { + forall k <- {-3, 4} { + // The following would have been an error (since this test file tests + // compilation, we don't include the test here): + // arr[i,j] := k; // error: k can take on more than one value + } + } + + method K3(i: int, j: int) + requires 0 <= i < arr.Length0 && 0 <= j < arr.Length1 + modifies arr + { + forall k: nat <- {-3, 4} | k <= i { + arr[k,j] := 50; // fine, since k:nat is at least 0 + } + } + + method K4(j: int) + requires 0 <= j < arr.Length1 + modifies arr + { + forall i | 0 <= i < arr.Length0, k: nat <- {-3, 4} { + arr[i,j] := k; // fine, since k can only take on one value + } + } + + method M() + { + var ar := new int [3,3]; + var S: set := {2,0}; + forall k | k in S { + ar[k,1]:= 0; + } + forall k <- S, j <- S { + ar[k,j]:= 0; + } + } + + method N() { + var ar := new int[3, 3]; + ar[2,2] := 0; + } + + method P() { + var ar := new int[3]; + var prev := ar[..]; + var S: set := {}; + forall k <- S { + ar[k] := 0; + } + assert ar[..] == prev; + } + + method Q() { + var ar := new int[3,3]; + var S: set := {1,2}; + forall k <- S { + ar[0,0] := 0; + } + assert ar[0,0] == 0; + } +} diff --git a/Test/dafny0/ForallCompilationNewSyntax.dfy.expect b/Test/dafny0/ForallCompilationNewSyntax.dfy.expect new file mode 100644 index 00000000000..66ffe3665d5 --- /dev/null +++ b/Test/dafny0/ForallCompilationNewSyntax.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 14 verified, 0 errors diff --git a/Test/dafny0/NewSyntaxComprehensions.dfy b/Test/dafny0/NewSyntaxComprehensions.dfy new file mode 100644 index 00000000000..a588713e521 --- /dev/null +++ b/Test/dafny0/NewSyntaxComprehensions.dfy @@ -0,0 +1,191 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method M() +{ + var numbers := set i | 0 <= i && i < 100; + var squares := set i | 0 <= i && i < 100 :: Id(i)*i; // verifying properties about set comprehensions with a term expression is hard + + assert 12 in numbers; + assert Id(5) == 5; + assert 25 in squares; + assert 200 in numbers; // error +} + +function method Id(x: int): int { x } // for triggering + +datatype D = A | B +// The following mainly test that set comprehensions can be compiled, but one would +// have to run the resulting program to check that the compiler is doing the right thing. +method Main() +{ + var q := set i,j | 0 <= i < 10 && 0 <= j < 3 :: i+j; + PrintSet(q); + q := set b: bool :: if b then 3 else 7; + var d := set b:D; + var test := forall d:D {:nowarn} :: d == A || d == B; // Ignoring the warning as we're only compiling here + PrintSet(q); + var m := set k <- q :: 2*k; + PrintSet(m); + PrintSet(set k <- q | k % 2 == 0); + var sq := [30, 40, 20]; + PrintSet(set k <- sq, i | 0 <= i < k && i % 7 == 0 :: k + i); + var bb := forall k <- sq, i {:nowarn} | 0 <= i < k && i % 7 == 0 :: k + i == 17; // Ignoring the warning as we're only compiling here +} + +method PrintSet(s: set) { + var q := s; + while (q != {}) + decreases q; + { + var x :| x in q; + print x, " "; + q := q - {x}; + } + print "\n"; +} + +// ---------- Regression tests ---------- + +method SetComprehensionBoxAntecedents() +{ + // The first assert below used to not verify, due to a missing $IsBox conjunct in the Boogie lambda + // that encodes the set comprehension. + var a := set x <- {0,1,2,3,4,5} | x < 3; + var b := {0,1,2}; + + if + case true => + assert a == b; + case true => + assert forall x <- a :: x in b; + assert forall x <- b :: x in a; + case true => + assert forall x :: x in a <==> x in b; +} + +// ---------- Sequence operations ---------- + +method Sequences0() { + var four1s := [1, 1, 1, 1]; + var twelve1s := seq(12, _ => 1); + assert twelve1s == four1s + four1s + four1s; + + var squares := seq(8, i => i*i); + assert |squares| == 8; + assert squares[6] == 36; + if * { + assert squares[7] == 0; // error + } + + var nats := seq(8, i => i); +} + +class SeqOp { + var x: real + + function method G(i: nat): real + reads this + { + if i < 20 then 2.5 else x + } + function method H(i: nat): real + reads if i < 20 then {} else {this} + { + if i < 20 then 2.5 else x + } + + function method S0(n: nat): seq { + seq(n, G) // error: S0 reads {this} + } + function method S1(n: nat): seq + reads this + { + seq(n, G) + } + function method S2(n: nat): seq { + seq(n, H) // error: S2 reads {this} + } + function method S3(n: nat): seq + reads this + { + seq(n, H) + } + function method S4(n: nat): seq { + seq(n, i => if i < 20 then 2.5 else x) // error: lambda reads {this} + } + function method S5(n: nat): seq { + seq(n, i reads this => if i < 20 then 2.5 else x) // error: S5 reads {this} + } + function method S6(n: nat): seq + reads this + { + seq(n, i reads this => if i < 20 then 2.5 else x) + } + function method S7(n: nat): seq { + seq(n, i requires i < 20 => if i < 20 then 2.5 else x) // error: S7 violates lambda's precondition + } + + function method T0(n: nat): seq + requires n <= 20 + { + seq(n, G) // error: T0 reads {this} + } + function method T1(n: nat): seq + requires n <= 20 + reads this + { + seq(n, G) + } + function method T2(n: nat): seq + requires n <= 20 + { + seq(n, H) + } + function method T3(n: nat): seq + requires n <= 20 + { + seq(n, i reads this => if i < 20 then 2.5 else x) // error: T3 reads {this} + } + function method T4(n: nat): seq + requires n <= 20 + { + seq(n, i requires i < 20 => if i < 20 then 2.5 else x) + } + function method T5(n: nat): seq + requires n <= 20 + { + seq(n, i reads if i < 20 then {} else {this} => if i < 20 then 2.5 else x) + } + + function method XT0(n: nat): seq { + seq(n, _ => 7) + } + function method XT1(n: nat): seq { + seq(n, _ => 7) + } + function method XT2(n: nat): seq { + seq(n, _ => -7) // error: -7 is not a nat + } + function method XT3(n: nat): seq { + seq(n, _ => -7) // error: this is not a seq + } + function method XT4(n: nat): seq { + seq(n, i requires 0 <= i < 3 => 10) // error: init function doesn't accept all indices + } + function method XT5(n: nat): seq { + seq(n, i requires 0 <= i < n => 10) + } + function method XT6(n: nat): seq { + seq(n, i => if i < n then 10 else -7) // error: type of lambda is inferred to be int->nat, so the -7 gives an error + } + function method XT7(n: nat): seq { + seq(n, i => var u: int := if i < n then 10 else -7; u) // fine: lambda has type int->int; use of this lambda always gives a nat + } + function method XT8(n: nat): seq { + seq(n, i => if i < n then -7 else 10) // error: this can't be assigned to a seq + } + function method XT9(n: nat): seq { + seq(n, i => if i < n then -7 else 10) // error: this can't be assigned to a seq + } +} diff --git a/Test/dafny0/NewSyntaxComprehensions.dfy.expect b/Test/dafny0/NewSyntaxComprehensions.dfy.expect new file mode 100644 index 00000000000..49f10c37f5e --- /dev/null +++ b/Test/dafny0/NewSyntaxComprehensions.dfy.expect @@ -0,0 +1,23 @@ +Comprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(25,11): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. +Comprehensions.dfy(54,11): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +Comprehensions.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +Comprehensions.dfy(115,40): Error: insufficient reads clause to read field +Comprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +Comprehensions.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function +Comprehensions.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +Comprehensions.dfy(148,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +Comprehensions.dfy(168,16): Error: value does not satisfy the subset constraints of 'nat' +Comprehensions.dfy(171,11): Error: value does not satisfy the subset constraints of 'nat' +Comprehensions.dfy(174,4): Error: all sequence indices must be in the domain of the initialization function +Comprehensions.dfy(180,38): Error: value does not satisfy the subset constraints of 'nat' +Comprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat' +Comprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat' +Comprehensions.dfy(12,13): Error: assertion might not hold +Comprehensions.dfy(78,22): Error: assertion might not hold + +Dafny program verifier finished with 16 verified, 15 errors From d24a665b99749bc5932da40b0cea396f34eca55a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 31 May 2022 11:03:48 -0700 Subject: [PATCH 20/39] Enable IsGenericInstantiation lookahead outside expressions --- Source/Dafny/Dafny.atg | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index dbd5acae14c..d2ad7a3c3f7 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -534,13 +534,13 @@ bool IsNotEndOfCase() { */ bool IsGenericInstantiation(bool inExpressionContext) { scanner.ResetPeek(); - if (!inExpressionContext) { - return la.kind == _openAngleBracket; - } IToken pt = la; if (!IsTypeList(ref pt)) { return false; } + if (!inExpressionContext) { + return true; + } /* There are ambiguities in the parsing. For example: * F( a < b , c > (d) ) * can either be a unary function F whose argument is a function "a" with type arguments "" and @@ -4752,7 +4752,7 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow Expression range = null; .) WildIdent - [ ":" TypeAndToken + [ ":" TypeAndToken ] [ // "<-" can also appear in GenericParameters in something like "<-T>", // so we parse it as two separate tokens. From 7d44c6575b7f5e701dc9956ded4326aecc741474 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 31 May 2022 14:44:09 -0700 Subject: [PATCH 21/39] Various test/runtime fixes --- Source/Dafny/AST/DafnyAst.cs | 22 ++++- Source/Dafny/Compilers/SinglePassCompiler.cs | 1 + Source/DafnyRuntime/DafnyRuntime.go | 5 + .../src/main/java/dafny/DafnySequence.java | 4 + ...nsions.dfy => ComprehensionsNewSyntax.dfy} | 0 ...ect => ComprehensionsNewSyntax.dfy.expect} | 98 +------------------ .../dafny0/NewSyntaxComprehensions.dfy.expect | 42 ++++---- 7 files changed, 49 insertions(+), 123 deletions(-) rename Test/comp/{NewSyntaxComprehensions.dfy => ComprehensionsNewSyntax.dfy} (100%) rename Test/comp/{NewSyntaxComprehensions.dfy.expect => ComprehensionsNewSyntax.dfy.expect} (57%) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 3dfd994b7ee..a5a14d2b96d 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6157,6 +6157,10 @@ public static void ExtractSingleRange(List qvars, out List/*?*/ lhs, Expression rhs, /// /// A ComprehensionExpr has the form: - /// BINDER x Attributes | Range(x) :: Term(x) - /// When BINDER is "forall" or "exists", the range may be "null" (which stands for the logical value "true"). - /// For other BINDERs (currently, "set"), the range is non-null. - /// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true". - /// Currently, BINDER is one of the logical quantifiers "exists" or "forall". + /// BINDER { x [: Type] [<- Domain] [Attributes] [| Range] } [:: Term(x)] + /// Where BINDER is currently "forall", "exists", "iset"/"set", or "imap"/"map". + /// + /// Quantifications used to only support a single range, but now each + /// quantified variable can have a range attached. + /// The overall Range is now filled in by the resolver by extracting any implicit + /// "x in Domain" constraints and per-variable Range constraints into a single conjunct. + /// + /// The Term is optional if the expression only has one quantified variable, + /// but required otherwise. + /// + /// LambdaExpr also inherits from this base class but isn't really a comprehension, + /// and should be considered implementation inheritance. /// public abstract class ComprehensionExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression { public virtual string WhatKind => "comprehension"; diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 4287ecbc8ff..c506dfc6f0e 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -3423,6 +3423,7 @@ Type CompileCollection(ComprehensionExpr.BoundedPool bound, IVariable bv, bool i var b = (ComprehensionExpr.MapBoundedPool)bound; TrParenExpr(su.Substitute(b.Map), collectionWriter, inLetExprBody, wStmts); GetSpecialFieldInfo(SpecialField.ID.Keys, null, null, out var keyName, out _, out _); + // TODO: Shouldn't this be UniqueElements? collectionWriter.Write($".{keyName}.Elements{propertySuffix}"); return b.CollectionElementType; } else if (bound is ComprehensionExpr.SeqBoundedPool) { diff --git a/Source/DafnyRuntime/DafnyRuntime.go b/Source/DafnyRuntime/DafnyRuntime.go index 7306c98fb5d..a7b667d116e 100644 --- a/Source/DafnyRuntime/DafnyRuntime.go +++ b/Source/DafnyRuntime/DafnyRuntime.go @@ -575,6 +575,11 @@ func (seq Seq) IsProperPrefixOf(seq2 Seq) bool { return sliceIsProperPrefixOf(seq.contents, seq2.contents) } +// Elements returns the sequence of elements (i.e. the sequence itself). +func (seq Seq) Elements() Seq { + return seq +} + // UniqueElements returns the set of elements in the sequence. func (seq Seq) UniqueElements() Set { return (*Builder)(&seq.contents).ToSet() diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java index 4cd4e893355..648c1c061c2 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java @@ -406,6 +406,10 @@ public String verbatimString(){ return builder.toString(); } + public Iterable Elements() { + return this; + } + public HashSet UniqueElements() { return new HashSet<>(asList()); } diff --git a/Test/comp/NewSyntaxComprehensions.dfy b/Test/comp/ComprehensionsNewSyntax.dfy similarity index 100% rename from Test/comp/NewSyntaxComprehensions.dfy rename to Test/comp/ComprehensionsNewSyntax.dfy diff --git a/Test/comp/NewSyntaxComprehensions.dfy.expect b/Test/comp/ComprehensionsNewSyntax.dfy.expect similarity index 57% rename from Test/comp/NewSyntaxComprehensions.dfy.expect rename to Test/comp/ComprehensionsNewSyntax.dfy.expect index 744e06331fc..6f7824bd366 100644 --- a/Test/comp/NewSyntaxComprehensions.dfy.expect +++ b/Test/comp/ComprehensionsNewSyntax.dfy.expect @@ -1,27 +1,15 @@ -Dafny program verifier finished with 27 verified, 0 errors +Dafny program verifier finished with 11 verified, 0 errors Dafny program verifier did not attempt verification -x=13 y=14 -x=13 y=14 b=yes true false true false map[12 := 6, 13 := 6, 14 := 7] map[16 := 12, 17 := 13, 18 := 14] -false false false false -true true true true XP returned: 0 false after: 0 before: 0 after: 2 before: 2 XM returned: 16 -0 12 3 8 -0 12 3 8 -0 12 3 8 -0 12 3 8 -[1, 1, 1, 1] -[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] -[0, 1, 4, 9, 16, 25, 36, 49] -[0, 1, 2, 3, 4, 5, 6, 7] 4 4 2 2 0 4 2 true 5 4 2 2 0 4 2 true 5 5 3 3 1 5 3 true @@ -39,12 +27,6 @@ true false 1 281 2 true true false 2 -the intersection is {null} -there are 3 elements in the union -true true true -false false false -true true true -false false false 4 3 2 1 true true true true 4 3 2 1 @@ -54,34 +36,16 @@ false false false false true true true true false false false false true true true true -false true -false true -null -false true -true true -3 Dafny program verifier did not attempt verification -x=13 y=14 -x=13 y=14 b=yes true false true false map[12 := 6, 13 := 6, 14 := 7] map[16 := 12, 17 := 13, 18 := 14] -false false false false -true true true true XP returned: 0 false after: 0 before: 0 after: 2 before: 2 XM returned: 16 -0 12 3 8 -0 12 3 8 -0 12 3 8 -0 12 3 8 -[1, 1, 1, 1] -[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] -[0, 1, 4, 9, 16, 25, 36, 49] -[0, 1, 2, 3, 4, 5, 6, 7] 4 4 2 2 0 4 2 true 5 4 2 2 0 4 2 true 5 5 3 3 1 5 3 true @@ -99,12 +63,6 @@ true false 1 281 2 true true false 2 -the intersection is {null} -there are 3 elements in the union -true true true -false false false -true true true -false false false 4 3 2 1 true true true true 4 3 2 1 @@ -114,34 +72,16 @@ false false false false true true true true false false false false true true true true -false true -false true -null -false true -true true -3 Dafny program verifier did not attempt verification -x=13 y=14 -x=13 y=14 b=yes true false true false map[12 := 6, 13 := 6, 14 := 7] map[16 := 12, 17 := 13, 18 := 14] -false false false false -true true true true XP returned: 0 false after: 0 before: 0 after: 2 before: 2 XM returned: 16 -0 12 3 8 -0 12 3 8 -0 12 3 8 -0 12 3 8 -[1, 1, 1, 1] -[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] -[0, 1, 4, 9, 16, 25, 36, 49] -[0, 1, 2, 3, 4, 5, 6, 7] 4 4 2 2 0 4 2 true 5 4 2 2 0 4 2 true 5 5 3 3 1 5 3 true @@ -159,12 +99,6 @@ true false 1 281 2 true true false 2 -the intersection is {null} -there are 3 elements in the union -true true true -false false false -true true true -false false false 4 3 2 1 true true true true 4 3 2 1 @@ -174,34 +108,16 @@ false false false false true true true true false false false false true true true true -false true -false true -null -false true -true true -3 Dafny program verifier did not attempt verification -x=13 y=14 -x=13 y=14 b=yes true false true false map[12 := 6, 13 := 6, 14 := 7] map[16 := 12, 17 := 13, 18 := 14] -false false false false -true true true true XP returned: 0 false after: 0 before: 0 after: 2 before: 2 XM returned: 16 -0 12 3 8 -0 12 3 8 -0 12 3 8 -0 12 3 8 -[1, 1, 1, 1] -[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] -[0, 1, 4, 9, 16, 25, 36, 49] -[0, 1, 2, 3, 4, 5, 6, 7] 4 4 2 2 0 4 2 true 5 4 2 2 0 4 2 true 5 5 3 3 1 5 3 true @@ -219,12 +135,6 @@ true false 1 281 2 true true false 2 -the intersection is {null} -there are 3 elements in the union -true true true -false false false -true true true -false false false 4 3 2 1 true true true true 4 3 2 1 @@ -234,9 +144,3 @@ false false false false true true true true false false false false true true true true -false true -false true -null -false true -true true -3 diff --git a/Test/dafny0/NewSyntaxComprehensions.dfy.expect b/Test/dafny0/NewSyntaxComprehensions.dfy.expect index 49f10c37f5e..9602a530b4b 100644 --- a/Test/dafny0/NewSyntaxComprehensions.dfy.expect +++ b/Test/dafny0/NewSyntaxComprehensions.dfy.expect @@ -1,23 +1,23 @@ -Comprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(25,11): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. -Comprehensions.dfy(54,11): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(115,40): Error: insufficient reads clause to read field -Comprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function -Comprehensions.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(148,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(168,16): Error: value does not satisfy the subset constraints of 'nat' -Comprehensions.dfy(171,11): Error: value does not satisfy the subset constraints of 'nat' -Comprehensions.dfy(174,4): Error: all sequence indices must be in the domain of the initialization function -Comprehensions.dfy(180,38): Error: value does not satisfy the subset constraints of 'nat' -Comprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat' -Comprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat' -Comprehensions.dfy(12,13): Error: assertion might not hold -Comprehensions.dfy(78,22): Error: assertion might not hold +NewSyntaxComprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on. +NewSyntaxComprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on. +NewSyntaxComprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on. +NewSyntaxComprehensions.dfy(25,11): Warning: /!\ No terms found to trigger on. +NewSyntaxComprehensions.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. +NewSyntaxComprehensions.dfy(54,11): Warning: /!\ No terms found to trigger on. +NewSyntaxComprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +NewSyntaxComprehensions.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +NewSyntaxComprehensions.dfy(115,40): Error: insufficient reads clause to read field +NewSyntaxComprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +NewSyntaxComprehensions.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function +NewSyntaxComprehensions.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +NewSyntaxComprehensions.dfy(148,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +NewSyntaxComprehensions.dfy(168,16): Error: value does not satisfy the subset constraints of 'nat' +NewSyntaxComprehensions.dfy(171,11): Error: value does not satisfy the subset constraints of 'nat' +NewSyntaxComprehensions.dfy(174,4): Error: all sequence indices must be in the domain of the initialization function +NewSyntaxComprehensions.dfy(180,38): Error: value does not satisfy the subset constraints of 'nat' +NewSyntaxComprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat' +NewSyntaxComprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat' +NewSyntaxComprehensions.dfy(12,13): Error: assertion might not hold +NewSyntaxComprehensions.dfy(78,22): Error: assertion might not hold Dafny program verifier finished with 16 verified, 15 errors From 2eef52a62d67f291a4bf81d2ad146dd7fcb23039 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 31 May 2022 14:46:34 -0700 Subject: [PATCH 22/39] Formatting --- Source/Dafny/AST/DafnyAst.cs | 12 ++++++------ Source/Dafny/DafnyOptions.cs | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index a5a14d2b96d..71e6241522b 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6127,12 +6127,12 @@ public BoundVar(IToken tok, string name, Type type) Contract.Requires(type != null); } } - + [DebuggerDisplay("Quantified<{name}>")] public class QuantifiedVar : BoundVar { public readonly Expression Domain; public readonly Expression Range; - + public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expression range) : base(tok, name, type) { Contract.Requires(tok != null); @@ -6145,16 +6145,16 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { bvars = new List(); range = null; - foreach(var qvar in qvars) { + foreach (var qvar in qvars) { BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); bvars.Add(bvar); if (qvar.Domain != null) { - var inDomainExpr = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain); - range = range == null ? inDomainExpr : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, inDomainExpr); + var inDomainExpr = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain); + range = range == null ? inDomainExpr : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, inDomainExpr); } if (qvar.Range != null) { - range = range == null ? qvar.Range : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); + range = range == null ? qvar.Range : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); } } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index e593d634809..aa31595b2f8 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -118,7 +118,7 @@ public enum FunctionSyntaxOptions { ExperimentalPredicateAlwaysGhost, Version4, } - + public enum QuantifierSyntaxOptions { Version3, Version4, From 85ebc3aaec7b6c2d186d1ec43a204756a44176d3 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 31 May 2022 14:49:08 -0700 Subject: [PATCH 23/39] Rename test --- ...nsions.dfy => ComprehensionsNewSyntax.dfy} | 0 .../dafny0/ComprehensionsNewSyntax.dfy.expect | 23 +++++++++++++++++++ .../dafny0/NewSyntaxComprehensions.dfy.expect | 23 ------------------- 3 files changed, 23 insertions(+), 23 deletions(-) rename Test/dafny0/{NewSyntaxComprehensions.dfy => ComprehensionsNewSyntax.dfy} (100%) create mode 100644 Test/dafny0/ComprehensionsNewSyntax.dfy.expect delete mode 100644 Test/dafny0/NewSyntaxComprehensions.dfy.expect diff --git a/Test/dafny0/NewSyntaxComprehensions.dfy b/Test/dafny0/ComprehensionsNewSyntax.dfy similarity index 100% rename from Test/dafny0/NewSyntaxComprehensions.dfy rename to Test/dafny0/ComprehensionsNewSyntax.dfy diff --git a/Test/dafny0/ComprehensionsNewSyntax.dfy.expect b/Test/dafny0/ComprehensionsNewSyntax.dfy.expect new file mode 100644 index 00000000000..92c90a3cc5d --- /dev/null +++ b/Test/dafny0/ComprehensionsNewSyntax.dfy.expect @@ -0,0 +1,23 @@ +ComprehensionsNewSyntax.dfy(6,17): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(22,11): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(24,7): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(25,11): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. +ComprehensionsNewSyntax.dfy(54,11): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +ComprehensionsNewSyntax.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +ComprehensionsNewSyntax.dfy(115,40): Error: insufficient reads clause to read field +ComprehensionsNewSyntax.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +ComprehensionsNewSyntax.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function +ComprehensionsNewSyntax.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +ComprehensionsNewSyntax.dfy(148,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor +ComprehensionsNewSyntax.dfy(168,16): Error: value does not satisfy the subset constraints of 'nat' +ComprehensionsNewSyntax.dfy(171,11): Error: value does not satisfy the subset constraints of 'nat' +ComprehensionsNewSyntax.dfy(174,4): Error: all sequence indices must be in the domain of the initialization function +ComprehensionsNewSyntax.dfy(180,38): Error: value does not satisfy the subset constraints of 'nat' +ComprehensionsNewSyntax.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat' +ComprehensionsNewSyntax.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat' +ComprehensionsNewSyntax.dfy(12,13): Error: assertion might not hold +ComprehensionsNewSyntax.dfy(78,22): Error: assertion might not hold + +Dafny program verifier finished with 16 verified, 15 errors diff --git a/Test/dafny0/NewSyntaxComprehensions.dfy.expect b/Test/dafny0/NewSyntaxComprehensions.dfy.expect deleted file mode 100644 index 9602a530b4b..00000000000 --- a/Test/dafny0/NewSyntaxComprehensions.dfy.expect +++ /dev/null @@ -1,23 +0,0 @@ -NewSyntaxComprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on. -NewSyntaxComprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on. -NewSyntaxComprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on. -NewSyntaxComprehensions.dfy(25,11): Warning: /!\ No terms found to trigger on. -NewSyntaxComprehensions.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. -NewSyntaxComprehensions.dfy(54,11): Warning: /!\ No terms found to trigger on. -NewSyntaxComprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -NewSyntaxComprehensions.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -NewSyntaxComprehensions.dfy(115,40): Error: insufficient reads clause to read field -NewSyntaxComprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -NewSyntaxComprehensions.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function -NewSyntaxComprehensions.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -NewSyntaxComprehensions.dfy(148,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -NewSyntaxComprehensions.dfy(168,16): Error: value does not satisfy the subset constraints of 'nat' -NewSyntaxComprehensions.dfy(171,11): Error: value does not satisfy the subset constraints of 'nat' -NewSyntaxComprehensions.dfy(174,4): Error: all sequence indices must be in the domain of the initialization function -NewSyntaxComprehensions.dfy(180,38): Error: value does not satisfy the subset constraints of 'nat' -NewSyntaxComprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat' -NewSyntaxComprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat' -NewSyntaxComprehensions.dfy(12,13): Error: assertion might not hold -NewSyntaxComprehensions.dfy(78,22): Error: assertion might not hold - -Dafny program verifier finished with 16 verified, 15 errors From 21ec6bbe75dc4e92955cabdffcce32840825353e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 1 Jun 2022 12:57:01 -0700 Subject: [PATCH 24/39] Improve resolution errors through token wrappers --- Source/Dafny/AST/DafnyAst.cs | 48 +++++++++++++++++-- Source/Dafny/DafnyOptions.cs | 2 +- Source/Dafny/Resolver.cs | 8 +++- Test/dafny0/QuantificationResolution.dfy | 14 ++++++ .../QuantificationResolution.dfy.expect | 0 5 files changed, 66 insertions(+), 6 deletions(-) create mode 100644 Test/dafny0/QuantificationResolution.dfy create mode 100644 Test/dafny0/QuantificationResolution.dfy.expect diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 71e6241522b..a2849afca1b 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6145,16 +6145,22 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { bvars = new List(); range = null; + var domainCloner = new QuantifiedVariableDomainCloner(); + var rangeCloner = new QuantifiedVariableRangeCloner(); + foreach (var qvar in qvars) { BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); bvars.Add(bvar); + if (qvar.Domain != null) { - var inDomainExpr = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), qvar.Domain); - range = range == null ? inDomainExpr : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, inDomainExpr); + var domainWithToken = domainCloner.CloneExpr(qvar.Domain); + var inDomainExpr = new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), domainWithToken); + range = range == null ? inDomainExpr : new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.And, range, inDomainExpr); } if (qvar.Range != null) { - range = range == null ? qvar.Range : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, range, qvar.Range); + var rangeWithToken = rangeCloner.CloneExpr(qvar.Range); + range = range == null ? qvar.Range : new BinaryExpr(rangeWithToken.tok, BinaryExpr.Opcode.And, range, rangeWithToken); } } @@ -9082,6 +9088,42 @@ public override string val { } } + public class QuantifiedVariableDomainToken : TokenWrapper { + public QuantifiedVariableDomainToken(IToken wrappedToken) + : base(wrappedToken) { + Contract.Requires(wrappedToken != null); + } + + public override string val { + get { return WrappedToken.val; } + set { WrappedToken.val = value; } + } + } + + public class QuantifiedVariableRangeToken : TokenWrapper { + public QuantifiedVariableRangeToken(IToken wrappedToken) + : base(wrappedToken) { + Contract.Requires(wrappedToken != null); + } + + public override string val { + get { return WrappedToken.val; } + set { WrappedToken.val = value; } + } + } + + class QuantifiedVariableDomainCloner : Cloner { + public override IToken Tok(IToken tok) { + return new QuantifiedVariableDomainToken(tok); + } + } + + class QuantifiedVariableRangeCloner : Cloner { + public override IToken Tok(IToken tok) { + return new QuantifiedVariableRangeToken(tok); + } + } + // ------------------------------------------------------------------------------------------------------ [DebuggerDisplay("{Printer.ExprToString(this)}")] public abstract class Expression { diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index aa31595b2f8..8a4987aab0c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1271,7 +1271,7 @@ public override void Error(string message, params string[] args) { /// class DafnyAttributeOptions : DafnyOptions { public static readonly HashSet KnownOptions = new() { - "functionSyntax" + "functionSyntax", "quantifierSyntax" }; private readonly Errors errors; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2c0d804a84f..003b8c3ec06 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -14996,7 +14996,9 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { case BinaryExpr.Opcode.And: case BinaryExpr.Opcode.Or: { ConstrainSubtypeRelation(Type.Bool, e.E0.Type, expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type); - ConstrainSubtypeRelation(Type.Bool, e.E1.Type, expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type); + var secondArgumentDescription = e.E1.tok is QuantifiedVariableRangeToken + ? "range of quantified variable" : "second argument to {0}"; + ConstrainSubtypeRelation(Type.Bool, e.E1.Type, expr, secondArgumentDescription + " must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type); expr.Type = Type.Bool; break; } @@ -15098,7 +15100,9 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { case BinaryExpr.Opcode.In: case BinaryExpr.Opcode.NotIn: - AddXConstraint(expr.tok, "Innable", e.E1.Type, e.E0.Type, "second argument to \"" + BinaryExpr.OpcodeString(e.Op) + "\" must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {0})"); + var subjectDescription = e.E1.tok is QuantifiedVariableDomainToken + ? "domain of quantified variable" : "second argument to \"" + BinaryExpr.OpcodeString(e.Op) + "\""; + AddXConstraint(expr.tok, "Innable", e.E1.Type, e.E0.Type, subjectDescription + " must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {0})"); expr.Type = Type.Bool; break; diff --git a/Test/dafny0/QuantificationResolution.dfy b/Test/dafny0/QuantificationResolution.dfy new file mode 100644 index 00000000000..045e3d9621d --- /dev/null +++ b/Test/dafny0/QuantificationResolution.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module {:options "/quantifierSyntax:4"} NewSyntax { + method M() + { + var _ := set x <- 5; + var _ := set x: int | 0 <= x < 10, y | "true" :: y; + var _ := set x <- [3], y | "true" :: y; + + // var numbers := [0, 1, 2, 3]; + // var _ := set x <- numbers | 0 < x, y | y == 6 / x :: y; + } +} \ No newline at end of file diff --git a/Test/dafny0/QuantificationResolution.dfy.expect b/Test/dafny0/QuantificationResolution.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d From cb979417a4f1351d29f2aad7aeb2fb59964b8c90 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 1 Jun 2022 16:20:13 -0700 Subject: [PATCH 25/39] Singletons, more tests --- Source/Dafny/AST/DafnyAst.cs | 12 ++++---- Test/dafny0/QuantificationNewSyntax.dfy | 22 ++++++++++++++ .../dafny0/QuantificationNewSyntax.dfy.expect | 8 +++++ Test/dafny0/QuantificationResolution.dfy | 29 +++++++++++++++++-- .../QuantificationResolution.dfy.expect | 26 +++++++++++++++++ 5 files changed, 89 insertions(+), 8 deletions(-) create mode 100644 Test/dafny0/QuantificationNewSyntax.dfy create mode 100644 Test/dafny0/QuantificationNewSyntax.dfy.expect diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index a2849afca1b..27bf0193c53 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6145,21 +6145,19 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { bvars = new List(); range = null; - var domainCloner = new QuantifiedVariableDomainCloner(); - var rangeCloner = new QuantifiedVariableRangeCloner(); - + foreach (var qvar in qvars) { BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); bvars.Add(bvar); if (qvar.Domain != null) { - var domainWithToken = domainCloner.CloneExpr(qvar.Domain); + var domainWithToken = QuantifiedVariableDomainCloner.Instance.CloneExpr(qvar.Domain); var inDomainExpr = new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), domainWithToken); range = range == null ? inDomainExpr : new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.And, range, inDomainExpr); } if (qvar.Range != null) { - var rangeWithToken = rangeCloner.CloneExpr(qvar.Range); + var rangeWithToken = QuantifiedVariableRangeCloner.Instance.CloneExpr(qvar.Range); range = range == null ? qvar.Range : new BinaryExpr(rangeWithToken.tok, BinaryExpr.Opcode.And, range, rangeWithToken); } } @@ -9113,12 +9111,16 @@ public override string val { } class QuantifiedVariableDomainCloner : Cloner { + public static readonly QuantifiedVariableDomainCloner Instance = new QuantifiedVariableDomainCloner(); + private QuantifiedVariableDomainCloner() {} public override IToken Tok(IToken tok) { return new QuantifiedVariableDomainToken(tok); } } class QuantifiedVariableRangeCloner : Cloner { + public static readonly QuantifiedVariableRangeCloner Instance = new QuantifiedVariableRangeCloner(); + private QuantifiedVariableRangeCloner() {} public override IToken Tok(IToken tok) { return new QuantifiedVariableRangeToken(tok); } diff --git a/Test/dafny0/QuantificationNewSyntax.dfy b/Test/dafny0/QuantificationNewSyntax.dfy new file mode 100644 index 00000000000..3053d123fcf --- /dev/null +++ b/Test/dafny0/QuantificationNewSyntax.dfy @@ -0,0 +1,22 @@ +// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module {:options "/quantifierSyntax:4"} NewSyntax { + method M() + { + // Illustrating that per-quantified variable ranges + // can be used to ensure later domains and ranges + // are well-formed. + var numbers := [0, 1, 2, 3]; + var _ := set x <- numbers, y | y == 6 / x :: y; // Error: possible division by zero + var _ := set x <- numbers | 0 < x, y | y == 6 / x :: y; // Success + var _ := set x <- numbers, y <- F(x) :: y; // Error: function precondition might not hold + var _ := set x <- numbers | x < 3, y <- F(x) :: y; // Success + var _ := set x <- numbers | x < 3, y <- F(x) :: y as nat; // Error: result of operation might violate subset type constraint for 'nat' + var _ := set x <- numbers | x < 3, y <- F(x) | 0 <= y :: y as nat; // Success + } + + function F(x: nat): seq requires x < 3 { + [-5, 4, 0, -12] + } +} \ No newline at end of file diff --git a/Test/dafny0/QuantificationNewSyntax.dfy.expect b/Test/dafny0/QuantificationNewSyntax.dfy.expect new file mode 100644 index 00000000000..fb9882e0876 --- /dev/null +++ b/Test/dafny0/QuantificationNewSyntax.dfy.expect @@ -0,0 +1,8 @@ +QuantificationNewSyntax.dfy(11,13): Warning: /!\ No trigger covering all quantified variables found. +QuantificationNewSyntax.dfy(12,13): Warning: /!\ No trigger covering all quantified variables found. +QuantificationNewSyntax.dfy(11,42): Error: possible division by zero +QuantificationNewSyntax.dfy(13,36): Error: function precondition might not hold +QuantificationNewSyntax.dfy(19,42): Related location +QuantificationNewSyntax.dfy(15,54): Error: result of operation might violate subset type constraint for 'nat' + +Dafny program verifier finished with 0 verified, 3 errors diff --git a/Test/dafny0/QuantificationResolution.dfy b/Test/dafny0/QuantificationResolution.dfy index 045e3d9621d..c65ae2f469c 100644 --- a/Test/dafny0/QuantificationResolution.dfy +++ b/Test/dafny0/QuantificationResolution.dfy @@ -5,10 +5,33 @@ module {:options "/quantifierSyntax:4"} NewSyntax { method M() { var _ := set x <- 5; + var _ := set x <- [5], y <- 5 :: y; var _ := set x: int | 0 <= x < 10, y | "true" :: y; var _ := set x <- [3], y | "true" :: y; - - // var numbers := [0, 1, 2, 3]; - // var _ := set x <- numbers | 0 < x, y | y == 6 / x :: y; + var _ := set x, y | "true" :: y; + + var _ := map x <- 5 :: x + 2; + var _ := map x <- [5], y <- 5 :: x := y; + var _ := map x: int | 0 <= x < 10, y | "true" :: x := y; + var _ := map x <- [3], y | "true" :: x := y; + var _ := map x, y | "true" :: x := y; + + var _ := forall x <- 5 :: x < 10; + var _ := forall x <- [5], y <- 5 :: x < 10; + var _ := forall x: int | 0 <= x < 10, y | "true" :: x < 10; + var _ := forall x <- [3], y | "true" :: x < 10; + var _ := forall x, y | "true" :: x < 10; + + var _ := exists x <- 5 :: x < 10; + var _ := exists x <- [5], y <- 5 :: x < 10; + var _ := exists x: int | 0 <= x < 10, y | "true" :: x < 10; + var _ := exists x <- [3], y | "true" :: x < 10; + var _ := exists x, y | "true" :: x < 10; + + forall x <- 5 {} + forall x <- [5], y <- 5 {} + forall x: int | 0 <= x < 10, y | "true" {} + forall x <- [3], y | "true" {} + forall x, y | "true" {} } } \ No newline at end of file diff --git a/Test/dafny0/QuantificationResolution.dfy.expect b/Test/dafny0/QuantificationResolution.dfy.expect index e69de29bb2d..f0d41fc6e13 100644 --- a/Test/dafny0/QuantificationResolution.dfy.expect +++ b/Test/dafny0/QuantificationResolution.dfy.expect @@ -0,0 +1,26 @@ +QuantificationResolution.dfy(9,43): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(10,31): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(11,24): Error: range of comprehension must be of type bool (instead got string) +QuantificationResolution.dfy(15,43): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(16,31): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(17,24): Error: range of comprehension must be of type bool (instead got string) +QuantificationResolution.dfy(21,46): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(22,34): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(23,27): Error: range of quantifier must be of type bool (instead got string) +QuantificationResolution.dfy(27,46): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(28,34): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(29,27): Error: range of quantifier must be of type bool (instead got string) +QuantificationResolution.dfy(33,37): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(34,25): Error: range of quantified variable must be of type bool (instead got string) +QuantificationResolution.dfy(35,18): Error: range restriction in forall statement must be of type bool (instead got string) +QuantificationResolution.dfy(7,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(8,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(13,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationResolution.dfy(14,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(19,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationResolution.dfy(20,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(25,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationResolution.dfy(26,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(31,16): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationResolution.dfy(32,26): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +25 resolution/type errors detected in QuantificationResolution.dfy From 4c4bb4d0f33facb526c124e2c780e30ed0710f7e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 1 Jun 2022 17:06:02 -0700 Subject: [PATCH 26/39] =?UTF-8?q?Don=E2=80=99t=20force=20`|=20true`=20on?= =?UTF-8?q?=20all=20quantifications,=20add=20comments?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Source/Dafny/AST/DafnyAst.cs | 35 ++++++++++++++++++++++++++++++----- Source/Dafny/Dafny.atg | 25 +++++++++++++++---------- 2 files changed, 45 insertions(+), 15 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 27bf0193c53..50237e971b8 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -6128,6 +6128,12 @@ public BoundVar(IToken tok, string name, Type type) } } + /// + /// A QuantifiedVar is a bound variable used in a quantifier such as "forall x :: ...", + /// a comprehension such as "set x | 0 <= x < 10", etc. + /// In addition to its type, which may be inferred, it can have an optional domain collection expression + /// (x <- C) and an optional range boolean expressions (x | E). + /// [DebuggerDisplay("Quantified<{name}>")] public class QuantifiedVar : BoundVar { public readonly Expression Domain; @@ -6142,6 +6148,19 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr Range = range; } + /// + /// Map a list of quantified variables to an eqivalent list of bound variables plus a single range expression. + /// The transformation looks like this in general: + /// + /// x1 <- C1 | E1, ..., xN <- CN | EN + /// + /// becomes: + /// + /// x1, ... xN | x1 in C1 && E1 && ... && xN in CN && EN + /// + /// Note the result will be null rather than "true" if there are no such domains or ranges. + /// Some quantification contexts (such as comprehensions) will replace this with "true". + /// public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { bvars = new List(); range = null; @@ -6151,20 +6170,18 @@ public static void ExtractSingleRange(List qvars, out List + /// A token wrapper used to produce better type checking errors + /// for quantified variables. See QuantifierVar.ExtractSingleRange() + /// public class QuantifiedVariableDomainToken : TokenWrapper { public QuantifiedVariableDomainToken(IToken wrappedToken) : base(wrappedToken) { @@ -9098,6 +9119,10 @@ public override string val { } } + /// + /// A token wrapper used to produce better type checking errors + /// for quantified variables. See QuantifierVar.ExtractSingleRange() + /// public class QuantifiedVariableRangeToken : TokenWrapper { public QuantifiedVariableRangeToken(IToken wrappedToken) : base(wrappedToken) { @@ -11537,7 +11562,7 @@ public LetOrFailExpr(IToken tok, CasePattern/*?*/ lhs, Expression rhs, /// /// Quantifications used to only support a single range, but now each /// quantified variable can have a range attached. - /// The overall Range is now filled in by the resolver by extracting any implicit + /// The overall Range is now filled in by the parser by extracting any implicit /// "x in Domain" constraints and per-variable Range constraints into a single conjunct. /// /// The Term is optional if the expression only has one quantified variable, diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d2ad7a3c3f7..6b947c5b221 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -4745,27 +4745,26 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression /*------------------------------------------------------------------------*/ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allowLemma, bool allowLambda, bool allowBitwiseOps.> = (. - IToken tok; - IToken id; - Type optType = null; + BoundVar bv; Expression domain = null; Expression range = null; .) - WildIdent - [ ":" TypeAndToken - ] + IdentTypeOptional [ // "<-" can also appear in GenericParameters in something like "<-T>", // so we parse it as two separate tokens. "<" "-" - /* We can't allow bitwise ops here since otherwise we'll swallow up any - optional "| " suffix */ + // We can't allow bitwise ops here since otherwise we'll swallow up any + // optional "| " suffix Expression ] { Attribute } - [ "|" + [ // Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement; + // I don't see how that's possible, but this IF is good and suppresses the reported ambiguity + IF(la.kind == _verticalbar) + "|" Expression ] - (. qvar = new QuantifiedVar(id, id.val, optType == null ? new InferredTypeProxy() : optType, domain, range); .) + (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.SyntacticType, domain, range); .) . /*------------------------------------------------------------------------*/ @@ -4787,6 +4786,12 @@ SetComprehensionExpr Date: Wed, 1 Jun 2022 17:39:03 -0700 Subject: [PATCH 27/39] Formatting --- Source/Dafny/AST/DafnyAst.cs | 8 ++++---- Source/Dafny/DafnyOptions.cs | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 50237e971b8..12641c017dd 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -9118,7 +9118,7 @@ public override string val { set { WrappedToken.val = value; } } } - + /// /// A token wrapper used to produce better type checking errors /// for quantified variables. See QuantifierVar.ExtractSingleRange() @@ -9137,15 +9137,15 @@ public override string val { class QuantifiedVariableDomainCloner : Cloner { public static readonly QuantifiedVariableDomainCloner Instance = new QuantifiedVariableDomainCloner(); - private QuantifiedVariableDomainCloner() {} + private QuantifiedVariableDomainCloner() { } public override IToken Tok(IToken tok) { return new QuantifiedVariableDomainToken(tok); } } - + class QuantifiedVariableRangeCloner : Cloner { public static readonly QuantifiedVariableRangeCloner Instance = new QuantifiedVariableRangeCloner(); - private QuantifiedVariableRangeCloner() {} + private QuantifiedVariableRangeCloner() { } public override IToken Tok(IToken tok) { return new QuantifiedVariableRangeToken(tok); } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 8a4987aab0c..67506343e42 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1271,7 +1271,8 @@ public override void Error(string message, params string[] args) { /// class DafnyAttributeOptions : DafnyOptions { public static readonly HashSet KnownOptions = new() { - "functionSyntax", "quantifierSyntax" + "functionSyntax", + "quantifierSyntax" }; private readonly Errors errors; From ce77a53dde6a66ea0bf0482f601fd04cc20c8c68 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 2 Jun 2022 11:06:46 -0700 Subject: [PATCH 28/39] Reject whitespace in between < and -, more tests --- Source/Dafny/Dafny.atg | 17 ++++++++-- Test/dafny0/QuantificationNewSyntax.dfy | 2 +- .../QuantificationNewSyntaxParseErrors.dfy | 34 +++++++++++++++++++ ...ntificationNewSyntaxParseErrors.dfy.expect | 7 ++++ ... => QuantificationNewSyntaxResolution.dfy} | 10 ++++++ ...antificationNewSyntaxResolution.dfy.expect | 28 +++++++++++++++ .../QuantificationResolution.dfy.expect | 26 -------------- 7 files changed, 94 insertions(+), 30 deletions(-) create mode 100644 Test/dafny0/QuantificationNewSyntaxParseErrors.dfy create mode 100644 Test/dafny0/QuantificationNewSyntaxParseErrors.dfy.expect rename Test/dafny0/{QuantificationResolution.dfy => QuantificationNewSyntaxResolution.dfy} (69%) create mode 100644 Test/dafny0/QuantificationNewSyntaxResolution.dfy.expect delete mode 100644 Test/dafny0/QuantificationResolution.dfy.expect diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 6b947c5b221..5d3caa1f64c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -228,6 +228,7 @@ bool IsQuantifierVariableDecl(QuantifiedVar previousVar) { // This would previously parse as two separate arguments to the print statement, but // could now also be parsed as a single set comprehension argument with two quantified variables // (and an invalid one since it would need an explicit ":: " section). + // // Even worse: // // print set x: x | E, y <- C; @@ -247,6 +248,14 @@ bool IsQuantifierVariableDecl(QuantifiedVar previousVar) { return la.kind == _comma && IsIdentifier(x.kind); } +// Checks for "<-", which has to be parsed as two separate tokens, +// but ensures no whitespace between them. +bool IsFromArrow() { + scanner.ResetPeek(); + IToken x = scanner.Peek(); + return la.kind == _openAngleBracket && x.kind == _minus + && la.line == x.line && la.col == x.col - 1; +} bool IsLabel(bool allowLabel) { if (!allowLabel) { @@ -529,8 +538,8 @@ bool IsNotEndOfCase() { /* The following is the largest lookahead there is. It needs to check if what follows * can be nothing but "<" Type { "," Type } ">". - * If inExpressionContext == false and there is an opening '<', then - * it is assumed, without checking, that what follows is a type parameter list + * If inExpressionContext == true, it also checks the token immediately after + * the ">" to help disambiguate some cases (see implementation comment). */ bool IsGenericInstantiation(bool inExpressionContext) { scanner.ResetPeek(); @@ -4751,7 +4760,9 @@ QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allow .) IdentTypeOptional [ // "<-" can also appear in GenericParameters in something like "<-T>", - // so we parse it as two separate tokens. + // so we parse it as two separate tokens, but use lookahead to ensure + // we don't allow whitespace between them. + IF(IsFromArrow()) "<" "-" // We can't allow bitwise ops here since otherwise we'll swallow up any // optional "| " suffix diff --git a/Test/dafny0/QuantificationNewSyntax.dfy b/Test/dafny0/QuantificationNewSyntax.dfy index 3053d123fcf..8e6a5c73838 100644 --- a/Test/dafny0/QuantificationNewSyntax.dfy +++ b/Test/dafny0/QuantificationNewSyntax.dfy @@ -19,4 +19,4 @@ module {:options "/quantifierSyntax:4"} NewSyntax { function F(x: nat): seq requires x < 3 { [-5, 4, 0, -12] } -} \ No newline at end of file +} diff --git a/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy b/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy new file mode 100644 index 00000000000..bd85f70c0aa --- /dev/null +++ b/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy @@ -0,0 +1,34 @@ +// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module {:options "/quantifierSyntax:3"} OldSyntax { + method M() + { + var y := 5; + print set x | 0 <= x < 10, y; // Allowed, parsed as two separate arguments to print + SomeMethod(set x | 0 <= x < 10, y); // Similarly + + var c := [1, 2, 3]; + print set x | 0 <= x < 10, y <- c; // Allowed, parsed as two separate arguments to print (the second being "y <(- c)") + SomeMethod(set x | 0 <= x < 10, y <- c); // Similarly + + // This is included because of the ambiguity of "<-" as either two separate tokens or one. + // Generic instantiations can never use variance symbols so this should always be cleanly rejected. + var _ := set x: SomeType<-T>; // Error: invalid UnaryExpression + } +} + +module {:options "/quantifierSyntax:4"} NewSyntax { + method M() + { + var y := 5; + print set x | 0 <= x < 10, y; // Error: a set comprehension with more than one bound variable must have a term expression + SomeMethod(set x | 0 <= x < 10, y); // Error: a set comprehension with more than one bound variable must have a term expression + + var c := [1, 2, 3]; + print set x | 0 <= x < 10, y <- c; // Error: a set comprehension with more than one bound variable must have a term expression + SomeMethod(set x | 0 <= x < 10, y <- c); // Error: a set comprehension with more than one bound variable must have a term expression + + var _ := set x: SomeType<-T>; // Error: invalid UnaryExpression + } +} \ No newline at end of file diff --git a/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy.expect b/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy.expect new file mode 100644 index 00000000000..0ac0a2a16d0 --- /dev/null +++ b/Test/dafny0/QuantificationNewSyntaxParseErrors.dfy.expect @@ -0,0 +1,7 @@ +QuantificationNewSyntaxParseErrors.dfy(17,32): Error: invalid UnaryExpression +QuantificationNewSyntaxParseErrors.dfy(25,31): Error: a set comprehension with more than one bound variable must have a term expression +QuantificationNewSyntaxParseErrors.dfy(26,36): Error: a set comprehension with more than one bound variable must have a term expression +QuantificationNewSyntaxParseErrors.dfy(29,36): Error: a set comprehension with more than one bound variable must have a term expression +QuantificationNewSyntaxParseErrors.dfy(30,41): Error: a set comprehension with more than one bound variable must have a term expression +QuantificationNewSyntaxParseErrors.dfy(32,32): Error: invalid UnaryExpression +6 parse errors detected in QuantificationNewSyntaxParseErrors.dfy diff --git a/Test/dafny0/QuantificationResolution.dfy b/Test/dafny0/QuantificationNewSyntaxResolution.dfy similarity index 69% rename from Test/dafny0/QuantificationResolution.dfy rename to Test/dafny0/QuantificationNewSyntaxResolution.dfy index c65ae2f469c..44601b84247 100644 --- a/Test/dafny0/QuantificationResolution.dfy +++ b/Test/dafny0/QuantificationNewSyntaxResolution.dfy @@ -4,6 +4,8 @@ module {:options "/quantifierSyntax:4"} NewSyntax { method M() { + // Ensuring we get sensible errors for type mismatches, + // despite the current desugaring implementation. var _ := set x <- 5; var _ := set x <- [5], y <- 5 :: y; var _ := set x: int | 0 <= x < 10, y | "true" :: y; @@ -33,5 +35,13 @@ module {:options "/quantifierSyntax:4"} NewSyntax { forall x: int | 0 <= x < 10, y | "true" {} forall x <- [3], y | "true" {} forall x, y | "true" {} + + + // Dealing with the ambiguity of "<-": we parse it as two separate tokens + // but shouldn't allow whitespace in between when it is used as a single token. + var c := [1, 2, 3]; + var _ := set x <- c; // Allowed + var _ := set x < - c; // Error: arguments to < must have a common supertype (got set and seq) + // Error: type of unary - must be of a numeric or bitvector type (instead got seq) } } \ No newline at end of file diff --git a/Test/dafny0/QuantificationNewSyntaxResolution.dfy.expect b/Test/dafny0/QuantificationNewSyntaxResolution.dfy.expect new file mode 100644 index 00000000000..879cbf89c1d --- /dev/null +++ b/Test/dafny0/QuantificationNewSyntaxResolution.dfy.expect @@ -0,0 +1,28 @@ +QuantificationNewSyntaxResolution.dfy(11,43): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(12,31): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(13,24): Error: range of comprehension must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(17,43): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(18,31): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(19,24): Error: range of comprehension must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(23,46): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(24,34): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(25,27): Error: range of quantifier must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(29,46): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(30,34): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(31,27): Error: range of quantifier must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(35,37): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(36,25): Error: range of quantified variable must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(37,18): Error: range restriction in forall statement must be of type bool (instead got string) +QuantificationNewSyntaxResolution.dfy(44,19): Error: arguments to < must have a common supertype (got set and seq) +QuantificationNewSyntaxResolution.dfy(44,23): Error: type of unary - must be of a numeric or bitvector type (instead got seq) +QuantificationNewSyntaxResolution.dfy(9,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(10,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(15,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationNewSyntaxResolution.dfy(16,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(21,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationNewSyntaxResolution.dfy(22,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(27,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) +QuantificationNewSyntaxResolution.dfy(28,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(33,16): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +QuantificationNewSyntaxResolution.dfy(34,26): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) +27 resolution/type errors detected in QuantificationNewSyntaxResolution.dfy diff --git a/Test/dafny0/QuantificationResolution.dfy.expect b/Test/dafny0/QuantificationResolution.dfy.expect deleted file mode 100644 index f0d41fc6e13..00000000000 --- a/Test/dafny0/QuantificationResolution.dfy.expect +++ /dev/null @@ -1,26 +0,0 @@ -QuantificationResolution.dfy(9,43): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(10,31): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(11,24): Error: range of comprehension must be of type bool (instead got string) -QuantificationResolution.dfy(15,43): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(16,31): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(17,24): Error: range of comprehension must be of type bool (instead got string) -QuantificationResolution.dfy(21,46): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(22,34): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(23,27): Error: range of quantifier must be of type bool (instead got string) -QuantificationResolution.dfy(27,46): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(28,34): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(29,27): Error: range of quantifier must be of type bool (instead got string) -QuantificationResolution.dfy(33,37): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(34,25): Error: range of quantified variable must be of type bool (instead got string) -QuantificationResolution.dfy(35,18): Error: range restriction in forall statement must be of type bool (instead got string) -QuantificationResolution.dfy(7,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(8,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(13,22): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) -QuantificationResolution.dfy(14,32): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(19,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) -QuantificationResolution.dfy(20,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(25,25): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got int) -QuantificationResolution.dfy(26,35): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(31,16): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -QuantificationResolution.dfy(32,26): Error: domain of quantified variable must be a set, multiset, or sequence with elements of type ?, or a map with domain ? (instead got int) -25 resolution/type errors detected in QuantificationResolution.dfy From 2e57a162271a8491ad68f557772bb8fecca84b84 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 2 Jun 2022 12:52:54 -0700 Subject: [PATCH 29/39] Update reference manual --- docs/DafnyRef/Expressions.md | 40 +++++++++++++++++------------------- docs/DafnyRef/Grammar.md | 36 ++++++++++++++++++++++++++++++-- docs/DafnyRef/Statements.md | 5 +++-- 3 files changed, 56 insertions(+), 25 deletions(-) diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 8e556a60caa..fddcfbbcdf6 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -981,21 +981,19 @@ Note that the braces enclosing the ``CaseClause``s may be omitted. QuantifierExpression(allowLemma, allowLambda) = ( "forall" | "exists" ) QuantifierDomain "::" Expression(allowLemma, allowLambda) - -QuantifierDomain = - IdentTypeOptional { "," IdentTypeOptional } { Attribute } - [ "|" Expression(allowLemma: true, allowLambda: true) ] ```` A ``QuantifierExpression`` is a boolean expression that specifies that a given expression (the one following the `::`) is true for all (for **forall**) or some (for **exists**) combination of values of the quantified variables, namely those in the ``QuantifierDomain``. +See [Section 2.6.5](#sec-quantifier-domains) for more details on quantifier domains. Here are some examples: ```dafny assert forall x : nat | x <= 5 :: x * x <= 25; (forall n :: 2 <= n ==> (exists d :: n < d < 2*n)) +assert forall x: nat | 0 <= x < |s|, y <- s[x] :: y < x; ``` The quantifier identifiers are _bound_ within the scope of the @@ -1010,11 +1008,7 @@ It this is not possible, the program is in error. ````grammar SetComprehensionExpr(allowLemma, allowLambda) = [ "set" | "iset" ] - IdentTypeOptional - { "," IdentTypeOptional } - { Attribute } - "|" - Expression(allowLemma, allowLambda) + QuantifierDomain(allowLemma, allowLambda) [ "::" Expression(allowLemma, allowLambda) ] ```` @@ -1040,12 +1034,17 @@ set x : T | P(x) :: x For the full form ```dafny -var S := set x1:T1, x2:T2 ... | P(x1, x2, ...) :: Q(x1, x2, ...) +var S := set x1: T1 <- C1 | P1(x1), + x2: T2 <- C2 | P2(x1, x2), + ... + :: Q(x1, x2, ...) ``` the elements of `S` will be all values resulting from evaluation of `Q(x1, x2, ...)` -for all combinations of quantified variables `x1, x2, ...` such that -predicate `P(x1, x2, ...)` holds. For example, +for all combinations of quantified variables `x1, x2, ...` (from their respective `C1, C2, ...` +domains) such that all predicates `P1(x1), P2(x1, x2), ...` hold. + +For example, ```dafny var S := set x:nat, y:nat | x < 2 && y < 2 :: (x, y) @@ -1054,7 +1053,9 @@ yields `S == {(0, 0), (0, 1), (1, 0), (1,1) }` The types on the quantified variables are optional and if not given Dafny will attempt to infer them from the contexts in which they are used in the -`P` or `Q` expressions. +various expressions. The `<- C` domain expressions are also optional and default to +`iset x: T` (i.e. all values of the variable's type), as are the `| P` expressions which +default to `true`. See also [Section 2.6.5](#sec-quantifier-domains) for more details on quantifier domains. If a finite set was specified ("set" keyword used), Dafny must be able to prove that the result is finite otherwise the set comprehension expression will not be @@ -1063,7 +1064,7 @@ accepted. Set comprehensions involving reference types such as ```dafny -set o: object | true +set o: object ``` are allowed in ghost expressions within methods, but not in ghost functions[^set-of-objects-not-in-functions]. @@ -1073,7 +1074,7 @@ where the bound variable is of a reference type. In non-ghost contexts, it is not allowed, because--even though the resulting set would be finite--it is not pleasant or practical to compute at run time. -[^set-of-objects-not-in-functions]: In order to be deterministic, the result of a function should only depend on the arguments and of the objects it [reads](#sec-reads-clause), and Dafny does not provide a way to explicitely pass the entire heap as the argument to a function. See [this post](https://github.com/dafny-lang/dafny/issues/1366#issuecomment-906785889) for more insights. +[^set-of-objects-not-in-functions]: In order to be deterministic, the result of a function should only depend on the arguments and of the objects it [reads](#sec-reads-clause), and Dafny does not provide a way to explicitly pass the entire heap as the argument to a function. See [this post](https://github.com/dafny-lang/dafny/issues/1366#issuecomment-906785889) for more insights. The universe in which set comprehensions are evaluated is the set of all _allocated_ objects, of the appropriate type and satisfying the given predicate. @@ -1199,19 +1200,16 @@ the whole let-or-fail expression. Typically that means that `tmp.PropagateFailur ````grammar MapComprehensionExpr(allowLemma, allowLambda) = ( "map" | "imap" ) - IdentTypeOptional - { "," IdentTypeOptional } - { Attribute } - [ "|" Expression(allowLemma: true, allowLambda: true) ] + QuantifierDomain(allowLemma, allowLambda) "::" Expression(allowLemma, allowLambda) [ ":=" Expression(allowLemma, allowLambda) ] ```` A ``MapComprehensionExpr`` defines a finite or infinite map value -by defining a domain (using the ``IdentTypeOptional`` and the optional -condition following the "|") and for each value in the domain, +by defining a domain and for each value in the domain, giving the mapped value using the expression following the "::". +See [Section 2.6.5](#sec-quantifier-domains) for more details on quantifier domains. For example: ```dafny diff --git a/docs/DafnyRef/Grammar.md b/docs/DafnyRef/Grammar.md index 6f82b179254..4ed42a375a5 100644 --- a/docs/DafnyRef/Grammar.md +++ b/docs/DafnyRef/Grammar.md @@ -561,7 +561,40 @@ A ``FormalsOptionalIds`` is a formal parameter list in which the types are requi but the names of the parameters are optional. This is used in algebraic datatype definitions. -### 2.6.5. Numeric Literals +### 2.6.5. Quantifier Domains {#sec-quantifier-domains} +````grammar +QuantifierDomain(allowLemma, allowLambda) = + QuantifierVarDecl(allowLemma, allowLambda) + { "," QuantifierVarDecl(allowLemma, allowLambda) } + +QuantifierVarDecl(allowLemma, allowLambda) = + IdentTypeOptional + [ <- Expression(allowLemma, allowLambda) ] + { Attribute } + [ | Expression(allowLemma, allowLambda) ] +```` + +A quantifier domain is used in several Dafny constructs to bind one or more variables +to a range of values. For example, in the quantifier `forall x : nat | x <= 5 :: x * x <= 25`, +the quantifier domain is the text `x : nat | x <= 5`, which binds the variable `x` to the values +`0`, `1`, `2`, `3`, `4`, and `5`. The overall expression is hence true if the `x * x <= 5` body is true +for each of these values (which it is in this case). + +The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, +which restricts the bindings to values that satisfy this expression. +In the example above `x <= 5` is the range attached to the `x` variable declaration. + +The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. +Here a collection is any value of a type that supports the `in` operator, namely sets, multisets, maps, and sequences. +The domain also restricts the bindings, in this case to the elements of the collection: `x <- C` implies `x in C`. +The example above can also be expressed as `var c := [0, 1, 2, 3, 4, 5]; forall x <- c :: x * x <= 25`. + +Note that a variable's domain expression may reference any variable declared before it, +and a variable's range expression may reference the attached variable (and usually does) and any variable declared before it. +For example, in the quantifier domain `x: nat | 0 <= x < |s|, y <- s[x] | x < y`, the expression `s[x]` is well-formed +because the range attached to `x` ensures `x` is a valid index in the sequence `s`. + +### 2.6.6. Numeric Literals ````grammar Nat = ( digits | hexdigits ) ```` @@ -571,4 +604,3 @@ A ``Nat`` represents a natural number expressed in either decimal or hexadecimal Dec = decimaldigits ```` A ``Dec`` represents a decimal fraction literal. - diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md index caaa8a73a92..6084df07542 100644 --- a/docs/DafnyRef/Statements.md +++ b/docs/DafnyRef/Statements.md @@ -1736,10 +1736,11 @@ ForallStmt = ```` The `forall` statement executes the body -simultaneously for all quantified values in the specified range. +simultaneously for all quantified values in the specified quantifier domain. +See [Section 2.6.5](#sec-quantifier-domains) for more details on quantifier domains. + There are several variant uses of the `forall` statement and there are a number of restrictions. - In particular, a `forall` statement can be classified as one of the following: * _Assign_ - the `forall` statement is used for simultaneous assignment. From 450b9a7ed34ed69c774a23b147b6a4b5bbce3048 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 2 Jun 2022 13:51:59 -0700 Subject: [PATCH 30/39] Document /quantifierSyntax --- Source/Dafny/DafnyOptions.cs | 10 ++++++++++ docs/DafnyRef/Options.txt | 10 ++++++++++ docs/DafnyRef/UserGuide.md | 13 +++++++++++++ 3 files changed, 33 insertions(+) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 67506343e42..af92a3af09a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1010,6 +1010,16 @@ syntax and has the exact same meaning as your previous version 3 program. experimentalPredicateAlwaysGhost - Compiled functions are written `function`. Ghost functions are written `ghost function`. Predicates are always ghost and are written `predicate`. +/quantifierSyntax: + The syntax for quantification domains is changing from Dafny version 3 to version 4, + more specifically where quantifier ranges (| ) are allowed. + This switch gives early access to the new syntax. + 3 (default) - Ranges are only allowed after all quantified variables are declared. + (e.g. set x, y | 0 <= x < |s| && y in s[x] && 0 <= y :: y) + 4 - Ranges are allowed after each quantified variable declaration. + (e.g. set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y) + Note that quantifier variable domains (<- ) are available + in both syntax versions. /disableScopes Treat all export sets as 'export reveal *'. i.e. don't hide function bodies or type definitions during translation. diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 182877107af..6c0bac1d71f 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -105,6 +105,16 @@ Usage: Dafny [ option ... ] [ filename ... ] experimentalPredicateAlwaysGhost - Compiled functions are written `function`. Ghost functions are written `ghost function`. Predicates are always ghost and are written `predicate`. + /quantifierSyntax: + The syntax for quantification domains is changing from Dafny version 3 to version 4, + more specifically where quantifier ranges (| ) are allowed. + This switch gives early access to the new syntax. + 3 (default) - Ranges are only allowed after all quantified variables are declared. + (e.g. set x, y | 0 <= x < |s| && y in s[x] && 0 <= y :: y) + 4 - Ranges are allowed after each quantified variable declaration. + (e.g. set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y) + Note that quantifier variable domains (<- ) are available + in both syntax versions. /disableScopes Treat all export sets as 'export reveal *'. i.e. don't hide function bodies or type definitions during translation. diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index ee78ec27aa6..52901c53b34 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -1117,6 +1117,19 @@ older versions of Dafny. `function`. Ghost functions are written `ghost function`. Predicates are always ghost and are written `predicate`. +* `-functionSyntax:` - select what quantifier syntax to recognize. + The syntax for quantification domains is changing from Dafny version 3 to version 4, + more specifically where quantifier ranges (`| `) are allowed. + This switch gives early access to the new syntax. + + * `3` (default) - Ranges are only allowed after all quantified variables are declared. + (e.g. `set x, y | 0 <= x < |s| && y in s[x] && 0 <= y :: y`) + * `4` - Ranges are allowed after each quantified variable declaration. + (e.g. `set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y`) + + Note that quantifier variable domains (`<- `) are available + in both syntax versions. + * `-disableScopes` - treat all export sets as `export reveal *` to never hide function bodies or type definitions during translation. From 5441b092bc409725f6d855906d41020e1477596a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Jun 2022 15:45:11 -0700 Subject: [PATCH 31/39] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- Source/Dafny/Dafny.atg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5d3caa1f64c..9aa29f2b72a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -223,7 +223,7 @@ bool IsQuantifierVariableDecl(QuantifiedVar previousVar) { // Introducing per-quantified variable ranges creates some ambiguities in the grammar, // since before that the range would terminate the quantifed domain. For example, the following statement: // - // print set x: x | E, y; + // print set x | E, y; // // This would previously parse as two separate arguments to the print statement, but // could now also be parsed as a single set comprehension argument with two quantified variables @@ -231,7 +231,7 @@ bool IsQuantifierVariableDecl(QuantifiedVar previousVar) { // // Even worse: // - // print set x: x | E, y <- C; + // print set x | E, y <- C; // // This was a valid statement before as well, because "y <- C" would be parsed as the expression // "y < (-C)". From 39bd35956fc8b74d3610577a1f456fdc9e5dc7ae Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Jun 2022 16:15:59 -0700 Subject: [PATCH 32/39] More PR feedback --- Source/Dafny/Compilers/SinglePassCompiler.cs | 1 - Test/comp/ForallNewSyntax.dfy | 9 +++++---- Test/comp/ForallNewSyntax.dfy.expect | 8 +++++--- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index c506dfc6f0e..4287ecbc8ff 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -3423,7 +3423,6 @@ Type CompileCollection(ComprehensionExpr.BoundedPool bound, IVariable bv, bool i var b = (ComprehensionExpr.MapBoundedPool)bound; TrParenExpr(su.Substitute(b.Map), collectionWriter, inLetExprBody, wStmts); GetSpecialFieldInfo(SpecialField.ID.Keys, null, null, out var keyName, out _, out _); - // TODO: Shouldn't this be UniqueElements? collectionWriter.Write($".{keyName}.Elements{propertySuffix}"); return b.CollectionElementType; } else if (bound is ComprehensionExpr.SeqBoundedPool) { diff --git a/Test/comp/ForallNewSyntax.dfy b/Test/comp/ForallNewSyntax.dfy index 67cd3c24b54..0600ebaa2e3 100644 --- a/Test/comp/ForallNewSyntax.dfy +++ b/Test/comp/ForallNewSyntax.dfy @@ -1,7 +1,8 @@ -// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t" -// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" -// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /compile:0 "%s" > "%t" +// RUN: %dafny /quantifierSyntax:4 /noVerify /compile:4 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /noVerify /compile:4 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /noVerify /compile:4 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /quantifierSyntax:4 /noVerify /compile:4 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/comp/ForallNewSyntax.dfy.expect b/Test/comp/ForallNewSyntax.dfy.expect index b79a345bbc6..3b5d37fbc21 100644 --- a/Test/comp/ForallNewSyntax.dfy.expect +++ b/Test/comp/ForallNewSyntax.dfy.expect @@ -1,5 +1,7 @@ Dafny program verifier finished with 25 verified, 0 errors + +Dafny program verifier did not attempt verification Arrays: Basic cases [0, 1, 2, 3, 4] [0, 1, 2, 3, 4] @@ -43,7 +45,7 @@ Objects: Functions [(2, 1.0), (3, 2.0), (3, 3.0)] [(3, 1.0), (4, 2.0), (5, 3.0)] -Dafny program verifier finished with 25 verified, 0 errors +Dafny program verifier did not attempt verification Arrays: Basic cases [0, 1, 2, 3, 4] [0, 1, 2, 3, 4] @@ -87,7 +89,7 @@ Objects: Functions [(2, 1.0), (3, 2.0), (3, 3.0)] [(3, 1.0), (4, 2.0), (5, 3.0)] -Dafny program verifier finished with 25 verified, 0 errors +Dafny program verifier did not attempt verification Arrays: Basic cases [0, 1, 2, 3, 4] [0, 1, 2, 3, 4] @@ -131,7 +133,7 @@ Objects: Functions [(2, 1.0), (3, 2.0), (3, 3.0)] [(3, 1.0), (4, 2.0), (5, 3.0)] -Dafny program verifier finished with 25 verified, 0 errors +Dafny program verifier did not attempt verification Arrays: Basic cases [0, 1, 2, 3, 4] [0, 1, 2, 3, 4] From 341e92733cb61045aa9a4ac94856017f8f060eee Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 6 Jun 2022 19:26:03 -0700 Subject: [PATCH 33/39] Reorder and improve Quantifier Domains refman content --- docs/DafnyRef/Grammar.md | 63 +++++++++++++++++++++++++++------------- 1 file changed, 43 insertions(+), 20 deletions(-) diff --git a/docs/DafnyRef/Grammar.md b/docs/DafnyRef/Grammar.md index 4ed42a375a5..16cb0c3715d 100644 --- a/docs/DafnyRef/Grammar.md +++ b/docs/DafnyRef/Grammar.md @@ -562,6 +562,49 @@ but the names of the parameters are optional. This is used in algebraic datatype definitions. ### 2.6.5. Quantifier Domains {#sec-quantifier-domains} + +Several Dafny constructs bind one or more variables to a range of possible values. +For example, the quantifier `forall x: nat | x <= 5 :: x * x <= 25` has the meaning +"for all integers x between 0 and 5, the square of x is at most 25". +Similarly, the set comprehension `set x: nat | x <= 5 :: f(x)` can be read as +"the set containing the result of applying f to x, for each integer x between 0 and 5". +The common syntax that specifies the bound variables and what values they take on +is known as the *quantifier domain*; in the previous examples this is `x: nat | x <= 5`, +which binds the variable `x` to the values `0`, `1`, `2`, `3`, `4`, and `5`. + +Here are some more examples. + +- `x: byte` (where `type byte = x | 0 <= x < 256`) +- `x: nat | x <= 5` +- `x <- integerSet` +- `x: nat <- integerSet` +- `x: nat <- integerSet | x % 2 == 0` +- `x: nat, y: nat | x < 2 && y < 2` +- `i | 0 <= i < |s|, y <- s[i] | i < y` + +A quantifier domain declares one or more *quantified variables*, separated by commas. +Each variable declaration can be nothing more than a variable name, but it +may also include any of three optional elements: + +1. The optional syntax `: T` declares the type of the quantified variable. + If not provided, it will be inferred from context. + +2. The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, + which restricts the bindings to values that satisfy this expression. + In the example above `x <= 5` is the range attached to the `x` variable declaration. + +3. The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. + Here a collection is any value of a type that supports the `in` operator, namely sets, multisets, maps, and sequences. + The domain also restricts the bindings, in this case to the elements of the collection: `x <- C` implies `x in C`. + The example above can also be expressed as `var c := [0, 1, 2, 3, 4, 5]; forall x <- c :: x * x <= 25`. + +Note that a variable's domain expression may reference any variable declared before it, +and a variable's range expression may reference the attached variable (and usually does) and any variable declared before it. +For example, in the quantifier domain `i | 0 <= i < |s|, y <- s[i] | i < y`, the expression `s[i]` is well-formed +because the range attached to `i` ensures `i` is a valid index in the sequence `s`. + +The general production for quantifier domains is: + ````grammar QuantifierDomain(allowLemma, allowLambda) = QuantifierVarDecl(allowLemma, allowLambda) @@ -574,26 +617,6 @@ QuantifierVarDecl(allowLemma, allowLambda) = [ | Expression(allowLemma, allowLambda) ] ```` -A quantifier domain is used in several Dafny constructs to bind one or more variables -to a range of values. For example, in the quantifier `forall x : nat | x <= 5 :: x * x <= 25`, -the quantifier domain is the text `x : nat | x <= 5`, which binds the variable `x` to the values -`0`, `1`, `2`, `3`, `4`, and `5`. The overall expression is hence true if the `x * x <= 5` body is true -for each of these values (which it is in this case). - -The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, -which restricts the bindings to values that satisfy this expression. -In the example above `x <= 5` is the range attached to the `x` variable declaration. - -The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. -Here a collection is any value of a type that supports the `in` operator, namely sets, multisets, maps, and sequences. -The domain also restricts the bindings, in this case to the elements of the collection: `x <- C` implies `x in C`. -The example above can also be expressed as `var c := [0, 1, 2, 3, 4, 5]; forall x <- c :: x * x <= 25`. - -Note that a variable's domain expression may reference any variable declared before it, -and a variable's range expression may reference the attached variable (and usually does) and any variable declared before it. -For example, in the quantifier domain `x: nat | 0 <= x < |s|, y <- s[x] | x < y`, the expression `s[x]` is well-formed -because the range attached to `x` ensures `x` is a valid index in the sequence `s`. - ### 2.6.6. Numeric Literals ````grammar Nat = ( digits | hexdigits ) From 4df4b5d3a07d3c20e092ce6e50388208a5cb86ce Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 6 Jun 2022 20:11:00 -0700 Subject: [PATCH 34/39] Bit more PR feedback --- Test/comp/Comprehensions.dfy | 8 ++++---- Test/comp/ComprehensionsNewSyntax.dfy | 10 ++++------ docs/DafnyRef/UserGuide.md | 2 +- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/Test/comp/Comprehensions.dfy b/Test/comp/Comprehensions.dfy index d590cfb2fa6..5e0015516a1 100644 --- a/Test/comp/Comprehensions.dfy +++ b/Test/comp/Comprehensions.dfy @@ -270,7 +270,7 @@ method SetComprehension() { method SetComprehension0() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object | o in s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA | o in s; @@ -289,7 +289,7 @@ method SetComprehension0() { method SetComprehension1() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z, null}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object | o in s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA | o in s; @@ -308,7 +308,7 @@ method SetComprehension1() { method SetComprehension2() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z, null}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object? | o in s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA? | o in s; @@ -329,7 +329,7 @@ predicate method True(g: G) { true } method SetComprehension3() { var s: set := {false, true}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: bool | o in s; var aa := set o: bool | o in s && !o; var bb := set o: bool | o in s && o; diff --git a/Test/comp/ComprehensionsNewSyntax.dfy b/Test/comp/ComprehensionsNewSyntax.dfy index 23c89021d3c..ec8e7a07fe0 100644 --- a/Test/comp/ComprehensionsNewSyntax.dfy +++ b/Test/comp/ComprehensionsNewSyntax.dfy @@ -15,8 +15,6 @@ method Main() { TestImplicitTypeTests.Test(); } -predicate method Thirteen(x: int) { x == 13 } -predicate method Even(y: int) { y % 2 == 1 } function method FourMore(x: int): int { x + 4 } method Quantifier() { @@ -83,7 +81,7 @@ method SetComprehension() { method SetComprehension0() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object <- s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA <- s; @@ -102,7 +100,7 @@ method SetComprehension0() { method SetComprehension1() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z, null}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object <- s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA <- s; @@ -121,7 +119,7 @@ method SetComprehension1() { method SetComprehension2() { var w, x, y, z := new ClassA, new ClassA, new ClassB, new ClassB; var s := {w, x, y, z, null}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: object? <- s; // The next set comprehension picks out 2 of the elements in s: var aa := set o: ClassA? <- s; @@ -142,7 +140,7 @@ predicate method True(g: G) { true } method SetComprehension3() { var s: set := {false, true}; - // The following set comprehension picks att elements in s: + // The following set comprehension picks all elements in s: var all := set o: bool <- s; var aa := set o: bool <- s | !o; var bb := set o: bool <- s | o; diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 52901c53b34..61541cd9def 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -1117,7 +1117,7 @@ older versions of Dafny. `function`. Ghost functions are written `ghost function`. Predicates are always ghost and are written `predicate`. -* `-functionSyntax:` - select what quantifier syntax to recognize. +* `-quantifierSyntax:` - select what quantifier syntax to recognize. The syntax for quantification domains is changing from Dafny version 3 to version 4, more specifically where quantifier ranges (`| `) are allowed. This switch gives early access to the new syntax. From 7c80d10e8bf3b7df3cb4c4316cc09c36aee1b791 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 7 Jun 2022 14:36:44 -0700 Subject: [PATCH 35/39] Fix test file --- Test/comp/ComprehensionsNewSyntax.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/comp/ComprehensionsNewSyntax.dfy.expect b/Test/comp/ComprehensionsNewSyntax.dfy.expect index 6f7824bd366..149346cdf49 100644 --- a/Test/comp/ComprehensionsNewSyntax.dfy.expect +++ b/Test/comp/ComprehensionsNewSyntax.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 11 verified, 0 errors +Dafny program verifier finished with 10 verified, 0 errors Dafny program verifier did not attempt verification true false From e7c1900ceba60aac32f895607d566a99e10749af Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 9 Jun 2022 10:30:23 -0700 Subject: [PATCH 36/39] Add release notes and note on CLI option --- RELEASE_NOTES.md | 1 + docs/DafnyRef/Grammar.md | 3 +++ 2 files changed, 4 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index ce5475d8c59..0dabd04a6e5 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,7 @@ # Upcoming - feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. +- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See Section [2.6.5](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual. - fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142) - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) diff --git a/docs/DafnyRef/Grammar.md b/docs/DafnyRef/Grammar.md index 16cb0c3715d..38bfc5c89dd 100644 --- a/docs/DafnyRef/Grammar.md +++ b/docs/DafnyRef/Grammar.md @@ -603,6 +603,9 @@ and a variable's range expression may reference the attached variable (and usual For example, in the quantifier domain `i | 0 <= i < |s|, y <- s[i] | i < y`, the expression `s[i]` is well-formed because the range attached to `i` ensures `i` is a valid index in the sequence `s`. +Allowing per-variable ranges is not fully backwards compatible, and so it is not yet allowed by default; +the `/functionSyntax:4` option needs to be provided to enable this feature (See [Section 24.10.5](#sec-controlling-language)). + The general production for quantifier domains is: ````grammar From 48250b8fc8c9f7a7943320e6209af7e053ab1400 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Jun 2022 08:40:01 -0700 Subject: [PATCH 37/39] Update RELEASE_NOTES.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- RELEASE_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 5ad78ca8494..19038299ddf 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,7 +1,7 @@ # Upcoming - feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. -- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See Section [2.6.5](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual. +- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See [the quantifier domain section](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual. - fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142) - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) From a29f370a9862ccc15569ea34f0d04f620ce1503c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Jun 2022 08:43:23 -0700 Subject: [PATCH 38/39] PR feedback --- docs/DafnyRef/Grammar.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/DafnyRef/Grammar.md b/docs/DafnyRef/Grammar.md index 38bfc5c89dd..e918c25c7a7 100644 --- a/docs/DafnyRef/Grammar.md +++ b/docs/DafnyRef/Grammar.md @@ -580,6 +580,7 @@ Here are some more examples. - `x: nat <- integerSet` - `x: nat <- integerSet | x % 2 == 0` - `x: nat, y: nat | x < 2 && y < 2` +- `x: nat | x < 2, y: nat | y < x` - `i | 0 <= i < |s|, y <- s[i] | i < y` A quantifier domain declares one or more *quantified variables*, separated by commas. @@ -589,15 +590,15 @@ may also include any of three optional elements: 1. The optional syntax `: T` declares the type of the quantified variable. If not provided, it will be inferred from context. -2. The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, - which restricts the bindings to values that satisfy this expression. - In the example above `x <= 5` is the range attached to the `x` variable declaration. - 3. The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. Here a collection is any value of a type that supports the `in` operator, namely sets, multisets, maps, and sequences. - The domain also restricts the bindings, in this case to the elements of the collection: `x <- C` implies `x in C`. + The domain restricts the bindings to the elements of the collection: `x <- C` implies `x in C`. The example above can also be expressed as `var c := [0, 1, 2, 3, 4, 5]; forall x <- c :: x * x <= 25`. +2. The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, + which restricts the bindings to values that satisfy this expression. + In the example above `x <= 5` is the range attached to the `x` variable declaration. + Note that a variable's domain expression may reference any variable declared before it, and a variable's range expression may reference the attached variable (and usually does) and any variable declared before it. For example, in the quantifier domain `i | 0 <= i < |s|, y <- s[i] | i < y`, the expression `s[i]` is well-formed From cbd0f032ba549827f05f7e8a6dd2d10645e59ee7 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 10 Jun 2022 08:49:14 -0700 Subject: [PATCH 39/39] I can count, I swear --- docs/DafnyRef/Grammar.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/DafnyRef/Grammar.md b/docs/DafnyRef/Grammar.md index e918c25c7a7..2184eee0bd0 100644 --- a/docs/DafnyRef/Grammar.md +++ b/docs/DafnyRef/Grammar.md @@ -590,12 +590,12 @@ may also include any of three optional elements: 1. The optional syntax `: T` declares the type of the quantified variable. If not provided, it will be inferred from context. -3. The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. +2. The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*. Here a collection is any value of a type that supports the `in` operator, namely sets, multisets, maps, and sequences. The domain restricts the bindings to the elements of the collection: `x <- C` implies `x in C`. The example above can also be expressed as `var c := [0, 1, 2, 3, 4, 5]; forall x <- c :: x * x <= 25`. -2. The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, +3. The optional syntax `| E` attaches a boolean expression `E` as a *quantified variable range*, which restricts the bindings to values that satisfy this expression. In the example above `x <= 5` is the range attached to the `x` variable declaration.