Reorganizing the structure of evarutil.ml (only restructuration, no

change of semantics).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 416 insertions, 372 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 0a4782d8c1..ab676f0e9a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -323,6 +323,7 @@ let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
 
 (* Tests if a de Bruijn index *)
 let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
+let isRelN n c = match kind_of_term c with Rel n' -> n = n' | _ -> false
 
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
diff --git a/kernel/term.mli b/kernel/term.mli
index a54130efa2..e83be6d63b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -229,8 +229,9 @@ val kind_of_type : types -> (constr, types) kind_of_type
 (** {6 Simple term case analysis. } *)
 
 val isRel  : constr -> bool
+val isRelN : int -> constr -> bool
 val isVar  : constr -> bool
-val isVarId  : identifier -> constr -> bool
+val isVarId : identifier -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
diff --git a/lib/util.ml b/lib/util.ml
index e6c76f7f3d..2bbdc76cf9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -666,6 +666,12 @@ let list_map_filter_i f =
 	match f i x with None -> l' | Some y -> y::l'
   in aux 0
 
+let list_filter_along f filter l =
+  snd (list_filter2 (fun b c -> f b) (filter,l))
+
+let list_filter_with filter l =
+  list_filter_along (fun x -> x) filter l
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -1183,6 +1189,12 @@ let array_rev_to_list a =
     if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
   tolist 0 []
 
+let array_filter_along f filter v =
+  Array.of_list (list_filter_along f filter (Array.to_list v))
+
+let array_filter_with filter v =
+  Array.of_list (list_filter_with filter (Array.to_list v))
+
 (* Stream *)
 
 let stream_nth n st =
diff --git a/lib/util.mli b/lib/util.mli
index 37d15792f2..8f8475afd7 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -87,6 +87,8 @@ val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
 val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
 val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+val list_filter_with : bool list -> 'a list -> 'a list
+val list_filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
 
 (** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
@@ -244,6 +246,8 @@ val array_fold_map2' :
 val array_distinct : 'a array -> bool
 val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_rev_to_list : 'a array -> 'a list
+val array_filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
+val array_filter_with : bool list -> 'a array -> 'a array
 
 (** {6 Streams. } *)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8e61cdebb7..f2fc80016b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -783,12 +783,12 @@ let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
-  match evar_conv_x ts env !evd CONV t1 t2 with
-      (evd',true) -> evd := evd'; true
+let e_conv ?(ts=full_transparent_state) env evdref t1 t2 =
+  match evar_conv_x ts env !evdref CONV t1 t2 with
+      (evd',true) -> evdref := evd'; true
     | _ -> false
 
-let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
-  match evar_conv_x ts env !evd CUMUL t1 t2 with
-      (evd',true) -> evd := evd'; true
+let e_cumul ?(ts=full_transparent_state) env evdref t1 t2 =
+  match evar_conv_x ts env !evdref CUMUL t1 t2 with
+      (evd',true) -> evdref := evd'; true
     | _ -> false
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8da1270727..2fbf0471b0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -22,8 +22,11 @@ open Reductionops
 open Pretype_errors
 open Retyping
 
-(* Expanding existential variables *)
-(* 1- flush_and_check_evars fails if an existential is undefined *)
+(****************************************************)
+(* Expanding/testing/exposing existential variables *)
+(****************************************************)
+
+(* flush_and_check_evars fails if an existential is undefined *)
 
 exception Uninstantiated_evar of existential_key
 
@@ -72,6 +75,75 @@ let nf_evars_undefined evm =
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
 
+(*-------------------*)
+(* Auxiliary functions for the conversion algorithms modulo evars
+ *)
+
+let has_undefined_evars_or_sorts 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)
+    | Sort s when is_sort_variable evd s -> raise Not_found
+    | _ -> 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_or_sorts evd t)
+
+let is_ground_env evd env =
+  let is_ground_decl = function
+      (_,Some b,_) -> is_ground_term evd b
+    | _ -> true in
+  List.for_all is_ground_decl (rel_context env) &&
+  List.for_all is_ground_decl (named_context env)
+(* Memoization is safe since evar_map and environ are applicative
+   structures *)
+let is_ground_env = memo1_2 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
+    | _              -> 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) when Evd.is_defined sigma evk
+	  -> whrec (existential_value sigma ev, l)
+      | Cast (c,_,_) -> whrec (c, l)
+      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | _ -> s
+  in
+  whrec (c, [])
+
+let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
+
+let collect_vars c =
+  let rec collrec acc c =
+    match kind_of_term c with
+    | Var id -> list_add_set id acc
+    | _      -> fold_constr collrec acc c
+  in
+  collrec [] c
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -167,6 +239,84 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter ?cand
   let evd = evar_declare sign newevk typ ~src:src ?filter ?candidates evd in
   (evd,mkEvar (newevk,Array.of_list instance))
 
+(* [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 push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let ids = List.map pi1 (named_context env) in
+  let inst_vars = List.map mkVar ids 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, _, env) =
+    Sign.fold_rel_context
+      (fun (na,c,t) (subst, avoid, env) ->
+	let id = next_name_away na avoid in
+	let d = (id,Option.map (substl subst) c,substl subst t) in
+	(mkVar id :: subst, id::avoid, push_named d env))
+      (rel_context env) ~init:([], ids, env) in
+  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
+
+(* [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 evd env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates typ =
+  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
+  let candidates = Option.map (List.map (substl subst)) candidates in
+  let instance =
+    match filter with
+    | None -> instance
+    | Some filter -> list_filter_with filter instance in
+  new_evar_instance sign evd typ' ~src:src ?filter ?candidates instance
+
+  (* The same using side-effect *)
+let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
+  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates 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
+
+(***************************************)
+(* Managing chains of local definitons *)
+(***************************************)
+
 (* Expand rels and vars that are bound to other rels or vars so that
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
@@ -292,6 +442,235 @@ let free_vars_and_rels_up_alias_expansion aliases c =
   frec (aliases,0) c;
   (!acc1,!acc2)
 
+(************************************)
+(* Removing a dependency in an evar *)
+(* (bind it to restrict_evar?)      *)
+(************************************)
+
+type clear_dependency_error =
+| OccurHypInSimpleClause of identifier option
+| EvarTypingBreak of existential
+
+exception ClearDependencyError of identifier * clear_dependency_error
+
+open Store.Field
+
+let cleared = Store.field ()
+
+let rec check_and_clear_in_constr evdref err ids c =
+  (* returns a new constr where all the evars have been 'cleaned'
+     (ie the hypotheses ids have been removed from the contexts of
+     evars) *)
+  let check id' =
+    if List.mem id' ids then
+      raise (ClearDependencyError (id',err))
+  in
+    match kind_of_term c with
+      | Var id' ->
+	  check id'; c
+
+      | ( Const _ | Ind _ | Construct _ ) ->
+          let vars = Environ.vars_of_global (Global.env()) c in
+            List.iter check vars; 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 evdref err ids 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 (nhyps,nargs,rids) =
+	      List.fold_right2
+		(fun (rid,ob,c as h) a (hy,ar,ri) ->
+		  (* Check if some id to clear occurs in the instance
+		     a of rid in ev and remember the dependency *)
+		  match
+		    List.filter (fun id -> List.mem id ids) (collect_vars a)
+		  with
+		  | id :: _ -> (hy,ar,(rid,id)::ri)
+		  | _ ->
+		  (* 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 *)
+		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
+		  | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
+		  | _ ->
+		  (* No dependency at all, we can keep this ev's context hyp *)
+		      (h::hy,a::ar,ri))
+		ctxt (Array.to_list l) ([],[],[]) 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 check_and_clear_in_constr evdref (EvarTypingBreak ev)
+		    (List.map fst rids) (evar_concl evi)
+	      with ClearDependencyError (rid,err) ->
+		raise (ClearDependencyError (List.assoc rid rids,err)) in
+
+            if rids = [] then c else begin
+	      let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
+	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
+	      evdref := Evd.define evk ev' !evdref;
+	      let (evk',_) = destEvar ev' in
+	    (* 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' = cleared.set true extra in
+	      let evi' = { evi with evar_extra = extra' } in
+	      evdref := Evd.add !evdref evk evi' ;
+	    (* spiwack: /hacking session *)
+	      mkEvar(evk', Array.of_list nargs)
+            end
+
+      | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
+
+let clear_hyps_in_evi evdref hyps concl 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 occuring in evi *)
+  let nconcl =
+    check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
+  let nhyps =
+    let check_context (id,ob,c) =
+      let err = OccurHypInSimpleClause (Some id) in
+      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
+	check_and_clear_in_constr evdref err ids c)
+    in
+    let check_value vk =
+      match !vk with
+	| VKnone -> vk
+	| VKvalue (v,d) ->
+	    if (List.for_all (fun e -> not (Idset.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 *)
+	      ref VKnone
+    in
+      remove_hyps ids check_context check_value hyps
+  in
+  (nhyps,nconcl)
+
+(********************************)
+(* Managing pattern-unification *)
+(********************************)
+
+let rec expand_and_check_vars aliases = function
+  | [] -> []
+  | a::l when isRel a or isVar a ->
+      let a = expansion_of_var aliases a in
+      if isRel a or isVar a then a :: expand_and_check_vars aliases l
+      else raise Exit
+  | _ ->
+      raise Exit
+
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
+let rec constr_list_distinct l =
+  let visited = Constrhash.create 23 in
+  let rec loop = function
+    | h::t ->
+	if Constrhash.mem visited h then false
+	else (Constrhash.add visited h h; loop t)
+    | [] -> true
+  in loop l
+
+let get_actual_deps aliases l t =
+  if occur_meta_or_existential t then
+    (* Probably no restrictions on allowed vars in presence of evars *)
+    l
+  else
+    (* Probably strong restrictions coming from t being evar-closed *)
+    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    List.filter (fun c ->
+      match kind_of_term c with
+      | Var id -> Idset.mem id fv_ids
+      | Rel n -> Intset.mem n fv_rels
+      | _ -> assert false) l
+
+let remove_instance_local_defs evd evk args =
+  let evi = Evd.find evd evk in
+  let rec aux = function
+  | (_,Some _,_)::sign, a::args -> aux (sign,args)
+  | (_,None,_)::sign, a::args -> a::aux (sign,args)
+  | [], [] -> []
+  | _ -> assert false in
+  aux (evar_filtered_context evi, args)
+
+(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
+
+let find_unification_pattern_args env l t =
+  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
+    let aliases = make_alias_map env in
+    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
+    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern_meta env nb m l t =
+  (* Variables from context and rels > nb are implicitly all there *)
+  (* so we need to be a rel <= nb *)
+  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
+    match find_unification_pattern_args env l t with
+    | Some _ as x when not (dependent (mkMeta m) t) -> x
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern_evar env evd (evk,args) l t =
+  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
+    let args = remove_instance_local_defs evd evk (Array.to_list args) in
+    let n = List.length args in
+    match find_unification_pattern_args env (args @ l) t with
+    | Some l when not (occur_evar evk t) -> Some (list_skipn n l)
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern (env,nb) evd f l t =
+  match kind_of_term f with
+  | Meta m -> is_unification_pattern_meta env nb m l t
+  | Evar ev -> is_unification_pattern_evar env evd ev l t
+  | _ -> None
+
+(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
+   (pattern unification). It is assumed that l is made of rel's that
+   are distinct and not bound to aliases. *)
+(* It is also assumed that c does not contain metas because metas
+   *implicitly* depend on Vars but lambda abstraction will not reflect this
+   dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
+   return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
+let solve_pattern_eqn env l c =
+  let c' = List.fold_right (fun a c ->
+    let c' = subst_term (lift 1 a) (lift 1 c) in
+    match kind_of_term a with
+      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
+      | Rel n ->
+          let d = map_rel_declaration (lift n) (lookup_rel n env) in
+          mkLambda_or_LetIn d c'
+      | Var id ->
+          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
+      | _ -> assert false)
+    l c in
+  (* Warning: we may miss some opportunity to eta-reduce more since c'
+     is not in normal form *)
+  whd_eta c'
+
+(*****************************************)
+(* Refining/solving unification problems *)
+(*****************************************)
+
 (* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
  * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
  * If a variable and an alias of it are bound to the same instance, we skip
@@ -345,80 +724,6 @@ let make_pure_subst evi args =
 	| _ -> anomaly "Instance does not match its signature")
     (evar_filtered_context evi) (array_rev_to_list args,[]))
 
-(* [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 push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
-  let ids = List.map pi1 (named_context env) in
-  let inst_vars = List.map mkVar ids 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, _, env) =
-    Sign.fold_rel_context
-      (fun (na,c,t) (subst, avoid, env) ->
-	let id = next_name_away na avoid in
-	let d = (id,Option.map (substl subst) c,substl subst t) in
-	(mkVar id :: subst, id::avoid, push_named d env))
-      (rel_context env) ~init:([], ids, env) in
-  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
-
-(* [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 evd env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates typ =
-  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
-  let candidates = Option.map (List.map (substl subst)) candidates in
-  let instance =
-    match filter with
-    | None -> instance
-    | Some filter -> snd (list_filter2 (fun b c -> b) (filter,instance)) in
-  new_evar_instance sign evd typ' ~src:src ?filter ?candidates instance
-
-  (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates 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
-
 (*------------------------------------*
  * operations on the evar constraints *
  *------------------------------------*)
@@ -480,8 +785,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
-  let inst_in_sign =
-    List.map mkVar (snd (list_filter2 (fun b id -> b) (filter1,ids1))) in
+  let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
     List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
       match b with
@@ -511,7 +815,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   (evd, ev2_in_sign, ev2_in_env)
 
 let subfilter env ccl filter newfilter args =
-  let vars = collect_vars ccl in
+  let vars = Termops.collect_vars ccl in
   let (filter, _, _, newargs) =
     List.fold_left2
       (fun (filter, newl, args, newargs) oldf (n, _, _) ->
@@ -541,124 +845,6 @@ let restrict_upon_filter ?(refine=false) evd evi evk p args =
   else
     evd,evk,args
 
-let collect_vars c =
-  let rec collrec acc c =
-    match kind_of_term c with
-    | Var id -> list_add_set id acc
-    | _      -> fold_constr collrec acc c
-  in
-  collrec [] c
-
-type clear_dependency_error =
-| OccurHypInSimpleClause of identifier option
-| EvarTypingBreak of existential
-
-exception ClearDependencyError of identifier * clear_dependency_error
-
-open Store.Field
-
-let cleared = Store.field ()
-
-let rec check_and_clear_in_constr evdref err ids c =
-  (* returns a new constr where all the evars have been 'cleaned'
-     (ie the hypotheses ids have been removed from the contexts of
-     evars) *)
-  let check id' =
-    if List.mem id' ids then
-      raise (ClearDependencyError (id',err))
-  in
-    match kind_of_term c with
-      | Var id' ->
-	  check id'; c
-
-      | ( Const _ | Ind _ | Construct _ ) ->
-          let vars = Environ.vars_of_global (Global.env()) c in
-            List.iter check vars; 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 evdref err ids 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 (nhyps,nargs,rids) =
-	      List.fold_right2
-		(fun (rid,ob,c as h) a (hy,ar,ri) ->
-		  (* Check if some id to clear occurs in the instance
-		     a of rid in ev and remember the dependency *)
-		  match
-		    List.filter (fun id -> List.mem id ids) (collect_vars a)
-		  with
-		  | id :: _ -> (hy,ar,(rid,id)::ri)
-		  | _ ->
-		  (* 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 *)
-		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
-		  | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
-		  | _ ->
-		  (* No dependency at all, we can keep this ev's context hyp *)
-		      (h::hy,a::ar,ri))
-		ctxt (Array.to_list l) ([],[],[]) 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 check_and_clear_in_constr evdref (EvarTypingBreak ev)
-		    (List.map fst rids) (evar_concl evi)
-	      with ClearDependencyError (rid,err) ->
-		raise (ClearDependencyError (List.assoc rid rids,err)) in
-
-            if rids = [] then c else begin
-	      let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
-	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
-	      evdref := Evd.define evk ev' !evdref;
-	      let (evk',_) = destEvar ev' in
-	    (* 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' = cleared.set true extra in
-	      let evi' = { evi with evar_extra = extra' } in
-	      evdref := Evd.add !evdref evk evi' ;
-	    (* spiwack: /hacking session *)
-	      mkEvar(evk', Array.of_list nargs)
-            end
-
-      | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
-
-let clear_hyps_in_evi evdref hyps concl 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 occuring in evi *)
-  let nconcl =
-    check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
-  let nhyps =
-    let check_context (id,ob,c) =
-      let err = OccurHypInSimpleClause (Some id) in
-      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
-	check_and_clear_in_constr evdref err ids c)
-    in
-    let check_value vk =
-      match !vk with
-	| VKnone -> vk
-	| VKvalue (v,d) ->
-	    if (List.for_all (fun e -> not (Idset.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 *)
-	      ref VKnone
-    in
-      remove_hyps ids check_context check_value hyps
-  in
-  (nhyps,nconcl)
-
 (* Inverting constructors in instances (common when inferring type of match) *)
 
 let find_projectable_constructor env evd cstr k args cstr_subst =
@@ -867,7 +1053,7 @@ let instance_of_projection f env t evd projs =
   | UniqueProjection (c,effects) ->
       (List.fold_left (do_projection_effects f env ty) evd effects, c)
 
-let filter_of_projection = function CannotInvert -> false | _ -> true
+let filter_of_projection = function Invertible _ -> true | _ -> false
 
 let filter_along f projs v =
   let l = Array.to_list v in
@@ -1283,173 +1469,6 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
 	| _ ->
 	    error_occur_check env evd evk rhs
 
-(*-------------------*)
-(* Auxiliary functions for the conversion algorithms modulo evars
- *)
-
-let has_undefined_evars_or_sorts 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)
-    | Sort s when is_sort_variable evd s -> raise Not_found
-    | _ -> 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_or_sorts evd t)
-
-let is_ground_env evd env =
-  let is_ground_decl = function
-      (_,Some b,_) -> is_ground_term evd b
-    | _ -> true in
-  List.for_all is_ground_decl (rel_context env) &&
-  List.for_all is_ground_decl (named_context env)
-(* Memoization is safe since evar_map and environ are applicative
-   structures *)
-let is_ground_env = memo1_2 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
-    | _              -> 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) when Evd.is_defined sigma evk
-	  -> whrec (existential_value sigma ev, l)
-      | Cast (c,_,_) -> whrec (c, l)
-      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
-      | _ -> s
-  in
-  whrec (c, [])
-
-let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
-
-let rec expand_and_check_vars aliases = function
-  | [] -> []
-  | a::l when isRel a or isVar a ->
-      let a = expansion_of_var aliases a in
-      if isRel a or isVar a then a :: expand_and_check_vars aliases l
-      else raise Exit
-  | _ ->
-      raise Exit
-
-module Constrhash = Hashtbl.Make
-  (struct type t = constr
-	  let equal = eq_constr
-	  let hash = hash_constr
-   end)
-
-let rec constr_list_distinct l =
-  let visited = Constrhash.create 23 in
-  let rec loop = function
-    | h::t ->
-	if Constrhash.mem visited h then false
-	else (Constrhash.add visited h h; loop t)
-    | [] -> true
-  in loop l
-
-let get_actual_deps aliases l t =
-  if occur_meta_or_existential t then
-    (* Probably no restrictions on allowed vars in presence of evars *)
-    l
-  else
-    (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
-    List.filter (fun c ->
-      match kind_of_term c with
-      | Var id -> Idset.mem id fv_ids
-      | Rel n -> Intset.mem n fv_rels
-      | _ -> assert false) l
-
-let remove_instance_local_defs evd evk args =
-  let evi = Evd.find evd evk in
-  let rec aux = function
-  | (_,Some _,_)::sign, a::args -> aux (sign,args)
-  | (_,None,_)::sign, a::args -> a::aux (sign,args)
-  | [], [] -> []
-  | _ -> assert false in
-  aux (evar_filtered_context evi, args)
-
-(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
-
-let find_unification_pattern_args env l t =
-  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let aliases = make_alias_map env in
-    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
-    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern_meta env nb m l t =
-  (* Variables from context and rels > nb are implicitly all there *)
-  (* so we need to be a rel <= nb *)
-  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
-    match find_unification_pattern_args env l t with
-    | Some _ as x when not (dependent (mkMeta m) t) -> x
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let args = remove_instance_local_defs evd evk (Array.to_list args) in
-    let n = List.length args in
-    match find_unification_pattern_args env (args @ l) t with
-    | Some l when not (occur_evar evk t) -> Some (list_skipn n l)
-    | _ -> None
-  else
-    None
-
-let is_unification_pattern (env,nb) evd f l t =
-  match kind_of_term f with
-  | Meta m -> is_unification_pattern_meta env nb m l t
-  | Evar ev -> is_unification_pattern_evar env evd ev l t
-  | _ -> None
-
-(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
-   (pattern unification). It is assumed that l is made of rel's that
-   are distinct and not bound to aliases. *)
-(* It is also assumed that c does not contain metas because metas
-   *implicitly* depend on Vars but lambda abstraction will not reflect this
-   dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
-   return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l c =
-  let c' = List.fold_right (fun a c ->
-    let c' = subst_term (lift 1 a) (lift 1 c) in
-    match kind_of_term a with
-      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
-      | Rel n ->
-          let d = map_rel_declaration (lift n) (lookup_rel n env) in
-          mkLambda_or_LetIn d c'
-      | Var id ->
-          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
-      | _ -> assert false)
-    l c in
-  (* Warning: we may miss some opportunity to eta-reduce more since c'
-     is not in normal form *)
-  whd_eta c'
-
 (* This code (i.e. solve_pb, etc.) takes a unification
  * problem, and tries to solve it. If it solves it, then it removes
  * all the conversion problems, and re-runs conversion on each one, in
@@ -1508,6 +1527,11 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
   with e when precatchable_exception e ->
     (evd,false)
 
+(*************************************)
+(* Removing a dependency in an evar *)
+(* (bind it to restrict_evar?)      *)
+(*************************************)
+
 (** The following functions return the set of evars immediately
     contained in the object, including defined evars *)
 
@@ -1630,7 +1654,9 @@ let check_evars env initial_sigma sigma c =
 
 open Glob_term
 
+(****************************************)
 (* Operations on value/type constraints *)
+(****************************************)
 
 type type_constraint = types option