From 75d8070b9600a341b90be3a0cace1f254d9915f4 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 | 8 ++++- src/ecCorePrinting.ml | 6 ++-- src/ecEnv.ml | 48 ++++++++++++++++++++------ src/ecEnv.mli | 3 ++ src/ecParser.mly | 10 +++++- src/ecParsetree.ml | 1 + src/ecPrinting.ml | 80 +++++++++++++++++++++++++++++++++---------- src/ecScope.ml | 15 +++++++- 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, 180 insertions(+), 35 deletions(-) create mode 100644 tests/theory-alias.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 8114cbac50..d03cff5f32 100644 --- a/src/ecCommands.ml +++ b/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) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index e98eb84534..e18ace4a67 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 @@ -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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a83045d38d..b6ba72edac 100644 --- a/src/ecEnv.ml +++ b/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 diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 0ed659eb22..4743bc9d04 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 b612e28d57..1ae0978646 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 *) 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 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index a93ada6c8f..1c30838d89 100644 --- a/src/ecParsetree.ml +++ b/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 diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 593a5abfca..2bf1014545 100644 --- a/src/ecPrinting.ml +++ b/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 diff --git a/src/ecScope.ml b/src/ecScope.ml index ac291529da..57095d3fa5 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2156,7 +2156,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 (* -------------------------------------------------------------------- *) @@ -2367,12 +2378,14 @@ module Search = struct notify scope `Info "%s" (Buffer.contents buffer) let locate (scope : scope) ({ pl_desc = name } : pqsymbol) = + let ppe = EcPrinting.PPEnv.ofenv (env scope) in + let shorten lk p = let lk (p : path) (qs : qsymbol) = match lk qs (env scope) with | Some (p', _) -> p_equal p p' | _ -> false in - EcPrinting.shorten_path lk p + EcPrinting.shorten_path ppe lk p in let buffer = Buffer.create 0 in 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 3c8257547c..aa1fbc3184 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1051,6 +1051,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 auto_rl -> Th_auto {auto_rl with locality=set_local auto_rl.locality} + | Th_alias alias -> Th_alias alias in { item with ti_item = lcitem } @@ -1353,6 +1354,7 @@ let add_item_ (item : theory_item) (scenv:scenv) = | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env | Th_auto auto -> EcEnv.Auto.add ~level:auto.level ?base:auto.base auto.axioms auto.locality env + | Th_alias (n,p) -> EcEnv.Theory.alias n p env | Th_reduction r -> EcEnv.Reduction.add r env | _ -> assert false in @@ -1381,6 +1383,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 @@ -1503,6 +1506,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 d1b24f4f6f..01b48a76a8 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1079,6 +1079,9 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = Th_auto { auto_rl with axioms = List.map (fst_map (subst_path s)) axioms } + | 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 a329d9318d..55b7f96a71 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 auto_rule + | 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 fb63e85447..8c81af8e32 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 auto_rule + | Th_alias of (symbol * path) and thsource = { ths_base : EcPath.path; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 0b122511bf..76df291e00 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.