diff options
author | 2006-03-27 14:38:28 +0000 | |
---|---|---|
committer | 2006-03-27 14:38:28 +0000 | |
commit | ba7d0994f166b7e5a2545af294e01e899b6e20d9 (patch) | |
tree | 96a09e9225939cc84ac8452b2466aba79beaf044 | |
parent | 7fc1c21b734a459ee9fef1f945a1a9c420aaa00c (diff) |
appel Zenon sans prelude
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/dp/dp.ml | 15 | ||||
-rw-r--r-- | contrib/dp/dp_why.ml | 2 | ||||
-rw-r--r-- | contrib/dp/fol.mli | 1 |
3 files changed, 9 insertions, 9 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 9a0ad2bb6..af684e6e9 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -26,7 +26,7 @@ open Hipattern open Libnames open Declarations -let debug = ref true +let debug = ref false let logic_dir = ["Coq";"Logic";"Decidable"] let coq_modules = @@ -369,8 +369,7 @@ and axiomatize_body env r id d = match r with (match d with | DeclPred (id, _, []) -> let value = tr_formula tv [] env b in - [id, And (Imp (Fatom (Pred (id, [])), value), - Imp (value, Fatom (Pred (id, []))))] + [id, Iff (Fatom (Pred (id, [])), value)] | DeclFun (id, _, [], _) -> let value = tr_term tv [] env b in [id, Fatom (Eq (Fol.App (id, []), value))] @@ -420,10 +419,7 @@ and axiomatize_body env r id d = match r with end | DeclPred _ -> let value = tr_formula tv bv env t in - let p = - And (Imp (Fatom (Pred (id, fol_vars)), value), - Imp (value, Fatom (Pred (id, fol_vars)))) - in + let p = Iff (Fatom (Pred (id, fol_vars)), value) in [id, foralls vars p] | _ -> assert false @@ -655,8 +651,9 @@ let call_simplify fwhy = r let call_zenon fwhy = - if Sys.command (sprintf "why --zenon %s" fwhy) <> 0 then - anomaly ("call to why --zenon " ^ fwhy ^ " failed; please report"); + let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in + if Sys.command cmd <> 0 then + anomaly ("call to " ^ cmd ^ " failed; please report"); let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in let cmd = sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml index 662a5a8be..e1ddb039b 100644 --- a/contrib/dp/dp_why.ml +++ b/contrib/dp/dp_why.ml @@ -77,6 +77,8 @@ let rec print_predicate fmt p = fprintf fmt "@[%a(%a)@]" ident id print_terms tl | Imp (a, b) -> fprintf fmt "@[(%a ->@ %a)@]" pp a pp b + | Iff (a, b) -> + fprintf fmt "@[(%a <->@ %a)@]" pp a pp b | And (a, b) -> fprintf fmt "@[(%a and@ %a)@]" pp a pp b | Or (a, b) -> diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli index 5dd46b0d1..a85469cc6 100644 --- a/contrib/dp/fol.mli +++ b/contrib/dp/fol.mli @@ -24,6 +24,7 @@ and atom = and form = | Fatom of atom | Imp of form * form + | Iff of form * form | And of form * form | Or of form * form | Not of form |