1 files changed, 69 insertions, 47 deletions

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))