diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 95 |
1 files changed, 49 insertions, 46 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 9b48b3ea..21b6bf93 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,105 +1,108 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_subst.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*s [Mod_subst] *) +(** {6 [Mod_subst] } *) open Names open Term -(* A delta_resolver maps name (constant, inductive, module_path) +(** {6 Delta resolver} *) + +(** A delta_resolver maps name (constant, inductive, module_path) to canonical name *) type delta_resolver -type substitution - val empty_delta_resolver : delta_resolver -val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver +val add_mp_delta_resolver : + module_path -> module_path -> delta_resolver -> delta_resolver -val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver - -> delta_resolver +val add_kn_delta_resolver : + kernel_name -> kernel_name -> 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_inline_delta_resolver : + kernel_name -> (int * constr option) -> 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 +(** Effect of a [delta_resolver] on kernel name, constant, inductive, etc *) -(* 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 kn_of_delta : delta_resolver -> kernel_name -> kernel_name +val constant_of_delta_kn : delta_resolver -> kernel_name -> constant val constant_of_delta : delta_resolver -> constant -> constant +val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive -val delta_of_mp : delta_resolver -> module_path -> module_path +val mp_of_delta : delta_resolver -> module_path -> module_path -(* Extract the set of inlined constant in the resolver *) -val inline_of_delta : delta_resolver -> kernel_name list +(** Extract the set of inlined constant in the resolver *) +val inline_of_delta : int option -> delta_resolver -> (int * 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 +(** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *) - -(* 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*) + +(** {6 Substitution} *) + +type substitution val empty_subst : substitution -(* add_* add [arg2/arg1]{arg3} to the substitution with no +val is_empty_subst : substitution -> bool + +(** 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 -> delta_resolver -> substitution -> substitution -(* map_* create a new substitution [arg2/arg1]{arg3} *) +(** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : mod_bound_id -> module_path -> delta_resolver -> substitution val map_mp : 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 + +(** 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 + + type 'a substituted val from_val : 'a -> 'a substituted val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a val subst_substituted : substitution -> 'a substituted -> 'a substituted -(*i debugging *) +(**/**) +(* 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 +(** [subst_mp sub mp] guarantees that whenever the result of the substitution is structutally equal [mp], it is equal by pointers as well [==] *) @@ -109,13 +112,13 @@ val subst_mp : val subst_ind : substitution -> mutual_inductive -> mutual_inductive -val subst_kn : +val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : substitution -> constant -> constant * constr -(* Here the semantics is completely unclear. +(** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" where X.t is later on instantiated with y? I choose the first @@ -123,14 +126,14 @@ val subst_con : val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference -(* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) +(** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name -(* [subst_mps sub c] performs the substitution [sub] on all kernel +(** [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_mbid : mod_bound_id -> substitution -> bool |