Represent exception default postconditions inside the exception map

Store exceptional postconditions as a single `Mop.t`, using the
default case as the `None` key instead of a separate optional field.

Author: lyonel2017

src/ecAst.ml

@@ -294,7 +294,7 @@ and pr = {
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mop.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 Mop.t)
 
 module POE = struct
-  let mk (main : form) (exnmap : form Mp.t * form option) =
+  let mk (main : form) (exnmap : form Mop.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 = Mop.empty; }
 
-  let is_empty ({ exnmap = (m, dfl) } : exnpost) =
-    Option.is_none dfl && Mp.is_empty m
+  let is_empty ({ exnmap } : exnpost) =
+    Mop.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 = Mop.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
@@ -601,10 +601,9 @@ module POE = struct
     in
 
     let main = f main1 main2 in
-    let map  = Mp.merge (fun _ -> merge) map1 map2 in
-    let dfl  = merge d1 d2 in
+    let map  = Mop.merge (fun _ -> merge) map1 map2 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)
+    || Mop.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)
+    && Mop.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)
+    && Mop.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) =
+    Mop.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 = Mop.fold (fun _ f state -> tx state f) poe.exnmap state in
     state
 
   let iter (tx : form -> unit) (poe : exnpost)  =
@@ -655,15 +648,9 @@ module POE = struct
       | _, _ -> assert false in
 
     f poe1.main poe2.main;
-    Mp.iter
+    Mop.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
+      (Mop.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)
+  && Mop.equal f_equal poe1.exnmap poe2.exnmap
 
 (*-------------------------------------------------------------------- *)
 let hf_equal hf1 hf2 =
@@ -1137,17 +1123,15 @@ 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 posts_hash (poe : exnpost) =
-  let h =
+  let post_hash (p : path option) (f : form) =
     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
+      (Why3.Hashcons.combine_option EcPath.p_hash p)
+      (f_hash f) in
+
+  Mop.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 +1494,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
+    Mop.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

@@ -294,13 +294,13 @@ and bdHoareS = {
   bhs_po  : form;
   [@alert priv_pl "Use the accessor function `bhs_po` instead of the field"]
   bhs_cmp : hoarecmp;
-  bhs_bd  : form;
+  bhs_bd  : form; 
   [@alert priv_pl "Use the accessor function `bhs_bd` instead of the field"]
 }
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mop.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 Mop.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 Mop.t -> exnpost
 
-  val destruct : exnpost -> form * (form Mp.t * form option)
+  val destruct : exnpost -> form * (form Mop.t)
 
   val to_list_pre : 'a prepoe -> 'a list
 

src/ecPrinting.ml

@@ -19,6 +19,7 @@ module Msym = EcSymbols.Msym
 module Sid  = EcIdent.Sid
 module Mid  = EcIdent.Mid
 module Sp   = EcPath.Sp
+module Mop  = EcPath.Mop
 
 (* -------------------------------------------------------------------- *)
 type prpo_display = { prpo_pr : bool; prpo_po : bool; }
@@ -1836,7 +1837,7 @@ and try_pp_notations
     let f    = f_app (f_op p tv rty) (args @ eargs) f.f_ty in
     pp_form_core_r ppe outer fmt f; true
 
-and pp_poe ppe fmt (l,d) =
+and pp_poe (ppe : PPEnv.t) (fmt : Format.formatter) (poe : form Mop.t) =
   let pp_branch fmt (e, f) =
     let bd, br = EcFol.decompose_lambda f in
     let doarg (x, gty) =
@@ -1850,7 +1851,14 @@ and pp_poe ppe fmt (l,d) =
     let ppe = PPEnv.add_locals ppe (List.map fst bd) in
     Format.fprintf fmt "@[<hov 2>| %a =>@ %a]" (pp_form ppe) eargs (pp_form ppe) br
   in
-  (pp_list "@ " pp_branch) fmt (EcPath.Mp.bindings l);
+
+  let poe, d =
+    List.partition_map (fun (p, v) ->
+      match p with Some p -> Left (p , v) | None -> Right v
+    ) (Mop.bindings poe) in
+  let d = List.ohead d in
+
+  (pp_list "@ " pp_branch) fmt poe;
   oiter (fun br -> Format.fprintf fmt "@[<hov 2>| _ =>@ %a]" (pp_form ppe) br) d
 
 and pp_form_core_r
@@ -1985,24 +1993,24 @@ 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
       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
         (pp_form ppepr) (hf_pr hf).inv
         (pp_form ppepo) (post)
-        (pp_poe ppepo) (poe, d)
+        (pp_poe ppepo) poe
 
   | 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 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
         (pp_pl_mem_binding pm ppe) (fst hs.hs_m)
         (pp_form ppe) (hs_pr hs).inv
         (pp_form ppe) post
-        (pp_poe ppe) (poe, d)
+        (pp_poe ppe) poe
 
   | FeHoareF hf ->
       let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_m hf.ehf_f ppe.PPEnv.ppe_env in
@@ -3092,8 +3100,8 @@ let pp_post (ppe : PPEnv.t) ?prpo fmt post =
     fmt post None
 
 (* -------------------------------------------------------------------- *)
-let pp_poe (ppe : PPEnv.t) ?prpo (fmt: Format.formatter) (poe,d) =
-  let pp_branch e f =
+let pp_poe (ppe : PPEnv.t) ?prpo (fmt: Format.formatter) poe =
+  let pp_branch (p : EcPath.path) (f : form) =
     let bd, br = EcFol.decompose_lambda f in
     let doarg (x, gty) =
       match gty with
@@ -3102,41 +3110,42 @@ let pp_poe (ppe : PPEnv.t) ?prpo (fmt: Format.formatter) (poe,d) =
     let args = List.map doarg bd in
     let tys = List.map (fun (_, ty) -> EcFol.as_gtty ty) bd in
     let ty = EcTypes.toarrow tys EcTypes.texn in
-    let eargs = EcFol.f_app (EcFol.f_op e [] ty) args EcTypes.texn in
+    let eargs = EcFol.f_app (EcFol.f_op p [] ty) args EcTypes.texn in
     let ppe = PPEnv.add_locals ppe (List.map fst bd) in
     pp_prpo ppe
       (pp_form ppe) eargs
       (omap (fun x -> x.prpo_po) prpo |> odfl false)
       fmt br None
   in
-  EcPath.Mp.iter pp_branch poe;
+
+  EcPath.Mop.iter (fun p f -> oiter (pp_branch^~ f) p) poe;
   oiter (fun d ->
       pp_prpo ppe Format.pp_print_string "_"
         (omap (fun x -> x.prpo_po) prpo |> odfl false)
-        fmt d None) d
+        fmt d None)
+      (Mop.find_opt None poe)
 
 (* -------------------------------------------------------------------- *)
 let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
   let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in
   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
 
   Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
   let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
   Format.fprintf fmt "    %a %a@\n%!" (pp_funname ppe) hf.hf_f (pp_pl_mem_binding pm ppe) hf.hf_m;
   Format.fprintf fmt "@\n%a" (pp_post ppepo ?prpo) post;
-  Format.fprintf fmt "@\n%a%!" (pp_poe ppepo ?prpo) (poe,d)
+  Format.fprintf fmt "@\n%a%!" (pp_poe ppepo ?prpo) poe
 
 (* -------------------------------------------------------------------- *)
 
 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 ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in
 
   Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m)
@@ -3148,7 +3157,7 @@ let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs =
   Format.fprintf fmt "@\n%!";
   Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) post;
   Format.fprintf fmt "@\n%!";
-  Format.fprintf fmt "%a%!" (pp_poe ppef ?prpo) (poe,d)
+  Format.fprintf fmt "%a%!" (pp_poe ppef ?prpo) poe
 
 (* -------------------------------------------------------------------- *)
 let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf =

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
+  Mop.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 : form Mop.t) (poe2 : form Mop.t) =
+  let remove_default (poe : form Mop.t) =
+    match Mop.find_opt None poe with
+    | None   -> poe, None
+    | Some x -> Mop.remove None poe, Some x
+  in
+  let poe1, d1 = remove_default poe1 in
+  let poe2, d2 = remove_default poe2 in
   let get_default d =
     match d with
     | Some d -> d
@@ -285,8 +292,8 @@ let merge2_poe_list (poe1,d1) (poe2,d2) =
 
     | None, None -> assert false
   in
-  let epost = Mp.merge aux poe1 poe2 in
-  let poe = List.map snd (Mp.bindings epost) in
+  let epost = Mop.merge aux poe1 poe2 in
+  let poe = List.map snd (Mop.bindings epost) in
   match d2, d1 with
   | None, _ -> poe
   | Some d2, Some d1 -> f_imp d2 d1 :: poe