cloning + substitution of exception

Author: bgregoir

examples/exception.ec

@@ -8,6 +8,7 @@ op p2: int -> bool.
 
 module M' ={
   proc truc (x:int) : int = {
+  if (! p1 x \/ ! p2 x) else raise assume; 
   ensure (! p1 x \/ ! p2 x) -> assume;
   if (!p1 x \/ !p2 x) { raise assert;}
   return x;
@@ -172,9 +173,11 @@ qed.
 
 exception arg1 of int.
 
+op toto i = arg1 i.
+
 module M3 = {
   proc f () = {
-    raise (arg1 3);
+    raise (toto 3);
   }
 
 }.
@@ -193,6 +196,8 @@ proof.
   proc. wp. skip => //.
 qed.
 
+exception return ['a] 
 
 
 
+exception arg ['a] of 'a.

src/ecParsetree.ml

@@ -1185,7 +1185,7 @@ type theory_cloning = {
 }
 
 and theory_renaming_kind =
-  [ `Lemma | `Op | `Pred | `Type | `Module | `ModType | `Theory]
+  [ `Lemma | `Op | `Pred | `Type | `Module | `ModType | `Theory | `Exn]
 
 and theory_renaming =
   (theory_renaming_kind list * string located pair)

src/ecSubst.ml

@@ -1013,6 +1013,12 @@ let subst_tc (s : subst) tc =
   let tc_axs = List.map (snd_map (subst_form s)) tc.tc_axs in
     { tc_prt; tc_ops; tc_axs; tc_loca = tc.tc_loca }
 
+
+(* -------------------------------------------------------------------- *)
+let subst_excep (s : subst) (ex : excep) =
+  { e_loca = ex.e_loca;
+    e_dom = subst_tys s ex.e_dom }
+
 (* -------------------------------------------------------------------- *)
 (* SUBSTITUTION OVER THEORIES *)
 let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
@@ -1023,8 +1029,8 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
   | Th_operator (x, op) ->
       Th_operator (x, subst_op s op)
 
-  | Th_exception (x, es) ->
-      Th_exception (x, es)
+  | Th_exception (x, ex) ->
+      Th_exception (x, subst_excep s ex)
 
   | Th_axiom (x, ax) ->
       Th_axiom (x, subst_ax s ax)

src/ecSubst.mli

@@ -47,6 +47,7 @@ val subst_tydecl  : subst -> tydecl -> tydecl
 val subst_tc      : subst -> typeclass -> typeclass
 val subst_theory  : subst -> theory -> theory
 val subst_branches : subst -> opbranches -> opbranches
+val subst_excep   : subst -> excep -> excep
 
 (* -------------------------------------------------------------------- *)
 val subst_path         : subst -> path  -> path

src/ecThCloning.ml

@@ -217,6 +217,7 @@ and rk_categories = {
   rkc_module  : bool;
   rkc_modtype : bool;
   rkc_theory  : bool;
+  rkc_exn     : bool;
 }
 
 (* -------------------------------------------------------------------- *)
@@ -231,6 +232,7 @@ let rename ((rk, (rex, itempl)) : renaming) (k, x) =
     | `Selected { rkc_module  = true }, `Module  -> true
     | `Selected { rkc_modtype = true }, `ModType -> true
     | `Selected { rkc_theory  = true }, `Theory  -> true
+    | `Selected { rkc_exn     = true }, `Exn     -> true
     | _, _ -> false in
 
   let newx =
@@ -385,10 +387,12 @@ end = struct
       | Some ({cth_mode = `Concrete} as th) -> th
     in
 
+    (* FIXME improve error message *)
     let rec contains_module cth =
       let doit it =
         match it.ti_item with
         | Th_module _ -> true
+        | Th_exception _ -> true
         | Th_theory (_, cth) -> contains_module cth
         | _ -> false
       in
@@ -435,7 +439,7 @@ end = struct
          let ovrd = (ovrd, mode) in
          nt_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
 
-      | Th_exception _ ->  (proofs, evc)
+      | Th_exception _ -> (proofs, evc)
 
       | Th_axiom (x, _) ->
         let axd = loced (thd @ prefix, x) in
@@ -524,12 +528,13 @@ end = struct
           | `Pred    -> { rk with rkc_preds   = true; }
           | `Module  -> { rk with rkc_module  = true; }
           | `ModType -> { rk with rkc_modtype = true; }
-          | `Theory  -> { rk with rkc_theory  = true; } in
+          | `Theory  -> { rk with rkc_theory  = true; }
+          | `Exn     -> { rk with rkc_exn     = true; } in
 
         let init = {
           rkc_lemmas  = false; rkc_types   = false; rkc_ops     = false;
           rkc_preds   = false; rkc_module  = false; rkc_modtype = false;
-          rkc_theory  = false; } in
+          rkc_theory  = false; rkc_exn     = false } in
 
         `Selected (List.fold_left update init k)
 

src/ecThCloning.mli

@@ -105,6 +105,7 @@ and rk_categories = {
   rkc_module  : bool;
   rkc_modtype : bool;
   rkc_theory  : bool;
+  rkc_exn     : bool;
 }
 
 (* -------------------------------------------------------------------- *)

src/ecTheoryReplay.ml

@@ -364,6 +364,7 @@ let string_of_renaming_kind = function
   | `Module  -> "module"
   | `ModType -> "module type"
   | `Theory  -> "theory"
+  | `Exn     -> "exception"
 
 (* -------------------------------------------------------------------- *)
 let rename ?(fold = true) ove subst (kind, name) =
@@ -386,7 +387,7 @@ let rename ?(fold = true) ove subst (kind, name) =
 
     let nameok =
       match kind with
-      | `Lemma | `Type ->
+      | `Lemma | `Type | `Exn ->
           EcIo.is_sym_ident newname
       | `Op | `Pred ->
           EcIo.is_op_ident newname
@@ -787,11 +788,11 @@ and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oont) =
 
 
 (* -------------------------------------------------------------------- *)
-and replay_excep
-  (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, excep)
-=
-  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_exception (name, excep)) in
-  (subst, ops, proofs, scope)
+and replay_exception (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, excep) =
+  let subst, name = rename ove subst (`Exn, name) in
+  let excep = EcSubst.subst_excep subst excep in
+  let item = Th_exception (name, excep) in
+  (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
 (* -------------------------------------------------------------------- *)
 and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
@@ -1067,7 +1068,7 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
      replay_ntd ove (subst, ops, proofs, scope) (import, x, oont)
 
   | Th_exception (x, e) ->
-    replay_excep ove (subst, ops, proofs, scope) (import, x, e)
+    replay_exception ove (subst, ops, proofs, scope) (import, x, e)
 
   | Th_axiom (x, ax) ->
      replay_axd ove (subst, ops, proofs, scope) (import, x, ax)

src/ecUserMessages.ml

@@ -716,7 +716,7 @@ end = struct
           (string_of_ovkind kd) (string_of_qsymbol x)
 
     | CE_ThyOverride x ->
-        msg "Cannot override theory `%s`: contains module"
+        msg "Cannot override theory `%s`: contains module or exception"
           (string_of_qsymbol x)
 
     | CE_UnkAbbrev x ->