Subtac fixes, new way of handling obligations in progress.

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

8 files changed, 91 insertions, 90 deletions

diff --git a/Makefile b/Makefile
index b71c7c5aa..ed029f4eb 100644
--- a/Makefile
+++ b/Makefile
@@ -292,19 +292,13 @@ FOCMO=\
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
   contrib/cc/g_congruence.cmo 
 
-SUBTACCMO=\
-	contrib/subtac/subtac_utils.cmo \
-	contrib/subtac/eterm.cmo \
-	contrib/subtac/g_eterm.cmo \
-	contrib/subtac/context.cmo \
-	contrib/subtac/subtac_errors.cmo \
-	contrib/subtac/subtac_coercion.cmo \
-	contrib/subtac/subtac_pretyping_F.cmo \
-	contrib/subtac/subtac_pretyping.cmo \
-	contrib/subtac/subtac_interp_fixpoint.cmo \
-	contrib/subtac/subtac_command.cmo \
-	contrib/subtac/subtac.cmo \
-	contrib/subtac/g_subtac.cmo
+SUBTACCMO=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
+  contrib/subtac/g_eterm.cmo contrib/subtac/context.cmo \
+  contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \
+  contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \
+  contrib/subtac/subtac_interp_fixpoint.cmo contrib/subtac/subtac_obligations.cmo \
+  contrib/subtac/subtac_command.cmo contrib/subtac/subtac.cmo \
+  contrib/subtac/g_subtac.cmo
 
 
 RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 859f90136..678655186 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -38,7 +38,6 @@ let subst_evars evs n t =
   let evar_info id = 
     let rec aux i = function
 	(k, h, v) :: tl -> 
-	  trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
 	  if k = id then (i, h, v) else aux (succ i) tl
       | [] -> raise Not_found
     in 
@@ -96,7 +95,9 @@ let etype_of_evar evs ev hyps =
       (id, copt, t) :: tl ->
 	let t' = subst_evars evs n t in
 	let t'' = subst_vars acc 0 t' in
- 	  mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
+	let copt' = option_map (subst_evars evs n) copt in
+	let copt' = option_map (subst_vars acc 0) copt' in
+ 	  mkNamedProd_or_LetIn (id, copt', t'') (aux (id :: acc) (succ n) tl)
     | [] ->
 	let t' = subst_evars evs n ev.evar_concl in
 	  subst_vars acc 0 t'	
@@ -108,7 +109,7 @@ 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 = List.rev (to_list evm) in
+  let evl = to_list evm in
     trace (str "Eterm, transformed to list");
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
@@ -116,7 +117,9 @@ let eterm_term evm t tycon =
       (fun (id, ev) l ->
 	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
-	 let y' = (id, hyps, etype_of_evar l ev 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 
@@ -124,7 +127,8 @@ let eterm_term evm t tycon =
     subst_evars evts 0 t 
   in
   let evar_names = 
-    List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
+    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
@@ -133,26 +137,17 @@ let eterm_term evm t tycon =
     (* 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
-  let _declare_evar (id, c) =
-    let id = id_of_string ("Evar" ^ string_of_int id) in
-      ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
-					  Decl_kinds.IsAssumption Decl_kinds.Definitional))
-  in
-  let _declare_assert acc (id, c) =
-    let id = id_of_string ("Evar" ^ string_of_int id) in
-      tclTHEN acc (Tactics.assert_tac false (Name id) c)
+    (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);
+		Termops.print_constr_env (Global.env ()) t);
        trace (str "Term constructed in eterm" ++ spc () ++
-	      Termops.print_constr_env (Global.env ()) t'');
+		Termops.print_constr_env (Global.env ()) t'');
        ignore(option_map 
 		(fun typ ->
 		   trace (str "Type :" ++ spc () ++
-			  Termops.print_constr_env (Global.env ()) typ))
+			    Termops.print_constr_env (Global.env ()) typ))
 		tycon);
      with _ -> ());
     t'', tycon, evar_names
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 55e60199f..cd26e817c 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -47,6 +47,7 @@ GEXTEND Gram
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g ] ]
     ;
+       
   END
 
 type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
@@ -57,6 +58,7 @@ let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_arg
   Genarg.create_arg "subtac_gallina_loc"
 
 VERNAC COMMAND EXTEND Subtac
-[ "Program" subtac_gallina_loc(g) ] -> 
-  [ Subtac.subtac g ]
+[ "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) ]      
 END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index fed61fb4c..d1ac74b24 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -229,18 +229,20 @@ let subtac (loc, command) =
     | Pretype_errors.PretypeError (env, e) ->
 	debug 2 (Himsg.explain_pretype_error env e)
 	  
-    | Stdpp.Exc_located (loc, e) ->
+    | (Stdpp.Exc_located (loc, e')) as e ->
 	debug 2 (str "Parsing exception: ");
-	(match e with
+	(match e' with
 	   | Type_errors.TypeError (env, e) ->
 	       debug 2 (Himsg.explain_type_error env e)
 		 
 	   | Pretype_errors.PretypeError (env, e) ->
 	       debug 2 (Himsg.explain_pretype_error env e)
 
-	   | e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e))
+	   | e'' -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e'');
+	       raise e)
   
     | e -> 
-	msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e)
+	msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
+	raise e
 
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c738d7a64..c173d7724 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -149,15 +149,6 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
-let definition_message id =
-  Options.if_verbose message ((string_of_id id) ^ " is defined")
-
-let recursive_message v =
-  match Array.length v with
-    | 0 -> error "no recursive definition"
-    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
-    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
-		    spc () ++ str "are recursively defined")
 
 let filter_map f l = 
   let rec aux acc = function
@@ -184,6 +175,11 @@ let rec gen_rels = function
     0 -> []
   | n -> mkRel n :: gen_rels (pred n)
 
+let id_of_name = function
+    Anonymous -> raise (Invalid_argument "id_of_name")
+  | Name n -> n
+
+ 
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
@@ -204,25 +200,35 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let argid = match argname with Name n -> n | _ -> assert(false) in
   let _liftafter = lift_binders 1 after_length after in
   let envwf = push_rel_context before env in
-  let wf_rel, measure_fn = 
-    let rconstr = interp_constr isevars envwf r in
-    if measure then
-      let lt_rel = constr_of_global (Lazy.force lt_ref) in
-      let name s = Name (id_of_string s) in
-	mkLambda (name "x", argtyp,
-		  mkLambda (name "y", argtyp,
-			    mkApp (lt_rel,
-				   [| mkApp (rconstr, [| mkRel 2 |]) ;
-				      mkApp (rconstr, [| mkRel 1 |]) |]))),
-	Some rconstr
-    else rconstr, None
+  let wf_rel, wf_rel_fun, measure_fn = 
+    let rconstr_body, rconstr = 
+      let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
+       let env = push_rel_context [arg] envwf in
+       let capp = interp_constr isevars env app in
+ 	capp, mkLambda (argname, argtyp, capp)
+     in
+       if measure then
+ 	let lt_rel = constr_of_global (Lazy.force lt_ref) in
+ 	let name s = Name (id_of_string s) in
+ 	let wf_rel_fun = 
+ 	  (fun x y ->
+ 	      mkApp (lt_rel, [| subst1 x rconstr_body; 
+ 				subst1 y rconstr_body |])) 
+ 	in
+ 	let wf_rel = 
+ 	  mkLambda (name "x", argtyp,
+ 		    mkLambda (name "y", lift 1 argtyp,
+ 			      wf_rel_fun (mkRel 2) (mkRel 1)))
+ 	in
+ 	  wf_rel, wf_rel_fun , Some rconstr
+       else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
   in
   let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
   in
   let argid' = id_of_string (string_of_id argid ^ "'") in
   let wfarg len = (Name argid', None, 
-		   mkSubset (Name argid') argtyp 
-		     (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+  		   mkSubset (Name argid') argtyp 
+		     (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let top_bl = after @ (arg :: before) in
   let intern_bl = after @ (wfarg 1 :: arg :: before) in
@@ -234,7 +240,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let projection = 
     mkApp (proj, [| argtyp ;
 		    (mkLambda (Name argid', argtyp,
-			       (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+			       (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
 		    mkRel 1
 		 |])
   in
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 90ffb8925..846e06cfb 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -37,7 +37,6 @@ val interp_constr_judgment :
   env ->
   constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
-val recursive_message : global_reference array -> std_ppcmds
 
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d4db7c278..702410230 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -88,17 +88,25 @@ let my_print_tycon_type = Evarutil.pr_tycon_type
 
 let debug_level = 2
 
+let debug_on = false
+
 let debug n s = 
-  if !Options.debug && n >= debug_level then
-    msgnl s
+  if debug_on then
+    if !Options.debug && n >= debug_level then
+      msgnl s
+    else ()
   else ()
 
 let debug_msg n s = 
-  if !Options.debug  && n >= debug_level then s
+  if debug_on then
+    if !Options.debug  && n >= debug_level then s
+    else mt ()
   else mt ()
 
 let trace s = 
-  if !Options.debug  && debug_level > 0 then msgnl s
+  if debug_on then
+    if !Options.debug  && debug_level > 0 then msgnl s
+    else ()
   else ()
 
 let wf_relations = Hashtbl.create 10
@@ -167,30 +175,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
 open Tactics
 open Tacticals
 
-let build_dependent_sum l =
-  let rec aux (tac, typ) = function
-      (n, t) :: tl ->
-	let t' = mkLambda (Name n, t, typ) in
-	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
-	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)	    	     
-	   with _ -> ());
-	let tac' = 
-	  tclTHENS (assert_tac true (Name n) t) 
-	    ([intros;
-	      (tclTHENSEQ 
-		 [constructor_tac (Some 1) 1 
-		    (Rawterm.ImplicitBindings [mkVar n]);
-		  tac]);
-	     ])
-	in
-	let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
-	  aux (tac', newt) tl
-    | [] -> tac, typ
-  in 
-    match l with 
-	(_, hd) :: tl -> aux (intros, hd) tl
-      | [] -> raise (Invalid_argument "build_dependent_sum")
-
 let id x = x
 
 let build_dependent_sum l =
@@ -438,3 +422,17 @@ let rewrite_cases env c =
   let c' = rewrite_cases c in
   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
     c'
+
+let id_of_name = function
+    Name n -> n
+  | Anonymous -> raise (Invalid_argument "id_of_name")
+
+let definition_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+let recursive_message v =
+  match Array.length v with
+    | 0 -> error "no recursive definition"
+    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+		    spc () ++ str "are recursively defined")
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 4a7e81772..9eed53e4e 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -88,3 +88,8 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
 val destruct_ex : constr -> constr -> constr list
 
 val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
+
+val id_of_name : name -> identifier
+
+val definition_message : identifier -> unit
+val recursive_message : global_reference array -> std_ppcmds