diff options
Diffstat (limited to 'plugins')
68 files changed, 819 insertions, 1092 deletions
diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el new file mode 100644 index 0000000000..4e8830f6c1 --- /dev/null +++ b/plugins/.dir-locals.el @@ -0,0 +1,4 @@ +((coq-mode . ((eval . (let ((default-directory (locate-dominating-file + buffer-file-name ".dir-locals.el"))) + (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) + (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2d9dec095a..201726d1e6 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -15,13 +15,11 @@ open Declarations open Term open EConstr open Vars -open Tacmach open Tactics open Typing open Ccalgo open Ccproof open Pp -open CErrors open Util open Proofview.Notations @@ -239,21 +237,43 @@ let build_projection intype (cstr:pconstructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let _M =mkMeta - let app_global f args k = - Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_app_global f args k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_refine c = Proofview.V82.tactic (refine c) -let refine c = refine c + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) + +let rec gen_holes env sigma t n accu = + let open Sigma in + if Int.equal n 0 then (sigma, List.rev accu) + else match EConstr.kind sigma t with + | Prod (_, u, t) -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in + let sigma = Sigma.to_evar_map sigma in + let t = EConstr.Vars.subst1 ev t in + gen_holes env sigma t (pred n) (ev :: accu) + | _ -> assert false + +let app_global_with_holes f args n = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + Refine.refine { Sigma.run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let t = Tacmach.New.pf_get_type_of gl fc in + let t = Termops.prod_applist sigma t (Array.to_list args) in + let ans = mkApp (fc, args) in + let (sigma, holes) = gen_holes env sigma t n [] in + let ans = applist (ans, holes) in + let evdref = ref sigma in + let () = Typing.e_check env evdref ans concl in + Sigma.Unsafe.of_pair (ans, !evdref) + end } + end } let assert_before n c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_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) + Sigma.Unsafe.of_pair (assert_before n c, evm) end } let refresh_type env evm ty = @@ -281,18 +301,18 @@ let rec proof_tac p : unit Proofview.tactic = let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in refresh_universes (type_of l) (fun typ -> - new_app_global _sym_eq [|typ;r;l;c|] exact_check) + app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in refresh_universes (type_of lr) (fun typ -> - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) + app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in refresh_universes (type_of t2) (fun typ -> - let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) + let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in + Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs @@ -303,18 +323,18 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in + let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = - app_global _trans_eq + app_global_with_holes _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|] in - Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + mkApp(tf2,[|tx2|])|] 2 in + Tacticals.New.tclTHENS prf + [Tacticals.New.tclTHEN lemma1 (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); + [Tacticals.New.tclTHEN lemma2 (proof_tac p2); reflexivity; Tacticals.New.tclZEROMSG (Pp.str @@ -330,8 +350,8 @@ let rec proof_tac p : unit Proofview.tactic = build_projection intype cstr special default gl in let injt= - app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) + app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in + Tacticals.New.tclTHEN injt (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } @@ -341,27 +361,29 @@ let refute_tac c t1 t2 p = let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = - let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k 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 refine_exact_check c = + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Sigma.Unsafe.of_pair (exact_check c, evm) + end } let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = - let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let neweq= app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + 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)] + [proof_tac p; endt refine_exact_check] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } @@ -375,44 +397,27 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] end } -let discriminate_tac (cstr,u as cstru) p = +(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *) +let discriminate_tac cstru p = Proofview.Goal.enter { enter = begin fun gl -> - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in - let identity = Universes.constr_of_global (Lazy.force _I) in - let identity = EConstr.of_constr identity in - let trivial = Universes.constr_of_global (Lazy.force _True) in - let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in - let outtype = mkSort outtype in - let pred = mkLambda(Name xid,outtype,mkRel 1) in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in - let proj = build_projection intype cstru trivial concl gl in - let injt=app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in - let endt k = - injt (fun injt -> - app_global _eq_rect - [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq=new_app_global _eq [|intype;t1;t2|] in + let neweq=app_global _eq [|intype;lhs;rhs|] in 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)]) + [proof_tac p; Equality.discrHyp hid]) end } (* wrap everything *) -let build_term_to_complete uf meta pac = +let build_term_to_complete uf pac = let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.init pac.arity meta) in - let all_args = List.rev_append real_args dummy_args in + let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in let (kn, u) = cinfo.ci_constr in - applist (mkConstructU (kn, EInstance.make u), all_args) + (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity) let cc_tactic depth additionnal_terms = Proofview.Goal.enter { enter = begin fun gl -> @@ -434,16 +439,17 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> + let open Glob_term in let env = Proofview.Goal.env gl in - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype ~lax:true false [] env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) + in Feedback.msg_info - (Pp.str "Goal is solvable by congruence but \ - some arguments are missing."); + (Pp.str "Goal is solvable by congruence but some arguments are missing."); Feedback.msg_info (Pp.str " Try " ++ hov 8 @@ -451,7 +457,7 @@ let cc_tactic depth additionnal_terms = str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env env sigma) + pr_missing terms_to_complete ++ str ")\"," end ++ @@ -472,13 +478,13 @@ let cc_tactic depth additionnal_terms = convert_to_hyp_tac ida ta idb tb p end } -let cc_fail gls = - user_err ~hdr:"Congruence" (Pp.str "congruence failed.") +let cc_fail = + Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - (Proofview.V82.tactic cc_fail) + cc_fail (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent @@ -492,16 +498,15 @@ 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 { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + Proofview.Goal.s_enter { s_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 let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) - (k term) - end }) + Sigma.Unsafe.of_pair (k term, evm) + end } let f_equal = Proofview.Goal.enter { enter = begin fun gl -> @@ -511,7 +516,7 @@ let f_equal = try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) - [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)] + [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index de6eb982ee..b4bb62be8e 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -8,13 +8,12 @@ (************************************************************************) open EConstr -open Proof_type val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : tactic +val cc_fail : unit Proofview.tactic val congruence_tac : int -> constr list -> unit Proofview.tactic diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2b12462ad5..322fbcea74 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -657,7 +657,7 @@ let extraction_library is_rec m = let l = List.rev (environment_until (Some dir_m)) in let select l (mp,struc) = if Visit.needed_mp mp - then (mp, extract_structure env mp no_delta true struc) :: l + then (mp, extract_structure env mp no_delta ~all:true struc) :: l else l in let struc = List.fold_left select [] l in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 7773f6a2fd..9900792cac 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -9,9 +9,9 @@ open Hipattern open Names open Term +open EConstr open Vars open Termops -open Tacmach open Util open Declarations open Globnames @@ -44,28 +44,27 @@ let rec nb_prod_after n c= 1+(nb_prod_after 0 b) | _ -> 0 -let construct_nhyps ind gls = +let construct_nhyps env ind = let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in - let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in + let constr_types = Inductiveops.arities_of_constructors env ind in let hyp = nb_prod_after nparams in Array.map hyp constr_types (* indhyps builds the array of arrays of constructor hyps for (ind largs)*) -let ind_hyps nevar ind largs gls= - let types= Inductiveops.arities_of_constructors (pf_env gls) ind in +let ind_hyps env sigma nevar ind largs = + let types= Inductiveops.arities_of_constructors env ind in let myhyps t = - let t1=Term.prod_applist t largs in - let t2=snd (decompose_prod_n_assum nevar t1) in - fst (decompose_prod_assum t2) in + let t = EConstr.of_constr t in + let t1=Termops.prod_applist sigma t largs in + let t2=snd (decompose_prod_n_assum sigma nevar t1) in + fst (decompose_prod_assum sigma t2) in Array.map myhyps types -let special_nf gl= - let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf env sigma t = + Reductionops.clos_norm_flags !red_flags env sigma t -let special_whd gl= - let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd env sigma t = + Reductionops.clos_whd_flags !red_flags env sigma t type kind_of_formula= Arrow of constr*constr @@ -78,20 +77,19 @@ type kind_of_formula= let pop t = Vars.lift (-1) t -let kind_of_formula gl term = - let normalize=special_nf gl in - let cciterm=special_whd gl term in - match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with - Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b))) +let kind_of_formula env sigma term = + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match match_with_imp_term sigma cciterm with + Some (a,b)-> Arrow (a, pop b) |_-> - match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with - Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b) + match match_with_forall_term sigma cciterm with + Some (_,a,b)-> Forall (a, b) |_-> - match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with + match match_with_nodep_ind sigma cciterm with Some (i,l,n)-> - let l = List.map EConstr.Unsafe.to_constr l in - let ind,u=EConstr.destInd (project gl) i in - let u = EConstr.EInstance.kind (project gl) u in + let ind,u=EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in if Int.equal nconstr 0 then @@ -100,7 +98,7 @@ let kind_of_formula gl term = let has_realargs=(n>0) in let is_trivial= let is_constant c = - Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in + Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) @@ -112,11 +110,11 @@ let kind_of_formula gl term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with + match match_with_sigma_type sigma cciterm with Some (i,l)-> - let (ind, u) = EConstr.destInd (project gl) i in - let u = EConstr.EInstance.kind (project gl) u in - Exists((ind, u), List.map EConstr.Unsafe.to_constr l) + let (ind, u) = EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in + Exists((ind, u), l) |_-> Atom (normalize cciterm) type atoms = {positive:constr list;negative:constr list} @@ -127,29 +125,29 @@ let no_atoms = (false,{positive=[];negative=[]}) let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) -let build_atoms gl metagen side cciterm = +let build_atoms env sigma metagen side cciterm = let trivial =ref false and positive=ref [] and negative=ref [] in - let normalize=special_nf gl in - let rec build_rec env polarity cciterm= - match kind_of_formula gl cciterm with + let normalize=special_nf env sigma in + let rec build_rec subst polarity cciterm= + match kind_of_formula env sigma cciterm with False(_,_)->if not polarity then trivial:=true | Arrow (a,b)-> - build_rec env (not polarity) a; - build_rec env polarity b + build_rec subst (not polarity) a; + build_rec subst polarity b | And(i,l,b) | Or(i,l,b)-> if b then begin - let unsigned=normalize (substnl env 0 cciterm) in + let unsigned=normalize (substnl subst 0 cciterm) in if polarity then positive:= unsigned :: !positive else negative:= unsigned :: !negative end; - let v = ind_hyps 0 i l gl in + let v = ind_hyps env sigma 0 i l in let g i _ decl = - build_rec env polarity (lift i (RelDecl.get_type decl)) in + build_rec subst polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -158,16 +156,16 @@ let build_atoms gl metagen side cciterm = Array.iter f v | Exists(i,l)-> let var=mkMeta (metagen true) in - let v =(ind_hyps 1 i l gl).(0) in + let v =(ind_hyps env sigma 1 i l).(0) in let g i _ decl = - build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in + build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in - build_rec (var::env) polarity b + build_rec (var::subst) polarity b | Atom t-> - let unsigned=substnl env 0 t in - if not (isMeta unsigned) then (* discarding wildcard atoms *) + let unsigned=substnl subst 0 t in + if not (isMeta sigma unsigned) then (* discarding wildcard atoms *) if polarity then positive:= unsigned :: !positive else @@ -177,9 +175,9 @@ let build_atoms gl metagen side cciterm = Concl -> build_rec [] true cciterm | Hyp -> build_rec [] false cciterm | Hint -> - let rels,head=decompose_prod cciterm in - let env=List.rev_map (fun _->mkMeta (metagen true)) rels in - build_rec env false head;trivial:=false (* special for hints *) + let rels,head=decompose_prod sigma cciterm in + let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in + build_rec subst false head;trivial:=false (* special for hints *) end; (!trivial, {positive= !positive; @@ -215,32 +213,32 @@ type t={id:global_reference; pat:(left_pattern,right_pattern) sum; atoms:atoms} -let build_formula side nam typ gl metagen= - let normalize = special_nf gl in +let build_formula env sigma side nam typ metagen= + let normalize = special_nf env sigma in try let m=meta_succ(metagen false) in let trivial,atoms= if !qflag then - build_atoms gl metagen side typ + build_atoms env sigma metagen side typ else no_atoms in let pattern= match side with Concl -> let pat= - match kind_of_formula gl typ with + match kind_of_formula env sigma typ with False(_,_) -> Rfalse | Atom a -> raise (Is_atom a) | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in + let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in Right pat | _ -> let pat= - match kind_of_formula gl typ with + match kind_of_formula env sigma typ with False(i,_) -> Lfalse | Atom a -> raise (Is_atom a) | And(i,_,b) -> @@ -257,7 +255,7 @@ let build_formula side nam typ gl metagen= | Arrow (a,b) -> let nfa=normalize a in LA (nfa, - match kind_of_formula gl a with + match kind_of_formula env sigma a with False(i,l)-> LLfalse(i,l) | Atom t-> LLatom | And(i,l,_)-> LLand(i,l) diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 5db8ff59ad..3f438c04a0 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Globnames val qflag : bool ref @@ -23,10 +24,10 @@ type ('a,'b) sum = Left of 'a | Right of 'b type counter = bool -> metavariable -val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array +val construct_nhyps : Environ.env -> pinductive -> int array -val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> Context.Rel.t array +val ind_hyps : Environ.env -> Evd.evar_map -> int -> pinductive -> + constr list -> EConstr.rel_context array type atoms = {positive:constr list;negative:constr list} @@ -34,7 +35,7 @@ type side = Hyp | Concl | Hint val dummy_id: global_reference -val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> +val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> constr -> bool * atoms type right_pattern = @@ -69,6 +70,6 @@ type t={id: global_reference; (*exception Is_atom of constr*) -val build_formula : side -> global_reference -> types -> - Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum +val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types -> + counter -> (t,types) sum diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 70748f0567..90e5f3ca55 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -13,7 +13,9 @@ open Formula open Sequent open Ground open Goptions -open Tacticals +open Tacmach.New +open Tacticals.New +open Proofview.Notations open Tacinterp open Libnames open Stdarg @@ -81,21 +83,29 @@ END let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") -let gen_ground_tac flag taco ids bases gl= +let gen_ground_tac flag taco ids bases = let backup= !qflag in - try + Proofview.tclOR begin + Proofview.Goal.enter { enter = begin fun gl -> qflag:=flag; let solver= match taco with Some tac-> tac | None-> snd (default_solver ()) in - let startseq gl= + let startseq k = + Proofview.Goal.s_enter { s_enter = begin fun gl -> let seq=empty_seq !ground_depth in - let seq,gl = extend_with_ref_list ids seq gl in - extend_with_auto_hints bases seq gl in - let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in - qflag:=backup;result - with reraise -> qflag:=backup;raise reraise + let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in + let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in + Sigma.Unsafe.of_pair (k seq, sigma) + end } + in + let result=ground_tac solver startseq in + qflag := backup; + result + end } + end + (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) (* special for compatibility with Intuition @@ -113,7 +123,6 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) -open Pp open Genarg open Ppconstr open Printer @@ -144,18 +153,15 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ] + [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ] END - -open Proofview.Notations -open Cc_plugin diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d6cd7e2a08..ab1dd07c11 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -12,8 +12,9 @@ open Sequent open Rules open Instances open Term -open Tacmach -open Tacticals +open Tacmach.New +open Tacticals.New +open Proofview.Notations let update_flags ()= let predref=ref Names.Cpred.empty in @@ -29,18 +30,24 @@ let update_flags ()= CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) -let ground_tac solver startseq gl= +let ground_tac solver startseq = + Proofview.Goal.enter { enter = begin fun gl -> update_flags (); - let rec toptac skipped seq gl= - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Feedback.msg_debug (Printer.pr_goal gl); + let rec toptac skipped seq = + Proofview.Goal.enter { enter = begin fun gl -> + let () = + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 + then + let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in + Feedback.msg_debug (Printer.pr_goal gl) + in tclORELSE (axiom_tac seq.gl seq) begin try - let (hd,seq1)=take_formula seq - and re_add s=re_add_formula_list skipped s in + let (hd,seq1)=take_formula (project gl) seq + and re_add s=re_add_formula_list (project gl) skipped s in let continue=toptac [] - and backtrack gl=toptac (hd::skipped) seq1 gl in + and backtrack =toptac (hd::skipped) seq1 in match hd.pat with Right rpat-> begin @@ -60,7 +67,7 @@ let ground_tac solver startseq gl= or_tac backtrack continue (re_add seq1) | Rfalse->backtrack | Rexists(i,dom,triv)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -80,7 +87,7 @@ let ground_tac solver startseq gl= left_or_tac ind backtrack hd.id continue (re_add seq1) | Lforall (_,_,_)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -119,7 +126,8 @@ let ground_tac solver startseq gl= ll_atom_tac typ la_tac hd.id continue (re_add seq1) end with Heap.EmptyHeap->solver - end gl in - let seq, gl' = startseq gl in - wrap (List.length (pf_hyps gl)) true (toptac []) seq gl' - + end + end } in + let n = List.length (Proofview.Goal.hyps gl) in + startseq (fun seq -> wrap n true (toptac []) seq) + end } diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index b5669463cd..4fd1e38a27 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val ground_tac: Tacmach.tactic -> - (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic +val ground_tac: unit Proofview.tactic -> + ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 9dc2a51a61..5a1e7c26a1 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,12 +10,12 @@ open Unify open Rules open CErrors open Util -open Term +open EConstr open Vars -open Tacmach +open Tacmach.New open Tactics -open Tacticals -open Termops +open Tacticals.New +open Proofview.Notations open Reductionops open Formula open Sequent @@ -25,11 +25,12 @@ open Sigma.Notations open Context.Rel.Declaration let compare_instance inst1 inst2= + let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in match inst1,inst2 with Phantom(d1),Phantom(d2)-> - (OrderedConstr.compare d1 d2) + (cmp d1 d2) | Real((m1,c1),n1),Real((m2,c2),n2)-> - ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 + ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2 | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1 | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1 @@ -56,12 +57,12 @@ let make_simple_atoms seq= | None->[] in {negative=seq.latoms;positive=ratoms} -let do_sequent setref triv id seq i dom atoms= +let do_sequent sigma setref triv id seq i dom atoms= let flag=ref true in let phref=ref triv in let do_atoms a1 a2 = let do_pair t1 t2 = - match unif_atoms i dom t1 t2 with + match unif_atoms sigma i dom t1 t2 with None->() | Some (Phantom _) ->phref:=true | Some c ->flag:=false;setref:=IS.add (c,id) !setref in @@ -71,26 +72,26 @@ let do_sequent setref triv id seq i dom atoms= do_atoms atoms (make_simple_atoms seq); !flag && !phref -let match_one_quantified_hyp setref seq lf= +let match_one_quantified_hyp sigma setref seq lf= match lf.pat with Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent setref triv lf.id seq i dom lf.atoms then + if do_sequent sigma setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref | _ -> anomaly (Pp.str "can't happen") -let give_instances lf seq= +let give_instances sigma lf seq= let setref=ref IS.empty in - List.iter (match_one_quantified_hyp setref seq) lf; + List.iter (match_one_quantified_hyp sigma setref seq) lf; IS.elements !setref (* collector for the engine *) -let rec collect_quantified seq= +let rec collect_quantified sigma seq= try - let hd,seq1=take_formula seq in + let hd,seq1=take_formula sigma seq in (match hd.pat with Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> - let (q,seq2)=collect_quantified seq1 in + let (q,seq2)=collect_quantified sigma seq1 in ((hd::q),seq2) | _->[],seq) with Heap.EmptyHeap -> [],seq @@ -99,60 +100,61 @@ let rec collect_quantified seq= let dummy_bvid=Id.of_string "x" -let mk_open_instance id idc gl m t= - let env=pf_env gl in - let evmap=Refiner.project gl in +let mk_open_instance env evmap id idc m t = let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_unsafe_type_of gl idc in + let typ=Typing.unsafe_type_of env evmap idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in + let (nam,_,_)=destProd evmap (whd_all env evmap typ) in match nam with Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in let rec aux n avoid env evmap decls = if Int.equal n 0 then evmap, decls else - let nid=(fresh_id avoid var_id gl) in + let nid=(fresh_id_in_env avoid var_id env) in let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let evmap = Sigma.to_evar_map evmap in let decl = LocalAssum (Name nid, c) in aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in - evmap, decls, revt + (evmap, decls, revt) (* tactics *) let left_instance_tac (inst,id) continue seq= let open EConstr in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = project gl in match inst with Phantom dom-> - if lookup (id,None) seq then + if lookup sigma (id,None) seq then tclFAIL 0 (Pp.str "already done") else - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) + tclTHENS (cut dom) [tclTHENLIST - [Proofview.V82.of_tactic introf; - pf_constr_of_global id (fun idc -> - (fun gls-> Proofview.V82.of_tactic (generalize - [mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); - Proofview.V82.of_tactic introf; + [introf; + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.enter { enter = begin fun gl -> + let id0 = List.nth (pf_ids_of_hyps gl) 0 in + generalize [mkApp(idc, [|mkVar id0|])] + end }); + introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; - tclTRY (Proofview.V82.of_tactic assumption)] - | Real((m,t) as c,_)-> - if lookup (id,Some c) seq then + tclTRY assumption] + | Real((m,t),_)-> + let c = (m, EConstr.to_constr sigma t) in + if lookup sigma (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= if m>0 then - pf_constr_of_global id (fun idc -> - fun gl-> - let evmap,rc,ot = mk_open_instance id idc gl m t in - let ot = EConstr.of_constr ot in + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.s_enter { s_enter = begin fun gl-> + let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in @@ -160,34 +162,38 @@ let left_instance_tac (inst,id) continue seq= try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in - tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) + Sigma.Unsafe.of_pair (generalize [gt], evmap) + end }) else - let t = EConstr.of_constr t in - pf_constr_of_global id (fun idc -> - Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) + pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])] in tclTHENLIST [special_generalize; - Proofview.V82.of_tactic introf; + introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] + end } let right_instance_tac inst continue seq= + let open EConstr in + Proofview.Goal.enter { enter = begin fun gl -> match inst with Phantom dom -> - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) + tclTHENS (cut dom) [tclTHENLIST - [Proofview.V82.of_tactic introf; - (fun gls-> - Proofview.V82.of_tactic (split (ImplicitBindings - [EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); + [introf; + Proofview.Goal.enter { enter = begin fun gl -> + let id0 = List.nth (pf_ids_of_hyps gl) 0 in + split (ImplicitBindings [mkVar id0]) + end }; tclSOLVE [wrap 0 true continue (deepen seq)]]; - tclTRY (Proofview.V82.of_tactic assumption)] + tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t]))) + (tclTHEN (split (ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") + end } let instance_tac inst= if (snd inst)==dummy_id then @@ -195,10 +201,10 @@ let instance_tac inst= else left_instance_tac inst -let quantified_tac lf backtrack continue seq gl= - let insts=give_instances lf seq in +let quantified_tac lf backtrack continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let insts=give_instances (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) - backtrack gl - - + backtrack + end } diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index ce711f3f97..47550f314e 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -9,9 +9,9 @@ open Globnames open Rules -val collect_quantified : Sequent.t -> Formula.t list * Sequent.t +val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t -val give_instances : Formula.t list -> Sequent.t -> +val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> (Unify.instance * global_reference) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index a60fd4d8f1..86a6770070 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -9,11 +9,12 @@ open CErrors open Util open Names -open Term +open EConstr open Vars -open Tacmach +open Tacmach.New open Tactics -open Tacticals +open Tacticals.New +open Proofview.Notations open Termops open Formula open Sequent @@ -22,148 +23,165 @@ open Locus module NamedDecl = Context.Named.Declaration +type tactic = unit Proofview.tactic + type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac type 'a with_backtracking = tactic -> 'a -let wrap n b continue seq gls= +let wrap n b continue seq = + Proofview.Goal.nf_enter { enter = begin fun gls -> Control.check_for_interrupt (); - let nc=pf_hyps gls in + let nc = Proofview.Goal.hyps gls in let env=pf_env gls in + let sigma = project gls in let rec aux i nc ctx= if i<=0 then seq else match nc with []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env (project gls) id (pf_concl gls) || - List.exists (occur_var_in_decl env (project gls) id) ctx then + if occur_var env sigma id (pf_concl gls) || + List.exists (occur_var_in_decl env sigma id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in + add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in let seq1=aux n nc [] in let seq2=if b then - add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in - continue seq2 gls + add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in + continue seq2 + end } let basename_of_global=function VarRef id->id | _->assert false let clear_global=function - VarRef id-> Proofview.V82.of_tactic (clear [id]) + VarRef id-> clear [id] | _->tclIDTAC (* connection rules *) -let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) - with Not_found->tclFAIL 0 (Pp.str "No axiom link") +let axiom_tac t seq = + Proofview.Goal.enter { enter = begin fun gl -> + try + pf_constr_of_global (find_left (project gl) t seq) >>= fun c -> + exact_no_check c + with Not_found -> tclFAIL 0 (Pp.str "No axiom link") + end } -let ll_atom_tac a backtrack id continue seq= +let ll_atom_tac a backtrack id continue seq = let open EConstr in tclIFTHENELSE - (try - tclTHENLIST - [pf_constr_of_global (find_left a seq) (fun left -> - pf_constr_of_global id (fun id -> - Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))]))); + (tclTHENLIST + [(Proofview.tclEVARMAP >>= fun sigma -> + let gr = + try Proofview.tclUNIT (find_left sigma a seq) + with Not_found -> tclFAIL 0 (Pp.str "No link") + in + gr >>= fun gr -> + pf_constr_of_global gr >>= fun left -> + pf_constr_of_global id >>= fun id -> + generalize [(mkApp(id, [|left|]))]); clear_global id; - Proofview.V82.of_tactic intro] - with Not_found->tclFAIL 0 (Pp.str "No link")) + intro]) (wrap 1 false continue seq) backtrack (* right connectives rules *) let and_tac backtrack continue seq= - tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack + tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack let or_tac backtrack continue seq= tclORELSE - (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq)))))) + (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) backtrack let arrow_tac backtrack continue seq= - tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq) + tclIFTHENELSE intro (wrap 1 true continue seq) (tclORELSE - (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq))) + (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) backtrack) (* left connectives rules *) -let left_and_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in +let left_and_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); + [(pf_constr_of_global id >>= simplest_elim); clear_global id; - tclDO n (Proofview.V82.of_tactic intro)]) + tclDO n intro]) (wrap n false continue seq) - backtrack gls + backtrack + end } -let left_or_tac ind backtrack id continue seq gls= - let v=construct_nhyps ind gls in +let left_or_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let v=construct_nhyps (pf_env gl) ind in let f n= tclTHENLIST [clear_global id; - tclDO n (Proofview.V82.of_tactic intro); + tclDO n intro; wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (pf_constr_of_global id >>= simplest_elim) (Array.map f v) - backtrack gls + backtrack + end } let left_false_tac id= - Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) + Tacticals.New.pf_constr_of_global id >>= simplest_elim (* left arrow connective rules *) (* We use this function for false, and, or, exists *) -let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= - let rcs=ind_hyps 0 indu largs gl in +let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) let myterm idc i= let rc=rcs.(i) in let p=List.length rc in + let u = EInstance.make u in let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p idc),[|capply|]) in - EConstr.of_constr (it_mkLambda_or_LetIn head rc) in + EConstr.it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in + let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); + [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc)); clear_global id; - tclDO lp (Proofview.V82.of_tactic intro)]) - (wrap lp false continue seq) backtrack gl + tclDO lp intro]) + (wrap lp false continue seq) backtrack + end } let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in let open Vars in - let a = EConstr.of_constr a in - let b = EConstr.of_constr b in - let c = EConstr.of_constr c in let cc=mkProd(Anonymous,a,(lift 1 b)) in let d idc = mkLambda (Anonymous,b, mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut c)) + (tclTHENS (cut c) [tclTHENLIST - [Proofview.V82.of_tactic introf; + [introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (Proofview.V82.of_tactic (cut cc)) - [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); + tclTHENS (cut cc) + [(pf_constr_of_global id >>= fun c -> exact_no_check c); tclTHENLIST - [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); + [(pf_constr_of_global id >>= fun idc -> generalize [d idc]); clear_global id; - Proofview.V82.of_tactic introf; - Proofview.V82.of_tactic introf; + introf; + introf; tclCOMPLETE (wrap 2 true continue seq)]]]) backtrack @@ -171,38 +189,40 @@ let ll_arrow_tac a b c backtrack id continue seq= let forall_tac backtrack continue seq= tclORELSE - (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq) + (tclIFTHENELSE intro (wrap 0 true continue seq) (tclORELSE - (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq))) + (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack) -let left_exists_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in +let left_exists_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Tacticals.New.pf_constr_of_global id >>= simplest_elim) (tclTHENLIST [clear_global id; - tclDO n (Proofview.V82.of_tactic intro); + tclDO n intro; (wrap (n-1) false continue seq)]) backtrack - gls + end } let ll_forall_tac prod backtrack id continue seq= tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod))) + (tclTHENS (cut prod) [tclTHENLIST - [Proofview.V82.of_tactic intro; - pf_constr_of_global id (fun idc -> - (fun gls-> + [intro; + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.enter { enter = begin fun gls-> let open EConstr in - let id0=pf_nth_hyp_id gls 1 in + let id0 = List.nth (pf_ids_of_hyps gls) 0 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); + tclTHEN (generalize [term]) (clear [id0]) + end }); clear_global id; - Proofview.V82.of_tactic intro; + intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; tclCOMPLETE (wrap 0 true continue (deepen seq))]) backtrack @@ -214,12 +234,13 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))] + [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] let normalize_evaluables= - onAllHypsAndConcl - (function - None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) - | Some id -> - Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) + Proofview.Goal.enter { enter = begin fun gl -> + unfold_in_concl (Lazy.force defined_connectives) <*> + tclMAP + (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + (pf_ids_of_hyps gl) + end } diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 381b7cd87c..fb21730830 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -7,10 +7,12 @@ (************************************************************************) open Term -open Tacmach +open EConstr open Names open Globnames +type tactic = unit Proofview.tactic + type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fb0c22c2b7..2d18b66054 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,11 +7,11 @@ (************************************************************************) open Term +open EConstr open CErrors open Util open Formula open Unify -open Tacmach open Globnames open Pp @@ -57,11 +57,11 @@ end module OrderedConstr= struct - type t=constr + type t=Constr.t let compare=constr_ord end -type h_item = global_reference * (int*constr) option +type h_item = global_reference * (int*Constr.t) option module Hitem= struct @@ -81,13 +81,15 @@ module CM=Map.Make(OrderedConstr) module History=Set.Make(Hitem) -let cm_add typ nam cm= +let cm_add sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in CM.add typ (nam::l) cm with Not_found->CM.add typ [nam] cm -let cm_remove typ nam cm= +let cm_remove sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in @@ -112,19 +114,19 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup item seq= +let lookup sigma item seq= History.mem item seq.history || match item with (_,None)->false - | (id,Some ((m,t) as c))-> + | (id,Some (m, t))-> let p (id2,o)= match o with None -> false - | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in + | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history -let add_formula side nam t seq gl= - match build_formula side nam t gl seq.cnt with +let add_formula env sigma side nam t seq = + match build_formula env sigma side nam t seq.cnt with Left f-> begin match side with @@ -136,7 +138,7 @@ let add_formula side nam t seq gl= | _ -> {seq with redexes=HP.add f seq.redexes; - context=cm_add f.constr nam seq.context} + context=cm_add sigma f.constr nam seq.context} end | Right t-> match side with @@ -144,18 +146,18 @@ let add_formula side nam t seq gl= {seq with gl=t;glatom=Some t} | _ -> {seq with - context=cm_add t nam seq.context; + context=cm_add sigma t nam seq.context; latoms=t::seq.latoms} -let re_add_formula_list lf seq= +let re_add_formula_list sigma lf seq= let do_one f cm= if f.id == dummy_id then cm - else cm_add f.constr f.id cm in + else cm_add sigma f.constr f.id cm in {seq with redexes=List.fold_right HP.add lf seq.redexes; context=List.fold_right do_one lf seq.context} -let find_left t seq=List.hd (CM.find t seq.context) +let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context) (*let rev_left seq= try @@ -164,7 +166,7 @@ let find_left t seq=List.hd (CM.find t seq.context) with Heap.EmptyHeap -> false *) -let rec take_formula seq= +let rec take_formula sigma seq= let hd=HP.maximum seq.redexes and hp=HP.remove seq.redexes in if hd.id == dummy_id then @@ -172,11 +174,11 @@ let rec take_formula seq= if seq.gl==hd.constr then hd,nseq else - take_formula nseq (* discarding deprecated goal *) + take_formula sigma nseq (* discarding deprecated goal *) else hd,{seq with redexes=hp; - context=cm_remove hd.constr hd.id seq.context} + context=cm_remove sigma hd.constr hd.id seq.context} let empty_seq depth= {redexes=HP.empty; @@ -196,18 +198,17 @@ let expand_constructor_hints = | gr -> [gr]) -let extend_with_ref_list l seq gl = +let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in - let f gr (seq,gl) = - let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in - let typ = EConstr.Unsafe.to_constr typ in - (add_formula Hyp gr typ seq gl,gl) in - List.fold_right f l (seq,gl) + let f gr (seq, sigma) = + let sigma, c = Evd.fresh_global env sigma gr in + let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in + (add_formula env sigma Hyp gr typ seq, sigma) in + List.fold_right f l (seq, sigma) open Hints -let extend_with_auto_hints l seq gl= +let extend_with_auto_hints env sigma l seq = let seqref=ref seq in let f p_a_t = match repr_hint p_a_t.code with @@ -215,10 +216,9 @@ let extend_with_auto_hints l seq gl= | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in (try - let (gr, _) = Termops.global_of_constr (project gl) c in - let typ=(pf_unsafe_type_of gl c) in - let typ = EConstr.Unsafe.to_constr typ in - seqref:=add_formula Hint gr typ !seqref gl + let (gr, _) = Termops.global_of_constr sigma c in + let typ=(Typing.unsafe_type_of env sigma c) in + seqref:=add_formula env sigma Hint gr typ !seqref with Not_found->()) | _-> () in let g _ _ l = List.iter f l in @@ -230,7 +230,7 @@ let extend_with_auto_hints l seq gl= error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; - !seqref, gl (*FIXME: forgetting about universes*) + !seqref, sigma (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 06c9251e7b..6ed251f34e 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,23 +6,22 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open EConstr open Formula -open Tacmach open Globnames -module OrderedConstr: Set.OrderedType with type t=constr +module OrderedConstr: Set.OrderedType with type t=Constr.t -module CM: CSig.MapS with type key=constr +module CM: CSig.MapS with type key=Constr.t -type h_item = global_reference * (int*constr) option +type h_item = global_reference * (int*Constr.t) option module History: Set.S with type elt = h_item -val cm_add : constr -> global_reference -> global_reference list CM.t -> +val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> global_reference list CM.t -val cm_remove : constr -> global_reference -> global_reference list CM.t -> +val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> global_reference list CM.t module HP: Heap.S with type elt=Formula.t @@ -40,23 +39,22 @@ val deepen: t -> t val record: h_item -> t -> t -val lookup: h_item -> t -> bool +val lookup: Evd.evar_map -> h_item -> t -> bool -val add_formula : side -> global_reference -> constr -> t -> - Proof_type.goal sigma -> t +val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t -val re_add_formula_list : Formula.t list -> t -> t +val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t -val find_left : constr -> t -> global_reference +val find_left : Evd.evar_map -> constr -> t -> global_reference -val take_formula : t -> Formula.t * t +val take_formula : Evd.evar_map -> t -> Formula.t * t val empty_seq : int -> t -val extend_with_ref_list : global_reference list -> - t -> Proof_type.goal sigma -> t * Proof_type.goal sigma +val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list -> + t -> t * Evd.evar_map -val extend_with_auto_hints : Hints.hint_db_name list -> - t -> Proof_type.goal sigma -> t * Proof_type.goal sigma +val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> + t -> t * Evd.evar_map val print_cmap: global_reference list CM.t -> Pp.std_ppcmds diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 7cbfb8e7de..49bf07155f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -8,6 +8,7 @@ open Util open Term +open EConstr open Vars open Termops open Reductionops @@ -21,13 +22,12 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) -let strip_outer_cast t = - EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) - let pop t = Vars.lift (-1) t +let subst_meta subst t = + let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in + EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t)) -let unif t1 t2= - let evd = Evd.empty in (** FIXME *) +let unif evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -35,7 +35,7 @@ let unif t1 t2= (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in let rec head_reduce t= (* forbids non-sigma-normal meta in head position*) - match kind_of_term t with + match EConstr.kind evd t with Meta i-> (try head_reduce (Int.List.assoc i !sigma) @@ -44,25 +44,25 @@ let unif t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1))) - and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in - match (kind_of_term nt1),(kind_of_term nt2) with + let nt1=head_reduce (whd_betaiotazeta evd t1) + and nt2=head_reduce (whd_betaiotazeta evd t2) in + match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then if i<j then bind j nt1 else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && - not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then + if Int.Set.is_empty (free_rels evd t) && + not (occur_term evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && - not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then + if Int.Set.is_empty (free_rels evd t) && + not (occur_term evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) - | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige - | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> @@ -84,19 +84,19 @@ let unif t1 t2= for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2)) done; assert false (* this place is unreachable but needed for the sake of typing *) with Queue.Empty-> !sigma -let value i t= +let value evd i t= let add x y= if x<0 then y else if y<0 then x else x+y in let rec vaux term= - if isMeta term && Int.equal (destMeta term) i then 0 else + if isMeta evd term && Int.equal (destMeta evd term) i then 0 else let f v t=add v (vaux t) in - let vr=fold_constr f (-1) term in + let vr=EConstr.fold evd f (-1) term in if vr<0 then -1 else vr+1 in vaux t @@ -104,11 +104,11 @@ type instance= Real of (int*constr)*int | Phantom of constr -let mk_rel_inst t= +let mk_rel_inst evd t= let new_rel=ref 1 in let rel_env=ref [] in let rec renum_rec d t= - match kind_of_term t with + match EConstr.kind evd t with Meta n-> (try mkRel (d+(Int.List.assoc n !rel_env)) @@ -117,15 +117,15 @@ let mk_rel_inst t= incr new_rel; rel_env:=(n,m) :: !rel_env; mkRel (m+d)) - | _ -> map_constr_with_binders succ renum_rec d t + | _ -> EConstr.map_with_binders evd succ renum_rec d t in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms i dom t1 t2= +let unif_atoms evd i dom t1 t2= try - let t=Int.List.assoc i (unif t1 t2) in - if isMeta t then Some (Phantom dom) - else Some (Real(mk_rel_inst t,value i t1)) + let t=Int.List.assoc i (unif evd t1 t2) in + if isMeta evd t then Some (Phantom dom) + else Some (Real(mk_rel_inst evd t,value evd i t1)) with UFAIL(_,_) ->None | Not_found ->Some (Phantom dom) @@ -134,11 +134,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *) let l=List.init n (fun i->mkMeta (k+i)) in substl l t -let more_general (m1,t1) (m2,t2)= +let more_general evd (m1,t1) (m2,t2)= let mt1=renum_metas_from 0 m1 t1 and mt2=renum_metas_from m1 m2 t2 in try - let sigma=unif mt1 mt2 in - let p (n,t)= n<m1 || isMeta t in + let sigma=unif evd mt1 mt2 in + let p (n,t)= n<m1 || isMeta evd t in List.for_all p sigma with UFAIL(_,_)->false diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 4fe9ad38d8..c9cca9bd8d 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -7,15 +7,16 @@ (************************************************************************) open Term +open EConstr exception UFAIL of constr*constr -val unif : constr -> constr -> (int*constr) list +val unif : Evd.evar_map -> constr -> constr -> (int*constr) list type instance= Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) | Phantom of constr (* domaine de quantification *) -val unif_atoms : metavariable -> constr -> constr -> constr -> instance option +val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option -val more_general : (int*constr) -> (int*constr) -> bool +val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index e11cbc279a..25d8f8c832 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -617,9 +617,9 @@ let rec fourier () = [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> + Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1))))] + (apply (get coq_Rinv_1)))] ) ])); diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8dae17d69e..55d361e3d2 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -19,12 +19,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration -let local_assum (na, t) = - RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* let msgnl = Pp.msgnl *) (* @@ -235,12 +229,13 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty +exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); - failwith "NoChange"; + raise NoChange; end in let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in @@ -542,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclTHEN tac (scan_type new_context new_t') - with Failure "NoChange" -> + with NoChange -> (* Last thing todo : push the rel in the context and continue *) scan_type (LocalAssum (x,t_x) :: context) t' end diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 7ddc84d015..61752aa339 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,5 +1,4 @@ open Names -open Term val prove_princ_for_struct : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index ee82d95d09..5e6128b1b9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util -open Term open Pp open Constrexpr open Indfun_common diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 394b252aac..8ec3d9b3ef 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function | Name n -> Name n let array_get_start a = - try - Array.init - (Array.length a - 1) - (fun i -> a.(i)) - with Invalid_argument "index out of bounds" -> - invalid_arg "array_get_start" + Array.init + (Array.length a - 1) + (fun i -> a.(i)) let id_of_name = function Name id -> id @@ -508,7 +505,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - let open EConstr in if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e4536278c0..8c972cd7cf 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,7 +7,6 @@ (************************************************************************) open Ltac_plugin -open Tacexpr open Declarations open CErrors open Util @@ -1026,7 +1025,7 @@ let invfun qhyp f = | Not_found -> error "No graph found" | Option.IsNone -> error "Cannot use equivalence with graph!" - +exception NoFunction let invfun qhyp f g = match f with | Some f -> invfun qhyp f g @@ -1041,23 +1040,23 @@ let invfun qhyp f g = begin let f1,_ = decompose_app sigma args.(1) in try - if not (isConst sigma f1) then failwith ""; + if not (isConst sigma f1) then raise NoFunction; let finfos = find_Function_infos (fst (destConst sigma f1)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct g - with | Failure "" | Option.IsNone | Not_found -> + with | NoFunction | Option.IsNone | Not_found -> try let f2,_ = decompose_app sigma args.(2) in - if not (isConst sigma f2) then failwith ""; + if not (isConst sigma f2) then raise NoFunction; let finfos = find_Function_infos (fst (destConst sigma f2)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f2 f_correct g with - | Failure "" -> + | NoFunction -> user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index d4865bf5ea..b99a05dfbc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Termops open Declarations open Glob_term open Glob_termops diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8c88399448..c463093553 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1221,6 +1221,7 @@ let get_current_subgoals_types () = let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in sigma, List.map (Goal.V82.abstract_type sigma) sgs +exception EmptySubgoals let build_and_l sigma l = let and_constr = Coqlib.build_coq_and () in let conj_constr = coq_conj () in @@ -1242,7 +1243,7 @@ let build_and_l sigma l = in let l = List.sort compare l in let rec f = function - | [] -> failwith "empty list of subgoals!" + | [] -> raise EmptySubgoals | [p] -> p,tclIDTAC,1 | p1::pl -> let c,tac,nb = f pl in @@ -1428,7 +1429,7 @@ let com_terminate using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); - with Failure "empty list of subgoals!" -> + with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; defined () diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index a5d9697ae7..470a93f2bc 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -9,7 +9,6 @@ open Util open Names open Term -open EConstr open CErrors open Evar_refiner open Tacmach diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index aa81f148e2..a3310c2d8c 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause | [ in_clause'(cl) ] -> [ cl ] END +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon +| [ local_test_lpar_id_colon(x) ] -> [ () ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7d4bccfadd..9b41675120 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,6 +67,10 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds +val test_lpar_id_colon : unit Pcoq.Gram.entry + +val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type + (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 9d50b6e6f9..cbd8a7f0fe 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -21,7 +21,6 @@ open Tacexpr open Glob_ops open CErrors open Util -open Evd open Termops open Equality open Misctypes @@ -52,8 +51,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) -let clause = Pltac.clause_dft_concl - TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] @@ -466,7 +463,7 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END @@ -815,6 +812,19 @@ TACTIC EXTEND destauto | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END +(**********************************************************************) + +(**********************************************************************) +(* A version of abstract constructing transparent terms *) +(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) +(**********************************************************************) + +TACTIC EXTEND transparent_abstract +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ] +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ] +END (* ********************************************************************* *) diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index dfa8331ff2..50e8255a67 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -16,7 +16,6 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr -open Proofview.Notations open Names DECLARE PLUGIN "g_auto" diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 40f30c7943..23ce368eea 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,9 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Misctypes open Class_tactics -open Pltac open Stdarg open Tacarg open Names @@ -85,7 +83,7 @@ TACTIC EXTEND not_evar END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] + [ "is_ground" constr(ty) ] -> [ is_ground ty ] END TACTIC EXTEND autoapply @@ -95,7 +93,6 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) open Term -open Proofview.Goal open Proofview.Notations let rec eq_constr_mod_evars sigma x y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 5fc22cb4ad..b5028190fa 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, ((arg, sep), id)) -> +| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg +| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false +| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +472,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), p)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b4a0e46ae7..5adf8475ae 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -18,7 +18,7 @@ open Glob_term open Geninterp open Extraargs open Tacmach -open Tacticals +open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,15 +123,19 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in - Tacticals.onAllHypsAndConcl + Proofview.Goal.enter { enter = begin fun gl -> + let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun cl -> match cl with - | Some id when is_tac id -> tclIDTAC - | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl)) + | Some id when is_tac id -> Tacticals.New.tclIDTAC + | _ -> cl_rewrite_clause c o AllOccurrences cl) + (None :: List.map (fun id -> Some id) hyps) + end } TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ] +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 60deb443a9..257100b012 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq = | _ -> err ()) (* idem for (x:t) *) -let test_lpar_id_colon = - Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) +open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 1d21118ae8..7e979d269d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 87b79374e7..75ab1c5ee6 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of ('a * Names.Id.t) Loc.located +| TacNonTerm of ('a * Names.Id.t option) Loc.located type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -250,7 +250,7 @@ type 'a extra_genarg_printer = let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in - let rec pr = function + let pr = function | TacTerm s -> primitive s | TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) in @@ -264,8 +264,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, (symb, id)) :: prods, arg :: args -> - TacNonTerm (loc, ((symb, arg), id)) :: pack prods args + | TacNonTerm (_, (_, None)) :: prods, args -> pack prods args + | TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args -> + TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in @@ -314,7 +315,7 @@ type 'a extra_genarg_printer = | Extend.Uentry _ | Extend.Uentryl _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" - let rec pr_targ prtac symb arg = match symb with + let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> prtac (1, Any) arg | Extend.Uentryl (_, l) -> prtac (l, Any) arg diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 23570392d8..19bdf2d49f 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -21,7 +21,7 @@ open Ppextend type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of ('a * Names.Id.t) Loc.located +| TacNonTerm of ('a * Names.Id.t option) Loc.located type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index eb97a0e70e..c5dbc8a148 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -136,7 +136,6 @@ let feedback_results results = let format_sec x = (Printf.sprintf "%.3fs" x) let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) let padl n s = ws (max 0 (n - utf8_length s)) ++ str s -let padr n s = str s ++ ws (max 0 (n - utf8_length s)) let padr_with c n s = let ulength = utf8_length s in str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2ef435b6ba..e8c9f4ebaa 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -17,7 +17,6 @@ open EConstr open Vars open Reduction open Tacticals.New -open Tacmach open Tactics open Pretype_errors open Typeclasses @@ -39,7 +38,7 @@ open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) (** Typeclass-based generalized rewriting. *) @@ -2196,7 +2195,8 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - Proofview.V82.tactic (fun gl -> + let open Tacmach.New in + Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2210,11 +2210,10 @@ let setoid_symmetry_in id = let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - Proofview.V82.of_tactic (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - gl) + end } let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 7a20838a27..6683d753bc 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -14,7 +14,6 @@ open Constrexpr open Tacexpr open Misctypes open Evd -open Proof_type open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index b09672a12b..9883c03c46 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -8,7 +8,6 @@ open Util open Names -open Term open EConstr open Misctypes open Pattern diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 1de4024fd1..4d7b0f9296 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -15,14 +15,13 @@ open Genarg open Extend open Pcoq open Egramml -open Egramcoq open Vernacexpr open Libnames open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of ('a * Names.Id.t) Loc.located +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -88,9 +87,6 @@ let rec parse_user_entry s sep = else Uentry s -let arg_list = function Rawwit t -> Rawwit (ListArg t) -let arg_opt = function Rawwit t -> Rawwit (OptArg t) - let interp_entry_name interp symb = let rec eval = function | Ulist1 e -> Ulist1 (eval e) @@ -178,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, (s, _)) -> + | TacNonTerm (loc, (s, ido)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (Loc.tag ?loc (typ, e)) + GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -206,7 +202,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, ((nt, sep), id)) -> + | TacNonTerm (loc, ((nt, sep), ido)) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -224,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, (symbol, id)) + TacNonTerm (loc, (symbol, ido)) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -300,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, (_, id)) -> Some id +| TacNonTerm (_, (_, ido)) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -320,7 +316,7 @@ let add_tactic_notation local n prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local n prods false ids tac + add_glob_tactic_notation local ~level:n prods false ids tac (**********************************************************************) (* ML Tactic entries *) @@ -366,7 +362,7 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, (_, id)) -> Some id + | TacNonTerm (_, (_, ido)) -> ido in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 48598f7f48..07aa7ad82e 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of ('a * Names.Id.t) Loc.located +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 94e14223aa..d1e2a7bbe6 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Genarg open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 8751a14c71..da7f114726 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -116,12 +116,6 @@ let intern_constr_reference strict ist = function CAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) -let intern_move_location ist = function - | MoveAfter id -> MoveAfter (intern_hyp ist id) - | MoveBefore id -> MoveBefore (intern_hyp ist id) - | MoveFirst -> MoveFirst - | MoveLast -> MoveLast - (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 91bc46fe72..f63c38d4fe 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -25,7 +25,6 @@ open Refiner open Tacmach.New open Tactic_debug open Constrexpr -open Term open Termops open Tacexpr open Genarg @@ -434,12 +433,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) = let interp_hyp_list ist env sigma l = List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l) -let interp_move_location ist env sigma = function - | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id) - | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id) - | MoveFirst -> MoveFirst - | MoveLast -> MoveLast - let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar (loc, id) -> diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 6cd5a63b32..2ec45312ea 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -8,7 +8,6 @@ open Names open Tactic_debug -open Term open EConstr open Tacexpr open Genarg diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index f04495c61d..20a2013a5e 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None) +let batch = ref false + +open Goptions + +let _ = + declare_bool_option + { optsync = false; + optdepr = false; + optname = "Ltac batch debug"; + optkey = ["Ltac";"Batch";"Debug"]; + optread = (fun () -> !batch); + optwrite = (fun x -> batch := x) } + let rec drop_spaces inst i = if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) else i @@ -150,6 +163,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + if Pervasives.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 38d8caca63..ac35464c45 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -10,7 +10,6 @@ open Environ open Pattern open Names open Tacexpr -open Term open EConstr open Evd diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index df186cc46b..1e46c253d2 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -10,7 +10,6 @@ open Term open EConstr open Hipattern open Names -open Pp open Geninterp open Misctypes open Tacexpr @@ -241,7 +240,7 @@ let tauto_uniform_unit_flags = { } (* This is the compatibility mode (not used) *) -let tauto_legacy_flags = { +let _tauto_legacy_flags = { binary_mode = true; binary_mode_bugged_detection = true; strict_in_contravariant_hyp = true; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 79d17db253..b6ad784d95 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -331,7 +331,6 @@ module M = struct open Coqlib - open Term open Constr open EConstr @@ -901,16 +900,13 @@ struct coq_Qeq, Mc.OpEq ] - let has_typ gl t1 typ = - let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in - EConstr.eq_constr (Tacmach.project gl) ty typ - + type gl = { env : Environ.env; sigma : Evd.evar_map } let is_convertible gl t1 t2 = - Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2 + Reductionops.is_conv gl.env gl.sigma t1 t2 let parse_zop gl (op,args) = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in match EConstr.kind sigma op with | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) | Ind((n,0),_) -> @@ -920,7 +916,7 @@ struct | _ -> failwith "parse_zop" let parse_rop gl (op,args) = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in match EConstr.kind sigma op with | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) | Ind((n,0),_) -> @@ -930,7 +926,7 @@ struct | _ -> failwith "parse_zop" let parse_qop gl (op,args) = - (assoc_const (Tacmach.project gl) op qop_table, args.(0) , args.(1)) + (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) let is_constant sigma t = (* This is an approx *) match EConstr.kind sigma t with @@ -1154,7 +1150,7 @@ struct rop_spec let parse_arith parse_op parse_expr env cstr gl = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in if debug then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); match EConstr.kind sigma cstr with @@ -1199,7 +1195,7 @@ struct *) let parse_formula gl parse_atom env tg term = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in let parse_atom env tg t = try @@ -1208,7 +1204,7 @@ struct with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = - let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Retyping.get_sort_of gl.env gl.sigma term in Sorts.is_prop sort in let rec xparse_formula env tg term = @@ -1720,7 +1716,6 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let vm = dump_varmap (spec.typ) (vm_of_list env) in (* 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 @@ -1730,7 +1725,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl)) + (Tacmach.New.pf_concl gl)) ] end } @@ -1967,11 +1962,13 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Some (ids,ff',res') - (** * Parse the proof environment, and call micromega_tauto *) +let fresh_id avoid id gl = + Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl) + let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) @@ -1979,17 +1976,17 @@ let micromega_gen unsat deduce spec dumpexpr prover tac = Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in - let sigma = Tacmach.project gl in - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in + let sigma = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let hyps = Tacmach.New.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let gl0 = { env = Tacmach.New.pf_env gl; sigma } in + let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in let dumpexpr = Lazy.force dumpexpr in - match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with + match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl0 with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in @@ -1998,7 +1995,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; @@ -2057,7 +2054,6 @@ let micromega_order_changer cert env ff = let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in 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 @@ -2069,7 +2065,7 @@ let micromega_order_changer cert env ff = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl))); + (Tacmach.New.pf_concl gl))); (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] end } @@ -2088,20 +2084,20 @@ let micromega_genr prover tac = dump_proof = dump_psatz coq_Q dump_q } in Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in - let sigma = Tacmach.project gl in - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in + let sigma = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let hyps = Tacmach.New.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let gl0 = { env = Tacmach.New.pf_env gl; sigma } in + let (hyps,concl,env) = parse_goal gl0 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 + match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl0 with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> let (ff,ids) = formula_hyps_concl @@ -2114,7 +2110,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index f4f9b3c2f1..3779944154 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -99,7 +99,7 @@ module PSet = ISet module System = Hashtbl.Make(Vect) type proof = -| Hyp of int +| Assum of int | Elim of var * proof * proof | And of proof * proof @@ -134,7 +134,7 @@ exception SystemContradiction of proof let hyps prf = let rec hyps prf acc = match prf with - | Hyp i -> ISet.add i acc + | Assum i -> ISet.add i acc | Elim(_,prf1,prf2) | And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in hyps prf ISet.empty @@ -143,7 +143,7 @@ let hyps prf = (** Pretty printing *) let rec pp_proof o prf = match prf with - | Hyp i -> Printf.fprintf o "H%i" i + | Assum i -> Printf.fprintf o "H%i" i | Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2 | And(prf1,prf2) -> Printf.fprintf o "A(%a,%a)" pp_proof prf1 pp_proof prf2 @@ -270,7 +270,7 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx = (match o with | Eq -> Some c , Some c | Ge -> Some c , None) ; - prf = Hyp idx } + prf = Assum idx } (** [load_system l] takes a list of constraints of type [cstr_compat] @@ -285,7 +285,7 @@ let load_system l = let vars = List.fold_left (fun vrs (cstr,i) -> match norm_cstr cstr i with - | Contradiction -> raise (SystemContradiction (Hyp i)) + | Contradiction -> raise (SystemContradiction (Assum i)) | Redundant -> vrs | Cstr(vect,info) -> xadd_cstr vect info sys ; @@ -867,7 +867,7 @@ let mk_proof hyps prf = let rec mk_proof prf = match prf with - | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ] + | Assum i -> [ ([i, Int 1] , List.nth hyps i) ] | Elim(v,prf1,prf2) -> let prfsl = mk_proof prf1 diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index cc89e2b9d8..e1ceabe9e2 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -21,8 +21,6 @@ let debugging = ref false;; exception Sanity;; -exception Unsolvable;; - (* ------------------------------------------------------------------------- *) (* Turn a rational into a decimal string with d sig digits. *) (* ------------------------------------------------------------------------- *) @@ -99,28 +97,11 @@ let vector_const c n = if c =/ Int 0 then vector_0 n else (n,itlist (fun k -> k |-> c) (1--n) undefined :vector);; -let vector_1 = vector_const (Int 1);; - let vector_cmul c (v:vector) = let n = dim v in if c =/ Int 0 then vector_0 n else n,mapf (fun x -> c */ x) (snd v) -let vector_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);; - -let vector_add (v1:vector) (v2:vector) = - let m = dim v1 and n = dim v2 in - if m <> n then failwith "vector_add: incompatible dimensions" else - (n,combine (+/) (fun x -> x =/ Int 0) (snd v1) (snd v2) :vector);; - -let vector_sub v1 v2 = vector_add v1 (vector_neg v2);; - -let vector_dot (v1:vector) (v2:vector) = - let m = dim v1 and n = dim v2 in - if m <> n then failwith "vector_add: incompatible dimensions" else - foldl (fun a i x -> x +/ a) (Int 0) - (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));; - let vector_of_list l = let n = List.length l in (n,itlist2 (|->) (1--n) l undefined :vector);; @@ -133,13 +114,6 @@ let matrix_0 (m,n) = ((m,n),undefined:matrix);; let dimensions (m:matrix) = fst m;; -let matrix_const c (m,n as mn) = - if m <> n then failwith "matrix_const: needs to be square" - else if c =/ Int 0 then matrix_0 mn - else (mn,itlist (fun k -> (k,k) |-> c) (1--n) undefined :matrix);; - -let matrix_1 = matrix_const (Int 1);; - let matrix_cmul c (m:matrix) = let (i,j) = dimensions m in if c =/ Int 0 then matrix_0 (i,j) @@ -152,8 +126,6 @@ let matrix_add (m1:matrix) (m2:matrix) = if d1 <> d2 then failwith "matrix_add: incompatible dimensions" else (d1,combine (+/) (fun x -> x =/ Int 0) (snd m1) (snd m2) :matrix);; -let matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);; - let row k (m:matrix) = let i,j = dimensions m in (j, @@ -166,20 +138,10 @@ let column k (m:matrix) = foldl (fun a (i,j) c -> if j = k then (i |-> c) a else a) undefined (snd m) : vector);; -let transp (m:matrix) = - let i,j = dimensions m in - ((j,i),foldl (fun a (i,j) c -> ((j,i) |-> c) a) undefined (snd m) :matrix);; - let diagonal (v:vector) = let n = dim v in ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);; -let matrix_of_list l = - let m = List.length l in - if m = 0 then matrix_0 (0,0) else - let n = List.length (List.hd l) in - (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;; - (* ------------------------------------------------------------------------- *) (* Monomials. *) (* ------------------------------------------------------------------------- *) @@ -195,24 +157,8 @@ let monomial_var x = (x |=> 1 :monomial);; let (monomial_mul:monomial->monomial->monomial) = combine (+) (fun x -> false);; -let monomial_pow (m:monomial) k = - if k = 0 then monomial_1 - else mapf (fun x -> k * x) m;; - -let monomial_divides (m1:monomial) (m2:monomial) = - foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;; - -let monomial_div (m1:monomial) (m2:monomial) = - let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in - if foldl (fun a x k -> k >= 0 && a) true m then m - else failwith "monomial_div: non-divisible";; - let monomial_degree x (m:monomial) = tryapplyd m x 0;; -let monomial_lcm (m1:monomial) (m2:monomial) = - (itlist (fun x -> x |-> max (monomial_degree x m1) (monomial_degree x m2)) - (union (dom m1) (dom m2)) undefined :monomial);; - let monomial_multidegree (m:monomial) = foldl (fun a x k -> k + a) 0 m;; let monomial_variables m = dom m;; @@ -252,12 +198,6 @@ let poly_cmmul (c,m) (p:poly) = let poly_mul (p1:poly) (p2:poly) = foldl (fun a m c -> poly_add (poly_cmmul (c,m) p2) a) poly_0 p1;; -let poly_div (p1:poly) (p2:poly) = - if not(poly_isconst p2) then failwith "poly_div: non-constant" else - let c = eval undefined p2 in - if c =/ Int 0 then failwith "poly_div: division by zero" - else poly_cmul (Int 1 // c) p1;; - let poly_square p = poly_mul p p;; let rec poly_pow p k = @@ -266,10 +206,6 @@ let rec poly_pow p k = else let q = poly_square(poly_pow p (k / 2)) in if k mod 2 = 1 then poly_mul p q else q;; -let poly_exp p1 p2 = - if not(poly_isconst p2) then failwith "poly_exp: not a constant" else - poly_pow p1 (Num.int_of_num (eval undefined p2));; - let degree x (p:poly) = foldl (fun a m c -> max (monomial_degree x m) a) 0 p;; let multidegree (p:poly) = @@ -282,14 +218,14 @@ let poly_variables (p:poly) = (* Order monomials for human presentation. *) (* ------------------------------------------------------------------------- *) -let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 && k1 > k2;; +let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 || x1 = x2 && k1 > k2;; let humanorder_monomial = let rec ord l1 l2 = match (l1,l2) with _,[] -> true | [],_ -> false - | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 && ord t1 t2 in - fun m1 m2 -> m1 = m2 or + | h1::t1,h2::t2 -> humanorder_varpow h1 h2 || h1 = h2 && ord t1 t2 in + fun m1 m2 -> m1 = m2 || ord (sort humanorder_varpow (graph m1)) (sort humanorder_varpow (graph m2));; @@ -297,42 +233,8 @@ let humanorder_monomial = (* Conversions to strings. *) (* ------------------------------------------------------------------------- *) -let string_of_vector min_size max_size (v:vector) = - let n_raw = dim v in - if n_raw = 0 then "[]" else - let n = max min_size (min n_raw max_size) in - let xs = List.map ((o) string_of_num (element v)) (1--n) in - "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^ - (if n_raw > max_size then ", ...]" else "]");; - -let string_of_matrix max_size (m:matrix) = - let i_raw,j_raw = dimensions m in - let i = min max_size i_raw and j = min max_size j_raw in - let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in - "["^end_itlist(fun s t -> s^";\n "^t) rstr ^ - (if j > max_size then "\n ...]" else "]");; - let string_of_vname (v:vname): string = (v: string);; -let rec string_of_term t = - match t with - Opp t1 -> "(- " ^ string_of_term t1 ^ ")" -| Add (t1, t2) -> - "(" ^ (string_of_term t1) ^ " + " ^ (string_of_term t2) ^ ")" -| Sub (t1, t2) -> - "(" ^ (string_of_term t1) ^ " - " ^ (string_of_term t2) ^ ")" -| Mul (t1, t2) -> - "(" ^ (string_of_term t1) ^ " * " ^ (string_of_term t2) ^ ")" -| Inv t1 -> "(/ " ^ string_of_term t1 ^ ")" -| Div (t1, t2) -> - "(" ^ (string_of_term t1) ^ " / " ^ (string_of_term t2) ^ ")" -| Pow (t1, n1) -> - "(" ^ (string_of_term t1) ^ " ^ " ^ (string_of_int n1) ^ ")" -| Zero -> "0" -| Var v -> "x" ^ (string_of_vname v) -| Const x -> string_of_num x;; - - let string_of_varpow x k = if k = 1 then string_of_vname x else string_of_vname x^"^"^string_of_int k;; @@ -363,6 +265,7 @@ let string_of_poly (p:poly) = (* Printers. *) (* ------------------------------------------------------------------------- *) +(* let print_vector v = Format.print_string(string_of_vector 0 20 v);; let print_matrix m = Format.print_string(string_of_matrix 20 m);; @@ -371,7 +274,6 @@ let print_monomial m = Format.print_string(string_of_monomial m);; let print_poly m = Format.print_string(string_of_poly m);; -(* #install_printer print_vector;; #install_printer print_matrix;; #install_printer print_monomial;; @@ -411,19 +313,6 @@ let sdpa_of_vector (v:vector) = end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; (* ------------------------------------------------------------------------- *) -(* String for block diagonal matrix numbered k. *) -(* ------------------------------------------------------------------------- *) - -let sdpa_of_blockdiagonal k m = - let pfx = string_of_int k ^" " in - let ents = - foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in - let entss = sort (increasing fst) ents in - itlist (fun ((b,i,j),c) a -> - pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ - " " ^ decimalize 20 c ^ "\n" ^ a) entss "";; - -(* ------------------------------------------------------------------------- *) (* String for a matrix numbered k, in SDPA sparse format. *) (* ------------------------------------------------------------------------- *) @@ -466,6 +355,7 @@ let token s = >> (fun ((_,t),_) -> t);; let decimal = + let (||) = parser_or in let numeral = some isnum in let decimalint = atleast 1 numeral >> ((o) Num.num_of_string implode) in let decimalfrac = atleast 1 numeral @@ -485,13 +375,12 @@ let mkparser p s = let x,rst = p(explode s) in if rst = [] then x else failwith "mkparser: unparsed input";; -let parse_decimal = mkparser decimal;; - (* ------------------------------------------------------------------------- *) (* Parse back a vector. *) (* ------------------------------------------------------------------------- *) -let parse_sdpaoutput,parse_csdpoutput = +let _parse_sdpaoutput, parse_csdpoutput = + let (||) = parser_or in let vector = token "{" ++ listof decimal (token ",") "decimal" ++ token "}" >> (fun ((_,v),_) -> vector_of_list v) in @@ -508,23 +397,10 @@ let parse_sdpaoutput,parse_csdpoutput = mkparser sdpaoutput,mkparser csdpoutput;; (* ------------------------------------------------------------------------- *) -(* Also parse the SDPA output to test success (CSDP yields a return code). *) -(* ------------------------------------------------------------------------- *) - -let sdpa_run_succeeded = - let rec skipupto dscr prs inp = - (dscr ++ prs >> snd - || some (fun c -> true) ++ skipupto dscr prs >> snd) inp in - let prs = skipupto (word "phase.value" ++ token "=") - (possibly (a "p") ++ possibly (a "d") ++ - (word "OPT" || word "FEAS")) in - fun s -> try ignore (prs (explode s)); true with Noparse -> false;; - -(* ------------------------------------------------------------------------- *) (* The default parameters. Unfortunately this goes to a fixed file. *) (* ------------------------------------------------------------------------- *) -let sdpa_default_parameters = +let _sdpa_default_parameters = "100 unsigned int maxIteration;\ \n1.0E-7 double 0.0 < epsilonStar;\ \n1.0E2 double 0.0 < lambdaStar;\ @@ -555,7 +431,7 @@ let sdpa_alt_parameters = \n1.0E-7 double 0.0 < epsilonDash;\ \n";; -let sdpa_params = sdpa_alt_parameters;; +let _sdpa_params = sdpa_alt_parameters;; (* ------------------------------------------------------------------------- *) (* CSDP parameters; so far I'm sticking with the defaults. *) @@ -588,10 +464,10 @@ let run_csdp dbg obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_problem "" obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -600,16 +476,6 @@ let run_csdp dbg obj mats = else (Sys.remove input_file; Sys.remove output_file)); rv,res);; -let csdp obj mats = - let rv,res = run_csdp (!debugging) obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" - else if rv = 3 then () - (* Format.print_string "csdp warning: Reduced accuracy"; - Format.print_newline() *) - else if rv <> 0 then failwith("csdp: error "^string_of_int rv) - else ()); - res;; - (* ------------------------------------------------------------------------- *) (* Try some apparently sensible scaling first. Note that this is purely to *) (* get a cleaner translation to floating-point, and doesn't affect any of *) @@ -653,21 +519,7 @@ let linear_program_basic a = let mats = List.map (fun j -> diagonal (column j a)) (1--n) and obj = vector_const (Int 1) m in let rv,res = run_csdp false obj mats in - if rv = 1 or rv = 2 then false - else if rv = 0 then true - else failwith "linear_program: An error occurred in the SDP solver";; - -(* ------------------------------------------------------------------------- *) -(* Alternative interface testing A x >= b for matrix A, vector b. *) -(* ------------------------------------------------------------------------- *) - -let linear_program a b = - let m,n = dimensions a in - if dim b <> m then failwith "linear_program: incompatible dimensions" else - let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n) - and obj = vector_const (Int 1) m in - let rv,res = run_csdp false obj mats in - if rv = 1 or rv = 2 then false + if rv = 1 || rv = 2 then false else if rv = 0 then true else failwith "linear_program: An error occurred in the SDP solver";; @@ -716,40 +568,6 @@ let equation_eval assig eq = foldl (fun a v c -> a +/ value(v) */ c) (Int 0) eq;; (* ------------------------------------------------------------------------- *) -(* Eliminate among linear equations: return unconstrained variables and *) -(* assignments for the others in terms of them. We give one pseudo-variable *) -(* "one" that's used for a constant term. *) -(* ------------------------------------------------------------------------- *) - -let failstore = ref [];; - -let eliminate_equations = - let rec extract_first p l = - match l with - [] -> failwith "extract_first" - | h::t -> if p(h) then h,t else - let k,s = extract_first p t in - k,h::s in - let rec eliminate vars dun eqs = - match vars with - [] -> if forall is_undefined eqs then dun - else (failstore := [vars,dun,eqs]; raise Unsolvable) - | v::vs -> - try let eq,oeqs = extract_first (fun e -> defined e v) eqs in - let a = apply eq v in - let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in - let elim e = - let b = tryapplyd e v (Int 0) in - if b =/ Int 0 then e else - equation_add e (equation_cmul (minus_num b // a) eq) in - eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) - with Failure _ -> eliminate vs dun eqs in - fun one vars eqs -> - let assig = eliminate vars undefined eqs in - let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in - setify vs,assig;; - -(* ------------------------------------------------------------------------- *) (* Eliminate all variables, in an essentially arbitrary order. *) (* ------------------------------------------------------------------------- *) @@ -780,18 +598,6 @@ let eliminate_all_equations one = setify vs,assig;; (* ------------------------------------------------------------------------- *) -(* Solve equations by assigning arbitrary numbers. *) -(* ------------------------------------------------------------------------- *) - -let solve_equations one eqs = - let vars,assigs = eliminate_all_equations one eqs in - let vfn = itlist (fun v -> (v |-> Int 0)) vars (one |=> Int(-1)) in - let ass = - combine (+/) (fun c -> false) (mapf (equation_eval vfn) assigs) vfn in - if forall (fun e -> equation_eval ass e =/ Int 0) eqs - then undefine one ass else raise Sanity;; - -(* ------------------------------------------------------------------------- *) (* Hence produce the "relevant" monomials: those whose squares lie in the *) (* Newton polytope of the monomials in the input. (This is enough according *) (* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal, *) @@ -898,19 +704,6 @@ let epoly_pmul p q acc = a q) acc p;; (* ------------------------------------------------------------------------- *) -(* Usual operations on equation-parametrized poly. *) -(* ------------------------------------------------------------------------- *) - -let epoly_cmul c l = - if c =/ Int 0 then undefined else mapf (equation_cmul c) l;; - -let epoly_neg = epoly_cmul (Int(-1));; - -let epoly_add = combine equation_add is_undefined;; - -let epoly_sub p q = epoly_add p (epoly_neg q);; - -(* ------------------------------------------------------------------------- *) (* Convert regular polynomial. Note that we treat (0,0,0) as -1. *) (* ------------------------------------------------------------------------- *) @@ -953,11 +746,11 @@ let run_csdp dbg nblocks blocksizes obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_blockproblem "" nblocks blocksizes obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -968,7 +761,7 @@ let run_csdp dbg nblocks blocksizes obj mats = let csdp nblocks blocksizes obj mats = let rv,res = run_csdp (!debugging) nblocks blocksizes obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" + (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () (*Format.print_string "csdp warning: Reduced accuracy"; Format.print_newline() *) @@ -988,8 +781,6 @@ let bmatrix_cmul c bm = let bmatrix_neg = bmatrix_cmul (Int(-1));; -let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);; - (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) (* ------------------------------------------------------------------------- *) @@ -1102,15 +893,6 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = cfs,List.map (fun (a,b) -> snd a,b) msq;; (* ------------------------------------------------------------------------- *) -(* Iterative deepening. *) -(* ------------------------------------------------------------------------- *) - -let rec deepen f n = - try print_string "Searching with depth limit "; - print_int n; print_newline(); f n - with Failure _ -> deepen f (n + 1);; - -(* ------------------------------------------------------------------------- *) (* The ordering so we can create canonical HOL polynomials. *) (* ------------------------------------------------------------------------- *) @@ -1136,10 +918,6 @@ let monomial_order = if deg1 < deg2 then false else if deg1 > deg2 then true else lexorder mon1 mon2;; -let dest_poly p = - List.map (fun (m,c) -> c,dest_monomial m) - (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));; - (* ------------------------------------------------------------------------- *) (* Map back polynomials and their composites to HOL. *) (* ------------------------------------------------------------------------- *) @@ -1373,9 +1151,6 @@ let rec allpermutations l = itlist (fun h acc -> List.map (fun t -> h::t) (allpermutations (subtract l [h])) @ acc) l [];; -let allvarorders l = - List.map (fun vlis x -> index x vlis) (allpermutations l);; - let changevariables_monomial zoln (m:monomial) = foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;; @@ -1392,15 +1167,6 @@ let sdpa_of_vector (v:vector) = let strs = List.map (o (decimalize 20) (element v)) (1--n) in end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; -let sdpa_of_blockdiagonal k m = - let pfx = string_of_int k ^" " in - let ents = - foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in - let entss = sort (increasing fst) ents in - itlist (fun ((b,i,j),c) a -> - pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ - " " ^ decimalize 20 c ^ "\n" ^ a) entss "";; - let sdpa_of_matrix k (m:matrix) = let pfx = string_of_int k ^ " 1 " in let ms = foldr (fun (i,j) c a -> if i > j then a else ((i,j),c)::a) @@ -1425,10 +1191,10 @@ let run_csdp dbg obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_problem "" obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -1439,7 +1205,7 @@ let run_csdp dbg obj mats = let csdp obj mats = let rv,res = run_csdp (!debugging) obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" + (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () (* (Format.print_string "csdp warning: Reduced accuracy"; Format.print_newline()) *) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index f54914f252..6b8b820ac6 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -525,7 +525,7 @@ let isspace,issep,isbra,issymb,isalpha,isnum,isalnum = and isalnum c = Array.get ctable (charcode c) >= 16 in isspace,issep,isbra,issymb,isalpha,isnum,isalnum;; -let (||) parser1 parser2 input = +let parser_or parser1 parser2 input = try parser1 input with Noparse -> parser2 input;; @@ -571,7 +571,7 @@ let finished input = (* ------------------------------------------------------------------------- *) -let temp_path = ref Filename.temp_dir_name;; +let temp_path = Filename.get_temp_dir_name ();; (* ------------------------------------------------------------------------- *) (* Convenient conversion between files and (lists of) strings. *) diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index b11d15e5ca..403f664e2b 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -462,6 +462,11 @@ try (try apply Rsth; exact Rplus_opp_r. Defined. +Class can_compute_Z (z : Z) := dummy_can_compute_Z : True. +Hint Extern 0 (can_compute_Z ?v) => + match isZcst v with true => exact I end : typeclass_instances. +Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z). + Lemma R_one_zero: 1%R <> 0%R. discrR. Qed. diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index b1ff59e780..a120d4efb2 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -153,7 +153,6 @@ module Make (P:Polynom.S) = struct type coef = P.t let coef0 = P.of_num (Num.Int 0) let coef1 = P.of_num (Num.Int 1) - let coefm1 = P.of_num (Num.Int (-1)) let string_of_coef c = "["^(P.to_string c)^"]" (*********************************************************************** @@ -197,8 +196,6 @@ module Hashpol = Hashtbl.Make( (* A pretty printer for polynomials, with Maple-like syntax. *) -open Format - let getvar lv i = try (List.nth lv i) with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv) @@ -252,59 +249,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef in (stringP p true) - - -let print_pol zeroP hdP tlP coefterm monterm string_of_coef - dimmon string_of_exp lvar p = - - let rec print_mon m coefone = - let s=ref [] in - for i=1 to (dimmon m) do - (match (string_of_exp m i) with - "0" -> () - | "1" -> s:= (!s) @ [(getvar lvar (i-1))] - | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]); - done; - (match !s with - [] -> if coefone - then print_string "1" - else () - | l -> if coefone - then print_string (String.concat "*" l) - else (print_string "*"; - print_string (String.concat "*" l))) - and print_term t start = let a = coefterm t and m = monterm t in - match (string_of_coef a) with - "0" -> () - | "1" ->(match start with - true -> print_mon m true - |false -> (print_string "+ "; - print_mon m true)) - | "-1" ->(print_string "-";print_space();print_mon m true) - | c -> if (String.get c 0)='-' - then (print_string "- "; - print_string (String.sub c 1 - ((String.length c)-1)); - print_mon m false) - else (match start with - true -> (print_string c;print_mon m false) - |false -> (print_string "+ "; - print_string c;print_mon m false)) - and printP p start = - if (zeroP p) - then (if start - then print_string("0") - else ()) - else (print_term (hdP p) start; - if start then open_hovbox 0; - print_space(); - print_cut(); - printP (tlP p) false) - in open_hovbox 3; - printP p true; - print_flush() - - let stringP metadata (p : poly) = string_of_pol (fun p -> match p with [] -> true | _ -> false) @@ -595,9 +539,6 @@ let addS x l = l @ [x] (* oblige de mettre en queue sinon le certificat decon critical pairs/s-polynomials *) -let ordcpair ((i1,j1),m1) ((i2,j2),m2) = - compare_mon m1 m2 - module CPair = struct type t = (int * int) * Monomial.t diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index db8f3e4b21..632b9dac14 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -22,7 +22,6 @@ open Utile let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2 -and num_10 = Int 10 let numdom r = let r' = Ratio.normalize_ratio (ratio_of_num r) in @@ -35,7 +34,6 @@ module BigInt = struct type t = big_int let of_int = big_int_of_int let coef0 = of_int 0 - let coef1 = of_int 1 let of_num = Num.big_int_of_num let to_num = Num.num_of_big_int let equal = eq_big_int @@ -49,7 +47,6 @@ module BigInt = struct let div = div_big_int let modulo = mod_big_int let to_string = string_of_big_int - let to_int x = int_of_big_int x let hash x = try (int_of_big_int x) with Failure _ -> 1 @@ -61,15 +58,6 @@ module BigInt = struct then a else if lt a b then pgcd b a else pgcd b (modulo a b) - - (* signe du pgcd = signe(a)*signe(b) si non nuls. *) - let pgcd2 a b = - if equal a coef0 then b - else if equal b coef0 then a - else let c = pgcd (abs a) (abs b) in - if ((lt coef0 a)&&(lt b coef0)) - ||((lt coef0 b)&&(lt a coef0)) - then opp c else c end (* @@ -146,8 +134,6 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let unconstr = mkRel 1 - let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") @@ -271,20 +257,6 @@ let set_nvars_term nvars t = | Pow (t1,n) -> aux t1 nvars in aux t nvars -let string_of_term p = - let rec aux p = - match p with - | Zero -> "0" - | Const r -> string_of_num r - | Var v -> "x"^v - | Opp t1 -> "(-"^(aux t1)^")" - | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")" - | Sub (t1,t2) -> "("^(aux t1)^"-"^(aux t2)^")" - | Mul (t1,t2) -> "("^(aux t1)^"*"^(aux t2)^")" - | Pow (t1,n) -> (aux t1)^"^"^(string_of_int n) - in aux p - - (*********************************************************************** Coefficients: recursive polynomials *) @@ -437,7 +409,7 @@ open Ideal that has the same size than lp and where true indicates an element that has been removed *) -let rec clean_pol lp = +let clean_pol lp = let t = Hashpol.create 12 in let find p = try Hashpol.find t p with diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 7780de7127..92b092ffe9 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -19,8 +19,8 @@ open Names open Nameops open Term open EConstr -open Tacticals -open Tacmach +open Tacticals.New +open Tacmach.New open Tactics open Logic open Libnames @@ -41,7 +41,9 @@ let elim_id id = Proofview.Goal.enter { enter = begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) end } -let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl +let resolve_id id = Proofview.Goal.enter { enter = begin fun gl -> + apply (Tacmach.New.pf_global id gl) +end } let timing timer_name f arg = f arg @@ -146,14 +148,14 @@ let intern_id,unintern_id,reset_intern_tables = Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), (fun () -> cpt := 0; Hashtbl.clear table) -let mk_then = tclTHENLIST +let mk_then tacs = tclTHENLIST tacs let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t let elim t = simplest_elim t -let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] +let pf_nf gl c = pf_apply Tacred.simpl gl c let rev_assoc k = let rec loop = function @@ -580,9 +582,12 @@ let abstract_path sigma typ path t = let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur -let focused_simpl path gl = +let focused_simpl path = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl + convert_concl_no_check newc DEFAULTcast + end } let focused_simpl path = focused_simpl path @@ -640,11 +645,19 @@ let decompile af = in loop af.body -let mkNewMeta () = mkMeta (Evarutil.new_meta()) +(** Backward compat to emulate the old Refine: normalize the goal conclusion *) +let new_hole env sigma c = + let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in + Evarutil.new_evar env sigma c -let clever_rewrite_base_poly typ p result theorem gl = +let clever_rewrite_base_poly typ p result theorem = + let open Tacmach.New in + let open Sigma in + Proofview.Goal.nf_enter { enter = begin fun gl -> let full = pf_concl gl in + let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in + Refine.refine { run = begin fun sigma -> let t = applist (mkLambda @@ -657,13 +670,17 @@ let clever_rewrite_base_poly typ p result theorem gl = [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), [abstracted]) in - exact (applist(t,[mkNewMeta()])) gl + let argt = mkApp (abstracted, [|result|]) in + let Sigma (hole, sigma, p) = new_hole env sigma argt in + Sigma (applist (t, [hole]), sigma, p) + end } + end } -let clever_rewrite_base p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl +let clever_rewrite_base p result theorem = + clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem -let clever_rewrite_base_nat p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl +let clever_rewrite_base_nat p result theorem = + clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem let clever_rewrite_gen p result (t,args) = let theorem = applist(t, args) in @@ -673,12 +690,29 @@ let clever_rewrite_gen_nat p result (t,args) = let theorem = applist(t, args) in clever_rewrite_base_nat p result theorem -let clever_rewrite p vpath t gl = +(** Solve using the term the term [t _] *) +let refine_app gl t = + let open Tacmach.New in + let open Sigma in + Refine.refine { run = begin fun sigma -> + let env = pf_env gl in + let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with + | Prod (_, t, _) -> t + | _ -> assert false + in + let Sigma (hole, sigma, p) = new_hole env sigma ht in + Sigma (applist (t, [hole]), sigma, p) + end } + +let clever_rewrite p vpath t = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> let full = pf_concl gl in let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in - exact (applist(t',[mkNewMeta()])) gl + refine_app gl t' + end } let rec shuffle p (t1,t2) = match t1,t2 with @@ -942,15 +976,15 @@ let rec transform sigma p t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t + unfold sp_Zminus :: tac,t | Kapp(Zsucc,[t1]) -> let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in - Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t + unfold sp_Zsucc :: tac,t | Kapp(Zpred,[t1]) -> let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in - Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t + unfold sp_Zpred :: tac,t | Kapp(Zmult,[t1;t2]) -> let tac1,t1' = transform sigma (P_APP 1 :: p) t1 and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in @@ -1068,7 +1102,7 @@ let replay_history tactic_normalisation = | HYP e :: l -> begin try - Tacticals.New.tclTHEN + tclTHEN (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end @@ -1080,16 +1114,16 @@ let replay_history tactic_normalisation = let k = if b then negone else one in let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; mkVar id1; mkVar id2 |])]; - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1104,8 +1138,8 @@ let replay_history tactic_normalisation = Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + tclTHENS + (tclTHENLIST [ unfold sp_Zle; simpl_in_concl; intro; @@ -1118,7 +1152,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le) + Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> let id = hyp_of_tag e1.id in let eq1 = val_of(decompile e1) @@ -1128,10 +1162,10 @@ let replay_history tactic_normalisation = let rhs = mk_plus (mk_times eq2 kk) dd in let state_eg = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eg) - [ Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + [ tclTHENS + (tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA1, @@ -1139,9 +1173,9 @@ let replay_history tactic_normalisation = (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) - [ Tacticals.New.tclTHENS + [ tclTHENS (cut (mk_gt kk izero)) - [ Tacticals.New.tclTHENLIST [ + [ tclTHENLIST [ (intros_using [aux1; aux2]); (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, @@ -1149,13 +1183,13 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in @@ -1166,10 +1200,10 @@ let replay_history tactic_normalisation = let kk = mk_integer k and dd = mk_integer d in let tac = scalar_norm_add [P_APP 2] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt dd izero)) - [ Tacticals.New.tclTHENS (cut (mk_gt kk dd)) - [Tacticals.New.tclTHENLIST [ + [ tclTHENS (cut (mk_gt kk dd)) + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA4, @@ -1177,14 +1211,14 @@ let replay_history tactic_normalisation = (clear [aux1;aux2]); unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); - Proofview.V82.tactic (mk_then tac); + resolve_id aux; + mk_then tac; assumption ] ; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] @@ -1197,9 +1231,9 @@ let replay_history tactic_normalisation = let state_eq = mk_eq eq1 (mk_times eq2 kk) in if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eq) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA18, @@ -1207,14 +1241,14 @@ let replay_history tactic_normalisation = (clear [aux1;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS (cut state_eq) + tclTHENS (cut state_eq) [ - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA3, @@ -1222,11 +1256,11 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1239,16 +1273,16 @@ let replay_history tactic_normalisation = (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: scalar_norm [P_APP 3] e1.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_eq eq1 (mk_inv eq2))) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity] + tclTHEN (mk_then tac) reflexivity] | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> let id = new_identifier () @@ -1272,9 +1306,9 @@ let replay_history tactic_normalisation = [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in - Tacticals.New.tclTHENS + tclTHENS (cut theorem) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (elim_id aux); (clear [aux]); @@ -1282,11 +1316,11 @@ let replay_history tactic_normalisation = (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (clear [aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1295,10 +1329,10 @@ let replay_history tactic_normalisation = let tac1 = norm_add [P_APP 2;P_TYPE] e.body in let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in - Tacticals.New.tclTHENS + tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ]; - Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]] + [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ]; + tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1317,10 +1351,10 @@ let replay_history tactic_normalisation = let p_initial = if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ] @@ -1329,10 +1363,10 @@ let replay_history tactic_normalisation = and kk2 = mk_integer k2 in let p_initial = [P_APP 2;P_TYPE] in let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - Tacticals.New.tclTHENS (cut (mk_gt kk1 izero)) - [Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk1 izero)) + [tclTHENS (cut (mk_gt kk2 izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| @@ -1340,29 +1374,29 @@ let replay_history tactic_normalisation = mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); (clear [aux1;aux2]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl + tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity + tclTHEN (resolve_id (hyp_of_tag e)) reflexivity | CONSTANT_NEG(e,k) :: l -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkVar (hyp_of_tag e)]); unfold sp_Zle; simpl_in_concl; unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | _ -> Proofview.tclUNIT () @@ -1380,12 +1414,12 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = let (tac,t') = normalize sigma p_initial t in let shift_left = tclTHEN - (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])) - (tclTRY (Proofview.V82.of_tactic (clear [id]))) + (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) + (tclTRY (clear [id])) in if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ])) + ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) else @@ -1430,7 +1464,7 @@ let destructure_omega gl tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id) + tclTHEN (tclTRY (clear [id])) (intro_using id) open Proofview.Notations @@ -1449,7 +1483,7 @@ let coq_omega = let id = new_identifier () in let i = new_id () in tag_hypothesis id i; - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); @@ -1460,7 +1494,7 @@ let coq_omega = body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), @@ -1476,13 +1510,13 @@ let coq_omega = with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)) + (tclTHEN prelude (replay_history tactic_normalisation path)) end else begin try let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; - Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") + tclTHEN prelude (replay_history tactic_normalisation path) + with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") end end } @@ -1495,36 +1529,36 @@ let nat_inject = Proofview.tclEVARMAP >>= fun sigma -> try match destructurate_term sigma t with | Kapp(Plus,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_plus),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Mult,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_mult),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Minus,[t1;t2]) -> let id = new_identifier () in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHEN + tclTHENS + (tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p + tclTHENLIST [ + (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ]; - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))) + (tclTHEN + (clever_rewrite_gen p (mk_integer zero) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp(S,[t']) -> @@ -1538,24 +1572,24 @@ let nat_inject = let rec loop p t : unit Proofview.tactic = try match destructurate_term sigma t with Kapp(S,[t]) -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p + (tclTHEN + (clever_rewrite_gen p (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t]))) + ((Lazy.force coq_inj_S),[t])) (loop (P_APP 1 :: p) t)) | _ -> explore p t with e when catchable_exception e -> explore p t in - if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t + if is_number t' then focused_simpl p else loop p t | Kapp(Pred,[t]) -> let t_minus_one = mkApp (Lazy.force coq_minus, [| t; mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t]))) + tclTHEN + (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + ((Lazy.force coq_pred_of_minus),[t])) (explore p t_minus_one) - | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p) + | Kapp(O,[]) -> focused_simpl p | _ -> Proofview.tclUNIT () with e when catchable_exception e -> Proofview.tclUNIT () @@ -1565,7 +1599,7 @@ let nat_inject = Proofview.tclEVARMAP >>= fun sigma -> begin try match destructurate_prop sigma t with Kapp(Le,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1574,7 +1608,7 @@ let nat_inject = (loop lit) ] | Kapp(Lt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1583,7 +1617,7 @@ let nat_inject = (loop lit) ] | Kapp(Ge,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1592,7 +1626,7 @@ let nat_inject = (loop lit) ] | Kapp(Gt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1601,7 +1635,7 @@ let nat_inject = (loop lit) ] | Kapp(Neq,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1611,7 +1645,7 @@ let nat_inject = ] | Kapp(Eq,[typ;t1;t2]) -> if is_conv typ (Lazy.force coq_nat) then - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); @@ -1697,20 +1731,20 @@ let fresh_id avoid id gl = let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.enter { enter = begin fun gl -> + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id = fresh_id [] id gl in - Tacticals.New.tclTHEN (introduction id) (tac id) + tclTHEN (introduction id) (tac id) end }) let onClearedName2 id tac = - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.enter { enter = begin fun gl -> + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id1 = fresh_id [] (add_suffix id "_left") gl in let id2 = fresh_id [] (add_suffix id "_right") gl in - Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] + tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end }) let rec is_Prop sigma c = match EConstr.kind sigma c with @@ -1724,7 +1758,7 @@ let destructure_hyps = let decidability = decidability gl in let pf_nf = pf_nf gl in let rec loop = function - | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) + | [] -> (tclTHEN nat_inject coq_omega) | decl::lit -> let i = NamedDecl.get_id decl in Proofview.tclEVARMAP >>= fun sigma -> @@ -1732,17 +1766,17 @@ let destructure_hyps = | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> - (Tacticals.New.tclTHENS + (tclTHENS (elim_id i) [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) @@ -1752,7 +1786,7 @@ let destructure_hyps = if is_Prop sigma (type_of t2) then let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> @@ -1763,7 +1797,7 @@ let destructure_hyps = | Kapp(Not,[t]) -> begin match destructurate_prop sigma t with Kapp(Or,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> @@ -1771,7 +1805,7 @@ let destructure_hyps = ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); @@ -1781,7 +1815,7 @@ let destructure_hyps = | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in let d2 = decidability t2 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); @@ -1793,7 +1827,7 @@ let destructure_hyps = (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. For t1, being decidable implies being Prop. *) let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); @@ -1802,7 +1836,7 @@ let destructure_hyps = ] | Kapp(Not,[t]) -> let d = decidability t in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) @@ -1810,7 +1844,7 @@ let destructure_hyps = | Kapp(op,[t1;t2]) -> (try let thm = not_binop op in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); (onClearedName i (fun _ -> loop lit)) @@ -1820,14 +1854,14 @@ let destructure_hyps = if !old_style_flag then begin match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); @@ -1837,12 +1871,12 @@ let destructure_hyps = end else begin match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> - (Tacticals.New.tclTHEN + (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> - (Tacticals.New.tclTHEN + (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) @@ -1870,23 +1904,24 @@ let destructure_goal = Proofview.V82.wrap_exceptions prop >>= fun prop -> match prop with | Kapp(Not,[t]) -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (unfold sp_not) intro) + (tclTHEN + (tclTHEN (unfold sp_not) intro) destructure_hyps) - | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) + | Kimp(a,b) -> (tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> let goal_tac = try let dec = decidability t in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tacmach.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) + tclTHEN + (Proofview.Goal.nf_enter { enter = begin fun gl -> + refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) + end }) intro with Undecidable -> Tactics.elim_type (Lazy.force coq_False) | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in - Tacticals.New.tclTHEN goal_tac destructure_hyps + tclTHEN goal_tac destructure_hyps in (loop concl) end } diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index bd991a955c..334b03de1d 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b) let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let e = original.body in let sigma = new_var_id () in + if e == [] then begin + display_system print_var [original] ; failwith "TL" + end; let smallest,var = - try - List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) - (abs (List.hd e).c, (List.hd e).v) (List.tl e) - with Failure "tl" -> display_system print_var [original] ; failwith "TL" in + List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) + (abs (List.hd e).c, (List.hd e).v) (List.tl e) + in let m = smallest + one in let new_eq = { constant = omega_mod original.constant m; diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fc9d70ae7d..c649cfb2c6 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -8,7 +8,7 @@ (* The `Quote' tactic *) -(* The basic idea is to automatize the inversion of interpetation functions +(* The basic idea is to automatize the inversion of interpretation functions in 2-level approach Examples are given in \texttt{theories/DEMOS/DemoQuote.v} diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5c68078d7d..8d7ae51fc0 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -285,7 +285,7 @@ module type Int = sig val mk : Bigint.bigint -> Term.constr val parse_term : Term.constr -> parse_term - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* check whether t is built only with numbers and + * - *) val is_scalar : Term.constr -> bool end @@ -350,10 +350,12 @@ let parse_term t = | _ -> Tother with e when Logic.catchable_exception e -> Tother +let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c + let parse_rel gl t = try match destructurate t with | Kapp("eq",[typ;t1;t2]) - when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) + when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index af50ea0fff..ee7ff451a9 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -168,7 +168,7 @@ module type Int = (* parsing a term (one level, except if a number is found) *) val parse_term : Term.constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) val is_scalar : Term.constr -> bool end diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 9a54ad7789..df7e5cb99e 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -38,7 +38,7 @@ let romega_tactic l = we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) (Tactics.intros) - (Proofview.V82.tactic total_reflexive_omega_tactic)) + (total_reflexive_omega_tactic)) TACTIC EXTEND romega diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index cfe14b230c..a20589fb46 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Proofview.Notations open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -16,13 +17,12 @@ open OmegaSolver (* Especially useful debugging functions *) let debug = ref false -let show_goal gl = - if !debug then (); Tacticals.tclIDTAC gl +let show_goal = Tacticals.New.tclIDTAC let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) -let (>>) = Tacticals.tclTHEN +let (>>) = Tacticals.New.tclTHEN let mkApp = Term.mkApp @@ -739,7 +739,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = - let concl = Tacmach.pf_concl gl in + let concl = Tacmach.New.pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in @@ -760,7 +760,7 @@ let reify_gl env gl = | [] -> if !debug then print_env_reification env; [] in - let t_lhyps = loop (Tacmach.pf_hyps_types gl) in + let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in (id_concl,t_concl) :: t_lhyps let rec destructurate_pos_hyp orig list_equations list_depends = function @@ -1283,21 +1283,22 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Proofview.V82.of_tactic (Tactics.generalize - (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >> - Proofview.V82.of_tactic (Tactics.change_concl reified) >> - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >> + Tactics.generalize + (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >> + Tactics.change_concl reified >> + Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> + Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I))) + Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) -let total_reflexive_omega_tactic gl = +let total_reflexive_omega_tactic = + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); @@ -1306,9 +1307,9 @@ let total_reflexive_omega_tactic gl = let full_reified_goal = reify_gl env gl in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env full_reified_goal systems_list gl + resolution env full_reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" - + end } (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 2b64204c93..e20e78b1a7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -19,7 +19,6 @@ open Environ open Libnames open Globnames open Glob_term -open Tacticals open Tacexpr open Coqlib open Mod_subst @@ -279,8 +278,6 @@ let my_constant c = let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) -let new_ring_path = - DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = @@ -336,12 +333,12 @@ let _ = add_map "ring" my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -783,20 +780,20 @@ let _ = add_map "field" (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", - (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); + (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot); my_reference "display_pow_linear", (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot); - (* FEeval: evaluate morphism, protect field + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot); + (* FEeval: evaluate polynomial, protect field operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_without_eq diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 4367d021c0..d9d32c681d 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -7,13 +7,10 @@ (************************************************************************) open Names -open Constr open EConstr open Libnames open Globnames open Constrexpr -open Tacexpr -open Proof_type open Newring_ast val protect_tac_in : string -> Id.t -> unit Proofview.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 9a0dfbf1ca..8be060e197 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -21,30 +21,21 @@ open Pp open Pcoq open Genarg open Stdarg -open Tacarg open Term open Vars -open Topconstr open Libnames open Tactics open Tacticals open Termops -open Namegen open Recordops open Tacmach -open Coqlib open Glob_term open Util open Evd -open Extend -open Goptions open Tacexpr -open Proofview.Notations open Tacinterp open Pretyping open Constr -open Pltac -open Extraargs open Ppconstr open Printer @@ -54,14 +45,9 @@ open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops -open Notation_term -open Notation_ops -open Locus -open Locusops DECLARE PLUGIN "ssrmatching_plugin" -type loc = Loc.t let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info @@ -89,8 +75,6 @@ let pp s = !pp_ref s let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] -let get_index = function ArgArg i -> i | _ -> - CErrors.anomaly (str"Uninterpreted index") (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -303,8 +287,6 @@ let unif_EQ_args env sigma pa a = let unif_HO env ise p c = Evarconv.the_conv_x env p c ise -let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise - let unif_HO_args env ise0 pa i ca = let n = Array.length pa in let rec loop ise j = @@ -370,11 +352,6 @@ let unif_end env sigma0 ise0 pt ok = let s, uc', t = nf_open_term sigma0 ise2 t in s, Evd.union_evar_universe_context uc uc', t -let pf_unif_HO gl sigma pt p c = - let env = pf_env gl in - let ise = unif_HO env (create_evar_defs sigma) p c in - unif_end env (project gl) ise pt (fun _ -> true) - let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in @@ -439,16 +416,10 @@ let all_ok _ _ = true let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 -let isFixed c = match kind_of_term c with - | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true - | _ -> false - let isRigid c = match kind_of_term c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false -exception UndefPat - let hole_var = mkVar (id_of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = @@ -916,13 +887,6 @@ let pp_pattern (sigma, p) = let pr_cpattern = pr_term let pr_rpattern _ _ _ = pr_pattern -let pr_option f = function None -> mt() | Some x -> f x -let pr_ssrpattern _ _ _ = pr_option pr_pattern -let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]") -let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep -let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")") -let pr_ssrpattern_roundp _ _ _ = pr_pattern_roundp - let wit_rpatternty = add_genarg "rpatternty" pr_pattern let glob_ssrterm gs = function @@ -1044,7 +1008,6 @@ let interp_wit wit ist gl x = let arg = interp_genarg ist globarg in let (sigma, arg) = of_ftactic arg gl in sigma, Value.cast (topwit wit) arg -let interp_constr = interp_wit wit_constr let interp_open_constr ist gl gc = interp_wit wit_open_constr ist gl gc let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c @@ -1201,7 +1164,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn ?loc x (a,(g,c)) = match c with - | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ?loc) b)) + | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)) | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t @@ -1261,7 +1224,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in - let concl = find_T env0 concl0 1 do_subst in + let concl = find_T env0 concl0 1 ~k:do_subst in let _ = end_T () in concl | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> @@ -1273,11 +1236,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = (* we start from sigma, so hole is considered a rigid head *) let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in - let concl = find_T env0 concl0 1 (fun env c _ h -> + let concl = find_T env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h - (fun env _ -> do_subst env e_body))) in + ~k:(fun env _ -> do_subst env e_body))) in let _ = end_X () in let _ = end_T () in concl | Some (sigma, E_In_X_In_T (e, hole, p)) -> @@ -1289,11 +1252,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_X, end_X = mk_tpattern_matcher sigma noindex holep in let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in - let concl = find_T env0 concl0 1 (fun env c _ h -> + let concl = find_T env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> - find_E env e_body h do_subst))) in + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> + find_E env e_body h ~k:do_subst))) in let _ = end_E () in let _ = end_X () in let _ = end_T () in concl | Some (sigma, E_As_X_In_T (e, hole, p)) -> @@ -1306,10 +1269,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher sigma occ holep in - let concl = find_TE env0 concl0 1 (fun env c _ h -> + let concl = find_TE env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in @@ -1352,7 +1315,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in let find_U, end_U = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - let concl = find_U env concl h (fun _ _ _ -> mkRel) in + let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index a8862d2646..8be989de57 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -4,7 +4,6 @@ open Genarg open Tacexpr open Environ -open Tacmach open Evd open Proof_type open Term @@ -226,7 +225,6 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.variable option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.variable -> cpattern -val cpattern_of_id : Names.variable -> cpattern val pr_constr_pat : constr -> Pp.std_ppcmds val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma |