Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui

s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).



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

7 files changed, 29 insertions, 100 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index c5c246877d..732ff1e69b 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -54,77 +54,11 @@ let subst_clenv sub clenv =
     env = clenv.env }
 
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
-let clenv_direct_nf_meta clenv c = direct_nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
 let clenv_value clenv = meta_instance clenv.evd clenv.templval
-let clenv_direct_value clenv = nf_betaiota clenv.templval.rebus
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
-let clenv_direct_nf_type clenv = nf_betaiota clenv.templtyp.rebus
-
-let plain_instance find c =
-  let rec irec u = match kind_of_term u with
-  | Meta p -> find p
-  | App (f,l) when isCast f ->
-      let (f,_,t) = destCast f in
-      let l' = Array.map irec l in 
-      (match kind_of_term f with
-      | Meta p ->
-	  (* Don't flatten application nodes: this is used to extract a
-             proof-term from a proof-tree and we want to keep the structure
-             of the proof-tree *)
-	  let g = find p in
-	  (match kind_of_term g with
-          | App _ -> 
-              let h = id_of_string "H" in
-              mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
-          | _ -> mkApp (g,l'))
-      | _ -> mkApp (irec f,l'))	
-  | Cast (m,_,_) when isMeta m -> find (destMeta m)
-  | _ -> map_constr irec u
-  in 
-  local_strong whd_betaiota
-    (if c.freemetas = Metaset.empty then c.rebus else irec c.rebus)
-
-let clenv_expand_metas clenv =
-  let seen = ref Metamap.empty in
-  let ongoing = ref Metaset.empty in
-  let todo = ref (meta_list clenv.evd) in
-
-  let rec process_all () = match !todo with
-  | [] -> ()
-  | (mv,cl)::_ -> let _ = process_meta mv cl in process_all ()
-
-  and process_meta mv cl =
-    ongoing := Metaset.add mv !ongoing;
-    let (body,typ) = match cl with
-    | Clval (na,(body,status),typ) ->
-	let body = plain_instance instance_of_meta body in
-	let typ = plain_instance instance_of_meta typ in
-	(body,Clval(na,(mk_freelisted body,status),mk_freelisted typ))
-    | Cltyp (na,typ) -> 
-	let typ = plain_instance instance_of_meta typ in
-        (mkMeta mv,Cltyp(na,mk_freelisted typ)) in
-    ongoing := Metaset.remove mv !ongoing;
-    seen := Metamap.add mv (body,typ) !seen;
-    todo := List.remove_assoc mv !todo;
-    body
-
-  and instance_of_meta mv =
-    try fst (Metamap.find mv !seen)
-    with Not_found ->
-      if Metaset.mem mv !ongoing then 
-	error "Cannot instantiate an existential variable with a term which depends on itself";
-    process_meta mv (find_meta clenv.evd mv) in
-
-    process_all ();
-
-    { clenv with
-      evd = replace_metas (Metamap.map snd !seen) clenv.evd;
-      templtyp = mk_freelisted(plain_instance instance_of_meta clenv.templtyp);
-      templval = mk_freelisted(plain_instance instance_of_meta clenv.templval)}
-
-let instantiated_clenv_template clenv = (clenv.templval,clenv.templtyp)
+
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
@@ -134,8 +68,7 @@ let clenv_get_type_of ce c =
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ =
-    whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_direct_nf_type cl) in
+  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -280,9 +213,13 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
  * returns a list of the metavars which appear in the type of
  * the metavar mv.  The list is unordered. *)
 
+let clenv_metavars evd mv =
+  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+
 let dependent_metas clenv mvs conclmetas =
   List.fold_right
-    (fun mv deps -> Metaset.union deps (meta_ftype clenv.evd mv).freemetas)
+    (fun mv deps ->
+       Metaset.union deps (clenv_metavars clenv.evd mv))
     mvs conclmetas
 
 let duplicated_metas c = 
@@ -294,14 +231,14 @@ let duplicated_metas c =
   snd (collrec ([],[]) c)
 
 let clenv_dependent hyps_only clenv =
-  let (body,typ) = instantiated_clenv_template clenv in
   let mvs = undefined_metas clenv.evd in
-  let deps = dependent_metas clenv mvs typ.freemetas in
-  let nonlinear = duplicated_metas body.rebus in
+  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  let nonlinear = duplicated_metas (clenv_value clenv) in
   (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
     (fun mv -> (Metaset.mem mv deps &&
-                not (hyps_only && Metaset.mem mv typ.freemetas))
+                not (hyps_only && Metaset.mem mv ctyp_mvs))
                or List.mem mv nonlinear) 
     mvs
 
@@ -430,9 +367,9 @@ type arg_bindings = open_constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let (body,typ) = instantiated_clenv_template clenv in
-  let mvs = Metaset.elements body.freemetas in
-  let deps = dependent_metas clenv mvs typ.freemetas in
+  let mvs = collect_metas (clenv_value clenv) in
+  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
 let check_bindings bl =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index de5a1e3758..dfa7513495 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -43,16 +43,10 @@ val subst_clenv : substitution -> clausenv -> clausenv
 
 (* subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
-(* subject of clenv (assume it is pre-instantiated) *)
-val clenv_direct_value : clausenv -> constr
 (* type of clenv (instantiated) *)
 val clenv_type      : clausenv -> types
-(* type of clenv (assume it is pre-instantiated) *)
-val clenv_direct_nf_type : clausenv -> types
 (* substitute resolved metas *)
 val clenv_nf_meta   : clausenv -> constr -> constr
-(* substitute resolved metas (assume the metas in clausenv are expanded) *)
-val clenv_direct_nf_meta   : clausenv -> constr -> constr
 (* type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
@@ -89,8 +83,6 @@ val clenv_dependent : bool -> clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
-val clenv_expand_metas : clausenv -> clausenv
-
 (***************************************************************)
 (* Bindings *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2b9a0ed82d..b29afc0cb3 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -610,18 +610,12 @@ let meta_with_name evd id =
           (str "Binder name \"" ++ pr_id id ++
            strbrk "\" occurs more than once in clause.")
 
-let mk_meta_subst evd =
-  Metamap.fold (fun mv cl subst -> match cl with
-    | Clval(_,(b,_),typ) -> (mv, b.rebus) :: subst
-    | Cltyp (_,typ)  -> subst) evd.metas []
 
 let meta_merge evd1 evd2 =
   {evd2 with
     metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
       evd2.metas (metamap_to_list evd1.metas) }
 
-let replace_metas metas evd = { evd with metas = metas }
-
 type metabinding = metavariable * constr * instance_status
 
 let retract_coercible_metas evd =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2fd6680435..825096acca 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,7 +218,6 @@ val meta_declare   :
   metavariable -> types -> ?name:name -> evar_defs -> evar_defs
 val meta_assign    : metavariable -> constr * instance_status -> evar_defs -> evar_defs
 val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> evar_defs
-val mk_meta_subst  : evar_defs -> meta_value_map
 
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
@@ -226,7 +225,6 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs
 val undefined_metas : evar_defs -> metavariable list
 val metas_of : evar_defs -> meta_type_map
 val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
-val replace_metas : clbinding Metamap.t -> evar_defs -> evar_defs
 
 type metabinding = metavariable * constr * instance_status
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7fdcded009..e24cf62bb1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -887,19 +887,28 @@ let meta_value evd mv =
   in 
   valrec mv
 
-let meta_instance evd b =
+let meta_instance env b =
   let c_sigma =
     List.map 
-      (fun mv -> (mv,meta_value evd mv)) (Metaset.elements b.freemetas)
+      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
   in 
   if c_sigma = [] then b.rebus else instance c_sigma b.rebus
 
-let nf_meta evd c = meta_instance evd (mk_freelisted c)
-
-let direct_nf_meta evd c = instance (mk_meta_subst evd) c
+let nf_meta env c = meta_instance env (mk_freelisted c)
 
 (* Instantiate metas that create beta/iota redexes *)
 
+let meta_value evd mv = 
+  let rec valrec mv =
+    match meta_opt_fvalue evd mv with
+    | Some (b,_) ->
+      instance
+        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+        b.rebus
+    | None -> mkMeta mv
+  in 
+  valrec mv
+
 let meta_reducible_instance evd b =
   let fm = Metaset.elements b.freemetas in
   let metas = List.fold_left (fun l mv -> 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3973774731..371a66a9d5 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -223,5 +223,4 @@ val whd_betaiota_deltazeta_for_iota_state :  state_reduction_function
 (*s Meta-related reduction functions *)
 val meta_instance : evar_defs -> constr freelisted -> constr
 val nf_meta       : evar_defs -> constr -> constr
-val direct_nf_meta       : evar_defs -> constr -> constr
 val meta_reducible_instance : evar_defs -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a18db9026b..a2671b5d11 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -467,7 +467,7 @@ let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
-  let t = Tacred.hnf_constr env sigma (nf_meta evd t) in
+  let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul flags t u
   with e when precatchable_exception e -> ([],[])