Fix renaming of exceptions

Author: strub

src/ecParser.mly

@@ -3608,6 +3608,7 @@ clone_rename_kind:
 | TYPE        { `Type    }
 | OP          { `Op      }
 | PRED        { `Pred    }
+| EXCEPTION   { `Exn     }
 | LEMMA       { `Lemma   }
 | MODULE      { `Module  }
 | MODULE TYPE { `ModType }

src/ecParsetree.ml

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

src/ecThCloning.ml

@@ -214,6 +214,7 @@ and rk_categories = {
   rkc_lemmas  : bool;
   rkc_ops     : bool;
   rkc_preds   : bool;
+  rkc_exns    : bool;
   rkc_types   : bool;
   rkc_module  : bool;
   rkc_modtype : bool;
@@ -230,7 +231,7 @@ type octxt = {
 module Renaming : sig
   val rename1 : octxt -> theory_renaming -> renaming
 end = struct
-  let rename1 oc (k, (r1, r2)) : renaming =
+  let rename1 oc ((k : theory_renaming_kind list), (r1, r2)) : renaming =
     let e1 =
       try  EcRegexp.regexp (unloc r1)
       with EcRegexp.Error _ -> clone_error oc.oc_env (CE_InvalidRE (unloc r1)) in
@@ -253,14 +254,15 @@ end = struct
           | `Type    -> { rk with rkc_types   = true; }
           | `Op      -> { rk with rkc_ops     = true; }
           | `Pred    -> { rk with rkc_preds   = true; }
+          | `Exn     -> { rk with rkc_exns    = true; }
           | `Module  -> { rk with rkc_module  = true; }
           | `ModType -> { rk with rkc_modtype = true; }
           | `Theory  -> { rk with rkc_theory  = 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_lemmas  = false; rkc_types  = false; rkc_ops    = false;
+          rkc_preds   = false; rkc_exns   = false; rkc_module = false;
+          rkc_modtype = false; rkc_theory = false; } in
 
         `Selected (List.fold_left update init k)
 
@@ -275,6 +277,7 @@ let rename ((rk, (rex, itempl)) : renaming) (k, x) =
     | `Selected { rkc_lemmas  = true }, `Lemma   -> true
     | `Selected { rkc_ops     = true }, `Op      -> true
     | `Selected { rkc_preds   = true }, `Pred    -> true
+    | `Selected { rkc_exns    = true }, `Exn     -> true
     | `Selected { rkc_types   = true }, `Type    -> true
     | `Selected { rkc_module  = true }, `Module  -> true
     | `Selected { rkc_modtype = true }, `ModType -> true

src/ecThCloning.mli

@@ -102,6 +102,7 @@ and rk_categories = {
   rkc_lemmas  : bool;
   rkc_ops     : bool;
   rkc_preds   : bool;
+  rkc_exns    : bool;
   rkc_types   : bool;
   rkc_module  : bool;
   rkc_modtype : bool;

src/ecTheoryReplay.ml

@@ -364,7 +364,8 @@ let xnpath ove x =
     (EcPath.fromqsymbol (snd ove.ovre_prefix, x))
 
 (* -------------------------------------------------------------------- *)
-let string_of_renaming_kind = function
+let string_of_renaming_kind (rkind : theory_renaming_kind) =
+  match rkind with
   | `Lemma   -> "lemma"
   | `Op      -> "operator"
   | `Pred    -> "predicate"
@@ -388,7 +389,7 @@ let rename ove subst (kind, name) =
       match kind with
       | `Lemma | `Type ->
           EcIo.is_sym_ident newname
-      | `Op | `Pred ->
+      | `Op | `Pred | `Exn ->
           EcIo.is_op_ident newname
       | `Module | `ModType | `Theory ->
           EcIo.is_mod_ident newname
@@ -522,9 +523,14 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
   let scenv = ove.ovre_hooks.henv scope in
   let env   = EcSection.env scenv in
 
+  let rk =
+    match oopd.op_kind with
+    | OB_oper (Some (OP_Exn _)) -> `Exn
+    | _ -> `Op in
+
   match Msym.find_opt x ove.ovre_ovrd.evc_ops with
   | None ->
-      let (subst, x) = rename ove subst (`Op, x) in
+      let (subst, x) = rename ove subst (rk, x) in
       let oopd = EcSubst.subst_op subst oopd in
       (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import (Th_operator (x, oopd)))
 
@@ -598,7 +604,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
         in
           match opmode with
           | `Alias ->
-              let subst, x = rename ove subst (`Op, x) in
+              let subst, x = rename ove subst (rk, x) in
               (newop, subst, x, true)
 
           | `Inline _ ->