diff options
Diffstat (limited to 'plugins')
48 files changed, 1318 insertions, 1072 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 020ab9307d..52c6c5d0f9 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -164,14 +164,17 @@ module Btauto = struct let reify env t = lapp eval [|convert_env env; convert t|] - let print_counterexample p penv gl = + let print_counterexample p penv = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let var = lapp witness [|p|] in let var = EConstr.of_constr var in (* Compute an assignment that dissatisfies the goal *) - let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in - let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in + let redfun, _ = Redexpr.reduction_of_red_expr env Genredexpr.(CbvVm None) in + let _, var = redfun env sigma var in let var = EConstr.Unsafe.to_constr var in - let rec to_list l = match decomp_term (Tacmach.project gl) l with + let rec to_list l = match decomp_term sigma l with | App (c, _) when c === (Lazy.force CoqList._nil) -> [] | App (c, [|_; h; t|]) @@ -196,7 +199,6 @@ module Btauto = struct let assign = List.combine penv var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in @@ -205,7 +207,8 @@ module Btauto = struct str "Not a tautology:" ++ spc () ++ l with e when CErrors.noncritical e -> (str "Not a tautology") in - Tacticals.tclFAIL 0 msg gl + Tacticals.New.tclFAIL 0 msg + end let try_unification env = Proofview.Goal.enter begin fun gl -> @@ -216,7 +219,7 @@ module Btauto = struct match t with | App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) - let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in + let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in tac | _ -> let msg = str "Btauto: Internal error" in 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 7b2ce671a3..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s) let finish_proof dynamic_infos g = observe_tac "finish" (Proofview.V82.of_tactic assumption) g -let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) +let refine c = + Proofview.V82.of_tactic + (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)) + let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v @@ -113,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) @@ -240,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 ()++ *) @@ -531,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 55e659d487..608155eb71 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -159,7 +159,7 @@ let recompute_binder_list fixpoint_exprl = fixpoint_exprl in let (_, _, _, typel), _, ctx, _ = - ComFixpoint.interp_fixpoint ~cofix:false fixl + ComFixpoint.interp_fixpoint ~check_recursivity:false ~cofix:false fixl in let constr_expr_typel = with_full_print @@ -191,61 +191,35 @@ let prepare_body {Vernacexpr.binders} rt = let fun_args, rt' = chop_rlambda_n n rt in (fun_args, rt') -let build_functional_principle ?(opaque = Declare.Transparent) - (evd : Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook = +let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs + _i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = - (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)) + (Tactics.compute_elim_sig sigma (EConstr.of_constr old_princ_type)) .Tactics.nparams in - (* let time1 = System.get_time () in *) let new_principle_type = Functional_principles_types.compute_new_princ_type_from_rel (Array.map Constr.mkConstU funs) sorts old_princ_type in - (* let time2 = System.get_time () in *) - (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) - let new_princ_name = - Namegen.next_ident_away_in_goal - (Id.of_string "___________princ_________") - Id.Set.empty - in let sigma, _ = - Typing.type_of ~refresh:true (Global.env ()) !evd + Typing.type_of ~refresh:true (Global.env ()) sigma (EConstr.of_constr new_principle_type) in - evd := sigma; - let hook = DeclareDef.Hook.make (hook new_principle_type) in - let lemma = - Lemmas.start_lemma ~name:new_princ_name ~poly:false !evd - (EConstr.of_constr new_principle_type) - in - (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - let lemma, _ = - Lemmas.by - (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) - lemma + let ftac = + Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams) in - (* let _tim2 = System.get_time () in *) - (* begin *) - (* let dur1 = System.time_difference tim1 tim2 in *) - (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) - (* end; *) - let {Declare.entries} = - Lemmas.pf_fold - (Declare.close_proof ~opaque ~keep_body_ucst_separate:false) - lemma + let env = Global.env () in + let uctx = Evd.evar_universe_context sigma in + let typ = EConstr.of_constr new_principle_type in + let body, typ, univs, _safe, _uctx = + Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac in - match entries with - | [entry] -> (entry, hook) - | _ -> - CErrors.anomaly - Pp.( - str - "[build_functional_principle] close_proof returned more than one \ - proof term") + (* uctx was ignored before *) + let hook = Declare.Hook.make (hook new_principle_type) in + (body, typ, univs, hook, sigma) let change_property_sort evd toSort princ princName = let open Context.Rel.Declaration in @@ -333,17 +307,19 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts register_with_sort Sorts.InProp; register_with_sort Sorts.InSet ) in - let entry, hook = - build_functional_principle evd old_princ_type new_sorts funs i proof_tac + let body, types, univs, hook, sigma0 = + build_functional_principle !evd old_princ_type new_sorts funs i proof_tac hook in + evd := sigma0; (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) 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 @@ -424,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 @@ -443,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 @@ -1334,8 +1310,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : - Evd.side_effects Declare.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1402,18 +1377,19 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent in - let entry, _hook = + let body, typ, univs, _hook, sigma0 = try - build_functional_principle ~opaque evd first_type (Array.of_list sorts) + build_functional_principle !evd first_type (Array.of_list sorts) this_block_funs 0 (Functional_principles_proofs.prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ -> ()) with e when CErrors.noncritical e -> raise (Defining_principle e) in + evd := sigma0; incr i; (* The others are just deduced *) - if List.is_empty other_princ_types then [entry] + if List.is_empty other_princ_types then [(body, typ, univs, opaque)] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in @@ -1422,10 +1398,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body = entry.Declare.proof_entry_body in - let ctxt, fix = - Term.decompose_lam_assum (fst (fst (Future.force first_princ_body))) - in + let first_princ_body = body in + let ctxt, fix = Term.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) let (idxs, _), ((_, ta, _) as decl) = Constr.destFix fix in let other_result = @@ -1457,8 +1431,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let entry, _hook = - build_functional_principle evd + let body, typ, univs, _hook, sigma0 = + build_functional_principle !evd (List.nth other_princ_types (!i - 1)) (Array.of_list sorts) this_block_funs !i (Functional_principles_proofs.prove_princ_for_struct evd false @@ -1466,15 +1440,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - entry + evd := sigma0; + (body, typ, univs, opaque) with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix ((idxs, i), decl)) ctxt in - Declare.definition_entry ~types:scheme_type princ_body) + (princ_body, Some scheme_type, univs, opaque)) other_fun_princ_types in - entry :: other_result + (body, typ, univs, opaque) :: other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1527,11 +1502,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) with Not_found -> Array.of_list (List.map - (fun entry -> - ( EConstr.of_constr - (fst (fst (Future.force entry.Declare.proof_entry_body))) - , EConstr.of_constr (Option.get entry.Declare.proof_entry_type) - )) + (fun (body, typ, _opaque, _univs) -> + (EConstr.of_constr body, EConstr.of_constr (Option.get typ))) (make_scheme evd (Array.map_to_list (fun const -> (const, Sorts.InType)) funs))) in @@ -2225,11 +2197,14 @@ let build_scheme fas = in let bodies_types = make_scheme evd pconstants in List.iter2 - (fun (princ_id, _, _) def_entry -> - ignore - (Declare.declare_constant ~name:princ_id - ~kind:Decls.(IsProof Theorem) - (Declare.DefinitionEntry def_entry)); + (fun (princ_id, _, _) (body, types, univs, opaque) -> + let (_ : Constant.t) = + let opaque = if opaque = Declare.Opaque then true else false in + let def_entry = Declare.definition_entry ~univs ~opaque ?types body in + Declare.declare_constant ~name:princ_id + ~kind:Decls.(IsProof Theorem) + (Declare.DefinitionEntry def_entry) + in Declare.definition_message princ_id) fas bodies_types 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..81e745b714 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 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/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 14fab251d0..0dbf16a821 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling -(** LtacProf cannot yet handle backtracking into multi-success tactics. - To properly support this, we'd have to somehow recreate our location in the - call-stack, and stop/restart the intervening timers. This is tricky and - possibly expensive, so instead we currently just emit a warning that - profiling results will be off. *) -let encountered_multi_success_backtracking = ref false - -let warn_profile_backtracking = - CWarnings.create ~name:"profile-backtracking" ~category:"ltac" - (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") - -let warn_encountered_multi_success_backtracking () = - if !encountered_multi_success_backtracking then - warn_profile_backtracking () - -let encounter_multi_success_backtracking () = - if not !encountered_multi_success_backtracking +let encountered_invalid_stack_no_self = ref false + +let warn_invalid_stack_no_self = + CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac" + (fun () -> strbrk + "Ltac Profiler encountered an invalid stack (no self \ + node). This can happen if you reset the profile during \ + tactic execution.") + +let encounter_invalid_stack_no_self () = + if not !encountered_invalid_stack_no_self then begin - encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking () + encountered_invalid_stack_no_self := true; + warn_invalid_stack_no_self () end @@ -76,8 +69,7 @@ module Local = Summary.Local let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] let reset_profile_tmp () = - Local.(stack := [empty_treenode root]); - encountered_multi_success_backtracking := false + Local.(stack := [empty_treenode root]) (* ************** XML Serialization ********************* *) @@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node = cumulate tree; !global in - warn_encountered_multi_success_backtracking (); let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ @@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c = match Local.(!stack) with | [] | [_] -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + encounter_invalid_stack_no_self (); reset_profile_tmp () | node :: (parent :: rest as full_stack) -> let name = string_of_call c in if not (String.equal name node.name) then (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + CErrors.anomaly + (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \ + likely due to backtracking into multi-success tactics."); let node = { node with total = node.total +. diff; local = node.local +. diff; @@ -332,38 +325,56 @@ let exit_tactic ~count_call start_time c = (* Calls are over, we reset the stack and send back data *) if rest == [] && get_profiling () then begin assert(String.equal root parent.name); + encountered_invalid_stack_no_self := false; reset_profile_tmp (); feedback_results parent end -let tclFINALLY tac (finally : unit Proofview.tactic) = +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. *) +let rec tclWRAPFINALLY before tac finally = + let open Proofview in let open Proofview.Notations in - Proofview.tclIFCATCH - tac - (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) + before >>= fun v -> tclCASE tac >>= function + | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e + | Next (ret, tac') -> tclOR + (finally v >>= fun () -> tclUNIT ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling then - match call_trace, Local.(!stack) with - | (_, c) :: _, parent :: rest -> - let name = string_of_call c in - let node = get_child name parent in - Local.(stack := node :: parent :: rest); - Some (time ()) - | _ :: _, [] -> assert false - | _ -> None - else None)) >>= function - | Some start_time -> - tclFINALLY - tac + (* We do an early check to [is_profiling] so that we save the + overhead of [tclWRAPFINALLY] when profiling is not set + *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function + | false -> tac + | true -> + tclWRAPFINALLY (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> exit_tactic ~count_call start_time c - | [] -> ())))) - | None -> tac + if !is_profiling then + match call_trace, Local.(!stack) with + | (_, c) :: _, parent :: rest -> + let name = string_of_call c in + let node = get_child name parent in + Local.(stack := node :: parent :: rest); + Some (time ()) + | _ :: _, [] -> assert false + | _ -> None + else None))) + tac + (function + | Some start_time -> + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> exit_tactic ~count_call start_time c + | [] -> ())))) + | None -> Proofview.tclUNIT ()) (* ************** Accumulation of data from workers ************************* *) @@ -396,6 +407,7 @@ let _ = | _ -> ())) let reset_profile () = + encountered_invalid_stack_no_self := false; reset_profile_tmp (); data := SM.empty diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3834b21a14..d6b2a17882 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 @@ -1894,10 +1894,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 +1961,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 +1981,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 +1989,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 () -> 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/tacentries.ml b/plugins/ltac/tacentries.ml index 9910796d9c..e6c59f446d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function +| MLTyNil -> 0 +| MLTyArg sign -> 1 + ml_sig_len sign + +let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a = + fun sign f -> + match sign with + | MLTyNil -> + begin function + | [] -> f + | _ :: _ -> CErrors.anomaly (str "Arity mismatch") + end + | MLTyArg sign -> + function + | [] -> CErrors.anomaly (str "Arity mismatch") + | arg :: args -> cast_ml sign (f arg) args + +let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args _ = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in + let len = ml_sig_len sign in + let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let vars = List.map (fun id -> Name id) args in + let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin + +module MLName = +struct + open Tacexpr + type t = ml_tactic_name + let compare tac1 tac2 = + let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in + if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin + else c +end + +module MLTacMap = Map.Make(MLName) + +let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty + +type ml_ltac_val = { + tacval_tac : Tacexpr.ml_tactic_name; + tacval_var : Id.t list; +} + +let in_tacval = +(* This is a hack to emulate value-returning ML-implemented tactics in Ltac. + We use a dummy generic argument to work around the limitations of the Ltac + runtime. Indeed, the TacML node needs to return unit values, since it is + considered a "tactic" in the runtime. Changing it to allow arbitrary values + would require to toggle this status, and thus to make it a "value" node. + This would in turn create too much backwards incompatibility. Instead, we + piggy back on the TacGeneric node, which by construction is used to return + values. + + The trick is to represent a n-ary application of a ML function as a generic + argument. We store in the node the name of the tactic and its arity, while + giving canonical names to the bound variables of the closure. This trick is + already performed in several external developments for specific calls, we + make it here generic. The argument should not be used for other purposes, so + we only export the registering functions. + *) + let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type = + Genarg.create_arg "ltac:val" + in + (* No need to internalize this ever *) + let intern_fun _ e = Empty.abort e in + let subst_fun s v = v in + let () = Genintern.register_intern0 wit intern_fun in + let () = Genintern.register_subst0 wit subst_fun in + (* No need to register a value tag for it via register_val0 since we will + never access this genarg directly. *) + let interp_fun ist tac = + let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in + let tac = MLTacMap.get tac.tacval_tac !ml_table in + tac args + in + let () = Geninterp.register_interp0 wit interp_fun in + (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v) + + +let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let len = ml_sig_len sign in + let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in + let vars = List.map (fun id -> Name id) vars in + let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in + let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in + Mltop.declare_cache_obj obj plugin (** ARGUMENT EXTEND *) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ce38431a18..6ee3ce091b 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -69,6 +69,25 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +(** {5 Low-level registering of tactics} *) + +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit +(** Helper function to define directly an Ltac function in OCaml without any + associated parsing rule nor further shenanigans. The Ltac function will be + defined as [name] in the Coq file that loads the ML plugin where this + function is called. It will have the arity given by the [ml_ty_sig] + argument. *) + +val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit +(** Same as {!ml_tactic_extend} but the function can return an argument + instead. *) + (** {5 TACTIC EXTEND} *) type _ ty_sig = 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 dda7f0742c..6d350ade8d 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 @@ -1059,7 +1070,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 -> @@ -1087,7 +1098,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | 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 +1160,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) -> @@ -1175,7 +1186,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 @@ -1278,7 +1289,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) -> @@ -1895,8 +1906,7 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure - (** Apply toplevel tactic values *) - let apply (f : value) (args: value list) = + let apply_expr f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar CAst.(make id)) in @@ -1905,9 +1915,18 @@ module Value = struct let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in let lfun = Id.Map.add (Id.of_string "F") f lfun in let ist = { (default_ist ()) with lfun = lfun; } in - let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) + + + (** Apply toplevel tactic values *) + let apply (f : value) (args: value list) = + let ist, tac = apply_expr f args in eval_tactic_ist ist tac + let apply_val (f : value) (args: value list) = + let ist, tac = apply_expr f args in + val_interp ist tac + end (* globalization + interpretation *) @@ -2014,6 +2033,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/tacinterp.mli b/plugins/ltac/tacinterp.mli index ce34356a37..cbb17bf0fa 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -29,6 +29,7 @@ sig val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a val apply : t -> t list -> unit Proofview.tactic + val apply_val : t -> t list -> t Ftactic.t end (** Values for interpretation *) 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/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7e4c4ce5c6..0f8d941b41 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -128,249 +128,142 @@ let selecti s m = *) module M = struct (** - * Location of the Coq libraries. - *) - - let logic_dir = ["Coq"; "Logic"; "Decidable"] - - let mic_modules = - [ ["Coq"; "Lists"; "List"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "DeclConstant"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "RMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "QArith"; "QArith_base"] - ; ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["LRing_normalise"] ] - - [@@@ocaml.warning "-3"] - - let coq_modules = - Coqlib.( - init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules - @ mic_modules) - - let bin_module = [["Coq"; "Numbers"; "BinNums"]] - - let r_modules = - [ ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["Coq"; "Reals"; "Raxioms"] - ; ["Coq"; "QArith"; "Qreals"] ] - - let z_modules = [["Coq"; "ZArith"; "BinInt"]] - - (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v *) - let gen_constant_in_modules s m n = + let constr_of_ref str = EConstr.of_constr - ( UnivGen.constr_of_monomorphic_global - @@ Coqlib.gen_reference_in_modules s m n ) - - let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules - - [@@@ocaml.warning "+3"] - - let constant = gen_constant_in_modules "ZMicromega" coq_modules - let bin_constant = gen_constant_in_modules "ZMicromega" bin_module - let r_constant = gen_constant_in_modules "ZMicromega" r_modules - let z_constant = gen_constant_in_modules "ZMicromega" z_modules - let m_constant = gen_constant_in_modules "ZMicromega" mic_modules - let coq_and = lazy (init_constant "and") - let coq_or = lazy (init_constant "or") - let coq_not = lazy (init_constant "not") - let coq_iff = lazy (init_constant "iff") - let coq_True = lazy (init_constant "True") - let coq_False = lazy (init_constant "False") - let coq_cons = lazy (constant "cons") - let coq_nil = lazy (constant "nil") - let coq_list = lazy (constant "list") - let coq_O = lazy (init_constant "O") - let coq_S = lazy (init_constant "S") - let coq_nat = lazy (init_constant "nat") - let coq_unit = lazy (init_constant "unit") + (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) + + let coq_and = lazy (constr_of_ref "core.and.type") + let coq_or = lazy (constr_of_ref "core.or.type") + let coq_not = lazy (constr_of_ref "core.not.type") + let coq_iff = lazy (constr_of_ref "core.iff.type") + let coq_True = lazy (constr_of_ref "core.True.type") + let coq_False = lazy (constr_of_ref "core.False.type") + let coq_cons = lazy (constr_of_ref "core.list.cons") + let coq_nil = lazy (constr_of_ref "core.list.nil") + let coq_list = lazy (constr_of_ref "core.list.type") + let coq_O = lazy (constr_of_ref "num.nat.O") + let coq_S = lazy (constr_of_ref "num.nat.S") + let coq_nat = lazy (constr_of_ref "num.nat.type") + let coq_unit = lazy (constr_of_ref "core.unit.type") (* let coq_option = lazy (init_constant "option")*) - let coq_None = lazy (init_constant "None") - let coq_tt = lazy (init_constant "tt") - let coq_Inl = lazy (init_constant "inl") - let coq_Inr = lazy (init_constant "inr") - let coq_N0 = lazy (bin_constant "N0") - let coq_Npos = lazy (bin_constant "Npos") - let coq_xH = lazy (bin_constant "xH") - let coq_xO = lazy (bin_constant "xO") - let coq_xI = lazy (bin_constant "xI") - let coq_Z = lazy (bin_constant "Z") - let coq_ZERO = lazy (bin_constant "Z0") - let coq_POS = lazy (bin_constant "Zpos") - let coq_NEG = lazy (bin_constant "Zneg") - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - let coq_Qmake = lazy (constant "Qmake") - let coq_Rcst = lazy (constant "Rcst") - let coq_C0 = lazy (m_constant "C0") - let coq_C1 = lazy (m_constant "C1") - let coq_CQ = lazy (m_constant "CQ") - let coq_CZ = lazy (m_constant "CZ") - let coq_CPlus = lazy (m_constant "CPlus") - let coq_CMinus = lazy (m_constant "CMinus") - let coq_CMult = lazy (m_constant "CMult") - let coq_CPow = lazy (m_constant "CPow") - let coq_CInv = lazy (m_constant "CInv") - let coq_COpp = lazy (m_constant "COpp") - let coq_R0 = lazy (constant "R0") - let coq_R1 = lazy (constant "R1") - let coq_proofTerm = lazy (constant "ZArithProof") - let coq_doneProof = lazy (constant "DoneProof") - let coq_ratProof = lazy (constant "RatProof") - let coq_cutProof = lazy (constant "CutProof") - let coq_enumProof = lazy (constant "EnumProof") - let coq_ExProof = lazy (constant "ExProof") - let coq_Zgt = lazy (z_constant "Z.gt") - let coq_Zge = lazy (z_constant "Z.ge") - let coq_Zle = lazy (z_constant "Z.le") - let coq_Zlt = lazy (z_constant "Z.lt") - let coq_Eq = lazy (init_constant "eq") - let coq_Zplus = lazy (z_constant "Z.add") - let coq_Zminus = lazy (z_constant "Z.sub") - let coq_Zopp = lazy (z_constant "Z.opp") - let coq_Zmult = lazy (z_constant "Z.mul") - let coq_Zpower = lazy (z_constant "Z.pow") - let coq_Qle = lazy (constant "Qle") - let coq_Qlt = lazy (constant "Qlt") - let coq_Qeq = lazy (constant "Qeq") - let coq_Qplus = lazy (constant "Qplus") - let coq_Qminus = lazy (constant "Qminus") - let coq_Qopp = lazy (constant "Qopp") - let coq_Qmult = lazy (constant "Qmult") - let coq_Qpower = lazy (constant "Qpower") - let coq_Rgt = lazy (r_constant "Rgt") - let coq_Rge = lazy (r_constant "Rge") - let coq_Rle = lazy (r_constant "Rle") - let coq_Rlt = lazy (r_constant "Rlt") - let coq_Rplus = lazy (r_constant "Rplus") - let coq_Rminus = lazy (r_constant "Rminus") - let coq_Ropp = lazy (r_constant "Ropp") - let coq_Rmult = lazy (r_constant "Rmult") - let coq_Rinv = lazy (r_constant "Rinv") - let coq_Rpower = lazy (r_constant "pow") - let coq_powerZR = lazy (r_constant "powerRZ") - let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (r_constant "Q2R") - let coq_PEX = lazy (constant "PEX") - let coq_PEc = lazy (constant "PEc") - let coq_PEadd = lazy (constant "PEadd") - let coq_PEopp = lazy (constant "PEopp") - let coq_PEmul = lazy (constant "PEmul") - let coq_PEsub = lazy (constant "PEsub") - let coq_PEpow = lazy (constant "PEpow") - let coq_PX = lazy (constant "PX") - let coq_Pc = lazy (constant "Pc") - let coq_Pinj = lazy (constant "Pinj") - let coq_OpEq = lazy (constant "OpEq") - let coq_OpNEq = lazy (constant "OpNEq") - let coq_OpLe = lazy (constant "OpLe") - let coq_OpLt = lazy (constant "OpLt") - let coq_OpGe = lazy (constant "OpGe") - let coq_OpGt = lazy (constant "OpGt") - let coq_PsatzIn = lazy (constant "PsatzIn") - let coq_PsatzSquare = lazy (constant "PsatzSquare") - let coq_PsatzMulE = lazy (constant "PsatzMulE") - let coq_PsatzMultC = lazy (constant "PsatzMulC") - let coq_PsatzAdd = lazy (constant "PsatzAdd") - let coq_PsatzC = lazy (constant "PsatzC") - let coq_PsatzZ = lazy (constant "PsatzZ") + let coq_None = lazy (constr_of_ref "core.option.None") + let coq_tt = lazy (constr_of_ref "core.unit.tt") + let coq_Inl = lazy (constr_of_ref "core.sum.inl") + let coq_Inr = lazy (constr_of_ref "core.sum.inr") + let coq_N0 = lazy (constr_of_ref "num.N.N0") + let coq_Npos = lazy (constr_of_ref "num.N.Npos") + let coq_xH = lazy (constr_of_ref "num.pos.xH") + let coq_xO = lazy (constr_of_ref "num.pos.xO") + let coq_xI = lazy (constr_of_ref "num.pos.xI") + let coq_Z = lazy (constr_of_ref "num.Z.type") + let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") + let coq_POS = lazy (constr_of_ref "num.Z.Zpos") + let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") + let coq_Q = lazy (constr_of_ref "rat.Q.type") + let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") + let coq_R = lazy (constr_of_ref "reals.R.type") + let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") + let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") + let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") + let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") + let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") + let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") + let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") + let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") + let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") + let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") + let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") + let coq_R0 = lazy (constr_of_ref "reals.R.R0") + let coq_R1 = lazy (constr_of_ref "reals.R.R1") + let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") + let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") + let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") + let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") + let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") + let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") + let coq_Zgt = lazy (constr_of_ref "num.Z.gt") + let coq_Zge = lazy (constr_of_ref "num.Z.ge") + let coq_Zle = lazy (constr_of_ref "num.Z.le") + let coq_Zlt = lazy (constr_of_ref "num.Z.lt") + let coq_Eq = lazy (constr_of_ref "core.eq.type") + let coq_Zplus = lazy (constr_of_ref "num.Z.add") + let coq_Zminus = lazy (constr_of_ref "num.Z.sub") + let coq_Zopp = lazy (constr_of_ref "num.Z.opp") + let coq_Zmult = lazy (constr_of_ref "num.Z.mul") + let coq_Zpower = lazy (constr_of_ref "num.Z.pow") + let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") + let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") + let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") + let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") + let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") + let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") + let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") + let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") + let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") + let coq_Rge = lazy (constr_of_ref "reals.R.Rge") + let coq_Rle = lazy (constr_of_ref "reals.R.Rle") + let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") + let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") + let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") + let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") + let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") + let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") + let coq_Rpower = lazy (constr_of_ref "reals.R.pow") + let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") + let coq_IZR = lazy (constr_of_ref "reals.R.IZR") + let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") + let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") + let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") + let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") + let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") + let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") + let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") + let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") + let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") + let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") + let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") + let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") + let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") + let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") + let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") + let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") + let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") + let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") + let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") + let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") + let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") + let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") + let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") + let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") (* let coq_GT = lazy (m_constant "GT")*) - let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant") - - let coq_TT = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "TT") - - let coq_FF = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "FF") - - let coq_And = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "Cj") - - let coq_Or = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "D") - - let coq_Neg = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "N") - - let coq_Atom = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "A") - - let coq_X = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "X") - - let coq_Impl = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "I") + let coq_DeclaredConstant = + lazy (constr_of_ref "micromega.DeclaredConstant.type") - let coq_Formula = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "BFormula") + let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") + let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") + let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj") + let coq_Or = lazy (constr_of_ref "micromega.GFormula.D") + let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N") + let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") + let coq_X = lazy (constr_of_ref "micromega.GFormula.X") + let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I") + let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") (** * Initialization : a few Caml symbols are derived from other libraries; * QMicromega, ZArithRing, RingMicromega. *) - let coq_QWitness = - lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "QMicromega"]] - "QWitness") - - let coq_Build = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Build_Formula") - - let coq_Cstr = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Formula") + let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") + let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") + let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") (** * Parsing and dumping : transformation functions between Caml and Coq @@ -1318,29 +1211,10 @@ end open M -let coq_Branch = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Branch") - -let coq_Elt = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Elt") - -let coq_Empty = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Empty") - -let coq_VarMap = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t") +let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch") +let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt") +let coq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty") +let coq_VarMap = lazy (constr_of_ref "micromega.VarMap.type") let rec dump_varmap typ m = match m with @@ -1900,13 +1774,7 @@ let micromega_order_changer cert env ff = [ ( "__ff" , ff , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) - ; ( "__varmap" - , vm - , EConstr.mkApp - ( gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t" - , [|typ|] ) ) + ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|])) ; ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) @@ -2029,8 +1897,6 @@ type provername = string * int option * The caching mechanism. *) -open Persistent_cache - module MakeCache (T : sig type prover_option type coeff @@ -2054,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/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/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 6a9a0657a3..42b9248979 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -55,18 +55,18 @@ let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) let interp_nbargs ist gl rc = try let rc6 = mkRApp rc (mkRHoles 6) in - let sigma, t = interp_open_constr ist gl (rc6, None) in + let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in let si = sig_it gl in let gl = re_sig si sigma in - 6 + Ssrcommon.nbargs_open_constr gl t + 6 + Ssrcommon.nbargs_open_constr (pf_env gl) t with _ -> 5 let interp_view_nbimps ist gl rc = try - let sigma, t = interp_open_constr ist gl (rc, None) in + let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in let si = sig_it gl in let gl = re_sig si sigma in - let pl, c = splay_open_constr gl t in + let pl, c = splay_open_constr (pf_env gl) t in if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl)) with _ -> 0 @@ -88,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) let n = match ist, DAst.get t with - | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) + | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in @@ -97,7 +97,7 @@ let apply_rconstr ?ist t gl = if i > n then errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t) else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in - refine_with (loop 0) gl + Proofview.V82.of_tactic (refine_with (loop 0)) gl let mkRAppView ist gl rv gv = let nb_view_imps = interp_view_nbimps ist gl rv in @@ -112,18 +112,20 @@ let refine_interp_apply_view dbl ist gl gv = interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in let rec loop = function | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv) - | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in + | h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in loop (pair dbl (Ssrview.AdaptorDb.get dbl) @ if dbl = Ssrview.AdaptorDb.Equivalence then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward)) else []) let apply_top_tac = - Tacticals.tclTHENLIST [ + Proofview.Goal.enter begin fun _ -> + Tacticals.New.tclTHENLIST [ introid top_id; - apply_rconstr (mkRVar top_id); - old_cleartac [SsrHyp(None,top_id)] + Proofview.V82.tactic (apply_rconstr (mkRVar top_id)); + cleartac [SsrHyp(None,top_id)] ] + end let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl -> let _, clr = interp_hyps ist gl gclr in @@ -131,7 +133,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars: let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in - [], Tacticals.tclTHEN (genstac (ggenl,[])) + [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[]))) else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in tclGENTAC (fun gl -> match gviews, ggenl with @@ -148,9 +150,9 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars: | [], [agens] -> let clr', (sigma, lemma) = interp_agens ist gl agens in let gl = pf_merge_uc_of sigma gl in - Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl + Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl | _, _ -> - Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl + Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl ) -let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac +let apply_top_tac = apply_top_tac diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 134a9e4b36..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) @@ -221,8 +224,8 @@ let intern_term ist env (_, c) = glob_constr ist env c (* FUNCLASS, which is probably just as well since these can *) (* lead to infinite arities. *) -let splay_open_constr gl (sigma, c) = - let env = pf_env gl in let t = Retyping.get_type_of env sigma c in +let splay_open_constr env (sigma, c) = + let t = Retyping.get_type_of env sigma c in Reductionops.splay_prod env sigma t let isAppInd env sigma c = @@ -253,11 +256,11 @@ let interp_refine ist gl rc = (sigma, (sigma, c)) -let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in - (project gl, (sigma, c)) +let interp_open_constr env sigma0 ist gc = + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist env sigma0 (gc, Tactypes.NoBindings) in + (sigma0, (sigma, c)) -let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) +let interp_term env sigma ist (_, c) = snd (interp_open_constr env sigma ist c) let of_ftactic ftac gl = let r = ref None in @@ -322,10 +325,10 @@ let ssrdgens_of_parsed_dgens = function | _ -> assert false -let nbargs_open_constr gl oc = - let pl, _ = splay_open_constr gl oc in List.length pl +let nbargs_open_constr env oc = + let pl, _ = splay_open_constr env oc in List.length pl -let pf_nbargs gl c = nbargs_open_constr gl (project gl, c) +let pf_nbargs env sigma c = nbargs_open_constr env (sigma, c) let internal_names = ref [] let add_internal_name pt = internal_names := pt :: !internal_names @@ -521,10 +524,10 @@ let resolve_typeclasses ~where ~fail env sigma = let nf_evar sigma t = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t)) -let pf_abs_evars2 gl rigid (sigma, c0) = +let abs_evars2 env sigma0 rigid (sigma, c0) = let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in - let sigma0, ucst = project gl, Evd.evar_universe_context sigma in - let nenv = env_size (pf_env gl) in + let sigma0, ucst = sigma0, Evd.evar_universe_context sigma in + let nenv = env_size env in let abs_evar n k = let evi = Evd.find sigma k in let concl = EConstr.Unsafe.to_constr evi.evar_concl in @@ -558,6 +561,11 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | [] -> c in List.length evlist, EConstr.of_constr (loop (get 1 c0) 1 evlist), List.map fst evlist, ucst +let pf_abs_evars2 gl rigid c = + abs_evars2 (pf_env gl) (project gl) rigid c + +let abs_evars env sigma t = abs_evars2 env sigma [] t + let pf_abs_evars gl t = pf_abs_evars2 gl [] t @@ -569,7 +577,7 @@ let pf_abs_evars gl t = pf_abs_evars2 gl [] t * the corresponding lambda looks like (fun evar_i : T(c)) where c is * the solution found by ssrautoprop. *) -let ssrautoprop_tac = ref (fun gl -> assert false) +let ssrautoprop_tac = ref (Proofview.Goal.enter (fun gl -> assert false)) (* Thanks to Arnaud Spiwack for this snippet *) let call_on_evar tac e s = @@ -581,12 +589,11 @@ open Pp let pp _ = () (* FIXME *) module Intset = Evar.Set -let pf_abs_evars_pirrel gl (sigma, c0) = +let abs_evars_pirrel env sigma0 (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); - pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0)); - let sigma0 = project gl in + pp(lazy(str"c0= " ++ Printer.pr_constr_env env sigma c0)); let c0 = nf_evar sigma0 (nf_evar sigma c0) in - let nenv = env_size (pf_env gl) in + let nenv = env_size env in let abs_evar n k = let evi = Evd.find sigma k in let concl = EConstr.Unsafe.to_constr evi.evar_concl in @@ -602,13 +609,13 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let n = max 0 (List.length a - nenv) in let k_ty = Retyping.get_sort_family_of - (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in + env sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env env sigma (Reductionops.nf_beta env sigma0 (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> Evar.print k) evlist)); let evplist = @@ -620,7 +627,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = if evplist = [] then evlist, [], sigma else List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) -> try - let ng, sigma = call_on_evar !ssrautoprop_tac i sigma in + let ng, sigma = call_on_evar (Proofview.V82.of_tactic !ssrautoprop_tac) i sigma in if (ng <> []) then errorstrm (str "Should we tell the user?"); List.filter (fun (j,_) -> j <> i) ev, evp, sigma with _ -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in @@ -667,6 +674,9 @@ let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"res= " ++ pr_constr res)); List.length evlist, res +let pf_abs_evars_pirrel gl c = + abs_evars_pirrel (pf_env gl) (project gl) c + (* Strip all non-essential dependencies from an abstracted term, generating *) (* standard names for the abstracted holes. *) @@ -678,7 +688,8 @@ let nb_evar_deps = function (try int_of_string (String.sub s m (String.length s - 1 - m)) with _ -> 0) | _ -> 0 -let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) +let type_id env sigma t = Id.of_string (Namegen.hdchar env sigma t) +let pf_type_id gl t = type_id (pf_env gl) (project gl) t let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty @@ -693,7 +704,7 @@ let pf_type_of gl t = let sigma, ty = pf_type_of gl (EConstr.of_constr t) in re_sig (sig_it gl) sigma, EConstr.Unsafe.to_constr ty -let pf_abs_cterm gl n c0 = +let abs_cterm env sigma n c0 = if n <= 0 then c0 else let c0 = EConstr.Unsafe.to_constr c0 in let noargs = [|0|] in @@ -725,13 +736,15 @@ let pf_abs_cterm gl n c0 = let na' = List.length dl in eva.(i) <- Array.of_list (na - na' :: dl); let x' = - if na' = 0 then Name (pf_type_id gl (EConstr.of_constr t2)) else mk_evar_name na' in + if na' = 0 then Name (type_id env sigma (EConstr.of_constr t2)) else mk_evar_name na' in mkLambda ({x with binder_name=x'}, t2, strip_evars (i + 1) c1) (* if noccurn 1 c2 then lift (-1) c2 else mkLambda (Name (pf_type_id gl t2), t2, c2) *) | _ -> strip i c in EConstr.of_constr (strip_evars 0 c0) +let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0 + (* }}} *) let pf_merge_uc uc gl = @@ -835,7 +848,7 @@ open Locus let rewritetac ?(under=false) dir c = (* Due to the new optional arg ?tac, application shouldn't be too partial *) let open Proofview.Notations in - Proofview.V82.of_tactic begin + Proofview.Goal.enter begin fun _ -> Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*> if under then Proofview.cycle 1 else Proofview.tclUNIT () end @@ -845,7 +858,7 @@ let rewritetac ?(under=false) dir c = type name_hint = (int * EConstr.types array) option ref let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t = - let sigma, ct as t = interp_term ist gl t in + let sigma, ct as t = interp_term (pf_env gl) (project gl) ist t in let sigma, _ as t = let env = pf_env gl in if not resolve_typeclasses then t @@ -857,7 +870,8 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t = let top_id = mk_internal_id "top assumption" -let ssr_n_tac seed n gl = +let ssr_n_tac seed n = + Proofview.Goal.enter begin fun gl -> let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = @@ -867,9 +881,10 @@ let ssr_n_tac seed n gl = if n = -1 then fail "The ssreflect library was not loaded" else fail ("The tactic "^name^" was not found") in let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in - Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl + Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr) + end -let donetac n gl = ssr_n_tac "done" n gl +let donetac n = ssr_n_tac "done" n open Constrexpr open Util @@ -890,7 +905,7 @@ let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false -let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = +let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty = let n_binders = ref 0 in let ty = match ty with | a, (t, None) -> @@ -915,15 +930,14 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t) | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in sigma, aux t in - let sigma, cty as ty = strip_cast (interp_term ist gl ty) in + let sigma, cty as ty = strip_cast (interp_term env sigma0 ist ty) in let ty = - let env = pf_env gl in if not resolve_typeclasses then ty else let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in sigma, Evarutil.nf_evar sigma cty in - let n, c, _, ucst = pf_abs_evars gl ty in - let lam_c = pf_abs_cterm gl n c in + let n, c, _, ucst = abs_evars env sigma0 ty in + let lam_c = abs_cterm env sigma0 n c in let ctx, c = EConstr.decompose_lam_n_assum sigma n lam_c in n, EConstr.it_mkProd_or_LetIn c ctx, lam_c, ucst ;; @@ -936,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) -> @@ -981,7 +995,8 @@ let dependent_apply_error = * * Refiner.refiner that does not handle metas with a non ground type but works * with dependently typed higher order metas. *) -let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl = +let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t = + Proofview.V82.tactic begin fun gl -> if with_evars then let refine gl = let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in @@ -1014,16 +1029,22 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Proofview.(V82.of_tactic (Tacticals.New.tclTHENLIST [ - V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t)); + Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t); (if first_goes_last then cycle 1 else tclUNIT ()) ])) gl + end -let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = +let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc = + 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 uct = Evd.evar_universe_context (fst oc) in - let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in - let gl = pf_unsafe_merge_uc uct gl in - try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl - with e when CErrors.noncritical e -> raise dependent_apply_error + let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in + Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*> + Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) + (fun _ -> Proofview.tclZERO dependent_apply_error) + end (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) @@ -1041,23 +1062,25 @@ let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac) end -let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl -> - let g, env = Tacmach.pf_concl gl, pf_env gl in - let sigma = project gl in +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 -> - Proofview.V82.of_tactic (convert_concl_no_check (Reductionops.whd_beta sigma g)) gl - | _ -> tclIDTAC gl) - (Proofview.V82.of_tactic - (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))) -;; + 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)) let anontac decl gl = let id = match RelDecl.get_name decl with | Name id -> if is_discharged_id id then id else mk_anon_id (Id.to_string id) (Tacmach.pf_ids_of_hyps gl) | _ -> mk_anon_id ssr_anon_hyp (Tacmach.pf_ids_of_hyps gl) in - introid id gl + Proofview.V82.of_tactic (introid id) gl let rec intro_anon gl = try anontac (List.hd (fst (EConstr.decompose_prod_n_assum (project gl) 1 (Tacmach.pf_concl gl)))) gl @@ -1085,16 +1108,17 @@ let interp_clr sigma = function let tclID tac = tac let tclDOTRY n tac = + let open Tacticals.New in if n <= 0 then tclIDTAC else - let rec loop i gl = - if i = n then tclTRY tac gl else - tclTRY (tclTHEN tac (loop (i + 1))) gl in + let rec loop i = + if i = n then tclTRY tac else + tclTRY (tclTHEN tac (loop (i + 1))) in loop 1 let tclDO n tac = let prefix i = str"At iteration " ++ int i ++ str": " in let tac_err_at i gl = - try tac gl + try Proofview.V82.of_tactic tac gl with | CErrors.UserError (l, s) as e -> let _, info = Exninfo.capture e in @@ -1105,11 +1129,15 @@ let tclDO n tac = let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in - loop 1 + Proofview.V82.tactic ~nf_evars:false (loop 1) + +let tclAT_LEAST_ONCE t = + let open Tacticals.New in + tclTHEN t (tclREPEAT t) let tclMULT = function - | 0, May -> tclREPEAT - | 1, May -> tclTRY + | 0, May -> Tacticals.New.tclREPEAT + | 1, May -> Tacticals.New.tclTRY | n, May -> tclDOTRY n | 0, Must -> tclAT_LEAST_ONCE | n, Must when n > 1 -> tclDO n @@ -1124,7 +1152,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = - let pat = interp_cpattern gl t None in (* UGLY API *) + let pat = interp_cpattern (pf_env gl) (project gl) t None in (* UGLY API *) let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in let (c, ucst), cl = @@ -1171,7 +1199,8 @@ let genclrtac cl cs clr = gl)) (old_cleartac clr) -let gentac gen gl = +let gentac gen = + Proofview.V82.tactic begin fun gl -> (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); @@ -1179,9 +1208,10 @@ let gentac gen gl = if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl else genclrtac cl [c] clr gl + end let genstac (gens, clr) = - tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens) + Tacticals.New.tclTHENLIST (cleartac clr :: List.rev_map gentac gens) let gen_tmp_ids ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl @@ -1191,7 +1221,7 @@ let gen_tmp_ids (tclTHENLIST (List.map (fun (id,orig_ref) -> tclTHEN - (gentac ((None,Some(false,[])),cpattern_of_id id)) + (Proofview.V82.of_tactic (gentac ((None,Some(false,[])),cpattern_of_id id))) (rename_hd_prod orig_ref)) ctx.tmp_ids) gl) ;; @@ -1214,24 +1244,6 @@ let pfLIFT f = Proofview.tclUNIT x ;; -(* TASSI: This version of unprotects inlines the unfold tactic definition, - * since we don't want to wipe out let-ins, and it seems there is no flag - * to change that behaviour in the standard unfold code *) -let unprotecttac gl = - let c, gl = pf_mkSsrConst "protect_term" gl in - let prot, _ = EConstr.destConst (project gl) c in - Tacticals.onClause (fun idopt -> - let hyploc = Option.map (fun id -> id, InHyp) idopt in - Proofview.V82.of_tactic (Tactics.reduct_option ~check:false - (Reductionops.clos_norm_flags - (CClosure.RedFlags.mkflags - [CClosure.RedFlags.fBETA; - CClosure.RedFlags.fCONST prot; - CClosure.RedFlags.fMATCH; - CClosure.RedFlags.fFIX; - CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)) - allHypsAndConcl gl - let is_protect hd env sigma = let _, protectC = mkSsrConst "protect_term" env sigma in EConstr.eq_constr_nounivs sigma hd protectC @@ -1259,7 +1271,7 @@ let abs_wgen keep_let f gen (gl,args,c) = gl, EConstr.mkVar x :: args, prod | _, Some ((x, "@"), Some p) -> let x = hoi_id x in - let cp = interp_cpattern gl p None in + let cp = interp_cpattern (pf_env gl) (project gl) p None in let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 @@ -1272,7 +1284,7 @@ let abs_wgen keep_let f gen (gl,args,c) = pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c) | _, Some ((x, _), Some p) -> let x = hoi_id x in - let cp = interp_cpattern gl p None in + let cp = interp_cpattern (pf_env gl) (project gl) p None in let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 @@ -1287,8 +1299,8 @@ let abs_wgen keep_let f gen (gl,args,c) = let clr_of_wgen gen clrs = match gen with | clr, Some ((x, _), None) -> let x = hoi_id x in - old_cleartac clr :: old_cleartac [SsrHyp(Loc.tag x)] :: clrs - | clr, _ -> old_cleartac clr :: clrs + cleartac clr :: cleartac [SsrHyp(Loc.tag x)] :: clrs + | clr, _ -> cleartac clr :: clrs let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast) @@ -1321,7 +1333,8 @@ end let tacREDUCE_TO_QUANTIFIED_IND ty = tacSIGMA >>= fun gl -> - tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty) + try tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty) + with e -> tclZERO e let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g -> let sigma, env = Goal.sigma g, Goal.env g in @@ -1460,7 +1473,7 @@ end let tacINTERP_CPATTERN cp = tacSIGMA >>= begin fun gl -> - tclUNIT (Ssrmatching.interp_cpattern gl cp None) + tclUNIT (Ssrmatching.interp_cpattern (pf_env gl) (project gl) cp None) end let tacUNIFY a b = @@ -1488,12 +1501,38 @@ let tclWITHTOP tac = Goal.enter begin fun gl -> Tactics.clear [top] end -let tacMK_SSR_CONST name = Goal.enter_one ~__LOC__ begin fun g -> - let sigma, env = Goal.(sigma g, env g) in - let sigma, c = mkSsrConst name env sigma in - Unsafe.tclEVARS sigma <*> - tclUNIT c -end +let tacMK_SSR_CONST name = + Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> + match mkSsrConst name env sigma with + | sigma, c -> Unsafe.tclEVARS sigma <*> tclUNIT c + | exception e when CErrors.noncritical e -> + tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null)) + +let tacDEST_CONST c = + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.destConst sigma c with + | c, _ -> tclUNIT c + | exception e when CErrors.noncritical e -> + tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null)) + +(* TASSI: This version of unprotects inlines the unfold tactic definition, + * since we don't want to wipe out let-ins, and it seems there is no flag + * to change that behaviour in the standard unfold code *) +let unprotecttac = + tacMK_SSR_CONST "protect_term" >>= tacDEST_CONST >>= fun prot -> + Tacticals.New.onClause (fun idopt -> + let hyploc = Option.map (fun id -> id, InHyp) idopt in + Tactics.reduct_option ~check:false + (Reductionops.clos_norm_flags + (CClosure.RedFlags.mkflags + [CClosure.RedFlags.fBETA; + CClosure.RedFlags.fCONST prot; + CClosure.RedFlags.fMATCH; + CClosure.RedFlags.fFIX; + CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc) + allHypsAndConcl + module type StateType = sig type state diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 3f92eab0bd..d1ad24496e 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -131,7 +131,8 @@ val pf_intern_term : ssrterm -> Glob_term.glob_constr val interp_term : - Tacinterp.interp_sign -> Goal.goal Evd.sigma -> + Environ.env -> Evd.evar_map -> + Tacinterp.interp_sign -> ssrterm -> evar_map * EConstr.t val interp_wit : @@ -145,7 +146,8 @@ val interp_refine : Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr) val interp_open_constr : - Tacinterp.interp_sign -> Goal.goal Evd.sigma -> + Environ.env -> Evd.evar_map -> + Tacinterp.interp_sign -> Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : @@ -153,7 +155,7 @@ val pf_e_type_of : EConstr.constr -> Goal.goal Evd.sigma * EConstr.types val splay_open_constr : - Goal.goal Evd.sigma -> + Environ.env -> evar_map * EConstr.t -> (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool @@ -179,8 +181,23 @@ val mk_internal_id : string -> Id.t val mk_tagged_id : string -> int -> Id.t val mk_evar_name : int -> Name.t val ssr_anon_hyp : string +val type_id : Environ.env -> Evd.evar_map -> EConstr.types -> Id.t val pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Id.t +val abs_evars : + Environ.env -> Evd.evar_map -> + evar_map * EConstr.t -> + int * EConstr.t * Evar.t list * + UState.t +val abs_evars2 : (* ssr2 *) + Environ.env -> Evd.evar_map -> Evar.t list -> + evar_map * EConstr.t -> + int * EConstr.t * Evar.t list * + UState.t +val abs_cterm : + Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t + + val pf_abs_evars : Goal.goal Evd.sigma -> evar_map * EConstr.t -> @@ -216,15 +233,8 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrConst : - string -> - env -> evar_map -> evar_map * EConstr.t -val pf_mkSsrConst : - string -> - Goal.goal Evd.sigma -> - EConstr.t * Goal.goal Evd.sigma -val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx +val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : GlobRef.t -> @@ -239,11 +249,14 @@ val ssrqid : string -> Libnames.qualid val new_tmp_id : tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx val mk_anon_id : string -> Id.t list -> Id.t +val abs_evars_pirrel : + Environ.env -> Evd.evar_map -> + evar_map * Constr.constr -> int * Constr.constr val pf_abs_evars_pirrel : Goal.goal Evd.sigma -> evar_map * Constr.constr -> int * Constr.constr -val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int -val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int +val nbargs_open_constr : Environ.env -> Evd.evar_map * EConstr.t -> int +val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> (Goal.goal * tac_ctx) Evd.sigma -> @@ -263,7 +276,7 @@ val red_product_skip_id : env -> evar_map -> EConstr.t -> EConstr.t val ssrautoprop_tac : - (Evar.t Evd.sigma -> Evar.t list Evd.sigma) ref + unit Proofview.tactic ref val mkProt : EConstr.t -> @@ -300,14 +313,15 @@ val pf_abs_ssrterm : val pf_interp_ty : ?resolve_typeclasses:bool -> + Environ.env -> + Evd.evar_map -> Tacinterp.interp_sign -> - Goal.goal Evd.sigma -> Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> int * EConstr.t * EConstr.t * UState.t -val ssr_n_tac : string -> int -> v82tac -val donetac : int -> v82tac +val ssr_n_tac : string -> int -> unit Proofview.tactic +val donetac : int -> unit Proofview.tactic val applyn : with_evars:bool -> @@ -315,7 +329,7 @@ val applyn : ?with_shelve:bool -> ?first_goes_last:bool -> int -> - EConstr.t -> v82tac + EConstr.t -> unit Proofview.tactic exception NotEnoughProducts val pf_saturate : ?beta:bool -> @@ -339,7 +353,7 @@ val refine_with : ?first_goes_last:bool -> ?beta:bool -> ?with_evars:bool -> - evar_map * EConstr.t -> v82tac + evar_map * EConstr.t -> unit Proofview.tactic val pf_resolve_typeclasses : where:EConstr.t -> @@ -350,18 +364,18 @@ val resolve_typeclasses : (*********************** Wrapped Coq tactics *****************************) -val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic +val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> unit Proofview.tactic type name_hint = (int * EConstr.types array) option ref val gentac : - Ssrast.ssrdocc * Ssrmatching.cpattern -> v82tac + Ssrast.ssrdocc * Ssrmatching.cpattern -> unit Proofview.tactic val genstac : ((Ssrast.ssrhyp list option * Ssrmatching.occ) * Ssrmatching.cpattern) list * Ssrast.ssrhyp list -> - Tacmach.tactic + unit Proofview.tactic val pf_interp_gen : bool -> @@ -378,7 +392,7 @@ val pfLIFT (** Basic tactics *) -val introid : ?orig:Name.t ref -> Id.t -> v82tac +val introid : ?orig:Name.t ref -> Id.t -> unit Proofview.tactic val intro_anon : v82tac val interp_clr : @@ -390,9 +404,9 @@ val genclrtac : val old_cleartac : ssrhyps -> v82tac val cleartac : ssrhyps -> unit Proofview.tactic -val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic +val tclMULT : int * ssrmmod -> unit Proofview.tactic -> unit Proofview.tactic -val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +val unprotecttac : unit Proofview.tactic val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool val abs_wgen : @@ -407,7 +421,7 @@ val abs_wgen : val clr_of_wgen : ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option -> - Proofview.V82.tac list -> Proofview.V82.tac list + unit Proofview.tactic list -> unit Proofview.tactic list val unfold : EConstr.t list -> unit Proofview.tactic diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index b44600a8cf..8e75ba7a2b 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -183,7 +183,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = else let c = Option.get oc in let gl, c_ty = pfe_type_of gl c in let pc = match c_gen with - | Some p -> interp_cpattern orig_gl p None + | Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None | _ -> mkTpat gl c in Some(c, c_ty, pc), gl in seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl @@ -233,7 +233,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in let pc = match n_c_args, c_gen with - | 0, Some p -> interp_cpattern orig_gl p None + | 0, Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None | _ -> mkTpat gl c in let cty = Some (c, c_ty, pc) in let elimty = Reductionops.whd_all env (project gl) elimty in @@ -312,7 +312,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let rec loop patterns clr i = function | [],[] -> patterns, clr, gl | ((oclr, occ), t):: deps, inf_t :: inf_deps -> - let p = interp_cpattern orig_gl t None in + let p = interp_cpattern (pf_env orig_gl) (project orig_gl) t None in let clr_t = interp_clr (project gl) (oclr,(tag_of_cpattern t,EConstr.of_constr (fst (redex_of_pattern env p)))) in (* if we are the index for the equation we do not clear *) @@ -392,10 +392,15 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let erefl = fire_subst gl erefl in let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in - let gen_eq_tac s = + let gen_eq_tac = + let open Proofview.Notations in + Proofview.Goal.enter begin fun s -> + let sigma = Proofview.Goal.sigma s in let open Evd in - let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in - apply_type new_concl [erefl] { s with sigma } + let sigma = merge_universe_context sigma (evar_universe_context (project gl)) in + Proofview.Unsafe.tclEVARS sigma <*> + Tactics.apply_type ~typecheck:true new_concl [erefl] + end in gen_eq_tac, eq_ty, gl in let rel = k + if c_is_head_p then 1 else 0 in @@ -403,7 +408,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl - | _ -> concl, Tacticals.tclIDTAC, clr, gl in + | _ -> concl, Tacticals.New.tclIDTAC, clr, gl in let mk_lam t r = EConstr.mkLambda_or_LetIn r t in let concl = List.fold_left mk_lam concl pred_rctx in let gl, concl = @@ -453,9 +458,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elim_tac = Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (refine_with ~with_evars:false elim); + refine_with ~with_evars:false elim; cleartac clr] in - let gen_eq_tac = Proofview.V82.tactic gen_eq_tac in Tacticals.New.tclTHENLIST [gen_eq_tac; elim_intro_tac ?seed:(Some seed) what eqid elim_tac is_rec clr] ;; @@ -467,19 +471,22 @@ let casetac x k = let k ?seed _what _eqid elim_tac _is_rec _clr = k ?seed elim_tac in ssrelim ~is_case:true [] (`EConstr ([],None,x)) None k -let pf_nb_prod gl = nb_prod (project gl) (pf_concl gl) - let rev_id = mk_internal_id "rev concl" let injecteq_id = mk_internal_id "injection equation" -let revtoptac n0 gl = - let n = pf_nb_prod gl - n0 in - let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in +let revtoptac n0 = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let n = nb_prod sigma concl - n0 in + let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) + end -let equality_inj l b id c gl = +let equality_inj l b id c = + Proofview.V82.tactic begin fun gl -> let msg = ref "" in try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with @@ -490,37 +497,53 @@ let equality_inj l b id c gl = !msg = "Nothing to inject." -> Feedback.msg_warning (Pp.str !msg); discharge_hyp (id, (id, "")) gl + end -let injectidl2rtac id c gl = - Tacticals.tclTHEN (equality_inj None true id c) (revtoptac (pf_nb_prod gl)) gl +let injectidl2rtac id c = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + Tacticals.New.tclTHEN (equality_inj None true id c) (revtoptac (nb_prod sigma concl)) + end let injectl2rtac sigma c = match EConstr.kind sigma c with | Var id -> injectidl2rtac id (EConstr.mkVar id, NoBindings) | _ -> let id = injecteq_id in - let xhavetac id c = Proofview.V82.of_tactic (Tactics.pose_proof (Name id) c) in - Tacticals.tclTHENLIST [xhavetac id c; injectidl2rtac id (EConstr.mkVar id, NoBindings); Proofview.V82.of_tactic (Tactics.clear [id])] + let xhavetac id c = Tactics.pose_proof (Name id) c in + Tacticals.New.tclTHENLIST [xhavetac id c; injectidl2rtac id (EConstr.mkVar id, NoBindings); Tactics.clear [id]] -let is_injection_case c gl = - let gl, cty = pfe_type_of gl c in - let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in +let is_injection_case env sigma c = + let sigma, cty = Typing.type_of env sigma c in + let (mind,_), _ = Tacred.reduce_to_quantified_ind env sigma cty in Coqlib.check_ind_ref "core.eq.type" mind -let perform_injection c gl = - let gl, cty = pfe_type_of gl c in - let mind, t = pf_reduce_to_quantified_ind gl cty in - let dc, eqt = EConstr.decompose_prod (project gl) t in - if dc = [] then injectl2rtac (project gl) c gl else - if not (EConstr.Vars.closed0 (project gl) eqt) then +let perform_injection c = + 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 sigma, cty = Typing.type_of env sigma c in + let mind, t = Tacred.reduce_to_quantified_ind env sigma cty in + let dc, eqt = EConstr.decompose_prod sigma t in + if dc = [] then injectl2rtac sigma c else + if not (EConstr.Vars.closed0 sigma eqt) then CErrors.user_err (Pp.str "can't decompose a quantified equality") else - let cl = pf_concl gl in let n = List.length dc in + let cl = Proofview.Goal.concl gl in + let n = List.length dc in let c_eq = mkEtaApp c n 2 in let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (EConstr.mkVar id, NoBindings) in - let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in - Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl + let injtac = Tacticals.New.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in + Proofview.Unsafe.tclEVARS sigma <*> + Tacticals.New.tclTHENLAST (Tactics.apply (EConstr.compose_lam dc cl1)) injtac + end -let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl -> - if is_injection_case c gl then perform_injection c gl - else Proofview.V82.of_tactic (casetac c (fun ?seed:_ k -> k)) gl) +let ssrscase_or_inj_tac c = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + if is_injection_case env sigma c then perform_injection c + else casetac c (fun ?seed:_ k -> k) + end diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 7b9cfed5ba..7f74fc78a2 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -41,10 +41,10 @@ val casetac : (?seed:Names.Name.t list array -> unit Proofview.tactic -> unit Proofview.tactic) -> unit Proofview.tactic -val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool +val is_injection_case : Environ.env -> Evd.evar_map -> EConstr.t -> bool val perform_injection : EConstr.constr -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic val ssrscase_or_inj_tac : EConstr.constr -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index d4303e9e8b..29a9c65561 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -42,29 +42,36 @@ let () = (* We must avoid zeta-converting any "let"s created by the "in" tactical. *) -let tacred_simpl gl = +let tacred_simpl env = let simpl_expr = Genredexpr.( Simpl(Redops.make_red_flag[FBeta;FMatch;FZeta;FDeltaBut []],None)) in - let esimpl, _ = Redexpr.reduction_of_red_expr (pf_env gl) simpl_expr in + let esimpl, _ = Redexpr.reduction_of_red_expr env simpl_expr in let esimpl e sigma c = let (_,t) = esimpl e sigma c in t in let simpl env sigma c = (esimpl env sigma c) in simpl -let safe_simpltac n gl = +let safe_simpltac n = if n = ~-1 then - let cl= red_safe (tacred_simpl gl) (pf_env gl) (project gl) (pf_concl gl) in - Proofview.V82.of_tactic (convert_concl_no_check cl) gl + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let cl = red_safe (tacred_simpl env) env sigma concl in + convert_concl_no_check cl + end else - ssr_n_tac "simpl" n gl + ssr_n_tac "simpl" n let simpltac = function | Simpl n -> safe_simpltac n - | Cut n -> tclTRY (donetac n) - | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (donetac n)) - | Nop -> tclIDTAC + | Cut n -> Tacticals.New.tclTRY (donetac n) + | SimplCut (n,m) -> Tacticals.New.tclTHEN (safe_simpltac m) (Tacticals.New.tclTRY (donetac n)) + | Nop -> Tacticals.New.tclIDTAC + +let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s) (** The "congr" tactic *) @@ -87,13 +94,13 @@ let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = ppdebug(lazy (Pp.str"===congr===")); ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); - let sigma, _ as it = interp_term ist gl t in + let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in let ist' = {ist with lfun = Id.Map.add pattern_id (Tacinterp.Value.of_constr f) Id.Map.empty } in let rf = mkRltacVar pattern_id in - let m = pf_nbargs gl f in + let m = pf_nbargs (pf_env gl) (project gl) f in let _, cf = if n > 0 then match interp_congrarg_at ist' gl n rf ty m with | Some cf -> cf @@ -105,14 +112,18 @@ let congrtac ((n, t), ty) ist gl = | Some cf -> cf | None -> loop (i + 1) in loop 1 in - tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl + Proofview.V82.of_tactic Tacticals.New.(tclTHEN (refine_with cf) (tclTRY Tactics.reflexivity)) gl let pf_typecheck t gl = let it = sig_it gl in let sigma,_ = pf_type_of gl t in re_sig [it] sigma -let newssrcongrtac arg ist gl = +let newssrcongrtac arg ist = + let open Proofview.Notations in + Proofview.Goal.enter_one ~__LOC__ begin fun _g -> + (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr -> + Proofview.V82.tactic begin fun gl -> ppdebug(lazy Pp.(str"===newcongr===")); ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) @@ -129,7 +140,6 @@ let newssrcongrtac arg ist gl = let sigma = Evd.create_evar_defs sigma in let (sigma, x) = Evarutil.new_evar env sigma ty in x, re_sig si sigma in - let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in (* here the two cases: simple equality or arrow *) @@ -150,6 +160,7 @@ let newssrcongrtac arg ist gl = ; congrtac (arg, mkRType) ist ]) (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow"))) gl + end (** 7. Rewriting tactics (rewrite, unlock) *) @@ -188,24 +199,28 @@ let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg = let norwmult = L2R, nomult let norwocc = noclr, None -let simplintac occ rdx sim gl = - let simptac m gl = +let simplintac occ rdx sim = + let simptac m = + Proofview.Goal.enter begin fun gl -> if m <> ~-1 then begin if rdx <> None then CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns"); if occ <> None then CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers"); - simpltac (Simpl m) gl + simpltac (Simpl m) end else - let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in + let sigma0, concl0, env0 = Proofview.Goal.(sigma gl, concl gl, env gl) in let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in - Proofview.V82.of_tactic - (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp))) - gl in + convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0) rdx occ simp)) + end + in + let open Tacticals.New in + Proofview.Goal.enter begin fun _ -> match sim with - | Simpl m -> simptac m gl - | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl - | _ -> simpltac sim gl + | Simpl m -> simptac m + | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) + | _ -> simpltac sim + end let rec get_evalref env sigma c = match EConstr.kind sigma c with | Var id -> EvalVarRef id @@ -233,7 +248,8 @@ let all_ok _ _ = true let fake_pmatcher_end () = mkProp, L2R, (Evd.empty, UState.empty, mkProp) -let unfoldintac occ rdx t (kt,_) gl = +let unfoldintac occ rdx t (kt,_) = + Proofview.V82.tactic begin fun gl -> let fs sigma x = Reductionops.nf_evar sigma x in let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let (sigma, t), const = strip_unfold_term env0 t kt in @@ -265,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) gl = | 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) @@ -286,9 +302,10 @@ let unfoldintac occ rdx t (kt,_) gl = with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in Proofview.V82.of_tactic (convert_concl ~check:true concl) gl -;; + end -let foldtac occ rdx ft gl = +let foldtac occ rdx ft = + Proofview.V82.tactic begin fun gl -> let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let sigma, t = ft in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in @@ -313,7 +330,7 @@ let foldtac occ rdx ft gl = let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in let _ = conclude () in Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl -;; + end let converse_dir = function L2R -> R2L | R2L -> L2R @@ -337,7 +354,8 @@ exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_e let id_map_redex _ sigma ~before:_ ~after = sigma, after -let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = +let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty = + Proofview.V82.tactic begin fun gl -> (* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) let env = pf_env gl in let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in @@ -369,8 +387,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ in ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); - try refine_with - ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl + try Proofview.V82.of_tactic (refine_with + ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with @@ -393,62 +411,73 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ | _ -> anomaly "rewrite rule not an application" in errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++ (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) -;; + end + +let pf_merge_uc_of s sigma = + Evd.merge_universe_context sigma (Evd.evar_universe_context s) -let rwcltac ?under ?map_redex cl rdx dir sr gl = +let rwcltac ?under ?map_redex cl rdx dir sr = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma0 = Proofview.Goal.sigma gl in let sr = let sigma, r = sr in - let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in + let sigma = resolve_typeclasses ~where:r ~fail:false env sigma in sigma, r in - let n, r_n,_, ucst = pf_abs_evars gl sr in - let r_n' = pf_abs_cterm gl n r_n in + let n, r_n,_, ucst = abs_evars env sigma0 sr in + let r_n' = abs_cterm env sigma0 n r_n in let r' = EConstr.Vars.subst_var pattern_id r_n' in - let gl = pf_unsafe_merge_uc ucst gl in - let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in + let sigma0 = Evd.set_universe_context sigma0 ucst in + let rdxt = Retyping.get_type_of env (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); - let cvtac, rwtac, gl = - if EConstr.Vars.closed0 (project gl) r' then - let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in + ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); + let cvtac, rwtac, sigma0 = + if EConstr.Vars.closed0 sigma0 r' then + let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); let open EConstr in match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in - pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl + pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, Tacticals.New.tclIDTAC, sigma0 | _ -> let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in - let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl + let sigma0 = pf_merge_uc_of sigma sigma0 in + convert_concl ~check:true cl', rewritetac ?under dir r', sigma0 else - let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in + let dc, r2 = EConstr.decompose_lam_n_assum sigma0 n r' in let r3, _, r3t = - try EConstr.destCast (project gl) r2 with _ -> - errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr) - ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in + try EConstr.destCast sigma0 r2 with _ -> + errorstrm Pp.(str "no cast from " ++ pr_econstr_pat env sigma0 (snd sr) + ++ str " to " ++ pr_econstr_env env sigma0 r2) in let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in - let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in + let cltac = Tactics.clear [pattern_id; rule_id] in let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in - apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl + Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0 in - let cvtac' _ = - try cvtac gl with - | PRtype_error e -> + let cvtac' = + Proofview.tclOR cvtac begin function + | (PRtype_error e, _) -> let error = Option.cata (fun (env, sigma, te) -> Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te)) (Pp.mt ()) e in - if occur_existential (project gl) (Tacmach.pf_concl gl) - then errorstrm Pp.(str "Rewriting impacts evars" ++ error) - else errorstrm Pp.(str "Dependent type error in rewrite of " - ++ pr_econstr_env (pf_env gl) (project gl) + if occur_existential sigma0 (Tacmach.New.pf_concl gl) + then Tacticals.New.tclZEROMSG Pp.(str "Rewriting impacts evars" ++ error) + else Tacticals.New.tclZEROMSG Pp.(str "Dependent type error in rewrite of " + ++ pr_econstr_env env sigma0 (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl) ++ error) + | (e, info) -> Proofview.tclZERO ~info e + end in - tclTHEN cvtac' rwtac gl + Proofview.Unsafe.tclEVARS sigma0 <*> + Tacticals.New.tclTHEN cvtac' rwtac + end [@@@ocaml.warning "-3"] let lz_coq_prod = @@ -474,21 +503,20 @@ let ssr_is_setoid env = Rewrite.is_applied_rewrite_relation env sigma [] (EConstr.mkApp (r, args)) <> None -let closed0_check cl p gl = +let closed0_check env sigma cl p = if closed0 cl then - errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p) + errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env env sigma p) let dir_org = function L2R -> 1 | R2L -> 2 -let rwprocess_rule dir rule gl = - let env = pf_env gl in +let rwprocess_rule env dir rule = let coq_prod = lz_coq_prod () in let is_setoid = ssr_is_setoid env in let r_sigma, rules = 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) -> @@ -558,15 +586,17 @@ let rwprocess_rule dir rule gl = in r_sigma, rules -let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = - let env = pf_env gl in - let r_sigma, rules = rwprocess_rule dir rule gl in +let rwrxtac ?under ?map_redex occ rdx_pat dir rule = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma0 = Proofview.Goal.sigma gl in + let r_sigma, rules = rwprocess_rule env dir rule in let find_rule rdx = let rec rwtac = function | [] -> - errorstrm Pp.(str "pattern " ++ pr_econstr_pat env (project gl) rdx ++ + errorstrm Pp.(str "pattern " ++ pr_econstr_pat env sigma0 rdx ++ str " does not match " ++ pr_dir_side dir ++ - str " of " ++ pr_econstr_pat env (project gl) (snd rule)) + str " of " ++ pr_econstr_pat env sigma0 (snd rule)) | (d, r, lhs, rhs) :: rs -> try let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in @@ -574,7 +604,8 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r) with _ -> rwtac rs in rwtac rules in - let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in + let env0 = env in + let concl0 = Proofview.Goal.concl gl in let find_R, conclude = match rdx_pat with | Some (_, (In_T _ | In_X_In_T _)) | None -> let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in @@ -586,23 +617,26 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), - fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx + fun cl -> let rdx,d,r = end_R () in closed0_check env0 sigma0 cl rdx; (d,r),rdx | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) -> let r = ref None in (fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h), - (fun concl -> closed0_check concl e gl; + (fun concl -> closed0_check env0 sigma0 concl e; let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in - let concl0 = EConstr.Unsafe.to_constr concl0 in + let concl0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in - rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl -;; - -let ssrinstancesofrule ist dir arg gl = - let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in - let rule = interp_term ist gl arg in - let r_sigma, rules = rwprocess_rule dir rule gl in + rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r + end + +let ssrinstancesofrule ist dir arg = + Proofview.Goal.enter begin fun gl -> + let env0 = Proofview.Goal.env gl in + let sigma0 = Proofview.Goal.sigma gl in + let concl0 = Proofview.Goal.concl gl in + let rule = interp_term env0 sigma0 ist arg in + let r_sigma, rules = rwprocess_rule env0 dir rule in let find, conclude = let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = @@ -619,33 +653,47 @@ let ssrinstancesofrule ist dir arg gl = Feedback.msg_info Pp.(str"BEGIN INSTANCES"); try while true do - ignore(find env0 (EConstr.Unsafe.to_constr concl0) 1 ~k:print) + ignore(find env0 (EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0) 1 ~k:print) done; raise NoMatch - with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl - -let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl - -let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = + with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC + end + +let ipat_rewrite occ dir c = Proofview.Goal.enter begin fun gl -> + rwrxtac occ None dir (Proofview.Goal.sigma gl, c) +end + +let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) = + 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 fail = ref false in - let interp_rpattern gl gc = - try interp_rpattern gl gc - with _ when snd mult = May -> fail := true; project gl, T mkProp in - let interp gc gl = - try interp_term ist gl gc - with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in - let rwtac gl = - let rx = Option.map (interp_rpattern gl) grx in - let gl = match rx with - | None -> gl - | Some (s,_) -> pf_merge_uc_of s gl in - let t = interp gt gl in - let gl = pf_merge_uc_of (fst t) gl in + let interp_rpattern env sigma gc = + try interp_rpattern env sigma gc + with _ when snd mult = May -> fail := true; sigma, T mkProp in + let interp env sigma gc = + try interp_term env sigma ist gc + with _ when snd mult = May -> fail := true; (sigma, EConstr.mkProp) in + let rwtac = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let rx = Option.map (interp_rpattern env sigma) grx in + let sigma = match rx with + | None -> sigma + | Some (s,_) -> pf_merge_uc_of s sigma in + let t = interp env sigma gt in + let sigma = pf_merge_uc_of (fst t) sigma in + Proofview.Unsafe.tclEVARS sigma <*> (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt - | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in - let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in - if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl + | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) + end + in + let ctac = cleartac (interp_clr sigma (oclr, (fst gt, snd (interp env sigma gt)))) in + if !fail then ctac else Tacticals.New.tclTHEN (tclMULT mult rwtac) ctac + end (** Rewrite argument sequence *) @@ -654,24 +702,37 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) (** The "rewrite" tactic *) let ssrrewritetac ?under ?map_redex ist rwargs = - tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) + Proofview.Goal.enter begin fun _ -> + Tacticals.New.tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) + end (** The "unlock" tactic *) -let unfoldtac occ ko t kt gl = - let env = pf_env gl in - let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in - let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in +let unfoldtac occ ko t kt = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let concl = Evarutil.nf_evar sigma concl in + let cl, c = fill_occ_term env sigma concl occ (fst (strip_unfold_term env t kt)) in + let cl' = EConstr.Vars.subst1 (Tacred.unfoldn [OnlyOccurrences [1], get_evalref env sigma c] env sigma c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in - Proofview.V82.of_tactic - (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl - -let unlocktac ist args gl = - let utac (occ, gt) gl = - unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in - let locked, gl = pf_mkSsrConst "locked" gl in - let key, gl = pf_mkSsrConst "master_key" gl in + convert_concl ~check:true (Reductionops.clos_norm_flags f env sigma cl') + end + +let unlocktac ist args = + let open Proofview.Notations in + let utac (occ, gt) = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + unfoldtac occ occ (interp_term env sigma ist gt) (fst gt) + end + in + Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked -> + Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key -> let ktacs = [ - (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); - Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in - tclTHENLIST (List.map utac args @ ktacs) gl + (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens); + Ssrelim.casetac key (fun ?seed:_ k -> k) + ] in + Tacticals.New.tclTHENLIST (List.map utac args @ ktacs) diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 0bb67c99db..1c3b1bb018 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -26,12 +26,12 @@ val mkclr : ssrclear -> ssrdocc val nodocc : ssrdocc val noclr : ssrdocc -val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic +val simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic val newssrcongrtac : int * Ssrast.ssrterm -> Ltac_plugin.Tacinterp.interp_sign -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic val mk_rwarg : @@ -49,7 +49,7 @@ val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> Ssrast.ssrterm -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic (* map_redex (by default the identity on after) is called on the * redex (before) and its replacement (after). It is used to @@ -59,11 +59,11 @@ val ssrrewritetac : ?map_redex:(Environ.env -> Evd.evar_map -> before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) -> Ltac_plugin.Tacinterp.interp_sign -> - ssrrwarg list -> Tacmach.tactic + ssrrwarg list -> unit Proofview.tactic -val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic +val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> unit Proofview.tactic val unlocktac : Ltac_plugin.Tacinterp.interp_sign -> (Ssrmatching.occ * Ssrast.ssrterm) list -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 43b527c32b..4961138190 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -28,19 +28,22 @@ module RelDecl = Context.Rel.Declaration let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) -let ssrposetac (id, (_, t)) gl = +let ssrposetac (id, (_, t)) = + Proofview.V82.tactic begin fun gl -> let ist, t = match t.Ssrast.interp_env with | Some ist -> ist, Ssrcommon.ssrterm_of_ast_closure_term t | None -> assert false in let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) + end -let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = +let ssrsettac id ((_, (pat, pty)), (_, occ)) = + Proofview.V82.tactic begin fun gl -> let pty = Option.map (fun { Ssrast.body; interp_env } -> let ist = Option.get interp_env in (mkRHole, Some body), ist) pty in - let pat = interp_cpattern gl pat pty in + let pat = interp_cpattern (pf_env gl) (project gl) pat pty in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in let (c, ucst), cl = let cl = EConstr.Unsafe.to_constr cl in @@ -56,7 +59,8 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in - Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl + Proofview.V82.of_tactic (Tacticals.New.tclTHEN (convert_concl ~check:true cl') (introid id)) gl + end open Util @@ -85,18 +89,30 @@ let combineCG t1 t2 f g = match t1, t2 with | _, (_, (_, None)) -> anomaly "have: mixed C-G constr" | _ -> anomaly "have: mixed G-C constr" -let basecuttac name c gl = - let hd, gl = pf_mkSsrConst name gl in - let t = EConstr.mkApp (hd, [|c|]) in - let gl, _ = pf_e_type_of gl t in - Proofview.V82.of_tactic (Tactics.apply t) gl +let basecuttac name t = + let open Proofview.Notations in + Ssrcommon.tacMK_SSR_CONST name >>= fun hd -> + let t = EConstr.mkApp (hd, [|t|]) in + Ssrcommon.tacTYPEOF t >>= fun _ty -> + Tactics.apply t -let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) +let evarcuttac name cs = + let open Proofview.Notations in + Ssrcommon.tacMK_SSR_CONST name >>= fun hd -> + let t = EConstr.mkApp (hd, cs) in + Ssrcommon.tacTYPEOF t >>= fun _ty -> + applyn ~with_evars:true ~with_shelve:false (Array.length cs) t + +let introstac ipats = tclIPAT ipats let havetac ist (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint))) - suff namefst gl + suff namefst = + let open Proofview.Notations in + Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key -> + Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract -> + Proofview.V82.tactic begin fun gl -> let concl = pf_concl gl in let pats = tclCompileIPats orig_pats in let binders = tclCompileIPats binders in @@ -108,34 +124,30 @@ let havetac ist match clr with | None -> introstac pats, [] | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in - let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in + let itac, id, clr = introstac pats, Tacticals.New.tclIDTAC, cleartac clr in let binderstac n = let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in - Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) + Tacticals.New.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.New.tclIDTAC) (introstac binders) in let simpltac = introstac simpl in let fixtc = not !ssrhaveNOtcresolution && match fk with FwdHint(_,true) -> false | _ -> true in let hint = hinttac ist true hint in - let cuttac t gl = - if transp then - let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in - let step = EConstr.mkApp (have_let, [|concl;t|]) in - let gl, _ = pf_e_type_of gl step in - applyn ~with_evars:true ~with_shelve:false 2 step gl - else basecuttac "ssr_have" t gl in + let cuttac t = Proofview.Goal.enter begin fun gl -> + if transp then evarcuttac "ssr_have_let" [|concl;t|] + else basecuttac "ssr_have" t + end in (* Introduce now abstract constants, so that everything sees them *) - let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in let unlock_abs (idty,args_id) gl = let gl, _ = pf_e_type_of gl idty in pf_unify_HO gl args_id.(2) abstract_key in - Tacticals.tclTHENFIRST itac_mkabs (fun gl -> + Tacticals.tclTHENFIRST (Proofview.V82.of_tactic itac_mkabs) (fun gl -> let mkt t = mk_term xNoFlag t in let mkl t = (xNoFlag, (t, None)) in let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in let interp_ty gl rtc t = - let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in + let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in let open CAst in let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) -> @@ -163,7 +175,7 @@ let havetac ist try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in - gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c + gl, ty, Tacticals.New.tclTHEN (Proofview.V82.tactic assert_is_conv) (Tactics.apply t), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function | IOpAbstractVars ids -> ids @@ -181,13 +193,12 @@ let havetac ist let gs = List.map (fun (_,a) -> Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in - let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in + let tacopen_skols = Proofview.V82.tactic (fun gl -> re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma) in let gl, ty = pf_e_type_of gl t in - gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id, - Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac) - (Tacticals.tclTHEN tacopen_skols (fun gl -> - let abstract, gl = pf_mkSsrConst "abstract" gl in - Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)) + gl, ty, Tactics.apply t, id, + Tacticals.New.tclTHEN (Tacticals.New.tclTHEN itac_c simpltac) + (Tacticals.New.tclTHEN tacopen_skols (Proofview.V82.tactic (fun gl -> + Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl))) | _,true,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, itac, clr @@ -196,11 +207,11 @@ let havetac ist gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c | _, false, false -> let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in - gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac + gl, cty, Tacticals.New.tclTHEN (binderstac n) hint, id, Tacticals.New.tclTHEN itac_c simpltac | _, true, false -> assert false in - Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl) + Proofview.V82.of_tactic (Tacticals.New.tclTHENS (cuttac cut) [ Tacticals.New.tclTHEN sol itac1; itac2 ]) gl) gl -;; +end let destProd_or_LetIn sigma c = match EConstr.kind sigma c with @@ -208,7 +219,8 @@ let destProd_or_LetIn sigma c = | LetIn (n,bo,ty,c) -> RelDecl.LocalDef (n, bo, ty), c | _ -> raise DestKO -let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = +let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave = + Proofview.V82.tactic begin fun gl -> let clr0 = Option.default [] clr0 in let pats = tclCompileIPats pats in let mkabs gen = abs_wgen false (fun x -> x) gen in @@ -243,7 +255,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let (sigma, ev) = Evarutil.new_evar env sigma EConstr.mkProp in let k, _ = EConstr.destEvar sigma ev in let fake_gl = {Evd.it = k; Evd.sigma = sigma} in - let _, ct, _, uc = pf_interp_ty ist fake_gl ct in + let _, ct, _, uc = pf_interp_ty (pf_env fake_gl) sigma ist ct in let rec var2rel c g s = match EConstr.kind sigma c, g with | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c) | Sort _, [] -> EConstr.Vars.subst_vars s ct @@ -260,39 +272,40 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac pats in let tacigens = - Tacticals.tclTHEN - (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0]))) + Tacticals.New.tclTHEN + (Tacticals.New.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0]))) (introstac (List.fold_right mkpats gens [])) in let hinttac = hinttac ist true hint in let cut_kind, fst_goal_tac, snd_goal_tac = match suff, ghave with - | true, `NoGen -> "ssr_wlog", Tacticals.tclTHEN hinttac (tacipat pats), tacigens - | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.tclTHEN tacigens (tacipat pats) + | true, `NoGen -> "ssr_wlog", Tacticals.New.tclTHEN hinttac (tacipat pats), tacigens + | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.New.tclTHEN tacigens (tacipat pats) | true, `Gen _ -> assert false | false, `Gen id -> if gens = [] then errorstrm(str"gen have requires some generalizations"); - let clear0 = old_cleartac clr0 in + let clear0 = cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with | None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats - | None, _ -> None, Tacticals.tclIDTAC, clear0, pats + | None, _ -> None, Tacticals.New.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> let id = mk_anon_id "tmp" (Tacmach.pf_ids_of_hyps gl) in - Some id, introid id, Tacticals.tclTHEN clear0 (Proofview.V82.of_tactic (Tactics.clear [id])), pats in + Some id, introid id, Tacticals.New.tclTHEN clear0 (Tactics.clear [id]), pats in let tac_specialize = match id with - | None -> Tacticals.tclIDTAC + | None -> Tacticals.New.tclIDTAC | Some id -> - if pats = [] then Tacticals.tclIDTAC else + if pats = [] then Tacticals.New.tclIDTAC else let args = Array.of_list args in ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); - Tacticals.tclTHENS (basecuttac "ssr_have" ct) - [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in + Tacticals.New.tclTHENS (basecuttac "ssr_have" ct) + [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in "ssr_have", (if hint = nohint then tacigens else hinttac), - Tacticals.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup] + Tacticals.New.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup] in - Tacticals.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl + Proofview.V82.of_tactic (Tacticals.New.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac]) gl + end (** The "suffice" tactic *) @@ -301,7 +314,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let pats = tclCompileIPats pats in let binders = tclCompileIPats binders in let simpl = tclCompileIPats simpl in - let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in + let htac = Tacticals.New.tclTHEN (introstac pats) (hinttac ist true hint) in let c = match Ssrcommon.ssrterm_of_ast_closure_term c with | (a, (b, Some ct)) -> begin match ct.CAst.v with @@ -314,10 +327,12 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = | _ -> anomaly "suff: ssr cast hole deleted by typecheck" end in - let ctac gl = - let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in - basecuttac "ssr_suff" ty gl in - Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))] + let ctac = + Proofview.V82.tactic begin fun gl -> + let _,ty,_,uc = pf_interp_ty (pf_env gl) (project gl) ist c in let gl = pf_merge_uc uc gl in + Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl + end in + Tacticals.New.tclTHENS ctac [htac; Tacticals.New.tclTHEN (cleartac clr) (introstac (binders@simpl))] open Proofview.Notations @@ -340,16 +355,14 @@ let intro_lock ipats = Proofview.tclDISPATCH (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in let protect_subgoal env sigma hd args = + Ssrcommon.tacMK_SSR_CONST "Under_rel" >>= fun under_rel -> + Ssrcommon.tacMK_SSR_CONST "Under_rel_from_rel" >>= fun under_from_rel -> Tactics.New.refine ~typecheck:true (fun sigma -> let lm2 = Array.length args - 2 in let sigma, carrier = Typing.type_of env sigma args.(lm2) in let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in let rel_args = Array.sub args lm2 2 in - let sigma, under_rel = - Ssrcommon.mkSsrConst "Under_rel" env sigma in - let sigma, under_from_rel = - Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in let under_rel_args = Array.append [|carrier; rel|] rel_args in let ty = EConstr.mkApp (under_rel, under_rel_args) in let sigma, t = Evarutil.new_evar env sigma ty in @@ -408,7 +421,7 @@ let pretty_rename evar_map term varnames = in aux term varnames -let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1) +let overtac = ssr_n_tac "over" ~-1 let check_numgoals ?(minus = 0) nh = Proofview.numgoals >>= fun ng -> @@ -492,7 +505,6 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = @ [betaiota]) in let rew = - Proofview.V82.tactic - (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) + Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule] in rew <*> intro_lock ipats <*> undertacs diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 8aacae39af..33bf56cfa9 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -16,9 +16,9 @@ open Ltac_plugin open Ssrast -val ssrsettac : Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> v82tac +val ssrsettac : Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> unit Proofview.tactic -val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac +val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> unit Proofview.tactic val havetac : ist -> bool * @@ -27,11 +27,9 @@ val havetac : ist -> (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) * (bool * Tacinterp.Value.t option list))) -> bool -> - bool -> v82tac + bool -> unit Proofview.tactic -val basecuttac : - string -> - EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma +val basecuttac : string -> EConstr.t -> unit Proofview.tactic val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> @@ -46,7 +44,7 @@ val wlogtac : Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> bool -> [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic val sufftac : Ssrast.ist -> @@ -55,7 +53,7 @@ val sufftac : (('a * ast_closure_term) * (bool * Tacinterp.Value.t option list)) -> - Tacmach.tactic + unit Proofview.tactic (* pad_intro (by default false) indicates whether the intro-pattern "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches, diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1edec8e8a0..46f90a7ee1 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -191,7 +191,7 @@ let isGEN_PUSH dg = (* generalize `id` as `new_name` *) let gen_astac id new_name = let gen = ((None,Some(false,[])),Ssrmatching.cpattern_of_id id) in - V82.tactic (Ssrcommon.gentac gen) + Ssrcommon.gentac gen <*> Ssrcommon.tclRENAME_HD_PROD new_name (* performs and resets all delayed generalizations *) @@ -337,7 +337,7 @@ let tac_case t = Ssrcommon.tacTYPEOF t >>= fun ty -> Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj -> if is_inj then - V82.tactic ~nf_evars:false (Ssrelim.perform_injection t) + Ssrelim.perform_injection t else Goal.enter begin fun g -> (Ssrelim.casetac t (fun ?seed k -> @@ -384,13 +384,11 @@ end let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let env, concl = Goal.(env gl, concl gl) in - let step = begin fun sigma -> + let step ablock abstract = begin fun sigma -> let (sigma, (abstract_proof, abstract_ty)) = let (sigma, (ty, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in - let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in let (sigma, lock) = Evarutil.new_evar env sigma ablock in - let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in let (sigma, abstract_id) = mk_abstract_id env sigma in let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in let sigma, m = Evarutil.new_evar env sigma abstract_ty in @@ -405,7 +403,9 @@ let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let sigma, _ = Typing.type_of env sigma term in sigma, term end in - Tactics.New.refine ~typecheck:false step <*> + Ssrcommon.tacMK_SSR_CONST "abstract_lock" >>= fun ablock -> + Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract -> + Tactics.New.refine ~typecheck:false (step ablock abstract) <*> tclFOCUS 1 3 Proofview.shelve end @@ -477,7 +477,7 @@ let rec ipat_tac1 ipat : bool tactic = | IOpInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP - (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) + (fun t -> Ssrelim.perform_injection t)) ipatss <*> notTAC @@ -494,11 +494,11 @@ let rec ipat_tac1 ipat : bool tactic = notTAC | IOpSimpl x -> - V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC + Ssrequality.simpltac x <*> notTAC | IOpRewrite (occ,dir) -> Ssrcommon.tclWITHTOP - (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC + (fun x -> Ssrequality.ipat_rewrite occ dir x) <*> notTAC | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC @@ -622,7 +622,7 @@ end let with_dgens { dgens; gens; clr } maintac = match gens with | [] -> with_defective maintac dgens clr | gen :: gens -> - V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen + Ssrcommon.genstac (gens, clr) <*> maintac dgens gen let mkCoqEq env sigma = let eq = Coqlib.((build_coq_eq_data ()).eq) in @@ -647,7 +647,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = | ProdType (_, src, tgt) -> begin match kind_of_type sigma src with | AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> - V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*> + Ssrcommon.unprotecttac <*> Ssrcommon.tclINTRO_ID ipat | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq () end @@ -700,7 +700,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = | _ -> tclUNIT () in let unprotect = if eqid <> None && is_rec - then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in + then Ssrcommon.unprotecttac else tclUNIT () in begin match seed with | None -> ssrelim | Some s -> IpatMachine.tclSEED_SUBGOALS s ssrelim end <*> @@ -727,7 +727,7 @@ let mkEq dir cl c t n env sigma = let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Ssrcommon.tacSIGMA >>= fun sigma0 -> Goal.enter_one begin fun g -> - let pat = Ssrmatching.interp_cpattern sigma0 t None in + let pat = Ssrmatching.interp_cpattern (Tacmach.pf_env sigma0) (Tacmach.project sigma0) t None in let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in let (c, ucst), cl = @@ -816,7 +816,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) = Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj -> let simple = (eqid = None && deps = [] && occ = None) in if simple && inj then - V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*> + Ssrelim.perform_injection vc <*> Tactics.clear (List.map Ssrcommon.hyp_id clear) <*> tclIPATssr ipats else @@ -870,7 +870,7 @@ let tclIPAT ip = let ssrmovetac = function | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) -> - let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in + let gentac = Ssrcommon.genstac (gens, []) in let conclusion _ t clear ccl = Tactics.apply_type ~typecheck:true ccl [t] <*> Tactics.clear (List.map Ssrcommon.hyp_id clear) in @@ -884,7 +884,7 @@ let ssrmovetac = function let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats)) | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> - let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in + let gentac = Ssrcommon.genstac (gens, clr) in gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats) | _, (_, ({ clr }, ipats)) -> Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)] @@ -985,7 +985,7 @@ let ssrabstract dgens = Ssrcommon.tacSIGMA >>= fun gl0 -> let open Ssrmatching in let ipats = List.map (fun (_,cp) -> - match id_of_pattern (interp_cpattern gl0 cp None) with + match id_of_pattern (interp_cpattern (Tacmach.pf_env gl0) (Tacmach.project gl0) cp None) with | None -> IPatAnon (One None) | Some id -> IPatId id) (List.tl gens) in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 442b40221b..60af804c1b 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -349,8 +349,8 @@ let interp_index ist gl idx = begin match Tacinterp.Value.to_constr v with | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in - begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral n when NumTok.Signed.is_int n -> + begin match Notation.uninterp_prim_token rc (None, []) with + | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n -> int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end @@ -1611,17 +1611,6 @@ let tactic_expr = Pltac.tactic_expr (** 1. Utilities *) -(** Tactic-level diagnosis *) - -(* debug *) - -{ - -(* Let's play with the new proof engine API *) -let old_tac = V82.tactic - -} - (** Name generation *) (* Since Coq now does repeated internal checks of its external lexical *) @@ -1731,18 +1720,20 @@ END { -let ssrautoprop gl = +let ssrautoprop = + Proofview.Goal.enter begin fun gl -> try let tacname = try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in - V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl - with Not_found -> V82.of_tactic (Auto.full_trivial []) gl + eval_tactic (Tacexpr.TacArg tacexpr) + with Not_found -> Auto.full_trivial [] + end let () = ssrautoprop_tac := ssrautoprop -let tclBY tac = Tacticals.tclTHEN tac (donetac ~-1) +let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1) (** Tactical arguments. *) @@ -1760,7 +1751,7 @@ open Ssrfwd } TACTIC EXTEND ssrtclby -| [ "by" ssrhintarg(tac) ] -> { V82.tactic (hinttac ist true tac) } +| [ "by" ssrhintarg(tac) ] -> { hinttac ist true tac } END (* We can't parse "by" in ARGUMENT EXTEND because it will only be made *) @@ -1778,7 +1769,7 @@ END let () = register_ssrtac "tcldo" begin fun args ist -> match args with | [arg] -> let arg = cast_arg wit_ssrdoarg arg in - V82.tactic (ssrdotac ist arg) + ssrdotac ist arg | _ -> assert false end @@ -1827,7 +1818,7 @@ let () = register_ssrtac "tclseq" begin fun args ist -> match args with let tac = cast_arg wit_ssrtclarg tac in let dir = cast_arg wit_ssrseqdir dir in let arg = cast_arg wit_ssrseqarg arg in - V82.tactic (tclSEQAT ist tac dir arg) + tclSEQAT ist tac dir arg | _ -> assert false end @@ -2191,9 +2182,9 @@ let vmexacttac pf = TACTIC EXTEND ssrexact | [ "exact" ssrexactarg(arg) ] -> { let views, (gens_clr, _) = arg in - V82.tactic (tclBY (V82.of_tactic (inner_ssrapplytac views gens_clr ist))) } + tclBY (inner_ssrapplytac views gens_clr ist) } | [ "exact" ] -> { - V82.tactic (Tacticals.tclORELSE (donetac ~-1) (tclBY (V82.of_tactic apply_top_tac))) } + Tacticals.New.tclORELSE (donetac ~-1) (tclBY apply_top_tac) } | [ "exact" "<:" lconstr(pf) ] -> { vmexacttac pf } END @@ -2220,9 +2211,9 @@ END TACTIC EXTEND ssrcongr | [ "congr" ssrcongrarg(arg) ] -> { let arg, dgens = arg in - V82.tactic begin + Proofview.Goal.enter begin fun _ -> match dgens with - | [gens], clr -> Tacticals.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist) + | [gens], clr -> Tacticals.New.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist) | _ -> errorstrm (str"Dependent family abstractions not allowed in congr") end } END @@ -2342,10 +2333,10 @@ ARGUMENT EXTEND ssrrwarg END TACTIC EXTEND ssrinstofruleL2R -| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist L2R arg) } +| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> { ssrinstancesofrule ist L2R arg } END TACTIC EXTEND ssrinstofruleR2L -| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist R2L arg) } +| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> { ssrinstancesofrule ist R2L arg } END (** Rewrite argument sequence *) @@ -2395,7 +2386,7 @@ END TACTIC EXTEND ssrrewrite | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] -> - { tclCLAUSES (old_tac (ssrrewritetac ist args)) clauses } + { tclCLAUSES (ssrrewritetac ist args) clauses } END (** The "unlock" tactic *) @@ -2426,16 +2417,16 @@ END TACTIC EXTEND ssrunlock | [ "unlock" ssrunlockargs(args) ssrclauses(clauses) ] -> - { tclCLAUSES (old_tac (unlocktac ist args)) clauses } + { tclCLAUSES (unlocktac ist args) clauses } END (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) TACTIC EXTEND ssrpose -| [ "pose" ssrfixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) } -| [ "pose" ssrcofixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) } -| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> { V82.tactic (ssrposetac (id, fwd)) } +| [ "pose" ssrfixfwd(ffwd) ] -> { ssrposetac ffwd } +| [ "pose" ssrcofixfwd(ffwd) ] -> { ssrposetac ffwd } +| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> { ssrposetac (id, fwd) } END (** The "set" tactic *) @@ -2444,7 +2435,7 @@ END TACTIC EXTEND ssrset | [ "set" ssrfwdid(id) ssrsetfwd(fwd) ssrclauses(clauses) ] -> - { tclCLAUSES (old_tac (ssrsettac id fwd)) clauses } + { tclCLAUSES (ssrsettac id fwd) clauses } END (** The "have" tactic *) @@ -2471,27 +2462,27 @@ END TACTIC EXTEND ssrhave | [ "have" ssrhavefwdwbinders(fwd) ] -> - { V82.tactic (havetac ist fwd false false) } + { havetac ist fwd false false } END TACTIC EXTEND ssrhavesuff | [ "have" "suff" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - { V82.tactic (havetac ist (false,(pats,fwd)) true false) } + { havetac ist (false,(pats,fwd)) true false } END TACTIC EXTEND ssrhavesuffices | [ "have" "suffices" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - { V82.tactic (havetac ist (false,(pats,fwd)) true false) } + { havetac ist (false,(pats,fwd)) true false } END TACTIC EXTEND ssrsuffhave | [ "suff" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - { V82.tactic (havetac ist (false,(pats,fwd)) true true) } + { havetac ist (false,(pats,fwd)) true true } END TACTIC EXTEND ssrsufficeshave | [ "suffices" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - { V82.tactic (havetac ist (false,(pats,fwd)) true true) } + { havetac ist (false,(pats,fwd)) true true } END (** The "suffice" tactic *) @@ -2515,11 +2506,11 @@ END TACTIC EXTEND ssrsuff -| [ "suff" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) } +| [ "suff" ssrsufffwd(fwd) ] -> { sufftac ist fwd } END TACTIC EXTEND ssrsuffices -| [ "suffices" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) } +| [ "suffices" ssrsufffwd(fwd) ] -> { sufftac ist fwd } END (** The "wlog" (Without Loss Of Generality) tactic *) @@ -2541,34 +2532,34 @@ END TACTIC EXTEND ssrwlog | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - { V82.tactic (wlogtac ist pats fwd hint false `NoGen) } + { wlogtac ist pats fwd hint false `NoGen } END TACTIC EXTEND ssrwlogs | [ "wlog" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } + { wlogtac ist pats fwd hint true `NoGen } END TACTIC EXTEND ssrwlogss | [ "wlog" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> - { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } + { wlogtac ist pats fwd hint true `NoGen } END TACTIC EXTEND ssrwithoutloss | [ "without" "loss" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - { V82.tactic (wlogtac ist pats fwd hint false `NoGen) } + { wlogtac ist pats fwd hint false `NoGen } END TACTIC EXTEND ssrwithoutlosss | [ "without" "loss" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } + { wlogtac ist pats fwd hint true `NoGen } END TACTIC EXTEND ssrwithoutlossss | [ "without" "loss" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> - { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } + { wlogtac ist pats fwd hint true `NoGen } END { @@ -2617,14 +2608,14 @@ TACTIC EXTEND ssrgenhave | [ "gen" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> { let pats = augment_preclr clr pats in - V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } + wlogtac ist pats fwd hint false (`Gen id) } END TACTIC EXTEND ssrgenhave2 | [ "generally" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> { let pats = augment_preclr clr pats in - V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } + wlogtac ist pats fwd hint false (`Gen id) } END { diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 00d1296291..cbc352126e 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -30,10 +30,12 @@ let get_index = function Locus.ArgArg i -> i | _ -> (** The "first" and "last" tacticals. *) -let tclPERM perm tac gls = - let subgls = tac gls in +let tclPERM perm tac = + Proofview.V82.tactic begin fun gls -> + let subgls = Proofview.V82.of_tactic tac gls in let subgll' = perm subgls.Evd.it in re_sig subgll' subgls.Evd.sigma + end let rot_hyps dir i hyps = let n = List.length hyps in @@ -46,17 +48,17 @@ let rot_hyps dir i hyps = let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = let i = get_index ivar in - let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in + let evtac t = ssrevaltac ist t in let tac1 = evtac atac1 in if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1 else - let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in + let evotac = function Some atac -> evtac atac | _ -> Tacticals.New.tclIDTAC in let tac3 = evotac atac3 in let rec mk_pad n = if n > 0 then tac3 :: mk_pad (n - 1) else [] in match dir, mk_pad (i - 1), List.map evotac atacs2 with - | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENFIRST tac1 tac2 - | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENLAST tac1 tac2 - | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 - | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) + | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENFIRST tac1 tac2 + | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENLAST tac1 tac2 + | L2R, pad, tacs2 -> Tacticals.New.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 + | R2L, pad, tacs2 -> Tacticals.New.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) (** The "in" pseudo-tactical *)(* {{{ **********************************************) @@ -74,7 +76,7 @@ let check_wgen_uniq gens = | [] -> () in check [] ids -let pf_clauseids gl gens clseq = +let pf_clauseids gens clseq = let keep_clears = List.map (fun (x, _) -> x, None) in if gens <> [] then (check_wgen_uniq gens; gens) else if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else @@ -82,14 +84,15 @@ let pf_clauseids gl gens clseq = let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false -let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) +let posetac id cl = Tactics.pose_tac (Name id) cl let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else [posetac idhide cl0; - Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkVar idhide))] + convert_concl_no_check (EConstr.mkVar idhide)] -let endclausestac id_map clseq gl_id cl0 gl = +let endclausestac id_map clseq gl_id cl0 = + Proofview.V82.tactic begin fun gl -> let not_hyp' id = not (List.mem_assoc id id_map) in let orig_id id = try List.assoc id id_map with Not_found -> id in let dc, c = EConstr.decompose_prod_assum (project gl) (pf_concl gl) in @@ -124,40 +127,45 @@ let endclausestac id_map clseq gl_id cl0 gl = let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical") - -let tclCLAUSES tac (gens, clseq) gl = - if clseq = InGoal || clseq = InSeqGoal then tac gl else - let clr_gens = pf_clauseids gl gens clseq in - let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in - let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in - let cl0 = pf_concl gl in - let dtac gl = + end + +let tclCLAUSES tac (gens, clseq) = + Proofview.Goal.enter begin fun gl -> + if clseq = InGoal || clseq = InSeqGoal then tac else + let clr_gens = pf_clauseids gens clseq in + let clear = Tacticals.New.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in + let gl_id = mk_anon_id hidden_goal_tag (Tacmach.New.pf_ids_of_hyps gl) in + let cl0 = Proofview.Goal.concl gl in + let dtac = + Proofview.V82.tactic begin fun gl -> let c = pf_concl gl in let gl, args, c = List.fold_right (abs_wgen true mk_discharged_id) gens (gl,[], c) in - apply_type c args gl in + apply_type c args gl + end + in let endtac = let id_map = CList.map_filter (function | _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id) | _, None -> None) gens in endclausestac id_map clseq gl_id cl0 in - Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl + Tacticals.New.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) + end (** The "do" tactical. ********************************************************) let hinttac ist is_by (is_or, atacs) = - let dtac = if is_by then donetac ~-1 else Tacticals.tclIDTAC in + Proofview.Goal.enter begin fun _ -> + let dtac = if is_by then donetac ~-1 else Tacticals.New.tclIDTAC in let mktac = function - | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac + | Some atac -> Tacticals.New.tclTHEN (ssrevaltac ist atac) dtac | _ -> dtac in match List.map mktac atacs with - | [] -> if is_or then dtac else Tacticals.tclIDTAC + | [] -> if is_or then dtac else Tacticals.New.tclIDTAC | [tac] -> tac - | tacs -> Tacticals.tclFIRST tacs + | tacs -> Tacticals.New.tclFIRST tacs + end let ssrdotac ist (((n, m), tac), clauses) = let mul = get_index n, m in tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses - -let tclCLAUSES tac g_c = - Proofview.V82.(tactic (tclCLAUSES (of_tactic tac) g_c)) diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index c5b0deb752..f907ac3801 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -20,7 +20,7 @@ val tclSEQAT : int Locus.or_var * (('a * Tacinterp.Value.t option list) * Tacinterp.Value.t option) -> - Tacmach.tactic + unit Proofview.tactic val tclCLAUSES : unit Proofview.tactic -> @@ -33,7 +33,7 @@ val tclCLAUSES : val hinttac : Tacinterp.interp_sign -> - bool -> bool * Tacinterp.Value.t option list -> Ssrast.v82tac + bool -> bool * Tacinterp.Value.t option list -> unit Proofview.tactic val ssrdotac : Tacinterp.interp_sign -> @@ -44,5 +44,5 @@ val ssrdotac : Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq) -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 33e523a4a4..2252435658 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -107,7 +107,7 @@ ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern } END TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> { Proofview.V82.tactic (ssrinstancesof arg) } +| [ "ssrinstancesoftpat" cpattern(arg) ] -> { ssrinstancesof arg } END { diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index d5a781e472..e004613ef3 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -14,7 +14,6 @@ open Ltac_plugin open Names open Pp open Genarg -open Stdarg open Term open Context module CoqConstr = Constr @@ -22,7 +21,6 @@ open CoqConstr open Vars open Libnames open Tactics -open Tacticals open Termops open Recordops open Tacmach @@ -173,8 +171,6 @@ let loc_ofCG = function let mk_term k c ist = k, (mkRHole, Some c), ist let mk_lterm = mk_term ' ' -let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty - let nf_evar sigma c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) @@ -409,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 @@ -932,31 +928,15 @@ let id_of_Cterm t = match id_of_cpattern t with | Some x -> x | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here" -let of_ftactic ftac gl = - let r = ref None in - let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in - let tac = Proofview.V82.of_tactic tac in - let { sigma = sigma } = tac gl in - let ans = match !r with - | None -> assert false (* If the tactic failed we should not reach this point *) - | Some ans -> ans - in - (sigma, ans) - -let interp_wit wit ist gl x = - let globarg = in_gen (glbwit wit) x in - let arg = interp_genarg ist globarg in - let (sigma, arg) = of_ftactic arg gl in - sigma, Value.cast (topwit wit) arg -let interp_open_constr ist gl gc = - interp_wit wit_open_constr ist gl gc -let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c +let interp_open_constr ist env sigma gc = + Tacinterp.interp_open_constr ist env sigma gc +let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t -let interp_term gl = function +let interp_term env sigma = function | (_, c, Some ist) -> - on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) + on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c) | _ -> errorstrm (str"interpreting a term with no ist") let thin id sigma goal = @@ -982,7 +962,7 @@ let pr_ist { lfun= lfun } = pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun) *) -let interp_pattern ?wit_ssrpatternarg gl red redty = +let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = pp(lazy(str"interpreting: " ++ pr_pattern red)); let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in @@ -990,7 +970,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let mkG ?(k=' ') x ist = k,(x,None), ist in let ist_of (_,_,ist) = ist in let decode (_,_,ist as t) ?reccall f g = - try match DAst.get (pf_intern_term gl t) with + try match DAst.get (pf_intern_term env sigma0 t) with | GCast(t,CastConv c) when isGHole t && isGLambda c-> let (x, c) = destGLambda c in f x (' ',(c,None),ist) @@ -1008,7 +988,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let cleanup_XinE h x rp sigma = let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) - let ctx = pf_hyps gl in + let ctx = Environ.named_context env in let len = Context.Named.length ctx in let name = ref None in try ignore(Context.Named.lookup x ctx); (name, fun k -> @@ -1019,7 +999,6 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1))) end) with Not_found -> ref (Some x), fun _ -> () in - let sigma0 = project gl in let new_evars = let rec aux acc t = match kind t with | Evar (k,_) -> @@ -1072,13 +1051,13 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = match red with | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast) | X_In_T (x,t) -> - let gty = pf_intern_term gl ty in + let gty = pf_intern_term env sigma0 ty in E_As_X_In_T (mkG (mkRCast mkRHole gty) (ist_of ty), x, t) | E_In_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | E_As_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); @@ -1086,12 +1065,12 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in match red with - | T t -> let sigma, t = interp_term gl t in sigma, T t - | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t + | T t -> let sigma, t = interp_term env sigma0 t in sigma, T t + | In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t | X_In_T (x, rp) | In_X_In_T (x, rp) -> let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in let rp = mkXLetIn (Name x) rp in - let sigma, rp = interp_term gl rp in + let sigma, rp = interp_term env sigma0 rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in let rp = subst1 h (nf_evar sigma rp) in @@ -1100,15 +1079,15 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let mk e x p = match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in let rp = mkXLetIn (Name x) rp in - let sigma, rp = interp_term gl rp in + let sigma, rp = interp_term env sigma0 rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in let rp = subst1 h (nf_evar sigma rp) in - let sigma, e = interp_term (re_sig (sig_it gl) sigma) e in + let sigma, e = interp_term env sigma e in sigma, mk e h rp ;; -let interp_cpattern gl red redty = interp_pattern gl (T red) redty;; -let interp_rpattern ~wit_ssrpatternarg gl red = interp_pattern ~wit_ssrpatternarg gl red None;; +let interp_cpattern env sigma red redty = interp_pattern env sigma (T red) redty;; +let interp_rpattern ~wit_ssrpatternarg env sigma red = interp_pattern ~wit_ssrpatternarg env sigma red None;; let id_of_pattern = function | _, T t -> (match kind t with Var id -> Some id | _ -> None) @@ -1245,23 +1224,23 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx -let fill_occ_term env cl occ sigma0 (sigma, t) = +let fill_occ_term env sigma0 cl occ (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with NoMatch -> try let sigma', uc, t' = unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in if sigma' != sigma0 then raise NoMatch - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with _ -> errorstrm (str "partial term " ++ pr_econstr_pat env sigma t ++ str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in - let cl,(_,t) = fill_occ_term env concl occ sigma0 t in + let cl, t = fill_occ_term env sigma0 concl occ t in cl, t let cpattern_of_id id = @@ -1286,18 +1265,23 @@ let wit_ssrpatternarg = wit_rpatternty let interp_rpattern = interp_rpattern ~wit_ssrpatternarg -let ssrpatterntac _ist arg gl = - let pat = interp_rpattern gl arg in - let sigma0 = project gl in - let concl0 = pf_concl gl in +let ssrpatterntac _ist arg = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let sigma0 = Proofview.Goal.sigma gl in + let concl0 = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let pat = interp_rpattern env sigma0 arg in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in + fill_occ_pattern env sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in - let gl, tty = pf_type_of gl t in + let sigma, tty = Typing.type_of env sigma0 t in let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in - Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl + Proofview.Unsafe.tclEVARS sigma <*> + convert_concl ~check:true concl DEFAULTcast + end (* Register "ssrpattern" tactic *) let () = @@ -1305,7 +1289,7 @@ let () = let arg = let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in Value.cast (topwit wit_ssrpatternarg) v in - Proofview.V82.tactic (ssrpatterntac ist arg) in + ssrpatterntac ist arg in let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = @@ -1315,25 +1299,29 @@ let () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in Mltop.declare_cache_obj obj "ssrmatching_plugin" -let ssrinstancesof arg gl = +let ssrinstancesof arg = + Proofview.Goal.enter begin fun gl -> let ok rhs lhs ise = true in (* not (equal lhs (Evarutil.nf_evar ise rhs)) in *) - let env, sigma, concl = pf_env gl, project gl, pf_concl gl in - let concl = EConstr.Unsafe.to_constr concl in - let sigma0, cpat = interp_cpattern gl arg None in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma concl in + let sigma0, cpat = interp_cpattern env sigma arg None in let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() - ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do ignore(find env concl 1 ~k:print) done; raise NoMatch - with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + with NoMatch -> ppnl (str"END INSTANCES"); Tacticals.New.tclIDTAC + end module Internal = struct diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 31b414cc42..17b47227cb 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -57,7 +57,7 @@ val redex_of_pattern : (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) val interp_rpattern : - goal sigma -> + Environ.env -> Evd.evar_map -> rpattern -> pattern @@ -65,7 +65,7 @@ val interp_rpattern : in the current [Ltac] interpretation signature [ise] and tactic input [gl]. [ty] is an optional type for the redex of [cpat] *) val interp_cpattern : - goal sigma -> + Environ.env -> Evd.evar_map -> cpattern -> (glob_constr_and_expr * Geninterp.interp_sign) option -> pattern @@ -191,6 +191,8 @@ val mk_tpattern_matcher : * by [Rel 1] and the instance of [t] *) val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t +val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t + (* It may be handy to inject a simple term into the first form of cpattern *) val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern @@ -230,7 +232,7 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma (* One can also "Set SsrMatchingDebug" from a .v *) val debug : bool -> unit -val ssrinstancesof : cpattern -> Tacmach.tactic +val ssrinstancesof : cpattern -> unit Proofview.tactic (** Functions used for grammar extensions. Do not use. *) |