Support for mutual defs in obligation handling.

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

4 files changed, 126 insertions, 151 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b433af2cc..bf09bcb18 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -311,15 +311,15 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	 evars;
      with _ -> ());    
       trace (str "Adding to obligations list");
-      Subtac_obligations.add_entry recname evars_def fullctyp evars;
+      Subtac_obligations.add_definition recname evars_def fullctyp evars;
       trace (str "Added to obligations list")
-(*
+
 let build_mutrec l boxed = 
-  let sigma = Evd.empty
-  and env0 = Global.env()
-  in 
+  let sigma = Evd.empty and env = Global.env () in 
+  let nc = named_context env in
+  let nc_len = named_context_length nc in
   let lnameargsardef =
-    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
+    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*)
     l
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
@@ -331,14 +331,14 @@ let build_mutrec l boxed =
       (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
 	 let isevars = ref (Evd.create_evar_defs sigma) in	  
 	 let arityc = Command.generalize_constr_expr arityc bl in
-	 let arity = interp_type isevars env0 arityc in
+	 let arity = interp_type isevars env arityc in
 	 let impl = 
 	   if Impargs.is_implicit_args()
-	   then Impargs.compute_implicits env0 arity
+	   then Impargs.compute_implicits env arity
 	   else [] in
 	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
 	   (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
-      (env0,[],[]) lnameargsardef in
+      (env,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
     List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
@@ -371,14 +371,14 @@ let build_mutrec l boxed =
   in
 
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
-    collect_non_rec env0 lrecnames recdef arityl nv in
+    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 env0 (recvec.(i)));
+		  my_print_constr env (recvec.(i)));
        with _ -> ());
       let ce = 
 	{ const_entry_body = mkFix ((nvrec,i),recdecls); 
@@ -437,94 +437,13 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
       in
-      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
-      (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
-      (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
-      (*let ce = 
-	{ const_entry_body = evars_def; 
-	  const_entry_type = Some evars_typ;
-	  const_entry_opaque = false;
-	  const_entry_boxed = boxed} in
-      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
-	definition_message fi;
-	trace (str (string_of_id fi) ++ str " is defined");*)
-	let evar_sum =
-	  if evars = [] then None
-	  else (
-	    (try trace (str "Building evars sum for : ");
-	       List.iter
-		 (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t))
-		 evars;
-	     with _ -> ());
-	    let sum = Subtac_utils.build_dependent_sum evars in
-	      (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum));
-	       with _ -> ());
-	      Some sum)
-	in
-	  collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
+      let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
+	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
   let defs = collect_evars 0 [] in
-
-  (* Solve evars then create the definitions *)
-  let real_evars = 
-    filter_map (fun (id, kn, sum) ->
-		  match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
-      defs
-  in
-    match real_evars with
-	[] -> declare (List.rev_map (fun (id, c, _) ->
-				   snd (decompose_lam_n recdefs c)) defs)
-      | l ->
-
-    Subtac_utils.and_tac real_evars
-      (fun f _ gr ->
-	 let _ = trace (str "Got a proof of: " ++ pr_global gr ++
-			str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in
-	 let constant = match gr with Libnames.ConstRef c -> c
-	   | _ -> assert(false)
-	 in
-	   try
-	     (*let value = Environ.constant_value (Global.env ()) constant in*)
-	     let pis = f (mkConst constant) in
-	       (try (trace (str "Accessors: " ++
-			   List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
-			     pis (mt()));
-		    trace (str "Applied existentials: " ++
-			   (List.fold_right
-			      (fun (id, kn, sumg, pi) acc ->
-				 let args = Subtac_utils.destruct_ex pi sumg in
-				   my_print_constr env0 (mkApp (kn, Array.of_list args)))
-			      pis (mt ()))))
-	       with _ -> ());
-	       let rec aux pis acc = function
-		   (id, kn, sum) :: tl ->
-		     (match sum with 
-			  None -> aux pis (kn :: acc) tl
-			| Some (_, sumg) -> 
-			    let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
-			    let args = Subtac_utils.destruct_ex pi sumg in
-			    let args = 
-			      List.map (fun c -> 
-					  try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
-					  with Not_found ->
-					    trace (str "Not_found while reducing " ++
-						   my_print_constr (Global.env ()) c);
-					    c
-				       ) args 				  
-			    in
-			    let _, newdef = decompose_lam_n (recdefs + List.length args) kn in
-			    let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
-			      aux pis (constr :: acc) tl)
-		 | [] -> List.rev acc
-	       in
-		 declare (aux pis [] defs)
-	   with Environ.NotEvaluableConst cer ->
-	     match cer with
-		 Environ.NoBody -> trace (str "Constant has no body")
-	       | Environ.Opaque -> trace (str "Constant is opaque")
-      )
-*)
+    Subtac_obligations.add_mutual_definitions defs
+      
 let out_n = function
     Some n -> n
   | None -> 0
@@ -544,8 +463,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		       errorlabstrm "Subtac_command.build_recursive"
 			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
 	    lnameargsardef
-	in assert(false)
-	     (*build_mutrec lnameargsardef boxed*)
+	in build_mutrec lnameargsardef boxed
 	  
       
       
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 7b13b4023..8bb79a785 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,8 +26,9 @@ 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;
 }
 
 let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
@@ -33,6 +36,18 @@ let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ;
 			     evar_body = Evar_empty ;
 			     evar_extra = None }
 
+let subst_deps obls deps 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))
+    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 +77,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,6 +88,53 @@ 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 ce = 
+    { const_entry_body = subst_body prg;
+      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
+
+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)
+  in
+  let defrec = 
+    Array.of_list (List.map (fun x -> subst_body x) 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 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
+  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;
@@ -113,30 +160,38 @@ 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 = 
+
+let init_prog_info n b t deps obls =
+  let obls' = 
     Array.map
       (fun (n, t, d) ->
          { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
-      e
+      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)
-	    
+    { 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 get_prog name =
@@ -150,15 +205,22 @@ 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)
     else (
-      declare_definition prg';
-      from_prg := ProgMap.remove prg.prg_name !from_prg
-    )		 
+      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 is_defined obls x = obls.(x).obl_body <> None
 
@@ -170,16 +232,6 @@ let deps_remaining obls x =
 	 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
@@ -190,7 +242,7 @@ let subtac_obligation (user_num, name) =
 	    None -> 
 	      (match deps_remaining obls num with
 		  [] ->
-		    let obl = subst_deps obls obl in
+		    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");		   
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 7d93d57bb..a8039300a 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,7 +1,12 @@
 open Util
 
-val add_entry : Names.identifier -> Term.constr -> Term.types ->
-  (Names.identifier * Term.types * Intset.t) array -> unit
+type obligation_info = (Names.identifier * Term.types * Intset.t) array
+
+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
 
 val subtac_obligation : int * Names.identifier option -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index f518f1ccf..d27ef4c16 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -160,4 +160,4 @@ let subtac_proof env isevars id l c tycon =
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
   let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
     trace (str "Adding to obligations list");
-    add_entry id def coqt evars
+    add_definition id def coqt evars