diff options
| -rw-r--r-- | engine/evarutil.ml | 30 | ||||
| -rw-r--r-- | engine/evarutil.mli | 9 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
3 files changed, 33 insertions, 10 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b3e17fa9d..bd86f4bd2 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -290,8 +290,18 @@ let make_pure_subst evi args = * we have the property that u and phi(t) are convertible in env. *) +let csubst_subst (k, s) c = + let rec subst n c = match Constr.kind c with + | Rel m -> + if m <= n then c + else if m - n <= k then Int.Map.find (k - m + n) s + else mkRel (m - k) + | _ -> Constr.map_with_binders succ subst n c + in + if k = 0 then c else subst 0 c + let subst2 subst vsubst c = - substl subst (replace_vars vsubst c) + csubst_subst subst (replace_vars vsubst c) let next_ident_away id avoid = let avoid id = Id.Set.mem id avoid in @@ -302,10 +312,18 @@ let next_name_away na avoid = let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in next_ident_away_from id avoid +type csubst = int * Constr.t Int.Map.t + +let empty_csubst = (0, Int.Map.empty) + type ext_named_context = - Vars.substl * (Id.t * Constr.constr) list * + csubst * (Id.t * Constr.constr) list * Id.Set.t * Context.Named.t +let push_var id (n, s) = + let s = Int.Map.add n (mkVar id) s in + (succ n, s) + let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in let replace_var_named_declaration id0 id decl = @@ -340,14 +358,14 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named context. Unless [id] is a section variable. *) - let subst = List.map (replace_vars [id0,mkVar id]) subst in + let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in let vsubst = (id0,mkVar id)::vsubst in let d = match c with | None -> LocalAssum (id0, subst2 subst vsubst t) | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) in let nc = List.map (replace_var_named_declaration id0 id) nc in - (mkVar id0 :: subst, vsubst, Id.Set.add id avoid, d :: nc) + (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) | _ -> (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where @@ -357,7 +375,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = | None -> LocalAssum (id, subst2 subst vsubst t) | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) in - (mkVar id :: subst, vsubst, Id.Set.add id avoid, d :: nc) + (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) let push_rel_context_to_named_context env typ = (* compute the instances relative to the named context and rel_context *) @@ -371,7 +389,7 @@ let push_rel_context_to_named_context env typ = (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = Context.Rel.fold_outside push_rel_decl_to_named_context - (rel_context env) ~init:([], [], avoid, named_context env) in + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) (*------------------------------------* diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 429ea73de..c0c81442d 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,15 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +type csubst + +val empty_csubst : csubst +val csubst_subst : csubst -> Constr.t -> Constr.t + type ext_named_context = - Vars.substl * (Id.t * Constr.constr) list * + csubst * (Id.t * Constr.constr) list * Id.Set.t * Context.Named.t val push_rel_decl_to_named_context : Context.Rel.Declaration.t -> ext_named_context -> ext_named_context val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list + named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3527b3b12..1ef96e034 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -82,7 +82,7 @@ let get_extra env = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside push_rel_decl_to_named_context - (Environ.rel_context env) ~init:([], [], avoid, named_context env) + (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) let make_env env = { env = env; extra = lazy (get_extra env) } let rel_context env = rel_context env.env @@ -102,7 +102,7 @@ let push_rel_context ctx env = { let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = - let subst2 subst vsubst c = substl subst (replace_vars vsubst c) in + let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in |