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

@@ -291,7 +291,7 @@ module HiPrinting = struct
     let ppe = EcPrinting.PPEnv.ofenv env in
 
     let pp_path =
-      EcPrinting.pp_shorten_path
+      EcPrinting.pp_shorten_path ppe
         (fun (p : EcPath.path) (q : EcSymbols.qsymbol) ->
           Option.equal EcPath.p_equal
             (Some p)
@@ -587,6 +587,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
@@ -760,6 +765,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
@@ -63,9 +63,9 @@ module type PrinterAPI = sig
   val pp_path     : path pp
 
   (* ------------------------------------------------------------------ *)
-  val shorten_path : (path -> qsymbol -> bool) -> path -> qsymbol * qsymbol option
+  val shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path -> qsymbol * qsymbol option
 
-  val pp_shorten_path : (path -> qsymbol -> bool) -> path pp
+  val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp
 
   (* ------------------------------------------------------------------ *)
   val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp

src/ecEnv.ml

@@ -184,6 +184,7 @@ type preenv = {
   env_atbase   : atbase 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;
@@ -312,6 +313,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;
@@ -636,9 +638,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 =
@@ -976,20 +978,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 =
@@ -1109,6 +1111,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)
@@ -2886,6 +2892,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
@@ -3088,6 +3113,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                                                             *)
 phint:
@@ -3757,6 +3764,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

@@ -1276,6 +1276,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,25 @@ module PPEnv = struct
             (fun env x -> EcEnv.Mod.bind_param x mty env)
             ppe.ppe_env xs; }
 
-  let p_shorten cond (nm, x) =
+  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    : qsymbol)
+    : qsymbol
+  =
     let rec shorten prefix (nm, x) =
       match cond (nm, x) with
       | true  -> (nm, x)
@@ -154,35 +172,46 @@ module PPEnv = struct
       end
     in
 
+    let p = EcPath.fromqsymbol p 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) = EcPath.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.toqsymbol p)
+      p_shorten ppe exists (P.toqsymbol 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.toqsymbol p)
+      p_shorten ppe exists (P.toqsymbol 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.toqsymbol p)
+      p_shorten ppe exists (P.toqsymbol 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.toqsymbol p)
+      p_shorten ppe exists (P.toqsymbol p)
 
   let op_symb (ppe : t) p info =
     let specs = [1, EcPath.pqoname (EcPath.prefix EcCoreLib.CI_Bool.p_eq) "<>"] in
@@ -220,21 +249,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.toqsymbol p)
+      else p_shorten ppe exists (P.toqsymbol 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.toqsymbol p)
+      p_shorten ppe exists (P.toqsymbol 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.toqsymbol p)
+      p_shorten ?alias ~istheory:true ppe exists (P.toqsymbol p)
 
   let rec mod_symb (ppe : t) mp : EcSymbols.msymbol =
     let (nm, x, p2) =
@@ -360,13 +389,18 @@ module PPEnv = struct
 end
 
 (* -------------------------------------------------------------------- *)
-let shorten_path (cond : P.path -> qsymbol -> bool) (p : P.path) : qsymbol * qsymbol option =
+let shorten_path
+  (ppe  : PPEnv.t)
+  (cond : P.path -> qsymbol -> bool)
+  (p    : P.path)
+  : qsymbol * qsymbol option
+=
   let (nm, x) = EcPath.toqsymbol p in
   let nm =
     match nm with
     | top :: nm when top = EcCoreLib.i_top -> nm
     | _ -> nm in
-  let nm', x' = PPEnv.p_shorten (cond p) (nm, x) in
+  let nm', x' = PPEnv.p_shorten ppe (cond p) (nm, x) in
   let plong, pshort = (nm, x), (nm', x') in
 
   (plong, if plong = pshort then None else Some pshort)
@@ -445,8 +479,13 @@ let pp_path fmt p =
   Format.fprintf fmt "%s" (P.tostring p)
 
 (* -------------------------------------------------------------------- *)
-let pp_shorten_path (cond : P.path -> qsymbol -> bool) (fmt : Format.formatter) (p : P.path) =
-  let plong, pshort  = shorten_path cond p in
+let pp_shorten_path
+  (ppe  : PPEnv.t)
+  (cond : P.path -> qsymbol -> bool)
+  (fmt  : Format.formatter)
+  (p    : P.path)
+=
+  let plong, pshort = shorten_path ppe cond p in
 
   match pshort with
   | None ->
@@ -507,8 +546,8 @@ let pp_axhnt ppe fmt (p, b) =
   Format.fprintf fmt "%a%s" (pp_axname ppe) p b
 
 (* -------------------------------------------------------------------- *)
-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 =
@@ -3547,6 +3586,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
         level (odfl "" base)
         (pp_list "@ " (pp_axhnt ppe)) axioms
 
+  | 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