WIP

Author: strub

examples/exception.ec

@@ -176,7 +176,6 @@ module M3 = {
   proc f () = {
     raise (toto 3);
   }
-
 }.
 
 lemma test5 :
@@ -195,7 +194,6 @@ qed.
 
 
 abstract theory Et.
-
   type t.
 
   op test : t -> bool.
@@ -218,7 +216,6 @@ abstract theory Et.
 end Et.
 
 require import List.
-print list.
 
 exception et1 of int.
 

src/ecAst.ml

@@ -234,20 +234,18 @@ and equivS = {
   es_sr  : stmt;
   es_po  : form; }
 
-and post = (form * form Mp.t * form option)
-
 and sHoareF = {
   hf_m  : memory;
   hf_pr : form;
   hf_f  : EcPath.xpath;
-  hf_po : post;
+  hf_po : exnpost;
 }
 
 and sHoareS = {
   hs_m  : memenv;
   hs_pr : form;
   hs_s  : stmt;
-  hs_po : post;
+  hs_po : exnpost;
 }
 
 and eHoareF = {
@@ -294,6 +292,11 @@ and pr = {
   pr_event : ss_inv;
 }
 
+and exnpost = {
+  main   : form;
+  exnmap : form Mp.t * form option;
+}
+
 let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv =
   let m' = match m with
   | Some m -> m
@@ -463,10 +466,9 @@ let ts_inv_lower_right3 (fn: ss_inv -> ss_inv -> ss_inv -> form)
   { m = inv1.ml; inv = inv' }
 
 (* ----------------------------------------------------------------- *)
-
 type hs_inv = {
-  hsi_m : memory;
-  hsi_inv : post;
+  hsi_m   : memory;
+  hsi_inv : exnpost;
 }
 
 type inv =
@@ -508,7 +510,7 @@ let lift_ss_inv3 (f: ss_inv -> ss_inv -> ss_inv -> 'a) : inv -> inv -> inv -> 'a
 let lift_ts_inv (f: ts_inv -> 'a) : inv -> 'a =
   let f inv = match inv with
   | Inv_ts ss -> f ss
-  |  _ -> failwith "expected two sided invariant" in
+  | _ -> failwith "expected two sided invariant" in
   f
 
 let lift_ts_inv2 (f: ts_inv -> ts_inv -> 'a) : inv -> inv -> 'a =
@@ -535,15 +537,15 @@ let map_inv (fn: form list -> form) (inv: inv list): inv =
       Inv_ts (map_ts_inv fn (List.map (function
         Inv_ts ts -> assert (ts.ml = ts'.ml && ts.mr = ts'.mr); ts
         | _ -> failwith "expected all invariants to have same kind") inv))
-  | _ ->  failwith  "Exceptions are not supported"
+  | Inv_hs _ ->  failwith  "Exceptions are not supported"
 
 let map_inv1 (fn: form -> form) (inv: inv): inv =
   match inv with
   | Inv_ss ss ->
       Inv_ss (map_ss_inv1 fn ss)
   | Inv_ts ts ->
       Inv_ts (map_ts_inv1 fn ts)
-  | _ -> failwith  "Exceptions are not supported"
+  | Inv_hs _ -> failwith  "Exceptions are not supported"
 
 let map_inv2 (fn: form -> form -> form) (inv1: inv) (inv2: inv): inv =
   match inv1, inv2 with
@@ -565,92 +567,121 @@ let map_inv3 (fn: form -> form -> form -> form)
       failwith "incompatible invariants for map_inv3"
 
 (* ----------------------------------------------------------------- *)
-let empty_poe f = (f, Mp.empty, None)
+type 'a prepoe = 'a * ('a Mp.t * 'a option)
 
-let empty_hs f =
-  {hsi_m=f.m;hsi_inv = empty_poe f.inv}
+let mk_poe (main : form) (exnmap : form Mp.t * form option) =
+  { main; exnmap; }
 
-let is_empty_poe poe =
-  match poe with
-  | (_,m,None) when Mp.is_empty m-> true
-  | _ -> false
+let destruct_poe (poe : exnpost) =
+  (poe.main, poe.exnmap)
+
+let empty_poe (f : form) : exnpost =
+  { main = f; exnmap = (Mp.empty, None); }
 
-let lift_f f = {hsi_m=f.m;hsi_inv=empty_poe f.inv}
+let empty_hs (f : ss_inv) =
+  { hsi_m = f.m; hsi_inv = empty_poe f.inv; }
 
-let lower_f f =
-  let (post, _,_) = f.hsi_inv in
-  {m=f.hsi_m;inv=post}
+let is_empty_poe ({ exnmap = (m, dfl) } : exnpost) =
+  Option.is_none dfl && Mp.is_empty m
 
-let update_hs_ss f p =
-  assert (f.m == p.hsi_m);
-  let (_,m,d) = p.hsi_inv in
-  {p with hsi_inv=(f.inv,m,d)}
+let lift_f (f : ss_inv) =
+  { hsi_m = f.m; hsi_inv = empty_poe f.inv; }
 
-let map_poe f (p,m,d) =
-  let p = f p in
-  let m = Mp.map f m in
-  let d = omap f d in
-  (p, m, d)
+let lower_f (f : hs_inv) =
+  { m = f.hsi_m; inv = f.hsi_inv.main; }
 
-let map_hs_inv1 f inv1 =  {inv1 with hsi_inv = map_poe f inv1.hsi_inv}
+let update_hs_ss (f : ss_inv) (p : hs_inv) : hs_inv =
+  assert (f.m ==(*phy*) p.hsi_m);
+  { p with hsi_inv = { main = f.inv; exnmap = p.hsi_inv.exnmap; } }
 
-let map2_poe f (p1,m1,d1) (p2,m2,d2) =
-  let p = f p1 p2 in
-  let aux _ a b =
+let map_poe (f : form -> form) ({ main; exnmap = (m, d) } : exnpost) : exnpost =
+  { main = f main; exnmap = (Mp.map f m, omap f d)}
+
+let map_hs_inv1 (f : form ->form) (inv1 : hs_inv) = 
+  { inv1 with hsi_inv = map_poe f inv1.hsi_inv; }
+
+let map2_prepoe (f : 'a -> 'b -> 'c) (poe1 : 'a prepoe) (poe2 : 'b prepoe) : 'c prepoe =
+  let (main1, (map1, d1)) = poe1 in
+  let (main2, (map2, d2)) = poe2 in
+
+  let merge (a : 'a option) (b : 'b option) =
     match a, b with
-    | Some a, Some b -> Some (f a b)
-    | _ , _ -> failwith "missing entry in exception map"
+    | None, None -> None
+    | Some a, Some b ->  Some (f a b)
+    | _ -> assert false
   in
-  let m = Mp.merge aux m1 m2 in
-  match d1, d2 with
-  | None, None -> (p, m, None)
-  | Some d1, Some d2 -> (p, m, Some (f d1 d2))
-  | _, _ -> failwith "missing default exception"
+
+  let main = f main1 main2 in
+  let map  = Mp.merge (fun _ -> merge) map1 map2 in
+  let dfl  = merge d1 d2 in
+
+  (main, (map, dfl))
+
+let map2_poe (f : form -> form -> form) (poe1 : exnpost) (poe2 : exnpost) =
+  let main, exnmap =
+    map2_prepoe f (destruct_poe poe1) (destruct_poe poe2) in
+
+  mk_poe main exnmap
 
 let map_hs_inv2
-    (fn: form -> form -> form) (inv1: hs_inv) (inv2: hs_inv): hs_inv =
+    (fn   : form -> form -> form)
+    (inv1 : hs_inv)
+    (inv2 : hs_inv)
+  : hs_inv
+  =
   assert (inv1.hsi_m = inv2.hsi_m);
-  let inv' = map2_poe fn inv1.hsi_inv inv2.hsi_inv in
-  { hsi_m = inv1.hsi_m; hsi_inv = inv' }
+  let inv = map2_poe fn inv1.hsi_inv inv2.hsi_inv in
+  { hsi_m = inv1.hsi_m; hsi_inv = inv }
 
-let exists_poe f (p,m,d) =
-  f p || Mp.exists (fun _ -> f) m || omap_dfl f false d
+let exists_poe (f : form -> bool) (poe : exnpost) =
+     f poe.main
+  || Mp.exists (fun _ -> f) (fst poe.exnmap)
+  || omap_dfl f false (snd poe.exnmap)
 
-let forall_poe f (p,m,d) =
-  f p && Mp.for_all (fun _ -> f) m && omap_dfl f true d
+let forall_poe (f : form -> bool) (poe : exnpost) =
+     f poe.main
+  && Mp.for_all (fun _ -> f) (fst poe.exnmap)
+  && omap_dfl f true (snd poe.exnmap)
 
-let forall2_poe f (p1,m1,d1) (p2,m2,d2) =
-  let b1 = f p1 p2 in
-  let b2 = Mp.equal f m1 m2 in
-  b1 && b2 && oeq f d1 d2
+let forall2_poe (f : form -> form -> bool) (poe1 : exnpost) (poe2 : exnpost) =
+     f poe1.main poe2.main
+  && Mp.equal f (fst poe1.exnmap) (fst poe2.exnmap)
+  && oeq f (snd poe1.exnmap) (snd poe2.exnmap)
 
-let poe_to_list (post,poe,d) =
+let prepoe_to_list ((main, (map, d)) : 'a prepoe) =
   let l =
     Mp.fold
       (fun _ p1 a -> p1 :: a)
-      poe
-      [post]
+      map
+      [main]
   in
   otolist d @ l
 
-let iter_poe f (p, m,d) =
-  f p;
-  Mp.iter (fun _ -> f) m;
-  oiter f d
+let poe_to_list (poe : exnpost) =
+  prepoe_to_list (destruct_poe poe)
+
+let iter_poe (f : form -> unit) (poe : exnpost)  =
+  f poe.main;
+  Mp.iter (fun _ -> f) (fst poe.exnmap);
+  oiter f (snd poe.exnmap)
 
-let iter2_poe f (p1,m1,d1) (p2,m2,d2) =
-  f p1 p2;
-  let aux _ a b =
+let iter2_poe (f : form -> form -> unit) (poe1 : exnpost) (poe2 : exnpost) =
+  let merge (a : form option) (b : form option) =
     match a, b with
-    | Some a, Some b -> Some (a,b)
-    | _ , _ -> failwith "missing entry in exception map"
-  in
-  let m = Mp.merge aux m1 m2 in
-  Mp.iter (fun _ (p1,p2) -> f p1 p2) m;
-  match d2, d1 with
-  | None, None -> ()
-  | Some d1, Some d2 -> f d1 d2
-  | _, _ -> failwith "missing default exception"
+    | None, None -> None
+    | Some a, Some b -> Some (a, b)
+    | _, _ -> assert false in
+
+  f poe1.main poe2.main;
+  Mp.iter
+    (fun _ (a, b) -> f a b)
+    (Mp.merge (fun _ -> merge) (fst poe1.exnmap) (fst poe2.exnmap));
+  begin
+    match snd poe1.exnmap, snd poe2.exnmap with
+    | None, None -> ()
+    | Some a, Some b -> f a b
+    | _, _ -> assert false
+  end
 
 (* ----------------------------------------------------------------- *)
 (* Accessors for program logic                                       *)
@@ -665,8 +696,8 @@ let ef_po ef = {ml=ef.ef_ml; mr=ef.ef_mr; inv=ef.ef_po}
 let es_pr es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_pr}
 let es_po es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_po}
 
-let hf_pr hf =  {m=hf.hf_m; inv=hf.hf_pr}
-let hf_po hf =  {hsi_m=hf.hf_m; hsi_inv=hf.hf_po}
+let hf_pr hf = {m=hf.hf_m; inv=hf.hf_pr}
+let hf_po hf = {hsi_m=hf.hf_m; hsi_inv=hf.hf_po}
 
 let hs_pr hs = {m=fst hs.hs_m; inv=hs.hs_pr}
 let hs_po hs = {hsi_m=fst hs.hs_m; hsi_inv=hs.hs_po}
@@ -1022,18 +1053,12 @@ let b_hash (bs : bindings) =
     Why3.Hashcons.combine_list b1_hash 0 bs
 
 (*-------------------------------------------------------------------- *)
-
-let posts_equal (post1, eposts1, d1) (post2, eposts2, d2) =
-  let b = f_equal post1 post2 in
-  let b =  b && Mp.equal f_equal eposts1 eposts2 in
-  b &&
-  match d1, d2 with
-  | Some f1, Some f2 -> f_equal f1 f2
-  | None, None -> true
-  | _, _ -> false
+let posts_equal (poe1 : exnpost) (poe2 : exnpost) =
+     f_equal poe1.main poe2.main
+  && Mp.equal f_equal (fst poe1.exnmap) (fst poe2.exnmap)
+  && oeq f_equal (snd poe1.exnmap) (snd poe2.exnmap)
 
 (*-------------------------------------------------------------------- *)
-
 let hf_equal hf1 hf2 =
      f_equal hf1.hf_pr hf2.hf_pr
   && posts_equal hf1.hf_po hf2.hf_po
@@ -1108,14 +1133,17 @@ let pr_equal pr1 pr2 =
   && mem_equal        pr1.pr_event.m pr2.pr_event.m
 
 (*-------------------------------------------------------------------- *)
+let post_hash (p : path) (f : form) =
+  Why3.Hashcons.combine (EcPath.p_hash p) (f_hash f)
 
-let post_hash e f = Why3.Hashcons.combine (EcPath.p_hash e) (f_hash f)
-
-let posts_hash (post, posts,d) =
-  let h = Why3.Hashcons.combine (f_hash post) (omap_dfl f_hash 0 d) in
-  Mp.fold
-    (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
-    posts h
+let posts_hash (poe : exnpost) =
+  let h =
+    Why3.Hashcons.combine
+      (f_hash poe.main) (omap_dfl f_hash 0 (snd poe.exnmap))
+  in
+    Mp.fold
+      (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
+      (fst poe.exnmap) h
 
 (* -------------------------------------------------------------------- *)
 let hf_hash hf =
@@ -1476,12 +1504,12 @@ module Hsform = Why3.Hashcons.Make (struct
 
   let fv_mlr ml mr = Sid.add ml (Sid.singleton mr)
 
-  let posts_fv (post, posts, d) =
-    let fv = f_fv post in
-    let fv = d |> omap f_fv |> odfl fv in
+  let posts_fv (poe : exnpost) =
+    let fv = f_fv poe.main in
+    let fv = snd poe.exnmap |> omap f_fv |> odfl fv in
     Mp.fold
       (fun _ f acc -> fv_union (f_fv f) acc)
-       posts fv
+      (fst poe.exnmap) fv
 
   let fv_node f =
     let union ex nodes =