Carry precondition forward as part of the residue

hipsleek · May 18, 2023 · b543c87 · b543c87
1 parent a4a0cf7
commit b543c87
Show file tree

Hide file tree

Showing 3 changed files with 61 additions and 24 deletions.
diff --git a/parsing/entail.ml b/parsing/entail.ml
@@ -614,7 +614,7 @@ let with_pure pi ((p, h) : state) : state = (conj [p; pi], h)
    i: index of stage
    all_vars: all quantified variables
 *)
-let rec check_staged_subsumption2 :
+let rec check_staged_subsumption_aux :
     int ->
     string list ->
     pi ->
@@ -647,7 +647,7 @@ let rec check_staged_subsumption2 :
         (es1.e_evars, (es1.e_pre, es1.e_post, es1.e_ret))
         (es2.e_evars, (es2.e_pre, with_pure arg_eqs es2.e_post, es2.e_ret))
     in
-    check_staged_subsumption2 (i + 1) all_vars
+    check_staged_subsumption_aux (i + 1) all_vars
       (conj [assump; residue])
       (es1r, ns1) (es2r, ns2)
   end
@@ -688,7 +688,7 @@ and stage_subsumes :
     Format.printf "(%s pre) %s => %s%s ==> %s@." what (string_of_pi left)
       (string_of_existentials vs1)
       (string_of_pi right) (string_of_res pre_res);
-    of_bool (conj [pre_r; assump]) pre_res
+    of_bool (conj [pre_l; pre_r; assump]) pre_res
   in
   (* covariance *)
   let new_univ = vars_in_pi pre_l @ vars_in_pi pre_r in
@@ -758,7 +758,7 @@ let check_staged_subsumption : spec -> spec -> unit option =
     (string_of_normalisedStagedSpec (es1, ns1))
     (string_of_normalisedStagedSpec (es2, ns2));
   (* check_staged_subsumption_ (es1, ns1) (es2, ns2) *)
-  check_staged_subsumption2 0
+  check_staged_subsumption_aux 0
     (Forward_rules.getExistientalVar (es1, ns1)
     @ Forward_rules.getExistientalVar (es2, ns2))
     True (es1, ns1) (es2, ns2)

diff --git a/src/programs.t/run.t b/src/programs.t/run.t
@@ -294,7 +294,7 @@
   (Eff 0 pre) T => ex f0,res_1. T ==> true
   (Eff 0 post) T => ex i,ret. res_1=ret/\0=0 ==> true
   (Norm pre) res_1=ret/\0=0 => ex i_2,f3. i_2=z/\i_2=f3 ==> true
-  (Norm post) f3=i_2/\res_1=ret/\0=0/\i_2=z/\i_2=f3 => res_1=ret/\z+1=i_2+1 ==> true
+  (Norm post) f3=i_2/\i_2=z/\i_2=f3/\res_1=ret/\0=0 => res_1=ret/\z+1=i_2+1 ==> true
 
   ========== Function: test21_true ==========
   [Specification] ex i ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
@@ -319,7 +319,7 @@
   (Eff 0 pre) T => ex f0,res_1. T ==> true
   (Eff 0 post) T => ex i,z,ret. res_1=ret/\0=0 ==> true
   (Norm pre) res_1=ret/\0=0 => ex i_2,f3. i_2=z/\i_2=f3 ==> true
-  (Norm post) f3=i_2/\res_1=ret/\0=0/\i_2=z/\i_2=f3 => res_1=ret/\z+1=i_2+1 ==> true
+  (Norm post) f3=i_2/\i_2=z/\i_2=f3/\res_1=ret/\0=0 => res_1=ret/\z+1=i_2+1 ==> true
 
   ========== Function: test0_true ==========
   [Specification] ex i z ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
@@ -344,7 +344,7 @@
   (Eff 0 pre) T => ex f0,res_1. T ==> true
   (Eff 0 post) T => ex i,z,ret. res_1=ret/\0=0 ==> true
   (Norm pre) res_1=ret/\0=0 => ex i_2,f3,i_4. i_2=z/\i_2=f3/\i_2+1=i_4 ==> true
-  (Norm post) f3=i_2/\i_4=i_2+1/\res_1=ret/\0=0/\i_2=z/\i_2=f3/\i_2+1=i_4 => i_4=ret/\z+1=i_4 ==> false
+  (Norm post) f3=i_2/\i_4=i_2+1/\i_2=z/\i_2=f3/\i_2+1=i_4/\res_1=ret/\0=0 => i_4=ret/\z+1=i_4 ==> false
 
   ========== Function: test1_false ==========
   [Specification] ex i z ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
@@ -393,7 +393,7 @@
   (Eff 0 pre) T => ex f0,res_1. T ==> true
   (Eff 0 post) T => ex i,z,ret. res_1=ret/\0=0 ==> true
   (Norm pre) res_1=ret/\0=0 => ex i_2,f3. i_2=z/\i_2=f3 ==> true
-  (Norm post) f3=i_2/\res_1=ret/\0=0/\i_2=z/\i_2=f3 => res_1=ret/\z+1=i_2+2 ==> false
+  (Norm post) f3=i_2/\i_2=z/\i_2=f3/\res_1=ret/\0=0 => res_1=ret/\z+1=i_2+2 ==> false
 
   ========== Function: test3_false ==========
   [Specification] ex i z ret; Eff(i->0, [], ret); req i->z; Norm(i->z+1, ret)
@@ -579,7 +579,7 @@
   ex a; req a->1; Norm(a->1, 1)
 
   (Norm pre) a>0 => ex f0. T ==> true
-  (Norm post) T => 1=1/\1=0 ==> false
+  (Norm post) a>0 => 1=1/\1=0 ==> false
 
   ========== Function: test16_false ==========
   [Specification] ex a; req a->1; Norm(a->1, 1)
@@ -660,6 +660,52 @@
   [Entail  Check] true
   ===========================================
 
+  before tactics
+  Norm(emp, ()); Norm(emp, a+1)
+  <:
+  req a=1; Norm(emp, 2)
+
+  norm, subsumption
+  req emp; Norm(emp, a+1)
+  <:
+  req a=1; Norm(emp, 2)
+
+  (Norm pre) a=1 => T ==> true
+  (Norm post) a=1 => a+1=2 ==> true
+
+  ========== Function: fa ==========
+  [Specification] req a=1; Norm(emp, 2)
+  [Normed   Spec] req a=1; Norm(emp, 2)
+
+  [Raw Post Spec] Norm(emp, ()); Norm(emp, a+1)
+  [Normed   Post] Norm(emp, a+1)
+
+  [Entail  Check] true
+  ==================================
+
+  before tactics
+  Norm(emp, ()); req 1=1; Norm(emp, 2); Norm(emp, 2)
+  <:
+  Norm(emp, 2)
+
+  norm, subsumption
+  req 1=1; Norm(emp, 2)
+  <:
+  req emp; Norm(emp, 2)
+
+  (Norm pre) T => 1=1 ==> true
+  (Norm post) 1=1 => 2=2 ==> true
+
+  ========== Function: test26_true ==========
+  [Specification] Norm(emp, 2)
+  [Normed   Spec] Norm(emp, 2)
+
+  [Raw Post Spec] Norm(emp, ()); req 1=1; Norm(emp, 2); Norm(emp, 2)
+  [Normed   Post] req 1=1; Norm(emp, 2)
+
+  [Entail  Check] true
+  ===========================================
+
 
   $ hip test_ho.ml 2>&1 | grep 'Function\|Entail.*Check' | ./check.py
   TESTS FAILED

diff --git a/src/programs.t/test_new_entail.ml b/src/programs.t/test_new_entail.ml
@@ -208,23 +208,14 @@ let test17_true ()
   let i = ref 0 in 
   1
 
-(* the inferred post state of this function is weird, probably because the existentials are gone *)
-
-(*
-let main_aux ()
-   (*@ ex i;
-      Norm(i->2, ())
-   @*)
-   = (match test () with
-     | v -> v
-     | effect Eff k ->
-       (continue (Obj.clone_continuation k) ());
-       (continue k ())
-     );
-*)
-
 let f1 () (*@ Norm(emp, 1) @*) = 1
 
 let test24_true ()  (*@ Norm(emp, 1) @*) =
   let ret = f1 () in
+  ret
+
+let fa a (*@ req a=1/\emp; Norm(emp, 2) @*) = a + 1
+
+let test26_true ()  (*@ Norm(emp, 2) @*) =
+  let ret = fa 1 in
   ret