Optimisation de clenv.ml pour que meta_instance ne soit pas appelé

abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.



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

10 files changed, 118 insertions, 62 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 732ff1e69b..c5c246877d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -54,11 +54,77 @@ 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
 
@@ -68,7 +134,8 @@ 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_type cl) in
+  let typ =
+    whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_direct_nf_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -213,13 +280,9 @@ 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 (clenv_metavars clenv.evd mv))
+    (fun mv deps -> Metaset.union deps (meta_ftype clenv.evd mv).freemetas)
     mvs conclmetas
 
 let duplicated_metas c = 
@@ -231,14 +294,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 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
+  let deps = dependent_metas clenv mvs typ.freemetas in
+  let nonlinear = duplicated_metas body.rebus in
   (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
     (fun mv -> (Metaset.mem mv deps &&
-                not (hyps_only && Metaset.mem mv ctyp_mvs))
+                not (hyps_only && Metaset.mem mv typ.freemetas))
                or List.mem mv nonlinear) 
     mvs
 
@@ -367,9 +430,9 @@ type arg_bindings = open_constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  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
+  let (body,typ) = instantiated_clenv_template clenv in
+  let mvs = Metaset.elements body.freemetas in
+  let deps = dependent_metas clenv mvs typ.freemetas 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 dfa7513495..de5a1e3758 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -43,10 +43,16 @@ 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
 
@@ -83,6 +89,8 @@ 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 b29afc0cb3..2b9a0ed82d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -610,12 +610,18 @@ 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 38db90dad4..2fd6680435 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,13 +218,15 @@ 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
 
 val undefined_metas : evar_defs -> metavariable list
-val metas_of : evar_defs -> metamap
+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 57af582a1c..e3553ddd6d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -130,15 +130,15 @@ type local_state_reduction_function = state -> state
 (*** Reduction Functions Operators ***)
 (*************************************)
 
-let rec whd_state (x, stack as s) =
+let rec whd_app_state (x, stack as s) =
   match kind_of_term x with
-    | App (f,cl) -> whd_state (f, append_stack cl stack)
-    | Cast (c,_,_)  -> whd_state (c, stack)
+    | App (f,cl) -> whd_app_state (f, append_stack cl stack)
+    | Cast (c,_,_)  -> whd_app_state (c, stack)
     | _             -> s
 
 let appterm_of_stack (f,s) = (f,list_of_stack s)
 
-let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_stack x = appterm_of_stack (whd_app_state (x, empty_stack))
 let whd_castapp_stack = whd_stack
 
 let stack_reduction_of_reduction red_fun env sigma s =
@@ -185,26 +185,6 @@ module type RedFlagsSig = sig
   val red_zeta : flags -> bool
 end
 
-(* Naive Implementation 
-module RedFlags = (struct
-  type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
-  type flags = flag list
-  let fbeta = BETA 
-  let fdelta = DELTA
-  let fevar = EVAR
-  let fiota = IOTA
-  let fzeta = ZETA
-  let feta = ETA
-  let mkflags l = l
-  let red_beta = List.mem BETA
-  let red_delta = List.mem DELTA
-  let red_evar = List.mem EVAR
-  let red_eta = List.mem ETA
-  let red_iota = List.mem IOTA
-  let red_zeta = List.mem ZETA
-end : RedFlagsSig)
-*)
-
 (* Compact Implementation *)
 module RedFlags = (struct
   type flag = int
@@ -531,14 +511,14 @@ let rec whd_evar sigma c =
 	  with NotInstantiatedEvar | Not_found -> None in
 	(match d with Some c -> whd_evar sigma c | None -> c)
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
-    | _ -> collapse_appl c
+    | _ -> c
 
 let nf_evar sigma =
   local_strong (whd_evar sigma)
 
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =
-  norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+  norm_val (create_clos_infos flgs env) (inject ((*nf_evar sigma *)t))
 
 let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
 let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
@@ -645,8 +625,8 @@ let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_l
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta metamap c = match kind_of_term c with
-  | Meta p -> (try List.assoc p metamap with Not_found -> c)
+let whd_meta metasubst c = match kind_of_term c with
+  | Meta p -> (try List.assoc p metasubst with Not_found -> c)
   | _ -> c
 
 (* Try to replace all metas. Does not replace metas in the metas' values
@@ -905,27 +885,18 @@ let meta_value evd mv =
   in 
   valrec mv
 
-let meta_instance env b =
+let meta_instance evd b =
   let c_sigma =
     List.map 
-      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+      (fun mv -> (mv,meta_value evd mv)) (Metaset.elements b.freemetas)
   in 
   if c_sigma = [] then b.rebus else instance c_sigma b.rebus
 
-let nf_meta env c = meta_instance env (mk_freelisted c)
+let nf_meta evd c = meta_instance evd (mk_freelisted c)
 
-(* Instantiate metas that create beta/iota redexes *)
+let direct_nf_meta evd c = instance (mk_meta_subst evd) c
 
-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
+(* Instantiate metas that create beta/iota redexes *)
 
 let meta_reducible_instance evd b =
   let fm = Metaset.elements b.freemetas in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 371a66a9d5..3973774731 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -223,4 +223,5 @@ 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/retyping.mli b/pretyping/retyping.mli
index c7901e9498..52e5d7049e 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -26,7 +26,7 @@ val get_sort_of : env -> evar_map -> types -> sorts
 val get_sort_family_of : env -> evar_map -> types -> sorts_family
 
 val get_type_of_with_meta :
-  env -> evar_map -> Termops.metamap -> constr -> types
+  env -> evar_map -> Termops.meta_type_map -> constr -> types
 
 (* Makes an assumption from a constr *)
 val get_assumption_of : env -> evar_map -> constr -> types
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 7cbde2d07b..a77fc57413 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -555,7 +555,9 @@ let pop t = lift (-1) t
 (*  bindings functions *)                         
 (***************************)
 
-type metamap = (metavariable * constr) list 
+type meta_type_map = (metavariable * types) list 
+
+type meta_value_map = (metavariable * constr) list 
 
 let rec subst_meta bl c = 
   match kind_of_term c with
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 15751b91c0..e9516ec486 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -105,8 +105,11 @@ val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val collect_metas : constr -> int list
 (* Substitution of metavariables *)
-type metamap = (metavariable * constr) list 
-val subst_meta : metamap -> constr -> constr
+type meta_value_map = (metavariable * constr) list 
+val subst_meta : meta_value_map -> constr -> constr
+
+(* Type assignment for metavariables *)
+type meta_type_map = (metavariable * types) list 
 
 (* [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a2671b5d11..a18db9026b 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_betaiota (nf_meta evd t)) in
+  let t = Tacred.hnf_constr env sigma (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 -> ([],[])