Subtac bug fix, add list take example.

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

8 files changed, 108 insertions, 45 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index f5115812ac..aa1d0ff388 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -44,6 +44,23 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
-Ltac subtac_simpl := simpl ; intros ; destruct_exists.
+Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in *.
+
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
+Ltac destruct_call f :=
+  match goal with
+    | H : ?T |- _  =>
+      match T with
+         context [f ?x ?y ?z] => destruct (f x y z)
+       | context [f ?x ?y] => destruct (f x y)
+       | context [f ?x] => destruct (f x)        
+      end
+    | |- ?T  =>
+      match T with
+        context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
+        | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
+        | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
+      end
+    end.
 
 Extraction Inline proj1_sig.
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index a333cbbfe3..568c513d88 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1607,7 +1607,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
 	option_map (fun tycon -> 
-		      let tycon' = (lift_tycon_type (succ (List.length arsign)) tycon) in
+		      let tycon' = (lift_tycon_type (List.length arsign) tycon) in
 			isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val
 			  tycon')
 	  tycon
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index ba85e705e8..c78145357e 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -221,21 +221,21 @@ module Coercion = struct
 					    mkApp (prod.intro, [| a'; b'; x ; y |]))
 			   end
 		       else
-			 if len = 1 && len = Array.length l' && i = i' then
-			   let argx, argy = l.(0), l'.(0) in
-			   let indtyp = Inductiveops.type_of_inductive env i in
-			   let argname, argtype, _ = destProd indtyp in
-			   let eq =
-			     mkApp (Lazy.force eqind, [| argtype; argx; argy |])
-			   in
-			   let pred = mkLambda (argname, argtype, 
-						mkApp (mkInd i, [| mkRel 1 |]))
-			   in
-			   let evar = make_existential dummy_loc env isevars eq in
-			     Some (fun x ->
-				     mkApp (Lazy.force eqrec, 
-					    [| argtype; argx; pred; x; argy; evar |]))
-			 else subco ()
+			 (* if len = 1 && len = Array.length l' && i = i' then *)
+(* 			   let argx, argy = l.(0), l'.(0) in *)
+(* 			   let indtyp = Inductiveops.type_of_inductive env i in *)
+(* 			   let argname, argtype, _ = destProd indtyp in *)
+(* 			   let eq = *)
+(* 			     mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *)
+(* 			   in *)
+(* 			   let pred = mkLambda (argname, argtype,  *)
+(* 						mkApp (mkInd i, [| mkRel 1 |])) *)
+(* 			   in *)
+(* 			   let evar = make_existential dummy_loc env isevars eq in *)
+(* 			     Some (fun x -> *)
+(* 				     mkApp (Lazy.force eqrec,  *)
+(* 					    [| argtype; argx; pred; x; argy; evar |])) *)
+(* 			 else  *)subco ()
 		 | _ ->  subco ())
 	  | _, _ ->  subco ()
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 43d6fcdec7..ef6d0bed10 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -168,6 +168,10 @@ let rec gen_rels = function
     0 -> []
   | n -> mkRel n :: gen_rels (pred n)
 
+let split_args n rel = match list_chop ((List.length rel) - n) rel with
+    (l1, x :: l2) -> l1, x, l2
+  | _ -> assert(false)
+
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
@@ -186,7 +190,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
     with _ -> ()
   in
   let env', binders_rel = interp_context isevars env bl in
-  let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+  let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
   let _liftafter = lift_binders 1 after_length after in
@@ -218,7 +222,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   in
   let argid' = id_of_string (string_of_id argid ^ "'") in
   let wfarg len = (Name argid', None, 
-  		   mkSubset (Name argid') argtyp 
+  		   mkSubset (Name argid') (lift len argtyp) 
 		     (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let top_bl = after @ (arg :: before) in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 5312fb3311..a20383688f 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -218,7 +218,7 @@ let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
     from_prg := map_replace prg.prg_name prg' !from_prg;
     if rem > 0 then (
-      Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining");
+      Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
     )
     else (
       debug 2 (str "No more obligations remaining");
@@ -258,8 +258,7 @@ let add_mutual_definitions l =
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
-let deps_remaining obls x = 
-  let deps = obls.(x).obl_deps in
+let deps_remaining obls deps = 
     Intset.fold
       (fun x acc -> 
 	 if is_defined obls x then acc
@@ -274,7 +273,7 @@ let subtac_obligation (user_num, name, typ) =
       let obl = obls.(num) in
 	match obl.obl_body with
 	    None -> 
-	      (match deps_remaining obls num with
+	      (match deps_remaining obls obl.obl_deps with
 		  [] ->
 		    let obl = subst_deps_obl obls obl in
 		    Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
@@ -308,20 +307,22 @@ let solve_obligations n tac =
   let prg = get_prog n in
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
-  let obls' = 
-    Array.map (fun x -> 
+  let obls' = Array.copy obls in
+  let _ = 
+    Array.iteri (fun i x -> 
 		 match x.obl_body with 
-		     Some _ -> x
+		     Some _ -> ()
 		   | None -> 
 		       (try
-			  let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
-			    decr rem;
-			    { x with obl_body = Some t }
+			  if deps_remaining obls' x.obl_deps = [] then
+			    let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
+			      decr rem;
+			      obls'.(i) <- { x with obl_body = Some t }
+			  else ()
 			with UserError (s, cmds) ->
-			  debug 1 cmds;
-			  x
-			  | _ -> x))
-      obls
+			  debug 1 cmds
+			  | _ -> ()))
+      obls'
   in
     update_obls prg obls' !rem
 
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index cd639e7784..c329712898 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -161,7 +161,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [(evars_of isevars)] and *)
   (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env isevars lvar = function
+  let rec pretype (tycon : type_constraint) env isevars lvar c = 
+    let _ = Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++
+			       str " with tycon " ++ Evarutil.pr_tycon env tycon) in
+    match c with
     | RRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env isevars
 	  (pretype_ref isevars env ref)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 7b7b66c217..f10e1cf6d8 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -98,7 +98,7 @@ let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
-let debug_level = 4
+let debug_level = 2
 
 let debug_on = true
 
@@ -527,8 +527,8 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
   in
   let mkHole = RHole (dummy_loc, InternalHole) in
   let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force jmeq_ind_ref)),
-		       [mkHole; c; mkHole; n])
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+		       [mkHole; c; n])
   in
   let eqs_types = 
     List.map
@@ -555,7 +555,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
 		in (loc, idl, cpl, c'))
       eqns
   in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force jmeq_refl_ref),
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
 			      [mkHole; c])
   in
   let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
@@ -575,11 +575,10 @@ let rec rewrite_cases c =
 	   | _ -> assert(false))
     | _ -> map_rawconstr rewrite_cases c
 	  
-let rewrite_cases env c = c
-(*
+let rewrite_cases env c =
   let c' = rewrite_cases c in
   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
-    c'*)
+    c'
 
 let id_of_name = function
     Name n -> n
@@ -614,15 +613,15 @@ let solve_by_tac ev t =
     *)
 
 let solve_by_tac evi t =
-  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
+  debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
   let id = id_of_string "H" in
-  Pfedit.start_proof id (Decl_kinds.Local,Decl_kinds.Proof Decl_kinds.Lemma) evi.evar_hyps evi.evar_concl
+  try 
+    Pfedit.start_proof id (Decl_kinds.Local,Decl_kinds.Proof Decl_kinds.Lemma) evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
-  try
     Pfedit.by (tclCOMPLETE t);
     let _,(const,_,_) = Pfedit.cook_proof () in 
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
-  with e when Logic.catchable_exception e -> 
+  with e -> 
     Pfedit.delete_current_proof();
     raise Exit
 
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
new file mode 100644
index 0000000000..fbb1727eae
--- /dev/null
+++ b/contrib/subtac/test/take.v
@@ -0,0 +1,39 @@
+Variable A : Set.
+Require Import JMeq.
+Require Import List.
+Require Import Coq.subtac.Utils.
+
+Program Fixpoint take (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
+  match n with
+  | 0 => nil
+  | S n => 
+    match l with
+    | cons hd tl => let rest := take tl n in cons hd rest
+    | _ => _
+    end
+  end.
+  
+Require Import Omega.
+
+
+Obligations.
+
+Solve Obligations using (subtac_simpl ; subst ; auto with arith).
+
+Obligations.
+
+Obligation 2.
+  subtac_simpl.
+  subst l x.
+  simpl in l0.
+  absurd (S n0 <= 0) ; omega.
+Defined.
+
+Obligation 4.
+  subtac_simpl.
+  destruct_call take ; subtac_simpl ; subst ; auto.
+Defined.
+
+Print take.
+
+Extraction take.