diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/certificate.ml | 20 | ||||
| -rw-r--r-- | plugins/micromega/certificate.mli | 6 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 471 | ||||
| -rw-r--r-- | plugins/micromega/dune (renamed from plugins/micromega/plugin_base.dune) | 2 | ||||
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 46 |
5 files changed, 191 insertions, 354 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 1958fff4cc..9eeba614c7 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -27,7 +27,13 @@ open NumCompat open Q.Notations open Mutils -let use_simplex = ref true +let use_simplex = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true + +(* If set to some [file], arithmetic goals are dumped in [file].v *) + +let dump_file = + Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"] type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res @@ -203,19 +209,19 @@ let fourier_linear_prover l = | Inl _ -> None let direct_linear_prover l = - if !use_simplex then Simplex.find_unsat_certificate l + if use_simplex () then Simplex.find_unsat_certificate l else fourier_linear_prover l let find_point l = let open Util in - if !use_simplex then Simplex.find_point l + if use_simplex () then Simplex.find_point l else match Mfourier.Fourier.find_point l with | Inr _ -> None | Inl cert -> Some cert let optimise v l = - if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l + if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l let dual_raw_certificate l = if debug then begin @@ -981,13 +987,11 @@ let xlia_simplex env red sys = with FoundProof prf -> compile_prf sys (Step (0, prf, Done)) let xlia env0 en red sys = - if !use_simplex then xlia_simplex env0 red sys else xlia en red sys - -let dump_file = ref None + if use_simplex () then xlia_simplex env0 red sys else xlia en red sys let gen_bench (tac, prover) can_enum prfdepth sys = let res = prover can_enum prfdepth sys in - ( match !dump_file with + ( match dump_file () with | None -> () | Some file -> let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli index cabd36ebb7..5b215549b0 100644 --- a/plugins/micromega/certificate.mli +++ b/plugins/micromega/certificate.mli @@ -12,16 +12,12 @@ module Mc = Micromega (** [use_simplex] is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier *) -val use_simplex : bool ref +val use_simplex : unit -> bool type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res type qres = (Mc.q Mc.psatz, int * Mc.q list) res -(** [dump_file] is bound to the Coq option Dump Arith. - If set to some [file], arithmetic goals are dumped in filexxx.v *) -val dump_file : string option ref - (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *) val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 43f6f5a35e..ee2c87d19a 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -37,74 +37,31 @@ let debug = false let max_depth = max_int (* Search limit for provers over Q R *) -let lra_proof_depth = ref max_depth +let lra_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth (* Search limit for provers over Z *) -let lia_enum = ref true -let lia_proof_depth = ref max_depth -let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth) -let get_lra_option () = !lra_proof_depth +let lia_enum = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true + +let lia_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth + +let get_lia_option () = + (Certificate.use_simplex (), lia_enum (), lia_proof_depth ()) (* Enable/disable caches *) -let use_lia_cache = ref true -let use_nia_cache = ref true -let use_nra_cache = ref true -let use_csdp_cache = ref true - -let () = - let int_opt l vref = - { optdepr = false - ; optkey = l - ; optread = (fun () -> Some !vref) - ; optwrite = - (fun x -> vref := match x with None -> max_depth | Some v -> v) } - in - let lia_enum_opt = - { optdepr = false - ; optkey = ["Lia"; "Enum"] - ; optread = (fun () -> !lia_enum) - ; optwrite = (fun x -> lia_enum := x) } - in - let solver_opt = - { optdepr = false - ; optkey = ["Simplex"] - ; optread = (fun () -> !Certificate.use_simplex) - ; optwrite = (fun x -> Certificate.use_simplex := x) } - in - let dump_file_opt = - { optdepr = false - ; optkey = ["Dump"; "Arith"] - ; optread = (fun () -> !Certificate.dump_file) - ; optwrite = (fun x -> Certificate.dump_file := x) } - in - let lia_cache_opt = - { optdepr = false - ; optkey = ["Lia"; "Cache"] - ; optread = (fun () -> !use_lia_cache) - ; optwrite = (fun x -> use_lia_cache := x) } - in - let nia_cache_opt = - { optdepr = false - ; optkey = ["Nia"; "Cache"] - ; optread = (fun () -> !use_nia_cache) - ; optwrite = (fun x -> use_nia_cache := x) } - in - let nra_cache_opt = - { optdepr = false - ; optkey = ["Nra"; "Cache"] - ; optread = (fun () -> !use_nra_cache) - ; optwrite = (fun x -> use_nra_cache := x) } - in - let () = declare_bool_option solver_opt in - let () = declare_bool_option lia_cache_opt in - let () = declare_bool_option nia_cache_opt in - let () = declare_bool_option nra_cache_opt in - let () = declare_stringopt_option dump_file_opt in - let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let () = declare_bool_option lia_enum_opt in - () +let use_lia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true + +let use_nia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true + +let use_nra_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true + +let use_csdp_cache () = true (** * Initialize a tag type to the Tag module declaration (see Mutils). @@ -171,249 +128,142 @@ let selecti s m = *) module M = struct (** - * Location of the Coq libraries. - *) - - let logic_dir = ["Coq"; "Logic"; "Decidable"] - - let mic_modules = - [ ["Coq"; "Lists"; "List"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "DeclConstant"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "RMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "QArith"; "QArith_base"] - ; ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["LRing_normalise"] ] - - [@@@ocaml.warning "-3"] - - let coq_modules = - Coqlib.( - init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules - @ mic_modules) - - let bin_module = [["Coq"; "Numbers"; "BinNums"]] - - let r_modules = - [ ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["Coq"; "Reals"; "Raxioms"] - ; ["Coq"; "QArith"; "Qreals"] ] - - let z_modules = [["Coq"; "ZArith"; "BinInt"]] - - (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v *) - let gen_constant_in_modules s m n = + let constr_of_ref str = EConstr.of_constr - ( UnivGen.constr_of_monomorphic_global - @@ Coqlib.gen_reference_in_modules s m n ) - - let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules - - [@@@ocaml.warning "+3"] - - let constant = gen_constant_in_modules "ZMicromega" coq_modules - let bin_constant = gen_constant_in_modules "ZMicromega" bin_module - let r_constant = gen_constant_in_modules "ZMicromega" r_modules - let z_constant = gen_constant_in_modules "ZMicromega" z_modules - let m_constant = gen_constant_in_modules "ZMicromega" mic_modules - let coq_and = lazy (init_constant "and") - let coq_or = lazy (init_constant "or") - let coq_not = lazy (init_constant "not") - let coq_iff = lazy (init_constant "iff") - let coq_True = lazy (init_constant "True") - let coq_False = lazy (init_constant "False") - let coq_cons = lazy (constant "cons") - let coq_nil = lazy (constant "nil") - let coq_list = lazy (constant "list") - let coq_O = lazy (init_constant "O") - let coq_S = lazy (init_constant "S") - let coq_nat = lazy (init_constant "nat") - let coq_unit = lazy (init_constant "unit") + (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) + + let coq_and = lazy (constr_of_ref "core.and.type") + let coq_or = lazy (constr_of_ref "core.or.type") + let coq_not = lazy (constr_of_ref "core.not.type") + let coq_iff = lazy (constr_of_ref "core.iff.type") + let coq_True = lazy (constr_of_ref "core.True.type") + let coq_False = lazy (constr_of_ref "core.False.type") + let coq_cons = lazy (constr_of_ref "core.list.cons") + let coq_nil = lazy (constr_of_ref "core.list.nil") + let coq_list = lazy (constr_of_ref "core.list.type") + let coq_O = lazy (constr_of_ref "num.nat.O") + let coq_S = lazy (constr_of_ref "num.nat.S") + let coq_nat = lazy (constr_of_ref "num.nat.type") + let coq_unit = lazy (constr_of_ref "core.unit.type") (* let coq_option = lazy (init_constant "option")*) - let coq_None = lazy (init_constant "None") - let coq_tt = lazy (init_constant "tt") - let coq_Inl = lazy (init_constant "inl") - let coq_Inr = lazy (init_constant "inr") - let coq_N0 = lazy (bin_constant "N0") - let coq_Npos = lazy (bin_constant "Npos") - let coq_xH = lazy (bin_constant "xH") - let coq_xO = lazy (bin_constant "xO") - let coq_xI = lazy (bin_constant "xI") - let coq_Z = lazy (bin_constant "Z") - let coq_ZERO = lazy (bin_constant "Z0") - let coq_POS = lazy (bin_constant "Zpos") - let coq_NEG = lazy (bin_constant "Zneg") - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - let coq_Qmake = lazy (constant "Qmake") - let coq_Rcst = lazy (constant "Rcst") - let coq_C0 = lazy (m_constant "C0") - let coq_C1 = lazy (m_constant "C1") - let coq_CQ = lazy (m_constant "CQ") - let coq_CZ = lazy (m_constant "CZ") - let coq_CPlus = lazy (m_constant "CPlus") - let coq_CMinus = lazy (m_constant "CMinus") - let coq_CMult = lazy (m_constant "CMult") - let coq_CPow = lazy (m_constant "CPow") - let coq_CInv = lazy (m_constant "CInv") - let coq_COpp = lazy (m_constant "COpp") - let coq_R0 = lazy (constant "R0") - let coq_R1 = lazy (constant "R1") - let coq_proofTerm = lazy (constant "ZArithProof") - let coq_doneProof = lazy (constant "DoneProof") - let coq_ratProof = lazy (constant "RatProof") - let coq_cutProof = lazy (constant "CutProof") - let coq_enumProof = lazy (constant "EnumProof") - let coq_ExProof = lazy (constant "ExProof") - let coq_Zgt = lazy (z_constant "Z.gt") - let coq_Zge = lazy (z_constant "Z.ge") - let coq_Zle = lazy (z_constant "Z.le") - let coq_Zlt = lazy (z_constant "Z.lt") - let coq_Eq = lazy (init_constant "eq") - let coq_Zplus = lazy (z_constant "Z.add") - let coq_Zminus = lazy (z_constant "Z.sub") - let coq_Zopp = lazy (z_constant "Z.opp") - let coq_Zmult = lazy (z_constant "Z.mul") - let coq_Zpower = lazy (z_constant "Z.pow") - let coq_Qle = lazy (constant "Qle") - let coq_Qlt = lazy (constant "Qlt") - let coq_Qeq = lazy (constant "Qeq") - let coq_Qplus = lazy (constant "Qplus") - let coq_Qminus = lazy (constant "Qminus") - let coq_Qopp = lazy (constant "Qopp") - let coq_Qmult = lazy (constant "Qmult") - let coq_Qpower = lazy (constant "Qpower") - let coq_Rgt = lazy (r_constant "Rgt") - let coq_Rge = lazy (r_constant "Rge") - let coq_Rle = lazy (r_constant "Rle") - let coq_Rlt = lazy (r_constant "Rlt") - let coq_Rplus = lazy (r_constant "Rplus") - let coq_Rminus = lazy (r_constant "Rminus") - let coq_Ropp = lazy (r_constant "Ropp") - let coq_Rmult = lazy (r_constant "Rmult") - let coq_Rinv = lazy (r_constant "Rinv") - let coq_Rpower = lazy (r_constant "pow") - let coq_powerZR = lazy (r_constant "powerRZ") - let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (r_constant "Q2R") - let coq_PEX = lazy (constant "PEX") - let coq_PEc = lazy (constant "PEc") - let coq_PEadd = lazy (constant "PEadd") - let coq_PEopp = lazy (constant "PEopp") - let coq_PEmul = lazy (constant "PEmul") - let coq_PEsub = lazy (constant "PEsub") - let coq_PEpow = lazy (constant "PEpow") - let coq_PX = lazy (constant "PX") - let coq_Pc = lazy (constant "Pc") - let coq_Pinj = lazy (constant "Pinj") - let coq_OpEq = lazy (constant "OpEq") - let coq_OpNEq = lazy (constant "OpNEq") - let coq_OpLe = lazy (constant "OpLe") - let coq_OpLt = lazy (constant "OpLt") - let coq_OpGe = lazy (constant "OpGe") - let coq_OpGt = lazy (constant "OpGt") - let coq_PsatzIn = lazy (constant "PsatzIn") - let coq_PsatzSquare = lazy (constant "PsatzSquare") - let coq_PsatzMulE = lazy (constant "PsatzMulE") - let coq_PsatzMultC = lazy (constant "PsatzMulC") - let coq_PsatzAdd = lazy (constant "PsatzAdd") - let coq_PsatzC = lazy (constant "PsatzC") - let coq_PsatzZ = lazy (constant "PsatzZ") + let coq_None = lazy (constr_of_ref "core.option.None") + let coq_tt = lazy (constr_of_ref "core.unit.tt") + let coq_Inl = lazy (constr_of_ref "core.sum.inl") + let coq_Inr = lazy (constr_of_ref "core.sum.inr") + let coq_N0 = lazy (constr_of_ref "num.N.N0") + let coq_Npos = lazy (constr_of_ref "num.N.Npos") + let coq_xH = lazy (constr_of_ref "num.pos.xH") + let coq_xO = lazy (constr_of_ref "num.pos.xO") + let coq_xI = lazy (constr_of_ref "num.pos.xI") + let coq_Z = lazy (constr_of_ref "num.Z.type") + let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") + let coq_POS = lazy (constr_of_ref "num.Z.Zpos") + let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") + let coq_Q = lazy (constr_of_ref "rat.Q.type") + let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") + let coq_R = lazy (constr_of_ref "reals.R.type") + let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") + let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") + let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") + let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") + let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") + let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") + let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") + let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") + let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") + let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") + let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") + let coq_R0 = lazy (constr_of_ref "reals.R.R0") + let coq_R1 = lazy (constr_of_ref "reals.R.R1") + let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") + let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") + let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") + let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") + let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") + let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") + let coq_Zgt = lazy (constr_of_ref "num.Z.gt") + let coq_Zge = lazy (constr_of_ref "num.Z.ge") + let coq_Zle = lazy (constr_of_ref "num.Z.le") + let coq_Zlt = lazy (constr_of_ref "num.Z.lt") + let coq_Eq = lazy (constr_of_ref "core.eq.type") + let coq_Zplus = lazy (constr_of_ref "num.Z.add") + let coq_Zminus = lazy (constr_of_ref "num.Z.sub") + let coq_Zopp = lazy (constr_of_ref "num.Z.opp") + let coq_Zmult = lazy (constr_of_ref "num.Z.mul") + let coq_Zpower = lazy (constr_of_ref "num.Z.pow") + let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") + let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") + let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") + let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") + let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") + let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") + let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") + let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") + let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") + let coq_Rge = lazy (constr_of_ref "reals.R.Rge") + let coq_Rle = lazy (constr_of_ref "reals.R.Rle") + let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") + let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") + let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") + let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") + let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") + let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") + let coq_Rpower = lazy (constr_of_ref "reals.R.pow") + let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") + let coq_IZR = lazy (constr_of_ref "reals.R.IZR") + let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") + let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") + let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") + let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") + let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") + let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") + let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") + let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") + let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") + let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") + let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") + let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") + let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") + let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") + let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") + let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") + let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") + let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") + let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") + let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") + let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") + let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") + let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") + let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") (* let coq_GT = lazy (m_constant "GT")*) - let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant") - - let coq_TT = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "TT") - - let coq_FF = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "FF") - - let coq_And = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "Cj") + let coq_DeclaredConstant = + lazy (constr_of_ref "micromega.DeclaredConstant.type") - let coq_Or = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "D") - - let coq_Neg = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "N") - - let coq_Atom = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "A") - - let coq_X = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "X") - - let coq_Impl = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "I") - - let coq_Formula = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "BFormula") + let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") + let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") + let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj") + let coq_Or = lazy (constr_of_ref "micromega.GFormula.D") + let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N") + let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") + let coq_X = lazy (constr_of_ref "micromega.GFormula.X") + let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I") + let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") (** * Initialization : a few Caml symbols are derived from other libraries; * QMicromega, ZArithRing, RingMicromega. *) - let coq_QWitness = - lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "QMicromega"]] - "QWitness") - - let coq_Build = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Build_Formula") - - let coq_Cstr = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Formula") + let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") + let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") + let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") (** * Parsing and dumping : transformation functions between Caml and Coq @@ -1361,29 +1211,10 @@ end open M -let coq_Branch = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Branch") - -let coq_Elt = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Elt") - -let coq_Empty = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Empty") - -let coq_VarMap = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t") +let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch") +let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt") +let coq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty") +let coq_VarMap = lazy (constr_of_ref "micromega.VarMap.type") let rec dump_varmap typ m = match m with @@ -1943,13 +1774,7 @@ let micromega_order_changer cert env ff = [ ( "__ff" , ff , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) - ; ( "__varmap" - , vm - , EConstr.mkApp - ( gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t" - , [|typ|] ) ) + ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|])) ; ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) @@ -2101,7 +1926,7 @@ struct let memo_opt use_cache cache_file f = let memof = memo cache_file f in - fun x -> if !use_cache then memof x else f x + fun x -> if use_cache () then memof x else f x end module CacheCsdp = MakeCache (struct @@ -2281,7 +2106,7 @@ let memo_nra = let linear_prover_Q = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2292,7 +2117,7 @@ let linear_prover_Q = let linear_prover_R = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2303,7 +2128,7 @@ let linear_prover_R = let nlinear_prover_R = { name = "nra" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = memo_nra ; hyps = hyps_of_cone ; compact = compact_cone diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune index 4153d06161..33ad3a0138 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/dune @@ -20,3 +20,5 @@ (modules g_zify zify) (synopsis "Coq's zify plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index f157a807ad..9051bbb5ca 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -41,13 +41,21 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct type mode = Closed | Open type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t} - let finally f rst = - try - let res = f () in - rst (); res - with reraise -> - (try rst () with any -> raise reraise); - raise reraise + (* XXX: Move to Fun.protect once in Ocaml 4.08 *) + let fun_protect ~(finally : unit -> unit) work = + let finally_no_exn () = + let exception Finally_raised of exn in + try finally () + with e -> + let bt = Printexc.get_raw_backtrace () in + Printexc.raise_with_backtrace (Finally_raised e) bt + in + match work () with + | result -> finally_no_exn (); result + | exception work_exn -> + let work_bt = Printexc.get_raw_backtrace () in + finally_no_exn (); + Printexc.raise_with_backtrace work_exn work_bt let read_key_elem inch = try Some (Marshal.from_channel inch) with @@ -76,21 +84,23 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct let unlock fd = let pos = lseek fd 0 SEEK_CUR in - try - ignore (lseek fd 0 SEEK_SET); - lockf fd F_ULOCK 1 - with Unix.Unix_error (_, _, _) -> - () - (* Here, this is really bad news -- - there is a pending lock which could cause a deadlock. - Should it be an anomaly or produce a warning ? - *); - ignore (lseek fd pos SEEK_SET) + let () = + try + ignore (lseek fd 0 SEEK_SET); + lockf fd F_ULOCK 1 + with Unix.Unix_error (_, _, _) -> + (* Here, this is really bad news -- + there is a pending lock which could cause a deadlock. + Should it be an anomaly or produce a warning ? + *) + () + in + ignore (lseek fd pos SEEK_SET) (* We make the assumption that an acquired lock can always be released *) let do_under_lock kd fd f = - if lock kd fd then finally f (fun () -> unlock fd) else f () + if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f () let open_in f = let flags = [O_RDONLY; O_CREAT] in |