Theory aliases

src/ecCommands.ml

@@ -557,6 +557,11 @@ and process_th_clone (scope : EcScope.scope) thcl =
   EcScope.Cloning.clone scope (Pragma.get ()).pm_check thcl
 
 (* -------------------------------------------------------------------- *)
+and process_th_alias (scope : EcScope.scope) (thcl : psymbol * pqsymbol) =
+  EcScope.check_state `InTop "theory alias" scope;
+  EcScope.Theory.alias scope thcl
+
+  (* -------------------------------------------------------------------- *)
 and process_mod_import (scope : EcScope.scope) mods =
   EcScope.check_state `InTop "module var import" scope;
   List.fold_left EcScope.Mod.import scope mods
@@ -730,6 +735,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
       | GthImport    name -> `Fct   (fun scope -> process_th_import  scope  name)
       | GthExport    name -> `Fct   (fun scope -> process_th_export  scope  name)
       | GthClone     thcl -> `Fct   (fun scope -> process_th_clone   scope  thcl)
+      | GthAlias     als  -> `Fct   (fun scope -> process_th_alias   scope  als)
       | GModImport   mods -> `Fct   (fun scope -> process_mod_import scope  mods)
       | GsctOpen     name -> `Fct   (fun scope -> process_sct_open   scope  name)
       | GsctClose    name -> `Fct   (fun scope -> process_sct_close  scope  name)

src/ecEnv.ml

@@ -632,9 +632,9 @@ module MC = struct
             (IPPath (root env))
             env.env_comps; }
 
-  let import up p obj env =
-    let name = ibasename p in
-      { env with env_current = up env.env_current name (p, obj) }
+  let import ?name up p obj env =
+    let name = odfl (ibasename p) name in
+    { env with env_current = up env.env_current name (p, obj) }
 
   (* -------------------------------------------------------------------- *)
   let lookup_var qnx env =
@@ -972,20 +972,20 @@ module MC = struct
     | None -> lookup_error (`QSymbol qnx)
     | Some (p, (args, obj)) -> (_downpath_for_th env p args, obj)
 
-  let import_theory p th env =
-    import (_up_theory true) (IPPath p) th env
+  let import_theory ?name p th env =
+    import ?name (_up_theory true) (IPPath p) th env
 
   (* -------------------------------------------------------------------- *)
-  let _up_mc candup mc p =
-    let name = ibasename p in
+  let _up_mc ?name candup mc p =
+    let name = odfl (ibasename p) name in
     if not candup && MMsym.last name mc.mc_components <> None then
       raise (DuplicatedBinding name);
     { mc with mc_components =
         MMsym.add name p mc.mc_components }
 
-  let import_mc p env =
-    let mc = _up_mc true env.env_current p in
-      { env with env_current = mc }
+  let import_mc ?name p env =
+    let mc = _up_mc ?name true env.env_current p in
+    { env with env_current = mc }
 
   (* ------------------------------------------------------------------ *)
   let rec mc_of_module_r (p1, args, p2, lc) me =
@@ -1105,6 +1105,10 @@ module MC = struct
       | Th_baserw (x, _) ->
           (add2mc _up_rwbase x (expath x) mc, None)
 
+      | Th_alias _ ->
+          (* FIXME:ALIAS *)
+          (mc, None)
+
       | Th_export _ | Th_addrw _ | Th_instance _
       | Th_auto   _ | Th_reduction _ ->
           (mc, None)
@@ -2852,6 +2856,20 @@ module Theory = struct
     else
       Option.get (Mp.find_opt p env.env_thenvs)
 
+
+  (* ------------------------------------------------------------------ *)
+  let rebind_alias (name : symbol) (path : path) (env : env) =
+    let th = by_path path env in
+    let env = MC.import_theory ~name path th env in
+    let env = MC.import_mc ~name (IPPath path) env in
+    env
+
+  (* ------------------------------------------------------------------ *)
+  let alias ?(import = import0) (name : symbol) (path : path) (env : env) =
+    let env =
+      if import.im_immediate then rebind_alias name path env else env in
+    { env with env_item = mkitem import (Th_alias (name, path)) :: env.env_item }
+
   (* ------------------------------------------------------------------ *)
   let rec bind_instance_th path inst cth =
     List.fold_left (bind_instance_th_item path) inst cth
@@ -3054,6 +3072,9 @@ module Theory = struct
         | Th_baserw (x, _) ->
             MC.import_rwbase (xpath x) env
 
+        | Th_alias (name, path) ->
+            rebind_alias name path env
+
         | Th_addrw _ | Th_instance _ | Th_auto _ | Th_reduction _ ->
             env
 

src/ecEnv.mli

@@ -293,6 +293,8 @@ module Theory : sig
     -> EcTypes.is_local
     -> EcTheory.thmode
     -> env -> compiled_theory option
+
+  val alias : ?import:import -> symbol -> path -> env -> env
 end
 
 (* -------------------------------------------------------------------- *)

src/ecParser.mly

@@ -3593,6 +3593,13 @@ realize:
 | REALIZE x=qident BY bracket(empty)
     {  { pr_name = x; pr_proof = Some None; } }
 
+
+(* -------------------------------------------------------------------- *)
+(* Theory aliasing                                                      *)
+
+theory_alias: (* FIXME: THEORY ALIAS -> S/R conflict *)
+| ALIAS THEORY name=uident EQ target=uqident { (name, target) }
+
 (* -------------------------------------------------------------------- *)
 (* Printing                                                             *)
 print:
@@ -3712,6 +3719,7 @@ global_action:
 | theory_export    { GthExport    $1 }
 | theory_clone     { GthClone     $1 }
 | theory_clear     { GthClear     $1 }
+| theory_alias     { GthAlias     $1 }
 | module_import    { GModImport   $1 }
 | section_open     { GsctOpen     $1 }
 | section_close    { GsctClose    $1 }

src/ecParsetree.ml

@@ -1255,6 +1255,7 @@ type global_action =
   | GthImport    of pqsymbol list
   | GthExport    of pqsymbol list
   | GthClone     of theory_cloning
+  | GthAlias     of (psymbol * pqsymbol)
   | GModImport   of pmsymbol located list
   | GsctOpen     of osymbol_r
   | GsctClose    of osymbol_r

src/ecPrinting.ml

@@ -3509,6 +3509,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
         lvl (odfl "" base)
         (pp_list "@ " (pp_axname ppe)) p
 
+  | EcTheory.Th_alias (name, target) ->
+      Format.fprintf fmt "alias theory %s = %a." name (pp_thname ppe) target
+
 (* -------------------------------------------------------------------- *)
 let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt =
   let ppnode = collect2_s ppe stmt.s_node [] in

src/ecScope.ml

@@ -2152,7 +2152,18 @@ module Theory = struct
               raise (ImportError (None, name.rqd_name, e))
         end
 
+  (* -------------------------------------------------------------------- *)
   let required scope = scope.sc_required
+
+  (* -------------------------------------------------------------------- *)
+  let alias (scope : scope) ?(import = EcTheory.import0) ((name, target) : psymbol * pqsymbol) =
+    let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in
+    let thpath, _ = ofdfl (fun () ->
+      hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target)
+    ) thpath in
+    let item = EcTheory.mkitem import (Th_alias (unloc name, thpath)) in
+
+    { scope with sc_env = EcSection.add_item item scope.sc_env }
 end
 
 (* -------------------------------------------------------------------- *)

src/ecScope.mli

@@ -174,6 +174,10 @@ module Theory : sig
   val add_clears : (pqsymbol option) list -> scope -> scope
 
   val required : scope -> required
+
+  (* [alias scope (name, thname)] create a theory alias [name] to
+   * [thname] *)
+  val alias : scope -> ?import:EcTheory.import -> psymbol * pqsymbol -> scope
 end
 
 (* -------------------------------------------------------------------- *)

src/ecSection.ml

@@ -1047,6 +1047,7 @@ let rec set_local_item item =
     | Th_addrw     (p,ps,lc) -> Th_addrw     (p, ps, set_local lc)
     | Th_reduction       r   -> Th_reduction r
     | Th_auto     (i,s,p,lc) -> Th_auto      (i, s, p, set_local lc)
+    | Th_alias         alias -> Th_alias     alias
 
   in { item with ti_item = lcitem }
 
@@ -1348,6 +1349,7 @@ let add_item_ (item : theory_item) (scenv:scenv) =
     | Th_baserw   (s,lc) -> EcEnv.BaseRw.add s lc env
     | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env
     | Th_auto (level, base, ps, lc) -> EcEnv.Auto.add ~level ?base ps lc env
+    | Th_alias     (n,p) -> EcEnv.Theory.alias n p env
     | Th_reduction r     -> EcEnv.Reduction.add r env
     | _                  -> assert false
   in
@@ -1376,6 +1378,7 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i
     | Th_addrw (p,ps,lc) -> generalize_addrw to_gen (p, ps, lc)
     | Th_reduction rl    -> generalize_reduction to_gen rl
     | Th_auto hints      -> generalize_auto to_gen hints
+    | Th_alias _         -> (to_gen, None) (* FIXME:ALIAS *)
 
   in
 
@@ -1498,6 +1501,7 @@ let check_item scenv item =
       hierror "local hint can only be declared inside section";
   | Th_reduction _ -> ()
   | Th_theory  _   -> assert false
+  | Th_alias _     -> () (* FIXME:ALIAS *)
 
 let rec add_item (item : theory_item) (scenv : scenv) =
   let item = if scenv.sc_loca = `Local then set_local_item item else item in

src/ecSubst.ml

@@ -1078,6 +1078,9 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
   | Th_auto (lvl, base, ps, lc) ->
       Th_auto (lvl, base, List.map (subst_path s) ps, lc)
 
+  | Th_alias (name, target) ->
+      Th_alias (name, subst_path s target)
+
 (* -------------------------------------------------------------------- *)
 and subst_theory (s : subst) (items : theory) =
   List.map (subst_theory_item s) items

src/ecThCloning.ml

@@ -441,6 +441,7 @@ end = struct
       | Th_addrw  _     -> (proofs, evc)
       | Th_reduction _  -> (proofs, evc)
       | Th_auto _       -> (proofs, evc)
+      | Th_alias _      -> (proofs, evc)
 
     and doit prefix (proofs, evc) dth =
       doit_r prefix (proofs, evc) dth.ti_item

src/ecTheory.ml

@@ -38,6 +38,7 @@ and theory_item_r =
   | Th_addrw     of EcPath.path * EcPath.path list * is_local
   | Th_reduction of (EcPath.path * rule_option * rule option) list
   | Th_auto      of (int * symbol option * path list * is_local)
+  | Th_alias     of (symbol * path) (* FIXME: currently, only theories *)
 
 and thsource = {
   ths_base : EcPath.path;

src/ecTheory.mli

@@ -35,6 +35,7 @@ and theory_item_r =
   (* reduction rule does not survive to section so no locality *)
   | Th_reduction of (EcPath.path * rule_option * rule option) list
   | Th_auto      of (int * symbol option * path list * is_local)
+  | Th_alias     of (symbol * path)
 
 and thsource = {
   ths_base : EcPath.path;

src/ecTheoryReplay.ml

@@ -945,6 +945,20 @@ and replay_instance
   with E.InvInstPath ->
     (subst, ops, proofs, scope)
 
+(* -------------------------------------------------------------------- *)
+and replay_alias
+  (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, target)
+=
+  let scenv = ove.ovre_hooks.henv scope in
+  let env = EcSection.env scenv in
+  let p = EcSubst.subst_path subst target in
+
+  if is_none (EcEnv.Theory.by_path_opt p env) then
+    (subst, ops, proofs, scope)
+  else
+    let scope = ove.ovre_hooks.hadd_item scope import (Th_alias (name, target)) in
+    (subst, ops, proofs, scope)
+
 (* -------------------------------------------------------------------- *)
 and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
   match item.ti_item with
@@ -990,6 +1004,9 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
   | Th_instance ((typ, ty), tc, lc) ->
      replay_instance ove (subst, ops, proofs, scope) (item.ti_import, (typ, ty), tc, lc)
 
+  | Th_alias (name, target) ->
+     replay_alias ove (subst, ops, proofs, scope) (item.ti_import, name, target)
+
   | Th_theory (ox, cth) -> begin
       let thmode = cth.cth_mode in
       let (subst, x) = rename ove subst (`Theory, ox) in

tests/theory-alias.ec

@@ -0,0 +1,11 @@
+theory T.
+  theory V.
+    op foo : int.
+  end V.
+
+  alias theory U = V.
+end T.
+
+import T.
+
+op bar : int = U.foo.