1 files changed, 150 insertions, 67 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 339c6a248e..f82ffccdc3 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,11 +10,12 @@ open CErrors
 open Util
 open Names
 open Term
-open Termops
-open Namegen
+open Constr
 open Pre_env
 open Environ
 open Evd
+open Termops
+open Namegen
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -53,15 +54,15 @@ let new_global evd x =
 
 (* flush_and_check_evars fails if an existential is undefined *)
 
-exception Uninstantiated_evar of existential_key
+exception Uninstantiated_evar of Evar.t
 
 let rec flush_and_check_evars sigma c =
-  match kind_of_term c with
+  match kind c with
   | Evar (evk,_ as ev) ->
       (match existential_opt_value sigma ev with
        | None -> raise (Uninstantiated_evar evk)
        | Some c -> flush_and_check_evars sigma c)
-  | _ -> map_constr (flush_and_check_evars sigma) c
+  | _ -> Constr.map (flush_and_check_evars sigma) c
 
 let flush_and_check_evars sigma c =
   flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
@@ -162,7 +163,7 @@ exception NoHeadEvar
 let head_evar sigma c =
   (** FIXME: this breaks if using evar-insensitive code *)
   let c = EConstr.Unsafe.to_constr c in
-  let rec hrec c = match kind_of_term c with
+  let rec hrec c = match kind c with
     | Evar (evk,_)   -> evk
     | Case (_,_,c,_) -> hrec c
     | App (c,_)      -> hrec c
@@ -198,9 +199,10 @@ let whd_head_evar sigma c =
 let meta_counter_summary_name = "meta counter"
 
 (* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
-  fun () -> incr meta_ctr; !meta_ctr
+let meta_ctr, meta_counter_summary_tag =
+  Summary.ref_tag 0 ~name:meta_counter_summary_name
+
+let new_meta () = incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = EConstr.mkMeta(new_meta())
 
@@ -255,22 +257,6 @@ let make_pure_subst evi args =
  *   we have the property that u and phi(t) are convertible in env.
  *)
 
-let csubst_subst (k, s) c =
-  (** Safe because this is a substitution *)
-  let c = EConstr.Unsafe.to_constr c in
-  let rec subst n c = match Constr.kind c with
-  | Rel m ->
-    if m <= n then c
-    else if m - n <= k then EConstr.Unsafe.to_constr (Int.Map.find (k - m + n) s)
-    else mkRel (m - k)
-  | _ -> Constr.map_with_binders succ subst n c
-  in
-  let c = if k = 0 then c else subst 0 c in
-  EConstr.of_constr c
-
-let subst2 subst vsubst c =
-  csubst_subst subst (EConstr.Vars.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
@@ -280,19 +266,79 @@ let next_name_away na avoid =
   let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
   next_ident_away_from id avoid
 
-type csubst = int * EConstr.t Int.Map.t
-
-let empty_csubst = (0, Int.Map.empty)
+type subst_val =
+| SRel of int
+| SVar of Id.t
+
+type csubst = {
+  csubst_len : int;
+  (** Cardinal of [csubst_rel] *)
+  csubst_var : Constr.t Id.Map.t;
+  (** A mapping of variables to variables. We use the more general
+      [Constr.t] to share allocations, but all values are of shape [Var _]. *)
+  csubst_rel : Constr.t Int.Map.t;
+  (** A contiguous mapping of integers to variables. Same remark for values. *)
+  csubst_rev : subst_val Id.Map.t;
+  (** Reverse mapping of the substitution *)
+}
+(** This type represent a name substitution for the named and De Bruijn parts of
+    a environment. For efficiency we also store the reverse substitution.
+    Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel]
+    must be pairwise distinct. *)
+
+let empty_csubst = {
+  csubst_len = 0;
+  csubst_rel = Int.Map.empty;
+  csubst_var = Id.Map.empty;
+  csubst_rev = Id.Map.empty;
+}
+
+let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
+  (** Safe because this is a substitution *)
+  let c = EConstr.Unsafe.to_constr c in
+  let rec subst n c = match Constr.kind c with
+  | Rel m ->
+    if m <= n then c
+    else if m - n <= k then Int.Map.find (k - m + n) s
+    else mkRel (m - k)
+  | Var id ->
+    begin try Id.Map.find id v with Not_found -> c end
+  | _ -> Constr.map_with_binders succ subst n c
+  in
+  let c = if k = 0 && Id.Map.is_empty v then c else subst 0 c in
+  EConstr.of_constr c
 
 type ext_named_context =
-  csubst * (Id.t * EConstr.constr) list *
-  Id.Set.t * EConstr.named_context
-
-let push_var id (n, s) =
-  let s = Int.Map.add n (EConstr.mkVar id) s in
-  (succ n, s)
-
-let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
+  csubst * Id.Set.t * EConstr.named_context
+
+let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } =
+  let s = Int.Map.add n (Constr.mkVar id) s in
+  let r = Id.Map.add id (SRel n) r in
+  { csubst_len = succ n; csubst_var = v; csubst_rel = s; csubst_rev = r }
+
+(** Post-compose the substitution with the generator [src ↦ tgt] *)
+let update_var src tgt subst =
+  let cur =
+    try Some (Id.Map.find src subst.csubst_rev)
+    with Not_found -> None
+  in
+  match cur with
+  | None ->
+    (** Missing keys stand for identity substitution [src ↦ src] *)
+    let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
+    let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
+    { subst with csubst_var; csubst_rev }
+  | Some bnd ->
+    let csubst_rev = Id.Map.add tgt bnd (Id.Map.remove src subst.csubst_rev) in
+    match bnd with
+    | SRel m ->
+      let csubst_rel = Int.Map.add m (Constr.mkVar tgt) subst.csubst_rel in
+      { subst with csubst_rel; csubst_rev }
+    | SVar id ->
+      let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in
+      { subst with csubst_var; csubst_rev }
+
+let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
@@ -306,7 +352,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
   in
   let extract_if_neq id = function
     | Anonymous -> None
-    | Name id' when id_ord id id' = 0 -> None
+    | Name id' when Id.compare id id' = 0 -> None
     | Name id' -> Some id'
   in
   let na = RelDecl.get_name decl in
@@ -328,18 +374,17 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
           binding named [id], we will keep [id0] (the name given
           by the user) and rename [id0] into [id] in the named
           context. Unless [id] is a section variable. *)
-      let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in
-      let vsubst = (id0,mkVar id)::vsubst in
-      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (subst2 subst vsubst) in
+      let subst = update_var id0 id subst in
+      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
       let nc = List.map (replace_var_named_declaration id0 id) nc in
-      (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc)
+      (push_var id0 subst, Id.Set.add id avoid, d :: nc)
   | _ ->
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
           the new binder has name [id]. Which amounts to the same
           behaviour than when [id=id0]. *)
-      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in
-      (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
+      let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
+      (push_var id subst, Id.Set.add id avoid, d :: nc)
 
 let push_rel_context_to_named_context env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
@@ -348,17 +393,17 @@ let push_rel_context_to_named_context env sigma typ =
   let ids = List.map get_id (named_context env) in
   let inst_vars = List.map mkVar ids in
   if List.is_empty (Environ.rel_context env) then
-    (named_context_val env, typ, inst_vars, empty_csubst, [])
+    (named_context_val env, typ, inst_vars, empty_csubst)
   else
     let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
     let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
     (* move the rel context to a named context and extend the named instance *)
     (* with vars of the rel context *)
     (* We do keep the instances corresponding to local definition (see above) *)
-    let (subst, vsubst, _, env) =
+    let (subst, _, env) =
       Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
-        (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
-    (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+        (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
+    (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
 
 (*------------------------------------*
  * Entry points to define new evars   *
@@ -423,8 +468,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin
 (* [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 evd typ in
-  let map c = subst2 subst vsubst c in
+  let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in
+  let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
     match filter with
@@ -478,8 +523,6 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
-let cleared = Store.field ()
-
 exception Depends of Id.t
 
 let rec check_and_clear_in_constr env evdref err ids global c =
@@ -487,7 +530,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
      (ie the hypotheses ids have been removed from the contexts of
      evars). [global] should be true iff there is some variable of [ids] which
      is a section variable *)
-    match kind_of_term c with
+    match kind c with
       | Var id' ->
       if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
 
@@ -552,16 +595,9 @@ let rec check_and_clear_in_constr env evdref err ids global c =
               let evd = !evdref in
               let (evd,_) = restrict_evar evd evk filter None in
               evdref := evd;
-	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
-	      let evi = Evd.find !evdref evk in
-	      let extra = evi.evar_extra in
-	      let extra' = Store.set extra cleared true in
-	      let evi' = { evi with evar_extra = extra' } in
-	      evdref := Evd.add !evdref evk evi' ;
-	    (* spiwack: /hacking session *)
               Evd.existential_value !evdref ev
 
-      | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
+      | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
 
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
@@ -665,11 +701,9 @@ let rec advance sigma evk =
   match evi.evar_body with
   | Evar_empty -> Some evk
   | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra cleared) then
-        let (evk,_) = Term.destEvar v in
-        advance sigma evk
-      else
-        None
+      match is_restricted_evar evi with
+      | Some evk -> advance sigma evk
+      | None -> None
 
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
@@ -701,16 +735,65 @@ let undefined_evars_of_evar_info evd evi =
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
+type undefined_evars_cache = {
+  mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t;
+}
+
+let create_undefined_evars_cache () = { cache = Id.Map.empty; }
+
+let cached_evar_of_hyp cache sigma decl accu = match cache with
+| None ->
+  let fold c acc =
+    let evs = undefined_evars_of_term sigma c in
+    Evar.Set.union evs acc
+  in
+  NamedDecl.fold_constr fold decl accu
+| Some cache ->
+  let id = NamedDecl.get_id decl in
+  let r =
+    try Id.Map.find id cache.cache
+    with Not_found ->
+      (** Dummy value *)
+      let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
+      let () = cache.cache <- Id.Map.add id r cache.cache in
+      r
+  in
+  let (decl', evs) = !r in
+  let evs =
+    if NamedDecl.equal (==) decl decl' then snd !r
+    else
+      let fold c acc =
+        let evs = undefined_evars_of_term sigma c in
+        Evar.Set.union evs acc
+      in
+      let evs = NamedDecl.fold_constr fold decl Evar.Set.empty in
+      let () = r := (decl, evs) in
+      evs
+  in
+  Evar.Set.fold Evar.Set.add evs accu
+
+let filtered_undefined_evars_of_evar_info ?cache sigma evi =
+  let evars_of_named_context cache accu nc =
+    let fold decl accu = cached_evar_of_hyp cache sigma (EConstr.of_named_decl decl) accu in
+    Context.Named.fold_outside fold nc ~init:accu
+  in
+  let accu = match evi.evar_body with
+  | Evar_empty -> Evar.Set.empty
+  | Evar_defined b -> evars_of_term b
+  in
+  let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in
+  evars_of_named_context cache accu (evar_filtered_context evi)
+
 (* spiwack: this is a more complete version of
    {!Termops.occur_evar}. The latter does not look recursively into an
    [evar_map]. If unification only need to check superficially, tactics
    do not have this luxury, and need the more complete version. *)
 let occur_evar_upto sigma n c =
   let c = EConstr.Unsafe.to_constr c in
-  let rec occur_rec c = match kind_of_term c with
+  let rec occur_rec c = match kind c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
-    | _ -> iter_constr occur_rec c
+    | _ -> Constr.iter occur_rec c
   in
   try occur_rec c; false with Occur -> true