Facilities to automatically solve obligations

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

9 files changed, 72 insertions, 42 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 449e0abe1e..219cd75bac 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -4,7 +4,7 @@ Notation "'fun' { x : A | P } => Q" :=
   (fun x:{x:A|P} => Q)
   (at level 200, x ident, right associativity).
 
-Notation "( x & y )" := (@exist _ _ x y) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
 Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
 intros.
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index f2e7a999cc..dbb0c4bdb5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -223,22 +223,26 @@ let subtac (loc, command) =
 		++ x ++ spc () ++ str "and" ++ spc () ++ y
 	in msg_warning cmds
     
-    | Type_errors.TypeError (env, e) ->
-	debug 2 (Himsg.explain_type_error env e)
+    | Type_errors.TypeError (env, exn) as e ->
+	debug 2 (Himsg.explain_type_error env exn);
+	raise e
 	  
-    | Pretype_errors.PretypeError (env, e) ->
-	debug 2 (Himsg.explain_pretype_error env e)
+    | Pretype_errors.PretypeError (env, exn) as e ->
+	debug 2 (Himsg.explain_pretype_error env exn);
+	raise e
 	  
     | (Stdpp.Exc_located (loc, e')) as e ->
 	debug 2 (str "Parsing exception: ");
 	(match e' with
-	   | Type_errors.TypeError (env, e) ->
-	       debug 2 (Himsg.explain_type_error env e)
+	   | Type_errors.TypeError (env, exn) ->
+	       debug 2 (Himsg.explain_type_error env exn);
+	       raise e
 		 
-	   | Pretype_errors.PretypeError (env, e) ->
-	       debug 2 (Himsg.explain_pretype_error env e)
+	   | Pretype_errors.PretypeError (env, exn) ->
+	       debug 2 (Himsg.explain_pretype_error env exn);
+	       raise e
 
-	   | e'' -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e'');
+	   | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
 	       raise e)
   
     | e -> 
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 70933e99b4..b11cc9d73d 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -91,7 +91,9 @@ module Coercion = struct
   let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
 
   let rec mu env isevars t =   
+    let isevars = ref isevars in
     let rec aux v = 
+      let v = hnf env isevars v in
       match disc_subset v with
 	  Some (u, p) -> 
 	    let f, ct = aux u in
@@ -135,8 +137,9 @@ module Coercion = struct
 		 | Type x, Type y when x = y -> None (* false *)
 		 | _ -> subco ())
 	  | Prod (name, a, b), Prod (name', a', b') ->
-	      let c1 = coerce_unify env a' a in
+	      let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
 	      let env' = push_rel (name', None, a') env in
+	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	      let c2 = coerce_unify env' b b' in
 		(match c1, c2 with
 		     None, None -> failwith "subtac.coerce': Should have detected equivalence earlier"
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 6725edecaa..e9e26fb88b 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -310,15 +310,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	 (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
 	 evars;
      with _ -> ());    
-    let prog = 
-      {  prg_name = recname;
-	 prg_body = evars_def;
-	 prg_type = fullctyp;
-	 prg_obligations = obligations_of_evars evars;
-      }
-    in
       trace (str "Adding to obligations list");
-      Subtac_obligations.add_entry recname prog;
+      Subtac_obligations.add_entry recname evars_def fullctyp evars;
       trace (str "Added to obligations list")
 
 let build_mutrec l boxed = 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index bc4f4cab4d..195c879c91 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -70,19 +70,41 @@ let declare_definition prg =
   in
     Subtac_utils.definition_message prg.prg_name
     
-let add_entry n e =
-  Options.if_verbose pp (str (string_of_id e.prg_name) ++ str " has type-checked");
-  let nobls = snd e.prg_obligations in
-    match nobls with
-	0 -> Options.if_verbose ppnl (str ".");
-	  declare_definition e
-      | 1 -> 
-	  Options.if_verbose ppnl (str ", generating one obligation");
-	  from_prg := ProgMap.add e.prg_name e !from_prg
-      | n -> 
-	  Options.if_verbose ppnl (str ", generating " ++ int n ++ str " obligations");
-	  from_prg := ProgMap.add e.prg_name e !from_prg
-	        
+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 = 
+    List.fold_left 
+      (fun acc (n, t) ->
+	 let ev = { evar_concl = t ; evar_body = Evar_empty ; 
+		    evar_hyps = Environ.empty_named_context_val ; evar_extra = None } 
+	 in 
+	 let cstr = 
+	   try
+	     let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in	       
+	       Some c
+	   with _ -> None
+	 in { obl_name = n ; obl_type = t; obl_body = cstr } :: acc)
+      [] e
+  in
+    match obls with
+	[] -> Options.if_verbose ppnl (str ".");
+	  declare_definition { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = ([||], 0) }
+      | l -> 
+	  let len = List.length l in
+	  let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+	  let obls = try_tactics l in
+	  let rem = List.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 = (Array.of_list 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
+		
+(*		
 let (theory_to_obj, obj_to_theory) = 
   let cache_th (name,th) = add_entry name th
   and export_th x = Some x in
@@ -93,7 +115,7 @@ let (theory_to_obj, obj_to_theory) =
       subst_function = (fun _ -> assert(false));
       classify_function = (fun (_,x) -> Dispose);
       export_function = export_th }
-
+*)
 
 let error s = Util.error s
 
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
new file mode 100644
index 0000000000..4132729806
--- /dev/null
+++ b/contrib/subtac/subtac_obligations.mli
@@ -0,0 +1,3 @@
+val add_entry : Names.identifier -> (Term.constr list -> Term.constr) -> Term.types -> (Names.identifier * Term.types) 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 6f7aaa5cc7..b3f8e22106 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -159,12 +159,5 @@ let subtac_proof env isevars id l c tycon =
   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 prog = 
-    {  prg_name = id;
-       prg_body = evars_def;
-       prg_type = coqt;
-       prg_obligations = obligations_of_evars evars;
-    }
-  in
     trace (str "Adding to obligations list");
-    add_entry id prog
+    add_entry id evars_def coqt evars
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 5fbbbc2be1..3248ed30df 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -87,7 +87,7 @@ let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
-let debug_level = 2
+let debug_level = 1
 
 let debug_on = true
 
@@ -437,3 +437,13 @@ let recursive_message v =
     | 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")
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let solve_by_tac ev t =
+  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
+  let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
+  let ts = Tacmach.mk_pftreestate goal in
+  let solved_state = Tacmach.solve_pftreestate t ts in
+  let c = Tacmach.extract_pftreestate solved_state in
+    debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
+    c
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 7f3d3640ae..c8afd9f8b3 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -94,3 +94,5 @@ val id_of_name : name -> identifier
 
 val definition_message : identifier -> unit
 val recursive_message : global_reference array -> std_ppcmds
+
+val solve_by_tac : evar_info -> Tacmach.tactic -> constr