diff --git a/src/ecCoq.ml b/src/ecCoq.ml new file mode 100644 index 0000000000..aba1822da2 --- /dev/null +++ b/src/ecCoq.ml @@ -0,0 +1,244 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcLocation +open EcFol +open EcEnv +open EcProvers + +(* -------------------------------------------------------------------- *) +module WCall_provers = Why3.Call_provers +module WConf = Why3.Whyconf +module WDriver = Why3.Driver +module WEnv = Why3.Env +module WTask = Why3.Task + +(* -------------------------------------------------------------------- *) +type coqenv = { + config : WConf.config; + main : WConf.main; + driver : WDriver.driver; + cnfprv : WConf.config_prover; + prover : WConf.prover; +} + +(* -------------------------------------------------------------------- *) +let call_prover_task ~(coqenv : coqenv) (call : WCall_provers.prover_call) = + EcUtils.try_finally + (fun () -> + match (Why3.Call_provers.wait_on_call call).pr_answer with + | Valid -> Some `Valid + | Invalid -> Some `Invalid + | _ -> None) + (fun () -> + WCall_provers.interrupt_call ~config:coqenv.main call) + +(* -------------------------------------------------------------------- *) +let run_batch ~(script : string) ~(coqenv : coqenv) (task : WTask.task) = + let config = Why3.Whyconf.get_main coqenv.config in + let config_mem = Why3.Whyconf.memlimit config in + let config_time = Why3.Whyconf.timelimit config in + let limit = + Why3.Call_provers.{ + limit_time = config_time; + limit_steps = 0; + limit_mem = config_mem; + } + in + let command = + Why3.Whyconf.get_complete_command + coqenv.cnfprv ~with_steps:false in + let call = + Why3.Driver.prove_task_prepared + ~old:script ~inplace:true + ~command ~limit ~config coqenv.driver task + in call_prover_task ~coqenv call + +(* -------------------------------------------------------------------- *) +let editor_command ~(coqenv : coqenv) : string = + try + let editors = Why3.Whyconf.get_editors coqenv.config in + let editors = + Why3.Whyconf.Meditor.filter + (fun _ a -> a.Why3.Whyconf.editor_name = "Emacs/ProofGeneral/Coq") + editors + in + let _, ed = Why3.Whyconf.Meditor.max_binding editors in + String.concat " " (ed.editor_command :: ed.editor_options) + + with Not_found -> + Why3.Whyconf.(default_editor (get_main coqenv.config)) + +(* -------------------------------------------------------------------- *) +let script_file ~(name : string located) ~(ext : string) = + let { pl_loc = loc; pl_desc = name; } = name in + let file = loc.loc_fname in + let path = Filename.dirname file in + let path = + if Filename.is_relative path then + Filename.concat (Sys.getcwd ()) path + else path in + let path = Filename.concat path ".interactive" in + let name = + if String.is_empty name then + let name = Filename.basename file in + let name = Filename.remove_extension name in + let l, r = loc.loc_start in + Format.sprintf "%s-%d-%d" name l r + else name + in + Format.sprintf "%s/%s%s" path name ext + +(* -------------------------------------------------------------------- *) +let update_script + ~(script : string) + ~(coqenv : coqenv) + (task : WTask.task) += + let backup = Format.sprintf "%s~" script in + Sys.rename script backup; + + let old = open_in backup in + EcUtils.try_finally + (fun () -> + IO.pp_to_file ~filename:script + (fun fmt -> ignore @@ + Why3.Driver.print_task_prepared ~old coqenv.driver fmt task)) + (fun () -> close_in old) + +(* -------------------------------------------------------------------- *) +let editor + ~(script : string) + ~(merge : bool) + ~(coqenv : coqenv) + (task : WTask.task) += + if merge then update_script ~script ~coqenv task; + let command = editor_command ~coqenv in + let config = WConf.get_main coqenv.config in + let call = WCall_provers.call_editor ~command ~config script in + ignore @@ call_prover_task ~coqenv call + +(* -------------------------------------------------------------------- *) +let prepare + ~(name : string located) + ~(coqenv : coqenv) + (task : WTask.task) += + let ext = Why3.Driver.file_of_task coqenv.driver "S" "T" task in + let ext = Filename.extension ext in + let script = script_file ~name ~ext in + + if Sys.file_exists script then + (script, true) + else begin + EcUtils.makedirs (Filename.dirname script); + EcUtils.IO.pp_to_file ~filename:script + (fun fmt -> ignore @@ + Why3.Driver.print_task_prepared coqenv.driver fmt task); + (script, false) + end + +(* -------------------------------------------------------------------- *) +let interactive + ~(name : string located) + ~(coqmode : coq_mode) + ~(coqenv : coqenv) + (task : WTask.task) += + let script, merge = prepare ~name ~coqenv task in + + if merge then + update_script ~script ~coqenv task; + + match coqmode with + | Check -> + run_batch ~script ~coqenv task + + | Edit -> + editor ~script ~merge ~coqenv task; + run_batch ~script ~coqenv task + + | Fix -> begin + match run_batch ~script ~coqenv task with + | Some `Valid as answer -> + answer + | _ -> + editor ~script ~merge ~coqenv task; + run_batch ~script ~coqenv task + end + +(* -------------------------------------------------------------------- *) +let is_trivial (t : Why3.Task.task) = + let goal = Why3.Task.task_goal_fmla t in + Why3.Term.t_equal goal Why3.Term.t_true + +(* -------------------------------------------------------------------- *) +let build_proof_task + ~(notify : notify option) + ~(name : string located) + ~(coqmode : coq_mode) + ~(config : WConf.config) + ~(env : WEnv.env) + (task : WTask.task) += + let exception CoqNotFound in + + try + let coqenv = + let (prover, cnfprv) = + let fp = Why3.Whyconf.parse_filter_prover "Coq" in + let provers = Why3.Whyconf.filter_provers config fp in + begin + match Why3.Whyconf.Mprover.is_empty provers with + | false -> Why3.Whyconf.Mprover.max_binding provers + | true -> raise CoqNotFound + end + in + let main = Why3.Whyconf.get_main config in + let driver = + Why3.Driver.load_driver_for_prover + main env cnfprv + in { config; main; driver; cnfprv; prover; } in + + let task = Why3.Driver.prepare_task coqenv.driver task in + + if is_trivial task then + Some `Valid + else + interactive ~name ~coqmode ~coqenv task + + with + | CoqNotFound -> + notify |> oiter (fun notify -> notify `Critical (lazy ( + Format.asprintf "Prover Coq not installed or not configured" + ))); + None + + | exn -> + notify |> oiter (fun notify -> notify `Critical (lazy ( + Format.asprintf "[Why3 Error] %a" Why3.Exn_printer.exn_printer exn + ))); + None + +(* -------------------------------------------------------------------- *) +let check + ~(loc : EcLocation.t) + ~(name : string) + ?(notify : notify option) + (pi : prover_infos) + ?(coqmode : coq_mode = Edit) + (hyps : LDecl.hyps) + (concl : form) += + EcProvers.maybe_start_why3_server pi; + + let config = EcProvers.get_w3_conf () in + let env = EcProvers.get_w3_env () in + let ec_env, hyps, tenv, decl = EcSmt.init hyps concl in + + let execute_task toadd = + let task = EcSmt.make_task tenv toadd decl in + let result = + build_proof_task ~notify ~name:(mk_loc loc name) ~coqmode ~config ~env task in + Option.map (fun r -> r = `Valid) result + in EcSmt.select ec_env pi hyps concl execute_task diff --git a/src/ecCoq.mli b/src/ecCoq.mli new file mode 100644 index 0000000000..51f6d9b8cc --- /dev/null +++ b/src/ecCoq.mli @@ -0,0 +1,15 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcEnv +open EcProvers + +(* -------------------------------------------------------------------- *) +val check : + loc:EcLocation.t + -> name:string + -> ?notify:notify + -> prover_infos + -> ?coqmode:coq_mode + -> LDecl.hyps + -> form + -> bool diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 6c043bc662..6bdc7e61fc 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -147,6 +147,21 @@ let process_smt ?loc (ttenv : ttenv) pi (tc : tcenv1) = | `Report -> t_seq (t_simplify ~delta:`No) (t_smt ~mode:(`Report loc) pi) tc +(* -------------------------------------------------------------------- *) + +let process_coq ~loc ~name (ttenv : ttenv) coqmode pi (tc : tcenv1) = + let pi = ttenv.tt_provers pi in + + match ttenv.tt_smtmode with + | `Admit -> + t_admit tc + + | (`Sloppy | `Strict) as mode -> + t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode coqmode pi) tc + + | `Report -> + t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode:(`Report (Some loc)) coqmode pi) tc + (* -------------------------------------------------------------------- *) let process_clear symbols tc = let hyps = FApi.tc1_hyps tc in diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 7bff4960e2..f2f99f75d1 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -73,6 +73,7 @@ val process_generalize : ?doeq:bool -> genpattern list -> backward val process_move : ?doeq:bool -> ppterm list -> prevert -> backward val process_clear : psymbol list -> backward val process_smt : ?loc:EcLocation.t -> ttenv -> pprover_infos -> backward +val process_coq : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward val process_apply : implicits:bool -> apply_t * prevert option -> backward val process_delta : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward val process_rewrite : ttenv -> ?target:psymbol -> rwarg list -> backward diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 96ef38eef7..d28afe1b63 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -154,6 +154,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Pwlog (ids, b, f) -> process_wlog ~suff:b ids f | Pgenhave gh -> process_genhave ttenv gh | Prwnormal _ -> assert false + | Pcoq (m, n, pi) -> process_coq ~loc:(loc t) ~name:n.pl_desc ttenv m pi in tx tc diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 8722955356..c1225b0720 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -106,6 +106,7 @@ "trivial" , TRIVIAL ; (* KW: tactic *) "auto" , AUTO ; (* KW: tactic *) + (* Other tactics *) "idtac" , IDTAC ; (* KW: tactic *) "move" , MOVE ; (* KW: tactic *) @@ -119,6 +120,10 @@ "exact" , EXACT ; (* KW: bytac *) "assumption" , ASSUMPTION ; (* KW: bytac *) "smt" , SMT ; (* KW: bytac *) + "coq" , COQ ; (* KW: bytac *) + "check" , CHECK ; (* KW: bytac *) + "edit" , EDIT ; (* KW: bytac *) + "fix" , FIX ; (* KW: bytac *) "by" , BY ; (* KW: bytac *) "reflexivity" , REFLEX ; (* KW: bytac *) "done" , DONE ; (* KW: bytac *) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index a0ffba33d2..33615bda58 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2435,6 +2435,35 @@ let t_smt ~(mode:smtmode) pi tc = then FApi.xmutate1 tc `Smt [] else error () +(* -------------------------------------------------------------------- *) +let t_coq + ~(loc : EcLocation.t) + ~(name : string) + ~(mode : smtmode) + (coqmode : EcProvers.coq_mode option) + (pi : EcProvers.prover_infos) + (tc : tcenv1) += + let error () = + match mode with + | `Sloppy -> + tc_error !!tc ~catchable:true "cannot prove goal" + | `Strict -> + tc_error !!tc ~catchable:false "cannot prove goal (strict)" + | `Report loc -> + EcEnv.notify (FApi.tc1_env tc) `Critical + "%s: Coq call failed" + (loc |> omap EcLocation.tostring |> odfl "unknown"); + t_admit tc + in + + let env, hyps, concl = FApi.tc1_eflat tc in + let notify = (fun lvl (lazy s) -> EcEnv.notify env lvl "%s" s) in + + if EcCoq.check ~loc ~name ~notify ?coqmode pi hyps concl + then FApi.xmutate1 tc `Smt [] + else error () + (* -------------------------------------------------------------------- *) let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(depth = 1) (tc : tcenv1) = let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 2b92eeef89..fb6fd7ee61 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -321,6 +321,14 @@ type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option] val t_smt: mode:smtmode -> prover_infos -> FApi.backward +val t_coq: + loc:EcLocation.t + -> name:string + -> mode:smtmode + -> coq_mode option + -> prover_infos + -> FApi.backward + (* -------------------------------------------------------------------- *) val t_solve : ?canfail:bool diff --git a/src/ecParser.mly b/src/ecParser.mly index 809b80f99f..d69ed3d780 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -304,7 +304,7 @@ let pr = match k with | `Only -> - ok_use_only r p; { r with pp_use_only = p :: r.pp_use_only } + ok_use_only r p; { r with pp_use_only = p :: r.pp_use_only } | `Include -> { r with pp_add_rm = (`Include, p) :: r.pp_add_rm } | `Exclude -> { r with pp_add_rm = (`Exclude, p) :: r.pp_add_rm } @@ -415,6 +415,10 @@ %token CONGR %token CONSEQ %token CONST +%token COQ +%token CHECK +%token EDIT +%token FIX %token DEBUG %token DECLARE %token DELTA @@ -666,6 +670,9 @@ _lident: | ECALL { "ecall" } | FROM { "from" } | EXIT { "exit" } +| CHECK { "check" } +| EDIT { "edit" } +| FIX { "fix" } | x=RING { match x with `Eq -> "ringeq" | `Raw -> "ring" } | x=FIELD { match x with `Eq -> "fieldeq" | `Raw -> "field" } @@ -2759,6 +2766,9 @@ logtactic: | SMT pi=smt_info { Psmt pi } +| COQ mode=coq_info name=loc(STRING) LPAREN dbmap=dbmap1* RPAREN + { Pcoq (mode, name, SMT.mk_smt_option [`WANTEDLEMMAS dbmap])} + | SMT LPAREN dbmap=dbmap1* RPAREN { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) } @@ -3717,6 +3727,12 @@ print: | REWRITE qs=qident { Pr_db (`Rewrite qs) } | SOLVE qs=ident { Pr_db (`Solve qs) } +coq_info: +| { None } +| CHECK { Some EcProvers.Check } +| EDIT { Some EcProvers.Edit } +| FIX { Some EcProvers.Fix } + smt_info: | li=smt_info1* { SMT.mk_smt_option li} diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index aa1e868a5c..d4ed0cbe5e 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -962,6 +962,7 @@ type logtactic = | Pmemory of psymbol | Pgenhave of pgenhave | Pwlog of (psymbol list * bool * pformula) + | Pcoq of (EcProvers.coq_mode option * psymbol * pprover_infos) (* -------------------------------------------------------------------- *) and ptactic_core_r = diff --git a/src/ecProvers.ml b/src/ecProvers.ml index cfa6999436..ac0955b142 100644 --- a/src/ecProvers.ml +++ b/src/ecProvers.ml @@ -306,6 +306,11 @@ let is_prover_known name = try ignore (get_prover name); true with UnknownProver _ -> false (* -------------------------------------------------------------------- *) + +let get_w3_main = Config.main +let get_w3_conf = Config.config +let get_w3_env = Config.w3_env + let get_w3_th dirname name = Env.read_theory (Config.w3_env ()) dirname name @@ -380,6 +385,12 @@ module Hints = struct | Some `Exclude -> false end +(* -------------------------------------------------------------------- *) +type coq_mode = + | Check (* Check scripts *) + | Edit (* Edit then check scripts *) + | Fix (* Try to check script, then edit script on non-success *) + (* -------------------------------------------------------------------- *) type prover_infos = { pr_maxprocs : int; diff --git a/src/ecProvers.mli b/src/ecProvers.mli index da21354e6b..41481c73ce 100644 --- a/src/ecProvers.mli +++ b/src/ecProvers.mli @@ -22,6 +22,12 @@ module Version : sig val to_string : version -> string end +(* -------------------------------------------------------------------- *) +type coq_mode = + | Check (* Check scripts *) + | Edit (* Edit then check scripts *) + | Fix (* Try to check script, then edit script on non-success *) + (* -------------------------------------------------------------------- *) type prover_eviction = [ | `Inconsistent @@ -76,5 +82,11 @@ val initialize : (* -------------------------------------------------------------------- *) type notify = EcGState.loglevel -> string Lazy.t -> unit +val maybe_start_why3_server : prover_infos -> unit + val execute_task : ?notify:notify -> prover_infos -> Why3.Task.task -> bool option val get_w3_th : string list -> string -> Why3.Theory.theory + +val get_w3_main : unit -> Why3.Whyconf.main +val get_w3_env : unit -> Why3.Env.env +val get_w3_conf : unit -> Why3.Whyconf.config diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 9bbd63a138..6d81016c62 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -1613,18 +1613,7 @@ let dump_why3 (env : EcEnv.env) (filename : string) = List.iter (trans_axiom tenv) (EcEnv.Ax.all env); dump_tasks tenv.te_task filename -(* -------------------------------------------------------------------- *) -let cnt = Counter.create () - -let check ?notify (pi : P.prover_infos) (hyps : LDecl.hyps) (concl : form) = - let out_task filename task = - let stream = open_out filename in - EcUtils.try_finally - (fun () -> Format.fprintf - (Format.formatter_of_out_channel stream) - "%a@." Why3.Pretty.print_task task) - (fun () -> close_out stream) in - +let init hyps concl = let env = LDecl.toenv hyps in let hyps = LDecl.tohyps hyps in let task = create_global_task () in @@ -1635,39 +1624,11 @@ let check ?notify (pi : P.prover_infos) (hyps : LDecl.hyps) (concl : form) = let wterm = Cast.force_prop (trans_form (tenv, lenv) concl) in let pr = WDecl.create_prsymbol (WIdent.id_fresh "goal") in let decl = WDecl.create_prop_decl WDecl.Pgoal pr wterm in + env,hyps,tenv,decl - let execute_task toadd = - if pi.P.pr_selected then begin - let buffer = Buffer.create 0 in - let fmt = Format.formatter_of_buffer buffer in - let ppe = EcPrinting.PPEnv.ofenv env in - let l = List.map fst toadd in - let pp fmt = EcPrinting.pp_list "@ " (EcPrinting.pp_axname ppe) fmt in - Format.fprintf fmt "selected lemmas: @[%a@]@." pp l; - notify |> oiter (fun notify -> notify `Warning - (lazy (Buffer.contents buffer))) - end; - - List.iter (trans_axiom tenv) toadd; - let task = WTask.add_decl tenv.te_task decl in - let tkid = Counter.next cnt in - - let dumpin_opt = - match pi.pr_dumpin with - | None -> Os.getenv "EC_WHY3" - | Some filename -> Some (EcLocation.unloc filename) - in - ( dumpin_opt |> oiter (fun filename -> - Format.eprintf "dumping in %s" filename; - let filename = Printf.sprintf "%.4d-%s" tkid filename in - out_task filename task)); - let (tp, res) = EcUtils.timed (P.execute_task ?notify pi) task in - - if 1 <= pi.P.pr_verbose then - notify |> oiter (fun notify -> notify `Warning (lazy ( - Printf.sprintf "SMT done: %.5f\n%!" tp))); - res in +(* -------------------------------------------------------------------- *) +let select env pi hyps concl execute_task = if pi.P.pr_all then let init_select p ax = ax.ax_visibility = `Visible && not (P.Hints.mem p pi.P.pr_unwanted) in @@ -1712,3 +1673,54 @@ let check ?notify (pi : P.prover_infos) (hyps : LDecl.hyps) (concl : form) = end in aux pi.P.pr_max other 4 + +(* -------------------------------------------------------------------- *) +let cnt = Counter.create () + +let make_task tenv toadd decl= + List.iter (trans_axiom tenv) toadd; + WTask.add_decl tenv.te_task decl + +let check ?notify (pi : P.prover_infos) (hyps : LDecl.hyps) (concl : form) = + let out_task filename task = + let stream = open_out filename in + EcUtils.try_finally + (fun () -> Format.fprintf + (Format.formatter_of_out_channel stream) + "%a@." Why3.Pretty.print_task task) + (fun () -> close_out stream) in + + let env,hyps,tenv,decl = init hyps concl in + + let execute_task toadd = + if pi.P.pr_selected then begin + let buffer = Buffer.create 0 in + let fmt = Format.formatter_of_buffer buffer in + let ppe = EcPrinting.PPEnv.ofenv env in + let l = List.map fst toadd in + let pp fmt = EcPrinting.pp_list "@ " (EcPrinting.pp_axname ppe) fmt in + Format.fprintf fmt "selected lemmas: @[%a@]@." pp l; + notify |> oiter (fun notify -> notify `Warning + (lazy (Buffer.contents buffer))) + end; + + let task = make_task tenv toadd decl in + let tkid = Counter.next cnt in + + let dumpin_opt = + match pi.pr_dumpin with + | None -> Os.getenv "EC_WHY3" + | Some filename -> Some (EcLocation.unloc filename) + in + ( dumpin_opt |> oiter (fun filename -> + Format.eprintf "dumping in %s" filename; + let filename = Printf.sprintf "%.4d-%s" tkid filename in + out_task filename task)); + let (tp, res) = EcUtils.timed (P.execute_task ?notify pi) task in + + if 1 <= pi.P.pr_verbose then + notify |> oiter (fun notify -> notify `Warning (lazy ( + Printf.sprintf "SMT done: %.5f\n%!" tp))); + res + in + select env pi hyps concl execute_task diff --git a/src/ecSmt.mli b/src/ecSmt.mli index 2072d9f0c6..688f8dc655 100644 --- a/src/ecSmt.mli +++ b/src/ecSmt.mli @@ -4,13 +4,35 @@ open EcFol open EcEnv open EcProvers +(* -------------------------------------------------------------------- *) +type tenv + (* -------------------------------------------------------------------- *) val check : ?notify:notify -> prover_infos -> LDecl.hyps -> form -> bool val dump_why3 : env -> string -> unit -module Frequency : sig +(* -------------------------------------------------------------------- *) +val init : + EcEnv.LDecl.hyps + -> EcFol.form + -> EcEnv.env * EcBaseLogic.hyps * tenv * Why3.Decl.decl + + val select : + EcEnv.env + -> EcProvers.prover_infos + -> EcBaseLogic.hyps + -> EcFol.form + -> ((EcPath.path * EcDecl.axiom) list -> bool option) + -> bool + +val make_task : + tenv + -> (EcPath.path * EcDecl.axiom) list + -> Why3.Decl.decl + -> Why3.Task.task - (* -------------------------------------------------------------------- *) +(* -------------------------------------------------------------------- *) +module Frequency : sig type relevant = Sp.t * Sx.t val r_empty : relevant @@ -29,5 +51,4 @@ module Frequency : sig val f_ops : Sp.t -> form -> relevant val add : frequency -> EcFol.form -> unit - end diff --git a/src/ecUtils.ml b/src/ecUtils.ml index e768900274..609d3e6bf9 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -13,6 +13,10 @@ let rec makedirs (x : string) = Unix.mkdir x 0o755 end +(* -------------------------------------------------------------------- *) +let safe_unlink ~(filename : string) : unit = + try Unix.unlink filename with Unix.Unix_error _ -> () + (* -------------------------------------------------------------------- *) type 'data cb = Cb : 'a * ('data -> 'a -> unit) -> 'data cb @@ -681,7 +685,19 @@ module String = struct end (* -------------------------------------------------------------------- *) -module IO = BatIO +module IO : sig + include module type of BatIO + + val pp_to_file : filename:string -> (Format.formatter -> unit) -> unit +end = struct + include BatIO + + let pp_to_file ~(filename : string) (pp : Format.formatter -> unit) = + BatFile.with_file_out filename (fun channel -> + let fmt = BatFormat.formatter_of_output channel in + Format.fprintf fmt "%t@." pp + ) + end (* -------------------------------------------------------------------- *) module File = struct diff --git a/src/ecUtils.mli b/src/ecUtils.mli index 69603eabfc..047f48e0c8 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -8,6 +8,7 @@ val unexpected : unit -> 'a (* -------------------------------------------------------------------- *) val makedirs : string -> unit +val safe_unlink : filename:string -> unit (* -------------------------------------------------------------------- *) type 'data cb = Cb : 'a * ('data -> 'a -> unit) -> 'data cb @@ -208,6 +209,8 @@ end (* -------------------------------------------------------------------- *) module IO : sig include module type of BatIO + + val pp_to_file : filename:string -> (Format.formatter -> unit) -> unit end (* -------------------------------------------------------------------- *)