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

4 files changed, 89 insertions, 38 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"
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index da32e50662..40a5230894 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -2,3 +2,4 @@
 open Proof_type
 
 val simplify : tactic
+
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index de5d898793..35370c6fdc 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -14,8 +14,14 @@ let rec print_term fmt = function
       fprintf fmt "%s" id
   | Cst n -> 
       fprintf fmt "%d" n
-  | Plus _ | Moins _ | Div _ | Mult _ ->
-      assert false (*TODO*) (* (+ a b) *)
+  | Plus (a, b) ->
+      fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b
+  | Moins (a, b) ->
+      fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b
+  | Mult (a, b) ->
+      fprintf fmt "@[(*@ %a@ %a)@]" (**) print_term a print_term b
+  | Div (a, b) ->
+      fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
   | App (id, []) ->
       fprintf fmt "%s" id 
   | App (id, tl) ->
@@ -38,11 +44,15 @@ let rec print_predicate fmt p =
   | Fatom (Eq (a, b)) ->
       fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b
   | Fatom (Le (a, b)) ->
-      fprintf fmt "@[(<= %a %a)@]" print_term a print_term b
+      fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b
+  | Fatom (Lt (a, b))->
+      fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b
+  | Fatom (Ge (a, b)) ->
+      fprintf fmt "@[(>= %a@ %a)@]" print_term a print_term b
+  | Fatom (Gt (a, b)) ->
+      fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
   | Fatom (Pred (id, tl)) -> 
       fprintf fmt "@[(EQ (%s@ %a) |@@true|)@]" id print_terms tl
-  | Fatom _ ->
-      assert false (*TODO*)
   | Imp (a, b) ->
       fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b
   | And (a, b) ->
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 607b4d9cc0..6a984dda30 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -16,3 +16,7 @@ TACTIC EXTEND Simplify
   [ "simplify" ] -> [ simplify ]
 END
 
+(* should be part of basic tactics syntax *)
+TACTIC EXTEND admit
+  [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
+END