From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/mod_subst.mli | 101 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 72 insertions(+), 29 deletions(-) (limited to 'kernel/mod_subst.mli') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index a2e45c52..a948d164 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -6,35 +6,83 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_subst.mli 10849 2008-04-25 15:55:16Z soubiran $ i*) +(*i $Id$ i*) (*s [Mod_subst] *) open Names open Term -type resolver +(* A delta_resolver maps name (constant, inductive, module_path) + to canonical name *) +type delta_resolver + type substitution -val make_resolver : (constant * constr option) list -> resolver +val empty_delta_resolver : delta_resolver + +val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver + +val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver + -> delta_resolver + +val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver + +val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver + +val add_mp_delta_resolver : module_path -> module_path -> delta_resolver + -> delta_resolver + +val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver + +(* Apply the substitution on the domain of the resolver *) +val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver + +(* Apply the substitution on the codomain of the resolver *) +val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver + +val subst_dom_codom_delta_resolver : + substitution -> delta_resolver -> delta_resolver + +(* *_of_delta return the associated name of arg2 in arg1 *) +val constant_of_delta : delta_resolver -> constant -> constant + +val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive + +val delta_of_mp : delta_resolver -> module_path -> module_path + +(* Extract the set of inlined constant in the resolver *) +val inline_of_delta : delta_resolver -> kernel_name list + +(* remove_mp is used for the computation of a resolver induced by Include P *) +val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver + + +(* mem tests *) +val mp_in_delta : module_path -> delta_resolver -> bool + +val con_in_delta : constant -> delta_resolver -> bool + +val mind_in_delta : mutual_inductive -> delta_resolver -> bool + +(*substitution*) val empty_subst : substitution -val add_msid : - mod_self_id -> module_path -> substitution -> substitution -val add_mbid : - mod_bound_id -> module_path -> resolver option -> substitution -> substitution +(* add_* add [arg2/arg1]{arg3} to the substitution with no + sequential composition *) +val add_mbid : + mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution val add_mp : - module_path -> module_path -> substitution -> substitution + module_path -> module_path -> delta_resolver -> substitution -> substitution -val map_msid : - mod_self_id -> module_path -> substitution +(* map_* create a new substitution [arg2/arg1]{arg3} *) val map_mbid : - mod_bound_id -> module_path -> resolver option -> substitution + mod_bound_id -> module_path -> delta_resolver -> substitution val map_mp : - module_path -> module_path -> substitution + module_path -> module_path -> delta_resolver -> substitution -(* sequential composition: +(* sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] *) val join : substitution -> substitution -> substitution @@ -47,16 +95,21 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted (*i debugging *) val debug_string_of_subst : substitution -> string val debug_pr_subst : substitution -> Pp.std_ppcmds +val debug_string_of_delta : delta_resolver -> string +val debug_pr_delta : delta_resolver -> Pp.std_ppcmds (*i*) (* [subst_mp sub mp] guarantees that whenever the result of the - substitution is structutally equal [mp], it is equal by pointers - as well [==] *) + substitution is structutally equal [mp], it is equal by pointers + as well [==] *) -val subst_mp : +val subst_mp : substitution -> module_path -> module_path -val subst_kn : +val subst_ind : + substitution -> mutual_inductive -> mutual_inductive + +val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : @@ -71,24 +124,14 @@ val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference (* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) -val replace_mp_in_con : module_path -> module_path -> constant -> constant +val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name (* [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) val subst_mps : substitution -> constr -> constr -(* [occur_*id id sub] returns true iff [id] occurs in [sub] +(* [occur_*id id sub] returns true iff [id] occurs in [sub] on either side *) -val occur_msid : mod_self_id -> substitution -> bool val occur_mbid : mod_bound_id -> substitution -> bool -val update_subst_alias : substitution -> substitution -> substitution - -val update_subst : substitution -> substitution -> substitution - -val subst_key : substitution -> substitution -> substitution - -val join_alias : substitution -> substitution -> substitution - -val remove_alias : substitution -> substitution -- cgit v1.2.3