From 9e0ae009b02c100b65a22e148829903f7a9a93e7 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 14 Jan 2025 23:46:35 +0100 Subject: [PATCH] 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 | 6 +++++ src/ecCorePrinting.ml | 2 +- src/ecEnv.ml | 48 +++++++++++++++++++++++++++++++-------- src/ecEnv.mli | 3 +++ src/ecParser.mly | 10 +++++++- src/ecParsetree.ml | 1 + src/ecPrinting.ml | 53 +++++++++++++++++++++++++++++++------------ src/ecScope.ml | 11 +++++++++ src/ecScope.mli | 4 ++++ src/ecSection.ml | 4 ++++ src/ecSubst.ml | 3 +++ src/ecThCloning.ml | 1 + src/ecTheory.ml | 1 + src/ecTheory.mli | 1 + src/ecTheoryReplay.ml | 17 ++++++++++++++ tests/theory-alias.ec | 13 +++++++++++ 16 files changed, 151 insertions(+), 27 deletions(-) create mode 100644 tests/theory-alias.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 6b0e8f4fad..c500bb2f1c 100644 --- a/src/ecCommands.ml +++ b/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) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index a8187a70e0..437e950618 100644 --- a/src/ecCorePrinting.ml +++ b/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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 0bf97288d7..ba9a04daa5 100644 --- a/src/ecEnv.ml +++ b/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 diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 95ae7910c1..0d25b330f4 100644 --- a/src/ecEnv.mli +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 9f72e6abff..8ef74324e6 100644 --- a/src/ecParser.mly +++ b/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 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 67eba5e110..6e414cd394 100644 --- a/src/ecParsetree.ml +++ b/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 diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index afec71e62f..90616ba055 100644 --- a/src/ecPrinting.ml +++ b/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 diff --git a/src/ecScope.ml b/src/ecScope.ml index 8f5e4adfa9..8564af8aae 100644 --- a/src/ecScope.ml +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecScope.mli b/src/ecScope.mli index f04f9595aa..661e60958f 100644 --- a/src/ecScope.mli +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecSection.ml b/src/ecSection.ml index 127040f6b1..ac475889c9 100644 --- a/src/ecSection.ml +++ b/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 diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 977f7e3657..a3b3473852 100644 --- a/src/ecSubst.ml +++ b/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 diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 5ed2df1d2c..2244653eb8 100644 --- a/src/ecThCloning.ml +++ b/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 diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 0d39c8d21d..5cff16990b 100644 --- a/src/ecTheory.ml +++ b/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; diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 472928561f..2c0428262f 100644 --- a/src/ecTheory.mli +++ b/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; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 227aaee341..20cd34baa7 100644 --- a/src/ecTheoryReplay.ml +++ b/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 diff --git a/tests/theory-alias.ec b/tests/theory-alias.ec new file mode 100644 index 0000000000..6caeaf4485 --- /dev/null +++ b/tests/theory-alias.ec @@ -0,0 +1,13 @@ +theory T. + theory V. + op foo : int. + end V. + + theory U = V. +end T. + +import T. + +op bar : int = U.foo. + +print T.