diff options
33 files changed, 326 insertions, 173 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index d6bd895a..f00db25a 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1,4 +1,5 @@ -using System.Numerics;
+using System; // for Func
+using System.Numerics;
namespace Dafny
{
@@ -27,7 +28,7 @@ namespace Dafny d[t] = true;
return new Set<T>(d);
}
-
+
public IEnumerable<T> Elements {
get {
return dict.Keys;
@@ -636,7 +637,16 @@ namespace Dafny {
return u;
}
+
+ public static U Let<T, U>(T t, Func<T,U> f) {
+ return f(t);
+ }
+
public delegate Result Function<Input,Result>(Input input);
+
+ public static A Id<A>(A a) {
+ return a;
+ }
}
public struct BigRational
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e01cc6bb..4c930724 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -938,55 +938,12 @@ namespace Microsoft.Dafny { void CompileReturnBody(Expression body, int indent) {
Contract.Requires(0 <= indent);
body = body.Resolved;
- SpillLetVariableDecls(body, indent);
Indent(indent);
wr.Write("return ");
TrExpr(body);
wr.WriteLine(";");
}
- void SpillLetVariableDecls(Expression expr, int indent) {
- Contract.Requires(0 <= indent);
- if (expr == null) {
- // allow "null" as an argument; nothing to do
- return;
- }
- if (expr is LetExpr) {
- var e = (LetExpr)expr;
- // Bound variables introduced in the LHS are ghost if either the entire let expression is declared
- // a ghost or the position of a variable corresponds to the datatype constructor argument that is
- // declared a ghost. If all variables are ghost, then the corresponding RHS is not needed; but if
- // there is any non-ghost variable, then the corresponding RHS is needed.
- Contract.Assert(e.LHSs.Count == e.RHSs.Count);
- var i = 0;
- foreach (var lhs in e.LHSs) {
- var needRHS = false;
- foreach (var v in lhs.Vars) {
- if (!v.IsGhost) {
- if (!needRHS) {
- // this is the first of lhs's variables that we have found we need
- Indent(indent);
- var nm = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);
- wr.WriteLine("{0} @{1};", TypeName(e.RHSs[i].Type), nm);
- needRHS = true;
- }
- Indent(indent);
- wr.WriteLine("{0} @{1};", TypeName(v.Type), v.CompileName);
- }
- }
- if (needRHS) {
- SpillLetVariableDecls(e.RHSs[i], indent);
- }
- i++;
- }
- SpillLetVariableDecls(e.Body, indent);
- return;
- }
- foreach (var ee in expr.SubExpressions) {
- SpillLetVariableDecls(ee, indent);
- }
- }
-
// ----- Type ---------------------------------------------------------------------------------
readonly string DafnySetClass = "Dafny.Set";
@@ -1025,6 +982,9 @@ namespace Microsoft.Dafny { } else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
string s = "@" + udt.FullCompileName;
+ if (type is ArrowType) {
+ s = "Func";
+ }
if (udt.TypeArgs.Count != 0) {
if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {
Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
@@ -1118,6 +1078,8 @@ namespace Microsoft.Dafny { return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";
} else if (type is MapType) {
return TypeName(type)+".Empty";
+ } else if (type is ArrowType) {
+ return "null";
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
@@ -1162,7 +1124,6 @@ namespace Microsoft.Dafny { if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (Attributes.Argument arg in s.Args) {
- SpillLetVariableDecls(arg.E, indent);
Indent(indent);
wr.Write("System.Console.Write(");
if (arg.S != null) {
@@ -1235,7 +1196,6 @@ namespace Microsoft.Dafny { }
} else {
Contract.Assume(s.Bounds != null);
- SpillLetVariableDecls(s.Expr, indent);
// For "i,j,k,l :| R(i,j,k,l);", emit something like:
//
@@ -1392,7 +1352,6 @@ namespace Microsoft.Dafny { TrStmt(s.Thn, indent);
}
} else {
- SpillLetVariableDecls(s.Guard, indent);
Indent(indent); wr.Write("if (");
TrExpr(s.Guard);
wr.WriteLine(")");
@@ -1407,7 +1366,6 @@ namespace Microsoft.Dafny { } else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alternative in s.Alternatives) {
- SpillLetVariableDecls(alternative.Guard, indent);
}
Indent(indent);
foreach (var alternative in s.Alternatives) {
@@ -1426,7 +1384,6 @@ namespace Microsoft.Dafny { Indent(indent);
wr.WriteLine("while (false) { }");
} else {
- SpillLetVariableDecls(s.Guard, indent);
Indent(indent);
wr.Write("while (");
TrExpr(s.Guard);
@@ -1441,7 +1398,6 @@ namespace Microsoft.Dafny { wr.WriteLine("while (true) {");
int ind = indent + IndentAmount;
foreach (var alternative in s.Alternatives) {
- SpillLetVariableDecls(alternative.Guard, ind);
}
Indent(ind);
foreach (var alternative in s.Alternatives) {
@@ -1551,8 +1507,6 @@ namespace Microsoft.Dafny { wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
- SpillLetVariableDecls(b.LowerBound, ind);
- SpillLetVariableDecls(b.UpperBound, ind);
Indent(ind);
wr.Write("for (var @{0} = ", bv.CompileName);
TrExpr(b.LowerBound);
@@ -1561,14 +1515,12 @@ namespace Microsoft.Dafny { wr.Write("; @{0}++) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
- SpillLetVariableDecls(b.Set, ind);
Indent(ind);
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Set);
wr.Write(").Elements) { ");
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
- SpillLetVariableDecls(b.Seq, ind);
Indent(ind);
wr.Write("foreach (var @{0} in (", bv.CompileName);
TrExpr(b.Seq);
@@ -1585,15 +1537,12 @@ namespace Microsoft.Dafny { // if (range) {
// ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));
// }
- SpillLetVariableDecls(s.Range, indent + n * IndentAmount);
Indent(indent + n * IndentAmount);
wr.Write("if ");
TrParenExpr(s.Range);
wr.WriteLine(" {");
var indFinal = indent + (n + 1) * IndentAmount;
- SpillLetVariableDecls(s0.Lhs, indFinal);
- SpillLetVariableDecls(rhs, indFinal);
Indent(indFinal);
wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);
if (s0.Lhs is MemberSelectExpr) {
@@ -1665,7 +1614,6 @@ namespace Microsoft.Dafny { // ...
// }
if (s.Cases.Count != 0) {
- SpillLetVariableDecls(s.Source, indent);
string source = "_source" + tmpVarCount;
tmpVarCount++;
Indent(indent);
@@ -1705,7 +1653,6 @@ namespace Microsoft.Dafny { string CreateLvalue(Expression lhs, int indent) {
lhs = lhs.Resolved;
- SpillLetVariableDecls(lhs, indent);
if (lhs is IdentifierExpr) {
var ll = (IdentifierExpr)lhs;
return "@" + ll.Var.CompileName;
@@ -1759,7 +1706,6 @@ namespace Microsoft.Dafny { void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent) {
Contract.Requires((target == null) != (targetExpr == null));
- SpillLetVariableDecls(targetExpr, indent);
var tRhs = rhs as TypeRhs;
if (tRhs != null && tRhs.InitCall != null) {
string nw = "_nw" + tmpVarCount;
@@ -1780,10 +1726,8 @@ namespace Microsoft.Dafny { // do nothing
} else {
if (rhs is ExprRhs) {
- SpillLetVariableDecls(((ExprRhs)rhs).Expr, indent);
} else if (tRhs != null && tRhs.ArrayDimensions != null) {
foreach (Expression dim in tRhs.ArrayDimensions) {
- SpillLetVariableDecls(dim, indent);
}
}
Indent(indent);
@@ -1810,13 +1754,11 @@ namespace Microsoft.Dafny { for (int i = 0; i < s.Method.Ins.Count; i++) {
Formal p = s.Method.Ins[i];
if (!p.IsGhost) {
- SpillLetVariableDecls(s.Args[i], indent);
}
}
if (receiverReplacement != null) {
// TODO: What to do here? When does this happen, what does it mean?
} else if (!s.Method.IsStatic) {
- SpillLetVariableDecls(s.Receiver, indent);
string inTmp = "_in" + tmpVarCount;
tmpVarCount++;
@@ -1884,7 +1826,6 @@ namespace Microsoft.Dafny { for (int i = 0; i < s.Method.Ins.Count; i++) {
Formal p = s.Method.Ins[i];
if (!p.IsGhost) {
- SpillLetVariableDecls(s.Args[i], indent);
}
}
if (receiverReplacement != null) {
@@ -1901,7 +1842,6 @@ namespace Microsoft.Dafny { wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
}
} else {
- SpillLetVariableDecls(s.Receiver, indent);
Indent(indent);
TrParenExpr(s.Receiver);
}
@@ -2243,6 +2183,15 @@ namespace Microsoft.Dafny { FunctionCallExpr e = (FunctionCallExpr)expr;
CompileFunctionCallExpr(e, wr, TrExpr);
+ } else if (expr is ApplyExpr) {
+ var e = expr as ApplyExpr;
+ wr.Write("Dafny.Helpers.Id<");
+ wr.Write(TypeName(e.Receiver.Type));
+ wr.Write(">(");
+ TrExpr(e.Receiver);
+ wr.Write(")");
+ TrExprList(e.Args);
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
@@ -2532,10 +2481,9 @@ namespace Microsoft.Dafny { // The Dafny "let" expression
// var Pattern(x,y) := G; E
// is translated into C# as:
- // ExpressionSequence(tmp = G,
- // ExpressionSequence(x = dtorX(tmp),
- // ExpressionSequence(y = dtorY(tmp), E)))
- // preceded by the declaration of tmp, x, y.
+ // LamLet(G, tmp =>
+ // LamLet(dtorX(tmp), x =>
+ // LamLet(dtorY(tmp), y => E)))
Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution
Contract.Assert(e.Exact); // because !Exact is ghost only
var neededCloseParens = 0;
@@ -2543,11 +2491,13 @@ namespace Microsoft.Dafny { var lhs = e.LHSs[i];
if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {
var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);
- wr.Write("Dafny.Helpers.ExpressionSequence({0} = ", rhsName);
+ wr.Write("Dafny.Helpers.Let<");
+ wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));
+ wr.Write(">(");
TrExpr(e.RHSs[i]);
- wr.Write(", ");
+ wr.Write(", " + rhsName + " => ");
neededCloseParens++;
- var c = TrCasePattern(lhs, rhsName);
+ var c = TrCasePattern(lhs, rhsName, e.Body.Type);
Contract.Assert(c != 0); // we already checked that there's at least one non-ghost
neededCloseParens += c;
}
@@ -2557,6 +2507,32 @@ namespace Microsoft.Dafny { wr.Write(")");
}
+ /*
+ int i = 0;
+ for (int i = 0; i < e.LHSs.Count; ++i) {
+ var lhs = e.LHSs[i];
+ if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {
+ var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);
+
+ wr.Write("Dafny.Helpers.Id<");
+ wr.Write(TypeName(new ArrowType(e.RHSs[i], bodyType)));
+ wr.Write(">(");
+ wr.Write(rhsName);
+ wr.Write(" => ");
+ neededCloseParens++;
+
+ c = TrCasePattern(lhs, rhsName));
+ Contract.Assert(c != 0); // we already checked that there's at least one non-ghost
+ neededCloseParens += c;
+ }
+ }
+
+ TrExpr(e.Body);
+ for (int i = 0; i < neededCloseParens; i++) {
+ wr.Write(")");
+ }
+ */
+
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
// new Dafny.Helpers.Function<SourceType, TargetType>(delegate (SourceType _source) {
@@ -2779,11 +2755,36 @@ namespace Microsoft.Dafny { } else if (expr is LambdaExpr) {
LambdaExpr e = (LambdaExpr)expr;
- wr.Write("((");
- wr.Write(Util.Comma(e.BoundVars, bv => bv.CompileName));
- wr.Write(") => ");
- TrExpr(e.Body);
- wr.Write(")");
+ ISet<IVariable> fvs = new HashSet<IVariable>();
+ bool dontCare = false;
+ Type dontCareT = null;
+
+ Translator.ComputeFreeVariables(expr, fvs, ref dontCare, ref dontCare, ref dontCareT, false);
+ var sm = new Dictionary<IVariable, Expression>();
+
+ var bvars = new List<BoundVar>();
+ var fexprs = new List<Expression>();
+ foreach(var fv in fvs) {
+ fexprs.Add(new IdentifierExpr(fv.Tok, fv.Name) {
+ Var = fv, // resolved here!
+ Type = fv.Type
+ });
+ var bv = new BoundVar(fv.Tok, fv.Name, fv.Type);
+ bvars.Add(bv);
+ sm[fv] = new IdentifierExpr(bv.Tok, bv.Name) {
+ Var = bv, // resolved here!
+ Type = bv.Type
+ };
+ }
+
+ var su = new Translator.Substituter(null, sm, new Dictionary<TypeParameter, Type>(), null);
+
+ BetaRedex(bvars, fexprs, expr.Type, () => {
+ wr.Write("(");
+ wr.Write(Util.Comma(e.BoundVars, bv => "@" + bv.CompileName));
+ wr.Write(") => ");
+ TrExpr(su.Substitute(e.Body));
+ });
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
@@ -2810,14 +2811,15 @@ namespace Microsoft.Dafny { }
}
- int TrCasePattern(CasePattern pat, string rhsName) {
+ int TrCasePattern(CasePattern pat, string rhsString, Type bodyType) {
Contract.Requires(pat != null);
- Contract.Requires(rhsName != null);
+ Contract.Requires(rhsString != null);
int c = 0;
if (pat.Var != null) {
var bv = pat.Var;
if (!bv.IsGhost) {
- wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = {1}, ", bv.CompileName, rhsName);
+ wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type) + "," + TypeName(bodyType) + ">");
+ wr.Write("(" + rhsString + ", @" + bv.CompileName + " => ");
c++;
}
} else if (pat.Arguments != null) {
@@ -2832,7 +2834,7 @@ namespace Microsoft.Dafny { // nothing to compile, but do a sanity check
Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));
} else {
- c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsName, FormalName(formal, k)));
+ c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsString, FormalName(formal, k)), bodyType);
k++;
}
}
@@ -2863,5 +2865,22 @@ namespace Microsoft.Dafny { }
twr.Write(")");
}
+
+ void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, Action makeBody) {
+ Contract.Requires(bvars != null);
+ Contract.Requires(exprs != null);
+ Contract.Requires(bvars.Count == exprs.Count);
+ wr.Write("Dafny.Helpers.Id<");
+ wr.Write(TypeName(new ArrowType(bvars.ConvertAll(bv => bv.Type), bodyType)));
+ wr.Write(">((");
+ wr.Write(Util.Comma(bvars, bv => "@" + bv.CompileName));
+ wr.Write(") => ");
+
+ makeBody();
+
+ wr.Write(")");
+ TrExprList(exprs);
+ }
+
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 03020860..c214fe90 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5070,7 +5070,7 @@ namespace Microsoft.Dafny { {
// Reads(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)[Box(o)]
// = $Frame_F(args...)[o]
- // && Scramble(...)
+ // // && Scramble(...)
var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args));
Bpl.Expr o; var oVar = BplBoundVar("o", predef.RefType, out o);
@@ -5079,8 +5079,8 @@ namespace Microsoft.Dafny { new List<Bpl.Expr> { lhs_inner, FunctionCall(f.tok, BuiltinFunction.Box, null, o) });
var et = new ExpressionTranslator(this, predef, h);
- var rhs = BplAnd(InRWClause(f.tok, o, null, f.Reads, et, selfExpr, rhs_dict),
- MakeScrambler(f.tok, f.FullSanitizedName + "#extraReads", Cons(oVar, Concat(vars, bvars))));
+ var rhs = InRWClause(f.tok, o, null, f.Reads, et, selfExpr, rhs_dict);
+ // MakeScrambler(f.tok, f.FullSanitizedName + "#extraReads", Cons(oVar, Concat(vars, bvars))));
sink.TopLevelDeclarations.Add(new Axiom(f.tok,
BplForall(Cons(oVar, Concat(vars, bvars)), BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs))));
@@ -5146,7 +5146,7 @@ namespace Microsoft.Dafny { //
// no precondition for these, but:
// for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN]
- // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx]
+ // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't
Action<string, Bpl.Type, string, Bpl.Type, string, Bpl.Type> SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => {
Contract.Assert((precond == null) == (precondTy == null));
var bvars = new List<Bpl.Variable>();
@@ -5177,7 +5177,7 @@ namespace Microsoft.Dafny { var bx = BplBoundVar("bx", predef.BoxType, bvars);
lhs = new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List<Bpl.Expr> { lhs, bx });
rhs = new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List<Bpl.Expr> { rhs, bx });
- op = Bpl.Expr.Imp;
+ // op = Bpl.Expr.Imp;
}
if (selectorVar == "r") {
op = (u, v) => Bpl.Expr.Imp(v, u);
@@ -12280,7 +12280,7 @@ namespace Microsoft.Dafny { ty.NormalizeExpand().TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs));
}
- static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, ref bool usesOldHeap, ref Type usesThis, bool inOldContext) {
+ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, ref bool usesOldHeap, ref Type usesThis, bool inOldContext) {
Contract.Requires(expr != null);
if (expr is ThisExpr) {
diff --git a/Test/dafny0/ComputationsLoop.dfy b/Test/dafny0/ComputationsLoop.dfy index b89455a2..ecba17e4 100644 --- a/Test/dafny0/ComputationsLoop.dfy +++ b/Test/dafny0/ComputationsLoop.dfy @@ -10,4 +10,5 @@ function KeepDoin'It(x: nat): nat lemma Test(r: nat)
{
assert KeepDoin'It(20) == r;
-}
\ No newline at end of file +}
+
diff --git a/Test/hofs/Apply.dfy b/Test/hofs/Apply.dfy index bdd102c2..28486398 100644 --- a/Test/hofs/Apply.dfy +++ b/Test/hofs/Apply.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy index 91d7e384..2b892b35 100644 --- a/Test/hofs/Classes.dfy +++ b/Test/hofs/Classes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/Compilation.dfy b/Test/hofs/Compilation.dfy new file mode 100644 index 00000000..c3132db2 --- /dev/null +++ b/Test/hofs/Compilation.dfy @@ -0,0 +1,48 @@ + +class Ref<A> { + var val : A; +} + +method Main() { + // simple + print "1 = ", (x => x)(1), "\n"; + print "3 = ", (x => y => x + y)(1)(2), "\n"; + print "3 = ", ((x,y) => y + x)(1,2), "\n"; + print "0 = ", (() => 0)(), "\n"; + + // local variable + var y := 1; + var f := x => x + y; + print "3 = ", f(2), "\n"; + print "4 = ", f(3), "\n"; + y := 2; + print "3 = ", f(2), "\n"; + print "4 = ", f(3), "\n"; + + // reference + var z := new Ref<int>; + z.val := 1; + f := x reads z requires z != null => x + z.val; + print "3 = ", f(2), "\n"; + print "4 = ", f(3), "\n"; + z.val := 2; + print "4 = ", f(2), "\n"; + print "5 = ", f(3), "\n"; + + // loop + f := x => x; + y := 10; + while (y > 0) + invariant forall x :: f.requires(x); + invariant forall x :: f.reads(x) == {}; + { + f := x => f(x+y); + y := y - 1; + } + print "55 = ", f(0), "\n"; + + // substitution test + print "0 = ", (x => var y:=x;y)(0), "\n"; + print "1 = ", (y => (x => var y:=x;y))(0)(1), "\n"; +} + diff --git a/Test/hofs/Compilation.dfy.expect b/Test/hofs/Compilation.dfy.expect new file mode 100644 index 00000000..0c6452d2 --- /dev/null +++ b/Test/hofs/Compilation.dfy.expect @@ -0,0 +1,3 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled assembly into Compilation.exe
diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy index c31b68da..be2672f5 100644 --- a/Test/hofs/Examples.dfy +++ b/Test/hofs/Examples.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" function Apply(f: A -> B, x: A): B diff --git a/Test/hofs/Examples.dfy.expect b/Test/hofs/Examples.dfy.expect index 76f19e0d..99fc5d0f 100644 --- a/Test/hofs/Examples.dfy.expect +++ b/Test/hofs/Examples.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 7 verified, 0 errors
+Compiled assembly into Examples.dll
diff --git a/Test/hofs/Field.dfy b/Test/hofs/Field.dfy index 6d3412d7..7d3f571d 100644 --- a/Test/hofs/Field.dfy +++ b/Test/hofs/Field.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" // calling fields should not make a resolution error: diff --git a/Test/hofs/FnRef.dfy b/Test/hofs/FnRef.dfy index fb8136b7..5f084bd4 100644 --- a/Test/hofs/FnRef.dfy +++ b/Test/hofs/FnRef.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect index 5185c21c..016ee494 100644 --- a/Test/hofs/FnRef.dfy.expect +++ b/Test/hofs/FnRef.dfy.expect @@ -18,10 +18,5 @@ Execution trace: (0,0): anon0
FnRef.dfy(56,13): anon8_Else
(0,0): anon10_Then
-FnRef.dfy(67,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- FnRef.dfy(56,13): anon8_Else
- (0,0): anon10_Else
-Dafny program verifier finished with 4 verified, 5 errors
+Dafny program verifier finished with 4 verified, 4 errors
diff --git a/Test/hofs/Frame.dfy b/Test/hofs/Frame.dfy index 891435ba..6c4c12ad 100644 --- a/Test/hofs/Frame.dfy +++ b/Test/hofs/Frame.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/Lambda.dfy b/Test/hofs/Lambda.dfy index 44adb4ce..eae83095 100644 --- a/Test/hofs/Lambda.dfy +++ b/Test/hofs/Lambda.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/LambdaParsefail.dfy b/Test/hofs/LambdaParsefail.dfy index 1d864d73..a9da4c5e 100644 --- a/Test/hofs/LambdaParsefail.dfy +++ b/Test/hofs/LambdaParsefail.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Fails() { diff --git a/Test/hofs/LambdaParsefail2.dfy b/Test/hofs/LambdaParsefail2.dfy index 148fc03c..ead3b9ec 100644 --- a/Test/hofs/LambdaParsefail2.dfy +++ b/Test/hofs/LambdaParsefail2.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/MutableField.dfy b/Test/hofs/MutableField.dfy index fa0a1f50..1783fe5c 100644 --- a/Test/hofs/MutableField.dfy +++ b/Test/hofs/MutableField.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy index 17aa828a..fa99377f 100644 --- a/Test/hofs/Naked.dfy +++ b/Test/hofs/Naked.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Functions { diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy index 73b08fe2..286be898 100644 --- a/Test/hofs/OneShot.dfy +++ b/Test/hofs/OneShot.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Ref<A> { diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index bc80713d..47f7f575 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -1,59 +1,103 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -function MyReadsOk(f : A -> B, a : A) : set<object> - reads f.reads(a); -{ - f.reads(a) -} +module ReadsRequiresReads { + function MyReadsOk(f : A -> B, a : A) : set<object> + reads f.reads(a); + { + f.reads(a) + } -function MyReadsOk2(f : A -> B, a : A) : set<object> - reads f.reads(a); -{ - (f.reads)(a) -} + function MyReadsOk2(f : A -> B, a : A) : set<object> + reads f.reads(a); + { + (f.reads)(a) + } -function MyReadsOk3(f : A -> B, a : A) : set<object> - reads (f.reads)(a); -{ - f.reads(a) -} + function MyReadsOk3(f : A -> B, a : A) : set<object> + reads (f.reads)(a); + { + f.reads(a) + } -function MyReadsOk4(f : A -> B, a : A) : set<object> - reads (f.reads)(a); -{ - (f.reads)(a) -} + function MyReadsOk4(f : A -> B, a : A) : set<object> + reads (f.reads)(a); + { + (f.reads)(a) + } -function MyReadsBad(f : A -> B, a : A) : set<object> -{ - f.reads(a) -} + function MyReadsBad(f : A -> B, a : A) : set<object> + { + f.reads(a) + } -function MyReadsBad2(f : A -> B, a : A) : set<object> -{ - (f.reads)(a) -} + function MyReadsBad2(f : A -> B, a : A) : set<object> + { + (f.reads)(a) + } -function MyReadsOk'(f : A -> B, a : A, o : object) : bool - reads f.reads(a); -{ - o in f.reads(a) -} + function MyReadsOk'(f : A -> B, a : A, o : object) : bool + reads f.reads(a); + { + o in f.reads(a) + } -function MyReadsBad'(f : A -> B, a : A, o : object) : bool -{ - o in f.reads(a) -} + function MyReadsBad'(f : A -> B, a : A, o : object) : bool + { + o in f.reads(a) + } -function MyRequiresOk(f : A -> B, a : A) : bool - reads f.reads(a); -{ - f.requires(a) -} + function MyRequiresOk(f : A -> B, a : A) : bool + reads f.reads(a); + { + f.requires(a) + } -function MyRequiresBad(f : A -> B, a : A) : bool -{ - f.requires(a) + function MyRequiresBad(f : A -> B, a : A) : bool + { + f.requires(a) + } } +module WhatWeKnowAboutReads { + function ReadsNothing():(){()} + + lemma IndeedNothing() { + assert ReadsNothing.reads() == {}; + } + + method NothingHere() { + assert (() => ()).reads() == {}; + } + + class S { + var s : S; + } + + function ReadsSomething(s : S):() + reads s; + {()} + + method MaybeSomething() { + var s := new S; + var s' := new S; + if * { assert s in ReadsSomething.reads(s) || ReadsSomething.reads(s) == {}; + } else if * { assert s in ReadsSomething.reads(s); + } else if * { assert ReadsSomething.reads(s) == {}; + } else if * { assert s' !in ReadsSomething.reads(s); + } else if * { assert s' in ReadsSomething.reads(s); + } + } + + method SomethingHere() { + var s := new S; + var s' := new S; + var f := (u) reads u => (); + if * { assert s in f.reads(s) || f.reads(s) == {}; + } else if * { assert s in f.reads(s); + } else if * { assert f.reads(s) == {}; + } else if * { assert s' !in f.reads(s); + } else if * { assert s' in f.reads(s); + } + } +} diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index 50f74728..e83e017c 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -1,18 +1,39 @@ -ReadsReads.dfy(30,5): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-ReadsReads.dfy(35,3): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-ReadsReads.dfy(46,10): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-ReadsReads.dfy(57,5): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon3_Else
+ReadsReads.dfy(66,33): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ReadsReads.dfy(86,50): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon16_Then
+ReadsReads.dfy(88,29): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Then
+ReadsReads.dfy(98,37): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ReadsReads.dfy(95,16): anon15_Else
+ (0,0): anon19_Then
+ReadsReads.dfy(100,29): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ReadsReads.dfy(95,16): anon15_Else
+ (0,0): anon21_Then
-Dafny program verifier finished with 6 verified, 4 errors
+Dafny program verifier finished with 13 verified, 9 errors
diff --git a/Test/hofs/Renaming.dfy b/Test/hofs/Renaming.dfy index 7a3f69a5..8a2dc03a 100644 --- a/Test/hofs/Renaming.dfy +++ b/Test/hofs/Renaming.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" function OnId(f : (bool -> bool) -> int) : int @@ -16,9 +16,9 @@ method Equal() { } method K<A,B>(P : (A -> A) -> bool) + requires P.requires(x => x); + requires P(y => y); { - assume P.requires(x => x); - assume P(y => y); assert P(z => z); assert (x => y => x) == ((a : A) => (b : B) => a); } diff --git a/Test/hofs/Renaming.dfy.expect b/Test/hofs/Renaming.dfy.expect index 790f6509..54fc4d53 100644 --- a/Test/hofs/Renaming.dfy.expect +++ b/Test/hofs/Renaming.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 5 verified, 0 errors
+Compiled assembly into Renaming.dll
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy index 7df4bbb3..fa5ffb0c 100644 --- a/Test/hofs/ResolveError.dfy +++ b/Test/hofs/ResolveError.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy index 4bb58078..c27fa82c 100644 --- a/Test/hofs/Simple.dfy +++ b/Test/hofs/Simple.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" function method MkId<A>() : A -> A { @@ -81,10 +81,18 @@ function P(f: A -> B, x : A): B f(x) } + function Q(f: U -> V, x : U): V - reads (f.reads)(x); // would be nice to be able to write P.reads(f,x) - requires (f.requires)(x); + reads P.reads(f,x); + requires f.requires(x); // would be nice to be able to write P.requires(f,x) { P(f,x) } +function QQ(f: U -> V, x : U): V + reads ((() => ((()=>f)()).reads)())((()=>x)()); + requires ((() => ((()=>f)()).requires)())((()=>x)()); +{ + ((() => P)())((()=>f)(),(()=>x)()) +} + diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect index 76871e06..55fe50e0 100644 --- a/Test/hofs/Simple.dfy.expect +++ b/Test/hofs/Simple.dfy.expect @@ -29,4 +29,4 @@ Execution trace: Simple.dfy(72,38): anon5_Else
Simple.dfy(73,38): anon6_Else
-Dafny program verifier finished with 13 verified, 7 errors
+Dafny program verifier finished with 14 verified, 7 errors
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy index 3ba4ffd6..e717b096 100644 --- a/Test/hofs/TreeMapSimple.dfy +++ b/Test/hofs/TreeMapSimple.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List<A> = Nil | Cons(head: A,tail: List<A>); @@ -27,7 +27,7 @@ function Pre(f : A -> B, s : set<A>) : bool } function method Map(xs : List<A>, f : A -> B): List<B> - reads (set x, y | x in ListData(xs) && y in f.reads(x) :: y); + reads Pre.reads(f, ListData(xs)); requires Pre(f, ListData(xs)); decreases xs; { @@ -37,7 +37,7 @@ function method Map(xs : List<A>, f : A -> B): List<B> } function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B> - reads (set x, y | x in TreeData(t0) && y in f.reads(x) :: y); + reads Pre.reads(f, TreeData(t0)); requires Pre(f, TreeData(t0)); decreases t0; { diff --git a/Test/hofs/TreeMapSimple.dfy.expect b/Test/hofs/TreeMapSimple.dfy.expect index 790f6509..f523ef5d 100644 --- a/Test/hofs/TreeMapSimple.dfy.expect +++ b/Test/hofs/TreeMapSimple.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 5 verified, 0 errors
+Compiled assembly into TreeMapSimple.dll
diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy index 2178db9f..add7e83c 100644 --- a/Test/hofs/Twice.dfy +++ b/Test/hofs/Twice.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" function method Twice(f : A -> A): A -> A diff --git a/Test/hofs/Types.dfy b/Test/hofs/Types.dfy index 9f62763a..e3813bcb 100644 --- a/Test/hofs/Types.dfy +++ b/Test/hofs/Types.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" method FnEqGhost<A>() { diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy index dd95cc76..f79562e9 100644 --- a/Test/hofs/WhileLoop.dfy +++ b/Test/hofs/WhileLoop.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t" +// RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Ref<A> { diff --git a/Test/hofs/WhileLoop.dfy.expect b/Test/hofs/WhileLoop.dfy.expect index 4ef2de53..7984cc3b 100644 --- a/Test/hofs/WhileLoop.dfy.expect +++ b/Test/hofs/WhileLoop.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 6 verified, 0 errors
+Compiled assembly into WhileLoop.dll
|