diff options
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 131 |
1 files changed, 48 insertions, 83 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d5..0f588a63 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,14 +1,17 @@ (************************************************************************) -(* 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) *) (************************************************************************) open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -26,7 +29,7 @@ let closedn n c = in try closed_rec n c; true with LocalOccur -> false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 c = closedn 0 c @@ -132,8 +135,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -160,25 +163,35 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst - | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match") + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l let adjust_subst_to_rel_context sign l = List.rev (subst_of_rel_context_instance sign l) +let adjust_rel_to_rel_context sign n = + let rec aux sign = + let open RelDecl in + match sign with + | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) + | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | [] -> (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function @@ -224,49 +237,6 @@ let subst_vars subst c = substn_vars 1 subst c (** Universe substitutions *) open Constr -let subst_univs_fn_puniverses fn = - let f = Univ.Instance.subst_fn fn in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - -let subst_univs_fn_constr f c = - let changed = ref false in - let fu = Univ.subst_univs_universe f in - let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in - let rec aux t = - match kind t with - | Sort (Sorts.Type u) -> - let u' = fu u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) - | Const (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstU (c, u')) - | Ind (i, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkIndU (i, u')) - | Construct (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstructU (c, u')) - | _ -> map aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_constr subst c = - if Univ.is_empty_subst subst then c - else - let f = Univ.make_subst subst in - subst_univs_fn_constr f c - -let subst_univs_constr = - if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr - else subst_univs_constr - let subst_univs_level_constr subst c = if Univ.is_empty_level_subst subst then c else @@ -308,42 +278,37 @@ let subst_instance_constr subst c = if Univ.Instance.is_empty subst then c else let f u = Univ.subst_instance_instance subst u in - let changed = ref false in - let rec aux t = + let rec aux t = match kind t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkConstU (c, u')) + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstU (c, u')) | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkIndU (i, u')) + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkIndU (i, u')) | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkConstructU (c, u')) - | Sort (Sorts.Type u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstructU (c, u')) + | Sort (Sorts.Type u) -> let u' = Univ.subst_instance_universe subst u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) + if u' == u then t else + (mkSort (Sorts.sort_of_univ u')) | _ -> Constr.map aux t in - let c' = aux c in - if !changed then c' else c + aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx - -type id_key = constant tableKey -let eq_id_key x y = Names.eq_table_key Constant.equal x y |