summaryrefslogtreecommitdiff
path: root/contrib/dp/dp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp/dp.ml')
-rw-r--r--contrib/dp/dp.ml316
1 files changed, 274 insertions, 42 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 131dd029..79ffaf3f 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -13,6 +13,8 @@
open Util
open Pp
+open Libobject
+open Summary
open Term
open Tacmach
open Tactics
@@ -25,12 +27,46 @@ open Coqlib
open Hipattern
open Libnames
open Declarations
+open Dp_why
let debug = ref false
+let set_debug b = debug := b
+let trace = ref false
+let set_trace b = trace := b
+let timeout = ref 10
+let set_timeout n = timeout := n
+
+let (dp_timeout_obj,_) =
+ declare_object
+ {(default_object "Dp_timeout") with
+ cache_function = (fun (_,x) -> set_timeout x);
+ load_function = (fun _ (_,x) -> set_timeout x);
+ export_function = (fun x -> Some x)}
+
+let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
+
+let (dp_debug_obj,_) =
+ declare_object
+ {(default_object "Dp_debug") with
+ cache_function = (fun (_,x) -> set_debug x);
+ load_function = (fun _ (_,x) -> set_debug x);
+ export_function = (fun x -> Some x)}
+
+let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
+
+let (dp_trace_obj,_) =
+ declare_object
+ {(default_object "Dp_trace") with
+ cache_function = (fun (_,x) -> set_trace x);
+ load_function = (fun _ (_,x) -> set_trace x);
+ export_function = (fun x -> Some x)}
+
+let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
let logic_dir = ["Coq";"Logic";"Decidable"]
let coq_modules =
init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+ @ [["Coq"; "ZArith"; "BinInt"]]
@ [["Coq"; "omega"; "OmegaLemmas"]]
let constant = gen_constant_in_modules "dp" coq_modules
@@ -52,6 +88,7 @@ let coq_Zneg = lazy (constant "Zneg")
let coq_xH = lazy (constant "xH")
let coq_xI = lazy (constant "xI")
let coq_xO = lazy (constant "xO")
+let coq_iff = lazy (constant "iff")
(* not Prop typed expressions *)
exception NotProp
@@ -104,7 +141,7 @@ let coq_rename_vars env vars =
type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
let decomp_type_quantifiers env t =
let rec loop vars t = match kind_of_term t with
- | Prod (n, a, t) when is_Set a ->
+ | Prod (n, a, t) when is_Set a || is_Type a ->
loop ((n,a) :: vars) t
| _ ->
let vars, env = coq_rename_vars env vars in
@@ -116,7 +153,7 @@ let decomp_type_quantifiers env t =
(* same thing with lambda binders (for axiomatize body) *)
let decomp_type_lambdas env t =
let rec loop vars t = match kind_of_term t with
- | Lambda (n, a, t) when is_Set a ->
+ | Lambda (n, a, t) when is_Set a || is_Type a ->
loop ((n,a) :: vars) t
| _ ->
let vars, env = coq_rename_vars env vars in
@@ -314,7 +351,7 @@ and make_term_abstraction tv env c =
*)
and tr_decl env id ty =
let tv, env, t = decomp_type_quantifiers env ty in
- if is_Set t then
+ if is_Set t || is_Type t then
DeclType (id, List.length tv)
else if is_Prop t then
DeclPred (id, List.length tv, [])
@@ -329,8 +366,8 @@ and tr_decl env id ty =
DeclPred(id, List.length tv, l)
else
let s = Typing.type_of env Evd.empty t in
- if is_Set s then
- DeclFun(id, List.length tv, l, tr_type tv env t)
+ if is_Set s || is_Type s then
+ DeclFun (id, List.length tv, l, tr_type tv env t)
else
raise NotFO
@@ -364,17 +401,18 @@ and axiomatize_body env r id d = match r with
begin match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
- let tv, env, b = decomp_type_lambdas env b in
let axioms =
(match d with
| DeclPred (id, _, []) ->
+ let tv, env, b = decomp_type_lambdas env b in
let value = tr_formula tv [] env b in
[id, Iff (Fatom (Pred (id, [])), value)]
| DeclFun (id, _, [], _) ->
+ let tv, env, b = decomp_type_lambdas env b in
let value = tr_term tv [] env b in
[id, Fatom (Eq (Fol.App (id, []), value))]
| DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
- Format.eprintf "axiomatize_body %S@." id;
+ (*Format.eprintf "axiomatize_body %S@." id;*)
let b = match kind_of_term b with
(* a single recursive function *)
| Fix (_, (_,_,[|b|])) ->
@@ -391,6 +429,7 @@ and axiomatize_body env r id d = match r with
| _ ->
b
in
+ let tv, env, b = decomp_type_lambdas env b in
let vars, t = decompose_lam b in
let n = List.length l in
let k = List.length vars in
@@ -401,21 +440,21 @@ and axiomatize_body env r id d = match r with
let vars = List.rev vars in
let bv = vars in
let vars = List.map (fun x -> string_of_id x) vars in
- let fol_var x =
- Fol.App (x, []) in
+ let fol_var x = Fol.App (x, []) in
let fol_vars = List.map fol_var vars in
let vars = List.combine vars l in
begin match d with
- | DeclFun _ ->
+ | DeclFun (_, _, _, ty) ->
begin match kind_of_term t with
| Case (ci, _, e, br) ->
equations_for_case env id vars tv bv ci e br
| _ ->
- let p =
- Fatom (Eq (App (id, fol_vars),
- tr_term tv bv env t))
+ let t = tr_term tv bv env t in
+ let ax =
+ add_proof (Fun_def (id, vars, ty, t))
in
- [id, foralls vars p]
+ let p = Fatom (Eq (App (id, fol_vars), t)) in
+ [ax, foralls vars p]
end
| DeclPred _ ->
let value = tr_formula tv bv env t in
@@ -436,7 +475,7 @@ and axiomatize_body env r id d = match r with
| IndRef i ->
iter_all_constructors i
(fun _ c ->
- let rc = reference_of_constr c in
+ let rc = global_of_constr c in
try
begin match tr_global env rc with
| DeclFun (_, _, [], _) -> ()
@@ -453,18 +492,20 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
iter_all_constructors ci.ci_ind
(fun j cj ->
try
- let cjr = reference_of_constr cj in
+ let cjr = global_of_constr cj in
begin match tr_global env cjr with
| DeclFun (idc, _, l, _) ->
let b = br.(j) in
let rec_vars, b = decompose_lam b in
let rec_vars, env = coq_rename_vars env rec_vars in
- let b = substl (List.map mkVar rec_vars) b in
+ let coq_rec_vars = List.map mkVar rec_vars in
+ let b = substl coq_rec_vars b in
let rec_vars = List.rev rec_vars in
+ let coq_rec_term = applist (cj, List.rev coq_rec_vars) in
+ let b = replace_vars [x, coq_rec_term] b in
let bv = bv @ rec_vars in
let rec_vars = List.map string_of_id rec_vars in
- let fol_var x =
- Fol.App (x, []) in
+ let fol_var x = Fol.App (x, []) in
let fol_rec_vars = List.map fol_var rec_vars in
let fol_rec_term = App (idc, fol_rec_vars) in
let rec_vars = List.combine rec_vars l in
@@ -558,7 +599,7 @@ and tr_formula tv bv env f =
Fatom (Pred (rename_global (VarRef id), []))
| _, [t;a;b] when c = build_coq_eq () ->
let ty = Typing.type_of env Evd.empty t in
- if is_Set ty then
+ if is_Set ty || is_Type ty then
let _ = tr_type tv env t in
Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
else
@@ -581,6 +622,8 @@ and tr_formula tv bv env f =
And (tr_formula tv bv env a, tr_formula tv bv env b)
| _, [a;b] when c = build_coq_or () ->
Or (tr_formula tv bv env a, tr_formula tv bv env b)
+ | _, [a;b] when c = Lazy.force coq_iff ->
+ Iff (tr_formula tv bv env a, tr_formula tv bv env b)
| Prod (n, a, b), _ ->
if is_imp_term f then
Imp (tr_formula tv bv env a, tr_formula tv bv env b)
@@ -632,55 +675,164 @@ let tr_goal gl =
hyps, c
-type prover = Simplify | CVCLite | Harvey | Zenon
+type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy
let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
let sprintf = Format.sprintf
+let file_contents f =
+ let buf = Buffer.create 1024 in
+ try
+ let c = open_in f in
+ begin try
+ while true do
+ let s = input_line c in Buffer.add_string buf s;
+ Buffer.add_char buf '\n'
+ done;
+ assert false
+ with End_of_file ->
+ close_in c;
+ Buffer.contents buf
+ end
+ with _ ->
+ sprintf "(cannot open %s)" f
+
+let timeout_sys_command cmd =
+ if !debug then Format.eprintf "command line: %s@." cmd;
+ let out = Filename.temp_file "out" "" in
+ let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+ let ret = Sys.command cmd in
+ if !debug then
+ Format.eprintf "Output file %s:@.%s@." out (file_contents out);
+ ret, out
+
+let timeout_or_failure c cmd out =
+ if c = 152 then
+ Timeout
+ else
+ Failure
+ (sprintf "command %s failed with output:\n%s " cmd (file_contents out))
+
+let prelude_files = ref ([] : string list)
+
+let set_prelude l = prelude_files := l
+
+let (dp_prelude_obj,_) =
+ declare_object
+ {(default_object "Dp_prelude") with
+ cache_function = (fun (_,x) -> set_prelude x);
+ load_function = (fun _ (_,x) -> set_prelude x);
+ export_function = (fun x -> Some x)}
+
+let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
+
+let why_files f = String.concat " " (!prelude_files @ [f])
+
let call_simplify fwhy =
- let cmd = sprintf "why --simplify %s" fwhy in
- if Sys.command cmd <> 0 then error ("Call to " ^ cmd ^ " failed");
+ let cmd =
+ sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy)
+ in
+ if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
let cmd =
- sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" fsx
+ sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+ !timeout fsx
in
let out = Sys.command cmd in
- let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in
+ let r =
+ if out = 0 then Valid None else if out = 1 then Invalid else Timeout
+ in
if not !debug then remove_files [fwhy; fsx];
r
+let call_ergo fwhy =
+ let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+ if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+ let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
+ let ftrace = Filename.temp_file "ergo_trace" "" in
+ let cmd =
+ if !trace then
+ sprintf "ergo -cctrace %s %s" ftrace fwhy
+ else
+ sprintf "ergo %s" fwhy
+ in
+ let ret,out = timeout_sys_command cmd in
+ let r =
+ if ret <> 0 then
+ timeout_or_failure ret cmd out
+ else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
+ Valid (if !trace then Some ftrace else None)
+ else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then
+ DontKnow
+ else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then
+ Invalid
+ else
+ Failure ("command failed: " ^ cmd)
+ in
+ if not !debug then remove_files [fwhy; out];
+ r
+
let call_zenon fwhy =
- let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in
+ let cmd =
+ sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
+ let out = Filename.temp_file "dp_out" "" in
let cmd =
- sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn
+ sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
+ in
+ let c = Sys.command cmd in
+ if not !debug then remove_files [fwhy; fznn];
+ if c = 137 then
+ Timeout
+ else begin
+ if c <> 0 then anomaly ("command failed: " ^ cmd);
+ if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then
+ error "Zenon failed";
+ let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in
+ if c = 0 then Valid (Some out) else Invalid
+ end
+
+let call_yices fwhy =
+ let cmd =
+ sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+ in
+ if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
+ let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
+ let cmd =
+ sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
+ !timeout fsmt
in
let out = Sys.command cmd in
let r =
- if out = 0 then Valid
- else if out = 1 then Invalid
- else if out = 137 then Timeout
- else anomaly ("malformed Zenon input file " ^ fznn)
+ if out = 0 then Valid None else if out = 1 then Invalid else Timeout
in
- if not !debug then remove_files [fwhy; fznn];
+ if not !debug then remove_files [fwhy; fsmt];
r
let call_cvcl fwhy =
- let cmd = sprintf "why --cvcl %s" fwhy in
+ let cmd =
+ sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
let cmd =
- sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" fcvc
+ sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
+ !timeout fcvc
in
let out = Sys.command cmd in
- let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in
+ let r =
+ if out = 0 then Valid None else if out = 1 then Invalid else Timeout
+ in
if not !debug then remove_files [fwhy; fcvc];
r
let call_harvey fwhy =
- let cmd = sprintf "why --harvey %s" fwhy in
+ let cmd =
+ sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+ in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in
@@ -688,7 +840,8 @@ let call_harvey fwhy =
let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
let outf = Filename.temp_file "rv" ".out" in
let out =
- Sys.command (sprintf "timeout 10 rv -e\"-T 2000\" %s > %s 2>&1" f outf)
+ Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
+ !timeout f outf)
in
let r =
if out <> 0 then
@@ -697,40 +850,69 @@ let call_harvey fwhy =
let cmd =
sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
in
- if Sys.command cmd = 0 then Valid else Invalid
+ if Sys.command cmd = 0 then Valid None else Invalid
in
if not !debug then remove_files [fwhy; frv; outf];
r
+let call_gwhy fwhy =
+ let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in
+ if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
+ NoAnswer
+
+let ergo_proof_from_file f gl =
+ let s =
+ let buf = Buffer.create 1024 in
+ let c = open_in f in
+ try
+ while true do Buffer.add_string buf (input_line c) done; assert false
+ with End_of_file ->
+ close_in c;
+ Buffer.contents buf
+ in
+ let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
+ let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
+ exact_check t gl
+
let call_prover prover q =
let fwhy = Filename.temp_file "coq_dp" ".why" in
Dp_why.output_file fwhy q;
- if !debug then ignore (Sys.command (sprintf "cat %s" fwhy));
match prover with
| Simplify -> call_simplify fwhy
+ | Ergo -> call_ergo fwhy
+ | Yices -> call_yices fwhy
| Zenon -> call_zenon fwhy
| CVCLite -> call_cvcl fwhy
| Harvey -> call_harvey fwhy
+ | Gwhy -> call_gwhy fwhy
let dp prover gl =
+ Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
try
let q = tr_goal gl in
begin match call_prover prover q with
- | Valid -> Tactics.admit_as_an_axiom gl
+ | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
+ | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
+ | Valid _ -> Tactics.admit_as_an_axiom gl
| Invalid -> error "Invalid"
| DontKnow -> error "Don't know"
| Timeout -> error "Timeout"
+ | Failure s -> error s
+ | NoAnswer -> Tacticals.tclIDTAC gl
end
with NotFO ->
error "Not a first order goal"
-
+
let simplify = tclTHEN intros (dp Simplify)
+let ergo = tclTHEN intros (dp Ergo)
+let yices = tclTHEN intros (dp Yices)
let cvc_lite = tclTHEN intros (dp CVCLite)
let harvey = dp Harvey
let zenon = tclTHEN intros (dp Zenon)
+let gwhy = tclTHEN intros (dp Gwhy)
let dp_hint l =
let env = Global.env () in
@@ -741,7 +923,8 @@ let dp_hint l =
if is_Prop s then
try
let id = rename_global r in
- let d = Axiom (id, tr_formula [] [] env ty) in
+ let tv, env, ty = decomp_type_quantifiers env ty in
+ let d = Axiom (id, tr_formula tv [] env ty) in
add_global r (Gfo d);
globals_stack := d :: !globals_stack
with NotFO ->
@@ -757,3 +940,52 @@ let dp_hint l =
end
in
List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
+
+let (dp_hint_obj,_) =
+ declare_object
+ {(default_object "Dp_hint") with
+ cache_function = (fun (_,l) -> dp_hint l);
+ load_function = (fun _ (_,l) -> dp_hint l);
+ export_function = (fun x -> Some x)}
+
+let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
+
+let dp_predefined qid s =
+ let r = Nametab.global qid in
+ let ty = Global.type_of_global r in
+ let env = Global.env () in
+ let id = rename_global r in
+ try
+ let d = match tr_decl env id ty with
+ | DeclType (_, n) -> DeclType (s, n)
+ | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
+ | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
+ | Axiom _ as d -> d
+ in
+ match d with
+ | Axiom _ -> msg_warning (str " ignored (axiom)")
+ | d -> add_global r (Gfo d)
+ with NotFO ->
+ msg_warning (str " ignored (not a first order declaration)")
+
+let (dp_predefined_obj,_) =
+ declare_object
+ {(default_object "Dp_predefined") with
+ cache_function = (fun (_,(id,s)) -> dp_predefined id s);
+ load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
+ export_function = (fun x -> Some x)}
+
+let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
+
+let _ = declare_summary "Dp options"
+ { freeze_function =
+ (fun () -> !debug, !trace, !timeout, !prelude_files);
+ unfreeze_function =
+ (fun (d,tr,tm,pr) ->
+ debug := d; trace := tr; timeout := tm; prelude_files := pr);
+ init_function =
+ (fun () ->
+ debug := false; trace := false; timeout := 10;
+ prelude_files := []);
+ survive_module = true;
+ survive_section = true }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:52:23 +0000