1 files changed, 233 insertions, 88 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 7b13b402..d6c1772f 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,6 +12,8 @@ open Decl_kinds
 open Util
 open Evd
 
+type obligation_info = (Names.identifier * Term.types * Intset.t) array
+
 type obligation =
     { obl_name : identifier;
       obl_type : types;
@@ -24,15 +26,42 @@ type obligations = (obligation array * int)
 type program_info = {
   prg_name: identifier;
   prg_body: constr;
-  prg_type: types;
+  prg_type: constr;
   prg_obligations: obligations;
+  prg_deps : identifier list;
+  prg_nvrec : int array;
 }
 
-let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
+let assumption_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+
+let set_default_tactic t = default_tactic := t
+
+let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
 			     evar_concl = o.obl_type ; 
 			     evar_body = Evar_empty ;
 			     evar_extra = None }
 
+let subst_deps obls deps t =
+  Intset.fold
+    (fun x acc ->
+       let xobl = obls.(x) 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
+
+let subst_deps_obl obls obl =
+  let t' = subst_deps obls obl.obl_deps obl.obl_type in
+    { obl with obl_type = t' }
+
 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)
@@ -62,21 +91,6 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-let declare_definition prg = 
-(*  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;
-      const_entry_opaque = false;
-      const_entry_boxed = false} 
-  in
-  let _constant = Declare.declare_constant 
-    prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
-  in
-    Subtac_utils.definition_message prg.prg_name
-    
 open Evd
 
 let terms_of_evar ev = 
@@ -88,14 +102,72 @@ let terms_of_evar ev =
 	  body, typ
     | _ -> assert(false)
 	  
+let rec intset_to = function
+    -1 -> Intset.empty
+  | n -> Intset.add n (intset_to (pred n))
+  
+let subst_body prg = 
+  let obls, _ = prg.prg_obligations in
+    subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body
+
+let declare_definition prg =
+  let body = subst_body prg in
+    (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
+		  my_print_constr (Global.env()) body);
+     with _ -> ());
+  let ce = 
+    { const_entry_body = body;
+      const_entry_type = Some prg.prg_type;
+      const_entry_opaque = false;
+      const_entry_boxed = false} 
+  in
+  let _constant = Declare.declare_constant 
+    prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
+  in
+    Subtac_utils.definition_message prg.prg_name
+
+open Pp
+open Ppconstr
+
+let declare_mutual_definition l =
+  let len = List.length 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 recvec = 
+    Array.of_list 
+      (List.map (fun x -> 
+		   let subs = (subst_body x) in
+		     snd (decompose_lam_n len subs)) l)
+  in
+  let nvrec = (List.hd l).prg_nvrec 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 (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 = 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) }
@@ -113,36 +185,30 @@ let try_tactics obls =
 	 | _ -> obl)
     obls
         
-let add_entry n b t obls =
-  Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let init_obls e = 
-    Array.map
-      (fun (n, t, d) ->
-         { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
-      e
+let red = Reductionops.nf_betaiota
+
+let init_prog_info n b t deps nvrec obls =
+  let obls' = 
+    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 = red t; 
+	   obl_deps = d })
+      obls
   in
-    if Array.length obls = 0 then (
-      Options.if_verbose ppnl (str ".");
-    declare_definition { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = ([||], 0) } )
-    else (
-      let len = Array.length obls in
-      let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") 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 
-	  Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining.");
-	if rem = 0 then 
-	  declare_definition prg
-	else
-	  from_prg := ProgMap.add n prg !from_prg)
-	    
-let error s = Util.error s
+    { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
+      prg_deps = deps; prg_nvrec = nvrec; }
+    
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
 
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
-	Some n -> ProgMap.find n prg_infos
+	Some n -> 
+	  (try ProgMap.find n prg_infos
+	   with Not_found -> error ("No obligations for program " ^ string_of_id n))
       | None -> 
 	  (let n = map_cardinal prg_infos in
 	     match n with 
@@ -150,57 +216,67 @@ let get_prog name =
 	       | 1 -> map_first prg_infos
 	       | _ -> error "More than one program with unsolved obligations")
 
+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 msgnl (int rem ++ str " obligation(s) remaining");
+    )
     else (
-      declare_definition prg';
-      from_prg := ProgMap.remove prg.prg_name !from_prg
-    )		 
+      Options.if_verbose msgnl (str "No more obligations remaining");
+      match prg'.prg_deps with
+	  [] ->
+	    declare_definition prg';
+	    from_prg := ProgMap.remove prg.prg_name !from_prg
+	| l ->
+	    let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+	      if List.for_all (fun x -> obligations_solved x) progs then 
+		(declare_mutual_definition progs;
+		 from_prg := List.fold_left
+		   (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
 	    
 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
 	 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 solve_obligation prg num =
+  let user_num = succ num in
+  let obls, rem = prg.prg_obligations in
+  let obl = obls.(num) in
+    if obl.obl_body <> None then
+      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")    
+    else
+      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
+		(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: " ++
+		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+	      Pfedit.by !default_tactic
+	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+
+let subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
   let prg = get_prog name in
   let obls, rem = prg.prg_obligations in
     if num < Array.length obls then
       let obl = obls.(num) in
 	match obl.obl_body with
-	    None -> 
-	      (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)))
+	    None -> solve_obligation prg num
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
       
@@ -217,33 +293,102 @@ let obligations_of_evars evars =
 	    }) evars)
   in arr, Array.length arr
 
+let solve_obligation_by_tac prg obls i tac =
+  let obl = obls.(i) in
+  match obl.obl_body with 
+      Some _ -> false
+    | None -> 
+	(try
+	   if deps_remaining obls obl.obl_deps = [] then
+	     let obl = subst_deps_obl obls obl in
+	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
+	       obls.(i) <- { obl with obl_body = Some t };
+	       true		 
+	   else false
+	 with _ -> false)  
+
 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.copy obls in
+  let _ = 
+    Array.iteri (fun i x -> 
+		   if solve_obligation_by_tac prg obls' i tac then
+		     decr rem)
+      obls'
+  in
+    update_obls prg obls' !rem
+
+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 [] (Array.make 0 0) obls in
+  let obls,_ = prg.prg_obligations in
+  if Array.length obls = 0 then (
+    Options.if_verbose ppnl (str ".");    
+    declare_definition prg;
+    from_prg := ProgMap.remove prg.prg_name !from_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; 
+      solve_obligations (Some n) !default_tactic)
+	
+let add_mutual_definitions l nvrec =
+  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 nvrec obls in
+	   ProgMap.add n prg acc)
+      !from_prg l
+  in
+    from_prg := upd;
+    List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps
+
+let admit_obligations n =
+  let prg = get_prog n in
+  let obls, rem = prg.prg_obligations in
   let obls' = 
-    Array.map (fun x -> 
+    Array.mapi (fun i x -> 
 		 match x.obl_body with 
-		     Some _ -> x
-		   | None -> 
-		       try
-			 let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
-			   decr rem;
-			   { x with obl_body = Some t }
-		       with _ -> x)
+		     None -> 
+			 let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+			   assumption_message x.obl_name;
+			   { x with obl_body = Some (mkConst kn) }
+		   | Some _ -> x)
       obls
   in
-    update_obls prg obls' !rem
+    update_obls prg obls' 0
 
+exception Found of int
+
+let array_find f arr = 
+  try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
+    raise Not_found
+  with Found i -> i
+
+let rec next_obligation n =
+  let prg = get_prog n in
+  let obls, rem = prg.prg_obligations in
+  let i = 
+    array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
+      obls
+  in
+    if solve_obligation_by_tac prg obls i !default_tactic then (
+      update_obls prg obls (pred rem);
+      next_obligation n
+    ) else solve_obligation prg i
+      
 open Pp
 let show_obligations n =
   let prg = get_prog n in
+  let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
     msgnl (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x -> 
 		   match x.obl_body with 
-		       None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ 
-					my_print_constr (Global.env ()) x.obl_type)
+		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
 		    | Some _ -> ())
       obls