diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /kernel/mod_subst.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r-- | kernel/mod_subst.ml | 62 |
1 files changed, 32 insertions, 30 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 95990bea..b3d06ce7 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Claudio Sacerdoti from contents of term.ml, names.ml and @@ -16,20 +18,20 @@ open Pp open Util open Names -open Term +open Constr (* For Inline, the int is an inlining level, and the constr (if present) is the term into which we should inline. *) type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -(* NB: earlier constructor Prefix_equiv of module_path +(* NB: earlier constructor Prefix_equiv of ModPath.t is now stored in a separate table, see Deltamap.t below *) module Deltamap = struct - type t = module_path MPmap.t * delta_hint KNmap.t + type t = ModPath.t MPmap.t * delta_hint KNmap.t let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -45,7 +47,7 @@ module Deltamap = struct end (* Invariant: in the [delta_hint] map, an [Equiv] should only - relate [kernel_name] with the same label (and section dirpath). *) + relate [KerName.t] with the same label (and section dirpath). *) type delta_resolver = Deltamap.t @@ -65,7 +67,7 @@ module Umap = struct let join map1 map2 = fold add_mp add_mbi map1 map2 end -type substitution = (module_path * delta_resolver) Umap.t +type substitution = (ModPath.t * delta_resolver) Umap.t let empty_subst = Umap.empty @@ -76,21 +78,21 @@ let is_empty_subst = Umap.is_empty let string_of_hint = function | Inline (_,Some _) -> "inline(Some _)" | Inline _ -> "inline()" - | Equiv kn -> string_of_kn kn + | Equiv kn -> KerName.to_string kn let debug_string_of_delta resolve = let kn_to_string kn hint l = - (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l + (KerName.to_string kn ^ "=>" ^ string_of_hint hint) :: l in let mp_to_string mp mp' l = - (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l + (ModPath.to_string mp ^ "=>" ^ ModPath.to_string mp') :: l in let l = Deltamap.fold mp_to_string kn_to_string resolve [] in String.concat ", " (List.rev l) let list_contents sub = - let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in - let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in + let one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in + let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in Umap.fold mp_one_pair mbi_one_pair sub [] @@ -117,7 +119,7 @@ let debug_pr_subst sub = let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc)) let add_kn_delta_resolver kn kn' = - assert (Label.equal (label kn) (label kn')); + assert (Label.equal (KerName.label kn) (KerName.label kn')); Deltamap.add_kn kn (Equiv kn') let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 @@ -165,12 +167,12 @@ let solve_delta_kn resolve kn = | Inline (lev, Some c) -> raise (Change_equiv_to_inline (lev,c)) | Inline (_, None) -> raise Not_found with Not_found -> - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - make_kn new_mp dir l + KerName.make new_mp dir l let kn_of_delta resolve kn = try solve_delta_kn resolve kn @@ -242,18 +244,18 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (make_kn mp' dir l) + solve_delta_kn resolve (KerName.make mp' dir l) | None -> kn let subst_kn sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - (make_kn mp' dir l) + (KerName.make mp' dir l) | None -> kn exception No_subst @@ -300,7 +302,7 @@ let subst_con0 sub (cst,u) = match search_delta_inline resolve knu knc with | Some t -> (* In case of inlining, discard the canonical part (cf #2608) *) - Constant.make1 knu, t + Constant.make1 knu, Vars.subst_instance_constr u t | None -> let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc @@ -340,7 +342,7 @@ let subst_evaluable_reference subst = function let rec map_kn f f' c = let func = map_kn f f' in - match kind_of_term c with + match kind c with | Const kn -> (try snd (f' kn) with No_subst -> c) | Proj (p,t) -> let p' = @@ -419,7 +421,7 @@ let subst_mps sub c = let rec replace_mp_in_mp mpfrom mpto mp = match mp with - | _ when mp_eq mp mpfrom -> mpto + | _ when ModPath.equal mp mpfrom -> mpto | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1 == mp1' then mp @@ -427,14 +429,14 @@ let rec replace_mp_in_mp mpfrom mpto mp = | _ -> mp let replace_mp_in_kn mpfrom mpto kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn - else make_kn mp'' dir l + else KerName.make mp'' dir l let rec mp_in_mp mp mp1 = match mp1 with - | _ when mp_eq mp1 mp -> true + | _ when ModPath.equal mp1 mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false @@ -446,7 +448,7 @@ let subset_prefixed_by mp resolver = match hint with | Inline _ -> rslv | Equiv _ -> - if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv in Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver @@ -515,7 +517,7 @@ let add_delta_resolver resolver1 resolver2 = let substition_prefixed_by k mp subst = let mp_prefixmp kmp (mp_to,reso) sub = - if mp_in_mp mp kmp && not (mp_eq mp kmp) then + if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key (mp_to,reso) sub else sub |