New vernacular command: theory aliases

Syntax this: `theory T = Path.To.Theort`

Theory aliases allow giving alternate names to theories - mainly
for readability issues. They are purely syntactic sugar and are
fully resolved (desugared) during typing.

The pretty-printer uses them when printing path, using a
longest-then-lastly-introduced strategy.

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/ecCorePrinting.ml

@@ -54,7 +54,7 @@ module type PrinterAPI = sig
   val pp_tyname  : PPEnv.t -> path pp
   val pp_axname  : PPEnv.t -> path pp
   val pp_tcname  : PPEnv.t -> path pp
-  val pp_thname  : PPEnv.t -> path pp
+  val pp_thname  : ?alias:bool -> PPEnv.t -> path pp
 
   val pp_mem      : PPEnv.t -> EcIdent.t pp
   val pp_memtype  : PPEnv.t -> EcMemory.memtype pp

src/ecEnv.ml

@@ -184,6 +184,7 @@ type preenv = {
   env_atbase   : (path list Mint.t) Msym.t;
   env_redbase  : mredinfo;
   env_ntbase   : ntbase Mop.t;
+  env_albase   : path Mp.t;             (* theory aliases   *)
   env_modlcs   : Sid.t;                 (* declared modules *)
   env_item     : theory_item list;      (* in reverse order *)
   env_norm     : env_norm ref;
@@ -308,6 +309,7 @@ let empty gstate =
     env_atbase   = Msym.empty;
     env_redbase  = Mrd.empty;
     env_ntbase   = Mop.empty;
+    env_albase   = Mp.empty;
     env_modlcs   = Sid.empty;
     env_item     = [];
     env_norm     = ref empty_norm_cache;
@@ -632,9 +634,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 +974,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 +1107,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 +2858,25 @@ 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 src = EcPath.pqname (root env) name in
+    let env = MC.import_theory ~name path th env in
+    let env = MC.import_mc ~name (IPPath path) env in
+    let env = { env with env_albase = Mp.add path src env.env_albase } 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 aliases (env : env) =
+    env.env_albase
+
   (* ------------------------------------------------------------------ *)
   let rec bind_instance_th path inst cth =
     List.fold_left (bind_instance_th_item path) inst cth
@@ -3054,6 +3079,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,9 @@ module Theory : sig
     -> EcTypes.is_local
     -> EcTheory.thmode
     -> env -> compiled_theory option
+
+  val alias : ?import:import -> symbol -> path -> env -> env
+  val aliases : env -> path Mp.t
 end
 
 (* -------------------------------------------------------------------- *)

src/ecParser.mly

@@ -1964,7 +1964,7 @@ theory_clear_items:
 | xs=theory_clear_item1* { xs }
 
 theory_open:
-| loca=is_local b=boption(ABSTRACT) THEORY x=uident
+| loca=is_local b=iboption(ABSTRACT) THEORY x=uident
     { (loca, b, x) }
 
 theory_close:
@@ -3620,6 +3620,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 *)
+| THEORY name=uident EQ target=uqident { (name, target) }
+
 (* -------------------------------------------------------------------- *)
 (* Printing                                                             *)
 print:
@@ -3739,6 +3746,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

@@ -1271,6 +1271,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

@@ -143,7 +143,18 @@ module PPEnv = struct
             (fun env x -> EcEnv.Mod.bind_param x mty env)
             ppe.ppe_env xs; }
 
-  let p_shorten cond p =
+  let reverse_theory_alias (ppe : t) (path : P.path) : P.path =
+    let aliases = EcEnv.Theory.aliases ppe.ppe_env in
+
+    let rec reverse (suffix : symbol list) (p : P.path option) =
+      Option.bind p (fun prefix ->
+        match P.Mp.find_opt prefix aliases with
+        | None -> reverse (P.basename prefix :: suffix) (P.prefix prefix)
+        | Some prefix -> Some (EcPath.extend prefix suffix)
+      )
+    in Option.value ~default:path (reverse [] (Some path))
+
+  let p_shorten ?(alias = true) ?(istheory = false) (ppe : t) (cond : qsymbol -> bool) (p : P.path) =
     let rec shorten prefix (nm, x) =
       match cond (nm, x) with
       | true  -> (nm, x)
@@ -154,36 +165,45 @@ module PPEnv = struct
       end
     in
 
+    let p =
+      if alias then begin
+        if istheory then
+          reverse_theory_alias ppe p
+        else
+          let thpath, base = P.prefix p, P.basename p in
+          let thpath = Option.map (reverse_theory_alias ppe) thpath in
+          P.pqoname thpath base
+      end else p in
     let (nm, x) = P.toqsymbol p in
     shorten (List.rev nm) ([], x)
 
   let ty_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.Ty.lookup_path ~unique:true sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let tc_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.TypeClass.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let rw_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.BaseRw.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let ax_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let op_symb (ppe : t) p info =
     let specs = [1, EcPath.pqoname (EcPath.prefix EcCoreLib.CI_Bool.p_eq) "<>"] in
@@ -221,21 +241,21 @@ module PPEnv = struct
       (* FIXME: for special operators, do check `info` *)
       if   List.exists (fun (_, sp) -> EcPath.p_equal sp p) specs
       then ([], EcPath.basename p)
-      else p_shorten exists p
+      else p_shorten ppe exists p
 
   let ax_symb (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
-  let th_symb (ppe : t) p =
+  let th_symb ?alias (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Theory.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ?alias ~istheory:true ppe exists p
 
   let rec mod_symb (ppe : t) mp : EcSymbols.msymbol =
     let (nm, x, p2) =
@@ -477,8 +497,8 @@ let pp_axname ppe fmt p =
   Format.fprintf fmt "%a" EcSymbols.pp_qsymbol (PPEnv.ax_symb ppe p)
 
 (* -------------------------------------------------------------------- *)
-let pp_thname ppe fmt p =
-  EcSymbols.pp_qsymbol fmt (PPEnv.th_symb ppe p)
+let pp_thname ?alias ppe fmt p =
+  EcSymbols.pp_qsymbol fmt (PPEnv.th_symb ?alias ppe p)
 
 (* -------------------------------------------------------------------- *)
 let pp_funname (ppe : PPEnv.t) fmt p =
@@ -3509,6 +3529,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 "theory %s = %a." name (pp_thname ~alias:false 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;