Fix issue 100. Add an axiom for functionHandle to trigger off of the origial

function and connect with Apply1 of the function.

3 files changed, 50 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 51b800a7..3417d4c3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5604,14 +5604,24 @@ namespace Microsoft.Dafny {
         var bvars = new List<Bpl.Variable>();

         var lhs_args = new List<Bpl.Expr>();

         var rhs_args = new List<Bpl.Expr>();

-

+        var func_vars = new List<Bpl.Variable>();

+        var func_args = new List<Bpl.Expr>();

+        var boxed_func_args = new List<Bpl.Expr>();

+        

         var idGen = f.IdGenerator.NestedFreshIdGenerator("$fh$");

         foreach (var fm in f.Formals) {

-          var fe = BplBoundVar(idGen.FreshId("x#"), predef.BoxType, bvars);

+          string fm_name = idGen.FreshId("x#");

+          // Box and its [Unbox]args

+          var fe = BplBoundVar(fm_name, predef.BoxType, bvars);

           lhs_args.Add(fe);

           var be = UnboxIfBoxed(fe, fm.Type);

           rhs_args.Add(be);

           rhs_dict[fm] = new BoogieWrapper(be, fm.Type);

+          // args and its [Box]args

+          var arg = BplBoundVar(fm_name, TrType(fm.Type), func_vars);

+          func_args.Add(arg);

+          var boxed = BoxIfUnboxed(arg, fm.Type);

+          boxed_func_args.Add(boxed);     

         }

 

         var h = BplBoundVar("$heap", predef.HeapType, vars);

@@ -5666,6 +5676,19 @@ namespace Microsoft.Dafny {
           sink.AddTopLevelDeclaration(new Axiom(f.tok,

             BplForall(Cons(bxVar, Concat(vars, bvars)), BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs))));

         }

+

+        {

+          // F(Ty1, .., TyN, Layer, Heap, self, arg1, .., argN)

+          // = [Unbox]Apply1(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, [Box]arg1, ..., [Box]argN)

+

+          var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args));

+          var lhs = FunctionCall(f.tok, f.FullSanitizedName, TrType(f.ResultType), Concat(SnocSelf(Snoc(args, h)), func_args));

+          var rhs = FunctionCall(f.tok, Apply(arity), TrType(f.ResultType), Concat(tyargs, Cons(fhandle, Cons(h, boxed_func_args))));

+          var rhs_unboxed = UnboxIfBoxed(rhs, f.ResultType);

+          

+          sink.AddTopLevelDeclaration(new Axiom(f.tok,

+            BplForall(Concat(vars, func_vars), BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs_unboxed))));

+        }

       }

       return name;

     }

diff --git a/Test/dafny4/Bug100.dfy b/Test/dafny4/Bug100.dfy
new file mode 100644
index 00000000..0c971e82
--- /dev/null
+++ b/Test/dafny4/Bug100.dfy
@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+lemma lemma_ensures(x:int, RefineInt:int->int)

+    requires forall y :: RefineInt.requires(y);

+    ensures forall y :: RefineInt(y) + x == RefineInt(x) + y;

+

+function Identity(z:int) : int

+

+lemma test()

+{

+    var v,w:int;

+    lemma_ensures(w, Identity);

+    //var RefineInt := Identity;

+    //assert RefineInt(v) == Identity(v);

+    assert Identity(v) + w == Identity(w) + v;

+}

+

+

+

+

+

+

diff --git a/Test/dafny4/Bug100.dfy.expect b/Test/dafny4/Bug100.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny4/Bug100.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors