From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- tactics/auto.ml | 2 +- tactics/eqschemes.ml | 71 ++++++++++++++++++++++----------------------- tactics/equality.ml | 4 +-- tactics/extratactics.ml4 | 2 +- tactics/hints.mli | 3 +- tactics/inv.ml | 3 +- tactics/leminv.ml | 9 +++--- tactics/rewrite.mli | 2 +- tactics/tactic_matching.mli | 2 +- tactics/tacticals.ml | 5 ++-- tactics/tacticals.mli | 35 +++++++++++----------- tactics/tactics.ml | 57 ++++++++++++++++++------------------ tactics/tactics.mli | 37 ++++++++++++----------- 13 files changed, 112 insertions(+), 120 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 4fb4b3263..a170c27fb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -327,7 +327,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in - let hyp = Context.map_named_declaration nf decl in + let hyp = Context.Named.Declaration.map nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 64a68ba6b..2c713a021 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -49,7 +49,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Environ open Inductive @@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, - extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt - @ extended_rel_list 0 realargs) + Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt + @ Context.Rel.to_extended_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s @@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) = error "Inductive equalities with local definitions in arity not supported."; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) let params,constrargs = List.chop mib.mind_nparams constrargs in if mip.mind_nrealargs > mib.mind_nparams then @@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) = error "Inductive equalities with local definitions in arity not supported"; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let _,constrargs = List.chop mib.mind_nparams constrargs in let constrargs = List.map (Vars.subst_instance_constr u) constrargs in @@ -170,7 +169,7 @@ let build_sym_scheme env ind = let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let realsign_ind = @@ -183,7 +182,7 @@ let build_sym_scheme env ind = my_it_mkLambda_or_LetIn_name (lift_rel_context (nrealargs+1) realsign_ind) (mkApp (mkIndU indu,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), @@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in - let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in + let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let applied_ind_C = mkApp (mkIndU indu, Array.append - (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt) + (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt) (rel_vect (nrealargs+1) nrealargs)) in let realsign_ind = name_context env ((Name varH,None,applied_ind)::realsign) in @@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind = (mkApp (eq,[| mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs]); mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]])|]]); @@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind = let eq,eqrefl,ctx = get_coq_eq ctx in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1; rel_vect 0 nrealargs; rel_vect nrealargs nrealargs]) in let applied_ind_G = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+3) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1; rel_vect (nrealargs+3) nrealargs; rel_vect 0 nrealargs]) in let realsign_P = lift_rel_context nrealargs realsign in @@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind = lift_rel_context (nrealargs+3) realsign) in let applied_sym_C n = mkApp(sym, - Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in + Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in let applied_sym_G = mkApp(sym, - Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1; + Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in @@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind = let ci = make_case_info (Global.env()) ind RegularStyle in let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in let applied_PC = - mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign) + mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign) (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in let applied_PG = mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs) @@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind = (if dep then [|mkRel 2|] else [||])) in let applied_sym_sym = mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect 4 nrealargs; rel_vect (nrealargs+4) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 4 nrealargs; [|mkRel 2|]])|]]) in @@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind = mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), applied_PR)), mkApp (sym_involutive, - Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), + Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), [|main_body|]) else main_body)))))) @@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = get_sym_eq_data env indu in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (4*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1; rel_vect 0 nrealargs; rel_vect (nrealargs+1) nrealargs]) in let applied_ind_P' = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+1) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1; rel_vect 0 nrealargs; rel_vect (2*nrealargs+1) nrealargs]) in let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in @@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let constrargs_cstr = constrargs@[cstr 0] in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind = applist (mkVar varP,if dep then constrargs_cstr else constrargs) in let applied_PG = mkApp (mkVar varP, - if dep then extended_rel_vect 0 realsign_ind - else extended_rel_vect 1 realsign) in + if dep then Context.Rel.to_extended_vect 0 realsign_ind + else Context.Rel.to_extended_vect 1 realsign) in let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind @@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') = | hp :: p :: ind :: indargs -> let c' = my_it_mkLambda_or_LetIn indargs - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p) - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp) - (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp) + (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind) (Reductionops.whd_beta Evd.empty (applist (c, - extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) + Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) in c', ctx' | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") @@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind = let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then + if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind = (mkNamedLambda varH (applist (mkIndU indu, - extended_rel_list (mip.mind_nrealargs+2) paramsctxt @ - extended_rel_list 0 realsign)) + Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @ + Context.Rel.to_extended_list 0 realsign)) (mkCase (ci, my_it_mkLambda_or_LetIn_name (lift_rel_context (mip.mind_nrealargs+3) realsign) @@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind = (Anonymous, applist (mkIndU indu, - extended_rel_list (2*mip.mind_nrealdecls+3) + Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3) paramsctxt - @ extended_rel_list 0 realsign), + @ Context.Rel.to_extended_list 0 realsign), mkApp (eq, [|mkVar varB; mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); diff --git a/tactics/equality.ml b/tactics/equality.ml index 92ebcb272..7d15e9ee6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1574,7 +1574,7 @@ let unfold_body x = Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let (_, xval, _) = Context.lookup_named x hyps in + let (_, xval, _) = Context.Named.lookup x hyps in let xval = match xval with | None -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") @@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x = (** [is_eq_x] ensures nf_evar on its side *) let hyps = Proofview.Goal.hyps gl in let test hyp _ = is_eq_x gl varx hyp in - Context.fold_named_context test ~init:() hyps; + Context.Named.fold_outside test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 92682fc7a..f311e47f6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -315,7 +315,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in + let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in let id = diff --git a/tactics/hints.mli b/tactics/hints.mli index 3a0521f66..b48fb776e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -10,7 +10,6 @@ open Pp open Util open Names open Term -open Context open Environ open Globnames open Decl_kinds @@ -192,7 +191,7 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> named_declaration -> hint_entry list + env -> evar_map -> Context.Named.Declaration.t -> hint_entry list (** [make_extern pri pattern tactic_expr] *) diff --git a/tactics/inv.ml b/tactics/inv.ml index ed1a62795..3574990f6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Namegen open Environ @@ -97,7 +96,7 @@ let make_inv_predicate env evd indf realargs id status concl = (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) in - let nhyps = rel_context_length hyps in + let nhyps = Context.Rel.length hyps in let env' = push_rel_context hyps env in (* Now the arity is pushed, and we need to construct the pairs * ai,mkRel(n-i+1) *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 75e69bc09..9154c50c8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -14,7 +14,6 @@ open Term open Vars open Termops open Namegen -open Context open Evd open Printer open Reductionops @@ -157,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> if Id.List.mem id ivars then - ((mkVar id)::revargs,add_named_decl d hyps) + ((mkVar id)::revargs, Context.Named.add d hyps) else (revargs,hyps)) env ~init:([],[]) @@ -206,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = fold_named_context (fun env (id,_,_ as d) sign -> if mem_named_context id global_named_context then sign - else add_named_decl d sign) - invEnv ~init:empty_named_context + else Context.Named.add d sign) + invEnv ~init:Context.Named.empty end in let avoid = ref [] in let { sigma=sigma } = Proof.V82.subgoals pf in @@ -218,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in avoid := h::!avoid; - ownSign := add_named_decl (h,None,ty) !ownSign; + ownSign := Context.Named.add (h,None,ty) !ownSign; applist (mkVar h, inst) | _ -> map_constr fill_holes c in diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 40a18ac45..1de47b2be 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -71,7 +71,7 @@ val cl_rewrite_clause : bool -> Locus.occurrences -> Id.t option -> tactic val is_applied_rewrite_relation : - env -> evar_map -> Context.rel_context -> constr -> types option + env -> evar_map -> Context.Rel.t -> constr -> types option val declare_relation : ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli index d8e6dd0ae..090207bcc 100644 --- a/tactics/tactic_matching.mli +++ b/tactics/tactic_matching.mli @@ -43,7 +43,7 @@ val match_term : val match_goal: Environ.env -> Evd.evar_map -> - Context.named_context -> + Context.Named.t -> Term.constr -> (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e181c8e14..aaef0f072 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Termops -open Context open Declarations open Tacmach open Clenv @@ -154,8 +153,8 @@ type branch_args = { branchnames : Tacexpr.intro_patterns} type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) + ba : branch_args; (* the branch args *) + assums : Context.Named.t} (* the list of assumptions introduced *) let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 80e01a8d0..d8aa3161e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,7 +9,6 @@ open Pp open Names open Term -open Context open Tacmach open Proof_type open Tacexpr @@ -60,29 +59,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val onNthHypId : int -> (Id.t -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic -val onNthDecl : int -> (named_declaration -> tactic) -> tactic +val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic val onLastHyp : (constr -> tactic) -> tactic -val onLastDecl : (named_declaration -> tactic) -> tactic +val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic -val onNLastDecls : int -> (named_context -> tactic) -> tactic +val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic val lastHypId : goal sigma -> Id.t val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> named_declaration +val lastDecl : goal sigma -> Context.Named.Declaration.t val nLastHypsId : int -> goal sigma -> Id.t list val nLastHyps : int -> goal sigma -> constr list -val nLastDecls : int -> goal sigma -> named_context +val nLastDecls : int -> goal sigma -> Context.Named.t -val afterHyp : Id.t -> goal sigma -> named_context +val afterHyp : Id.t -> goal sigma -> Context.Named.t val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic -val onHyps : (goal sigma -> named_context) -> - (named_context -> tactic) -> tactic +val onHyps : (goal sigma -> Context.Named.t) -> + (Context.Named.t -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -99,18 +98,18 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) type branch_args = { - ity : pinductive; (** the type we were eliminating on *) + ity : pinductive; (** the type we were eliminating on *) largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) pred : constr; (** the predicate we used *) nassums : int; (** the number of assumptions to be introduced *) branchsign : bool list; (** the signature of the branch. - true=recursive argument, false=constant *) + true=recursive argument, false=constant *) branchnames : intro_patterns} type branch_assumptions = { - ba : branch_args; (** the branch args *) - assums : named_context} (** the list of assumptions introduced *) + ba : branch_args; (** the branch args *) + assums : Context.Named.t} (** the list of assumptions introduced *) (** [check_disjunctive_pattern_size loc pats n] returns an appropriate error message if |pats| <> n *) @@ -223,7 +222,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context + val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -232,11 +231,11 @@ module New : sig val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic - val onLastDecl : (named_declaration -> unit tactic) -> unit tactic + val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic - val onHyps : ([ `NF ], named_context) Proofview.Goal.enter -> - (named_context -> unit tactic) -> unit tactic - val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic + val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> + (Context.Named.t -> unit tactic) -> unit tactic + val afterHyp : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic val tryAllHyps : (identifier -> unit tactic) -> unit tactic val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2e7adc513..f2319804e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Find_subterm open Namegen @@ -1405,7 +1404,7 @@ let make_projection env sigma params cstr sign elim i n c u = then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in - let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in + let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) else None @@ -1413,7 +1412,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> - let args = extended_rel_vect 0 sign in + let args = Context.Rel.to_extended_vect 0 sign in let proj = if Environ.is_projection proj env then mkProj (Projection.make proj false, mkApp (c, args)) @@ -2528,7 +2527,7 @@ let bring_hyps hyps = let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in - let args = Array.of_list (instance_from_named_context hyps) in + let args = Array.of_list (Context.Named.to_instance hyps) in Proofview.Refine.refine { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -2589,7 +2588,7 @@ let generalize_dep ?(with_let=false) c gl = d::toquant else toquant in - let to_quantify = Context.fold_named_context seek sign ~init:[] in + let to_quantify = Context.Named.fold_outside seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in @@ -2609,7 +2608,7 @@ let generalize_dep ?(with_let=false) c gl = in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in - let args = instance_from_named_context to_quantify_rev in + let args = Context.Named.to_instance to_quantify_rev in tclTHENLIST [tclEVARS evd; apply_type cl'' (if Option.is_empty body then c::args else args); @@ -2687,7 +2686,7 @@ let quantify lconstr = let unfold_body x gl = let hyps = pf_hyps gl in let xval = - match Context.lookup_named x hyps with + match Context.Named.lookup x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") in @@ -3108,20 +3107,20 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (* number of parameters *) - predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (* Number of predicates *) - branches: rel_context; (* branchr,...,branch1 *) - nbranches: int; (* Number of branches *) - args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (* number of arguments *) - indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) - concl: types; (* Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) - indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) - farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) + params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (* number of parameters *) + predicates: Context.Rel.t; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (* Number of predicates *) + branches: Context.Rel.t; (* branchr,...,branch1 *) + nbranches: int; (* Number of branches *) + args: Context.Rel.t; (* (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (* number of arguments *) + indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) + farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) } let empty_scheme = @@ -3280,7 +3279,7 @@ let hyps_of_vars env sign nogen hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) @@ -3511,7 +3510,7 @@ let occur_rel n c = We also return the conclusion. *) let decompose_paramspred_branch_args elimt = - let rec cut_noccur elimt acc2 : rel_context * rel_context * types = + let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types = match kind_of_term elimt with | Prod(nme,tpe,elimt') -> let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in @@ -3520,7 +3519,7 @@ let decompose_paramspred_branch_args elimt = else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt | _ -> error_ind_scheme "" in - let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types = + let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types = match kind_of_term elimt with | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl @@ -3648,7 +3647,7 @@ let compute_scheme_signature scheme names_info ind_type_guess = let ind_is_ok = List.equal Term.eq_constr (List.lastn scheme.nargs indargs) - (extended_rel_list 0 scheme.args) in + (Context.Rel.to_extended_list 0 scheme.args) in if not (ccl_arg_ok && ind_is_ok) then error_ind_scheme "the conclusion of" in (cond, check_concl) @@ -4563,10 +4562,10 @@ let abstract_subproof id gk tac = List.fold_right (fun (id,_,_ as d) (s1,s2) -> if mem_named_context id current_sign && - interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d + interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d then (s1,push_named_context_val d s2) - else (add_named_decl d s1,s2)) - global_sign (empty_named_context,empty_named_context_val) in + else (Context.Named.add d s1,s2)) + global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in let concl = @@ -4594,7 +4593,7 @@ let abstract_subproof id gk tac = in let const, args = if !shrink_abstract then shrink_entry sign const - else (const, List.rev (instance_from_named_context sign)) + else (const, List.rev (Context.Named.to_instance sign)) in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f5695ff06..873a11bd2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -9,7 +9,6 @@ open Loc open Names open Term -open Context open Environ open Proof_type open Evd @@ -33,9 +32,9 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool val introduction : ?check:bool -> Id.t -> unit Proofview.tactic val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic +val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -val convert_hyp_no_check : named_declaration -> unit Proofview.tactic +val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic val thin : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic @@ -50,7 +49,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t -val find_intro_names : rel_context -> goal sigma -> Id.t list +val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic @@ -180,7 +179,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> tactic -val bring_hyps : named_context -> unit Proofview.tactic +val bring_hyps : Context.Named.t -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic @@ -239,20 +238,20 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (** number of parameters *) - predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (** Number of predicates *) - branches: rel_context; (** branchr,...,branch1 *) - nbranches: int; (** Number of branches *) - args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (** number of arguments *) - indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) - concl: types; (** Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) - indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) - farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) + params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (** number of parameters *) + predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (** Number of predicates *) + branches: Context.Rel.t; (** branchr,...,branch1 *) + nbranches: int; (** Number of branches *) + args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (** number of arguments *) + indarg: Context.Rel.Declaration.t option; (** Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (** Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) + farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme -- cgit v1.2.3