diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 533 |
1 files changed, 305 insertions, 228 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df170c8d..9cf81ecc 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -1,26 +1,26 @@ (************************************************************************) -(* 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 CErrors open Util open Names open Term -open Vars -open Termops -open Namegen +open Constr open Pre_env open Environ open Evd -open Sigma.Notations +open Termops +open Namegen -let safe_evar_info sigma evk = - try Some (Evd.find sigma evk) - with Not_found -> None +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) @@ -44,10 +44,11 @@ let evd_comb2 f evdref x y = z let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x + EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) let new_global evd x = - Sigma.fresh_global (Global.env()) evd x + let (evd, c) = Evd.fresh_global (Global.env()) evd x in + (evd, EConstr.of_constr c) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -55,44 +56,25 @@ let new_global evd x = (* flush_and_check_evars fails if an existential is undefined *) -exception Uninstantiated_evar of existential_key +exception Uninstantiated_evar of Evar.t let rec flush_and_check_evars sigma c = - match kind_of_term c with + match kind c with | Evar (evk,_ as ev) -> (match existential_opt_value sigma ev with | None -> raise (Uninstantiated_evar evk) | Some c -> flush_and_check_evars sigma c) - | _ -> map_constr (flush_and_check_evars sigma) c - -(* let nf_evar_key = Profile.declare_profile "nf_evar" *) -(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *) - -let rec whd_evar sigma c = - match kind_of_term c with - | Evar (evk, args) -> - begin match safe_evar_info sigma evk with - | Some ({ evar_body = Evar_defined c } as info) -> - let args = Array.map (fun c -> whd_evar sigma c) args in - let c = instantiate_evar_array info c args in - whd_evar sigma c - | _ -> c - end - | Sort (Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> c - -let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t) + | _ -> Constr.map (flush_and_check_evars sigma) c + +let flush_and_check_evars sigma c = + flush_and_check_evars sigma (EConstr.Unsafe.to_constr c) + +(** Term exploration up to instantiation. *) +let kind_of_term_upto = EConstr.kind_upto + +let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t) +let whd_evar = EConstr.whd_evar +let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c) let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; @@ -107,33 +89,33 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in - if Univ.LMap.is_empty subst then evm, nf_evar evm + if Univ.LMap.is_empty subst then evm, nf_evar0 evm else let f = nf_evars_universes evm in Evd.raw_map (fun _ -> map_evar_info f) evm, f let nf_named_context_evar sigma ctx = - Context.Named.map (nf_evar sigma) ctx + Context.Named.map (nf_evar0 sigma) ctx let nf_rel_context_evar sigma ctx = Context.Rel.map (nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in - let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in - push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) + let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in + EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) -let nf_evar_info evc info = map_evar_info (nf_evar evc) info +let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info let nf_evar_map evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm @@ -145,21 +127,11 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) -(* A probably faster though more approximative variant of - [has_undefined (nf_evar c)]: instances are not substituted and - maybe an evar occurs in an instance and it would disappear by - instantiation *) - let has_undefined_evars evd t = let rec has_ev t = - match kind_of_term t with - | Evar (ev,args) -> - (match evar_body (Evd.find evd ev) with - | Evar_defined c -> - has_ev c; Array.iter has_ev args - | Evar_empty -> - raise NotInstantiatedEvar) - | _ -> iter_constr has_ev t in + match EConstr.kind evd t with + | Evar _ -> raise NotInstantiatedEvar + | _ -> EConstr.iter evd has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true @@ -167,13 +139,11 @@ let is_ground_term evd t = not (has_undefined_evars evd t) let is_ground_env evd env = - let open Context.Rel.Declaration in let is_ground_rel_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b) | _ -> true in - let open Context.Named.Declaration in let is_ground_named_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b) | _ -> true in List.for_all is_ground_rel_decl (rel_context env) && List.for_all is_ground_named_decl (named_context env) @@ -192,8 +162,10 @@ let is_ground_env = memo is_ground_env exception NoHeadEvar -let head_evar = - let rec hrec c = match kind_of_term c with +let head_evar sigma c = + (** FIXME: this breaks if using evar-insensitive code *) + let c = EConstr.Unsafe.to_constr c in + let rec hrec c = match kind c with | Evar (evk,_) -> evk | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c @@ -201,33 +173,24 @@ let head_evar = | Proj (p, c) -> hrec c | _ -> raise NoHeadEvar in - hrec + hrec c (* Expand head evar if any (currently consider only applications but I guess it should consider Case too) *) let whd_head_evar_stack sigma c = - let rec whrec (c, l as s) = - match kind_of_term c with - | Evar (evk,args as ev) -> - let v = - try Some (existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None in - begin match v with - | None -> s - | Some c -> whrec (c, l) - end + let rec whrec (c, l) = + match EConstr.kind sigma c with | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, args :: l) - | _ -> s + | c -> (EConstr.of_kind c, l) in whrec (c, []) let whd_head_evar sigma c = + let open EConstr in let (f, args) = whd_head_evar_stack sigma c in - (** optim: don't reallocate if empty/singleton *) match args with - | [] -> f | [arg] -> mkApp (f, arg) | _ -> mkApp (f, Array.concat args) @@ -238,11 +201,12 @@ let whd_head_evar sigma c = let meta_counter_summary_name = "meta counter" (* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr +let meta_ctr, meta_counter_summary_tag = + Summary.ref_tag 0 ~name:meta_counter_summary_name -let mk_new_meta () = mkMeta(new_meta()) +let new_meta () = incr meta_ctr; !meta_ctr + +let mk_new_meta () = EConstr.mkMeta(new_meta()) (* The list of non-instantiated existential declarations (order is important) *) @@ -255,12 +219,11 @@ let non_instantiated sigma = (************************) let make_pure_subst evi args = - let open Context.Named.Declaration in snd (List.fold_right (fun decl (args,l) -> match args with - | a::rest -> (rest, (get_id decl, a)::l) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* @@ -296,19 +259,6 @@ 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 = - csubst_subst subst (replace_vars vsubst c) - let next_ident_away id avoid = let avoid id = Id.Set.mem id avoid in next_ident_away_from id avoid @@ -318,34 +268,96 @@ 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 subst_val = +| SRel of int +| SVar of Id.t + +type csubst = { + csubst_len : int; + (** Cardinal of [csubst_rel] *) + csubst_var : Constr.t Id.Map.t; + (** A mapping of variables to variables. We use the more general + [Constr.t] to share allocations, but all values are of shape [Var _]. *) + csubst_rel : Constr.t Int.Map.t; + (** A contiguous mapping of integers to variables. Same remark for values. *) + csubst_rev : subst_val Id.Map.t; + (** Reverse mapping of the substitution *) +} +(** This type represent a name substitution for the named and De Bruijn parts of + a environment. For efficiency we also store the reverse substitution. + Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel] + must be pairwise distinct. *) + +let empty_csubst = { + csubst_len = 0; + csubst_rel = Int.Map.empty; + csubst_var = Id.Map.empty; + csubst_rev = Id.Map.empty; +} + +let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c = + (** Safe because this is a substitution *) + let c = EConstr.Unsafe.to_constr c in + 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) + | Var id -> + begin try Id.Map.find id v with Not_found -> c end + | _ -> Constr.map_with_binders succ subst n c + in + let c = if k = 0 && Id.Map.is_empty v then c else subst 0 c in + EConstr.of_constr c type ext_named_context = - 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 + csubst * Id.Set.t * EConstr.named_context + +let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } = + let s = Int.Map.add n (Constr.mkVar id) s in + let r = Id.Map.add id (SRel n) r in + { csubst_len = succ n; csubst_var = v; csubst_rel = s; csubst_rev = r } + +(** Post-compose the substitution with the generator [src ↦ tgt] *) +let update_var src tgt subst = + let cur = + try Some (Id.Map.find src subst.csubst_rev) + with Not_found -> None + in + match cur with + | None -> + (** Missing keys stand for identity substitution [src ↦ src] *) + let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in + let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in + { subst with csubst_var; csubst_rev } + | Some bnd -> + let csubst_rev = Id.Map.add tgt bnd (Id.Map.remove src subst.csubst_rev) in + match bnd with + | SRel m -> + let csubst_rel = Int.Map.add m (Constr.mkVar tgt) subst.csubst_rel in + { subst with csubst_rel; csubst_rev } + | SVar id -> + let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in + { subst with csubst_var; csubst_rev } + +let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = + let open EConstr in + let open Vars in + let map_decl f d = + NamedDecl.map_constr f d + in let replace_var_named_declaration id0 id decl = - let id' = get_id decl in + let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) + decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None - | Name id' when id_ord id id' = 0 -> None + | Name id' when Id.compare id id' = 0 -> None | Name id' -> Some id' in - let open Context.Rel.Declaration in - let (na, c, t) = to_tuple decl in - let open Context.Named.Declaration in + let na = RelDecl.get_name decl in let id = (* ppedrot: we want to infer nicer names for the refine tactic, but keeping at the same time backward compatibility in other code @@ -356,7 +368,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = else (** id_of_name_using_hdchar only depends on the rel context which is empty here *) - next_ident_away (id_of_name_using_hdchar empty_env t na) avoid + next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> @@ -364,64 +376,66 @@ 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 = (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 subst = update_var id0 id subst in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = List.map (replace_var_named_declaration id0 id) nc in - (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) + (push_var id0 subst, 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 the new binder has name [id]. Which amounts to the same behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in - (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in + (push_var id subst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env typ = +let push_rel_context_to_named_context env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in + let open EConstr in let ids = List.map get_id (named_context env) in let inst_vars = List.map mkVar ids in if List.is_empty (Environ.rel_context env) then - (named_context_val env, typ, inst_vars, empty_csubst, []) + (named_context_val env, typ, inst_vars, empty_csubst) else let avoid = List.fold_right Id.Set.add ids Id.Set.empty in let inst_rels = List.rev (rel_list 0 (nb_rel env)) in (* move the rel context to a named context and extend the named instance *) (* with vars of the rel context *) (* 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:(empty_csubst, [], avoid, named_context env) in - (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + let (subst, _, env) = + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) in + (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) (*------------------------------------* * Entry points to define new evars * *------------------------------------*) -let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter candidates = - let evd = Sigma.to_evar_map evd in - let evd, evk' = Evd.restrict evk filter ?candidates evd in - Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) +let restrict_evar evd evk filter ?src candidates = + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in + Evd.declare_future_goal evk' evd, evk' let new_pure_evar_full evd evi = - let evd = Sigma.to_evar_map evd in let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in - Sigma.Unsafe.of_pair (evk, evd) + (evd, evk) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let evd = Sigma.to_evar_map evd in + let typ = EConstr.Unsafe.to_constr typ in + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in + let name = match naming with + | Misctypes.IntroAnonymous -> None + | Misctypes.IntroIdentifier id -> Some id + | Misctypes.IntroFresh id -> + let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in + let id = Namegen.next_ident_away_from id has_name in + Some id + in let evi = { evar_hyps = sign; evar_concl = typ; @@ -431,70 +445,75 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca evar_candidates = candidates; evar_extra = store; } in - let (evd, newevk) = Evd.new_evar evd ~naming evi in + let (evd, newevk) = Evd.new_evar evd ?name evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in - Sigma.Unsafe.of_pair (newevk, evd) + (evd, newevk) let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = + let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in - Sigma (mkEvar (newevk,Array.of_list instance), evd, p) + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + evd, mkEvar (newevk,Array.of_list instance) + +let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in + let instance = + match filter with + | None -> instance + | Some filter -> Filter.filter_list filter instance in + new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in - let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in + let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in + let map c = csubst_subst subst c in + let candidates = Option.map (fun l -> List.map map l) candidates in let instance = match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in - (Sigma.to_evar_map evd, evk) - let new_type_evar env evd ?src ?filter ?naming ?principal rigid = - let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in - let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in - Sigma ((e, s), evd', p +> q) + let (evd', s) = new_sort_variable rigid evd in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + evd', (e, s) let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in - let sigma = Sigma.to_evar_map sigma in - evdref := sigma; + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in + evdref := evd; c let new_Type ?(rigid=Evd.univ_flexible) env evd = - let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in - Sigma (mkSort s, sigma, p) + let open EConstr in + let (evd, s) = new_sort_variable rigid evd in + (evd, mkSort s) let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = let evd', s = new_sort_variable rigid !evdref in - evdref := evd'; mkSort s + evdref := evd'; EConstr.mkSort s (* The same using side-effect *) let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in evdref := evd'; ev (* This assumes an evar with identity instance and generalizes it over only - the De Bruijn part of the context *) + the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = + let open EConstr in let evi = Evd.find sigma ev in let sign = named_context_of_val evi.evar_hyps in List.fold_left2 (fun (c,inst as x) a d -> - if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x) - (evi.evar_concl,[]) (Array.to_list args) sign + if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x) + (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign (************************************) (* Removing a dependency in an evar *) @@ -506,8 +525,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -let cleared = Store.field () - exception Depends of Id.t let rec check_and_clear_in_constr env evdref err ids global c = @@ -515,7 +532,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = (ie the hypotheses ids have been removed from the contexts of evars). [global] should be true iff there is some variable of [ids] which is a section variable *) - match kind_of_term c with + match kind c with | Var id' -> if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c @@ -532,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) - let nc = whd_evar !evdref c in + let nc = Evd.existential_value !evdref ev in (check_and_clear_in_constr env evdref err ids global nc) else (* We check for dependencies to elements of ids in the @@ -542,6 +559,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = removed *) let evi = Evd.find_undefined !evdref evk in let ctxt = Evd.evar_filtered_context evi in + let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in let (rids,filter) = List.fold_right2 (fun h a (ri,filter) -> @@ -549,19 +567,18 @@ let rec check_and_clear_in_constr env evdref err ids global c = (* Check if some id to clear occurs in the instance a of rid in ev and remember the dependency *) let check id = if Id.Set.mem id ids then raise (Depends id) in - let () = Id.Set.iter check (collect_vars a) in + let () = Id.Set.iter check (collect_vars !evdref (EConstr.of_constr a)) in (* Check if some rid to clear in the context of ev has dependencies in another hyp of the context of ev and transitively remember the dependency *) let check id _ = - if occur_var_in_decl (Global.env ()) id h + if occur_var_in_decl (Global.env ()) !evdref id h then raise (Depends id) in let () = Id.Map.iter check ri in (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) + with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) ctxt (Array.to_list l) (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) @@ -577,33 +594,25 @@ let rec check_and_clear_in_constr env evdref err ids global c = else let origfilter = Evd.evar_filter evi in let filter = Evd.Filter.apply_subfilter origfilter filter in - let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (_, evd, _) = restrict_evar evd evk filter None in - let evd = Sigma.to_evar_map evd in + let evd = !evdref in + let (evd,_) = restrict_evar evd evk filter None in evdref := evd; - (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) - let evi = Evd.find !evdref evk in - let extra = evi.evar_extra in - let extra' = Store.set extra cleared true in - let evi' = { evi with evar_extra = extra' } in - evdref := Evd.add !evdref evk evi' ; - (* spiwack: /hacking session *) - whd_evar !evdref c + Evd.existential_value !evdref ev - | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c + | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in let nhyps = - let open Context.Named.Declaration in let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids global) decl + let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in + NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl in let check_value vk = match force_lazy_val vk with | None -> vk @@ -618,7 +627,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,terms) + (nhyps,List.map EConstr.of_constr terms) let clear_hyps_in_evi env evdref hyps concl ids = match clear_hyps_in_evi_main env evdref hyps [concl] ids with @@ -642,8 +651,8 @@ let process_dependent_evar q acc evm is_dependent e = hypotheses), they are all dependent. *) queue_term q true evi.evar_concl; List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); + let open NamedDecl in + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b @@ -694,11 +703,9 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra cleared) then - let (evk,_) = Term.destEvar v in - advance sigma evk - else - None + match is_restricted_evar evi with + | Some evk -> advance sigma evk + | None -> None (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. @@ -707,42 +714,88 @@ let rec advance sigma evk = let undefined_evars_of_term evd t = let rec evrec acc c = - match kind_of_term c with + match EConstr.kind evd c with | Evar (n, l) -> - let acc = Array.fold_left evrec acc l in - (try match (Evd.find evd n).evar_body with - | Evar_empty -> Evar.Set.add n acc - | Evar_defined c -> evrec acc c - with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) - | _ -> fold_constr evrec acc c + let acc = Evar.Set.add n acc in + Array.fold_left evrec acc l + | _ -> EConstr.fold evd evrec acc c in evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c)))) nc ~init:Evar.Set.empty let undefined_evars_of_evar_info evd evi = - Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) + Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl)) (Evar.Set.union (match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> undefined_evars_of_term evd b) + | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b)) (undefined_evars_of_named_context evd (named_context_of_val evi.evar_hyps))) +type undefined_evars_cache = { + mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t; +} + +let create_undefined_evars_cache () = { cache = Id.Map.empty; } + +let cached_evar_of_hyp cache sigma decl accu = match cache with +| None -> + let fold c acc = + let evs = undefined_evars_of_term sigma c in + Evar.Set.union evs acc + in + NamedDecl.fold_constr fold decl accu +| Some cache -> + let id = NamedDecl.get_id decl in + let r = + try Id.Map.find id cache.cache + with Not_found -> + (** Dummy value *) + let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in + let () = cache.cache <- Id.Map.add id r cache.cache in + r + in + let (decl', evs) = !r in + let evs = + if NamedDecl.equal (==) decl decl' then snd !r + else + let fold c acc = + let evs = undefined_evars_of_term sigma c in + Evar.Set.union evs acc + in + let evs = NamedDecl.fold_constr fold decl Evar.Set.empty in + let () = r := (decl, evs) in + evs + in + Evar.Set.fold Evar.Set.add evs accu + +let filtered_undefined_evars_of_evar_info ?cache sigma evi = + let evars_of_named_context cache accu nc = + let fold decl accu = cached_evar_of_hyp cache sigma (EConstr.of_named_decl decl) accu in + Context.Named.fold_outside fold nc ~init:accu + in + let accu = match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term b + in + let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in + evars_of_named_context cache accu (evar_filtered_context evi) + (* spiwack: this is a more complete version of {!Termops.occur_evar}. The latter does not look recursively into an [evar_map]. If unification only need to check superficially, tactics do not have this luxury, and need the more complete version. *) let occur_evar_upto sigma n c = - let rec occur_rec c = match kind_of_term c with + let c = EConstr.Unsafe.to_constr c in + let rec occur_rec c = match kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) - | _ -> iter_constr occur_rec c + | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -750,8 +803,9 @@ let occur_evar_upto sigma n c = any type has type Type. May cause some trouble, but not so far... *) let judge_of_new_Type evd = - let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in - Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p) + let open EConstr in + let (evd', s) = new_univ_variable univ_rigid evd in + (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) let subterm_source evk (loc,k) = let evk = match k with @@ -759,10 +813,33 @@ let subterm_source evk (loc,k) = | _ -> evk in (loc,Evar_kinds.SubEvar evk) - -(** Term exploration up to instantiation. *) -let kind_of_term_upto sigma t = - Constr.kind (whd_evar sigma t) +(* Add equality constraints for covariant/invariant positions. For + irrelevant positions, unify universes when flexible. *) +let compare_cumulative_instances cv_pb variances u u' sigma = + let open Universes in + let cstrs = Univ.Constraint.empty in + let soft = Constraints.empty in + let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> + let open Univ.Variance in + match v with + | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft + | Covariant when cv_pb == Reduction.CUMUL -> + Univ.Constraint.add (u,Univ.Le,u') cstrs, soft + | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) + (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') + in + match Evd.add_constraints sigma cstrs with + | sigma -> + Inl (Evd.add_universe_constraints sigma soft) + | exception Univ.UniverseInconsistency p -> Inr p + +let compare_constructor_instances evd u u' = + let open Universes in + let soft = + Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) + Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') + in + Evd.add_universe_constraints evd soft (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable @@ -784,5 +861,5 @@ let eq_constr_univs_test sigma1 sigma2 t u = in match ans with None -> false | Some _ -> true -type type_constraint = types option -type val_constraint = constr option +type type_constraint = EConstr.types option +type val_constraint = EConstr.constr option |