From e2d1b7891526c90e26a790a9783aed8f69a57450 Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Tue, 12 Aug 2014 14:44:55 -0700 Subject: Compile lambda functions and apply expressions, and change let expr compilation --- Test/hofs/Apply.dfy | 2 +- Test/hofs/Classes.dfy | 2 +- Test/hofs/Compilation.dfy | 48 +++++++++++++ Test/hofs/Compilation.dfy.expect | 3 + Test/hofs/Examples.dfy | 2 +- Test/hofs/Examples.dfy.expect | 1 + Test/hofs/Field.dfy | 2 +- Test/hofs/FnRef.dfy | 2 +- Test/hofs/FnRef.dfy.expect | 7 +- Test/hofs/Frame.dfy | 2 +- Test/hofs/Lambda.dfy | 2 +- Test/hofs/LambdaParsefail.dfy | 2 +- Test/hofs/LambdaParsefail2.dfy | 2 +- Test/hofs/MutableField.dfy | 2 +- Test/hofs/Naked.dfy | 2 +- Test/hofs/OneShot.dfy | 2 +- Test/hofs/ReadsReads.dfy | 136 ++++++++++++++++++++++++------------- Test/hofs/ReadsReads.dfy.expect | 31 +++++++-- Test/hofs/Renaming.dfy | 6 +- Test/hofs/Renaming.dfy.expect | 1 + Test/hofs/ResolveError.dfy | 2 +- Test/hofs/Simple.dfy | 14 +++- Test/hofs/Simple.dfy.expect | 2 +- Test/hofs/TreeMapSimple.dfy | 6 +- Test/hofs/TreeMapSimple.dfy.expect | 1 + Test/hofs/Twice.dfy | 2 +- Test/hofs/Types.dfy | 2 +- Test/hofs/WhileLoop.dfy | 2 +- Test/hofs/WhileLoop.dfy.expect | 1 + 29 files changed, 206 insertions(+), 83 deletions(-) create mode 100644 Test/hofs/Compilation.dfy create mode 100644 Test/hofs/Compilation.dfy.expect (limited to 'Test/hofs') 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 { + 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; + 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 { 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 - reads f.reads(a); -{ - f.reads(a) -} +module ReadsRequiresReads { + function MyReadsOk(f : A -> B, a : A) : set + reads f.reads(a); + { + f.reads(a) + } -function MyReadsOk2(f : A -> B, a : A) : set - reads f.reads(a); -{ - (f.reads)(a) -} + function MyReadsOk2(f : A -> B, a : A) : set + reads f.reads(a); + { + (f.reads)(a) + } -function MyReadsOk3(f : A -> B, a : A) : set - reads (f.reads)(a); -{ - f.reads(a) -} + function MyReadsOk3(f : A -> B, a : A) : set + reads (f.reads)(a); + { + f.reads(a) + } -function MyReadsOk4(f : A -> B, a : A) : set - reads (f.reads)(a); -{ - (f.reads)(a) -} + function MyReadsOk4(f : A -> B, a : A) : set + reads (f.reads)(a); + { + (f.reads)(a) + } -function MyReadsBad(f : A -> B, a : A) : set -{ - f.reads(a) -} + function MyReadsBad(f : A -> B, a : A) : set + { + f.reads(a) + } -function MyReadsBad2(f : A -> B, a : A) : set -{ - (f.reads)(a) -} + function MyReadsBad2(f : A -> B, a : A) : set + { + (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(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 { @@ -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 = Nil | Cons(head: A,tail: List); @@ -27,7 +27,7 @@ function Pre(f : A -> B, s : set) : bool } function method Map(xs : List, f : A -> B): List - 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, f : A -> B): List } function method TMap(t0 : Tree, f : A -> B) : Tree - 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() { 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 { 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 -- cgit v1.2.3