almost done

songyahui · May 8, 2024 · cca5b94 · cca5b94
1 parent b8135a7
commit cca5b94
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 19 deletions.
diff --git a/parsing/forward_rules.ml b/parsing/forward_rules.ml
@@ -480,38 +480,41 @@ let rec resolveInnerTryCatches typ env (match_summary:tryCatchLemma option) (spe
 
       let spec_body'= normalize_spec (NormalReturn(pi, heap)::spec_body) in 
       print_endline ("--------\n spec_body' " ^ string_of_normalisedStagedSpec spec_body');
+      print_endline ("\n handler:' " ^ string_of_handlingcases (h_n, h_eff)^"\n");
 
       let phi1, _ = handling_spec typ env match_summary spec_body' h_n h_eff  in 
+      print_endline ("--------\n phi1 " ^ string_of_disj_spec phi1 ^"\n");
 
-      let ret =
-          match phi1 with 
-          | [spec_body] ->
-            (match unsnoc spec_body with
+      let res = 
+        List.map 
+        (fun phi1_spec_body -> 
+        let ret =
+            (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 (_, _, _, ret) | _, HigherOrder (_, _, _, ret) |  _, TryCatch (_, _, _, ret) -> failwith (Format.asprintf "ret not a variable: %s" (string_of_term ret))
             | _ -> 
-            (match retriveLastRes spec_body with 
+            (match retriveLastRes phi1_spec_body with 
             | Some (Var v) -> v 
             | _ -> "res"
-            )
-            )
-          | _ -> "res"
+            ))
       in
 
-      print_endline ("--------\n phi1' " ^ string_of_disj_spec phi1 ^"\n");
 
-      print_endline ("returns are " ^ ret ^ string_of_term ret');
-      (* And(pi, ) *)
+      print_endline ("returns are " ^ ret ^ " " ^ string_of_term ret');
 
-      let phi1 = List.map (fun spec -> (NormalReturn (Atomic(EQ, Var ret,ret' ), EmptyHeap))::spec) phi1 in 
-      print_endline ("\n handler:' " ^ string_of_handlingcases (h_n, h_eff)^"\n");
+      let phi1_spec_body' = (NormalReturn (Atomic(EQ, Var ret,ret' ), EmptyHeap)) :: phi1_spec_body in 
+      print_endline ("--------\n phi1' " ^ string_of_spec phi1_spec_body' ^"\n");
+
+      phi1_spec_body'
+      )
+
+      phi1 in 
 
-
       let phi2 = (helper xs) in 
-      if List.length phi2 == 0 then phi1
-      else flattenList(List.map (fun tail -> List.map (fun hd -> hd @ tail) phi1) phi2)
+      if List.length phi2 == 0 then res
+      else flattenList(List.map (fun tail -> List.map (fun hd -> hd @ tail) res) phi2)
 
 
     | x ::xs -> 

diff --git a/src/demo/7_amb.ml b/src/demo/7_amb.ml
@@ -70,8 +70,7 @@ try
  catch {
     x -> ens res=x 
   | (Success r) -> ens res=r 
- }[hr] ;
- ens res= hr
+ }[hr] 
 @*)
 = 
   match iter (helperk) xs; perform (Failure 404) with 
@@ -87,7 +86,7 @@ let amb (xs) counter : bool
 
 let m xs counter
 (*@ ex r1; Choose(emp, (xs), r1); ex x r; req counter->x; Norm(counter->x+1 /\ r1= true /\ res =r /\ r=7 ) 
- \/ ex r1; Choose(emp, (xs), r1); ex r2 x;req counter->x; Failure(counter->x+1 /\r1=false, 500, r2); Norm(res =r2 ) @*)
+ \/ ex r1; Choose(emp, (xs), r1); ex r2 x;req counter->x; Failure(counter->x+1 /\r1=false, 500, r2) @*)
 = if amb xs counter then 7 
   else 
     perform (Failure 500)