diff options
Diffstat (limited to 'plugins')
33 files changed, 379 insertions, 215 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0c305d09e8..c485c38009 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) | SymAx c -> @@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic = app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHEN injt (proof_tac prf)))) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = @@ -508,11 +506,9 @@ let f_equal = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = - try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match EConstr.kind sigma concl with diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index afc83b780b..0f96b9bbe8 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -259,7 +259,7 @@ let parse_ind_args si args relmax = let rec extract_type env sg db j c args = - match EConstr.kind sg (whd_betaiotazeta sg c) with + match EConstr.kind sg (whd_betaiotazeta env sg c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) @@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args = and extract_type_scheme env sg db c p = if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta sg c in + let c = whd_betaiotazeta env sg c in match EConstr.kind sg c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 834e4251d3..f13901c36d 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -57,12 +57,12 @@ let make_simple_atoms seq= | None->[] in {negative=seq.latoms;positive=ratoms} -let do_sequent sigma setref triv id seq i dom atoms= +let do_sequent env 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 sigma i dom t1 t2 with + match unif_atoms env sigma i dom t1 t2 with None->() | Some (Phantom _) ->phref:=true | Some c ->flag:=false;setref:=IS.add (c,id) !setref in @@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms= do_atoms atoms (make_simple_atoms seq); !flag && !phref -let match_one_quantified_hyp sigma setref seq lf= +let match_one_quantified_hyp env sigma setref seq lf= match lf.pat with Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent sigma setref triv lf.id seq i dom lf.atoms then + if do_sequent env 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 sigma lf seq= +let give_instances env sigma lf seq= let setref=ref IS.empty in - List.iter (match_one_quantified_hyp sigma setref seq) lf; + List.iter (match_one_quantified_hyp env sigma setref seq) lf; IS.elements !setref (* collector for the engine *) @@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq= let open EConstr in Proofview.Goal.enter begin fun gl -> let sigma = project gl in + let env = Proofview.Goal.env gl in match inst with Phantom dom-> - if lookup sigma (id,None) seq then + if lookup env sigma (id,None) seq then tclFAIL 0 (Pp.str "already done") else tclTHENS (cut dom) @@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq= tclTRY assumption] | Real((m,t),_)-> let c = (m, EConstr.to_constr sigma t) in - if lookup sigma (id,Some c) seq then + if lookup env sigma (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= @@ -205,7 +206,8 @@ let instance_tac inst= let quantified_tac lf backtrack continue seq = Proofview.Goal.enter begin fun gl -> - let insts=give_instances (project gl) lf seq in + let env = Proofview.Goal.env gl in + let insts=give_instances env (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) backtrack diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c0f4c78ff3..08c2c4d916 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -13,7 +13,7 @@ open Rules val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t -val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> +val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t -> (Unify.instance * GlobRef.t) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7bf13fd25b..3dd5059e5d 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup sigma item seq= +let lookup env sigma item seq= History.mem item seq.history || match item with (_,None)->false @@ -117,7 +117,7 @@ let lookup sigma item seq= let p (id2,o)= match o with None -> false - | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in + | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history let add_formula env sigma side nam t seq = diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 3a5da6ad14..bba89c823c 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -39,7 +39,7 @@ val deepen: t -> t val record: h_item -> t -> t -val lookup: Evd.evar_map -> h_item -> t -> bool +val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e58e80116d..9c3debe48f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -29,7 +29,7 @@ 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 evd t1 t2= +let unif env evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -46,8 +46,8 @@ let unif evd t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta evd t1) - and nt2=head_reduce (whd_betaiotazeta evd t2) in + let nt1=head_reduce (whd_betaiotazeta env evd t1) + and nt2=head_reduce (whd_betaiotazeta env evd t2) in match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then @@ -123,9 +123,9 @@ let mk_rel_inst evd t= in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms evd i dom t1 t2= +let unif_atoms env evd i dom t1 t2= try - let t=Int.List.assoc i (unif evd t1 t2) in + let t=Int.List.assoc i (unif env 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 @@ -136,11 +136,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 evd (m1,t1) (m2,t2)= +let more_general env 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 evd mt1 mt2 in + let sigma=unif env 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 71e786eb90..c6767f04ac 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -13,12 +13,12 @@ open EConstr exception UFAIL of constr*constr -val unif : Evd.evar_map -> constr -> constr -> (int*constr) list +val unif : Environ.env -> 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 : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option +val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option -val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool +val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f4200854c2..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) = refine to_refine g) ] let find_rectype env sigma c = - let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in + let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t, l) @@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type = let new_ctxt, new_end_of_type = decompose_prod_n_assum sigma ctxt_size new_type_of_hyp in - let prove_new_hyp : tactic = - tclTHEN - (tclDO ctxt_size (Proofview.V82.of_tactic intro)) - (fun g -> - let all_ids = pf_ids_of_hyps g in - let new_ids, _ = list_chop ctxt_size all_ids in - let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.type_of g to_refine in - tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g) + let prove_new_hyp = + let open Tacticals.New in + let open Tacmach.New in + tclTHEN (tclDO ctxt_size intro) + (Proofview.Goal.enter (fun g -> + let all_ids = pf_ids_of_hyps g in + let new_ids, _ = list_chop ctxt_size all_ids in + let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in + let evm, _ = + Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g) + to_refine + in + tclTHEN + (Proofview.Unsafe.tclEVARS evm) + (Proofview.V82.tactic (refine to_refine)))) in let simpl_eq_tac = change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp - prove_new_hyp + (Proofview.V82.of_tactic prove_new_hyp) in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) (* str "removing an equation " ++ fnl ()++ *) @@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = let prov_hid = pf_get_new_id hid g in let c = mkApp (mkVar hid, args) in let evm, _ = pf_apply Typing.type_of g c in - tclTHENLIST - [ Refiner.tclEVARS evm - ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c) - ; thin [hid] - ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ] + let open Tacticals.New in + Proofview.V82.of_tactic + (tclTHENLIST + [ Proofview.Unsafe.tclEVARS evm + ; pose_proof (Name prov_hid) c + ; clear [hid] + ; rename_hyp [(prov_hid, hid)] ]) g) (fun (* if not then we are in a mutual function block diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index c53dcc7edd..608155eb71 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac in (* uctx was ignored before *) - let hook = DeclareDef.Hook.make (hook new_principle_type) in + let hook = Declare.Hook.make (hook new_principle_type) in (body, typ, univs, hook, sigma) let change_property_sort evd toSort princ princName = @@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts let uctx = Evd.evar_universe_context sigma in let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = - DeclareDef.declare_entry ~name:new_princ_name ~hook - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + Declare.declare_entry ~name:new_princ_name ~hook + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] ~uctx entry in @@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl = Pp.(str "Body of Function must be given") in ComDefinition.do_definition ~name:fname.CAst.v ~poly:false - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl = (None, evd, List.rev rev_pconstants) | _ -> ComFixpoint.do_fixpoint - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd, rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e83fe56cc9..af53f16e1f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -2,7 +2,7 @@ open Names open Pp open Constr open Libnames -open Refiner +open Tacmach let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id) let mk_rel_id = mk_prefix "R_" @@ -395,7 +395,8 @@ let jmeq_refl () = with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = - tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l + Proofview.V82.of_tactic + (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l) let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -427,15 +428,16 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = - tclREPEAT - (List.fold_right - (fun (eq, b) i -> - tclORELSE - (Proofview.V82.of_tactic - ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) - i) - (if rev then List.rev eqs else eqs) - (tclFAIL 0 (mt ()))) + let open Tacticals in + (tclREPEAT + (List.fold_right + (fun (eq, b) i -> + tclORELSE + (Proofview.V82.of_tactic + ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) + i) + (if rev then List.rev eqs else eqs) + (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"]) let decompose_lam_n sigma n = if n < 0 then diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ffb9a7e69b..9b2d9c4815 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g = in continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g -let pf_type c tac gl = - let evars, ty = Typing.type_of (pf_env gl) (project gl) c in - tclTHEN (Refiner.tclEVARS evars) (tac ty) gl +let pf_type c tac = + let open Tacticals.New in + Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let evars, ty = Typing.type_of env sigma c in + tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty)) + +let pf_type c tac = + Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty))) let pf_typel l tac = let rec aux tys l = @@ -1483,7 +1490,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in + let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type in @@ -1721,7 +1728,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook {DeclareDef.Hook.S.uctx; _} = + let hook {Declare.Hook.S.uctx; _} = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref @@ -1767,5 +1774,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls functional_ref (EConstr.of_constr rec_arg_type) relation rec_arg_num term_id using_lemmas (List.length res_vars) evd - (DeclareDef.Hook.make hook)) + (Declare.Hook.make hook)) () diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 17a7121a3f..f867a47c08 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -14,10 +14,7 @@ open Constr open Context open CErrors open Evar_refiner -open Tacmach open Tacexpr -open Refiner -open Evd open Locus open Context.Named.Declaration open Ltac_pretype @@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration (* The instantiate tactic *) -let instantiate_evar evk (ist,rawc) env sigma = +let instantiate_evar evk (ist,rawc) = + let open Proofview.Notations in + Proofview.tclENV >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let evi = Evd.find sigma evk in let filtered = Evd.evar_filtered_env env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in @@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma = ltac_genargs = ist.Geninterp.lfun; } in let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in - tclEVARS sigma' + Proofview.Unsafe.tclEVARS sigma' + end let evar_list sigma c = let rec evrec acc c = @@ -47,14 +49,15 @@ let evar_list sigma c = evrec [] c let instantiate_tac n c ido = - Proofview.V82.tactic begin fun gl -> - let env = Global.env () in - let sigma = gl.sigma in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in let evl = match ido with - ConclLocation () -> evar_list sigma (pf_concl gl) + ConclLocation () -> evar_list sigma concl | HypLocation (id,hloc) -> - let decl = Environ.lookup_named id (pf_env gl) in + let decl = Environ.lookup_named id env in match hloc with InHyp -> (match decl with @@ -70,17 +73,16 @@ let instantiate_tac n c ido = user_err Pp.(str "Not enough uninstantiated existential variables."); if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in - instantiate_evar evk c env sigma gl + instantiate_evar evk c end let instantiate_tac_by_name id c = - Proofview.V82.tactic begin fun gl -> - let env = Global.env () in - let sigma = gl.sigma in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let evk = try Evd.evar_key id sigma with Not_found -> user_err Pp.(str "Unknown existential variable.") in - instantiate_evar evk c env sigma gl + instantiate_evar evk c end let let_evar name typ = diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index c4731e5c34..eb53fd45d0 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -31,6 +31,8 @@ let create_generic_quotation name e wit = let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string +let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global + let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr @@ -342,3 +344,55 @@ 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 + +{ + +(* Work around a limitation of the macro system *) +let strategy_level0 = Pcoq.Prim.strategy_level + +let pr_strategy _ _ _ v = Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy } +| [ strategy_level0(n) ] -> { n } +END + +{ + +let intern_strategy ist v = match v with +| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id) +| ArgArg v -> ArgArg v + +let subst_strategy _ v = v + +let interp_strategy ist gl = function +| ArgArg n -> gl.Evd.sigma, n +| ArgVar { CAst.v = id; CAst.loc } -> + let v = + try Id.Map.find id ist.lfun + with Not_found -> + CErrors.user_err ?loc + (str "Unbound variable " ++ Id.print id ++ str".") + in + let v = + try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v + with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level" + in + gl.Evd.sigma, v + +let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level_or_var + TYPED AS strategy_level + PRINTED BY { pr_strategy } + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { intern_strategy } + SUBSTITUTED BY { subst_strategy } + RAW_PRINTED BY { pr_loc_strategy } + GLOB_PRINTED BY { pr_loc_strategy } +| [ strategy_level(n) ] -> { ArgArg n } +| [ identref(id) ] -> { ArgVar id } +END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fbdb7c0032..e52bf55f71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -78,3 +78,7 @@ val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Id.t Locus.clause_expr) Genarg.genarg_type + +val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type + +val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0bad3cbe5b..ffb597d4cb 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP = TACTIC EXTEND optimize_heap | [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } END + +(** Tactic analogous to [Strategy] vernacular *) + +TACTIC EXTEND with_strategy +| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> { + with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac) +} +END diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0f0341f123..35c90444b1 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -54,16 +54,23 @@ END { +let pr_search_strategy_name _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" + | Some s -> pr_search_strategy_name _prc _prlc _prt s | None -> Pp.mt () } +ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name } +| [ "bfs" ] -> { Bfs } +| [ "dfs" ] -> { Dfs } +END + ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } -| [ "(bfs)" ] -> { Some Bfs } -| [ "(dfs)" ] -> { Some Dfs } +| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s } | [ ] -> { None } END @@ -135,7 +142,9 @@ let progress_evars t = let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars sigma concl newconcl - then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") + then + let info = Exninfo.reify () in + Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () end in t <*> check diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..0e661543db 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } @@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - { ComHints.HintsExtern (n,c, in_tac tac) } ] ] + { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 6a158bde17..e51b1f051d 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,9 +30,6 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] -let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09f1fc371a..d74e981c6d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1325,6 +1325,8 @@ let () = register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_smart_global + (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3834b21a14..4bc8d61258 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite." let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) - let t = Reductionops.whd_betaiota evd t in + let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false | App (f, [|arg|]) -> @@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -971,7 +971,7 @@ let unfold_match env sigma sk app = | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in - Reductionops.whd_beta sigma (mkApp (v, args)) + Reductionops.whd_beta env sigma (mkApp (v, args)) | _ -> app let is_rew_cast = function RewCast _ -> true | _ -> false @@ -1566,7 +1566,8 @@ let assert_replacing id newt tac = Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = - Proofview.tclZERO (Refiner.FailError (n, lazy s)) + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") - | Some None -> if progress then newfail 0 (str"Failed to progress") - else Proofview.tclUNIT () + | Some None -> + if progress + then newfail 0 (str"Failed to progress") + else Proofview.tclUNIT () | Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in @@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let tactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () - with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded") + with e when CErrors.noncritical e -> + let _, info = Exninfo.capture e in + Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = tactic_init_setoid () <*> @@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause = (cl_rewrite_clause_newtac ~progress strat clause) (fun (e, info) -> match e with | RewriteFailure e -> - tclZEROMSG (str"setoid rewrite failed: " ++ e) + tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) - | e -> Proofview.tclZERO ~info e)) + tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) + | e -> + Proofview.tclZERO ~info e)) (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause = @@ -1894,10 +1900,10 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let _r : GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma + Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma in () let build_morphism_signature env sigma m = @@ -1961,10 +1967,10 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in - let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in + let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in let cst = GlobRef.ConstRef cst in Classes.add_instance @@ -1981,7 +1987,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let poly = atts.polymorphic in let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook { DeclareDef.Hook.S.dref; _ } = dref |> function + let hook { Declare.Hook.S.dref; _ } = dref |> function | GlobRef.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info @@ -1989,7 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (GlobRef.ConstRef cst) | _ -> assert false in - let hook = DeclareDef.Hook.make hook in + let hook = Declare.Hook.make hook in let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> @@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) (fun (e, info) -> match e with | RewriteFailure e -> - tclFAIL 0 (str"setoid rewrite failed: " ++ e) + tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) end @@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let not_declared env sigma ty rel = - tclFAIL 0 +let not_declared ~info env sigma ty rel = + tclFAIL ~info 0 (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") @@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback = let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel - with e -> Proofview.tclZERO e + with e -> + (* XXX what is the right test here as to whether e can be converted ? *) + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e end begin function | e -> @@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback = | Hipattern.NoEquationFound -> begin match e with | (Not_found, _) -> - let rel, _, _ = decompose_app_rel env sigma concl in - not_declared env sigma ty rel - | (e, info) -> Proofview.tclZERO ~info e + let rel, _, _ = decompose_app_rel env sigma concl in + not_declared ~info env sigma ty rel + | (e, info) -> + Proofview.tclZERO ~info e end | e' -> Proofview.tclZERO ~info e' end diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 04d85ed390..91d26519b8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v = | VarRef var -> EvalVarRef var | ConstRef c -> EvalConstRef c | IndRef _ | ConstructRef _ -> fail () + else if has_type v (topwit wit_smart_global) then + let open GlobRef in + let r = out_gen (topwit wit_smart_global) v in + match r with + | VarRef var -> EvalVarRef var + | ConstRef c -> EvalConstRef c + | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c)) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 597c3fdaac..53dc518bd3 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -14,7 +14,6 @@ open CAst open Pattern open Genredexpr open Glob_term -open Tacred open Util open Names open Libnames @@ -95,9 +94,16 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) - else - try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> Nametab.error_global_not_found qid + else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then + let id = qualid_basename qid in + ArgArg (qid.CAst.loc, GlobRef.VarRef id) + else match locate_global_with_alias ~head:true qid with + | r -> ArgArg (qid.CAst.loc, r) + | exception Not_found -> + if not !strict_check && qualid_is_ident qid then + let id = qualid_basename qid in + ArgArg (qid.CAst.loc, GlobRef.VarRef id) + else Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -287,38 +293,42 @@ let intern_destruction_arg ist = function else clear,ElimOnIdent (make ?loc id) -let short_name = function - | {v=AN qid} when qualid_is_ident qid && not !strict_check -> +let short_name qid = + if qualid_is_ident qid && not !strict_check then Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | _ -> None - -let intern_evaluable_global_reference ist qid = - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) - with Not_found -> - if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else Nametab.error_global_not_found qid + else None + +let evalref_of_globref ?loc ?short = function + | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | r -> + let tpe = match r with + | GlobRef.IndRef _ -> "inductive" + | GlobRef.ConstructRef _ -> "constructor" + | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false + in + user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++ + Nametab.pr_global_env Id.Set.empty r ++ spc () ++ + str "into an evaluable reference.") + +let intern_evaluable ist = function + | {v=AN qid} -> + begin match intern_global_reference ist qid with + | ArgVar _ as v -> v + | ArgArg (loc, r) -> + let short = short_name qid in + evalref_of_globref ?loc ?short r + end + | {v=ByNotation (ntn,sc);loc} -> + let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in + let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in + evalref_of_globref ?loc r -let intern_evaluable_reference_or_by_notation ist = function - | {v=AN r} -> intern_evaluable_global_reference ist r +let intern_smart_global ist = function + | {v=AN r} -> intern_global_reference ist r | {v=ByNotation (ntn,sc);loc} -> - evaluable_of_global_reference ist.genv - (Notation.interp_notation_as_global_reference ?loc - GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) - -(* Globalize a reduction expression *) -let intern_evaluable ist r = - let f ist r = - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) - in - match r with - | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> - ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> - let id = qualid_basename qid in - ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) - | _ -> f ist r + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true + GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) @@ -380,10 +390,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let c = Constrintern.interp_reference sign r in match DAst.get c with | GRef (r,None) -> - Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) + Inl (evalref_of_globref r) | GVar id -> - let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in - Inl (ArgArg (r,None)) + let r = evalref_of_globref (GlobRef.VarRef id) in + Inl r | _ -> let bound_names = Glob_ops.bound_glob_vars c in Inr (bound_names,(c,None),dummy_pat) in @@ -813,6 +823,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); + Genintern.register_intern0 wit_smart_global (lift intern_smart_global); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6debc7d9b9..5abe18e00c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) = fail located_exc end -let catch_error call_trace f x = +let update_loc ?loc (e, info) = + (e, Option.cata (Loc.add_loc info) info loc) + +let catch_error ?loc call_trace f x = try f x with e when CErrors.noncritical e -> let e = Exninfo.capture e in + let e = update_loc ?loc e in catching_error call_trace Exninfo.iraise e -let wrap_error tac k = - if is_traced () then Proofview.tclORELSE tac k else tac +let catch_error_loc ?loc tac = + Proofview.tclOR tac (fun exn -> + let (e, info) = update_loc ?loc exn in + Proofview.tclZERO ~info e) + +let wrap_error ?loc tac k = + if is_traced () then Proofview.tclORELSE tac k + else catch_error_loc ?loc tac -let catch_error_tac call_trace tac = - wrap_error +let catch_error_tac ?loc call_trace tac = + wrap_error ?loc tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -535,9 +545,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = ltac_idents = constrvars.idents; ltac_genargs = ist.lfun; } in - let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in + let loc = loc_of_glob_constr term in + let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in let (evd,c) = - catch_error trace (understand_ltac flags env sigma vars kind) term + catch_error ?loc trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -763,7 +774,9 @@ let interp_message_token ist = function | MsgIdent {loc;v=id} -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with - | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) + | None -> Ftactic.lift ( + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found.")) | Some v -> message_of_value v let interp_message ist l = @@ -1059,7 +1072,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in Profile_ltac.do_profile "eval_tactic:2" trace - (catch_error_tac trace (interp_atomic ist t)) + (catch_error_tac ?loc trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) | TacId s -> @@ -1076,18 +1089,22 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | TacFail (g,n,s) -> let msg = interp_message ist s in - let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in + let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in let tac = match g with - | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l) - | TacGlobal -> tac + | TacLocal -> + let info = Exninfo.reify () in + fun l -> Proofview.tclINDEPENDENT (tac ~info l) + | TacGlobal -> + let info = Exninfo.reify () in + tac ~info in Ftactic.run msg tac | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) - end + end [@ocaml.warning "-3"] | TacAbstract (t,ido) -> let call = LtacMLCall tac in let trace = push_trace(None,call) ist in @@ -1149,7 +1166,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with ; poly ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> - Ftactic.lift (tactic_of_value ist v) + Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v)) in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> @@ -1163,8 +1180,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac - else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ - expected " ++ int len1 ++ str ", found " ++ int len2) + else + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info + (str "Arguments length mismatch: \ + expected " ++ int len1 ++ str ", found " ++ int len2) in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) @@ -1175,7 +1195,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in let tac args = let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in - Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) + Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist)) in Ftactic.run args tac @@ -1256,7 +1276,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in - let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in + let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1278,7 +1298,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac trace (val_interp ist body)) >>= fun v -> + (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1302,12 +1322,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body))) | (VFun(appl,trace,olfun,[],body)) -> let extra_args = List.length largs in - Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++ - str (string_of_int extra_args) ++ - str " extra " ++ str (String.plural extra_args "argument") ++ - str ".") - | VRec(_,_) -> fail - else fail + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info + (str "Illegal tactic application: got " ++ + str (string_of_int extra_args) ++ + str " extra " ++ str (String.plural extra_args "argument") ++ + str ".") + | VRec(_,_) -> + let info = Exninfo.reify () in + fail ~info + else + let info = Exninfo.reify () in + fail ~info (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = @@ -1335,7 +1361,8 @@ and tactic_of_value ist vle = let givenargs = List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in let numgiven = List.length givenargs in - Tacticals.New.tclZEROMSG + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ (match numargs with 0 -> assert false @@ -1353,11 +1380,15 @@ and tactic_of_value ist vle = | _ -> Pp.str "arguments were provided for variables " ++ pr_enum Pp.str givenargs ++ Pp.str ".") - | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") + | VRec _ -> + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in tactic_of_value ist tac - else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.") + else + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.") (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = @@ -1551,10 +1582,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = pr_econstr_env env sigma cresult) end <*> Ftactic.return cresult - with CannotCoerceTo _ -> + with CannotCoerceTo _ as exn -> + let _, info = Exninfo.capture exn in let env = Proofview.Goal.env gl in - Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ pr_inspect env e result) + Tacticals.New.tclZEROMSG ~info + (str "Must evaluate to a closed term" ++ fnl() ++ + str "offending expression: " ++ fnl() ++ pr_inspect env e result) end @@ -2022,6 +2055,7 @@ let interp_pre_ident ist env sigma s = let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + register_interp0 wit_smart_global (lift interp_reference); register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 600c30b403..ed298b7e66 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 525199735d..2b43b11fe1 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx } (** Failure of the pattern-matching monad: no success. *) - let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error } + let fail (type a) : a m = { stream = fun _ _ -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error } let run (m : 'a m) = let ctx = { @@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct (** Declares a substitution, a context substitution and a term substitution. *) let put subst context terms : unit m = let s = { subst ; context ; terms ; lhs = () } in - { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } + { stream = fun k ctx -> match merge s ctx with + | None -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error + | Some s -> k () s } (** Declares a substitution. *) let put_subst subst : unit m = put subst empty_context_subst empty_term_subst diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ee2c87d19a..0f8d941b41 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1897,8 +1897,6 @@ type provername = string * int option * The caching mechanism. *) -open Persistent_cache - module MakeCache (T : sig type prover_option type coeff @@ -1922,7 +1920,7 @@ struct Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) end - include PHashtable (E) + include Persistent_cache.PHashtable (E) let memo_opt use_cache cache_file f = let memof = memo cache_file f in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 79d6c05e1d..3ba6365783 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1475,7 +1475,9 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") + with NO_CONTRADICTION as e -> + let _, info = Exninfo.capture e in + tclZEROMSG ~info (Pp.str"Omega can't solve this system") end end @@ -1890,7 +1892,9 @@ let destructure_goal = end) intro with Undecidable -> Tactics.elim_type (Lazy.force coq_False) - | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + | e when Proofview.V82.catchable_exception e -> + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e in tclTHEN goal_tac destructure_hyps in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 633cdbd735..e7c75e029e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try (* find_ring_strucure can raise an exception *) - let rl = make_args_list sigma rl t in - let evdref = ref sigma in - let e = find_ring_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in - let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + let rl = make_args_list sigma rl t in + let evdref = ref sigma in + let e = find_ring_structure env sigma rl in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in + let lH = carg (make_hyp_list env evdref lH) in + let ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) end (***********************************************************************) @@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try - let rl = make_args_list sigma rl t in - let evdref = ref sigma in - let e = find_field_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in - let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + let rl = make_args_list sigma rl t in + let evdref = ref sigma in + let e = find_field_structure env sigma rl in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in + let lH = carg (make_hyp_list env evdref lH) in + let field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) end diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e05c4c26dd..01e8daf82d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -22,7 +22,7 @@ open Locusops open Ltac_plugin open Tacmach -open Refiner +open Tacticals open Libnames open Ssrmatching_plugin open Ssrmatching @@ -81,6 +81,9 @@ let nohint = false, [] type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma +let project gl = gl.Evd.sigma +let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma } + let push_ctx a gl = re_sig (sig_it gl, a) (project gl) let push_ctxs a gl = re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl) @@ -947,7 +950,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ let open EConstr in if n = 0 then let args = List.rev args in - (if beta then Reductionops.whd_beta sigma else fun x -> x) + (if beta then Reductionops.whd_beta env sigma else fun x -> x) (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match kind_of_type sigma ty with | ProdType (_, src, tgt) -> @@ -1062,11 +1065,12 @@ end let introid ?(orig=ref Anonymous) name = let open Proofview.Notations in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let g = Proofview.Goal.concl gl in match EConstr.kind sigma g with | App (hd, _) when EConstr.isLambda sigma hd -> - convert_concl_no_check (Reductionops.whd_beta sigma g) + convert_concl_no_check (Reductionops.whd_beta env sigma g) | _ -> Tacticals.New.tclIDTAC end <*> (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name)) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab07dd5be9..29a9c65561 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) = | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) | Proj _ when same_proj sigma0 c t -> body env t c | _ -> - let c = Reductionops.whd_betaiotazeta sigma0 c in + let c = Reductionops.whd_betaiotazeta env sigma0 c in match EConstr.kind sigma0 c with | Const _ when EConstr.eq_constr sigma0 c t -> body env t t | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) @@ -516,7 +516,7 @@ let rwprocess_rule env dir rule = let rec loop d sigma r t0 rs red = let t = if red = 1 then Tacred.hnf_constr env sigma t0 - else Reductionops.whd_betaiotazeta sigma t0 in + else Reductionops.whd_betaiotazeta env sigma t0 in ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 88a3e85211..ad0a31622c 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> + (* XXX this is another catch all! *) + let e, info = Exninfo.capture e in Ssrprinters.ppdebug (lazy Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob)); - tclZERO e + tclZERO ~info e end (* Commits the term to the monad *) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index adaf7c8cc1..e004613ef3 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -405,7 +405,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in match kind f with |