appel de Simplify depuis Coq

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

4 files changed, 273 insertions, 38 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 529a10509..417d74b6d 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 000000000..de5d89879
--- /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 000000000..03b6d3475
--- /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 e42d1f224..5299f8ad7 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