Debug obligation handling code

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

4 files changed, 92 insertions, 35 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index b95f643a5..790e61a0a 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -125,12 +125,12 @@ let trunc_named_context n ctx =
 let eterm_obligations name nclen evm t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
-  let evl = to_list evm in
+  let evl = List.rev (to_list evm) in
   trace (str "Eterm, transformed to list");
   let evn = 
     let i = ref (-1) in
-      List.map (fun (id, ev) -> incr i; 
-		  (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i)), ev)) evl
+      List.rev_map (fun (id, ev) -> incr i; 
+		  (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
   in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
@@ -163,7 +163,7 @@ let eterm_obligations name nclen evm t tycon =
 			    Termops.print_constr_env (Global.env ()) typ))
 		evars);
      with _ -> ());
-    Array.of_list evars, t'
+    Array.of_list (List.rev evars), t'
 
 let mkMetas n = 
   let rec aux i acc = 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 26a195e3d..7b13b4023 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -10,10 +10,11 @@ open Libobject
 open Entries
 open Decl_kinds
 open Util
+open Evd
 
 type obligation =
     { obl_name : identifier;
-      obl_type  : types;
+      obl_type : types;
       obl_body : constr option;
       obl_deps : Intset.t;
     }
@@ -27,6 +28,11 @@ type program_info = {
   prg_obligations: obligations;
 }
 
+let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
+			     evar_concl = o.obl_type ; 
+			     evar_body = Evar_empty ;
+			     evar_extra = None }
+
 module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
 
 let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
@@ -57,9 +63,9 @@ let _ =
       Summary.survive_section = false }
 
 let declare_definition prg = 
-  let obls_constrs = 
-    Array.fold_right (fun x acc -> (out_some x.obl_body) :: acc) (fst prg.prg_obligations) []
-  in
+(*  let obls_constrs = 
+    Array.fold_right (fun x acc -> (out_some x.obl_evar.evar_body) :: acc) (fst prg.prg_obligations) []
+  in*)
   let ce = 
     { const_entry_body = prg.prg_body;
       const_entry_type = Some prg.prg_type;
@@ -72,21 +78,47 @@ let declare_definition prg =
     Subtac_utils.definition_message prg.prg_name
     
 open Evd
+
+let terms_of_evar ev = 
+  match ev.evar_body with
+      Evar_defined b ->
+	let nc = Environ.named_context_of_val ev.evar_hyps in
+	let body = Termops.it_mkNamedLambda_or_LetIn b nc in
+	let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
+	  body, typ
+    | _ -> assert(false)
+	  
+let declare_obligation obl body =
+  let ce = 
+    { const_entry_body = body;
+      const_entry_type = Some obl.obl_type;
+      const_entry_opaque = true;
+      const_entry_boxed = false} 
+  in
+  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) }
       
+let try_tactics obls = 
+  Array.map
+    (fun obl ->
+       match obl.obl_body with
+	   None ->
+	     (try
+		let ev = evar_of_obligation obl in
+		let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in	       
+		  declare_obligation obl c		  
+	      with _ -> obl)
+	 | _ -> obl)
+    obls
+        
 let add_entry n b t obls =
   Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let try_tactics e = 
+  let init_obls e = 
     Array.map
       (fun (n, t, d) ->
-	 let ev = { evar_concl = t ; evar_body = Evar_empty ; 
-		    evar_hyps = Environ.empty_named_context_val ; evar_extra = None } 
-	 in 
-	 let cstr = 
-	   try
-	     let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in	       
-	       Some c
-	   with _ -> None
-	 in { obl_name = n ; obl_type = t; obl_body = cstr; obl_deps = d })
+         { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
       e
   in
     if Array.length obls = 0 then (
@@ -95,7 +127,7 @@ let add_entry n b t obls =
     else (
       let len = Array.length obls in
       let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
-      let obls = try_tactics obls in
+      let obls = init_obls obls in
       let rem = Array.fold_left (fun acc obl -> if obl.obl_body = None then succ acc else acc) 0 obls in
       let prg = { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = (obls, rem) } in
 	if rem < len then 
@@ -128,6 +160,26 @@ let update_obls prg obls rem =
       from_prg := ProgMap.remove prg.prg_name !from_prg
     )		 
 	    
+let is_defined obls x = obls.(x).obl_body <> None
+
+let deps_remaining obls x = 
+  let deps = obls.(x).obl_deps in
+    Intset.fold
+      (fun x acc -> 
+	 if is_defined obls x then acc
+	 else x :: acc)
+      deps []
+
+let subst_deps obls obl =
+  let t' = 
+    Intset.fold
+      (fun x acc ->
+	 let xobl = obls.(x) in
+	 let oblb = out_some xobl.obl_body in
+	   Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
+      obl.obl_deps obl.obl_type
+  in { obl with obl_type = t' }
+
 let subtac_obligation (user_num, name) =
   let num = pred user_num in
   let prg = get_prog name in
@@ -136,14 +188,19 @@ let subtac_obligation (user_num, name) =
       let obl = obls.(num) in
 	match obl.obl_body with
 	    None -> 
-	      Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
-		(fun strength gr -> 
-		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
-		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
-		   let obls = Array.copy obls in
-		   let _ = obls.(num) <- obl in
-		     update_obls prg obls (pred rem));
-	      trace (str "Started obligation " ++ int user_num ++ str "  proof")
+	      (match deps_remaining obls num with
+		  [] ->
+		    let obl = subst_deps obls obl in
+		    Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
+		      (fun strength gr -> 
+			 debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
+			 let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
+			 let obls = Array.copy obls in
+			 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) "
+		     ++ 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))
       
@@ -160,13 +217,6 @@ let obligations_of_evars evars =
 	    }) evars)
   in arr, Array.length arr
 
-let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
-			     evar_concl = o.obl_type ; 
-			     evar_body = Evar_empty ;
-			     evar_extra = None }
-
-
-
 let solve_obligations n tac = 
   let prg = get_prog n in
   let obls, rem = prg.prg_obligations in
@@ -192,7 +242,7 @@ let show_obligations n =
     msgnl (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x -> 
 		   match x.obl_body with 
-		       None -> msgnl (int i ++ str " : " ++ spc () ++ 
+		       None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ 
 					my_print_constr (Global.env ()) x.obl_type)
 		    | Some _ -> ())
       obls
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 3248ed30d..7b96758ad 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -447,3 +447,8 @@ let solve_by_tac ev t =
   let c = Tacmach.extract_pftreestate solved_state in
     debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
     c
+
+let rec string_of_list sep f = function
+    [] -> ""
+  | x :: [] -> f x
+  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index c8afd9f8b..ebfc51232 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -96,3 +96,5 @@ val definition_message : identifier -> unit
 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