Work on mutual defs, various bug fixes.

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

8 files changed, 125 insertions, 157 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 790e61a0a..8ec173630 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -141,7 +141,8 @@ let eterm_obligations name nclen evm t tycon =
 	 let hyps = trunc_named_context nclen hyps in
 	 trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
 	 let evtyp, deps = etype_of_evar l ev hyps in
-	 trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
+	 trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp ++
+		  str " depends on evars : " ++ str (Subtac_utils.string_of_intset deps));
 	 let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
 	   y' :: l) 
       evn []
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 955ee8ac2..43d6fcdec 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -364,52 +364,6 @@ let build_mutrec l boxed =
 
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env lrecnames recdef arityl nv in
-  let declare arrec defrec =
-    let recvec = 
-      Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
-    let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
-    let rec declare i fi =
-      (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
-		  my_print_constr env (recvec.(i)));
-       with _ -> ());
-      let ce = 
-	{ const_entry_body = mkFix ((nvrec,i),recdecls); 
-          const_entry_type = Some arrec.(i);
-          const_entry_opaque = false;
-          const_entry_boxed = boxed} in
-      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
-      in (ConstRef kn)
-    in 
-      (* declare the recursive definitions *)
-    let lrefrec = Array.mapi declare namerec in
-      Options.if_verbose ppnl (recursive_message lrefrec);
-
-
-      (*(* The others are declared as normal definitions *)
-      let var_subst id = (id, Constrintern.global_reference id) in
-      let _ = 
-	List.fold_left
-	  (fun subst (f,def,t) ->
-	     let ce = { const_entry_body = replace_vars subst def;
-			const_entry_type = Some t;
-			const_entry_opaque = false;
-			const_entry_boxed = boxed } in
-	     let _ =
-	       Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
-	     in
-      	       warning ((string_of_id f)^" is non-recursively defined");
-      	       (var_subst f) :: subst)
-	  (List.map var_subst (Array.to_list namerec))
-	  lnonrec 
-      in*)
-      List.iter (fun (df,c,scope) ->
-		   Metasyntax.add_notation_interpretation df [] c scope) notations
-  in 
-  let declare l = 
-    let recvec = Array.of_list l
-    and arrec = Array.map pi3 arrec
-    in declare arrec recvec
-  in
   let recdefs = Array.length defrec in
     trace (int recdefs ++ str " recursive definitions");
     (* Solve remaining evars *)
@@ -430,11 +384,11 @@ let build_mutrec l boxed =
 	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
       in
       let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
-	collect_evars (succ i) ((id, def, typ, evars) :: acc)
+	collect_evars (succ i) ((id, nvrec.(i), def, typ, evars) :: acc)
     else acc
   in 
   let defs = collect_evars 0 [] in
-    Subtac_obligations.add_mutual_definitions defs
+    Subtac_obligations.add_mutual_definitions (List.rev defs)
       
 let out_n = function
     Some n -> n
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 8bb79a785..e2192f28d 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -28,7 +28,7 @@ type program_info = {
   prg_body: constr;
   prg_type: constr;
   prg_obligations: obligations;
-  prg_deps : identifier list;
+  prg_deps : (identifier * int) list;
 }
 
 let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
@@ -40,7 +40,13 @@ let subst_deps obls deps t =
   Intset.fold
     (fun x acc ->
        let xobl = obls.(x) in
-       let oblb = out_some xobl.obl_body in
+	 debug 3 (str "Trying to get body of obligation " ++ int x);
+       let oblb = 
+	 try out_some xobl.obl_body
+	 with _ ->
+	   debug 3 (str "Couldn't get body of obligation " ++ int x);
+	   assert(false)
+       in
 	 Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
     deps t
 
@@ -108,41 +114,49 @@ let declare_definition prg =
   in
     Subtac_utils.definition_message prg.prg_name
 
-let declare_mutual_definition l = assert(false)
-  (*let len = List.length l in
-  let namerec = List.map (fun x -> x.prg_name) l in
-  let arrrec = 
-    Array.of_list (List.map (fun x -> x.prg_type) l)
+open Pp
+open Ppconstr
+
+let declare_mutual_definition l =
+  let len = List.length l in
+  let l, nvlist = List.split l in
+  let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
+  let arrec = 
+    Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l)
   in
-  let defrec = 
-    Array.of_list (List.map (fun x -> subst_body x) l)
+  let recvec = 
+    Array.of_list 
+      (List.map (fun x -> 
+		   let subs = (subst_body x) in
+		     snd (decompose_lam_n len subs)) l)
   in
-  let recvec = Array.map (subst_vars (List.rev namerec)) defrec in
-  let recdecls = (Array.of_list (List.map (fun id -> Name id) namerec), arrec, recvec) in
+  let nvrec = Array.of_list nvlist in
+  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
-		  my_print_constr env (recvec.(i)));
+		  my_print_constr (Global.env()) (recvec.(i)));
      with _ -> ());
     let ce = 
       { const_entry_body = mkFix ((nvrec,i),recdecls); 
         const_entry_type = Some arrec.(i);
         const_entry_opaque = false;
-        const_entry_boxed = boxed} in
+        const_entry_boxed = true} in
     let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
     in
       ConstRef kn
   in
   let lrefrec = Array.mapi declare namerec in
     Options.if_verbose ppnl (recursive_message lrefrec)
-    *)     
+         
 let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
       const_entry_type = Some obl.obl_type;
-      const_entry_opaque = true;
+      const_entry_opaque = false;
       const_entry_boxed = false} 
   in
-  let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property)
+  let constant = Declare.declare_constant obl.obl_name 
+    (DefinitionEntry ce,IsProof Property)
   in
     Subtac_utils.definition_message obl.obl_name;
     { obl with obl_body = Some (mkConst constant) }
@@ -163,36 +177,17 @@ let try_tactics obls =
 
 let init_prog_info n b t deps obls =
   let obls' = 
-    Array.map
-      (fun (n, t, d) ->
+    Array.mapi
+      (fun i (n, t, d) ->
+	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = t; prg_obligations = (obls', Array.length obls');
       prg_deps = deps }
-
-let add_definition n b t obls =
-  Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n b t [] obls in
-  let obls,_ = prg.prg_obligations in
-  if Array.length obls = 0 then (
-    Options.if_verbose ppnl (str ".");
-    declare_definition prg)
-  else (
-    let len = Array.length obls in
-    let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
-      from_prg := ProgMap.add n prg !from_prg)
-	
-let add_mutual_definitions l =
-  let deps = List.map (fun (n, b, t, obls) -> n) l in
-  let upd = List.fold_left
-      (fun acc (n, b, t, obls) ->
-	 let prg = init_prog_info n b t deps obls in
-	   ProgMap.add n prg acc)
-      !from_prg l
-  in from_prg := upd
     
-let error s = Util.error s
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
 
 let get_prog name =
   let prg_infos = !from_prg in
@@ -209,18 +204,45 @@ let obligations_solved prg = (snd prg.prg_obligations) = 0
 
 let update_obls prg obls rem = 
   let prg' = { prg with prg_obligations = (obls, rem) } in
-    if rem > 1 then (
-      debug 2 (int rem ++ str " obligations remaining");
-      from_prg := map_replace prg.prg_name prg' !from_prg)
+    from_prg := map_replace prg.prg_name prg' !from_prg;
+    if rem > 0 then (
+      Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining");
+    )
     else (
+      debug 2 (str "No more obligations remaining");
       match prg'.prg_deps with
 	  [] ->
 	    declare_definition prg';
 	    from_prg := ProgMap.remove prg.prg_name !from_prg
 	| l ->
-	    if List.for_all (fun x -> obligations_solved (ProgMap.find x !from_prg)) prg'.prg_deps then 
-	      declare_mutual_definition (List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps)
-    )
+	    let progs = List.map (fun (x,y) -> ProgMap.find x !from_prg, y) prg'.prg_deps in
+	      if List.for_all (fun x -> obligations_solved (fst x)) progs then 
+		declare_mutual_definition progs)
+
+let add_definition n b t obls =
+  Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+  let prg = init_prog_info n b t [] obls in
+  let obls,_ = prg.prg_obligations in
+  if Array.length obls = 0 then (
+    Options.if_verbose ppnl (str ".");
+    declare_definition prg)
+  else (
+    let len = Array.length obls in
+    let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+      from_prg := ProgMap.add n prg !from_prg)
+	
+let add_mutual_definitions l =
+  let deps = List.map (fun (n, nclen, b, t, obls) -> n, nclen) l in
+  let upd = List.fold_left
+      (fun acc (n, nclen, b, t, obls) ->
+	 let prg = init_prog_info n b t deps obls in
+	   ProgMap.add n prg acc)
+      !from_prg l
+  in
+    from_prg := upd;
+    let prg = (ProgMap.find (fst (List.hd deps)) !from_prg) in
+    let o, r = prg.prg_obligations in
+      update_obls prg o r
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
@@ -251,7 +273,7 @@ let subtac_obligation (user_num, name) =
 			 let _ = obls.(num) <- obl in
 			   update_obls prg obls (pred rem));
 		    trace (str "Started obligation " ++ int user_num ++ str "  proof")
-     		 | l -> msgnl (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+     		 | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		     ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)))
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index a8039300a..6ba479764 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -6,7 +6,7 @@ val add_definition : Names.identifier ->  Term.constr -> Term.types ->
   obligation_info -> unit
 
 val add_mutual_definitions : 
-  (Names.identifier * Term.constr * Term.types * obligation_info) list -> unit
+  (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit
 
 val subtac_obligation : int * Names.identifier option -> unit
 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index b196bf913..8164910f2 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -591,3 +591,6 @@ let rec string_of_list sep f = function
     [] -> ""
   | x :: [] -> f x
   | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
+
+let string_of_intset d = 
+  string_of_list "," string_of_int (Intset.elements d)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index ebfc51232..86662c478 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -98,3 +98,4 @@ val recursive_message : global_reference array -> std_ppcmds
 val solve_by_tac : evar_info -> Tacmach.tactic -> constr
 
 val string_of_list : string -> ('a -> string) -> 'a list -> string
+val string_of_intset : Intset.t -> string
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 0b40ef82a..8a9bec52f 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,13 +1,28 @@
-Program Fixpoint f (a : nat) : nat := 
+Program Fixpoint f (a : nat) : { x : nat | x > 0 } := 
   match a with
-  | 0 => 0
+  | 0 => 1
   | S a' => g a a'
   end
-with g (a b : nat) { struct b } : nat := 
+with g (a b : nat) { struct b } : { x : nat | x > 0 } := 
   match b with
-  | 0 => 0
+  | 0 => 1
   | S b' => f b'
   end.
 
+Obligations of f.
+
+Obligation 1 of f.
+  simpl ; intros ; auto with arith.
+Defined.
+
+Obligation 1 of g.
+  simpl ; intros ; auto with arith.
+Defined.
+
 Check f.
-Check g.
\ No newline at end of file
+Check g.
+
+
+
+
+
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index c14edad55..7fa80fbd0 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -11,71 +11,43 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
 
 Obligations.
 
-Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) =>
-@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a
-  (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)).
-
-Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
-  (a & a).
+Require Import Coq.subtac.Utils.
+Require Import Coq.subtac.FixSub.
+Require Import Omega.
 
 Obligation 1.
-intros ; simpl ; auto.
+  simpl ; intros.
+  destruct_exists ; simpl in * ; auto with arith.
+  omega.
 Qed.
 
-Solve Obligations using auto.
-reflexivity.
-Defined.
-
-Extraction testsig.
-Extraction sig.
-Extract Inductive sig => "" [ "" ].
-Extraction testsig.
-
-Require Import Coq.Arith.Compare_dec.
+Obligation 2 of euclid.
+  simpl ; intros.
+  destruct_exists ; simpl in * ; auto with arith.
+  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+Qed.
 
-Require Import Omega.
+Obligation 4 of euclid.
+  exact Wf_nat.lt_wf.
+Qed.
 
-Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w.
-intros.
-assert(y * S z = y * z + y).
-auto.
-rewrite H1.
-omega.
+Obligation 3 of euclid.
+  simpl ; intros.
+  destruct_exists ; simpl in *.
+  omega.
 Qed.
 
-Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
-  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
-  (S q' & r)
-  else (O & a).
-intro euclid.
-simpl ; intros.
-Print euclid_evars.
-eapply euclid_evars with euclid.
-refine (euclid_evars _ _ _ euclid a Acc_a b).
-; simpl ; intros.
-Show Existentials.
+Extraction Inline Fix_sub Fix_F_sub.  
+Extract Inductive sigT => "pair" [ "" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extraction le_lt_dec.
+Extraction euclid.
 
-induction b0 ; induction r.
-simpl in H.
-simpl.
-simpl in p0.
-destruct p0.
-split.
 
-apply minus_eq_add.
-omega.
-auto with arith.
-auto.
-simpl.
-induction b0 ; simpl.
-split ; auto.
-omega.
-exact (euclid a0 Acc_a0 b0).
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
+  (a & a).
 
-exact (Acc_a).
-auto.
-auto.
-Focus 1.
 
+Solve Obligations using simpl ; auto.
 
+Extraction testsig.