Suite restructuration unification et division des problèmes

d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).



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

7 files changed, 83 insertions, 41 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 3386f45f51..5f9a3ff93d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -388,7 +388,9 @@ let destApplication = destApp
 
 let isApp c = match kind_of_term c with App _ -> true | _ -> false
 
-let isProd c = match kind_of_term c with | Prod(_) -> true | _ -> false
+let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
+
+let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
 
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index 4133ca8920..fcae3341e4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -234,6 +234,7 @@ val isMeta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
 val isApp : constr -> bool
+val isLambda : constr -> bool
 val isProd : constr -> bool
 val isConst : constr -> bool
 val isConstruct : constr -> bool
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 96facdef2a..cfecbf3191 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -383,6 +383,32 @@ let error_already_defined b =
         anomalylabstrm ""
           (str "Position " ++ int n ++ str" already defined")
 
+let rec similar_type_shapes t u =
+  let t,_ = decompose_app t and u,_ = decompose_app u in
+  match kind_of_term t, kind_of_term u with
+  | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2
+  | Const cst, Const cst' -> cst = cst'
+  | Var id, Var id' -> id = id'
+  | Ind ind, Ind ind' -> ind = ind'
+  | Rel n, Rel n' -> n = n'
+  | Sort s, Sort s' -> family_of_sort s = family_of_sort s'
+  | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c'
+  | _ -> false
+
+let clenv_unify_similar_types clenv t u =
+  if similar_type_shapes t u then 
+    try Processed, clenv_unify true CUMUL t u clenv 
+    with e when precatchable_exception e -> Coercible t, clenv
+  else Coercible t, clenv
+
+let clenv_assign_binding clenv k (sigma,c) =
+  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+  let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
+  let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
+  let status,clenv'' = clenv_unify_similar_types clenv' c_typ k_typ in
+(*  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*)
+  { clenv'' with evd = meta_assign k (c,status) clenv''.evd }
+
 let clenv_match_args bl clenv =
   if bl = [] then
     clenv
@@ -390,25 +416,15 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,b,(sigma,c)) ->
+      (fun clenv (loc,b,(sigma,c as sc)) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  let c_typ = nf_betaiota (clenv_get_type_of clenv c) in
-	  let c_typ = clenv_hnf_constr clenv c_typ in
-	  let clenv = { clenv with evd = evar_merge clenv.evd sigma} in
-	  {clenv with evd = meta_assign k (c,Coercible c_typ) clenv.evd})
+	  clenv_assign_binding clenv k sc)
       clenv bl
 
-let clenv_assign_binding clenv k (sigma,c) =
-  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-  let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
-  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
-  { clenv' with evd = meta_assign k (c',Coercible c_typ) evd }
-
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
   let k =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ebd635b807..7b5690e2cc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -335,7 +335,8 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
 *)
 
 type instance_status =
-    IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
+  | IsSuperType | IsSubType
+  | ConvUpToEta of int | Coercible of types | Processed
 
 (* Clausal environments *)
 
@@ -538,13 +539,13 @@ let meta_merge evd1 evd2 =
 
 type metabinding = metavariable * constr * instance_status
 
-let retract_defined_metas evd =
+let retract_coercible_metas evd =
   let mc,ml = 
     Metamap.fold (fun n v (mc,ml) -> 
       match v with
-	| Clval (na,(b,s),typ) ->
+	| Clval (na,(b,s),typ) when s <> Processed ->
 	    (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
-	| Cltyp _ as v ->
+	| v ->
 	    mc, Metamap.add n v ml)
       evd.metas ([],Metamap.empty) in
   mc, { evd with metas = ml }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 784e066b71..b6ffd02c12 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -112,7 +112,8 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 *)
 
 type instance_status =
-    IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
+  | IsSuperType | IsSubType
+  | ConvUpToEta of int | Coercible of types | Processed
 
 type clbinding =
   | Cltyp of name * constr freelisted
@@ -180,7 +181,7 @@ val metas_of : evar_defs -> metamap
 
 type metabinding = metavariable * constr * instance_status
 
-val retract_defined_metas : evar_defs -> metabinding list * evar_defs
+val retract_coercible_metas : evar_defs -> metabinding list * evar_defs
 val subst_defined_metas : metabinding list -> constr -> constr option
 
 (**********************************************************)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3e9b08beb4..7f05b1cbfa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -882,28 +882,49 @@ let nf_meta env c = meta_instance env (mk_freelisted c)
 
 (* Instantiate metas that create beta/iota redexes *)
 
-let meta_reducible_instance env b =
-  let s =
-    List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+let meta_value evd mv = 
+  let rec valrec mv =
+    try
+      let b,_ = meta_fvalue evd mv in
+      instance
+        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+        b.rebus
+    with Anomaly _ | Not_found -> 
+      mkMeta mv
   in 
+  valrec mv
+
+let meta_reducible_instance evd b =
+  let fm = Metaset.elements b.freemetas in
+  let s = List.fold_left (fun l mv -> 
+    try let g,s = meta_fvalue evd mv in (mv,(g.rebus,s))::l 
+    with Anomaly _ | Not_found -> l) [] fm in 
   let rec irec u =
     let u = whd_betaiota u in
     match kind_of_term u with
     | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
-        let bl' = Array.map irec bl in
-        let p' = irec p in
 	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
-	let g = List.assoc m s in
-	(match kind_of_term g with
-           | Construct _ -> whd_betaiota (mkCase (ci,p',g,bl'))
-           | _ -> mkCase (ci,p',c,bl'))
+	(match
+	  try
+	    let g,s = List.assoc m s in
+	    if isConstruct g or s = Processed then Some g else None
+	  with Not_found -> None
+	  with
+	    | Some g -> irec (mkCase (ci,p,g,bl))
+	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
     | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
-        let l' = Array.map irec l in
 	let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
-	let g = List.assoc m s in
-	(match kind_of_term g with
-           | Lambda _ -> beta_appvect g l'
-           | _ -> mkApp (f,l'))
+	(match
+	  try
+	    let g,s = List.assoc m s in
+	    if isLambda g or s = Processed then Some g else None
+	  with Not_found -> None
+	  with
+	    | Some g -> irec (mkApp (g,l))
+	    | None -> mkApp (f,Array.map irec l))
+    | Meta m ->
+	(try let g,s = List.assoc m s in if s = Processed then irec g else u
+	with Not_found -> u)
     | _ -> map_constr irec u
   in 
-  if s = [] then b.rebus else irec b.rebus
+  if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e296737f25..bd6fb5ad88 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -65,7 +65,7 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
 let opp_status = function
   | IsSuperType -> IsSubType
   | IsSubType -> IsSuperType
-  | ConvUpToEta _ | Coercible _ as x -> x
+  | ConvUpToEta _ | Coercible _ | Processed as x -> x
 
 let extract_instance_status = function
   | Cumul -> (IsSubType,IsSuperType)
@@ -231,13 +231,13 @@ let merge_instances env sigma mod_delta st1 st2 c1 c2 =
   | (ConvUpToEta n1, ConvUpToEta n2) ->
       let side = left (* arbitrary choice, but agrees with compatibility *) in
       unify_with_eta side mod_delta env sigma n1 n2 c1 c2
-  | ((IsSubType | ConvUpToEta _ | Coercible _ as oppst1),
-     (IsSubType | ConvUpToEta _ | Coercible _)) ->
+  | ((IsSubType | ConvUpToEta _ | Coercible _ | Processed as oppst1),
+     (IsSubType | ConvUpToEta _ | Coercible _ | Processed)) ->
       let res = unify_0 env sigma Cumul mod_delta c2 c1 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else (st2=IsSubType, ConvUpToEta 0, res)
-  | ((IsSuperType | ConvUpToEta _ | Coercible _ as oppst1),
-     (IsSuperType | ConvUpToEta _ | Coercible _)) ->
+  | ((IsSuperType | ConvUpToEta _ | Coercible _ | Processed as oppst1),
+     (IsSuperType | ConvUpToEta _ | Coercible _ | Processed)) ->
       let res = unify_0 env sigma Cumul mod_delta c1 c2 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else (st2=IsSuperType, ConvUpToEta 0, res)
@@ -379,7 +379,7 @@ let w_merge env with_types mod_delta metas evars evd =
     	  else
 	    begin
 	      let evd,n =
-		if with_types (* or occur_meta mvty *) then
+		if with_types & status <> Processed then
                   let sigma = evars_of evd in
 		  let metas = metas_of evd in
 	          let mvty = Typing.meta_type evd mv in
@@ -439,7 +439,7 @@ let w_merge env with_types mod_delta metas evars evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let w_unify_core_0 env with_types cv_pb mod_delta m n evd =
-  let (mc1,evd') = retract_defined_metas evd in
+  let (mc1,evd') = retract_coercible_metas evd in
   let (mc2,ec) = 
     unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in 
   w_merge env with_types mod_delta mc2 ec evd'