diff options
Diffstat (limited to 'contrib/dp/dp.ml')
-rw-r--r-- | contrib/dp/dp.ml | 316 |
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 } |