Merge the default optional postcondition for exception into the map of exceptions

Author: lyonel2017

src/ecAst.ml

@@ -294,7 +294,7 @@ and pr = {
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mp.t;
 }
 
 let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv =
@@ -565,33 +565,33 @@ let map_inv3 (fn: form -> form -> form -> form)
       failwith "incompatible invariants for map_inv3"
 
 (* ----------------------------------------------------------------- *)
-type 'a prepoe = 'a * ('a Mp.t * 'a option)
+type 'a prepoe = 'a * ('a Mp.t)
 
 module POE = struct
-  let mk (main : form) (exnmap : form Mp.t * form option) =
+  let mk (main : form) (exnmap : form Mp.t) =
     { main; exnmap; }
 
   let destruct (poe : exnpost) =
     (poe.main, poe.exnmap)
 
   let empty (f : form) : exnpost =
-    { main = f; exnmap = (Mp.empty, None); }
+    { main = f; exnmap = Mp.empty; }
 
-  let is_empty ({ exnmap = (m, dfl) } : exnpost) =
-    Option.is_none dfl && Mp.is_empty m
+  let is_empty ({ exnmap } : exnpost) =
+    Mp.is_empty exnmap
 
   let lift (f : ss_inv) =
     { hsi_m = f.m; hsi_inv = empty f.inv; }
 
   let lower (f : hs_inv) =
     { m = f.hsi_m; inv = f.hsi_inv.main; }
 
-  let map (f : form -> form) ({ main; exnmap = (m, d) } : exnpost) : exnpost =
-    { main = f main; exnmap = (Mp.map f m, omap f d)}
+  let map (f : form -> form) ({ main; exnmap } : exnpost) : exnpost =
+    { main = f main; exnmap = Mp.map f exnmap}
 
   let map2_pre (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 (main1, map1) = poe1 in
+    let (main2, map2) = poe2 in
 
     let merge (a : 'a option) (b : 'b option) =
       match a, b with
@@ -602,9 +602,8 @@ module POE = struct
 
     let main = f main1 main2 in
     let map  = Mp.merge (fun _ -> merge) map1 map2 in
-    let dfl  = merge d1 d2 in
 
-    (main, (map, dfl))
+    (main, map)
 
   let map2 (f : form -> form -> form) (poe1 : exnpost) (poe2 : exnpost) =
     let main, exnmap =
@@ -614,34 +613,28 @@ module POE = struct
 
   let exists (f : form -> bool) (poe : exnpost) =
       f poe.main
-    || Mp.exists (fun _ -> f) (fst poe.exnmap)
-    || omap_dfl f false (snd poe.exnmap)
+    || Mp.exists (fun _ -> f) poe.exnmap
 
   let forall (f : form -> bool) (poe : exnpost) =
       f poe.main
-    && Mp.for_all (fun _ -> f) (fst poe.exnmap)
-    && omap_dfl f true (snd poe.exnmap)
+    && Mp.for_all (fun _ -> f) poe.exnmap
 
   let forall2 (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)
+    && Mp.equal f poe1.exnmap poe2.exnmap
 
-  let to_list_pre ((main, (map, d)) : 'a prepoe) =
-    let l =
-      Mp.fold
-        (fun _ p1 a -> p1 :: a)
-        map
-        [main]
-    in otolist d @ l
+  let to_list_pre ((main, map) : 'a prepoe) =
+    Mp.fold
+      (fun _ p1 a -> p1 :: a)
+      map
+      [main]
 
   let to_list (poe : exnpost) =
     to_list_pre (destruct poe)
 
   let fold (tx : 'a -> form -> 'a) (state : 'a) (poe : exnpost)  =
     let state = tx state poe.main in
-    let state = Mp.fold (fun _ f state -> tx state f) (fst poe.exnmap) state in
-    let state = ofold (fun f state -> tx state f) state (snd poe.exnmap) in
+    let state = Mp.fold (fun _ f state -> tx state f) poe.exnmap state in
     state
 
   let iter (tx : form -> unit) (poe : exnpost)  =
@@ -657,13 +650,7 @@ module POE = struct
     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
+      (Mp.merge (fun _ -> merge) poe1.exnmap poe2.exnmap)
 end
 
 (* ----------------------------------------------------------------- *)
@@ -1059,8 +1046,7 @@ let b_hash (bs : bindings) =
 (*-------------------------------------------------------------------- *)
 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)
+  && Mp.equal f_equal poe1.exnmap poe2.exnmap
 
 (*-------------------------------------------------------------------- *)
 let hf_equal hf1 hf2 =
@@ -1141,13 +1127,9 @@ let post_hash (p : path) (f : form) =
   Why3.Hashcons.combine (EcPath.p_hash p) (f_hash f)
 
 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
+  Mp.fold
+    (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
+    poe.exnmap (f_hash poe.main)
 
 (* -------------------------------------------------------------------- *)
 let hf_hash hf =
@@ -1510,10 +1492,9 @@ module Hsform = Why3.Hashcons.Make (struct
 
   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)
-      (fst poe.exnmap) fv
+      poe.exnmap fv
 
   let fv_node f =
     let union ex nodes =

src/ecAst.mli

@@ -300,7 +300,7 @@ and bdHoareS = {
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mp.t;
 }
 
 and ss_inv = {
@@ -370,7 +370,7 @@ type hs_inv = {
 }
 
 (* -------------------------------------------------------------------- *)
-type 'a prepoe = 'a * ('a Mp.t * 'a option)
+type 'a prepoe = 'a * ('a Mp.t)
 
 module POE : sig
   val empty : form -> exnpost
@@ -381,9 +381,9 @@ module POE : sig
 
   val lower : hs_inv -> ss_inv
 
-  val mk : form -> (form Mp.t * form option) -> exnpost
+  val mk : form -> form Mp.t -> exnpost
 
-  val destruct : exnpost -> form * (form Mp.t * form option)
+  val destruct : exnpost -> form * (form Mp.t)
 
   val to_list_pre : 'a prepoe -> 'a list
 

src/ecCoreLib.ml

@@ -10,6 +10,9 @@ let i_top  = "Top"
 let i_self = "Self"
 let p_top  = EcPath.psymbol i_top
 
+let i_wild = "_"
+let p_wild = EcPath.psymbol i_wild
+
 (* -------------------------------------------------------------------- *)
 let i_Pervasive = "Pervasive"
 let p_Pervasive = EcPath.pqname p_top i_Pervasive

src/ecCoreLib.mli

@@ -23,6 +23,9 @@ val i_top  : symbol
 val i_self : symbol
 val p_top  : path
 
+val i_wild : symbol
+val p_wild : path
+
 (* -------------------------------------------------------------------- *)
 val i_Pervasive : symbol
 val p_Pervasive : path

src/ecPrinting.ml

@@ -1973,7 +1973,12 @@ and pp_form_core_r
       let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
       let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
       let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
-      let { main = post; exnmap = (poe, d) } = (hf_po hf).hsi_inv in
+      let { main = post; exnmap = poe } = (hf_po hf).hsi_inv in
+      let poe, d =
+        match EcPath.Mp.find EcCoreLib.p_wild poe with
+        | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+        | exception Not_found -> poe, None
+      in
       Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_funname ppe) hf.hf_f
         (pp_pl_mem_binding pm ppe) hf.hf_m
@@ -1983,7 +1988,12 @@ and pp_form_core_r
 
   | FhoareS hs ->
       let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
-      let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
+      let { main = post; exnmap = poe; } = (hs_po hs).hsi_inv in
+      let poe, d =
+        match EcPath.Mp.find EcCoreLib.p_wild poe with
+        | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+        | exception Not_found -> poe, None
+      in
       let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
       Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_stmt_for_form ppe) hs.hs_s
@@ -3079,7 +3089,12 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
   let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
   let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
 
-  let { main = post; exnmap = (poe, d); } = (hf_po hf).hsi_inv in
+  let { main = post; exnmap = poe; } = (hf_po hf).hsi_inv in
+  let poe, d =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
 
   Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
   let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
@@ -3093,7 +3108,12 @@ let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs =
   let ppef = PPEnv.push_mem ppe ~active:true hs.hs_m in
   let ppnode = collect2_s ppef hs.hs_s.s_node [] in
 
-  let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
+  let { main = post; exnmap = poe; } = (hs_po hs).hsi_inv in
+  let poe, d =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
 
   let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in
 

src/ecProofTyping.ml

@@ -89,9 +89,9 @@ let pf_process_pattern pe hyps fp =
 let pf_process_poe hyps poe =
   let env  = LDecl.toenv hyps in
   let ue = unienv_of_hyps hyps in
-  let m, d = EcTyping.trans_poe env ue poe in
+  let m = EcTyping.trans_poe env ue poe in
   let ts  = Tuni.subst (EcUnify.UniEnv.close ue) in
-  Mp.map (EcFol.Fsubst.f_subst ts) m, omap (EcFol.Fsubst.f_subst ts) d
+  Mp.map (EcFol.Fsubst.f_subst ts) m
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_form_opt ?mv tc oty pf =
@@ -262,7 +262,14 @@ let destruct_exists ?(reduce = true) hyps fp : dexists option =
     lazy_destruct ~reduce hyps doit fp
 
 (* -------------------------------------------------------------------- *)
-let merge2_poe_list (poe1,d1) (poe2,d2) =
+let merge2_poe_list poe1 poe2 =
+  let aux poe =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
+  let poe1, d1 = aux poe1 in
+  let poe2, d2 = aux poe2 in
   let get_default d =
     match d with
     | Some d -> d

src/ecProofTyping.mli

@@ -33,7 +33,7 @@ val pf_process_xreal    : proofenv -> ?mv:metavs -> LDecl.hyps -> pformula -> fo
 
 val pf_process_exp      : proofenv -> LDecl.hyps -> [`InProc|`InOp] -> ty option -> pexpr -> expr
 val pf_process_pattern  : proofenv -> LDecl.hyps -> pformula -> ptnenv * form
-val pf_process_poe      : LDecl.hyps -> phoare_exception -> form Mp.t * form option
+val pf_process_poe      : LDecl.hyps -> phoare_exception -> form Mp.t
 
 (* Typing in the [proofenv] implies for the [tcenv].
  * Typing exceptions are recasted in the proof env. context *)
@@ -83,7 +83,4 @@ val destruct_product: ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dproduct optio
 val destruct_exists : ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dexists  option
 
 (* -------------------------------------------------------------------- *)
-val merge2_poe_list :
-  form Mp.t * form option ->
-  form Mp.t * form option ->
-  form list
+val merge2_poe_list : form Mp.t -> form Mp.t  -> form list

src/ecReduction.ml

@@ -1344,19 +1344,13 @@ let ztuple args1 args2 ty stk = zpush Ztuple [] args1 args2 ty stk
 let zproj i ty stk = zpush (Zproj i) [] [] [] ty stk
 let zhl f fs1 fs2 stk = zpush (Zhl f) [] fs1 fs2 f.f_ty stk
 
-let zpoe ({ exnmap = (epost, d) } : exnpost) (dpoe : form list) =
-  let d, dpoe =
-    match d, dpoe with
-    | None, _ -> None, dpoe
-    | _, h::q -> Some h, q
-    | _, _ -> assert false
-  in
+let zpoe ({ exnmap = epost } : exnpost) (dpoe : form list) =
   let key = List.map fst (Mp.bindings epost) in
   let poe =
     List.fold_left2
       (fun m a b -> Mp.add a b m)
       Mp.empty key dpoe
-  in (poe,d)
+  in poe
 
 let zpop ri side f hd =
   let args =
@@ -1376,16 +1370,16 @@ let zpop ri side f hd =
   | Zproj i, [f1]      -> f_proj f1 i hd.se_ty
   | Zhl {f_node = FhoareF hf}, (pr :: po :: dpoe) ->
     let m = hf.hf_m in
-    let poe, d = zpoe (hf_po hf).hsi_inv dpoe in
-    f_hoareF {m;inv=pr} hf.hf_f { hsi_m = m; hsi_inv = POE.mk po (poe, d); }
+    let poe = zpoe (hf_po hf).hsi_inv dpoe in
+    f_hoareF {m;inv=pr} hf.hf_f { hsi_m = m; hsi_inv = POE.mk po poe; }
   | Zhl {f_node = FhoareS hs}, (pr :: po :: dpoe) ->
     let m = fst hs.hs_m in
-    let (poe, d) = zpoe (hs_po hs).hsi_inv dpoe in
+    let poe = zpoe (hs_po hs).hsi_inv dpoe in
     f_hoareS
       (snd hs.hs_m)
       { m; inv = pr}
       hs.hs_s
-      { hsi_m = m ; hsi_inv = POE.mk po (poe, d); }
+      { hsi_m = m ; hsi_inv = POE.mk po poe; }
   | Zhl {f_node = FeHoareF hf}, [pr;po] ->
     let m = hf.ehf_m in
     f_eHoareF {m;inv=pr} hf.ehf_f {m;inv=po}
@@ -1510,9 +1504,9 @@ let rec conv ri env f1 f2 stk =
     ->
       let pr2 = (ss_inv_rebind (hf_pr hf2) hf1.hf_m).inv in
       let po2 = (hs_inv_rebind (hf_po hf2) hf1.hf_m).hsi_inv in
-      let aux { main = post; exnmap = (poe, d); } =
+      let aux { main = post; exnmap = poe; } =
         let poe = List.map snd (Mp.bindings poe) in
-        match d with None -> post :: poe | Some d -> post :: d :: poe
+        post :: poe
       in
       let lf1 = aux (hf_po hf1).hsi_inv in
       let lf2 = aux po2 in
@@ -1524,9 +1518,9 @@ let rec conv ri env f1 f2 stk =
     | _subst ->
       let pr2 = (ss_inv_rebind (hs_pr hs2) (fst hs1.hs_m)).inv in
       let po2 = (hs_inv_rebind (hs_po hs2) (fst hs1.hs_m)).hsi_inv in
-      let aux { main = post; exnmap = (poe, d) } =
+      let aux { main = post; exnmap = poe } =
         let poe = List.map snd (Mp.bindings poe) in
-        match d with None -> post :: poe | Some d -> post :: d :: poe
+        post :: poe
       in
       let lf1 = aux (hs_po hs1).hsi_inv in
       let lf2 = aux po2 in

src/ecSubst.ml

@@ -811,14 +811,13 @@ and subst_module (s : subst) (m : module_expr) =
 and subst_hs_inv (s : subst) (inv : hs_inv) =
   let s = add_memory s inv.hsi_m inv.hsi_m in
   let main = subst_form s inv.hsi_inv.main in
-  let map =
+  let exnmap =
     Mp.fold (fun p f m ->
       let p = subst_path s p in
       let f = subst_form s f in
       Mp.add p f m
-    ) (fst inv.hsi_inv.exnmap) Mp.empty in
-  let dfl = omap (subst_form s) (snd inv.hsi_inv.exnmap) in
-  { hsi_inv = { main; exnmap = (map, dfl) }; hsi_m = inv.hsi_m }
+    ) inv.hsi_inv.exnmap Mp.empty in
+  { hsi_inv = { main; exnmap }; hsi_m = inv.hsi_m }
 
 (* -------------------------------------------------------------------- *)
 let subst_modsig ?params (s : subst) (comps : module_sig) =