working amb

songyahui · May 9, 2024 · 79ea5b3 · 79ea5b3
1 parent cca5b94
commit 79ea5b3
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 12 deletions.
diff --git a/parsing/forward_rules.ml b/parsing/forward_rules.ml
@@ -488,23 +488,23 @@ let rec resolveInnerTryCatches typ env (match_summary:tryCatchLemma option) (spe
       let res = 
         List.map 
         (fun phi1_spec_body -> 
-        let ret =
+        let (ret:term) =
             (match unsnoc phi1_spec_body with
-            | _, RaisingEff (_pre, _post, _constr, Var ret) -> ret
-            | _, HigherOrder (_pre, _post, _constr, Var ret) -> ret
-            | _, TryCatch (_pre, _post, _constr, Var ret) -> ret
+            | _, RaisingEff (_pre, _post, _constr, ret) -> ret
+            | _, HigherOrder (_pre, _post, _constr, ret) -> ret
+            | _, TryCatch (_pre, _post, _constr, ret) -> ret
             | _, RaisingEff (_, _, _, ret) | _, HigherOrder (_, _, _, ret) |  _, TryCatch (_, _, _, ret) -> failwith (Format.asprintf "ret not a variable: %s" (string_of_term ret))
             | _ -> 
             (match retriveLastRes phi1_spec_body with 
-            | Some (Var v) -> v 
-            | _ -> "res"
+            | Some t -> t
+            | _ -> Var "res"
             ))
       in
 
 
-      print_endline ("returns are " ^ ret ^ " " ^ string_of_term ret');
+      print_endline ("returns are " ^ string_of_term ret ^ " " ^ string_of_term ret');
 
-      let phi1_spec_body' = (NormalReturn (Atomic(EQ, Var ret,ret' ), EmptyHeap)) :: phi1_spec_body in 
+      let phi1_spec_body' = (NormalReturn (Atomic(EQ, ret,ret' ), EmptyHeap)) :: phi1_spec_body in 
       print_endline ("--------\n phi1' " ^ string_of_spec phi1_spec_body' ^"\n");
 
       phi1_spec_body'

diff --git a/src/demo/7_amb.ml b/src/demo/7_amb.ml
@@ -94,16 +94,20 @@ let m xs counter
 
 let handle (xs) counter 
 (*@ 
-ex r c a r1; req counter -> a; containRetTrue (xs, c, r1); ens counter->a+c /\ r1 = true /\ res = r /\ r=7 
+ex v1308; Failure(xs=[], (404), v1308); ens res=v1308 \/ 
+ex v1311; req counter->v1311; ens counter->(v1311+1)/\is_cons(xs)=true/\head_r=true/\res=7 \/ 
+ex t v1230 v1268 v1269 v1270; req counter->v1230/\(v1230+1)=v1268; ens tail(xs)=t/\is_cons(xs)=true/\head_r=false/\v1268=(v1230+1); containRetTrue(t, v1269, v1270); ens counter->(v1268+v1269)/\v1270=true/\res=7 \/ 
+ex t v1230 v1273 v1274 v1275; req counter->v1230/\(v1230+1)=v1273; ens tail(xs)=t/\is_cons(xs)=true/\head_r=false/\v1273=(v1230+1); containRetTrue(t, v1274, v1275); ex v1226; Failure(counter->(v1273+v1274)/\v1275=false, (500), v1226); ens res=v1226
 @*)
-(* \/ ex r c a r1; req counter -> a; containRetTrue (xs, c, r1); Failure(counter->a+c /\r1=false, 500, r) *)
+(* 
+ex r c a r1; req counter -> a; containRetTrue (xs, c, r1); ens counter->a+c /\ r1 = true /\ res = r /\ r=7    
+\/ ex r c a r1; req counter -> a; containRetTrue (xs, c, r1); Failure(counter->a+c /\r1=false, 500, r) *)
 = match m xs counter with
   (* try-catch lemma defined here *)
   (*@   try ex t r;  iter(helperk, t,r) # ex r200; Failure(emp, (404), r200) catch 
-     =  ex r c a r1; req counter -> a; containRetTrue (t, c, r1); ens counter->a+c /\ r1 = true /\ res = r /\ r=7 
+     =  ex r c a r1; req counter -> a; containRetTrue (t, c, r1); ens counter->a+c /\ r1 = true /\ res=7 
      \/ ex r c a r1; req counter -> a; containRetTrue (t, c, r1); Failure(counter->a+c /\r1=false, 500, r)
   @*) 
-
   | x -> x
   | effect (Choose xs) k -> aux k xs