diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 18 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacarg.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 7 | ||||
| -rw-r--r-- | plugins/micromega/ZifyInst.v | 4 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 212 | ||||
| -rw-r--r-- | plugins/micromega/mutils.ml | 81 | ||||
| -rw-r--r-- | plugins/micromega/mutils.mli | 42 | ||||
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 4 |
10 files changed, 281 insertions, 111 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ca33e4e757..7be049269c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -920,20 +920,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decls.(IsProof Theorem)) () in - - let lemma = Lemmas.start_lemma - (*i The next call to mk_equation_id is valid since we are constructing the lemma - Ensures by: obvious - i*) - ~name:(mk_equation_id f_id) - ~poly:false - ~info - evd - lemma_type - in + + (*i The next call to mk_equation_id is valid since we are + constructing the lemma Ensures by: obvious i*) + let lemma = Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type in let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 570b72136c..6011af74e5 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1387,15 +1387,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decls.(IsProof Theorem)) () in - let lemma = Lemmas.start_lemma - ~name:lem_id - ~poly:false - ~info - !evd - typ in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in @@ -1456,11 +1448,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsProof Theorem) () in - let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info - sigma (fst lemmas_types_infos.(i)) in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c62aa0cf6b..4c5eab1a9b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1332,9 +1332,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma)) - () in + let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info @@ -1376,7 +1374,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx tac_start tac_end = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in + let info = Lemmas.Info.make ~hook () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 9e8e86d4fc..252c15478d 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -20,7 +20,7 @@ let make0 ?dyn name = wit let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *) -let wit_simple_intropattern = make0 "simple_intropattern" +let wit_simple_intropattern = make0 ~dyn:(val_tag (topwit wit_intropattern)) "simple_intropattern" let wit_quant_hyp = make0 "quant_hyp" let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index e64129d204..da89a027e2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -145,11 +145,8 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") let is_intro_pattern v = - if has_type v (topwit wit_intropattern [@warning "-3"]) then - Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v - else - if has_type v (topwit wit_simple_intropattern) then - Some (out_gen (topwit wit_simple_intropattern) v).CAst.v + if has_type v (topwit wit_intro_pattern) then + Some (out_gen (topwit wit_intro_pattern) v).CAst.v else None diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 3c44113604..1217e8a5f7 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -172,6 +172,10 @@ Program Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. Add UnOp Op_Z_of_N. +Instance Op_Z_to_N : UnOp Z.to_N := + { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }. +Add UnOp Op_Z_to_N. + Instance Op_Z_neg : UnOp Z.neg := { TUOp := Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}. Add UnOp Op_Z_neg. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ceb651abed..1772a3c333 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -50,6 +50,13 @@ let get_lia_option () = let get_lra_option () = !lra_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 = @@ -88,8 +95,38 @@ let () = optwrite = (fun x -> Certificate.dump_file := x) } in + let lia_cache_opt = + { + optdepr = false; + optname = "cache of lia (.lia.cache)"; + optkey = ["Lia" ; "Cache"]; + optread = (fun () -> !use_lia_cache); + optwrite = (fun x -> use_lia_cache := x) + } in + + let nia_cache_opt = + { + optdepr = false; + optname = "cache of nia (.nia.cache)"; + optkey = ["Nia" ; "Cache"]; + optread = (fun () -> !use_nia_cache); + optwrite = (fun x -> use_nia_cache := x) + } in + + let nra_cache_opt = + { + optdepr = false; + optname = "cache of nra (.nra.cache)"; + 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 @@ -745,7 +782,7 @@ struct (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) let eq_constr gl x y = let evd = gl.sigma in - match EConstr.eq_constr_universes gl.env evd x y with + match EConstr.eq_constr_universes_proj gl.env evd x y with | Some csts -> let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in begin @@ -769,15 +806,16 @@ struct ({vars=vars';gl=gl'}, CamlToCoq.positive n) let get_rank env v = - let evd = env.gl.sigma in + let gl = env.gl in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr evd e v - then n - else _get_rank l (n+1) in + match eq_constr gl e v with + | Some _ -> n + | None -> _get_rank l (n+1) + in _get_rank env.vars 1 let elements env = env.vars @@ -1978,13 +2016,47 @@ type provername = string * int option open Persistent_cache -module Cache = PHashtable(struct - type t = (provername * micromega_polys) - let equal = (=) - let hash = Hashtbl.hash -end) -let csdp_cache = ".csdp.cache" +module MakeCache(T : sig type prover_option + type coeff + val hash_prover_option : int -> prover_option -> int + val hash_coeff : int -> coeff -> int + val eq_prover_option : prover_option -> prover_option -> bool + val eq_coeff : coeff -> coeff -> bool + + end) = + struct + module E = + struct + type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list + + let equal = Hash.(eq_pair T.eq_prover_option (CList.equal (eq_pair (eq_pol T.eq_coeff) Hash.eq_op1))) + + let hash = + let hash_cstr = Hash.(hash_pair (hash_pol T.hash_coeff) hash_op1) in + Hash.( (hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) + end + + include PHashtable(E) + + 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 + + end + + + +module CacheCsdp = MakeCache(struct + type prover_option = provername + type coeff = Mc.q + let hash_prover_option = Hash.(hash_pair hash_string + (hash_elt (Option.hash (fun x -> x)))) + let eq_prover_option = Hash.(eq_pair String.equal + (Option.equal Int.equal)) + let hash_coeff = Hash.hash_q + let eq_coeff = Hash.eq_q + end) (** * Build the command to call csdpcert, and launch it. This in turn will call @@ -2017,7 +2089,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste *) let xcall_csdpcert = - Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb) + CacheCsdp.memo_opt use_csdp_cache ".csdp.cache" (fun (prover,pb) -> really_call_csdpcert prover pb) (** * Prover callback functions. @@ -2112,23 +2184,31 @@ let compact_pt pt f = let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) -module CacheZ = PHashtable(struct - type prover_option = bool * bool* int - type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheZ = MakeCache(struct + type prover_option = bool * bool* int + type coeff = Mc.z + let hash_prover_option : int -> prover_option -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option : prover_option -> prover_option -> bool = (=) + let eq_coeff = Hash.eq_z + let hash_coeff = Hash.hash_z + end) -module CacheQ = PHashtable(struct - type t = int * ((Mc.q Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheQ = MakeCache(struct + type prover_option = int + type coeff = Mc.q + let hash_prover_option : int -> int -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option = Int.equal + let eq_coeff = Hash.eq_q + let hash_coeff = Hash.hash_q + end) -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo ".nia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) +let memo_lia = CacheZ.memo_opt use_lia_cache ".lia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_nlia = CacheZ.memo_opt use_nia_cache ".nia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) +let memo_nra = CacheQ.memo_opt use_nra_cache ".nra.cache" + (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) @@ -2154,63 +2234,63 @@ let linear_prover_R = { } let nlinear_prover_R = { - name = "nra"; - get_option = get_lra_option; - prover = memo_nra ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "nra"; + get_option = get_lra_option; + prover = memo_nra ; + hyps = hyps_of_cone ; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Q str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_R str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone; - pp_prf = pp_psatz pp_q; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "real nonlinear prover"; + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone; + pp_prf = pp_psatz pp_q; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Z str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "lia"; + get_option = get_lia_option; + prover = memo_lia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let nlinear_Z = { - name = "nlia"; - get_option = get_lia_option; - prover = memo_nlia ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "nlia"; + get_option = get_lia_option; + prover = memo_nlia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } (** diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 537b6175b4..39905f8c52 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -233,6 +233,13 @@ struct | Zpos p -> (positive_big_int p) | Zneg p -> minus_big_int (positive_big_int p) + let z x = + match x with + | Z0 -> 0 + | Zpos p -> index p + | Zneg p -> - (index p) + + let q_to_num {qnum = x ; qden = y} = Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) @@ -420,6 +427,80 @@ let command exe_path args vl = stdout_read; stdout_write; stderr_read; stderr_write]) +(** Hashing utilities *) + +module Hash = + struct + + module Mc = Micromega + + open Hashset.Combine + + let int_of_eq_op1 = Mc.(function + | Equal -> 0 + | NonEqual -> 1 + | Strict -> 2 + | NonStrict -> 3) + + let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2 + + let hash_op1 h o = combine h (int_of_eq_op1 o) + + + let rec eq_positive p1 p2 = + match p1 , p2 with + | Mc.XH , Mc.XH -> true + | Mc.XI p1 , Mc.XI p2 -> eq_positive p1 p2 + | Mc.XO p1 , Mc.XO p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_z z1 z2 = + match z1 , z2 with + | Mc.Z0 , Mc.Z0 -> true + | Mc.Zpos p1, Mc.Zpos p2 + | Mc.Zneg p1, Mc.Zneg p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_q {Mc.qnum = qn1 ; Mc.qden = qd1} {Mc.qnum = qn2 ; Mc.qden = qd2} = + eq_z qn1 qn2 && eq_positive qd1 qd2 + + let rec eq_pol eq p1 p2 = + match p1 , p2 with + | Mc.Pc c1 , Mc.Pc c2 -> eq c1 c2 + | Mc.Pinj(i1,p1) , Mc.Pinj(i2,p2) -> eq_positive i1 i2 && eq_pol eq p1 p2 + | Mc.PX(p1,i1,p1') , Mc.PX(p2,i2,p2') -> + eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2' + | _ , _ -> false + + + let eq_pair eq1 eq2 (x1,y1) (x2,y2) = + eq1 x1 x2 && eq2 y1 y2 + + + let hash_pol helt = + let rec hash acc = function + | Mc.Pc c -> helt (combine acc 1) c + | Mc.Pinj(p,c) -> hash (combine (combine acc 1) (CoqToCaml.index p)) c + | Mc.PX(p1,i,p2) -> hash (hash (combine (combine acc 2) (CoqToCaml.index i)) p1) p2 in + hash + + + let hash_pair h1 h2 h (e1,e2) = + h2 (h1 h e1) e2 + + let hash_elt f h e = combine h (f e) + + let hash_string h (e:string) = hash_elt Hashtbl.hash h e + + let hash_z = hash_elt CoqToCaml.z + + let hash_q = hash_elt (fun q -> Hashtbl.hash (CoqToCaml.q_to_num q)) + + end + + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 8dbdea39e2..9692bc631b 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -67,14 +67,46 @@ end module CoqToCaml : sig val z_big_int : Micromega.z -> Big_int.big_int - val q_to_num : Micromega.q -> Num.num - val positive : Micromega.positive -> int - val n : Micromega.n -> int - val nat : Micromega.nat -> int - val index : Micromega.positive -> int + val z : Micromega.z -> int + val q_to_num : Micromega.q -> Num.num + val positive : Micromega.positive -> int + val n : Micromega.n -> int + val nat : Micromega.nat -> int + val index : Micromega.positive -> int end +module Hash : sig + + val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool + + val eq_positive : Micromega.positive -> Micromega.positive -> bool + + val eq_z : Micromega.z -> Micromega.z -> bool + + val eq_q : Micromega.q -> Micromega.q -> bool + + val eq_pol : ('a -> 'a -> bool) -> 'a Micromega.pol -> 'a Micromega.pol -> bool + + val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a * 'b -> 'a * 'b -> bool + + val hash_op1 : int -> Micromega.op1 -> int + + val hash_pol : (int -> 'a -> int) -> int -> 'a Micromega.pol -> int + + val hash_pair : (int -> 'a -> int) -> (int -> 'b -> int) -> int -> 'a * 'b -> int + + val hash_z : int -> Micromega.z -> int + + val hash_q : int -> Micromega.q -> int + + val hash_string : int -> string -> int + + val hash_elt : ('a -> int) -> int -> 'a -> int + +end + + val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 14a1bc9712..14e2e40846 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -127,7 +127,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.replace htbl key elem ; + Table.add htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -164,7 +164,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.replace tbl k e ; + Table.add tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; |