appel de Simplify depuis Coq

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

7 files changed, 283 insertions, 45 deletions

diff --git a/.depend b/.depend
index 2a65cd66c8..433e0d1793 100644
--- a/.depend
+++ b/.depend
@@ -393,6 +393,7 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \
 contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 contrib/correctness/pwp.cmi: kernel/term.cmi 
 contrib/dp/dp.cmi: proofs/proof_type.cmi 
+contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi 
 contrib/extraction/common.cmi: kernel/names.cmi contrib/extraction/mlutil.cmi \
     contrib/extraction/miniml.cmi 
 contrib/extraction/extract_env.cmi: kernel/names.cmi library/libnames.cmi 
@@ -2639,10 +2640,14 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \
     library/nametab.cmx kernel/names.cmx library/libnames.cmx \
     tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \
     contrib/correctness/pwp.cmi 
-contrib/dp/dp.cmo: lib/util.cmi kernel/term.cmi proofs/tacmach.cmi lib/pp.cmi \
-    contrib/dp/fol.cmi contrib/dp/dp.cmi 
-contrib/dp/dp.cmx: lib/util.cmx kernel/term.cmx proofs/tacmach.cmx lib/pp.cmx \
-    contrib/dp/fol.cmi contrib/dp/dp.cmi 
+contrib/dp/dp.cmo: lib/util.cmi kernel/term.cmi tactics/tacticals.cmi \
+    proofs/tacmach.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
+    contrib/dp/fol.cmi interp/coqlib.cmi contrib/dp/dp.cmi 
+contrib/dp/dp.cmx: lib/util.cmx kernel/term.cmx tactics/tacticals.cmx \
+    proofs/tacmach.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
+    contrib/dp/fol.cmi interp/coqlib.cmx contrib/dp/dp.cmi 
+contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
+contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi 
 contrib/dp/g_dp.cmo: lib/util.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
     proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
     lib/options.cmi parsing/egrammar.cmi contrib/dp/dp.cmi \
diff --git a/Makefile b/Makefile
index 0cb6223e3e..3ed55298ec 100644
--- a/Makefile
+++ b/Makefile
@@ -246,7 +246,7 @@ RINGCMO=\
   contrib/ring/ring.cmo contrib/ring/g_ring.cmo 
 
 DPCMO=\
-  contrib/dp/dp.cmo contrib/dp/g_dp.cmo
+  contrib/dp/dp_simplify.cmo contrib/dp/dp.cmo contrib/dp/g_dp.cmo
 
 FIELDCMO=\
   contrib/field/field.cmo 
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 529a105097..417d74b6df 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -1,18 +1,147 @@
+(* Author : Nicolas Ayache and Jean-Christophe Filliatre *)
+(* Goal : Tactics to call decision procedures *)
+
 
 open Util
 open Pp
 open Term
 open Tacmach
 open Fol
+open Names
+open Nameops
+open Coqlib
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+  init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+    @ [["Coq"; "omega"; "OmegaLemmas"]]
+
+let constant = gen_constant_in_modules "Omega" coq_modules
+
+let coq_Z = lazy (constant "Z")
+
+(* not Prop typed expressions *)
+exception NotProp
+
+(* not first-order expressions *)
+exception NotFO
+
+(* assumption: t:Set *)
+let tr_type env t =
+  if t = Lazy.force coq_Z then Base "INT"
+  else raise NotFO
+
+(* assumption: t:T:Set *)
+let tr_term env t =
+  match kind_of_term t with
+    | Var id -> Tvar (string_of_id id)
+    | _ -> raise NotFO
+
+(* assumption: f is of type Prop *)
+let tr_formula env f =
+  let c, args = decompose_app f in
+  match kind_of_term c, args with
+    | _, [t;a;b] when c = build_coq_eq () -> 
+	(* TODO: verifier type t *)
+	Fatom (Eq (tr_term env a, tr_term env b))
+    | _ ->
+	raise NotFO
+
+
+let tr_goal gl =
+  let tr_one_hyp (id, ty) =
+    let id = string_of_id id in
+    if is_Prop ty then
+      DeclProp id
+    else if is_Set ty then
+      DeclType id
+    else 
+      let s = pf_type_of gl ty in
+      if is_Prop s then
+	Assert (id, tr_formula (pf_env gl) ty)
+      else if is_Set s then
+	DeclVar (id, tr_type (pf_env gl) ty)
+      else
+	raise NotFO
+  in
+  let c = tr_formula (pf_env gl) (pf_concl gl) in
+  let hyps =
+    List.fold_left 
+      (fun acc h -> try tr_one_hyp h :: acc with NotFO -> acc)
+      [] (pf_hyps_types gl)
+  in
+  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)))
+
+
+let rec allGoodTypeHyps gl hyps_types = match hyps_types with
+  | [] -> 
+      Tacticals.tclIDTAC gl
+  | (id, t)::l' -> 
+      if not (isGoodType gl t) then 
+	errorlabstrm "allGoodTypeHyps"
+	  (pr_id id ++ str " must be Prop, Set or " ++ pr_id id ++ 
+	   str "'s type must be Prop or Set");
+      allGoodTypeHyps gl l'
+
+let allGoodType gl =
+  let concl_type = pf_type_of gl (pf_concl gl) in
+  if not (is_Prop concl_type) then error "Goal is not a Prop";
+  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
 
+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 = pf_concl gl in
-  if not (is_Prop (pf_type_of gl concl)) then error "not a proposition";
-  error "not yet implemented"
+  let concl_type = pf_type_of gl (pf_concl gl) in
+  if not (is_Prop concl_type) then error "Goal is not a Prop";
+  try 
+    let q = tr_goal gl in
+    begin match call_prover prover q with
+      | Valid -> admit_as_an_axiom gl
+      | Invalid -> error "Invalid"
+      | DontKnow -> error "Don't know"
+      | Timeout -> error "Timeout"
+    end
+  with NotFO ->
+    error "Not a first order goal"
+  
 
 let simplify = dp Simplify
 let cvc_lite = dp CVCLite
 let harvey = dp Harvey
-
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
new file mode 100644
index 0000000000..de5d898793
--- /dev/null
+++ b/contrib/dp/dp_simplify.ml
@@ -0,0 +1,91 @@
+
+open Format
+open Fol
+
+let rec print_list sep print fmt = function
+  | [] -> ()
+  | [x] -> print fmt x
+  | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
+
+let space fmt () = fprintf fmt "@ "
+
+let rec print_term fmt = function
+  | Tvar id -> 
+      fprintf fmt "%s" id
+  | Cst n -> 
+      fprintf fmt "%d" n
+  | Plus _ | Moins _ | Div _ | Mult _ ->
+      assert false (*TODO*) (* (+ a b) *)
+  | App (id, []) ->
+      fprintf fmt "%s" id 
+  | App (id, tl) ->
+      fprintf fmt "@[(%s@ %a)@]" id print_terms tl
+  | Db _ ->
+      assert false (*TODO*)
+
+and print_terms fmt tl = 
+  print_list space print_term fmt tl
+
+let rec print_predicate fmt p = 
+  let pp = print_predicate in 
+  match p with
+  | True ->
+      fprintf fmt "TRUE"
+  | False ->
+      fprintf fmt "FALSE"
+  | Fvar id -> 
+      fprintf fmt "%s" id
+  | 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
+  | 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) ->
+      fprintf fmt "@[(AND@ %a@ %a)@]" pp a pp b
+  | Or (a, b) ->
+      fprintf fmt "@[(OR@ %a@ %a)@]" pp a pp b
+  | Not a ->
+      fprintf fmt "@[(NOT@ %a)@]" pp a
+(*
+  | Forall (_,id,n,_,p) -> 
+      let id' = next_away id (predicate_vars p) in
+      let p' = subst_in_predicate (subst_onev n id') p in
+      fprintf fmt "@[(FORALL (%a)@ %a)@]" Ident.print id' pp p'
+  | Exists (id,n,t,p) -> 
+      let id' = next_away id (predicate_vars p) in
+      let p' = subst_in_predicate (subst_onev n id') p in
+      fprintf fmt "@[(EXISTS (%a)@ %a)@]" Ident.print id' pp p'
+*)
+  | Exists _|Forall _ ->
+      assert false (*TODO*)
+
+let print_query fmt (decls,concl) =
+  let print_decl = function
+    | DeclVar _ | DeclProp _ | DeclType _ -> 
+	()
+    | Assert (id, f)  -> 
+	fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
+  in
+  List.iter print_decl decls;
+  print_predicate fmt concl
+
+let call q = 
+  let f = Filename.temp_file "coq_dp" ".sx" in
+  let c = open_out f in
+  let fmt = formatter_of_out_channel c in
+  fprintf fmt "@[%a@]@." print_query q;
+  close_out c;
+  let cmd = 
+    sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" f
+  in
+  prerr_endline cmd; flush stderr;
+  let out = Sys.command cmd in
+  if out = 0 then Valid else if out = 1 then Invalid else Timeout
+  (* TODO: effacer le fichier f et le fichier out *)
+
+
diff --git a/contrib/dp/dp_simplify.mli b/contrib/dp/dp_simplify.mli
new file mode 100644
index 0000000000..03b6d3475e
--- /dev/null
+++ b/contrib/dp/dp_simplify.mli
@@ -0,0 +1,4 @@
+
+open Fol
+
+val call : query -> prover_answer
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index e42d1f2245..5299f8ad77 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -1,37 +1,48 @@
 
-type typ =   Base of string
-	   | Arrow of typ * typ
-	   | Tuple of typ list
-
-type term =   Cst of int
-	    | Db of int
-            | Tvar of string
-            | Plus of term * term
-	    | Moins of term * term
-	    | Mult of term * term
-	    | Div of term * term
-	    | App of string * (term list)
-and
-     atom =   Eq of term * term
-	    | Le of term * term
-	    | Lt of term * term
-	    | Ge of term * term
-	    | Gt of term * term
-            | Pred of string * (term list)
-and
-     form =   Fatom of atom
-            | Fvar of string
-	    | Imp of form * form
-	    | And of form * form
-	    | Or of form * form
-	    | Not of form
-	    | Forall of form
-	    | Exists of form
-
-type decl =
-  | Assert of form
-(*  | ...*)
-
-type query = decl list * form
+type typ =  
+  | Base of string
+  | Arrow of typ * typ
+  | Tuple of typ list
 
+type term =   
+  | Cst of int
+  | Db of int
+  | Tvar of string
+  | Plus of term * term
+  | Moins of term * term
+  | Mult of term * term
+  | Div of term * term
+  | App of string * (term list)
 
+and atom =   
+  | Eq of term * term
+  | Le of term * term
+  | Lt of term * term
+  | Ge of term * term
+  | Gt of term * term
+  | Pred of string * (term list)
+
+and form = 
+  | Fatom of atom
+  | Fvar of string
+  | Imp of form * form
+  | And of form * form
+  | Or of form * form
+  | Not of form
+  | Forall of form
+  | Exists of form
+  | True
+  | False
+
+type hyp =
+  | Assert of string * form
+  | DeclVar of string * typ
+  | DeclProp of string
+  | DeclType of string
+
+type query = hyp list * form
+
+
+(* prover result *)
+
+type prover_answer = Valid | Invalid | DontKnow | Timeout
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index d34361ac43..04d4566cb6 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -37,8 +37,6 @@ open Proof_trees
    intersection of the free-rels of the term and the current stack be
    contained in the arguments of the application *)
 
-val is_imp_term : constr -> bool
-
 (*s I implemented the following functions which test whether a term [t]
    is an inductive but non-recursive type, a general conjuction, a
    general disjunction, or a type with no constructors.