diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /engine/evarutil.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'engine/evarutil.ml')
-rw-r--r-- | engine/evarutil.ml | 788 |
1 files changed, 788 insertions, 0 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml new file mode 100644 index 00000000..df170c8d --- /dev/null +++ b/engine/evarutil.ml @@ -0,0 +1,788 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CErrors +open Util +open Names +open Term +open Vars +open Termops +open Namegen +open Pre_env +open Environ +open Evd +open Sigma.Notations + +let safe_evar_info sigma evk = + try Some (Evd.find sigma evk) + with Not_found -> None + +let safe_evar_value sigma ev = + try Some (Evd.existential_value sigma ev) + with NotInstantiatedEvar | Not_found -> None + +(** Combinators *) + +let evd_comb0 f evdref = + let (evd',x) = f !evdref in + evdref := evd'; + x + +let evd_comb1 f evdref x = + let (evd',y) = f !evdref x in + evdref := evd'; + y + +let evd_comb2 f evdref x y = + let (evd',z) = f !evdref x y in + evdref := evd'; + z + +let e_new_global evdref x = + evd_comb1 (Evd.fresh_global (Global.env())) evdref x + +let new_global evd x = + Sigma.fresh_global (Global.env()) evd x + +(****************************************************) +(* Expanding/testing/exposing existential variables *) +(****************************************************) + +(* flush_and_check_evars fails if an existential is undefined *) + +exception Uninstantiated_evar of existential_key + +let rec flush_and_check_evars sigma c = + match kind_of_term 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) + +let j_nf_evar sigma j = + { uj_val = nf_evar sigma j.uj_val; + uj_type = nf_evar sigma j.uj_type } +let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl +let jv_nf_evar sigma = Array.map (j_nf_evar sigma) +let tj_nf_evar sigma {utj_val=v;utj_type=t} = + {utj_val=nf_evar sigma v;utj_type=t} + +let nf_evars_universes evm = + Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) + (Evd.universe_subst evm) + +let nf_evars_and_universes evm = + let evm = Evd.nf_constraints evm in + evm, nf_evars_universes evm + +let e_nf_evars_and_universes evdref = + evdref := Evd.nf_constraints !evdref; + nf_evars_universes !evdref, Evd.universe_subst !evdref + +let nf_evar_map_universes evm = + let evm = Evd.nf_constraints evm in + let subst = Evd.universe_subst evm in + if Univ.LMap.is_empty subst then evm, nf_evar 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 + +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 nf_evar_info evc info = map_evar_info (nf_evar evc) info + +let nf_evar_map evm = + Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm + +let nf_evar_map_undefined evm = + Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) 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 + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true + +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 + | _ -> true in + let open Context.Named.Declaration in + let is_ground_named_decl = function + | LocalDef (_,b,_) -> is_ground_term evd b + | _ -> true in + List.for_all is_ground_rel_decl (rel_context env) && + List.for_all is_ground_named_decl (named_context env) + +(* Memoization is safe since evar_map and environ are applicative + structures *) +let memo f = + let m = ref None in + fun x y -> match !m with + | Some (x', y', r) when x == x' && y == y' -> r + | _ -> let r = f x y in m := Some (x, y, r); r + +let is_ground_env = memo is_ground_env + +(* Return the head evar if any *) + +exception NoHeadEvar + +let head_evar = + let rec hrec c = match kind_of_term c with + | Evar (evk,_) -> evk + | Case (_,_,c,_) -> hrec c + | App (c,_) -> hrec c + | Cast (c,_,_) -> hrec c + | Proj (p, c) -> hrec c + | _ -> raise NoHeadEvar + in + hrec + +(* 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 + | Cast (c,_,_) -> whrec (c, l) + | App (f,args) -> whrec (f, args :: l) + | _ -> s + in + whrec (c, []) + +let whd_head_evar sigma c = + 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) + +(**********************) +(* Creating new metas *) +(**********************) + +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 mk_new_meta () = mkMeta(new_meta()) + +(* The list of non-instantiated existential declarations (order is important) *) + +let non_instantiated sigma = + let listev = Evd.undefined_map sigma in + Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + +(************************) +(* Manipulating filters *) +(************************) + +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")) + (evar_filtered_context evi) (Array.rev_to_list args,[])) + +(*------------------------------------* + * functional operations on evar sets * + *------------------------------------*) + +(* [push_rel_context_to_named_context] builds the defining context and the + * initial instance of an evar. If the evar is to be used in context + * + * Gamma = a1 ... an xp ... x1 + * \- named part -/ \- de Bruijn part -/ + * + * then the x1...xp are turned into variables so that the evar is declared in + * context + * + * a1 ... an xp ... x1 + * \----------- named part ------------/ + * + * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)" + * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed + * in context Gamma. + * + * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first) + * Remark 2: If some of the ai or xj are definitions, we keep them in the + * instance. This is necessary so that no unfolding of local definitions + * happens when inferring implicit arguments (consider e.g. the problem + * "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which + * produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want + * the hole to be instantiated by x', not by x (which would have been + * the case in [invert_definition] if x' had disappeared from the instance). + * Note that at any time, if, in some context env, the instance of + * declaration x:A is t and the instance of definition x':=phi(x) is u, then + * 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 + +let next_name_away na avoid = + let avoid id = Id.Set.mem id avoid in + 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 = + 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 = + let id' = 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) + in + let extract_if_neq id = function + | Anonymous -> None + | Name id' when id_ord 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 id = + (* ppedrot: we want to infer nicer names for the refine tactic, but + keeping at the same time backward compatibility in other code + using this function. For now, we only attempt to preserve the + old behaviour of Program, but ultimately, one should do something + about this whole name generation problem. *) + if Flags.is_program_mode () then next_name_away na avoid + 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 + in + match extract_if_neq id na with + | Some id0 when not (is_section_variable id0) -> + (* spiwack: if [id<>id0], rather than introducing a new + 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 nc = List.map (replace_var_named_declaration id0 id) nc in + (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 + 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 push_rel_context_to_named_context env typ = + (* compute the instances relative to the named context and rel_context *) + let open Context.Named.Declaration 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, []) + 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) + +(*------------------------------------* + * Entry points to define new evars * + *------------------------------------*) + +let default_source = (Loc.ghost,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 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) + +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 default_naming = Misctypes.IntroAnonymous in + let naming = Option.default default_naming naming in + let evi = { + evar_hyps = sign; + evar_concl = typ; + evar_body = Evar_empty; + evar_filter = filter; + evar_source = src; + evar_candidates = candidates; + evar_extra = store; } + in + let (evd, newevk) = Evd.new_evar evd ~naming 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) + +let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = + 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) + +(* [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 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 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; + 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 e_new_Type ?(rigid=Evd.univ_flexible) env evdref = + let evd', s = new_sort_variable rigid !evdref in + evdref := evd'; 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 + evdref := evd'; + ev + +(* This assumes an evar with identity instance and generalizes it over only + the De Bruijn part of the context *) +let generalize_evar_over_rels sigma (ev,args) = + 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 + +(************************************) +(* Removing a dependency in an evar *) +(************************************) + +type clear_dependency_error = +| OccurHypInSimpleClause of Id.t option +| EvarTypingBreak of existential + +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 = + (* returns a new constr where all the evars have been 'cleaned' + (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 + | Var id' -> + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c + + | ( Const _ | Ind _ | Construct _ ) -> + let () = if global then + let check id' = + if Id.Set.mem id' ids then + raise (ClearDependencyError (id',err)) + in + Id.Set.iter check (Environ.vars_of_global env c) + in + 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 + (check_and_clear_in_constr env evdref err ids global nc) + else + (* We check for dependencies to elements of ids in the + evar_info corresponding to e and in the instance of + arguments. Concurrently, we build a new evar + corresponding to e where hypotheses of ids have been + removed *) + let evi = Evd.find_undefined !evdref evk in + let ctxt = Evd.evar_filtered_context evi in + let (rids,filter) = + List.fold_right2 + (fun h a (ri,filter) -> + try + (* 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 + (* 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 + 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)) + 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 *) + let _nconcl = + try + let nids = Id.Map.domain rids in + let global = Id.Set.exists is_section_variable nids in + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi) + with ClearDependencyError (rid,err) -> + raise (ClearDependencyError (Id.Map.find rid rids,err)) in + + if Id.Map.is_empty rids then 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 + 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 + + | _ -> map_constr (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 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 + in + let check_value vk = match force_lazy_val vk with + | None -> vk + | Some (_, d) -> + if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then + (* v does depend on any of ids, it's ok *) + vk + else + (* v depends on one of the cleared hyps: + we forget the computed value *) + dummy_lazy_val () + in + remove_hyps ids check_context check_value hyps + in + (nhyps,terms) + +let clear_hyps_in_evi env evdref hyps concl ids = + match clear_hyps_in_evi_main env evdref hyps [concl] ids with + | (nhyps,[nconcl]) -> (nhyps,nconcl) + | _ -> assert false + +let clear_hyps2_in_evi env evdref hyps t concl ids = + match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with + | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) + | _ -> assert false + +(* spiwack: a few functions to gather evars on which goals depend. *) +let queue_set q is_dependent set = + Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set +let queue_term q is_dependent c = + queue_set q is_dependent (evars_of_term c) + +let process_dependent_evar q acc evm is_dependent e = + let evi = Evd.find evm e in + (* Queues evars appearing in the types of the goal (conclusion, then + 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); + match decl with + | LocalAssum _ -> () + | LocalDef (_,b,_) -> queue_term q true b + end (Environ.named_context_of_val evi.evar_hyps); + match evi.evar_body with + | Evar_empty -> + if is_dependent then Evar.Map.add e None acc else acc + | Evar_defined b -> + let subevars = evars_of_term b in + (* evars appearing in the definition of an evar [e] are marked + as dependent when [e] is dependent itself: if [e] is a + non-dependent goal, then, unless they are reach from another + path, these evars are just other non-dependent goals. *) + queue_set q is_dependent subevars; + if is_dependent then Evar.Map.add e (Some subevars) acc else acc + +let gather_dependent_evars q evm = + let acc = ref Evar.Map.empty in + while not (Queue.is_empty q) do + let (is_dependent,e) = Queue.pop q in + (* checks if [e] has already been added to [!acc] *) + begin if not (Evar.Map.mem e !acc) then + acc := process_dependent_evar q !acc evm is_dependent e + end + done; + !acc + +let gather_dependent_evars evm l = + let q = Queue.create () in + List.iter (fun a -> Queue.add (false,a) q) l; + gather_dependent_evars q evm + +(* /spiwack *) + +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +(* spiwack: [advance] is probably performance critical, and the good + behaviour of its definition may depend sensitively to the actual + definition of [Evd.find]. Currently, [Evd.find] starts looking for + a value in the heap of undefined variable, which is small. Hence in + the most common case, where [advance] is applied to an unsolved + goal ([advance] is used to figure if a side effect has modified the + goal) it terminates quickly. *) +let rec advance sigma evk = + let evi = Evd.find sigma evk in + 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 + +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +let undefined_evars_of_term evd t = + let rec evrec acc c = + match kind_of_term 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 + 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))) + 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 + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> undefined_evars_of_term evd b) + (undefined_evars_of_named_context evd + (named_context_of_val evi.evar_hyps))) + +(* 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 + | 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 + in + try occur_rec c; false with Occur -> true + +(* We don't try to guess in which sort the type should be defined, since + 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 subterm_source evk (loc,k) = + let evk = match k with + | Evar_kinds.SubEvar (evk) -> evk + | _ -> 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) + +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +let eq_constr_univs_test sigma1 sigma2 t u = + (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) + let open Evd in + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + let ans = + Universes.eq_constr_univs_infer_with + (fun t -> kind_of_term_upto sigma1 t) + (fun u -> kind_of_term_upto sigma2 u) + (universes sigma2) fold t u sigma2 + in + match ans with None -> false | Some _ -> true + +type type_constraint = types option +type val_constraint = constr option |