diff options
Diffstat (limited to 'plugins')
30 files changed, 1533 insertions, 1212 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 57268a9cf..5a49fc8f4 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,3 +1,4 @@ +open Proofview.Notations let contrib_name = "btauto" @@ -216,7 +217,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let t = decomp_term concl in @@ -228,10 +229,10 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end + end } let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in @@ -255,6 +256,6 @@ module Btauto = struct | _ -> let msg = str "Cannot recognize a boolean equality" in Tacticals.New.tclFAIL 0 msg - end + end } end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0baa53370..09d9cf019 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -22,6 +22,7 @@ open Ccproof open Pp open Errors open Util +open Proofview.Notations let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -254,13 +255,13 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) - end + end } let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with @@ -325,10 +326,10 @@ let rec proof_tac p : unit Proofview.tactic = app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl @@ -338,14 +339,14 @@ let refute_tac c t1 t2 p = let false_t=mkApp (c,[|mkVar hid|]) in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - end + end } let refine_exact_check c gl = let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl @@ -357,20 +358,20 @@ let convert_to_goal_tac c t1 t2 p = let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] - end + end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt2=constr_of_term t2 in let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in let false_t=mkApp (c2,[|mkVar h|]) in Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] - end + end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl @@ -384,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p = let identity = Universes.constr_of_global (Lazy.force _I) in (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -399,7 +400,7 @@ let discriminate_tac (cstr,u as cstru) p = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) - end + end } (* wrap everything *) @@ -411,7 +412,7 @@ let build_term_to_complete uf meta pac = applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (Pp.str "Reading subgoal ...") in let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in @@ -462,7 +463,7 @@ let cc_tactic depth additionnal_terms = convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> convert_to_hyp_tac ida ta idb tb p - end + end } let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") @@ -485,8 +486,7 @@ let congruence_tac depth l = let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter begin - fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in @@ -494,10 +494,10 @@ let mk_eq f c1 c2 k = let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) - end) + end }) let f_equal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) @@ -523,4 +523,4 @@ let f_equal = | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end - end + end } diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index ba9fb728c..f47b35541 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,6 +29,7 @@ open Termops open Namegen open Goptions open Misctypes +open Sigma.Notations (* Strictness option *) @@ -86,7 +87,7 @@ Please \"suppose\" something or \"end\" it now." | _ -> () let mk_evd metalist gls = - let evd0= create_goal_evar_defs (sig_sig gls) in + let evd0= clear_metas (sig_sig gls) in let add_one (meta,typ) evd = meta_declare meta typ evd in List.fold_right add_one metalist evd0 @@ -1305,7 +1306,11 @@ let understand_my_constr env sigma c concl = Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) let my_refine c gls = - let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + let oc = { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + Sigma.Unsafe.of_pair (c, sigma) + end } in Proofview.V82.of_tactic (Tactics.New.refine oc) gls (* end focus/claim *) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index ce93c5a3f..a47dc5b2f 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -93,6 +93,7 @@ let start_deriving f suchthat lemma = ignore (Declare.declare_constant lemma lemma_def) in + let terminator = Proof_global.make_terminator terminator in let () = Proof_global.start_dependent_proof lemma kind goals terminator in let _ = Proof_global.with_current_proof begin fun _ p -> Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 10644da25..38aef62e1 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index d7842e127..466c8054b 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str ("Please load library "^(DirPath.to_string dp^" first."))) + err (str "Please load library " ++ pr_dirpath dp ++ str " first.") | _ -> () end | _ -> () diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 39d99d2e0..0f70d3ea0 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Globnames val qflag : bool ref @@ -27,7 +26,7 @@ type counter = bool -> metavariable val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> rel_context array + Proof_type.goal Tacmach.sigma -> Context.Rel.t array type atoms = {positive:constr list;negative:constr list} diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 041526881..25509b4b5 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -52,8 +52,15 @@ let _= in declare_int_option gdopt +let default_intuition_tac = + let tac _ _ = Auto.h_auto None [] None in + let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in + let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in + Tacenv.register_ml_tactic name [| tac |]; + Tacexpr.TacML (Loc.ghost, entry, []) + let (set_default_solver, default_solver, print_default_solver) = - Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver" + Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 72e9371be..4c0aa6c75 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -19,6 +19,7 @@ open Globnames open Tacmach open Fourier open Contradiction +open Proofview.Notations (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -412,13 +413,6 @@ let tac_zero_infeq_false gl (n,d) = (tac_zero_inf_pos gl (-n,d))) ;; -let create_meta () = mkMeta(Evarutil.new_meta());; - -let my_cut c gl= - let concl = pf_concl gl in - apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl -;; - let exact = exact_check;; let tac_use h = @@ -462,7 +456,7 @@ exception GoalDone (* Résolution d'inéquations linéaires dans R *) let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast concl in @@ -586,7 +580,7 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + tac:=(Tacticals.New.tclTHENS (cut ineq) [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] )) @@ -622,7 +616,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end + end } ;; (* diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 169a70600..4eab5f912 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -3,12 +3,12 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Declarations open Pp open Tacmach +open Termops open Proof_type open Tacticals open Tactics @@ -52,10 +52,10 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end @@ -229,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta -let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = +let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t ); @@ -705,7 +705,7 @@ let build_proof in tclTHENSEQ [ - Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( @@ -932,7 +932,7 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) )) + ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) )) ((* observe_tac "thin" *) (thin to_revert)) g @@ -1472,7 +1472,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = tclCOMPLETE( Eauto.eauto_with_bases (true,5) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ) ) @@ -1562,7 +1562,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l) + tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda..e2c3bbb97 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -3,7 +3,6 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Pp @@ -12,6 +11,7 @@ open Tactics open Indfun_common open Functional_principles_proofs open Misctypes +open Sigma.Notations exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -29,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env = Global.env () in let env_with_params = Environ.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context = + let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = match predicates with | [] -> [] |(Name x,v,t)::predicates -> @@ -648,12 +648,15 @@ let build_case_scheme fa = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes in - let ind_fun = + let (ind, sf) = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma, scheme = - (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (scheme, sigma, _) = + Indrec.build_case_analysis_scheme_default env sigma ind sf + in + let sigma = Sigma.to_evar_map sigma in let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a15e46bfe..97b9e95e1 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -55,7 +55,9 @@ let pr_with_bindings_typed prc prlc (c,bl) = let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) + | Some b -> + let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in + spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) ARGUMENT EXTEND fun_ind_using diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 5d92fca5e..80de8e764 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = let new_env = add_pat_variables env pat typ in let res = fst ( - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dbd43806..d1e109825 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,6 +10,7 @@ open Glob_term open Declarations open Misctypes open Decl_kinds +open Sigma.Notations let is_rec_info scheme_info = let test_branche min acc (_,_,br) = @@ -85,7 +86,7 @@ let functional_induction with_clean c princl pat = in let encoded_pat_as_patlist = List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in @@ -727,9 +728,9 @@ let rec add_args id new_args b = List.map (fun (e,o) -> add_args id new_args e,o) bl) | CCases(loc,sty,b_option,cel,cal) -> CCases(loc,sty,Option.map (add_args id new_args) b_option, - List.map (fun (b,(na,b_option)) -> + List.map (fun (b,na,b_option) -> add_args id new_args b, - (na, b_option)) cel, + na, b_option) cel, List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal ) | CLetTuple(loc,nal,(na,b_option),b1,b2) -> @@ -751,10 +752,8 @@ let rec add_args id new_args b = | CCast(loc,b1,b2) -> CCast(loc,add_args id new_args b1, Miscops.map_cast_type (add_args id new_args) b2) - | CRecord (loc, w, pars) -> - CRecord (loc, - (match w with Some w -> Some (add_args id new_args w) | _ -> None), - List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CRecord (loc, pars) -> + CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") | CPrim _ -> b diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index a800c186a..0c9d3bb81 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,6 +19,7 @@ open Tactics open Indfun_common open Tacmach open Misctypes +open Termops (* Some pretty printing function for debugging purpose *) @@ -70,8 +71,8 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - observe (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal " ++ goal ); + observe (hov 0 (str "observation "++ s++str " raised exception " ++ + Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; @@ -457,7 +458,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | (id,None,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id]) + (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -698,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = }) Locusops.onConcl ; - Simple.generalize (List.map mkVar ids); + generalize (List.map mkVar ids); thin ids ] else @@ -737,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = tclTHENSEQ [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" - (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); + (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) @@ -920,7 +921,7 @@ let revert_graph kn post_tac hid g = let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ - Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); post_tac hid @@ -964,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic = in tclTHENSEQ[ pre_tac hid; - Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 87d7ca76d..57782dd71 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Declarations open Glob_term @@ -258,27 +257,27 @@ type merge_infos = lnk2: int merged_arg array; (** rec params which remain rec param (ie not linked) *) - recprms1: rel_declaration list; - recprms2: rel_declaration list; + recprms1: Context.Rel.Declaration.t list; + recprms2: Context.Rel.Declaration.t list; nrecprms1: int; nrecprms2: int; (** rec parms which became non parm (either linked to something or because after a rec parm that became non parm) *) - otherprms1: rel_declaration list; - otherprms2: rel_declaration list; + otherprms1: Context.Rel.Declaration.t list; + otherprms2: Context.Rel.Declaration.t list; notherprms1:int; notherprms2:int; (** args which remain args in merge *) - args1:rel_declaration list; - args2:rel_declaration list; + args1:Context.Rel.Declaration.t list; + args2:Context.Rel.Declaration.t list; nargs1:int; nargs2:int; (** functional result args *) - funresprms1: rel_declaration list; - funresprms2: rel_declaration list; + funresprms1: Context.Rel.Declaration.t list; + funresprms2: Context.Rel.Declaration.t list; nfunresprms1:int; nfunresprms2:int; } @@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift lident , bindlist , Some cstr_expr , lcstor_expr -let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = +let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] (Global.env()) Evd.empty t in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 065d0fe53..b09678341 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -29,6 +29,7 @@ open Proof_type open Pfedit open Glob_term open Pretyping +open Termops open Constrintern open Misctypes open Genredexpr @@ -38,6 +39,7 @@ open Auto open Eauto open Indfun_common +open Sigma.Notations @@ -212,10 +214,10 @@ let rec print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); end; (* print_debug_queue false e; *) end @@ -685,11 +687,14 @@ let mkDestructEq : to_revert_constr in pf_typel new_hyps (fun _ -> observe_tclTHENLIST (str "mkDestructEq") - [Simple.generalize new_hyps; + [generalize new_hyps; (fun g2 -> - Proofview.V82.of_tactic (change_in_concl None - (fun patvars sigma -> - pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2); + let changefun patvars = { run = fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in + Sigma.Unsafe.of_pair (c, sigma) + } in + Proofview.V82.of_tactic (change_in_concl None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert @@ -1110,7 +1115,7 @@ let termination_proof_header is_mes input_type ids args_id relation [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> - tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id])) + tclTHEN (Tactics.generalize [mkVar id]) (clear [id])) )) ; observe_tac (str "fix") (fix (Some hrec) (nargs+1)); @@ -1300,7 +1305,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") [ - Simple.generalize [lemma]; + generalize [lemma]; Proofview.V82.of_tactic (Simple.intro hid); (fun g -> let ids = pf_ids_of_hyps g in @@ -1327,10 +1332,10 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp tclFIRST[ tclTHEN (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) - e_assumption; + (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ] ) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index a461b26a0..50e0033e5 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -96,6 +96,14 @@ Ltac psatzl dom := Ltac lra := first [ psatzl R | psatzl Q ]. +Ltac nra := + unfold Rdiv in * ; + xnra ; + abstract + (intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + (* Local Variables: *) diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index a5fceb562..914881db0 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -63,82 +63,82 @@ let r_spec = z_spec let dev_form n_spec p = let rec dev_form p = match p with - | Mc.PEc z -> Poly.constant (n_spec.number_to_num z) - | Mc.PEX v -> Poly.variable (C2Ml.positive v) - | Mc.PEmul(p1,p2) -> - let p1 = dev_form p1 in - let p2 = dev_form p2 in - Poly.product p1 p2 - | Mc.PEadd(p1,p2) -> Poly.addition (dev_form p1) (dev_form p2) - | Mc.PEopp p -> Poly.uminus (dev_form p) - | Mc.PEsub(p1,p2) -> Poly.addition (dev_form p1) (Poly.uminus (dev_form p2)) - | Mc.PEpow(p,n) -> - let p = dev_form p in - let n = C2Ml.n n in - let rec pow n = - if Int.equal n 0 - then Poly.constant (n_spec.number_to_num n_spec.unit) - else Poly.product p (pow (n-1)) in - pow n in - dev_form p + | Mc.PEc z -> Poly.constant (n_spec.number_to_num z) + | Mc.PEX v -> Poly.variable (C2Ml.positive v) + | Mc.PEmul(p1,p2) -> + let p1 = dev_form p1 in + let p2 = dev_form p2 in + Poly.product p1 p2 + | Mc.PEadd(p1,p2) -> Poly.addition (dev_form p1) (dev_form p2) + | Mc.PEopp p -> Poly.uminus (dev_form p) + | Mc.PEsub(p1,p2) -> Poly.addition (dev_form p1) (Poly.uminus (dev_form p2)) + | Mc.PEpow(p,n) -> + let p = dev_form p in + let n = C2Ml.n n in + let rec pow n = + if Int.equal n 0 + then Poly.constant (n_spec.number_to_num n_spec.unit) + else Poly.product p (pow (n-1)) in + pow n in + dev_form p let monomial_to_polynomial mn = Monomial.fold (fun v i acc -> - let v = Ml2C.positive v in - let mn = if Int.equal i 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in - if Pervasives.(=) acc (Mc.PEc (Mc.Zpos Mc.XH)) (** FIXME *) - then mn - else Mc.PEmul(mn,acc)) - mn - (Mc.PEc (Mc.Zpos Mc.XH)) + let v = Ml2C.positive v in + let mn = if Int.equal i 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in + if Pervasives.(=) acc (Mc.PEc (Mc.Zpos Mc.XH)) (** FIXME *) + then mn + else Mc.PEmul(mn,acc)) + mn + (Mc.PEc (Mc.Zpos Mc.XH)) let list_to_polynomial vars l = assert (List.for_all (fun x -> ceiling_num x =/ x) l); let var x = monomial_to_polynomial (List.nth vars x) in - + let rec xtopoly p i = function | [] -> p | c::l -> if c =/ (Int 0) then xtopoly p (i+1) l - else let c = Mc.PEc (Ml2C.bigint (numerator c)) in - let mn = - if Pervasives.(=) c (Mc.PEc (Mc.Zpos Mc.XH)) - then var i - else Mc.PEmul (c,var i) in - let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else - Mc.PEadd (mn, p) in - xtopoly p' (i+1) l in - - xtopoly (Mc.PEc Mc.Z0) 0 l + else let c = Mc.PEc (Ml2C.bigint (numerator c)) in + let mn = + if Pervasives.(=) c (Mc.PEc (Mc.Zpos Mc.XH)) + then var i + else Mc.PEmul (c,var i) in + let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else + Mc.PEadd (mn, p) in + xtopoly p' (i+1) l in + + xtopoly (Mc.PEc Mc.Z0) 0 l let rec fixpoint f x = let y' = f x in - if Pervasives.(=) y' x then y' - else fixpoint f y' + if Pervasives.(=) y' x then y' + else fixpoint f y' let rec_simpl_cone n_spec e = let simpl_cone = Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in let rec rec_simpl_cone = function - | Mc.PsatzMulE(t1, t2) -> - simpl_cone (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2)) - | Mc.PsatzAdd(t1,t2) -> - simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2)) - | x -> simpl_cone x in - rec_simpl_cone e - - + | Mc.PsatzMulE(t1, t2) -> + simpl_cone (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2)) + | Mc.PsatzAdd(t1,t2) -> + simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2)) + | x -> simpl_cone x in + rec_simpl_cone e + + let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c type cone_prod = - Const of cone - | Ideal of cone *cone - | Mult of cone * cone - | Other of cone + Const of cone +| Ideal of cone *cone +| Mult of cone * cone +| Other of cone and cone = Mc.zWitness @@ -147,32 +147,32 @@ let factorise_linear_cone c = let rec cone_list c l = match c with - | Mc.PsatzAdd (x,r) -> cone_list r (x::l) - | _ -> c :: l in - + | Mc.PsatzAdd (x,r) -> cone_list r (x::l) + | _ -> c :: l in + let factorise c1 c2 = match c1 , c2 with - | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> - if Pervasives.(=) x x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None - | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> - if Pervasives.(=) x x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None - | _ -> None in - + | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> + if Pervasives.(=) x x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None + | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> + if Pervasives.(=) x x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None + | _ -> None in + let rec rebuild_cone l pending = match l with - | [] -> (match pending with - | None -> Mc.PsatzZ - | Some p -> p - ) - | e::l -> - (match pending with - | None -> rebuild_cone l (Some e) - | Some p -> (match factorise p e with - | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e)) - | Some f -> rebuild_cone l (Some f) ) - ) in + | [] -> (match pending with + | None -> Mc.PsatzZ + | Some p -> p + ) + | e::l -> + (match pending with + | None -> rebuild_cone l (Some e) + | Some p -> (match factorise p e with + | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e)) + | Some f -> rebuild_cone l (Some f) ) + ) in - (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None) + (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None) @@ -199,28 +199,28 @@ open Mfourier let constrain_monomial mn l = let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in - if Pervasives.(=) mn Monomial.const - then - { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; - op = Eq ; - cst = Big_int zero_big_int } - else - { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; - op = Eq ; - cst = Big_int zero_big_int } + if Pervasives.(=) mn Monomial.const + then + { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; + op = Eq ; + cst = Big_int zero_big_int } + else + { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; + op = Eq ; + cst = Big_int zero_big_int } - + let positivity l = let rec xpositivity i l = match l with - | [] -> [] - | (_,Mc.Equal)::l -> xpositivity (i+1) l - | (_,_)::l -> - {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; - op = Ge ; - cst = Int 0 } :: (xpositivity (i+1) l) + | [] -> [] + | (_,Mc.Equal)::l -> xpositivity (i+1) l + | (_,_)::l -> + {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; + op = Ge ; + cst = Int 0 } :: (xpositivity (i+1) l) in - xpositivity 0 l + xpositivity 0 l let string_of_op = function @@ -241,23 +241,23 @@ let build_linear_system l = let monomials = List.fold_left (fun acc p -> - Poly.fold (fun m _ acc -> MonSet.add m acc) p acc) - (MonSet.singleton Monomial.const) l' + Poly.fold (fun m _ acc -> MonSet.add m acc) p acc) + (MonSet.singleton Monomial.const) l' in (* For each monomial, compute a constraint *) let s0 = MonSet.fold (fun mn res -> (constrain_monomial mn l')::res) monomials [] in - (* I need at least something strictly positive *) + (* I need at least something strictly positive *) let strict = { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.map (fun (x,y) -> - match y with Mc.Strict -> - Big_int unit_big_int - | _ -> Big_int zero_big_int) l)); + match y with Mc.Strict -> + Big_int unit_big_int + | _ -> Big_int zero_big_int) l)); op = Ge ; cst = Big_int unit_big_int } in (* Add the positivity constraint *) - {coeffs = Vect.from_list ([Big_int unit_big_int]) ; - op = Ge ; - cst = Big_int zero_big_int}::(strict::(positivity l)@s0) + {coeffs = Vect.from_list ([Big_int unit_big_int]) ; + op = Ge ; + cst = Big_int zero_big_int}::(strict::(positivity l)@s0) let big_int_to_z = Ml2C.bigint @@ -266,32 +266,32 @@ let big_int_to_z = Ml2C.bigint -- at a lower layer, certificates are using nums... *) let make_certificate n_spec (cert,li) = let bint_to_cst = n_spec.bigint_to_number in - match cert with - | [] -> failwith "empty_certificate" - | e::cert' -> -(* let cst = match compare_big_int e zero_big_int with - | 0 -> Mc.PsatzZ - | 1 -> Mc.PsatzC (bint_to_cst e) - | _ -> failwith "positivity error" - in *) - let rec scalar_product cert l = - match cert with - | [] -> Mc.PsatzZ - | c::cert -> - match l with - | [] -> failwith "make_certificate(1)" - | i::l -> - let r = scalar_product cert l in - match compare_big_int c zero_big_int with - | -1 -> Mc.PsatzAdd ( - Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), - r) - | 0 -> r - | _ -> Mc.PsatzAdd ( - Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), - r) in - (factorise_linear_cone - (simplify_cone n_spec (scalar_product cert' li))) + match cert with + | [] -> failwith "empty_certificate" + | e::cert' -> + (* let cst = match compare_big_int e zero_big_int with + | 0 -> Mc.PsatzZ + | 1 -> Mc.PsatzC (bint_to_cst e) + | _ -> failwith "positivity error" + in *) + let rec scalar_product cert l = + match cert with + | [] -> Mc.PsatzZ + | c::cert -> + match l with + | [] -> failwith "make_certificate(1)" + | i::l -> + let r = scalar_product cert l in + match compare_big_int c zero_big_int with + | -1 -> Mc.PsatzAdd ( + Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), + r) + | 0 -> r + | _ -> Mc.PsatzAdd ( + Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), + r) in + (factorise_linear_cone + (simplify_cone n_spec (scalar_product cert' li))) exception Found of Monomial.t @@ -301,91 +301,157 @@ exception Strict module MonMap = Map.Make(Monomial) let primal l = - let vr = ref 0 in - - let vect_of_poly map p = - Poly.fold (fun mn vl (map,vect) -> - if Pervasives.(=) mn Monomial.const - then (map,vect) - else - let (mn,m) = try (MonMap.find mn map,map) with Not_found -> let res = (!vr, MonMap.add mn !vr map) in incr vr ; res in - (m,if Int.equal (sign_num vl) 0 then vect else (mn,vl)::vect)) p (map,[]) in - - let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in + let vr = ref 0 in + + let vect_of_poly map p = + Poly.fold (fun mn vl (map,vect) -> + if Pervasives.(=) mn Monomial.const + then (map,vect) + else + let (mn,m) = try (MonMap.find mn map,map) with Not_found -> let res = (!vr, MonMap.add mn !vr map) in incr vr ; res in + (m,if Int.equal (sign_num vl) 0 then vect else (mn,vl)::vect)) p (map,[]) in + + let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in - let cmp x y = Int.compare (fst x) (fst y) in + let cmp x y = Int.compare (fst x) (fst y) in - snd (List.fold_right (fun (p,op) (map,l) -> - let (mp,vect) = vect_of_poly map p in - let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in + snd (List.fold_right (fun (p,op) (map,l) -> + let (mp,vect) = vect_of_poly map p in + let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in - (mp,cstr::l)) l (MonMap.empty,[])) + (mp,cstr::l)) l (MonMap.empty,[])) let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = -(* List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *) - + (* List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *) + let sys = build_linear_system l in - try - match Fourier.find_point sys with - | Inr _ -> None - | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) - (* should not use rats_to_ints *) - with x when Errors.noncritical x -> - if debug - then (Printf.printf "raw certificate %s" (Printexc.to_string x); - flush stdout) ; - None + try + match Fourier.find_point sys with + | Inr _ -> None + | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) + (* should not use rats_to_ints *) + with x when Errors.noncritical x -> + if debug + then (Printf.printf "raw certificate %s" (Printexc.to_string x); + flush stdout) ; + None let raw_certificate l = - try - let p = primal l in - match Fourier.find_point p with - | Inr prf -> - if debug then Printf.printf "AProof : %a\n" pp_proof prf ; - let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in - if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; - Some (rats_to_ints (Vect.to_list cert)) - | Inl _ -> None - with Strict -> + try + let p = primal l in + match Fourier.find_point p with + | Inr prf -> + if debug then Printf.printf "AProof : %a\n" pp_proof prf ; + let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in + if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; + Some (rats_to_ints (Vect.to_list cert)) + | Inl _ -> None + with Strict -> (* Fourier elimination should handle > *) - dual_raw_certificate l + dual_raw_certificate l let simple_linear_prover l = let (lc,li) = List.split l in - match raw_certificate lc with - | None -> None (* No certificate *) - | Some cert -> Some (cert,li) - + match raw_certificate lc with + | None -> None (* No certificate *) + | Some cert -> Some (cert,li) + let linear_prover n_spec l = - let build_system n_spec l = - let li = List.combine l (interval 0 (List.length l -1)) in - let (l1,l') = List.partition - (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in - List.map - (fun ((x,y),i) -> match y with - Mc.NonEqual -> failwith "cannot happen" - | y -> ((dev_form n_spec x, y),i)) l' in - let l' = build_system n_spec l in - simple_linear_prover (*n_spec*) l' + let build_system n_spec l = + let li = List.combine l (interval 0 (List.length l -1)) in + let (l1,l') = List.partition + (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in + List.map + (fun ((x,y),i) -> match y with + Mc.NonEqual -> failwith "cannot happen" + | y -> ((dev_form n_spec x, y),i)) l' in + let l' = build_system n_spec l in + simple_linear_prover (*n_spec*) l' let linear_prover n_spec l = try linear_prover n_spec l with x when Errors.noncritical x -> - (print_string (Printexc.to_string x); None) + (print_string (Printexc.to_string x); None) + +let compute_max_nb_cstr l d = + let len = List.length l in + max len (max d (len * d)) + +let linear_prover_with_cert prfdepth spec l = + max_nb_cstr := compute_max_nb_cstr l prfdepth ; + match linear_prover spec l with + | None -> None + | Some cert -> Some (make_certificate spec cert) + +let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) = + LinPoly.MonT.clear (); + max_nb_cstr := compute_max_nb_cstr sys prfdepth ; + (* Assign a proof to the initial hypotheses *) + let sys = mapi (fun c i -> (c,Mc.PsatzIn (Ml2C.nat i))) sys in + + + (* Add all the product of hypotheses *) + let prod = all_pairs (fun ((c,o),p) ((c',o'),p') -> + ((Mc.PEmul(c,c') , Mc.opMult o o') , Mc.PsatzMulE(p,p'))) sys in + + (* Only filter those have a meaning *) + let prod = List.fold_left (fun l ((c,o),p) -> + match o with + | None -> l + | Some o -> ((c,o),p) :: l) [] prod in + + let sys = sys @ prod in + + let square = + (* Collect the squares and state that they are positive *) + let pols = List.map (fun ((p,_),_) -> dev_form q_spec p) sys in + let square = + List.fold_left (fun acc p -> + Poly.fold + (fun m _ acc -> + match Monomial.sqrt m with + | None -> acc + | Some s -> MonMap.add s m acc) p acc) MonMap.empty pols in + + let pol_of_mon m = + Monomial.fold (fun x v p -> Mc.PEmul(Mc.PEpow(Mc.PEX(Ml2C.positive x),Ml2C.n v),p)) m (Mc.PEc q_spec.unit) in + + let norm0 = + Mc.norm q_spec.zero q_spec.unit Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool in + + + MonMap.fold (fun s m acc -> ((pol_of_mon m , Mc.NonStrict), Mc.PsatzSquare(norm0 (pol_of_mon s)))::acc) square [] in + + Printf.printf "#square %i\n" (List.length square) ; + flush stdout ; + + let sys = sys @ square in -let linear_prover_with_cert spec l = - match linear_prover spec l with - | None -> None - | Some cert -> Some (make_certificate spec cert) + (* Call the linear prover without the proofs *) + let sys_no_prf = List.map fst sys in + + match linear_prover q_spec sys_no_prf with + | None -> None + | Some cert -> + let cert = make_certificate q_spec cert in + let rec map_psatz = function + | Mc.PsatzIn n -> snd (List.nth sys (C2Ml.nat n)) + | Mc.PsatzSquare c -> Mc.PsatzSquare c + | Mc.PsatzMulC(c,p) -> Mc.PsatzMulC(c, map_psatz p) + | Mc.PsatzMulE(p1,p2) -> Mc.PsatzMulE(map_psatz p1,map_psatz p2) + | Mc.PsatzAdd(p1,p2) -> Mc.PsatzAdd(map_psatz p1,map_psatz p2) + | Mc.PsatzC c -> Mc.PsatzC c + | Mc.PsatzZ -> Mc.PsatzZ in + Some (map_psatz cert) @@ -395,11 +461,11 @@ let make_linear_system l = (Poly.constant (Int 0)) l' in let monomials = Poly.fold (fun mn _ l -> if Pervasives.(=) mn Monomial.const then l else mn::l) monomials [] in - (List.map (fun (c,op) -> - {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; - op = op ; - cst = minus_num ( (Poly.get Monomial.const c))}) l - ,monomials) + (List.map (fun (c,op) -> + {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; + op = op ; + cst = minus_num ( (Poly.get Monomial.const c))}) l + ,monomials) let pplus x y = Mc.PEadd(x,y) @@ -413,7 +479,7 @@ let rec mem p x l = let rec remove_assoc p x l = match l with [] -> [] | e::l -> if p x (fst e) then - remove_assoc p x l else e::(remove_assoc p x l) + remove_assoc p x l else e::(remove_assoc p x l) let eq x y = Int.equal (Vect.compare x y) 0 @@ -424,39 +490,39 @@ let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l only searching for naive cutting planes *) let develop_constraint z_spec (e,k) = - match k with - | Mc.NonStrict -> (dev_form z_spec e , Ge) - | Mc.Equal -> (dev_form z_spec e , Eq) - | _ -> assert false + match k with + | Mc.NonStrict -> (dev_form z_spec e , Ge) + | Mc.Equal -> (dev_form z_spec e , Eq) + | _ -> assert false let op_of_op_compat = function - | Ge -> Mc.NonStrict - | Eq -> Mc.Equal + | Ge -> Mc.NonStrict + | Eq -> Mc.Equal let integer_vector coeffs = - let vars , coeffs = List.split coeffs in - List.combine vars (List.map (fun x -> Big_int x) (rats_to_ints coeffs)) + let vars , coeffs = List.split coeffs in + List.combine vars (List.map (fun x -> Big_int x) (rats_to_ints coeffs)) let integer_cstr {coeffs = coeffs ; op = op ; cst = cst } = - let vars , coeffs = List.split coeffs in - match rats_to_ints (cst::coeffs) with - | cst :: coeffs -> - { - coeffs = List.combine vars (List.map (fun x -> Big_int x) coeffs) ; - op = op ; cst = Big_int cst} - | _ -> assert false - + let vars , coeffs = List.split coeffs in + match rats_to_ints (cst::coeffs) with + | cst :: coeffs -> + { + coeffs = List.combine vars (List.map (fun x -> Big_int x) coeffs) ; + op = op ; cst = Big_int cst} + | _ -> assert false + let pexpr_of_cstr_compat var cstr = - let {coeffs = coeffs ; op = op ; cst = cst } = integer_cstr cstr in - try - let expr = list_to_polynomial var (Vect.to_list coeffs) in - let d = Ml2C.bigint (denominator cst) in - let n = Ml2C.bigint (numerator cst) in - (pplus (pmult (pconst d) expr) (popp (pconst n)), op_of_op_compat op) - with Failure _ -> failwith "pexpr_of_cstr_compat" + let {coeffs = coeffs ; op = op ; cst = cst } = integer_cstr cstr in + try + let expr = list_to_polynomial var (Vect.to_list coeffs) in + let d = Ml2C.bigint (denominator cst) in + let n = Ml2C.bigint (numerator cst) in + (pplus (pmult (pconst d) expr) (popp (pconst n)), op_of_op_compat op) + with Failure _ -> failwith "pexpr_of_cstr_compat" @@ -465,41 +531,41 @@ open Sos_types let rec scale_term t = match t with - | Zero -> unit_big_int , Zero - | Const n -> (denominator n) , Const (Big_int (numerator n)) - | Var n -> unit_big_int , Var n - | Inv _ -> failwith "scale_term : not implemented" - | Opp t -> let s, t = scale_term t in s, Opp t - | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - let e = mult_big_int g (mult_big_int s1' s2') in - if Int.equal (compare_big_int e unit_big_int) 0 - then (unit_big_int, Add (y1,y2)) - else e, Add (Mul(Const (Big_int s2'), y1), - Mul (Const (Big_int s1'), y2)) - | Sub _ -> failwith "scale term: not implemented" - | Mul(y,z) -> let s1,y1 = scale_term y and s2,y2 = scale_term z in - mult_big_int s1 s2 , Mul (y1, y2) - | Pow(t,n) -> let s,t = scale_term t in - power_big_int_positive_int s n , Pow(t,n) - | _ -> failwith "scale_term : not implemented" + | Zero -> unit_big_int , Zero + | Const n -> (denominator n) , Const (Big_int (numerator n)) + | Var n -> unit_big_int , Var n + | Inv _ -> failwith "scale_term : not implemented" + | Opp t -> let s, t = scale_term t in s, Opp t + | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in + let g = gcd_big_int s1 s2 in + let s1' = div_big_int s1 g in + let s2' = div_big_int s2 g in + let e = mult_big_int g (mult_big_int s1' s2') in + if Int.equal (compare_big_int e unit_big_int) 0 + then (unit_big_int, Add (y1,y2)) + else e, Add (Mul(Const (Big_int s2'), y1), + Mul (Const (Big_int s1'), y2)) + | Sub _ -> failwith "scale term: not implemented" + | Mul(y,z) -> let s1,y1 = scale_term y and s2,y2 = scale_term z in + mult_big_int s1 s2 , Mul (y1, y2) + | Pow(t,n) -> let s,t = scale_term t in + power_big_int_positive_int s n , Pow(t,n) + | _ -> failwith "scale_term : not implemented" let scale_term t = let (s,t') = scale_term t in - s,t' + s,t' let get_index_of_ith_match f i l = let rec get j res l = match l with - | [] -> failwith "bad index" - | e::l -> if f e - then - (if Int.equal j i then res else get (j+1) (res+1) l ) - else get j (res+1) l in - get 0 0 l + | [] -> failwith "bad index" + | e::l -> if f e + then + (if Int.equal j i then res else get (j+1) (res+1) l ) + else get j (res+1) l in + get 0 0 l let rec scale_certificate pos = match pos with @@ -511,97 +577,97 @@ let rec scale_certificate pos = match pos with | Rational_le n -> (denominator n) , Rational_le (Big_int (numerator n)) | Rational_lt n -> (denominator n) , Rational_lt (Big_int (numerator n)) | Square t -> let s,t' = scale_term t in - mult_big_int s s , Square t' + mult_big_int s s , Square t' | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in - mult_big_int s1 s2 , Eqmul (y1,y2) + mult_big_int s1 s2 , Eqmul (y1,y2) | Sum (y, z) -> let s1,y1 = scale_certificate y - and s2,y2 = scale_certificate z in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - mult_big_int g (mult_big_int s1' s2'), - Sum (Product(Rational_le (Big_int s2'), y1), - Product (Rational_le (Big_int s1'), y2)) + and s2,y2 = scale_certificate z in + let g = gcd_big_int s1 s2 in + let s1' = div_big_int s1 g in + let s2' = div_big_int s2 g in + mult_big_int g (mult_big_int s1' s2'), + Sum (Product(Rational_le (Big_int s2'), y1), + Product (Rational_le (Big_int s1'), y2)) | Product (y, z) -> - let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in - mult_big_int s1 s2 , Product (y1,y2) + let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in + mult_big_int s1 s2 , Product (y1,y2) open Micromega - let rec term_to_q_expr = function - | Const n -> PEc (Ml2C.q n) - | Zero -> PEc ( Ml2C.q (Int 0)) - | Var s -> PEX (Ml2C.index - (int_of_string (String.sub s 1 (String.length s - 1)))) - | Mul(p1,p2) -> PEmul(term_to_q_expr p1, term_to_q_expr p2) - | Add(p1,p2) -> PEadd(term_to_q_expr p1, term_to_q_expr p2) - | Opp p -> PEopp (term_to_q_expr p) - | Pow(t,n) -> PEpow (term_to_q_expr t,Ml2C.n n) - | Sub(t1,t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2) - | _ -> failwith "term_to_q_expr: not implemented" - - let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e) - - - let rec product l = - match l with - | [] -> Mc.PsatzZ - | [i] -> Mc.PsatzIn (Ml2C.nat i) - | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l) +let rec term_to_q_expr = function + | Const n -> PEc (Ml2C.q n) + | Zero -> PEc ( Ml2C.q (Int 0)) + | Var s -> PEX (Ml2C.index + (int_of_string (String.sub s 1 (String.length s - 1)))) + | Mul(p1,p2) -> PEmul(term_to_q_expr p1, term_to_q_expr p2) + | Add(p1,p2) -> PEadd(term_to_q_expr p1, term_to_q_expr p2) + | Opp p -> PEopp (term_to_q_expr p) + | Pow(t,n) -> PEpow (term_to_q_expr t,Ml2C.n n) + | Sub(t1,t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2) + | _ -> failwith "term_to_q_expr: not implemented" + +let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e) + + +let rec product l = + match l with + | [] -> Mc.PsatzZ + | [i] -> Mc.PsatzIn (Ml2C.nat i) + | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l) let q_cert_of_pos pos = let rec _cert_of_pos = function - Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) + Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else - Mc.PsatzC (Ml2C.q n) + if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else + Mc.PsatzC (Ml2C.q n) | Square t -> Mc.PsatzSquare (term_to_q_pol t) | Eqmul (t, y) -> Mc.PsatzMulC(term_to_q_pol t, _cert_of_pos y) | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z) | Product (y, z) -> Mc.PsatzMulE (_cert_of_pos y, _cert_of_pos z) in - simplify_cone q_spec (_cert_of_pos pos) + simplify_cone q_spec (_cert_of_pos pos) - let rec term_to_z_expr = function - | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) - | Zero -> PEc ( Z0) - | Var s -> PEX (Ml2C.index - (int_of_string (String.sub s 1 (String.length s - 1)))) - | Mul(p1,p2) -> PEmul(term_to_z_expr p1, term_to_z_expr p2) - | Add(p1,p2) -> PEadd(term_to_z_expr p1, term_to_z_expr p2) - | Opp p -> PEopp (term_to_z_expr p) - | Pow(t,n) -> PEpow (term_to_z_expr t,Ml2C.n n) - | Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2) - | _ -> failwith "term_to_z_expr: not implemented" +let rec term_to_z_expr = function + | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) + | Zero -> PEc ( Z0) + | Var s -> PEX (Ml2C.index + (int_of_string (String.sub s 1 (String.length s - 1)))) + | Mul(p1,p2) -> PEmul(term_to_z_expr p1, term_to_z_expr p2) + | Add(p1,p2) -> PEadd(term_to_z_expr p1, term_to_z_expr p2) + | Opp p -> PEopp (term_to_z_expr p) + | Pow(t,n) -> PEpow (term_to_z_expr t,Ml2C.n n) + | Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2) + | _ -> failwith "term_to_z_expr: not implemented" - let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e) +let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e) let z_cert_of_pos pos = let s,pos = (scale_certificate pos) in let rec _cert_of_pos = function - Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) + Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else - Mc.PsatzC (Ml2C.bigint (big_int_of_num n)) + if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else + Mc.PsatzC (Ml2C.bigint (big_int_of_num n)) | Square t -> Mc.PsatzSquare (term_to_z_pol t) | Eqmul (t, y) -> - let is_unit = - match t with - | Const n -> n =/ Int 1 - | _ -> false in - if is_unit - then _cert_of_pos y - else Mc.PsatzMulC(term_to_z_pol t, _cert_of_pos y) + let is_unit = + match t with + | Const n -> n =/ Int 1 + | _ -> false in + if is_unit + then _cert_of_pos y + else Mc.PsatzMulC(term_to_z_pol t, _cert_of_pos y) | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z) | Product (y, z) -> Mc.PsatzMulE (_cert_of_pos y, _cert_of_pos z) in - simplify_cone z_spec (_cert_of_pos pos) + simplify_cone z_spec (_cert_of_pos pos) (** All constraints (initial or derived) have an index and have a justification i.e., proof. Given a constraint, all the coefficients are always integers. @@ -612,116 +678,109 @@ open Num open Big_int open Polynomial -(*module Mc = Micromega*) -(*module Ml2C = Mutils.CamlToCoq -module C2Ml = Mutils.CoqToCaml -*) -let debug = false - - module Env = struct - type t = int list + type t = int list - let id_of_hyp hyp l = - let rec xid_of_hyp i l = - match l with - | [] -> failwith "id_of_hyp" - | hyp'::l -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l in - xid_of_hyp 0 l + let id_of_hyp hyp l = + let rec xid_of_hyp i l = + match l with + | [] -> failwith "id_of_hyp" + | hyp'::l -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l in + xid_of_hyp 0 l end let coq_poly_of_linpol (p,c) = - let pol_of_mon m = - Monomial.fold (fun x v p -> Mc.PEmul(Mc.PEpow(Mc.PEX(Ml2C.positive x),Ml2C.n v),p)) m (Mc.PEc (Mc.Zpos Mc.XH)) in + let pol_of_mon m = + Monomial.fold (fun x v p -> Mc.PEmul(Mc.PEpow(Mc.PEX(Ml2C.positive x),Ml2C.n v),p)) m (Mc.PEc (Mc.Zpos Mc.XH)) in - List.fold_left (fun acc (x,v) -> - let mn = LinPoly.MonT.retrieve x in - Mc.PEadd(Mc.PEmul(Mc.PEc (Ml2C.bigint (numerator v)), pol_of_mon mn),acc)) (Mc.PEc (Ml2C.bigint (numerator c))) p - + List.fold_left (fun acc (x,v) -> + let mn = LinPoly.MonT.retrieve x in + Mc.PEadd(Mc.PEmul(Mc.PEc (Ml2C.bigint (numerator v)), pol_of_mon mn),acc)) (Mc.PEc (Ml2C.bigint (numerator c))) p + let rec cmpl_prf_rule env = function - | Hyp i | Def i -> Mc.PsatzIn (Ml2C.nat (Env.id_of_hyp i env)) - | Cst i -> Mc.PsatzC (Ml2C.bigint i) - | Zero -> Mc.PsatzZ - | MulPrf(p1,p2) -> Mc.PsatzMulE(cmpl_prf_rule env p1, cmpl_prf_rule env p2) - | AddPrf(p1,p2) -> Mc.PsatzAdd(cmpl_prf_rule env p1 , cmpl_prf_rule env p2) - | MulC(lp,p) -> let lp = Mc.norm0 (coq_poly_of_linpol lp) in - Mc.PsatzMulC(lp,cmpl_prf_rule env p) - | Square lp -> Mc.PsatzSquare (Mc.norm0 (coq_poly_of_linpol lp)) - | _ -> failwith "Cuts should already be compiled" - + | Hyp i | Def i -> Mc.PsatzIn (Ml2C.nat (Env.id_of_hyp i env)) + | Cst i -> Mc.PsatzC (Ml2C.bigint i) + | Zero -> Mc.PsatzZ + | MulPrf(p1,p2) -> Mc.PsatzMulE(cmpl_prf_rule env p1, cmpl_prf_rule env p2) + | AddPrf(p1,p2) -> Mc.PsatzAdd(cmpl_prf_rule env p1 , cmpl_prf_rule env p2) + | MulC(lp,p) -> let lp = Mc.norm0 (coq_poly_of_linpol lp) in + Mc.PsatzMulC(lp,cmpl_prf_rule env p) + | Square lp -> Mc.PsatzSquare (Mc.norm0 (coq_poly_of_linpol lp)) + | _ -> failwith "Cuts should already be compiled" + let rec cmpl_proof env = function - | Done -> Mc.DoneProof - | Step(i,p,prf) -> - begin - match p with - | CutPrf p' -> - Mc.CutProof(cmpl_prf_rule env p', cmpl_proof (i::env) prf) - | _ -> Mc.RatProof(cmpl_prf_rule env p,cmpl_proof (i::env) prf) - end - | Enum(i,p1,_,p2,l) -> - Mc.EnumProof(cmpl_prf_rule env p1,cmpl_prf_rule env p2,List.map (cmpl_proof (i::env)) l) + | Done -> Mc.DoneProof + | Step(i,p,prf) -> + begin + match p with + | CutPrf p' -> + Mc.CutProof(cmpl_prf_rule env p', cmpl_proof (i::env) prf) + | _ -> Mc.RatProof(cmpl_prf_rule env p,cmpl_proof (i::env) prf) + end + | Enum(i,p1,_,p2,l) -> + Mc.EnumProof(cmpl_prf_rule env p1,cmpl_prf_rule env p2,List.map (cmpl_proof (i::env)) l) let compile_proof env prf = - let id = 1 + proof_max_id prf in - let _,prf = normalise_proof id prf in - if debug then Printf.fprintf stdout "compiled proof %a\n" output_proof prf; - cmpl_proof env prf + let id = 1 + proof_max_id prf in + let _,prf = normalise_proof id prf in + if debug then Printf.fprintf stdout "compiled proof %a\n" output_proof prf; + cmpl_proof env prf type prf_sys = (cstr_compat * prf_rule) list let xlinear_prover sys = - match Fourier.find_point sys with - | Inr prf -> - if debug then Printf.printf "AProof : %a\n" pp_proof prf ; - let cert = (*List.map (fun (x,n) -> x+1,n)*) (fst (List.hd (Proof.mk_proof sys prf))) in - if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; - Some (rats_to_ints (Vect.to_list cert)) - | Inl _ -> None + match Fourier.find_point sys with + | Inr prf -> + if debug then Printf.printf "AProof : %a\n" pp_proof prf ; + let cert = (*List.map (fun (x,n) -> x+1,n)*) (fst (List.hd (Proof.mk_proof sys prf))) in + if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; + Some (rats_to_ints (Vect.to_list cert)) + | Inl _ -> None let output_num o n = output_string o (string_of_num n) let output_bigint o n = output_string o (string_of_big_int n) let proof_of_farkas prf cert = -(* Printf.printf "\nproof_of_farkas %a , %a \n" (pp_list output_prf_rule) prf (pp_list output_bigint) cert ; *) - let rec mk_farkas acc prf cert = - match prf, cert with - | _ , [] -> acc - | [] , _ -> failwith "proof_of_farkas : not enough hyps" - | p::prf,c::cert -> - mk_farkas (add_proof (mul_proof c p) acc) prf cert in - let res = mk_farkas Zero prf cert in + (* Printf.printf "\nproof_of_farkas %a , %a \n" (pp_list output_prf_rule) prf (pp_list output_bigint) cert ; *) + let rec mk_farkas acc prf cert = + match prf, cert with + | _ , [] -> acc + | [] , _ -> failwith "proof_of_farkas : not enough hyps" + | p::prf,c::cert -> + mk_farkas (add_proof (mul_proof c p) acc) prf cert in + let res = mk_farkas Zero prf cert in (*Printf.printf "==> %a" output_prf_rule res ; *) - res + res let linear_prover sys = - let (sysi,prfi) = List.split sys in - match xlinear_prover sysi with - | None -> None - | Some cert -> Some (proof_of_farkas prfi cert) + let (sysi,prfi) = List.split sys in + match xlinear_prover sysi with + | None -> None + | Some cert -> Some (proof_of_farkas prfi cert) let linear_prover = - if debug - then - fun sys -> - Printf.printf "<linear_prover"; flush stdout ; - let res = linear_prover sys in - Printf.printf ">"; flush stdout ; - res - else linear_prover + if debug + then + fun sys -> + Printf.printf "<linear_prover"; flush stdout ; + let res = linear_prover sys in + Printf.printf ">"; flush stdout ; + res + else linear_prover @@ -733,11 +792,11 @@ let linear_prover = *) type checksat = - | Tauto (* Tautology *) - | Unsat of prf_rule (* Unsatisfiable *) - | Cut of cstr_compat * prf_rule (* Cutting plane *) - | Normalise of cstr_compat * prf_rule (* coefficients are relatively prime *) - +| Tauto (* Tautology *) +| Unsat of prf_rule (* Unsatisfiable *) +| Cut of cstr_compat * prf_rule (* Cutting plane *) +| Normalise of cstr_compat * prf_rule (* coefficients are relatively prime *) + (** [check_sat] - detects constraints that are not satisfiable; @@ -745,83 +804,83 @@ type checksat = *) let check_sat (cstr,prf) = - let {coeffs=coeffs ; op=op ; cst=cst} = cstr in - match coeffs with - | [] -> - if eval_op op (Int 0) cst then Tauto else Unsat prf - | _ -> - let gcdi = (gcd_list (List.map snd coeffs)) in - let gcd = Big_int gcdi in - if eq_num gcd (Int 1) - then Normalise(cstr,prf) - else - if Int.equal (sign_num (mod_num cst gcd)) 0 - then (* We can really normalise *) - begin - assert (sign_num gcd >=1 ) ; - let cstr = { - coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; - op = op ; cst = cst // gcd - } in - Normalise(cstr,Gcd(gcdi,prf)) - (* Normalise(cstr,CutPrf prf)*) - end - else - match op with - | Eq -> Unsat (CutPrf prf) - | Ge -> - let cstr = { - coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; - op = op ; cst = ceiling_num (cst // gcd) - } in Cut(cstr,CutPrf prf) + let {coeffs=coeffs ; op=op ; cst=cst} = cstr in + match coeffs with + | [] -> + if eval_op op (Int 0) cst then Tauto else Unsat prf + | _ -> + let gcdi = (gcd_list (List.map snd coeffs)) in + let gcd = Big_int gcdi in + if eq_num gcd (Int 1) + then Normalise(cstr,prf) + else + if Int.equal (sign_num (mod_num cst gcd)) 0 + then (* We can really normalise *) + begin + assert (sign_num gcd >=1 ) ; + let cstr = { + coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; + op = op ; cst = cst // gcd + } in + Normalise(cstr,Gcd(gcdi,prf)) + (* Normalise(cstr,CutPrf prf)*) + end + else + match op with + | Eq -> Unsat (CutPrf prf) + | Ge -> + let cstr = { + coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; + op = op ; cst = ceiling_num (cst // gcd) + } in Cut(cstr,CutPrf prf) (** Proof generating pivoting over variable v *) let pivot v (c1,p1) (c2,p2) = - let {coeffs = v1 ; op = op1 ; cst = n1} = c1 - and {coeffs = v2 ; op = op2 ; cst = n2} = c2 in + let {coeffs = v1 ; op = op1 ; cst = n1} = c1 + and {coeffs = v2 ; op = op2 ; cst = n2} = c2 in (* Could factorise gcd... *) - let xpivot cv1 cv2 = - ( - {coeffs = Vect.add (Vect.mul cv1 v1) (Vect.mul cv2 v2) ; - op = Proof.add_op op1 op2 ; - cst = n1 */ cv1 +/ n2 */ cv2 }, + let xpivot cv1 cv2 = + ( + {coeffs = Vect.add (Vect.mul cv1 v1) (Vect.mul cv2 v2) ; + op = Proof.add_op op1 op2 ; + cst = n1 */ cv1 +/ n2 */ cv2 }, - AddPrf(mul_proof (numerator cv1) p1,mul_proof (numerator cv2) p2)) in + AddPrf(mul_proof (numerator cv1) p1,mul_proof (numerator cv2) p2)) in + + match Vect.get v v1 , Vect.get v v2 with + | None , _ | _ , None -> None + | Some a , Some b -> + if Int.equal ((sign_num a) * (sign_num b)) (-1) + then + let cv1 = abs_num b + and cv2 = abs_num a in + Some (xpivot cv1 cv2) + else + if op1 == Eq + then + let cv1 = minus_num (b */ (Int (sign_num a))) + and cv2 = abs_num a in + Some (xpivot cv1 cv2) + else if op2 == Eq + then + let cv1 = abs_num b + and cv2 = minus_num (a */ (Int (sign_num b))) in + Some (xpivot cv1 cv2) + else None (* op2 could be Eq ... this might happen *) - match Vect.get v v1 , Vect.get v v2 with - | None , _ | _ , None -> None - | Some a , Some b -> - if Int.equal ((sign_num a) * (sign_num b)) (-1) - then - let cv1 = abs_num b - and cv2 = abs_num a in - Some (xpivot cv1 cv2) - else - if op1 == Eq - then - let cv1 = minus_num (b */ (Int (sign_num a))) - and cv2 = abs_num a in - Some (xpivot cv1 cv2) - else if op2 == Eq - then - let cv1 = abs_num b - and cv2 = minus_num (a */ (Int (sign_num b))) in - Some (xpivot cv1 cv2) - else None (* op2 could be Eq ... this might happen *) - exception FoundProof of prf_rule let simpl_sys sys = - List.fold_left (fun acc (c,p) -> - match check_sat (c,p) with - | Tauto -> acc - | Unsat prf -> raise (FoundProof prf) - | Cut(c,p) -> (c,p)::acc - | Normalise (c,p) -> (c,p)::acc) [] sys + List.fold_left (fun acc (c,p) -> + match check_sat (c,p) with + | Tauto -> acc + | Unsat prf -> raise (FoundProof prf) + | Cut(c,p) -> (c,p)::acc + | Normalise (c,p) -> (c,p)::acc) [] sys (** [ext_gcd a b] is the extended Euclid algorithm. @@ -829,77 +888,77 @@ let simpl_sys sys = Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm *) let rec ext_gcd a b = - if Int.equal (sign_big_int b) 0 - then (unit_big_int,zero_big_int) - else - let (q,r) = quomod_big_int a b in - let (s,t) = ext_gcd b r in - (t, sub_big_int s (mult_big_int q t)) + if Int.equal (sign_big_int b) 0 + then (unit_big_int,zero_big_int) + else + let (q,r) = quomod_big_int a b in + let (s,t) = ext_gcd b r in + (t, sub_big_int s (mult_big_int q t)) let pp_ext_gcd a b = - let a' = big_int_of_int a in - let b' = big_int_of_int b in - - let (x,y) = ext_gcd a' b' in - Printf.fprintf stdout "%s * %s + %s * %s = %s\n" - (string_of_big_int x) (string_of_big_int a') - (string_of_big_int y) (string_of_big_int b') - (string_of_big_int (add_big_int (mult_big_int x a') (mult_big_int y b'))) + let a' = big_int_of_int a in + let b' = big_int_of_int b in + + let (x,y) = ext_gcd a' b' in + Printf.fprintf stdout "%s * %s + %s * %s = %s\n" + (string_of_big_int x) (string_of_big_int a') + (string_of_big_int y) (string_of_big_int b') + (string_of_big_int (add_big_int (mult_big_int x a') (mult_big_int y b'))) exception Result of (int * (proof * cstr_compat)) let split_equations psys = - List.partition (fun (c,p) -> c.op == Eq) + List.partition (fun (c,p) -> c.op == Eq) let extract_coprime (c1,p1) (c2,p2) = - let rec exist2 vect1 vect2 = - match vect1 , vect2 with - | _ , [] | [], _ -> None - | (v1,n1)::vect1' , (v2, n2) :: vect2' -> - if Pervasives.(=) v1 v2 - then - if Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0 - then Some (v1,n1,n2) - else - exist2 vect1' vect2' - else - if v1 < v2 - then exist2 vect1' vect2 - else exist2 vect1 vect2' in - - if c1.op == Eq && c2.op == Eq - then exist2 c1.coeffs c2.coeffs - else None + let rec exist2 vect1 vect2 = + match vect1 , vect2 with + | _ , [] | [], _ -> None + | (v1,n1)::vect1' , (v2, n2) :: vect2' -> + if Pervasives.(=) v1 v2 + then + if Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0 + then Some (v1,n1,n2) + else + exist2 vect1' vect2' + else + if v1 < v2 + then exist2 vect1' vect2 + else exist2 vect1 vect2' in + + if c1.op == Eq && c2.op == Eq + then exist2 c1.coeffs c2.coeffs + else None let extract2 pred l = - let rec xextract2 rl l = - match l with - | [] -> (None,rl) (* Did not find *) - | e::l -> - match extract (pred e) l with - | None,_ -> xextract2 (e::rl) l - | Some (r,e'),l' -> Some (r,e,e'), List.rev_append rl l' in - - xextract2 [] l + let rec xextract2 rl l = + match l with + | [] -> (None,rl) (* Did not find *) + | e::l -> + match extract (pred e) l with + | None,_ -> xextract2 (e::rl) l + | Some (r,e'),l' -> Some (r,e,e'), List.rev_append rl l' in + + xextract2 [] l let extract_coprime_equation psys = - extract2 extract_coprime psys + extract2 extract_coprime psys let apply_and_normalise f psys = - List.fold_left (fun acc pc' -> - match f pc' with - | None -> pc'::acc - | Some pc' -> - match check_sat pc' with - | Tauto -> acc - | Unsat prf -> raise (FoundProof prf) - | Cut(c,p) -> (c,p)::acc - | Normalise (c,p) -> (c,p)::acc - ) [] psys + List.fold_left (fun acc pc' -> + match f pc' with + | None -> pc'::acc + | Some pc' -> + match check_sat pc' with + | Tauto -> acc + | Unsat prf -> raise (FoundProof prf) + | Cut(c,p) -> (c,p)::acc + | Normalise (c,p) -> (c,p)::acc + ) [] psys @@ -908,314 +967,317 @@ let pivot_sys v pc psys = apply_and_normalise (pivot v pc) psys let reduce_coprime psys = - let oeq,sys = extract_coprime_equation psys in - match oeq with - | None -> None (* Nothing to do *) - | Some((v,n1,n2),(c1,p1),(c2,p2) ) -> - let (l1,l2) = ext_gcd (numerator n1) (numerator n2) in - let l1' = Big_int l1 and l2' = Big_int l2 in - let cstr = - {coeffs = Vect.add (Vect.mul l1' c1.coeffs) (Vect.mul l2' c2.coeffs); - op = Eq ; - cst = (l1' */ c1.cst) +/ (l2' */ c2.cst) - } in - let prf = add_proof (mul_proof (numerator l1') p1) (mul_proof (numerator l2') p2) in - - Some (pivot_sys v (cstr,prf) ((c1,p1)::sys)) + let oeq,sys = extract_coprime_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some((v,n1,n2),(c1,p1),(c2,p2) ) -> + let (l1,l2) = ext_gcd (numerator n1) (numerator n2) in + let l1' = Big_int l1 and l2' = Big_int l2 in + let cstr = + {coeffs = Vect.add (Vect.mul l1' c1.coeffs) (Vect.mul l2' c2.coeffs); + op = Eq ; + cst = (l1' */ c1.cst) +/ (l2' */ c2.cst) + } in + let prf = add_proof (mul_proof (numerator l1') p1) (mul_proof (numerator l2') p2) in + + Some (pivot_sys v (cstr,prf) ((c1,p1)::sys)) (** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *) let reduce_unary psys = - let is_unary_equation (cstr,prf) = - if cstr.op == Eq - then - try - Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs)) - with Not_found -> None - else None in - - let (oeq,sys) = extract is_unary_equation psys in - match oeq with - | None -> None (* Nothing to do *) - | Some(v,pc) -> - Some(pivot_sys v pc sys) + let is_unary_equation (cstr,prf) = + if cstr.op == Eq + then + try + Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs)) + with Not_found -> None + else None in + + let (oeq,sys) = extract is_unary_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + Some(pivot_sys v pc sys) let reduce_non_lin_unary psys = - let is_unary_equation (cstr,prf) = - if cstr.op == Eq - then - try - let x = fst (List.find (fun (x,n) -> (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in - let x' = LinPoly.MonT.retrieve x in - if List.for_all (fun (y,_) -> Pervasives.(=) y x || Int.equal (snd (Monomial.div (LinPoly.MonT.retrieve y) x')) 0) cstr.coeffs - then Some x - else None - with Not_found -> None - else None in - - - let (oeq,sys) = extract is_unary_equation psys in - match oeq with - | None -> None (* Nothing to do *) - | Some(v,pc) -> - Some(apply_and_normalise (LinPoly.pivot_eq v pc) sys) + let is_unary_equation (cstr,prf) = + if cstr.op == Eq + then + try + let x = fst (List.find (fun (x,n) -> (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in + let x' = LinPoly.MonT.retrieve x in + if List.for_all (fun (y,_) -> Pervasives.(=) y x || Int.equal (snd (Monomial.div (LinPoly.MonT.retrieve y) x')) 0) cstr.coeffs + then Some x + else None + with Not_found -> None + else None in + + + let (oeq,sys) = extract is_unary_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + Some(apply_and_normalise (LinPoly.pivot_eq v pc) sys) let reduce_var_change psys = - let rec rel_prime vect = - match vect with - | [] -> None - | (x,v)::vect -> - let v = numerator v in - try - let (x',v') = List.find (fun (_,v') -> - let v' = numerator v' in - eq_big_int (gcd_big_int v v') unit_big_int) vect in - Some ((x,v),(x',numerator v')) - with Not_found -> rel_prime vect in - - let rel_prime (cstr,prf) = if cstr.op == Eq then rel_prime cstr.coeffs else None in - - let (oeq,sys) = extract rel_prime psys in - - match oeq with - | None -> None - | Some(((x,v),(x',v')),(c,p)) -> - let (l1,l2) = ext_gcd v v' in - let l1,l2 = Big_int l1 , Big_int l2 in + let rec rel_prime vect = + match vect with + | [] -> None + | (x,v)::vect -> + let v = numerator v in + try + let (x',v') = List.find (fun (_,v') -> + let v' = numerator v' in + eq_big_int (gcd_big_int v v') unit_big_int) vect in + Some ((x,v),(x',numerator v')) + with Not_found -> rel_prime vect in - let get v vect = - match Vect.get v vect with - | None -> Int 0 - | Some n -> n in + let rel_prime (cstr,prf) = if cstr.op == Eq then rel_prime cstr.coeffs else None in - let pivot_eq (c',p') = - let {coeffs = coeffs ; op = op ; cst = cst} = c' in - let vx = get x coeffs in - let vx' = get x' coeffs in - let m = minus_num (vx */ l1 +/ vx' */ l2) in - Some ({coeffs = - Vect.add (Vect.mul m c.coeffs) coeffs ; op = op ; cst = m */ c.cst +/ cst} , - AddPrf(MulC(([], m),p),p')) in + let (oeq,sys) = extract rel_prime psys in + + match oeq with + | None -> None + | Some(((x,v),(x',v')),(c,p)) -> + let (l1,l2) = ext_gcd v v' in + let l1,l2 = Big_int l1 , Big_int l2 in - Some (apply_and_normalise pivot_eq sys) + let get v vect = + match Vect.get v vect with + | None -> Int 0 + | Some n -> n in + let pivot_eq (c',p') = + let {coeffs = coeffs ; op = op ; cst = cst} = c' in + let vx = get x coeffs in + let vx' = get x' coeffs in + let m = minus_num (vx */ l1 +/ vx' */ l2) in + Some ({coeffs = + Vect.add (Vect.mul m c.coeffs) coeffs ; op = op ; cst = m */ c.cst +/ cst} , + AddPrf(MulC(([], m),p),p')) in + Some (apply_and_normalise pivot_eq sys) - let reduce_pivot psys = - let is_equation (cstr,prf) = - if cstr.op == Eq - then - try - Some (fst (List.hd cstr.coeffs)) - with Not_found -> None - else None in - let (oeq,sys) = extract is_equation psys in - match oeq with - | None -> None (* Nothing to do *) - | Some(v,pc) -> - if debug then - Printf.printf "Bad news : loss of completeness %a=%s" Vect.pp_vect (fst pc).coeffs (string_of_num (fst pc).cst); - Some(pivot_sys v pc sys) +let reduce_pivot psys = + let is_equation (cstr,prf) = + if cstr.op == Eq + then + try + Some (fst (List.hd cstr.coeffs)) + with Not_found -> None + else None in + let (oeq,sys) = extract is_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + if debug then + Printf.printf "Bad news : loss of completeness %a=%s" Vect.pp_vect (fst pc).coeffs (string_of_num (fst pc).cst); + Some(pivot_sys v pc sys) - let iterate_until_stable f x = - let rec iter x = - match f x with - | None -> x - | Some x' -> iter x' in - iter x - let rec app_funs l x = - match l with - | [] -> None - | f::fl -> - match f x with - | None -> app_funs fl x - | Some x' -> Some x' - let reduction_equations psys = - iterate_until_stable (app_funs - [reduce_unary ; reduce_coprime ; - reduce_var_change (*; reduce_pivot*)]) psys +let iterate_until_stable f x = + let rec iter x = + match f x with + | None -> x + | Some x' -> iter x' in + iter x - let reduction_non_lin_equations psys = - iterate_until_stable (app_funs - [reduce_non_lin_unary (*; reduce_coprime ; - reduce_var_change ; reduce_pivot *)]) psys +let rec app_funs l x = + match l with + | [] -> None + | f::fl -> + match f x with + | None -> app_funs fl x + | Some x' -> Some x' + +let reduction_equations psys = + iterate_until_stable (app_funs + [reduce_unary ; reduce_coprime ; + reduce_var_change (*; reduce_pivot*)]) psys + +let reduction_non_lin_equations psys = + iterate_until_stable (app_funs + [reduce_non_lin_unary (*; reduce_coprime ; + reduce_var_change ; reduce_pivot *)]) psys (** [get_bound sys] returns upon success an interval (lb,e,ub) with proofs *) - let get_bound sys = - let is_small (v,i) = - match Itv.range i with - | None -> false - | Some i -> i <=/ (Int 1) in - - let select_best (x1,i1) (x2,i2) = - if Itv.smaller_itv i1 i2 - then (x1,i1) else (x2,i2) in +let get_bound sys = + let is_small (v,i) = + match Itv.range i with + | None -> false + | Some i -> i <=/ (Int 1) in + + let select_best (x1,i1) (x2,i2) = + if Itv.smaller_itv i1 i2 + then (x1,i1) else (x2,i2) in (* For lia, there are no equations => these precautions are not needed *) (* For nlia, there are equations => do not enumerate over equations! *) - let all_planes sys = - let (eq,ineq) = List.partition (fun c -> c.op == Eq) sys in - match eq with - | [] -> List.rev_map (fun c -> c.coeffs) ineq - | _ -> - List.fold_left (fun acc c -> - if List.exists (fun c' -> Vect.equal c.coeffs c'.coeffs) eq - then acc else c.coeffs ::acc) [] ineq in - - let smallest_interval = - List.fold_left - (fun acc vect -> - if is_small acc - then acc - else - match Fourier.optimise vect sys with - | None -> acc - | Some i -> - if debug then Printf.printf "Found a new bound %a" Vect.pp_vect vect ; - select_best (vect,i) acc) (Vect.null, (None,None)) (all_planes sys) in - let smallest_interval = - match smallest_interval - with - | (x,(Some i, Some j)) -> Some(i,x,j) - | x -> None (* This should not be possible *) - in - match smallest_interval with - | Some (lb,e,ub) -> - let (lbn,lbd) = (sub_big_int (numerator lb) unit_big_int, denominator lb) in - let (ubn,ubd) = (add_big_int unit_big_int (numerator ub) , denominator ub) in - (match + let all_planes sys = + let (eq,ineq) = List.partition (fun c -> c.op == Eq) sys in + match eq with + | [] -> List.rev_map (fun c -> c.coeffs) ineq + | _ -> + List.fold_left (fun acc c -> + if List.exists (fun c' -> Vect.equal c.coeffs c'.coeffs) eq + then acc else c.coeffs ::acc) [] ineq in + + let smallest_interval = + List.fold_left + (fun acc vect -> + if is_small acc + then acc + else + match Fourier.optimise vect sys with + | None -> acc + | Some i -> + if debug then Printf.printf "Found a new bound %a" Vect.pp_vect vect ; + select_best (vect,i) acc) (Vect.null, (None,None)) (all_planes sys) in + let smallest_interval = + match smallest_interval + with + | (x,(Some i, Some j)) -> Some(i,x,j) + | x -> None (* This should not be possible *) + in + match smallest_interval with + | Some (lb,e,ub) -> + let (lbn,lbd) = (sub_big_int (numerator lb) unit_big_int, denominator lb) in + let (ubn,ubd) = (add_big_int unit_big_int (numerator ub) , denominator ub) in + (match (* x <= ub -> x > ub *) - xlinear_prover ({coeffs = Vect.mul (Big_int ubd) e ; op = Ge ; cst = Big_int ubn} :: sys), + xlinear_prover ({coeffs = Vect.mul (Big_int ubd) e ; op = Ge ; cst = Big_int ubn} :: sys), (* lb <= x -> lb > x *) - xlinear_prover - ({coeffs = Vect.mul (minus_num (Big_int lbd)) e ; op = Ge ; cst = minus_num (Big_int lbn)} :: sys) - with - | Some cub , Some clb -> Some(List.tl clb,(lb,e,ub), List.tl cub) - | _ -> failwith "Interval without proof" - ) - | None -> None - - - let check_sys sys = - List.for_all (fun (c,p) -> List.for_all (fun (_,n) -> sign_num n <> 0) c.coeffs) sys - - - let xlia reduction_equations sys = - - let rec enum_proof (id:int) (sys:prf_sys) : proof option = - if debug then (Printf.printf "enum_proof\n" ; flush stdout) ; - assert (check_sys sys) ; - - let nsys,prf = List.split sys in - match get_bound nsys with - | None -> None (* Is the systeme really unbounded ? *) - | Some(prf1,(lb,e,ub),prf2) -> - if debug then Printf.printf "Found interval: %a in [%s;%s] -> " Vect.pp_vect e (string_of_num lb) (string_of_num ub) ; - (match start_enum id e (ceiling_num lb) (floor_num ub) sys - with - | Some prfl -> - Some(Enum(id,proof_of_farkas prf prf1,e, proof_of_farkas prf prf2,prfl)) - | None -> None - ) - - and start_enum id e clb cub sys = - if clb >/ cub - then Some [] - else - let eq = {coeffs = e ; op = Eq ; cst = clb} in - match aux_lia (id+1) ((eq, Def id) :: sys) with - | None -> None - | Some prf -> - match start_enum id e (clb +/ (Int 1)) cub sys with - | None -> None - | Some l -> Some (prf::l) - - and aux_lia (id:int) (sys:prf_sys) : proof option = - assert (check_sys sys) ; - if debug then Printf.printf "xlia: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; - try - let sys = reduction_equations sys in - if debug then + xlinear_prover + ({coeffs = Vect.mul (minus_num (Big_int lbd)) e ; op = Ge ; cst = minus_num (Big_int lbn)} :: sys) + with + | Some cub , Some clb -> Some(List.tl clb,(lb,e,ub), List.tl cub) + | _ -> failwith "Interval without proof" + ) + | None -> None + + +let check_sys sys = + List.for_all (fun (c,p) -> List.for_all (fun (_,n) -> sign_num n <> 0) c.coeffs) sys + + +let xlia (can_enum:bool) reduction_equations sys = + + + let rec enum_proof (id:int) (sys:prf_sys) : proof option = + if debug then (Printf.printf "enum_proof\n" ; flush stdout) ; + assert (check_sys sys) ; + + let nsys,prf = List.split sys in + match get_bound nsys with + | None -> None (* Is the systeme really unbounded ? *) + | Some(prf1,(lb,e,ub),prf2) -> + if debug then Printf.printf "Found interval: %a in [%s;%s] -> " Vect.pp_vect e (string_of_num lb) (string_of_num ub) ; + (match start_enum id e (ceiling_num lb) (floor_num ub) sys + with + | Some prfl -> + Some(Enum(id,proof_of_farkas prf prf1,e, proof_of_farkas prf prf2,prfl)) + | None -> None + ) + + and start_enum id e clb cub sys = + if clb >/ cub + then Some [] + else + let eq = {coeffs = e ; op = Eq ; cst = clb} in + match aux_lia (id+1) ((eq, Def id) :: sys) with + | None -> None + | Some prf -> + match start_enum id e (clb +/ (Int 1)) cub sys with + | None -> None + | Some l -> Some (prf::l) + + and aux_lia (id:int) (sys:prf_sys) : proof option = + assert (check_sys sys) ; + if debug then Printf.printf "xlia: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; + try + let sys = reduction_equations sys in + if debug then Printf.printf "after reduction: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; - match linear_prover sys with - | Some prf -> Some (Step(id,prf,Done)) - | None -> enum_proof id sys - with FoundProof prf -> + match linear_prover sys with + | Some prf -> Some (Step(id,prf,Done)) + | None -> if can_enum then enum_proof id sys else None + with FoundProof prf -> (* [reduction_equations] can find a proof *) - Some(Step(id,prf,Done)) in + Some(Step(id,prf,Done)) in (* let sys' = List.map (fun (p,o) -> Mc.norm0 p , o) sys in*) - let id = List.length sys in - let orpf = - try - let sys = simpl_sys sys in - aux_lia id sys - with FoundProof pr -> Some(Step(id,pr,Done)) in - match orpf with - | None -> None - | Some prf -> + let id = List.length sys in + let orpf = + try + let sys = simpl_sys sys in + aux_lia id sys + with FoundProof pr -> Some(Step(id,pr,Done)) in + match orpf with + | None -> None + | Some prf -> (*Printf.printf "direct proof %a\n" output_proof prf ; *) - let env = mapi (fun _ i -> i) sys in - let prf = compile_proof env prf in + let env = mapi (fun _ i -> i) sys in + let prf = compile_proof env prf in (*try if Mc.zChecker sys' prf then Some prf else raise Certificate.BadCertificate with Failure s -> (Printf.printf "%s" s ; Some prf) *) Some prf - - - let cstr_compat_of_poly (p,o) = - let (v,c) = LinPoly.linpol_of_pol p in - {coeffs = v ; op = o ; cst = minus_num c } - - - let lia sys = - LinPoly.MonT.clear (); - let sys = List.map (develop_constraint z_spec) sys in - let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in - let sys = mapi (fun c i -> (c,Hyp i)) sys in - xlia reduction_equations sys - - - let nlia sys = - LinPoly.MonT.clear (); - let sys = List.map (develop_constraint z_spec) sys in - let sys = mapi (fun c i -> (c,Hyp i)) sys in - - let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in - - let collect_square = - List.fold_left (fun acc ((p,_),_) -> Poly.fold - (fun m _ acc -> - match Monomial.sqrt m with - | None -> acc - | Some s -> MonMap.add s m acc) p acc) MonMap.empty sys in - let sys = MonMap.fold (fun s m acc -> - let s = LinPoly.linpol_of_pol (Poly.add s (Int 1) (Poly.constant (Int 0))) in - let m = Poly.add m (Int 1) (Poly.constant (Int 0)) in - ((m, Ge), (Square s))::acc) collect_square sys in - -(* List.iter (fun ((p,_),_) -> Printf.printf "square %a\n" Poly.pp p) gen_square*) - - let sys = - if is_linear then sys - else sys @ (all_sym_pairs (fun ((c,o),p) ((c',o'),p') -> - ((Poly.product c c',opMult o o'), MulPrf(p,p'))) sys) in + - let sys = List.map (fun (c,p) -> cstr_compat_of_poly c,p) sys in - assert (check_sys sys) ; - xlia (if is_linear then reduction_equations else reduction_non_lin_equations) sys +let cstr_compat_of_poly (p,o) = + let (v,c) = LinPoly.linpol_of_pol p in + {coeffs = v ; op = o ; cst = minus_num c } + + +let lia (can_enum:bool) (prfdepth:int) sys = + LinPoly.MonT.clear (); + max_nb_cstr := compute_max_nb_cstr sys prfdepth ; + let sys = List.map (develop_constraint z_spec) sys in + let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in + let sys = mapi (fun c i -> (c,Hyp i)) sys in + xlia can_enum reduction_equations sys + + +let nlia enum prfdepth sys = + LinPoly.MonT.clear (); + max_nb_cstr := compute_max_nb_cstr sys prfdepth; + let sys = List.map (develop_constraint z_spec) sys in + let sys = mapi (fun c i -> (c,Hyp i)) sys in + + let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in + + let collect_square = + List.fold_left (fun acc ((p,_),_) -> Poly.fold + (fun m _ acc -> + match Monomial.sqrt m with + | None -> acc + | Some s -> MonMap.add s m acc) p acc) MonMap.empty sys in + let sys = MonMap.fold (fun s m acc -> + let s = LinPoly.linpol_of_pol (Poly.add s (Int 1) (Poly.constant (Int 0))) in + let m = Poly.add m (Int 1) (Poly.constant (Int 0)) in + ((m, Ge), (Square s))::acc) collect_square sys in + + (* List.iter (fun ((p,_),_) -> Printf.printf "square %a\n" Poly.pp p) gen_square*) + + let sys = + if is_linear then sys + else sys @ (all_sym_pairs (fun ((c,o),p) ((c',o'),p') -> + ((Poly.product c c',opMult o o'), MulPrf(p,p'))) sys) in + + let sys = List.map (fun (c,p) -> cstr_compat_of_poly c,p) sys in + assert (check_sys sys) ; + xlia enum (if is_linear then reduction_equations else reduction_non_lin_equations) sys diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cce0a7280..1dd53a3fd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -18,6 +18,9 @@ open Pp open Mutils +open Proofview +open Goptions +open Proofview.Notations (** * Debug flag @@ -37,6 +40,53 @@ let time str f x = flush stdout); res + +(* Limit the proof search *) + +let max_depth = max_int + +(* Search limit for provers over Q R *) +let lra_proof_depth = ref max_depth + + +(* Search limit for provers over Z *) +let lia_enum = ref true +let lia_proof_depth = ref max_depth + +let get_lia_option () = + (!lia_enum,!lia_proof_depth) + +let get_lra_option () = + !lra_proof_depth + + + +let _ = + + let int_opt l vref = + { + optsync = true; + optdepr = false; + optname = List.fold_right (^) l ""; + optkey = l ; + optread = (fun () -> Some !vref); + optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v)) + } in + + let lia_enum_opt = + { + optsync = true; + optdepr = false; + optname = "Lia Enum"; + optkey = ["Lia";"Enum"]; + optread = (fun () -> !lia_enum); + optwrite = (fun x -> lia_enum := x) + } 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 + () + (** * Initialize a tag type to the Tag module declaration (see Mutils). *) @@ -359,6 +409,7 @@ struct 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") @@ -1094,10 +1145,6 @@ struct | N (a) -> Mc.N(f2f a) | I(a,_,b) -> Mc.I(f2f a,f2f b) - let is_prop t = - match t with - | Names.Anonymous -> true (* Not quite right *) - | Names.Name x -> false let mkC f1 f2 = C(f1,f2) let mkD f1 f2 = D(f1,f2) @@ -1121,6 +1168,11 @@ struct (A(at,tg,t), env,Tag.next tg) with e when Errors.noncritical e -> (X(t),env,tg) in + let is_prop term = + let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in + Term.is_prop_sort sort in + let rec xparse_formula env tg term = match kind_of_term term with | App(l,rst) -> @@ -1140,13 +1192,15 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) -> + | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)-> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg | _ when eq_constr term (Lazy.force coq_True) -> (TT,env,tg) | _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg) - | _ -> X(term),env,tg in + | _ when is_prop term -> X(term),env,tg + | _ -> raise ParseError + in xparse_formula env tg ((*Reductionops.whd_zeta*) term) let dump_formula typ dump_atom f = @@ -1377,50 +1431,57 @@ let rcst_domain_spec = lazy { dump_proof = dump_psatz coq_Q dump_q } +open Proofview.Notations + + (** * Instanciate the current Coq goal with a Micromega formula, a varmap, and a * witness. *) - - -let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = +let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in - (* todo : directly generate the proof term - or generalize befor conversion? *) - Tacticals.tclTHENSEQ [ - (fun gl -> - Proofview.V82.of_tactic (Tactics.change_concl - (set - [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); - ("__wit", cert, cert_typ) - ] - (Tacmach.pf_concl gl))) gl); - Tactics.generalize env ; - Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; - ] - + (* todo : directly generate the proof term - or generalize before conversion? *) + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + Tacticals.New.tclTHENLIST + [ + Tactics.change_concl + (set + [ + ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, Term.mkApp + (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); + ("__wit", cert, cert_typ) + ] + (Tacmach.pf_concl gl)) + ; + Tactics.new_generalize env ; + Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) + ] + end } (** * The datastructures that aggregate prover attributes. *) -type ('a,'prf) prover = { +type ('option,'a,'prf) prover = { name : string ; (* name of the prover *) - prover : 'a list -> 'prf option ; (* the prover itself *) + get_option : unit ->'option ; (* find the options of the prover *) + prover : 'option * 'a list -> 'prf option ; (* the prover itself *) hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) } + + (** * Given a list of provers and a disjunction of atoms, find a proof of any of * the atoms. Returns an (optional) pair of a proof and a prover @@ -1430,7 +1491,7 @@ type ('a,'prf) prover = { let find_witness provers polys1 = let provers = List.map (fun p -> (fun l -> - match p.prover l with + match p.prover (p.get_option (),l) with | None -> None | Some prf -> Some(prf,p)) , p.name) provers in try_any provers (List.map fst polys1) @@ -1485,7 +1546,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let res = try prover.compact prf remap with x when Errors.noncritical x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) - match prover.prover (List.map fst new_cl) with + match prover.prover (prover.get_option () ,List.map fst new_cl) with | None -> failwith "proof compaction error" | Some p -> p in @@ -1646,58 +1707,76 @@ let micromega_gen (negate:'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) unsat deduce - spec prover gl = - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in - try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - + spec prover = + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in + try + let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let env = Env.elements env in + let spec = Lazy.force spec in + match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with - | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl - | Some (ids,ff',res') -> - (Tacticals.tclTHENSEQ - [ - Tactics.generalize (List.map Term.mkVar ids) ; - micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' - ]) gl - with - | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str - (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "the use of a specialized external tool called csdp. \n\n" - ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl - - - -let micromega_order_changer cert env ff gl = - let coeff = Lazy.force coq_Rcst in - let dump_coeff = dump_Rcst in - let typ = Lazy.force coq_R in - let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in + | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") + | Some (ids,ff',res') -> + (Tacticals.New.tclTHENLIST + [ + Tactics.new_generalize (List.map Term.mkVar ids) ; + micromega_order_change spec res' + (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' + ]) + with + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") + | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + Tacticals.New.tclFAIL 0 (Pp.str + (" Skipping what remains of this tactic: the complexity of the goal requires " + ^ "the use of a specialized external tool called csdp. \n\n" + ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" + ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) + end } + +let micromega_gen parse_arith + (negate:'cst atom -> 'cst mc_cnf) + (normalise:'cst atom -> 'cst mc_cnf) + unsat deduce + spec prover = + (micromega_gen parse_arith negate normalise unsat deduce spec prover) + + +let micromega_order_changer cert env ff = + let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in + let coeff = Lazy.force coq_Rcst in + let dump_coeff = dump_Rcst in + let typ = Lazy.force coq_R in + let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in + let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Proofview.V82.of_tactic (Tactics.change_concl - (set + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + Tacticals.New.tclTHENLIST [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp - (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); - ("__wit", cert, cert_typ) + (Tactics.change_concl + (set + [ + ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, Term.mkApp + (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); + ("__wit", cert, cert_typ) + ] + (Tacmach.pf_concl gl))); + Tactics.new_generalize env ; + Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - (Tacmach.pf_concl gl) - )) - gl + end } -let micromega_genr prover gl = +let micromega_genr prover = let parse_arith = parse_rarith in let negate = Mc.rnegate in let normalise = Mc.rnormalise in @@ -1710,39 +1789,41 @@ let micromega_genr prover gl = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in - try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - - let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in - let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in - - match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with - | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in + try + let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let env = Env.elements env in + let spec = Lazy.force spec in + + let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in + let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in + + match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with + | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> let (ff,ids') = formula_hyps_concl (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in - - (Tacticals.tclTHENSEQ + (Tacticals.New.tclTHENLIST [ - Tactics.generalize (List.map Term.mkVar ids) ; + Tactics.new_generalize (List.map Term.mkVar ids) ; micromega_order_changer res' env (abstract_wrt_formula ff' ff) - ]) gl + ]) with - | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str + | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut") + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl - + ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) + end } +let micromega_genr prover = (micromega_genr prover) let lift_ratproof prover l = @@ -1898,38 +1979,61 @@ let compact_pt pt f = let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) -let linear_prover_Z = { - name = "linear prover" ; - prover = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ; - hyps = hyps_of_pt ; - compact = compact_pt ; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} +module CacheZ = PHashtable(struct + type prover_option = bool * int + type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) + let equal = (=) + let hash = Hashtbl.hash +end) + +module CacheQ = PHashtable(struct + type t = int * ((Mc.q Mc.pol * Mc.op1) list) + let equal = (=) + let hash = Hashtbl.hash +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 "nlia.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 linear_prover_Q = { - name = "linear prover"; - prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; - 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 = "linear prover"; + get_option = get_lra_option ; + prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) 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 linear_prover_R = { name = "linear prover"; - prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; + get_option = get_lra_option ; + prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) 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 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) +} let non_linear_prover_Q str o = { name = "real nonlinear prover"; - prover = call_csdpcert_q (str, o); + 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 ; @@ -1938,7 +2042,8 @@ let non_linear_prover_Q str o = { let non_linear_prover_R str o = { name = "real nonlinear prover"; - prover = call_csdpcert_q (str, o); + 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; @@ -1947,30 +2052,19 @@ let non_linear_prover_R str o = { let non_linear_prover_Z str o = { name = "real nonlinear prover"; - prover = lift_ratproof (call_csdpcert_z (str, o)); + 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) } -module CacheZ = PHashtable(struct - type t = (Mc.z Mc.pol * Mc.op1) list - let equal = Pervasives.(=) - let hash = Hashtbl.hash -end) - -let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia) -let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia) - -(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*) -(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*) - - let linear_Z = { name = "lia"; - prover = memo_zlinear_prover ; + get_option = get_lia_option; + prover = memo_zlinear_prover ; hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; @@ -1979,7 +2073,8 @@ let linear_Z = { let nlinear_Z = { name = "nlia"; - prover = memo_nlia ; + get_option = get_lia_option; + prover = memo_nlia ; hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; @@ -2001,56 +2096,56 @@ let tauto_lia ff = * solvers *) -let psatzl_Z gl = +let psatzl_Z = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_prover_Z ] gl + [ linear_Z ] -let psatzl_Q gl = +let psatzl_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec - [ linear_prover_Q ] gl + [ linear_prover_Q ] -let psatz_Q i gl = +let psatz_Q i = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec - [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl - - -let psatzl_R gl = - micromega_genr [ linear_prover_R ] gl + [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] +let psatzl_R = + micromega_genr [ linear_prover_R ] -let psatz_R i gl = - micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl +let psatz_R i = + micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] -let psatz_Z i gl = +let psatz_Z i = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl + [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] -let sos_Z gl = +let sos_Z = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ non_linear_prover_Z "pure_sos" None ] gl + [ non_linear_prover_Z "pure_sos" None ] -let sos_Q gl = +let sos_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec - [ non_linear_prover_Q "pure_sos" None ] gl + [ non_linear_prover_Q "pure_sos" None ] -let sos_R gl = - micromega_genr [ non_linear_prover_R "pure_sos" None ] gl +let sos_R = + micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia gl = +let xlia = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_Z ] gl + [ linear_Z ] with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise -let xnlia gl = +let xnlia = try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ nlinear_Z ] gl + [ nlinear_Z ] with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise +let nra = + micromega_genr [ nlinear_prover_R ] (* Local Variables: *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 75237aaa5..bfc9c727d 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -21,58 +21,50 @@ open Misctypes DECLARE PLUGIN "micromega_plugin" -let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") - | ArgArg x -> x - TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (out_arg i)) ] -| [ "psatz_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (-1)) ] +| [ "psatz_Z" int_or_var(i) ] -> [ (Coq_micromega.psatz_Z i) ] +| [ "psatz_Z" ] -> [ (Coq_micromega.psatz_Z (-1)) ] END TACTIC EXTEND Lia -[ "xlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xlia) ] +[ "xlia" ] -> [ (Coq_micromega.xlia) ] END TACTIC EXTEND Nia -[ "xnlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xnlia) ] +[ "xnlia" ] -> [ (Coq_micromega.xnlia) ] END - +TACTIC EXTEND NRA +[ "xnra" ] -> [ (Coq_micromega.nra)] +END TACTIC EXTEND Sos_Z -| [ "sos_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Z) ] +| [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ] END TACTIC EXTEND Sos_Q -| [ "sos_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Q) ] +| [ "sos_Q" ] -> [ (Coq_micromega.sos_Q) ] END TACTIC EXTEND Sos_R -| [ "sos_R" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_R) ] -END - -(* -TACTIC EXTEND Omicron -[ "psatzl_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Z) ] +| [ "sos_R" ] -> [ (Coq_micromega.sos_R) ] END -*) TACTIC EXTEND LRA_Q -[ "psatzl_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Q) ] +[ "psatzl_Q" ] -> [ (Coq_micromega.psatzl_Q) ] END TACTIC EXTEND LRA_R -[ "psatzl_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_R) ] +[ "psatzl_R" ] -> [ (Coq_micromega.psatzl_R) ] END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (out_arg i)) ] -| [ "psatz_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (-1)) ] +| [ "psatz_R" int_or_var(i) ] -> [ (Coq_micromega.psatz_R i) ] +| [ "psatz_R" ] -> [ (Coq_micromega.psatz_R (-1)) ] END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (out_arg i)) ] -| [ "psatz_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (-1)) ] +| [ "psatz_Q" int_or_var(i) ] -> [ (Coq_micromega.psatz_Q i) ] +| [ "psatz_Q" ] -> [ (Coq_micromega.psatz_Q (-1)) ] END diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index a36369d22..e22fe5843 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -98,12 +98,12 @@ module PSet = ISet module System = Hashtbl.Make(Vect) - type proof = - | Hyp of int - | Elim of var * proof * proof - | And of proof * proof - +type proof = +| Hyp of int +| Elim of var * proof * proof +| And of proof * proof +let max_nb_cstr = ref max_int type system = { sys : cstr_info ref System.t ; @@ -120,7 +120,7 @@ and cstr_info = { (** A system of constraints has the form [\{sys = s ; vars = v\}]. [s] is a hashtable mapping a normalised vector to a [cstr_info] record where - [bound] is an interval - - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint. + - [prf_idx] is the set of hypothesis indexes (i.e. constraints in the initial system) used to obtain the current constraint. In the initial system, each constraint is given an unique singleton proof_idx. When a new constraint c is computed by a function f(c1,...,cn), its proof_idx is ISet.fold union (List.map (fun x -> x.proof_idx) [c1;...;cn] - [pos] is the number of positive values of the vector @@ -208,8 +208,7 @@ let merge_cstr_info i1 i2 = *) let xadd_cstr vect cstr_info sys = - if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ; - try + try let info = System.find sys vect in match merge_cstr_info cstr_info !info with | None -> raise (SystemContradiction (And(cstr_info.prf, (!info).prf))) @@ -217,6 +216,13 @@ let xadd_cstr vect cstr_info sys = with | Not_found -> System.replace sys vect (ref cstr_info) +exception TimeOut + +let xadd_cstr vect cstr_info sys = + if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ; + if System.length sys < !max_nb_cstr + then xadd_cstr vect cstr_info sys + else raise TimeOut type cstr_ext = | Contradiction (** The constraint is contradictory. @@ -866,7 +872,7 @@ let mk_proof hyps prf = | Elim(v,prf1,prf2) -> let prfsl = mk_proof prf1 and prfsr = mk_proof prf2 in - (* I take only the pairs for which the elimination is meaningfull *) + (* I take only the pairs for which the elimination is meaningful *) forall_pairs (pivot v) prfsl prfsr | And(prf1,prf2) -> let prfsl1 = mk_proof prf1 diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 2dd443f00..c13e8fc28 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -66,6 +66,15 @@ let all_sym_pairs f l = | e::l -> xpairs (pair_with acc e l) l in xpairs [] l +let all_pairs f l = + let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in + + let rec xpairs acc l = + match l with + | [] -> acc + | e::lx -> xpairs (pair_with acc e l) lx in + xpairs [] l + let rec map3 f l1 l2 l3 = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 8a2a957cd..7e38109d6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,6 +27,7 @@ open Globnames open Nametab open Contradiction open Misctypes +open Proofview.Notations module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -34,9 +35,9 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) let elim_id id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) - end + end } let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl let timing timer_name f arg = f arg @@ -1416,7 +1417,7 @@ let reintroduce id = open Proofview.Notations let coq_omega = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in let destructure_omega = Tacmach.New.of_old destructure_omega gl in @@ -1464,12 +1465,12 @@ let coq_omega = Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end - end + end } let coq_omega = coq_omega let nat_inject = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = try match destructurate_term t with @@ -1603,7 +1604,7 @@ let nat_inject = in let hyps_types = Tacmach.New.pf_hyps_types gl in loop (List.rev hyps_types) - end + end } let dec_binop = function | Zne -> coq_dec_Zne @@ -1673,22 +1674,22 @@ let onClearedName id tac = (* so renaming may be necessary *) Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id = Tacmach.New.of_old (fresh_id [] id) gl in Tacticals.New.tclTHEN (introduction id) (tac id) - end) + end }) let onClearedName2 id tac = Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end) + end }) let destructure_hyps = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in @@ -1828,10 +1829,10 @@ let destructure_hyps = in let hyps = Proofview.Goal.hyps gl in loop hyps - end + end } let destructure_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let decidability = Tacmach.New.of_old decidability gl in let rec loop t = @@ -1855,7 +1856,7 @@ let destructure_goal = Tacticals.New.tclTHEN goal_tac destructure_hyps in (loop concl) - end + end } let destructure_goal = destructure_goal diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ff6acf139..dbd7460e2 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -109,6 +109,7 @@ open Pattern open Patternops open Constr_matching open Tacmach +open Proofview.Notations (*i*) (*s First, we need to access some Coq constants @@ -227,7 +228,7 @@ let compute_ivs f cs gl = let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let is_conv = Reductionops.is_conv env sigma in begin match decomp_term body3 with | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) @@ -446,7 +447,7 @@ let quote_terms ivs lc = yet. *) let quote f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in let ivs = compute_ivs f cl gl in @@ -459,10 +460,10 @@ let quote f lid = match ivs.variable_lhs with | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end + end } let gen_quote cont c f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in let ivs = compute_ivs f cl gl in @@ -474,7 +475,7 @@ let gen_quote cont c f lid = match ivs.variable_lhs with | None -> cont (mkApp (f, [| p |])) | Some _ -> cont (mkApp (f, [| vm; p |])) - end + end } (*i diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 new file mode 100644 index 000000000..856ec0db5 --- /dev/null +++ b/plugins/setoid_ring/g_newring.ml4 @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Pp +open Util +open Libnames +open Printer +open Newring_ast +open Newring + +DECLARE PLUGIN "newring_plugin" + +TACTIC EXTEND protect_fv + [ "protect_fv" string(map) "in" ident(id) ] -> + [ Proofview.V82.tactic (protect_tac_in map id) ] +| [ "protect_fv" string(map) ] -> + [ Proofview.V82.tactic (protect_tac map) ] +END + +TACTIC EXTEND closed_term + [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> + [ Proofview.V82.tactic (closed_term t l) ] +END + +VERNAC ARGUMENT EXTEND ring_mod + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] + | [ "abstract" ] -> [ Ring_kind Abstract ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] + | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] + | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] + | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] + | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] + | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] + | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + [ Pow_spec (Closed l, pow_spec) ] + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + [ Pow_spec (CstTac cst_tac, pow_spec) ] + | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] +END + +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> + [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) power sign div] + | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.ring_req)) + ) !from_name ] +END + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] +END + +VERNAC ARGUMENT EXTEND field_mod + | [ ring_mod(m) ] -> [ Ring_mod m ] + | [ "completeness" constr(inj) ] -> [ Inject inj ] +END + +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> + [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] +| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.field_req)) + ) !field_from_name ] +END + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] +END diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml index e704c466e..e203b9f65 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml @@ -30,8 +30,8 @@ open Declare open Decl_kinds open Entries open Misctypes - -DECLARE PLUGIN "newring_plugin" +open Newring_ast +open Proofview.Notations (****************************************************************************) (* controlled reduction *) @@ -105,13 +105,6 @@ let protect_tac_in map id = Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; -TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> - [ Proofview.V82.tactic (protect_tac_in map id) ] -| [ "protect_fv" string(map) ] -> - [ Proofview.V82.tactic (protect_tac map) ] -END;; - (****************************************************************************) let closed_term t l = @@ -120,12 +113,6 @@ let closed_term t l = if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) ;; -TACTIC EXTEND closed_term - [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ Proofview.V82.tactic (closed_term t l) ] -END -;; - (* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] @@ -143,11 +130,15 @@ let closed_term_ast l = mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let tacname = { + mltac_name = tacname; + mltac_index = 0; + } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, - [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) + [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)])) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -188,16 +179,20 @@ let ltac_lcall tac args = let ltac_letin (x, e1) e2 = TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) -let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = - Tacinterp.eval_tactic +let ltac_apply (f:glob_tactic_expr) (args: Tacinterp.Value.t list) = + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar (Loc.ghost, id)) in + (succ i, x :: vars, Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + Tacinterp.eval_tactic_ist ist (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) let ltac_record flds = TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) - -let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) - let dummy_goal env sigma = let (gl,_,sigma) = Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in @@ -207,20 +202,39 @@ let constr_of v = match Value.to_constr v with | Some c -> c | None -> failwith "Ring.exec_tactic: anomaly" +let tactic_res = ref [||] + +let get_res = + let open Tacexpr in + let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in + let entry = { mltac_name = name; mltac_index = 0 } in + let tac args ist = + let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in + let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in + tactic_res := Array.init n init; + Proofview.tclUNIT () + in + Tacenv.register_ml_tactic name [| tac |]; + entry + let exec_tactic env evd n f args = + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar (Loc.ghost, id)) in + (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in - let res = ref [||] in - let get_res ist = - let l = List.map (fun id -> Id.Map.find id ist.lfun) lid in - res := Array.of_list l; - TacId[] in - let getter = - Tacexp(TacFun(List.map(fun id -> Some id) lid, - Tacintern.glob_tactic(tacticIn get_res))) in + let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in + let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in + let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in + (** Evaluate the whole result *) let gl = dummy_goal env evd in - let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in + let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) + Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -355,20 +369,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -type ring_info = - { ring_carrier : types; - ring_req : constr; - ring_setoid : constr; - ring_ext : constr; - ring_morph : constr; - ring_th : constr; - ring_cst_tac : glob_tactic_expr; - ring_pow_tac : glob_tactic_expr; - ring_lemma1 : constr; - ring_lemma2 : constr; - ring_pre_tac : glob_tactic_expr; - ring_post_tac : glob_tactic_expr } - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -600,13 +600,6 @@ let dest_morph env sigma m_spec = (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" - -type 'constr coeff_spec = - Computational of 'constr (* equality test *) - | Abstract (* coeffs = Z *) - | Morphism of 'constr (* general morphism *) - - let reflect_coeff rkind = (* We build an ill-typed terms on purpose... *) match rkind with @@ -614,10 +607,6 @@ let reflect_coeff rkind = | Computational c -> lapp coq_comp [|c|] | Morphism m -> lapp coq_morph [|m|] -type cst_tac_spec = - CstTac of raw_tactic_expr - | Closed of reference list - let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacintern.glob_tactic t @@ -686,7 +675,7 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = let rk = reflect_coeff morphth in let params,ctx = exec_tactic env !evd 5 (zltac "ring_lemmas") - (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in + [sth;ext;rth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -721,41 +710,12 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = ring_post_tac = posttac }) in () -type 'constr ring_mod = - Ring_kind of 'constr coeff_spec - | Const_tac of cst_tac_spec - | Pre_tac of raw_tactic_expr - | Post_tac of raw_tactic_expr - | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr - | Pow_spec of cst_tac_spec * Constrexpr.constr_expr - (* Syntaxification tactic , correctness lemma *) - | Sign_spec of Constrexpr.constr_expr - | Div_spec of Constrexpr.constr_expr - - let ic_coeff_spec = function | Computational t -> Computational (ic_unsafe t) | Morphism t -> Morphism (ic_unsafe t) | Abstract -> Abstract -VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] - | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] - | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] - | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] - | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] - | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] - | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] - | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] - | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] - | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> - [ Pow_spec (CstTac cst_tac, pow_spec) ] - | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] -END - let set_once s r v = if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") @@ -780,20 +740,6 @@ let process_ring_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF - | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) power sign div] - | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) - ) !from_name ] -END - (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) @@ -809,24 +755,28 @@ let make_term_list env evd carrier rl = (plapp evd coq_nil [|carrier|]) in Typing.solve_evars env evd l +let carg = Tacinterp.Value.of_constr +let tacarg expr = + Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr + let ltac_ring_structure e = let req = carg e.ring_req in let sth = carg e.ring_setoid in let ext = carg e.ring_ext in let morph = carg e.ring_morph in let th = carg e.ring_th in - let cst_tac = Tacexp e.ring_cst_tac in - let pow_tac = Tacexp e.ring_pow_tac in + let cst_tac = tacarg e.ring_cst_tac in + let pow_tac = tacarg e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in - let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in + let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in + let posttac = tacarg (TacFun([None],e.ring_post_tac)) in [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] let ring_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) let evdref = ref sigma in @@ -837,14 +787,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = let ring = ltac_ring_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end - -TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] -END - - + end } (***********************************************************************) @@ -919,19 +862,6 @@ let dest_field env evd th_spec = (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" -type field_info = - { field_carrier : types; - field_req : constr; - field_cst_tac : glob_tactic_expr; - field_pow_tac : glob_tactic_expr; - field_ok : constr; - field_simpl_eq_ok : constr; - field_simpl_ok : constr; - field_simpl_eq_in_ok : constr; - field_cond : constr; - field_pre_tac : glob_tactic_expr; - field_post_tac : glob_tactic_expr } - let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" @@ -1034,7 +964,7 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power let rk = reflect_coeff morphth in let params,ctx = exec_tactic env !evd 9 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in + [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in let lemma3 = params.(5) in @@ -1078,15 +1008,6 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power field_pre_tac = pretac; field_post_tac = posttac }) in () -type 'constr field_mod = - Ring_mod of 'constr ring_mod - | Inject of Constrexpr.constr_expr - -VERNAC ARGUMENT EXTEND field_mod - | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "completeness" constr(inj) ] -> [ Inject inj ] -END - let process_field_mods l = let kind = ref None in let set = ref None in @@ -1111,38 +1032,23 @@ let process_field_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF -| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] -| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) - ) !field_from_name ] -END - - let ltac_field_structure e = let req = carg e.field_req in - let cst_tac = Tacexp e.field_cst_tac in - let pow_tac = Tacexp e.field_pow_tac in + let cst_tac = tacarg e.field_cst_tac in + let pow_tac = tacarg e.field_pow_tac in let field_ok = carg e.field_ok in let field_simpl_ok = carg e.field_simpl_ok in let field_simpl_eq_ok = carg e.field_simpl_eq_ok in let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in - let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in - let posttac = Tacexp(TacFun([None],e.field_post_tac)) in + let pretac = tacarg (TacFun([None],e.field_pre_tac)) in + let posttac = tacarg (TacFun([None],e.field_post_tac)) in [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f:glob_tactic_expr) lH rl t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try let evdref = ref sigma in @@ -1153,10 +1059,4 @@ let field_lookup (f:glob_tactic_expr) lH rl t = let field = ltac_field_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end - - -TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] -END + end } diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli new file mode 100644 index 000000000..4bd3383d6 --- /dev/null +++ b/plugins/setoid_ring/newring.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Libnames +open Globnames +open Constrexpr +open Tacexpr +open Proof_type +open Newring_ast + +val protect_tac_in : string -> Id.t -> tactic + +val protect_tac : string -> tactic + +val closed_term : constr -> global_reference list -> tactic + +val process_ring_mods : + constr_expr ring_mod list -> + constr coeff_spec * (constr * constr) option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val ic : constr_expr -> Evd.evar_map * constr + +val from_name : ring_info Spmap.t ref + +val ring_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic + +val process_field_mods : + constr_expr field_mod list -> + constr coeff_spec * + (constr * constr) option * constr option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_field_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + constr option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val field_from_name : field_info Spmap.t ref + +val field_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli new file mode 100644 index 000000000..c26fcc8d1 --- /dev/null +++ b/plugins/setoid_ring/newring_ast.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Constr +open Libnames +open Constrexpr +open Tacexpr + +type 'constr coeff_spec = + Computational of 'constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of 'constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of reference list + +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of constr_expr * constr_expr + | Pow_spec of cst_tac_spec * constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of constr_expr + | Div_spec of constr_expr + +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of constr_expr + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; + ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib index a98392f1e..7d6c49588 100644 --- a/plugins/setoid_ring/newring_plugin.mllib +++ b/plugins/setoid_ring/newring_plugin.mllib @@ -1,2 +1,3 @@ Newring Newring_plugin_mod +G_newring |