Correct implementation of undo in obligations handling code, correct some bugs in pattern-matching

compilation with multiple matched objects.


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

9 files changed, 101 insertions, 125 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 67bd70baf9..db30c497a1 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -5,7 +5,7 @@ Set Implicit Arguments.
 Notation " {{ x }} " := (tt : { y : unit | x }).
 
 Notation "{ ( x , y )  :  A  |  P }" := 
-  (sig (fun t:A => let (x,y) := t in P))
+  (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident) : type_scope.
 
 Notation " ! " := (False_rect _ _).
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 6285599dc8..9e9a767076 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -109,6 +109,8 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations
     [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> 
     [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" ] -> 
+    [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ]
 | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
 | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
     END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index fc2da8f587..ff5df49e39 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -43,79 +43,6 @@ open Eterm
 let require_library dirpath =
   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
     Library.require_library [qualid] None
-(*
-let subtac_one_fixpoint env isevars (f, decl) = 
-  let ((id, n, bl, typ, body), decl) = 
-    Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
-  in
-  let _ = 
-    try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
-	       Ppconstr.pr_constr_expr body)
-    with _ -> ()
-  in ((id, n, bl, typ, body), decl)
-*)
-	      
-let subtac_fixpoint isevars l = 
-  (* TODO: Copy command.build_recursive *)
-  ()
-(*
-let save id const (locality,kind) hook =
-  let {const_entry_body = pft;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
-  let l,r = match locality with
-    | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
-	let c = SectionLocalDef (pft, tpo, opacity) in
-	let _ = declare_variable id (Lib.cwd(), c, k) in
-	(Local, VarRef id)
-    | Local ->
-        let k = logical_kind_of_goal_kind kind in
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	(Global, ConstRef kn)
-    | Global ->
-        let k = logical_kind_of_goal_kind kind in
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	(Global, ConstRef kn) in
-  Pfedit.delete_current_proof ();
-  hook l r;
-  definition_message id
-
-let save_named opacity =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  save id const persistence hook
-
-let check_anonymity id save_ident =
-  if atompart_of_id id <> "Unnamed_thm" then
-    error "This command can only be used for unnamed theorem"
-(*
-    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
-*)
-
-let save_anonymous opacity save_ident =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  save save_ident const persistence hook
-
-let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,_,hook) = Pfedit.cook_proof () in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const (Global, Proof kind) hook
-
-let subtac_end_proof = function
-  | Admitted -> admit ()
-  | Proved (is_opaque,idopt) ->
-    if_verbose show_script ();
-    match idopt with
-    | None -> save_named is_opaque
-    | Some ((_,id),None) -> save_anonymous is_opaque id
-    | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
-
-	*)
 
 open Pp
 open Ppconstr
@@ -145,11 +72,9 @@ let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgo
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
-(*     if !pcoq <> None then (out_some !pcoq).start_proof () *)
-
+	  
 let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
-
-
+  
 let assumption_message id =
   Options.if_verbose message ((string_of_id id) ^ " is assumed")
 
@@ -181,18 +106,8 @@ let subtac (loc, command) =
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
 		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
-(* 		   let evm, c, ctyp =  in *)
-(* 		     trace (str "Starting proof"); *)
-(* 		     Command.start_proof id goal_kind c hook; *)
-(* 		     trace (str "Started proof");	      *)
-		     
 	       | DefineBody (bl, _, c, tycon) -> 
-		   Subtac_pretyping.subtac_proof env isevars id bl c tycon
-		     (* let tac = Eterm.etermtac (evm, c) in  *)
-		     (* 		     trace (str "Starting proof"); *)
-		     (* 		     Command.start_proof id goal_kind ctyp hook; *)
-		     (* 		     trace (str "Started proof"); *)
-		     (* 		     Pfedit.by tac) *))
+		   Subtac_pretyping.subtac_proof env isevars id bl c tycon)
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index 25922782c0..b51150aa0e 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,3 +1,2 @@
 val require_library : string -> unit
-val subtac_fixpoint : 'a -> 'b -> unit
 val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 7a66660a00..9f465a6e86 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1677,24 +1677,35 @@ let build_ineqs prevpatterns pats liftsign =
 		  None -> None
 		| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
 		    if is_included curpat ppat then
-		      let lens = List.length ppat_sign in (* Length of previous pattern's signature *)
-		      let len' = lens + len in (* Accumulated length of previous pattern's signatures *)
+		      (* Length of previous pattern's signature *)
+		      let lens = List.length ppat_sign in
+		      (* Accumulated length of previous pattern's signatures *)
+		      let len' = lens + len in
+			trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by "
+				  ++ int len');
 		      let acc = 
-			(lift_rel_context len ppat_sign @ sign, (* Jump over previous prevpat signs *)
-			 len',
-			 succ n, (* nth pattern *)
-			 mkApp (Lazy.force eq_ind,
+			((* Jump over previous prevpat signs *)
+			  lift_rel_context len ppat_sign @ sign, 
+			  len',
+			  succ n, (* nth pattern *)
+			  mkApp (Lazy.force eq_ind,
 				[| lift (lens + liftsign) ppat_ty ;
-				   liftn liftsign (succ lens) ppat_c ; 
+				   ppat_c ; 
+				   (*liftn liftsign lens ppat_c ; *)
 				   lift len' curpat_c |]) :: 
-			   List.map (lift lens) c)
+			    List.map 
+			    (fun t -> 
+			      liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *)
+			      (lift lens t (* Jump over this prevpat signature *))) c)
 		      in Some acc
 		    else None)
-	   (Some ([], 0, 1, [])) eqnpats pats
+	   (Some ([], 0, 0, [])) eqnpats pats
 	 in match acc with 
 	     None -> c
 	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) (lift_rel_context liftsign sign) in
+	       let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) 
+		 (lift_rel_context liftsign sign) 
+	       in
 		 conj :: c)
       [] prevpatterns
   in match diffs with [] -> None
@@ -1732,8 +1743,8 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari
 	 let rhs_rels, signlen, arsignlen = 
 	   List.fold_left 
 	     (fun (renv, n, m) (sign,c,(_, args),_) -> 
-		((lift_rel_context n sign) @ renv, List.length sign + n, 
-		 succ (List.length args) + m))
+	       (lift_rel_context n sign @ renv, List.length sign + n, 
+	         succ (List.length args) + m))
 	     ([], 0, 0) pats in
 	 let signenv = push_rel_context rhs_rels env in
 (* 	   trace (str "Env with signature is: " ++ my_print_env signenv); *)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c92e719104..eaa177bce2 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -179,8 +179,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let nc_len = named_context_length nc in
   let pr c = my_print_constr env c in
   let prr = Printer.pr_rel_context env in
-  let prn = Printer.pr_named_context env in
-  let pr_rel env = Printer.pr_rel_context env in
+  let _prn = Printer.pr_named_context env in
+  let _pr_rel env = Printer.pr_rel_context env in
 (*   let _ =  *)
 (*     try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++  *)
 (* 		 Ppconstr.pr_binders bl ++ str " : " ++  *)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 7295fd24da..e2101a2d9d 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,3 +1,4 @@
+(* -*- default-directory: "~/research/coq/trunk/" -*- *)
 open Printf
 open Pp
 open Subtac_utils
@@ -37,7 +38,7 @@ 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 default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic 0)
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
 
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
@@ -83,16 +84,34 @@ let map_first m =
     
 let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 
+let freeze () = !from_prg, !default_tactic_expr
+let unfreeze (v, t) = from_prg := v; set_default_tactic t
+let init () =
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" [])
+
 let _ = 
   Summary.declare_summary "program-tcc-table"
-    { Summary.freeze_function = (fun () -> !from_prg, !default_tactic_expr);
-      Summary.unfreeze_function =
-        (fun (v, t) -> from_prg := v; set_default_tactic t);
-      Summary.init_function =
-        (fun () -> from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []));
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
       Summary.survive_module = false;
       Summary.survive_section = false }
 
+let progmap_union = ProgMap.fold ProgMap.add
+
+let cache (_, (infos, tac)) =
+  from_prg := progmap_union infos !from_prg;
+  default_tactic_expr := tac
+
+let (input,output) = 
+  declare_object
+    { (default_object "Program state") with
+      cache_function = cache ; 
+      load_function = (fun _ -> cache);
+      open_function = (fun _ -> cache);
+      classify_function = (fun _ -> Dispose);
+      export_function = (fun x -> Some x) }
+    
 open Evd
 
 let terms_of_evar ev = 
@@ -221,27 +240,38 @@ let get_prog name =
 
 let obligations_solved prg = (snd prg.prg_obligations) = 0
 
+let update_state s = 
+(*   msgnl (str "Updating obligations info"); *)
+  Lib.add_anonymous_leaf (input s)
+
+let obligations_message rem = 
+  if rem > 0 then
+    if rem = 1 then
+      Options.if_verbose msgnl (int rem ++ str " obligation remaining")
+    else
+      Options.if_verbose msgnl (int rem ++ str " obligations remaining")
+  else
+    Options.if_verbose msgnl (str "No more obligations remaining")
+      
 let update_obls prg obls rem = 
   let prg' = { prg with prg_obligations = (obls, rem) } in
     from_prg := map_replace prg.prg_name prg' !from_prg;
-    if rem > 0 then (
-      Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
-      true)
+    obligations_message rem;
+    if rem > 0 then ()
     else (
-      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;
-	    false
+	    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);
-	      false)
+		     ProgMap.remove x.prg_name acc) !from_prg progs));
+    update_state (!from_prg, !default_tactic_expr);
+    rem
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
@@ -285,7 +315,7 @@ let rec solve_obligation prg num =
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
-		     if update_obls prg obls (pred rem) then
+		     if update_obls prg obls (pred rem) <> 0 then
 		       auto_solve_obligations (Some prg.prg_name));
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
@@ -334,11 +364,12 @@ and solve_obligations n tac =
       obls'
   in
     update_obls prg obls' !rem
-
+      
 and try_solve_obligations n tac = 
   ignore (solve_obligations n tac)
 
-and auto_solve_obligations n =
+and auto_solve_obligations n : unit =
+  Options.if_verbose msgnl (str "Solving obligations automatically...");
   try_solve_obligations n !default_tactic
     
 let add_definition n b t obls =
@@ -353,7 +384,7 @@ let add_definition n b t obls =
     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; 
-      try_solve_obligations (Some n) !default_tactic)
+      auto_solve_obligations (Some n))
 	
 let add_mutual_definitions l nvrec =
   let deps = List.map (fun (n, b, t, obls) -> n) l in
@@ -364,7 +395,7 @@ let add_mutual_definitions l nvrec =
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> try_solve_obligations (Some x) !default_tactic) deps
+    List.iter (fun x -> auto_solve_obligations (Some x)) deps
 
 let admit_obligations n =
   let prg = get_prog n in
@@ -410,3 +441,4 @@ let show_obligations n =
 		    | Some _ -> ())
       obls
 			
+let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 16abb47aaf..0ad9e730d5 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -4,6 +4,7 @@ type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
     (* ident, type, opaque or transparent, dependencies *)
 
 val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
+val default_tactic : unit -> Proof_type.tactic
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   obligation_info -> unit
@@ -15,7 +16,8 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> bool
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> int 
+  (* Number of remaining obligations to be solved for this program *)
 val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index b8d13fe6bc..3ceea173fe 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -70,7 +70,22 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    inversion l0.
+    intros.
+    inversion H.
   Defined.
+
+  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
+    match l, n with
+      | hd :: _, 0 => hd
+      | _ :: tl, S n' => nth' tl n'
+      | nil, _ => !
+    end.
+
+  Next Obligation.
+  Proof.
+    intros.
+    inversion H.
+  Defined.
+
 End Nth.