Work on obligation separation.

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

7 files changed, 139 insertions, 191 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9c11569ef..b95f643a5 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -32,71 +32,33 @@ let list_assoc_index x l =
     | [] -> raise Not_found
   in aux 0 l
 
+
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
-let subst_evars evs n t = 
-  let evar_info id = 
-    let rec aux i = function
-	(k, h, v) :: tl -> 
-	  if k = id then (i, h, v) else aux (succ i) tl
-      | [] -> raise Not_found
-    in 
-    let (idx, hyps, v) = aux 0 evs in
-      n + idx + 1, hyps
-  in
-  let rec substrec depth c = match kind_of_term c with
-    | Evar (k, args) ->
-	(let index, hyps = 
-	   try evar_info k
-	   with Not_found -> 
-	     anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
-	 in
-	 (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
-		       int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
-	 let ex = mkRel (index + depth) in
-	   (* Evar arguments are created in inverse order, 
-	      and we must not apply to defined ones (i.e. LetIn's)
-	   *)
-	 let args =
-	   let rec aux hyps args acc =
-	     match hyps, args with
-		 ((_, None, _) :: tlh), (c :: tla) -> 
-		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
-	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
-		   aux tlh tla acc
-	       | [], [] -> acc
-	       | _, _ -> acc (* failwith "subst_evars: invalid argument" *)
-	   in aux hyps (Array.to_list args) [] 
-	 in
-	   mkApp (ex, Array.of_list args))
-    | _ -> map_constr_with_binders succ substrec depth c
-  in 
-    substrec 0 t
-
 let subst_evar_constr evs n t = 
+  let seen = ref Intset.empty in
   let evar_info id = 
     let rec aux i = function
-	(k, n, h, v) :: tl -> 
-	  if k = id then (n, h, v) else aux (succ i) tl
+	(k, x) :: tl -> 
+	  if k = id then x else aux (succ i) tl
       | [] -> raise Not_found
-    in 
-    let (c, hyps, v) = aux 0 evs in
-      c, hyps
+    in aux 0 evs
   in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
-	(let ex, hyps = 
-	   try evar_info k
-	   with Not_found -> 
-	     anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
-	 in
-	   (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
-		       int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
-	   (* Evar arguments are created in inverse order, 
-	      and we must not apply to defined ones (i.e. LetIn's)
-	   *)
-	 let args =
-	   let rec aux hyps args acc =
+	let (id, idstr), hyps, _, _ = 
+	  try evar_info k
+	  with Not_found -> 
+	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+	in
+        seen := Intset.add id !seen;
+	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+			int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
+	  (* Evar arguments are created in inverse order, 
+	     and we must not apply to defined ones (i.e. LetIn's)
+	  *)
+	let args =
+	  let rec aux hyps args acc =
 	     match hyps, args with
 		 ((_, None, _) :: tlh), (c :: tla) -> 
 		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
@@ -106,10 +68,11 @@ let subst_evar_constr evs n t =
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
 	   in aux hyps (Array.to_list args) [] 
 	 in
-	   mkApp (ex, Array.of_list args))
+	   mkApp (mkVar idstr, Array.of_list args)
     | _ -> map_constr_with_binders succ substrec depth c
   in 
-    substrec 0 t
+  let t' = substrec 0 t in
+    t', !seen
 
       
 (** Substitute variable references in t using De Bruijn indices, 
@@ -127,70 +90,31 @@ let subst_vars acc n t =
 
 (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
   to a product : forall H1 : t1, ..., forall Hn : tn, concl.
-  Changes evars and hypothesis references to De Bruijn indices.
+    Changes evars and hypothesis references to variable references.
 *)
 let etype_of_evar evs ev hyps =
   let rec aux acc n = function
       (id, copt, t) :: tl ->
-	let t' = subst_evars evs n t in
+	let t', s = subst_evar_constr evs n t in
 	let t'' = subst_vars acc 0 t' in
-	let copt' = option_map (subst_evars evs n) copt in
+	let copt', s = 
+	  match copt with
+	      Some c -> 
+		let c', s' = subst_evar_constr evs n c in
+		  Some c', Intset.union s s'
+	    | None -> None, s
+	in
 	let copt' = option_map (subst_vars acc 0) copt' in
- 	  mkNamedProd_or_LetIn (id, copt', t'') (aux (id :: acc) (succ n) tl)
+ 	let rest, s' = aux (id :: acc) (succ n) tl in
+	  mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s
     | [] ->
-	let t' = subst_evars evs n ev.evar_concl in
-	  subst_vars acc 0 t'	
+	let t', s = subst_evar_constr evs n ev.evar_concl in
+	  subst_vars acc 0 t', s
   in aux [] 0 (rev hyps)
 
 
 open Tacticals
     
-let eterm_term 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
-    trace (str "Eterm, transformed to list");
-  let evts = 
-    (* Remove existential variables in types and build the corresponding products *)
-    fold_right 
-      (fun (id, ev) l ->
-	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
-	 let hyps = Environ.named_context_of_val ev.evar_hyps in
-	 let evtyp = etype_of_evar l ev hyps in
-	   trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
-	 let y' = (id, hyps, evtyp) in
-	   y' :: l) 
-      evl []
-  in 
-  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
-    subst_evars evts 0 t 
-  in
-  let evar_names = 
-    let i = ref 0 in
-      List.map (fun (id, _, c) -> incr i; (id_of_string ("evar_" ^ string_of_int !i)), c) evts
-  in
-  let evar_bl =
-    List.map (fun (id, c) -> Name id, None, c) evar_names
-  in
-  let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
-    (* Generalize over the existential variables *)
-  let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl 
-  and tycon = option_map 
-    (fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
-  in
-    (try 
-       trace (str "Term given to eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t);
-       trace (str "Term constructed in eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t'');
-       ignore(option_map 
-		(fun typ ->
-		   trace (str "Type :" ++ spc () ++
-			    Termops.print_constr_env (Global.env ()) typ))
-		tycon);
-     with _ -> ());
-    t'', tycon, evar_names
-
 let rec take n l = 
   if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)    
 
@@ -203,34 +127,30 @@ let eterm_obligations name nclen evm t tycon =
      refer to previous existentials in the list only *)
   let evl = 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
+  in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
     fold_right 
-      (fun (id, ev) l ->
+      (fun (id, (n, nstr), ev) l ->
 	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
 	 let hyps = trunc_named_context nclen hyps in
-	   trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
-	 let evtyp = etype_of_evar l ev hyps in
-	   trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
-	 let y' = (id, hyps, evtyp) 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);
+	 let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
 	   y' :: l) 
-      evl []
+      evn []
   in 
-  let evar_names = 
-    let i = ref 0 in
-      List.map (fun (id, h, c) -> incr i; 
-		  (id, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i), h, c)) evts
-  in
-  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
-    subst_evar_constr (List.map (fun (id, n, h, c) -> id, mkVar n, h, c) evar_names) 0 t 
+  let t', _ = (* Substitute evar refs in the term by variables *)
+    subst_evar_constr evts 0 t 
   in
-  let _, evars =
-    fold_right
-      (fun (_, n, h, c) (acc, l) ->
-	 let evt = Termops.it_mkProd_wo_LetIn c acc in
-	   ((Name n, None, c) :: acc, (n, evt) :: l))
-      evar_names ([], [])
+  let evars = 
+    List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
   in
     (try 
        trace (str "Term given to eterm" ++ spc () ++
@@ -238,26 +158,12 @@ let eterm_obligations name nclen evm t tycon =
        trace (str "Term constructed in eterm" ++ spc () ++
 		Termops.print_constr_env (Global.env ()) t');
        ignore(iter
-		(fun (n, typ) ->
-		   trace (str "Evar :" ++ spc () ++ str (string_of_id n) ++
+		(fun (name, typ, deps) ->
+		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
 			    Termops.print_constr_env (Global.env ()) typ))
 		evars);
      with _ -> ());
-    let subst_closure l = 
-      let l' = List.map2 (fun (id, _, h, c) cst -> (id, cst, h, c)) evar_names l in
-      let _, l'' = 
-	List.fold_right 
-	  (fun (id, cst, h, c) (acc, res) ->
-	     let cst' = applist (cst, List.rev acc) in
-	       (cst' :: acc, (id, cst', h, c) :: res))
-	  l' ([], [])
-      in
-      let t' = subst_evar_constr l'' 0 t in
-	trace (str "Term constructed in eterm" ++ spc () ++
-		 Termops.print_constr_env (Global.env ()) t');
-	t'
-    in
-      subst_closure, evars
+    Array.of_list evars, t'
 
 let mkMetas n = 
   let rec aux i acc = 
@@ -265,12 +171,12 @@ let mkMetas n =
     else acc
   in aux n []
 
-let eterm evm t (tycon : types option) = 
-  let t, tycon, evs = eterm_term evm t tycon in
-    match tycon with
-	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) []
-      | None -> Tactics.apply_term t (mkMetas (List.length evs))
+(* let eterm evm t (tycon : types option) =  *)
+(*   let t, tycon, evs = eterm_term evm t tycon in *)
+(*     match tycon with *)
+(* 	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *)
+(*       | None -> Tactics.apply_term t (mkMetas (List.length evs)) *)
      
-open Tacmach
+(* open Tacmach *)
 
-let etermtac (evm, t) = eterm evm t None
+let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index dec9efa8b..77d9f293d 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -12,12 +12,13 @@ open Tacmach
 open Term
 open Evd
 open Names
+open Util
 
 val mkMetas : int -> constr list
 
-val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
 val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> 
-  (constr list -> constr) * (identifier * types) list
+  (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index ff3bcb82e..1ec77c690 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -30,6 +30,7 @@ open Topconstr
 
 module Gram = Pcoq.Gram
 module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
 
 module SubtacGram =
 struct
@@ -76,4 +77,8 @@ VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
 | [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ]
 | [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ]      
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
+| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
 END
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index e9e26fb88..b433af2cc 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -304,16 +304,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   in
   let evm = non_instanciated_map env isevars in
   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
-  let evars_def, evars = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
     (try trace (str "Generated obligations : ");
-       List.iter
-	 (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+       Array.iter
+	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
 	 evars;
      with _ -> ());    
       trace (str "Adding to obligations list");
       Subtac_obligations.add_entry recname evars_def fullctyp evars;
       trace (str "Added to obligations list")
-
+(*
 let build_mutrec l boxed = 
   let sigma = Evd.empty
   and env0 = Global.env()
@@ -524,7 +524,7 @@ let build_mutrec l boxed =
 		 Environ.NoBody -> trace (str "Constant has no body")
 	       | Environ.Opaque -> trace (str "Constant is opaque")
       )
-
+*)
 let out_n = function
     Some n -> n
   | None -> 0
@@ -544,8 +544,8 @@ 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
-	  build_mutrec lnameargsardef boxed
+	in assert(false)
+	     (*build_mutrec lnameargsardef boxed*)
 	  
       
       
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 195c879c9..859180036 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -71,7 +71,7 @@ let declare_definition prg =
     Subtac_utils.definition_message prg.prg_name
     
 open Evd
-
+      
 let add_entry n b t obls =
   Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let try_tactics e = 
@@ -103,26 +103,11 @@ let add_entry n b t obls =
 	      declare_definition prg
 	    else
 	      from_prg := ProgMap.add n prg !from_prg
-		
-(*		
-let (theory_to_obj, obj_to_theory) = 
-  let cache_th (name,th) = add_entry name th
-  and export_th x = Some x in
-  declare_object
-    {(default_object "program-tcc") with
-      open_function = (fun i o -> if i=1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = (fun _ -> assert(false));
-      classify_function = (fun (_,x) -> Dispose);
-      export_function = export_th }
-*)
 
 let error s = Util.error s
 
-let subtac_obligation (user_num, name) =
-  let num = pred user_num in
+let get_prog name =
   let prg_infos = !from_prg in
-  let prg = 
     match name with
 	Some n -> ProgMap.find n prg_infos
       | None -> 
@@ -131,7 +116,20 @@ let subtac_obligation (user_num, name) =
 		 0 -> error "No obligations remaining"
 	       | 1 -> map_first prg_infos
 	       | _ -> error "More than one program with unsolved obligations")
-  in
+
+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
+    )		 
+	    
+let subtac_obligation (user_num, name) =
+  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
@@ -143,14 +141,7 @@ let subtac_obligation (user_num, name) =
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
-		   let prg' = { prg with prg_obligations = (obls, pred 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
-		     ));
+		     update_obls prg obls (pred rem));
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof")
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
@@ -166,3 +157,41 @@ let obligations_of_evars evars =
 	      obl_body = None;
 	    }) 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
+  let rem = ref rem in
+  let obls' = 
+    Array.map (fun 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)
+      obls
+  in
+    update_obls prg obls' !rem
+
+open Pp
+let show_obligations n =
+  let prg = get_prog n 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 i ++ str " : " ++ spc () ++ 
+					my_print_constr (Global.env ()) x.obl_type)
+		    | Some _ -> ())
+      obls
+			
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 413272980..7d93d57bb 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,3 +1,10 @@
-val add_entry : Names.identifier -> (Term.constr list -> Term.constr) -> Term.types -> (Names.identifier * Term.types) list -> unit
+open Util
+
+val add_entry : Names.identifier -> Term.constr -> Term.types ->
+  (Names.identifier * Term.types * Intset.t) array -> unit
 
 val subtac_obligation : int * Names.identifier option -> unit
+
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+
+val show_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index b3f8e2210..f518f1ccf 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -158,6 +158,6 @@ let subtac_proof env isevars id l c tycon =
   let nc = named_context env in
   let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars_def, evars = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+  let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
     trace (str "Adding to obligations list");
-    add_entry id evars_def coqt evars
+    add_entry id def coqt evars