In clone, allow applying renamings pre-emptively

When cloning a theory and subtituting a sub-theory by
some other one, it is now possible to apply renamings
on the target sub-theory.

The syntax is:

```
clone T ... with theory T <- U { rename ... }
```

This allows to substitute one theory by some other
one that got some of its components renamed by a
previous clone.

For example:

```
abstract theory Word.
  op foo_XX = ...
end Word.

clone Word as W16 rename "_XX" as "_16".

abstract theory UseWord.
  clone Word as W.
end UseWord.

clone UseWord as UseWord16 with
  theory W <- W16 { rename "_XX" as "_16" }.
```

Author: strub

src/ecParser.mly

@@ -3640,8 +3640,8 @@ clone_override:
 | MODULE TYPE x=uqident mode=loc(opclmode) y=uqident
    { (x, PTHO_ModTyp (y, unloc mode)) }
 
-| THEORY x=uqident mode=loc(opclmode) y=uqident
-   { (x, PTHO_Theory (y, unloc mode)) }
+| THEORY x=uqident mode=loc(opclmode) y=uqident renames=brace(clone_rename)?
+   { (x, PTHO_Theory (y, unloc mode, odfl [] renames)) }
 
 realize:
 | REALIZE x=qident

src/ecParsetree.ml

@@ -1193,7 +1193,7 @@ and op_override = op_override_def genoverride * clmode
 and pr_override = pr_override_def genoverride * clmode
 and me_override = pqsymbol * clmode
 and mt_override = pqsymbol * clmode
-and th_override = pqsymbol * clmode
+and th_override = pqsymbol * clmode * theory_renaming list
 and ax_override = pqsymbol * clmode
 and nt_override = EcPath.path * clmode
 

src/ecThCloning.ml

@@ -219,6 +219,53 @@ and rk_categories = {
   rkc_theory  : bool;
 }
 
+(* -------------------------------------------------------------------- *)
+type octxt = {
+  oc_env : EcEnv.env;
+  oc_oth : ctheory;
+}
+
+(* -------------------------------------------------------------------- *)
+module Renaming : sig
+  val rename1 : octxt -> theory_renaming -> renaming
+end = struct
+  let rename1 oc (k, (r1, r2)) : renaming =
+    let e1 =
+      try  EcRegexp.regexp (unloc r1)
+      with EcRegexp.Error _ -> clone_error oc.oc_env (CE_InvalidRE (unloc r1)) in
+    let e2 =
+      try  EcRegexp.subst (unloc r2)
+      with EcRegexp.Error _ -> clone_error oc.oc_env (CE_InvalidRE (unloc r2)) in
+
+    Array.iter
+      (fun m ->
+        if EcRegexp.match_ (`S "^0+$") (oget m.(1)) then
+          clone_error oc.oc_env (CE_InvalidRE (unloc r2)))
+      (try  EcRegexp.extract (`S "\\$([0-9]+)") (unloc r2)
+       with Not_found -> [||]);
+
+    let k =
+      if List.is_empty k then `All else
+
+        let update rk = function
+          | `Lemma   -> { rk with rkc_lemmas  = true; }
+          | `Type    -> { rk with rkc_types   = true; }
+          | `Op      -> { rk with rkc_ops     = true; }
+          | `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
+
+        let init = {
+          rkc_lemmas  = false; rkc_types   = false; rkc_ops     = false;
+          rkc_preds   = false; rkc_module  = false; rkc_modtype = false;
+          rkc_theory  = false; } in
+
+        `Selected (List.fold_left update init k)
+
+    in (k, (e1, e2))
+end
+
 (* -------------------------------------------------------------------- *)
 let rename ((rk, (rex, itempl)) : renaming) (k, x) =
   let selected =
@@ -239,12 +286,6 @@ let rename ((rk, (rex, itempl)) : renaming) (k, x) =
 
   if x = newx then None else Some newx
 
-(* -------------------------------------------------------------------- *)
-type octxt = {
-  oc_env : EcEnv.env;
-  oc_oth : ctheory;
-}
-
 (* -------------------------------------------------------------------- *)
 module OVRD : sig
   type state = theory_cloning_proof list * evclone
@@ -373,7 +414,9 @@ end = struct
     in (proofs, evc)
 
   (* ------------------------------------------------------------------ *)
-  let th_ovrd oc ((proofs, evc) : state) name ((thd, mode) : th_override) =
+  let th_ovrd oc ((proofs, evc) : state) name ((thd, mode, prerenames) : th_override) =
+    let prerenames = List.map (Renaming.rename1 oc) prerenames in
+
     let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
 
     let loced x = mk_loc lc x in
@@ -406,42 +449,53 @@ end = struct
     let thd  = let thd = EcPath.toqsymbol sp in (fst thd @ [snd thd]) in
     let xdth = nm @ [x] in
 
+    let rename (kind, name) =
+      try
+        List.find_map (fun rnm -> rename rnm (kind, name)) prerenames
+      with Not_found -> name in
+
     assert (not (Msym.mem x evc.evc_ths));
 
     let evc = { evc with
       evc_ths = Msym.change (fun sub ->
         let sub, clear = odfl (evc_empty, false) sub in
         Some (sub, clear || (mode <> `Alias))) x evc.evc_ths } in
 
-    let rec doit_r prefix (proofs, evc) dth =
+    let rec doit_r (prefix, tgprefix) (proofs, evc) dth =
+      let dtpath (x : symbol) =
+        loced (xdth @ prefix, x) in
+
+      let tgpath ?kind (x : symbol) =
+        let x = Option.fold ~none:x ~some:(fun k -> rename (k, x)) kind in
+        EcPath.fromqsymbol (thd @ tgprefix, x) in
+
       match dth with
       | Th_type (x, _) ->
-         let ovrd = `ByPath (EcPath.fromqsymbol (thd @ prefix, x)) in
-         let ovrd = (ovrd, mode) in
-         ty_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
+         let ovrd = `ByPath (tgpath ~kind:`Type x), mode in
+         ty_ovrd oc (proofs, evc) (dtpath x) ovrd
 
       | Th_operator (x, ({ op_kind = OB_oper _ })) ->
-         let ovrd = `ByPath (EcPath.fromqsymbol (thd @ prefix, x)) in
-         let ovrd = (ovrd, mode) in
-         op_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
+         let ovrd = (`ByPath (tgpath ~kind:`Op x), mode) in
+         op_ovrd oc (proofs, evc) (dtpath x) ovrd
 
       | Th_operator (x, ({ op_kind = OB_pred _ })) ->
-         let ovrd = `ByPath (EcPath.fromqsymbol (thd @ prefix, x)) in
-         let ovrd = (ovrd, mode) in
-         pr_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
+         let ovrd = (`ByPath (tgpath ~kind:`Pred x), mode) in
+         pr_ovrd oc (proofs, evc) (dtpath x) ovrd
 
       | Th_operator (x, {op_kind=OB_nott _; _ }) ->
-         let ovrd = EcPath.fromqsymbol (thd @ prefix, x) in
-         let ovrd = (ovrd, mode) in
-         nt_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
+         let ovrd = (tgpath x, mode) in
+         nt_ovrd oc (proofs, evc) (dtpath x) ovrd
 
       | Th_axiom (x, _) ->
-        let axd = loced (thd @ prefix, x) in
-        let name = (loced (xdth @ prefix, x)) in
-        ax_ovrd oc (proofs, evc) name  (axd, mode)
+        let axd  = loced (EcPath.toqsymbol (tgpath ~kind:`Axiom x)) in
+        ax_ovrd oc (proofs, evc) (dtpath x) (axd, mode)
 
       | Th_theory (x, dth) when dth.cth_mode = `Concrete ->
-         List.fold_left (doit (prefix @ [x])) (proofs, evc) dth.cth_items
+        let tgx = rename (`Theory, x) in
+         List.fold_left
+          (doit (prefix @ [x], tgprefix @ [tgx]))
+          (proofs, evc)
+          dth.cth_items
 
       | Th_theory (_, _) ->
           (proofs, evc)
@@ -453,9 +507,9 @@ end = struct
          (proofs, evc)
 
       | Th_modtype (x, _) ->
-         modtype_ovrd
-           oc (proofs, evc) (loced (xdth @ prefix, x))
-           (loced (thd @ prefix, x), mode)
+        let ovrd = loced (EcPath.toqsymbol (tgpath ~kind:`ModType x)) in
+        modtype_ovrd
+          oc (proofs, evc) (dtpath x) (ovrd, mode)
 
       | Th_instance _   -> (proofs, evc)
 
@@ -468,7 +522,7 @@ end = struct
     and doit prefix (proofs, evc) dth =
       doit_r prefix (proofs, evc) dth.ti_item
 
-    in List.fold_left (doit []) (proofs, evc) dth.cth_items
+    in List.fold_left (doit ([], [])) (proofs, evc) dth.cth_items
 
   (* ------------------------------------------------------------------ *)
   let ovrd oc state name (ovrd : theory_override) =
@@ -492,47 +546,6 @@ end = struct
         th_ovrd oc state name thd
 end
 
-(* -------------------------------------------------------------------- *)
-module Renaming : sig
-  val rename1 : octxt -> theory_renaming -> renaming
-end = struct
-  let rename1 oc (k, (r1, r2)) : renaming =
-    let e1 =
-      try  EcRegexp.regexp (unloc r1)
-      with EcRegexp.Error _ -> clone_error oc.oc_env (CE_InvalidRE (unloc r1)) in
-    let e2 =
-      try  EcRegexp.subst (unloc r2)
-      with EcRegexp.Error _ -> clone_error oc.oc_env (CE_InvalidRE (unloc r2)) in
-
-    Array.iter
-      (fun m ->
-        if EcRegexp.match_ (`S "^0+$") (oget m.(1)) then
-          clone_error oc.oc_env (CE_InvalidRE (unloc r2)))
-      (try  EcRegexp.extract (`S "\\$([0-9]+)") (unloc r2)
-       with Not_found -> [||]);
-
-    let k =
-      if List.is_empty k then `All else
-
-        let update rk = function
-          | `Lemma   -> { rk with rkc_lemmas  = true; }
-          | `Type    -> { rk with rkc_types   = true; }
-          | `Op      -> { rk with rkc_ops     = true; }
-          | `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
-
-        let init = {
-          rkc_lemmas  = false; rkc_types   = false; rkc_ops     = false;
-          rkc_preds   = false; rkc_module  = false; rkc_modtype = false;
-          rkc_theory  = false; } in
-
-        `Selected (List.fold_left update init k)
-
-    in (k, (e1, e2))
-end
-
 (* -------------------------------------------------------------------- *)
 module Proofs : sig
   val proof : intheory:bool -> octxt -> evclone -> theory_cloning_proof -> evclone

src/ecTheoryReplay.ml

@@ -367,23 +367,14 @@ let string_of_renaming_kind = function
   | `Theory  -> "theory"
 
 (* -------------------------------------------------------------------- *)
-let rename ?(fold = true) ove subst (kind, name) =
+let rename ove subst (kind, name) =
   try
     let newname =
-      match fold with
-      | false ->
-        List.find_map
-          (fun rnm -> EcThCloning.rename rnm (kind, name))
-          ove.ovre_rnms
-      | _ ->
-        let newname =
-          List.fold_left (* FIXME:parallel substitution *)
-            (fun name rnm ->
-              Option.value ~default:name (EcThCloning.rename rnm (kind, name)))
+      List.fold_left (* FIXME:parallel substitution *)
+        (fun name rnm ->
+            Option.value ~default:name (EcThCloning.rename rnm (kind, name)))
             name ove.ovre_rnms in
-        if newname = name then raise Not_found;
-        newname
-    in
+    if newname = name then raise Not_found;
 
     let nameok =
       match kind with