Ajout de l'axiome du but prouve par la tactique simplifi

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

1 files changed, 69 insertions, 33 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 417d74b6df..6e9fdac6ee 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -9,7 +9,9 @@ open Tacmach
 open Fol
 open Names
 open Nameops
+open Termops
 open Coqlib
+open Hipattern
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
@@ -19,6 +21,16 @@ let coq_modules =
 let constant = gen_constant_in_modules "Omega" coq_modules
 
 let coq_Z = lazy (constant "Z")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zdiv = lazy (constant "Zdiv")
+let coq_Zs = lazy (constant "Zs")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
 
 (* not Prop typed expressions *)
 exception NotProp
@@ -27,23 +39,70 @@ exception NotProp
 exception NotFO
 
 (* assumption: t:Set *)
-let tr_type env t =
+let rec tr_type env t =
   if t = Lazy.force coq_Z then Base "INT"
+  else if is_Prop t then Base "BOOLEAN"
+  else if is_Set t then Base "TYPE"
+  else if is_imp_term t then 
+    begin match match_with_imp_term t with
+      | Some (t1, t2) -> Arrow (tr_type env t1, tr_type env t2)
+      | _ -> assert false
+    end
+  (* else if then *)
   else raise NotFO
 
 (* assumption: t:T:Set *)
-let tr_term env t =
+let rec tr_term env t =
   match kind_of_term t with
-    | Var id -> Tvar (string_of_id id)
-    | _ -> raise NotFO
+    | Var id -> 
+	Tvar (string_of_id id)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
+	Plus (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
+	Moins (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
+	Mult (tr_term env a, tr_term env b)
+    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
+	Div (tr_term env a, tr_term env b)
+    | Term.App (f, cl) -> 
+	begin try
+	  let r = Libnames.reference_of_constr f in
+	  let s = string_of_id (Nametab.id_of_global r) in
+	  App (s, List.map (tr_term env) (Array.to_list cl))
+	with Not_found ->
+	  raise NotFO
+	end
+    | _ -> 
+	raise NotFO
 
 (* assumption: f is of type Prop *)
-let tr_formula env f =
+let rec tr_formula env f =
   let c, args = decompose_app f in
   match kind_of_term c, args with
+    | Var id, [] -> 
+	Fvar (string_of_id id)
     | _, [t;a;b] when c = build_coq_eq () -> 
 	(* TODO: verifier type t *)
 	Fatom (Eq (tr_term env a, tr_term env b))
+    | _, [a;b] when c = Lazy.force coq_Zle ->
+	Fatom (Le (tr_term env a, tr_term env b))
+    | _, [] when c = build_coq_False () ->
+	False
+    | _, [] when c = build_coq_True () ->
+	True
+    | _, [a] when c = build_coq_not () ->
+	Not (tr_formula env a)
+    | _, [a;b] when c = build_coq_and () ->
+	And (tr_formula env a, tr_formula env b)
+    | _, [a;b] when c = build_coq_or () ->
+	Or (tr_formula env a, tr_formula env b)
+    | Prod (_, a, b), _ ->
+	if is_imp_term f then
+	  Imp (tr_formula env a, tr_formula env b)
+	else
+	  assert false (*TODO Forall *)
+    | _, [a] when c = build_coq_ex () ->
+	assert false (*TODO*) (*Exists (tr_formula env a)*)
     | _ ->
 	raise NotFO
 
@@ -73,18 +132,11 @@ let tr_goal gl =
   hyps, c
 
 
-(* Checks if a Coq formula is first-ordered *) 
-let rec is_FO c = match kind_of_term c with
-    Prod(n, t1, t2) -> assert false (*TODO*)
-  | Lambda(n, t, c) ->assert false (*TODO*)
-  | _ -> false
-
-(* Translates a first-order Coq formula into a specific first-order
- language formula *)
-(* let rec to_FO f = *)
-
 let rec isGoodType gl t = 
-(is_Prop t) || (is_Set t) || (is_Prop (pf_type_of gl (body_of_type t))) || (is_Set (pf_type_of gl (body_of_type t)))
+  (is_Prop t) || 
+  (is_Set t) || 
+  (is_Prop (pf_type_of gl (body_of_type t))) || 
+  (is_Set (pf_type_of gl (body_of_type t)))
 
 
 let rec allGoodTypeHyps gl hyps_types = match hyps_types with
@@ -103,18 +155,6 @@ let allGoodType gl =
   let hyps_types = pf_hyps_types gl in 
   allGoodTypeHyps gl hyps_types
 
-(*** UTILISER prterm
-let rec type_to_string t = match kind_of_term t with
-    Sort (Prop Null) -> "Prop "
-  | Sort (Prop Pos) -> "Set "
-  | Sort (Type _) -> "Type "
-  | Cast (c,_) -> type_to_string c
-  | _ -> "Other"
-
-let rec hyps_types_to_string = function
-    [] -> ""
-  | e::l -> (type_to_string e) ^ (hyps_types_to_string l)
-***)
 
 type prover = Simplify | CVCLite | Harvey
 
@@ -122,10 +162,6 @@ let call_prover prover q = match prover with
   | Simplify -> Dp_simplify.call q
   | CVCLite -> error "CVC Lite not yet interfaced"
   | Harvey -> error "haRVey not yet interfaced"
-
-let admit_as_an_axiom gl =
-  msgnl (str "Valid!");
-  Tacticals.tclIDTAC gl
   
 let dp prover gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
@@ -133,7 +169,7 @@ let dp prover gl =
   try 
     let q = tr_goal gl in
     begin match call_prover prover q with
-      | Valid -> admit_as_an_axiom gl
+      | Valid -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
       | DontKnow -> error "Don't know"
       | Timeout -> error "Timeout"