Debug wellfounded defs, work on cleaning obls envs

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

8 files changed, 106 insertions, 56 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 1844fea55..33b140f61 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -11,6 +11,7 @@ open Evd
 open List
 open Pp
 open Util
+open Subtac_utils
 
 let reverse_array arr = 
   Array.of_list (List.rev (Array.to_list arr))
@@ -32,6 +33,14 @@ let list_assoc_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
+let rec list_split_at n l = 
+  match n with
+    | 0 -> ([], l)
+    | n' ->
+	match l with
+	  | [] -> assert(false)
+	  | hd :: tl -> let (l, r) = list_split_at (pred n') tl in
+	      (hd :: l, r)
 
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
@@ -46,17 +55,19 @@ let subst_evar_constr evs n t =
   in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
-	let (id, idstr), hyps, _, _ = 
+	let (id, idstr), hyps, chop, _, _ = 
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
 	in
         seen := Intset.add id !seen;
-(* 	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ *)
-(* 			int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () ); *)
 	  (* Evar arguments are created in inverse order, 
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
+	let args = 
+	  let (l, r) = list_split_at chop (Array.to_list args) in
+	    r
+	in
 	let args =
 	  let rec aux hyps args acc =
 	     match hyps, args with
@@ -66,9 +77,13 @@ let subst_evar_constr evs n t =
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
-	   in aux hyps (Array.to_list args) [] 
-	 in
-	   mkApp (mkVar idstr, Array.of_list args)
+	  in aux hyps args [] 
+	in
+  	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++
+			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
+			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
+ 	   with _ -> ());
+	  mkApp (mkVar idstr, Array.of_list args)
     | _ -> map_constr_with_binders succ substrec depth c
   in 
   let t' = substrec 0 t in
@@ -92,7 +107,7 @@ let subst_vars acc n t =
   to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
 *)
-let etype_of_evar evs ev hyps =
+let etype_of_evar evs hyps concl =
   let rec aux acc n = function
       (id, copt, t) :: tl ->
 	let t', s = subst_evar_constr evs n t in
@@ -108,7 +123,7 @@ let etype_of_evar evs ev hyps =
  	let rest, s' = aux (id :: acc) (succ n) tl in
 	  mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s
     | [] ->
-	let t', s = subst_evar_constr evs n ev.evar_concl in
+	let t', s = subst_evar_constr evs n concl in
 	  subst_vars acc 0 t', s
   in aux [] 0 (rev hyps)
 
@@ -122,7 +137,14 @@ let trunc_named_context n ctx =
   let len = List.length ctx in
     take (len - n) ctx
   
-let eterm_obligations name nclen evm t tycon = 
+let rec chop_product n t = 
+  if n = 0 then Some t
+  else 
+    match kind_of_term t with
+      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
+      | _ -> None
+
+let eterm_obligations name nclen evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   let evl = List.rev (to_list evm) in
@@ -137,8 +159,19 @@ let eterm_obligations name nclen evm t tycon =
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
 	 let hyps = trunc_named_context nclen hyps in
-	 let evtyp, deps = etype_of_evar l ev hyps in
-	 let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
+	 let evtyp, deps = etype_of_evar l hyps ev.evar_concl in
+	 let evtyp, hyps, chop = 
+	   match chop_product fs evtyp with
+	       Some t -> 
+		 (try
+		    trace (str "Choped a product: " ++ spc () ++
+			     Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++
+			     Termops.print_constr_env (Global.env ()) t);
+		  with _ -> ());
+		 t, trunc_named_context fs hyps, fs
+	     | None -> evtyp, hyps, 0
+	 in
+	 let y' = (id, ((n, nstr), hyps, chop, evtyp, deps)) in
 	   y' :: l) 
       evn []
   in 
@@ -146,19 +179,19 @@ let eterm_obligations name nclen evm t tycon =
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
+    List.map (fun (_, ((_, name), _, _, typ, deps)) -> name, typ, deps) evts
   in
-(*     (try  *)
-(*        trace (str "Term given to eterm" ++ spc () ++ *)
-(* 		Termops.print_constr_env (Global.env ()) t); *)
-(*        trace (str "Term constructed in eterm" ++ spc () ++ *)
-(* 		Termops.print_constr_env (Global.env ()) t'); *)
-(*        ignore(iter *)
-(* 		(fun (name, typ, deps) -> *)
-(* 		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *)
-(* 			    Termops.print_constr_env (Global.env ()) typ)) *)
-(* 		evars); *)
-(*      with _ -> ()); *)
+    (try
+       trace (str "Term given to eterm" ++ spc () ++
+		Termops.print_constr_env (Global.env ()) t);
+       trace (str "Term constructed in eterm" ++ spc () ++
+		Termops.print_constr_env (Global.env ()) t');
+       ignore(iter
+		(fun (name, typ, deps) ->
+		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
+			    Termops.print_constr_env (Global.env ()) typ))
+		evars);
+     with _ -> ());
     Array.of_list (List.rev evars), t'
 
 let mkMetas n = 
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index 77d9f293d..a7fcecf2a 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -18,7 +18,8 @@ val mkMetas : int -> constr list
 
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
-val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> 
+val eterm_obligations : identifier -> int -> evar_map -> int -> constr -> types option -> (* id, named context length, evars, number of
+											     function prototypes to try to clear from evars contexts *)
   (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 088dc775b..72bb80aa6 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1602,11 +1602,7 @@ let list_mapi f l =
       [] -> []
     | hd :: tl -> f n hd :: aux (succ n) tl
   in aux 0 l
-	
-let rec pp_list f = function
-    [] -> mt()
-  | x :: y -> f x ++ spc () ++ pp_list f y
-       
+	       
 let constr_of_pat env isevars arsign neqs arity pat idents = 
   let rec typ env (ty, realargs) pat idents = 
     trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 1220c13f4..33e7e1627 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -239,13 +239,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		    mkRel 1
 		 |])
   in
-  (try trace (str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
-  let intern_arity' = liftn 1 after_length top_arity in (* arity in after :: wfarg :: arg :: before *)
-  (try trace (str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ());
-  let intern_arity = substnl [projection] after_length intern_arity' in (* substitute the projection of wfarg for arg *)
-  (try trace (str "Top arity after subst: " ++ my_print_constr top_env intern_arity) with _ -> ());
-  let intern_arity = liftn 1 (succ after_length) intern_arity in (* back in after :: wfarg :: arg :: before (ie, jump over arg) *)
-  (try trace (str "Top arity after subst in intern_env: " ++ my_print_constr _intern_env intern_arity) with _ -> ());
+  (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity);
+     trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ());
+  (* Top arity is in top_env = after :: arg :: before *)
+(*   let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *)
+(*       (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *)
+(* 	 trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *)
+  let intern_arity = substnl [projection] after_length top_arity in (* substitute the projection of wfarg for arg *)
+  (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ());
+(*   let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
+(*   (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
   let intern_before_env = push_rel_context before env in
   let intern_fun_bl = liftafter @ [wfarg 1]  in (* FixMe dependencies *)
 (*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
@@ -253,6 +256,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   (try trace (str "Intern fun arity: " ++
 		  my_print_constr _intern_env intern_fun_arity) with _ -> ());
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+  (try trace (str "Intern fun arity product: " ++
+		  my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
   let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
 (*   (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
@@ -304,7 +309,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (*   in *)
   let evm = non_instanciated_map env isevars in
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
@@ -387,7 +392,7 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
-      let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
+      let evars, def = Eterm.eterm_obligations id nc_len evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 2b36bd2d2..647c47b6a 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -151,5 +151,5 @@ let subtac_proof env isevars id l c tycon =
   let nc = named_context env in
   let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+  let evars, def = Eterm.eterm_obligations id nc_len evm 0 coqc (Some coqt) in
     add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 51bb1f4be..4dc157397 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -129,6 +129,10 @@ let trace s =
     else ()
   else ()
 
+let rec pp_list f = function
+    [] -> mt()
+  | x :: y -> f x ++ spc () ++ pp_list f y
+
 let wf_relations = Hashtbl.create 10
 
 let std_relations () = 
@@ -646,3 +650,4 @@ let utils_tac s =
 
 let utils_call tac args =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index d042eab79..00f01d6e1 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -118,3 +118,5 @@ val string_of_intset : Intset.t -> string
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
 
 val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
+
+val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 7ab720f6b..948ab8e92 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import List.
 Require Import Coq.subtac.Utils.
 
@@ -20,9 +21,9 @@ Section Map_DependentRecursor.
   Variable U V : Set.
   Variable l : list U.
   Variable f : { x : U | In x l } -> V.
-
+  Obligations Tactic := idtac.
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
-    { measure l' length } : { r : list V | length r = length l' } :=
+    { measure length l' } : { r : list V | length r = length l' } :=
     match l' with
     nil => nil
     | cons x tl => let tl' := map_rec tl in
@@ -31,10 +32,10 @@ Section Map_DependentRecursor.
     
     Obligation 1.
     intros.
-    destruct tl' ; simpl ; simpl in e.
-    subst x0 tl0.
-    rewrite <- Heql'.
-    rewrite e.
+    unfold proj1_sig in map_rec.
+    intros.
+    destruct l' ; subtac_simpl.
+    rewrite <- Heq_l'.
     auto.
     Qed.
 
@@ -42,19 +43,17 @@ Section Map_DependentRecursor.
     simpl.
     intros.
     destruct l'.
-    simpl in Heql'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
+    subtac_simpl.
     inversion s.
-    apply H.
-    auto with datatypes.
+    unfold sub_list. 
+    intuition.
     Qed.
 
 
     Obligation 3 of map_rec.
     simpl.
     intros.
-    rewrite <- Heql'.
+    rewrite <- Heq_l'.
     simpl ; auto with arith.
     Qed.
 
@@ -62,16 +61,25 @@ Section Map_DependentRecursor.
     simpl.
     intros.
     destruct l'.
-    simpl in Heql'.
+    simpl in Heq_l'.
     destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
+    inversion Heq_l'.
     subst x tl.
-    apply sub_list_tl with u ; auto.
+    inversion s.
+    apply H.
+    auto with datatypes.
     Qed.
   
     Obligation 5.
-    intros.
-    rewrite <- Heql' ; auto.
+    Proof.
+      intros.
+      destruct tl'.
+      destruct l'.
+      simpl in *.
+      subst.
+      simpl.
+      subtac_simpl.
+      simpl ; rewrite e ; auto.
     Qed.
     
     Program Definition map : list V := map_rec l.