summaryrefslogtreecommitdiff
path: root/engine/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evarutil.ml')
-rw-r--r--engine/evarutil.ml788
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 22:37:55 +0000