- modifs de la condition de garde pour mieux tenir compte des raisonnements

  par l'absurde
- un open_constr est maintenant un terme accompagne du sigma dans lequel il
  est typable (il manquait l'info concernant le contexte de typage des
  nouvelles evars)


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

8 files changed, 148 insertions, 132 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e78e9fd81c..c7f1fc2ed7 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -198,19 +198,23 @@ let (automatic : tactic) =
  * Vernac: Correctness <string> <program> [; <tactic>].
  *)
 
-let reduce_open_constr (em,c) =
+let reduce_open_constr (em0,c) =
   let existential_map_of_constr = 
     let rec collect em c = match kind_of_term c with
       | Cast (c',t) -> 
 	  (match kind_of_term c' with
-	     | Evar ev -> (ev,t) :: em
+	     | Evar (ev,_) ->
+                 if not (Evd.in_dom em ev) then
+                   Evd.add em ev (Evd.map em0 ev)
+                 else
+                   em
 	     | _ -> fold_constr collect em c)
       | Evar _ -> 
 	  assert false (* all existentials should be casted *)
       | _ -> 
 	  fold_constr collect em c
     in
-    collect []
+    collect Evd.empty
   in
   let c = Pred.red_cci c in
   let em = existential_map_of_constr c in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c98e222a00..eaf6f06c25 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -297,6 +297,33 @@ exception FixGuardError of guard_error
    Below are functions to handle such environment.
  *)
 type size = Large | Strict
+
+let size_glb s1 s2 =
+  match s1,s2 with
+      Strict, Strict -> Strict
+    | _ -> Large
+
+type subterm_spec =
+    Subterm of (size * wf_paths)
+  | Dead_code
+  | Not_subterm
+
+let spec_of_tree t =
+  if t=mk_norec then Not_subterm else Subterm(Strict,t)
+
+let subterm_spec_glb =
+  let glb2 s1 s2 =
+    match s1,s2 with
+        _, Dead_code -> s1
+      | Dead_code, _ -> s2
+      | Not_subterm, _ -> Not_subterm
+      | _, Not_subterm -> Not_subterm
+      | Subterm (a1,t1), Subterm (a2,t2) ->
+          if t1=t2 then Subterm (size_glb a1 a2, t1)
+          (* branches do not return objects with same spec *)
+          else Not_subterm in
+  Array.fold_left glb2 Dead_code
+          
 type guard_env =
   { env     : env;
     (* dB of last fixpoint *)
@@ -306,55 +333,53 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : (int * (size * wf_paths)) list;
+    genv    : subterm_spec list;
   }
 
-let make_renv env minds recarg (_,tyi as ind) =
-  let (mib,mip) = lookup_mind_specif env ind in
+let make_renv env minds recarg (sp,tyi) =
+  let mib = Environ.lookup_mind sp env in
   let mind_recvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
-  let lcx = mind_recvec.(tyi)  in
   { env = env;
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    genv = [(1,(Large,mind_recvec.(tyi)))] }
+    genv = [Subterm(Large,mind_recvec.(tyi))] }
 
-let map_lift_fst_n m = List.map (function (n,t)->(n+m,t))
-
-let push_var_renv renv (x,ty) =
+let push_var renv (x,ty,spec) =
   { renv with 
     env = push_rel (x,None,ty) renv.env;
     rel_min = renv.rel_min+1;
-    genv = map_lift_fst_n 1 renv.genv }
+    genv = spec:: renv.genv }
+
+let assign_var_spec renv (i,spec) =
+  { renv with genv = list_assign renv.genv (i-1) spec }
+
+let push_var_renv renv (x,ty) =
+  push_var renv (x,ty,Not_subterm)
+
+(* Fetch recursive information about a variable p *)
+let subterm_var p renv = 
+  try List.nth renv.genv (p-1)
+  with Failure _ | Invalid_argument _ -> Not_subterm
+
+(* Add a variable and mark it as strictly smaller with information [spec]. *)
+let add_subterm renv (x,a,spec) =
+  push_var renv (x,a,spec_of_tree spec)
 
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { renv with 
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = map_lift_fst_n n renv.genv }
+    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { renv with
     env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = map_lift_fst_n n renv.genv }
-
-(* Add a variable and mark it as strictly smaller with information [spec]. *)
-let add_recarg renv (x,a,spec) =
-  let renv' = push_var_renv renv (x,a) in
-  if spec = mk_norec then renv'
-  else { renv' with genv = (1,(Strict,spec))::renv'.genv }
-
-(* Fetch recursive information about a variable *)
-let subterm_var p renv = 
-  let rec findrec = function 
-    | (a,ta)::l -> 
-        if a < p then findrec l else if a = p then Some ta else None
-    | _ -> None in
-  findrec renv.genv
+    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
 
 
 (******************************)
@@ -376,21 +401,6 @@ let lookup_subterms env ind =
   let (_,mip) = lookup_mind_specif env ind in
   mip.mind_recargs
 
-
-let case_branches_specif renv spec lc = 
-  let rec crec renv lrec c = 
-    let c' = strip_outer_cast c in 
-    match lrec, kind_of_term c' with 
-      |	(ra::lr,Lambda (x,a,b)) ->
-          let renv' = add_recarg renv (x,a,ra) in
-          crec renv' lr b
-      | (_,LetIn (x,c,a,b)) -> crec renv lrec (subst1 c b)
-      (* Rq: if branch is not eta-long, then the recursive information
-         is not propagated: *)
-      | (_,_) -> (renv,c') in
-  if spec = mk_norec then Array.map (fun c -> (renv,c)) lc
-  else array_map2 (crec renv) (dest_subterms spec) lc
-
 (*********************************)
 
 (* finds the inductive type of the recursive argument of a fixpoint *)
@@ -416,27 +426,20 @@ let inductive_of_fix env recarg body =
    - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta) 
    - [None] otherwise
 *)
+
 let rec subterm_specif renv t ind = 
   let f,l = decompose_app (whd_betadeltaiota renv.env t) in
   match kind_of_term f with 
     | Rel k -> subterm_var k renv
 
     | Case (ci,_,c,lbr) ->
-        if Array.length lbr = 0
-        (* New: if it is built by contadiction, it is OK *)
-        then Some (Strict,mk_norec)
+        if Array.length lbr = 0 then Dead_code
         else
-          let lcv =
-            match subterm_specif renv c ci.ci_ind with
-                Some (_,lr) -> lr
-              | None -> mk_norec in 
-          let lbr' = case_branches_specif renv lcv lbr in
+          let lbr_spec = case_branches_specif renv c ci.ci_ind lbr in
           let stl  =
-            Array.map (fun (renv',br') -> subterm_specif renv' br' ind) lbr' in
-          let stl0 = stl.(0) in
-	  if array_for_all (fun st -> st=stl0) stl then stl0 
-          (* branches do not return objects with same spec *)
-          else None
+            Array.map (fun (renv',br') -> subterm_specif renv' br' ind)
+              lbr_spec in
+          subterm_spec_glb stl
 	       
     | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
 (* when proving that the fixpoint f(x)=e is less than n, it is enough
@@ -449,7 +452,7 @@ let rec subterm_specif renv t ind =
         (* pushing the fixpoints *)
         let renv' = push_fix_renv renv recdef in
         let renv' =
-          { renv' with genv=(nbfix-i,(Strict,recargs))::renv'.genv } in
+          assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
         let decrArg = recindxs.(i) in 
         let theBody = bodies.(i)   in
         let nbOfAbst = decrArg+1 in
@@ -457,19 +460,12 @@ let rec subterm_specif renv t ind =
         (* pushing the fix parameters *)
         let renv'' = push_ctxt_renv renv' sign in
         let renv'' =
-          { renv'' with
-            genv =
-              if List.length l < nbOfAbst then renv''.genv
-              else
-                let decrarg_ind =
-                  inductive_of_fix renv''.env decrArg theBody in
-                let theDecrArg  = List.nth l decrArg in
-	        try 
-	          match subterm_specif renv theDecrArg decrarg_ind with 
-		      (Some recArgsDecrArg) ->
-                        (1,recArgsDecrArg) :: renv''.genv 
-                    | None -> renv''.genv
-	        with Not_found -> renv''.genv } in
+          if List.length l < nbOfAbst then renv''
+          else
+            let decrarg_ind = inductive_of_fix renv''.env decrArg theBody in
+            let theDecrArg  = List.nth l decrArg in
+	    let arg_spec    = subterm_specif renv theDecrArg decrarg_ind in
+            assign_var_spec renv'' (1, arg_spec) in
 	subterm_specif renv'' strippedBody ind
 	    
     | Lambda (x,a,b) -> 
@@ -477,22 +473,40 @@ let rec subterm_specif renv t ind =
         subterm_specif (push_var_renv renv (x,a)) b ind
 
     (* A term with metas is considered OK *)
-    | Meta _ -> Some (Strict,lookup_subterms renv.env ind)
+    | Meta _ -> Dead_code
     (* Other terms are not subterms *)
-    | _ -> None
+    | _ -> Not_subterm
 
 (* Propagation of size information through Cases: if the matched
    object is a recursive subterm then compute the information
-   associated to its own subterms. *)
-let spec_subterm_large renv c ind = 
-  match subterm_specif renv c ind with
-    Some (_,lr) -> lr
-  | None -> mk_norec
+   associated to its own subterms.
+   Rq: if branch is not eta-long, then the recursive information
+   is not propagated *)
+and case_branches_specif renv c ind lbr = 
+  let c_spec = subterm_specif renv c ind in
+  let rec push_branch_args renv lrec c = 
+    let c' = strip_outer_cast (whd_betadeltaiota renv.env c) in 
+    match lrec, kind_of_term c' with 
+      |	(ra::lr,Lambda (x,a,b)) ->
+          let renv' = push_var renv (x,a,ra) in
+          push_branch_args renv' lr b
+      | (_,_) -> (renv,c') in
+  match c_spec with
+      Subterm (_,t) ->
+        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
+        assert (Array.length sub_spec = Array.length lbr);
+        array_map2 (push_branch_args renv) sub_spec lbr
+    | Dead_code -> 
+        let t = dest_subterms (lookup_subterms renv.env ind) in
+        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
+        assert (Array.length sub_spec = Array.length lbr);
+        array_map2 (push_branch_args renv) sub_spec lbr
+    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
 
 (* Check term c can be applied to one of the mutual fixpoints. *)
 let check_is_subterm renv c ind = 
   match subterm_specif renv c ind with
-    Some (Strict,_) -> ()
+    Subterm (Strict,_) | Dead_code -> ()
   |  _ -> raise (FixGuardError RecursionOnIllegalTerm)
 
 (***********************************************************************)
@@ -527,12 +541,11 @@ let check_one_fix renv recpos def =
 	  else List.for_all (check_rec_call renv) l        
 
       | Case (ci,p,c_0,lrest) ->
-            (* compute the recarg information for the arguments of
-               each branch *)
-            let lc  = spec_subterm_large renv c_0 ci.ci_ind in
-            let lbr = case_branches_specif renv lc lrest in
-            array_for_all (fun (renv',br') -> check_rec_call renv' br') lbr
-	    && List.for_all (check_rec_call renv) (c_0::p::l)
+          List.for_all (check_rec_call renv) (c_0::p::l) &&
+          (* compute the recarg information for the arguments of
+             each branch *)
+          let lbr = case_branches_specif renv c_0 ci.ci_ind lrest in
+          array_for_all (fun (renv',br') -> check_rec_call renv' br') lbr
 
   (* Enables to traverse Fixpoint definitions in a more intelligent
      way, ie, the rule :
@@ -554,20 +567,23 @@ let check_one_fix renv recpos def =
           array_for_all (check_rec_call renv) typarray && 
 	  let nbfix = Array.length typarray in
           let decrArg = recindxs.(i) in
-	  let theBody = bodies.(i)   in
           let renv' = push_fix_renv renv recdef in 
           if (List.length l < (decrArg+1)) then
 	    array_for_all (check_rec_call renv') bodies
           else 
-            let decrarg_ind = inductive_of_fix renv'.env decrArg theBody in
-            let theDecrArg  = List.nth l decrArg in
-	    (try 
-	      match subterm_specif renv theDecrArg decrarg_ind with
-                  Some recArgsDecrArg -> 
-		    check_nested_fix_body renv'
-                      (decrArg+1) recArgsDecrArg theBody
-		| None -> array_for_all (check_rec_call renv') bodies
-	     with Not_found -> array_for_all (check_rec_call renv') bodies)
+            let ok_vect =
+              Array.mapi
+                (fun j body ->
+                  if i=j then
+                    let decrarg_ind =
+                      inductive_of_fix renv'.env decrArg body in
+                    let theDecrArg  = List.nth l decrArg in
+	            let arg_spec =
+                      subterm_specif renv theDecrArg decrarg_ind in
+	            check_nested_fix_body renv' (decrArg+1) arg_spec body
+                  else check_rec_call renv' body)
+                bodies in
+            array_for_all (fun b -> b) ok_vect
 
       | Const sp as c -> 
           (try List.for_all (check_rec_call renv) l
@@ -610,14 +626,13 @@ let check_one_fix renv recpos def =
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
-      check_rec_call
-        { renv with genv=(1,recArgsDecrArg)::renv.genv } body
+      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
     else
       match kind_of_term body with
 	| Lambda (x,a,b) ->
+            let renv' = push_var_renv renv (x,a) in
 	    check_rec_call renv a &&
-	    check_nested_fix_body (push_var_renv renv (x,a))
-              (decr-1) recArgsDecrArg b
+	    check_nested_fix_body renv' (decr-1) recArgsDecrArg b
 	| _ -> anomaly "Not enough abstractions in fix body"
     
   in
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 2f40f0b28d..6edb387bcb 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -33,10 +33,9 @@ val interp_sort          : Coqast.t -> sorts
 val interp_elimination_sort : Coqast.t -> sorts_family
 
 val interp_openconstr    :
-  evar_map -> env -> Coqast.t -> (existential * constr) list * constr
+  evar_map -> env -> Coqast.t -> evar_map * constr
 val interp_casted_openconstr    :
-  evar_map -> env -> Coqast.t -> constr ->
-    (existential * constr) list * constr
+  evar_map -> env -> Coqast.t -> constr -> evar_map * constr
 
 (* [interp_type_with_implicits] extends [interp_type] by allowing
    implicits arguments in the ``rel'' part of [env]; the extra
@@ -61,7 +60,7 @@ val interp_constr_gen     :
 val interp_openconstr_gen     :
   evar_map -> env -> (identifier * constr) list ->
     (int * constr) list -> Coqast.t -> constr option
-      -> (existential * constr) list * constr
+      -> evar_map * constr
 
 (*Interprets constr patterns according to a list of instantiations
   (variables)*)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1d69a14ae9..a18b5499c5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -472,7 +472,6 @@ let unsafe_infer_type valcon isevars env lvar lmeta constr =
 (* assumes the defined existentials have been replaced in c (should be
    done in unsafe_infer and unsafe_infer_type) *)
 let check_evars fail_evar initial_sigma sigma c =
-  let metamap = ref [] in
   let rec proc_rec c =
     match kind_of_term c with
       | Evar (ev,args as k) ->
@@ -480,14 +479,10 @@ let check_evars fail_evar initial_sigma sigma c =
 	  if not (Evd.in_dom initial_sigma ev) then
 	    (if fail_evar then
 	      errorlabstrm "whd_ise"
-		(str"There is an unknown subterm I cannot solve")
-	    else (* try to avoid duplication *)
-              (if not (List.exists (fun (k',_) -> k=k') !metamap) then
-	        metamap :=
-                (k, nf_evar sigma (existential_type sigma k)) :: !metamap))
+		(str"There is an unknown subterm I cannot solve"))
       | _ -> iter_constr proc_rec c      
   in
-  (proc_rec c; !metamap)
+  proc_rec c
 
 (* TODO: comment faire remonter l'information si le typage a resolu des
        variables du sigma original. il faudrait que la fonction de typage
@@ -495,15 +490,14 @@ let check_evars fail_evar initial_sigma sigma c =
 *)
 
 (* constr with holes *)
-type open_constr = (existential * types) list * constr
+type open_constr = evar_map * constr
 
 let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let isevars = create_evar_defs sigma in
   let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
-  let metamap =
-    check_evars fail_evar sigma (evars_of isevars)
-      (mkCast(j.uj_val,j.uj_type)) in
-  (metamap, j)
+  let new_sigma = evars_of isevars in
+  check_evars fail_evar sigma new_sigma (mkCast(j.uj_val,j.uj_type));
+  (new_sigma, j)
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env [] [] typ c
@@ -515,17 +509,16 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
   let isevars = create_evar_defs sigma in
   let j = unsafe_infer tycon isevars env lvar lmeta c in
-  let metamap =
-    check_evars fail_evar sigma (evars_of isevars)
-      (mkCast(j.uj_val,j.uj_type)) in
-  (metamap, j)
+  let new_sigma = evars_of isevars in
+  check_evars fail_evar sigma new_sigma (mkCast(j.uj_val,j.uj_type));
+  (new_sigma, j)
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
   let isevars = create_evar_defs sigma in
   let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
-  let metamap =
-    check_evars fail_evar sigma (evars_of isevars) tj.utj_val in
-  (metamap, tj)
+  let new_sigma = evars_of isevars in
+  check_evars fail_evar sigma new_sigma tj.utj_val;
+  (new_sigma, tj)
 
 type meta_map = (int * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 91a8da2c77..e76c6c14fa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ type meta_map = (int * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
 
 (* constr with holes *)
-type open_constr = (existential * types) list * constr
+type open_constr = evar_map * constr
 
 
 (* Generic call to the interpreter from rawconstr to constr, failing
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 67de8df987..465e7cc7a6 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -53,17 +53,21 @@ let meta_ctr=ref 0;;
 let new_meta ()=incr meta_ctr;!meta_ctr;;
 
 (* replaces a mapping of existentials into a mapping of metas. *)
-let exist_to_meta (emap, c) =
+let exist_to_meta sigma (emap, c) =
   let subst = ref [] in
   let mmap = ref [] in
-  let add_binding (e,ty) =
-    let n = new_meta() in
-    subst := (e, mkMeta n) :: !subst;
-    mmap := (n, ty) :: !mmap in
-  List.iter add_binding emap;
+  let add_binding (e,ev_decl) =
+    if not (Evd.in_dom sigma e) then begin
+      let n = new_meta() in
+      subst := (e, mkMeta n) :: !subst;
+      mmap := (n, ev_decl.evar_concl) :: !mmap
+    end in
+  List.iter add_binding (Evd.to_list emap);
   let rec replace c =
     match kind_of_term c with
-        Evar k -> List.assoc k !subst
+        Evar (k,_) ->
+          (try List.assoc k !subst
+          with Not_found -> c)
       | _ -> map_constr replace c in
   (!mmap, replace c)
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 162698112c..5968199359 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -24,8 +24,8 @@ val new_meta : unit -> int
 (* [exist_to_meta] generates new metavariables for each existential
    and performs the replacement in the given constr *)
 val exist_to_meta :
-  ((existential * constr) list * constr) ->
-  ((int * constr) list * constr)
+  Evd.evar_map -> (Evd.evar_map * constr) ->
+  ((int * types) list * constr)
 
 (* The Type of Constructions clausale environments. *)
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index ddddd21d88..a942b37b71 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -334,8 +334,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 (* Et finalement la tactique refine elle-même : *)
 
 let refine oc gl =
+  let sigma = project gl in
   let env = pf_env gl in
-  let (gmm,c) = Clenv.exist_to_meta oc in
+  let (gmm,c) = Clenv.exist_to_meta sigma oc in
   let th = compute_metamap env gmm c in
   tcc_aux th gl