Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

1 files changed, 133 insertions, 72 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d6c1772f..d182f7cd 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
@@ -12,12 +13,22 @@ open Decl_kinds
 open Util
 open Evd
 
-type obligation_info = (Names.identifier * Term.types * Intset.t) array
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
+
+exception NoObligations of identifier option
+
+let explain_no_obligations = function
+    Some ident -> str "No obligations for program " ++ str (string_of_id ident)
+  | None -> str "No obligations remaining"
+
+type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
 
 type obligation =
     { obl_name : identifier;
       obl_type : types;
       obl_body : constr option;
+      obl_opaque : bool;
       obl_deps : Intset.t;
     }
 
@@ -36,8 +47,9 @@ 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 ())
 
-let set_default_tactic t = default_tactic := t
+let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
 let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
 			     evar_concl = o.obl_type ; 
@@ -81,26 +93,35 @@ 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);
-      Summary.unfreeze_function =
-        (fun v -> from_prg := v);
-      Summary.init_function =
-        (fun () -> from_prg := ProgMap.empty);
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-open Evd
+let progmap_union = ProgMap.fold ProgMap.add
 
-let terms_of_evar ev = 
-  match ev.evar_body with
-      Evar_defined b ->
-	let nc = Environ.named_context_of_val ev.evar_hyps in
-	let body = Termops.it_mkNamedLambda_or_LetIn b nc in
-	let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
-	  body, typ
-    | _ -> assert(false)
+let cache (_, (infos, tac)) =
+  from_prg := infos;
+  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 rec intset_to = function
     -1 -> Intset.empty
@@ -113,7 +134,8 @@ let subst_body prg =
 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);
+		  my_print_constr (Global.env()) body ++ str " : " ++ 
+		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
   let ce = 
     { const_entry_body = body;
@@ -163,7 +185,7 @@ let declare_obligation obl body =
   let ce = 
     { const_entry_body = body;
       const_entry_type = Some obl.obl_type;
-      const_entry_opaque = false;
+      const_entry_opaque = obl.obl_opaque;
       const_entry_boxed = false} 
   in
   let constant = Declare.declare_constant obl.obl_name 
@@ -190,42 +212,53 @@ let red = Reductionops.nf_betaiota
 let init_prog_info n b t deps nvrec obls =
   let obls' = 
     Array.mapi
-      (fun i (n, t, d) ->
+      (fun i (n, t, o, 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_type = red t; obl_opaque = o;
 	   obl_deps = d })
       obls
   in
     { 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 -> 
 	  (try ProgMap.find n prg_infos
-	   with Not_found -> error ("No obligations for program " ^ string_of_id n))
+	   with Not_found -> raise (NoObligations (Some n)))
       | None -> 
 	  (let n = map_cardinal prg_infos in
 	     match n with 
-		 0 -> error "No obligations remaining"
+		 0 -> raise (NoObligations None)
 	       | 1 -> map_first prg_infos
 	       | _ -> error "More than one program with unsolved obligations")
 
+let get_prog_err n = 
+  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
+
 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");
-    )
+    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';
@@ -235,7 +268,10 @@ let update_obls prg obls rem =
 	      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))
+		   (fun acc x -> 
+		     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
 
@@ -246,7 +282,24 @@ let deps_remaining obls deps =
 	 else x :: acc)
       deps []
 
-let solve_obligation prg num =
+let kind_of_opacity o =
+  if o then Subtac_utils.goal_proof_kind
+  else Subtac_utils.goal_kind
+   
+let obligations_of_evars evars =
+  let arr = 
+    Array.of_list
+      (List.map
+	 (fun (n, t) ->
+	    { obl_name = n;
+	      obl_type = t;
+	      obl_body = None;
+	      obl_opaque = false;
+	      obl_deps = Intset.empty;
+	    }) evars)
+  in arr, Array.length arr
+
+let rec solve_obligation prg num =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -256,22 +309,23 @@ let solve_obligation prg num =
       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
+	      Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) 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));
+		     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);
 	      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) =
+and subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
-  let prg = get_prog name in
+  let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num < Array.length obls then
       let obl = obls.(num) in
@@ -280,20 +334,8 @@ let subtac_obligation (user_num, name, typ) =
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
       
-      
-let obligations_of_evars evars =
-  let arr = 
-    Array.of_list
-      (List.map
-	 (fun (n, t) ->
-	    { obl_name = n;
-	      obl_type = t;
-	      obl_body = None;
-	      obl_deps = Intset.empty;
-	    }) evars)
-  in arr, Array.length arr
-
-let solve_obligation_by_tac prg obls i tac =
+   
+and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
   match obl.obl_body with 
       Some _ -> false
@@ -302,13 +344,15 @@ let solve_obligation_by_tac prg obls i tac =
 	   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 };
+	       if obl.obl_opaque then 
+		 obls.(i) <- declare_obligation obl t
+	       else
+		 obls.(i) <- { obl with obl_body = Some t };
 	       true		 
 	   else false
 	 with _ -> false)  
 
-let solve_obligations n tac = 
-  let prg = get_prog n in
+and solve_prg_obligations prg tac = 
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
@@ -320,6 +364,27 @@ let solve_obligations n tac =
   in
     update_obls prg obls' !rem
 
+and solve_obligations n tac = 
+  let prg = get_prog_err n in
+    solve_prg_obligations prg tac
+
+and solve_all_obligations tac = 
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+      
+and try_solve_obligation n prg tac = 
+  let prg = get_prog prg in 
+  let obls, rem = prg.prg_obligations in
+  let obls' = Array.copy obls in
+    if solve_obligation_by_tac prg obls' n tac then
+      ignore(update_obls prg obls' (pred rem));
+    
+and try_solve_obligations n tac = 
+  try ignore (solve_obligations n tac) with NoObligations _ -> ()
+
+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 =
   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
@@ -332,7 +397,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; 
-      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
@@ -343,22 +408,21 @@ let add_mutual_definitions l nvrec =
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> 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
+  let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
-  let obls' = 
-    Array.mapi (fun i x -> 
+    Array.iteri (fun i x -> 
 		 match x.obl_body with 
 		     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' 0
+                       let x = subst_deps_obl obls x in
+		       let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+			 assumption_message x.obl_name;
+			 obls.(i) <- { x with obl_body = Some (mkConst kn) }
+		   | Some _ -> ())
+      obls;
+    ignore(update_obls prg obls 0)
 
 exception Found of int
 
@@ -367,21 +431,17 @@ let array_find f arr =
     raise Not_found
   with Found i -> i
 
-let rec next_obligation n =
-  let prg = get_prog n in
+let next_obligation n =
+  let prg = get_prog_err 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
+  in solve_obligation prg i
       
 open Pp
 let show_obligations n =
-  let prg = get_prog n in
+  let prg = get_prog_err n in
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
     msgnl (int rem ++ str " obligation(s) remaining: ");
@@ -392,3 +452,4 @@ let show_obligations n =
 		    | Some _ -> ())
       obls
 			
+let default_tactic () = !default_tactic