Skip to content

Commit

Permalink
Allow attributes on CaseExpression (#1298)
Browse files Browse the repository at this point in the history 
* Allow attributes on CaseExpression

* resolve attributes on caseExpr

* fixed rprint

* minor comment

* attribute checks updated

Co-authored-by: Jatin Arora <[email protected]>
  • Loading branch information
@mschlaipfer @typerSniper
mschlaipfer and typerSniper authored Jul 13, 2021
1 parent f02462d commit 0f25bcc
Show file tree
Hide file tree
Showing 8 changed files with 78 additions and 34 deletions.
6 changes: 3 additions & 3 deletions Source/Dafny/Cloner.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -478,12 +478,12 @@ public virtual Expression CloneExpr(Expression expr) {
public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) {
Contract.Requires(c != null);
Contract.Requires(c.Arguments != null);
return new MatchCaseExpr(Tok(c.tok), c.Ctor, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body));
return new MatchCaseExpr(Tok(c.tok), c.Ctor, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body), CloneAttributes(c.Attributes));
}

public NestedMatchCaseExpr CloneNestedMatchCaseExpr(NestedMatchCaseExpr c) {
Contract.Requires(c != null);
return new NestedMatchCaseExpr(Tok(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body));
return new NestedMatchCaseExpr(Tok(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body), CloneAttributes(c.Attributes));
}

public virtual Expression CloneApplySuffix(ApplySuffix e) {
Expand Down Expand Up @@ -902,7 +902,7 @@ public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, strin
if (def == null) {
continue;
}

if (!declmap.ContainsKey(def)) {
declmap.Add(def, new List<AliasModuleDecl>());
sigmap.Add(def, new ModuleSignature());
Expand Down
4 changes: 3 additions & 1 deletion Source/Dafny/Dafny.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4113,11 +4113,13 @@ CaseExpression<out NestedMatchCaseExpr c, bool allowLemma, bool allowLambda, boo
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x;
ExtendedPattern/*!*/ pat = null;
Expression/*!*/ body;
Attributes attrs = null;
.)
"case" (. x = t; .)
{ Attribute<ref attrs> }
ExtendedPattern<out pat> (. .)
"=>"
Expression<out body, allowLemma, allowLambda, allowBitwiseOps> (. c = new NestedMatchCaseExpr(x, pat, body); .)
Expression<out body, allowLemma, allowLambda, allowBitwiseOps> (. c = new NestedMatchCaseExpr(x, pat, body, attrs); .)
.

/*------------------------------------------------------------------------*/
Expand Down
14 changes: 10 additions & 4 deletions Source/Dafny/DafnyAst.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9558,7 +9558,7 @@ public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression n
var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
new_body = VarSubstituter(old_case.Arguments.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, new_body);

var new_case = new MatchCaseExpr(old_case.tok, old_case.Ctor, newVars, new_body);
var new_case = new MatchCaseExpr(old_case.tok, old_case.Ctor, newVars, new_body, old_case.Attributes);

new_case.Ctor = old_case.Ctor; // resolve here
return new_case;
Expand Down Expand Up @@ -12132,18 +12132,20 @@ public MatchCase(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> argume
public class MatchCaseExpr : MatchCase
{
private Expression body;
public Attributes Attributes;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(body != null);
}

public MatchCaseExpr(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> arguments, Expression body)
public MatchCaseExpr(IToken tok, DatatypeCtor ctor, [Captured] List<BoundVar> arguments, Expression body, Attributes attrs = null)
: base(tok, ctor, arguments) {
Contract.Requires(tok != null);
Contract.Requires(ctor != null);
Contract.Requires(cce.NonNullElements(arguments));
Contract.Requires(body != null);
this.body = body;
this.Attributes = attrs;
}

public Expression Body {
Expand Down Expand Up @@ -12428,10 +12430,12 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) {
public class NestedMatchCaseExpr : NestedMatchCase
{
public readonly Expression Body;
public Attributes Attributes;

public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body): base(tok, pat) {
public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs): base(tok, pat) {
Contract.Requires(body != null);
this.Body = body;
this.Attributes = attrs;
}
}

Expand Down Expand Up @@ -12496,13 +12500,15 @@ public class NestedMatchExpr : ConcreteSyntaxExpression
public readonly Expression Source;
public readonly List<NestedMatchCaseExpr> Cases;
public readonly bool UsesOptionalBraces;
public Attributes Attributes;

public NestedMatchExpr(IToken tok, Expression source, [Captured] List<NestedMatchCaseExpr> cases, bool usesOptionalBraces): base(tok) {
public NestedMatchExpr(IToken tok, Expression source, [Captured] List<NestedMatchCaseExpr> cases, bool usesOptionalBraces, Attributes attrs = null): base(tok) {
Contract.Requires(source != null);
Contract.Requires(cce.NonNullElements(cases));
this.Source = source;
this.Cases = cases;
this.UsesOptionalBraces = usesOptionalBraces;
this.Attributes = attrs;
}
}

Expand Down
9 changes: 7 additions & 2 deletions Source/Dafny/Printer.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1892,7 +1892,9 @@ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, boo
foreach (var mc in e.Cases) {
bool isLastCase = i == e.Cases.Count - 1;
Indent(ind);
wr.Write("case ");
wr.Write("case");
PrintAttributes(mc.Attributes);
wr.Write(" ");
PrintExtendedPattern(mc.Pat);
wr.WriteLine(" =>");
PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
Expand All @@ -1919,7 +1921,10 @@ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, boo
foreach (var mc in e.Cases) {
bool isLastCase = i == e.Cases.Count - 1;
Indent(ind);
wr.Write("case {0}", mc.Ctor.Name);
wr.Write("case");
PrintAttributes(mc.Attributes);
wr.Write(" ");
wr.Write(mc.Ctor.Name);
PrintMatchCaseArgument(mc);
wr.WriteLine(" =>");
PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
Expand Down
24 changes: 16 additions & 8 deletions Source/Dafny/Resolver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
using System.Diagnostics.Contracts;
using Microsoft.BaseTypes;
using Microsoft.Boogie;
using Microsoft.CodeAnalysis.CSharp.Syntax;

namespace Microsoft.Dafny
{
Expand Down Expand Up @@ -11580,9 +11581,11 @@ public SyntaxContainer(IToken tok) {
private class CExpr : SyntaxContainer
{
public readonly Expression Body;
public Attributes Attributes;

public CExpr(IToken tok, Expression body) : base(tok) {
public CExpr(IToken tok, Expression body, Attributes attrs = null) : base(tok) {
this.Body = body;
this.Attributes = attrs;
}
}

Expand Down Expand Up @@ -11652,14 +11655,17 @@ public override string ToString() {
private class RBranchExpr : RBranch {

public Expression Body;
public Attributes Attributes;

public RBranchExpr(IToken tok, int branchid, List<ExtendedPattern> patterns, Expression body) : base(tok, branchid, patterns) {
public RBranchExpr(IToken tok, int branchid, List<ExtendedPattern> patterns, Expression body, Attributes attrs = null) : base(tok, branchid, patterns) {
this.Body = body;
this.Attributes = attrs;
}

public RBranchExpr(int branchid, NestedMatchCaseExpr x) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
public RBranchExpr(int branchid, NestedMatchCaseExpr x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
this.Body = x.Body;
this.Patterns.Add(x.Pat);
this.Attributes = attrs;
}

public override string ToString() {
Expand All @@ -11675,7 +11681,7 @@ private static RBranchStmt CloneRBranchStmt(RBranchStmt branch) {

private static RBranchExpr CloneRBranchExpr(RBranchExpr branch) {
Cloner cloner = new Cloner();
return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body));
return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body), cloner.CloneAttributes((branch.Attributes)));
}

private static RBranch CloneRBranch(RBranch branch) {
Expand All @@ -11699,7 +11705,7 @@ private SyntaxContainer PackBody(IToken tok, RBranch branch) {
if (branch is RBranchStmt br) {
return new CStmt(tok, new BlockStmt(tok, tok, br.Body), br.Attributes);
} else if (branch is RBranchExpr) {
return new CExpr(tok, ((RBranchExpr)branch).Body);
return new CExpr(tok, ((RBranchExpr)branch).Body, ((RBranchExpr)branch).Attributes);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // RBranch has only two implementations
}
Expand Down Expand Up @@ -11817,7 +11823,8 @@ private MatchCase MakeMatchCaseFromContainer(IToken tok, KeyValuePair<string, Da
newMatchCase = new MatchCaseStmt(tok, ctor.Value, freshPatBV, insideBranch, c.Attributes);
} else {
var insideBranch = ((CExpr)insideContainer).Body;
newMatchCase = new MatchCaseExpr(tok, ctor.Value, freshPatBV, insideBranch);
var attrs = ((CExpr)insideContainer).Attributes;
newMatchCase = new MatchCaseExpr(tok, ctor.Value, freshPatBV, insideBranch, attrs);
}
newMatchCase.Ctor = ctor.Value;
return newMatchCase;
Expand Down Expand Up @@ -12036,7 +12043,7 @@ private SyntaxContainer CompileRBranchConstructor(MatchTempInfo mti, MatchingCon
c.Attributes = new Attributes("split", args, c.Attributes);
}
var newMatchStmt = new MatchStmt(mti.Tok, mti.EndTok, currMatchee, newMatchCaseStmts, true, mti.Attributes, context);
return new CStmt(null, newMatchStmt); //Wokring HERE
return new CStmt(null, newMatchStmt);
} else {
var newMatchExpr = new MatchExpr(mti.Tok, currMatchee, newMatchCases.ConvertAll(x => (MatchCaseExpr)x), true, context);
return new CExpr(null, newMatchExpr);
Expand Down Expand Up @@ -12164,7 +12171,7 @@ private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) {
List<RBranch> branches = new List<RBranch>();
for (int id = 0; id < e.Cases.Count(); id++) {
var branch = e.Cases.ElementAt(id);
branches.Add(new RBranchExpr(id, branch));
branches.Add(new RBranchExpr(id, branch, branch.Attributes));
mti.BranchTok[id] = branch.Tok;
}

Expand Down Expand Up @@ -12410,6 +12417,7 @@ private void CheckLinearNestedMatchCase(Type type, NestedMatchCase mc, ResolveOp
private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpts opts) {
foreach(NestedMatchCaseExpr mc in me.Cases) {
scope.PushMarker();
ResolveAttributes(mc.Attributes, null, opts);
CheckLinearNestedMatchCase(dtd, mc, opts);
scope.PopMarker();
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Dafny/Verifier/Substituter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ public virtual Expression Substitute(Expression expr) {
if (newBoundVars != mc.Arguments || body != mc.Body) {
anythingChanged = true;
}
var newCaseExpr = new MatchCaseExpr(mc.tok, mc.Ctor, newBoundVars, body);
var newCaseExpr = new MatchCaseExpr(mc.tok, mc.Ctor, newBoundVars, body, mc.Attributes);
newCaseExpr.Ctor = mc.Ctor; // resolve here
cases.Add(newCaseExpr);
}
Expand Down
9 changes: 9 additions & 0 deletions Test/dafny0/AttributeChecks.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,15 @@ method Match(xs: List<int>) returns (r: int)
}
}

function method CaseExpr(r: List<int>): List<int>
{
match r {
case Nil => Nil
case {:ignore 3 + true} Cons(h, Nil) => Nil // error: 3 + true is ill-typed
case {:ignore false} Cons(h, t) => CaseExpr(t)
}
}

method Calc(x: int, y: int)
{
calc {:split 1} {:split 1 + false} { // error: 1 + false is ill-typed
Expand Down
44 changes: 29 additions & 15 deletions Test/dafny0/AttributeChecks.dfy.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,18 @@ method Match(xs: List<int>) returns (r: int)
}
}

function method CaseExpr(r: List<int>): List<int>
{
match r {
case Nil =>
Nil
case {:ignore 3 + true} Cons(h, Nil) =>
Nil
case {:ignore false} Cons(h, t) =>
CaseExpr(t)
}
}

method Calc(x: int, y: int)
{
calc {:split 1} {:split 1 + false} {
Expand Down Expand Up @@ -104,12 +116,12 @@ method For(lo: int, hi: int) returns (k: int)
}
return 2;
}
AttributeChecks.dfy(94,7): Error: unresolved identifier: k
AttributeChecks.dfy(93,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(93,28): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(97,25): Error: unresolved identifier: k
AttributeChecks.dfy(96,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(96,28): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(103,7): Error: unresolved identifier: k
AttributeChecks.dfy(102,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(102,28): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(106,25): Error: unresolved identifier: k
AttributeChecks.dfy(105,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(105,28): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(18,17): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(18,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(28,35): Error: type of right argument to + (int) must agree with the result type (bool)
Expand All @@ -118,12 +130,14 @@ AttributeChecks.dfy(42,19): Error: type of left argument to + (int) must agree w
AttributeChecks.dfy(42,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(52,19): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(52,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(58,28): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(58,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(68,25): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(68,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(75,23): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(75,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(86,30): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(86,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
22 resolution/type errors detected in AttributeChecks.dfy
AttributeChecks.dfy(60,20): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(60,20): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(67,28): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(67,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(77,25): Error: type of left argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(77,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(84,23): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(84,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
AttributeChecks.dfy(95,30): Error: type of right argument to + (int) must agree with the result type (bool)
AttributeChecks.dfy(95,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool)
24 resolution/type errors detected in AttributeChecks.dfy

0 comments on commit 0f25bcc

Please sign in to comment.