diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 6 | ||||
| -rw-r--r-- | tactics/btermdn.ml | 15 | ||||
| -rw-r--r-- | tactics/cbn.ml | 86 | ||||
| -rw-r--r-- | tactics/eauto.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 53 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 11 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 29 |
9 files changed, 98 insertions, 111 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 353e138599..0189e3ab04 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -500,12 +500,6 @@ let delta_auto debug mod_delta n lems dbnames = (search d n mod_delta db_list hints) end -let delta_auto = - if Flags.profile then - let key = CProfile.declare_profile "delta_auto" in - CProfile.profile5 key delta_auto - else delta_auto - let auto ?(debug=Off) n = delta_auto debug false n let new_auto ?(debug=Off) n = delta_auto debug true n diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index af0ca22868..794d2bb94f 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -32,18 +32,25 @@ let compare_term_label t1 t2 = match t1, t2 with type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything -let decomp_pat = +let decomp_pat p = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc) + | PProj (p, c) -> + let hole = PMeta None in + let params = List.make (Projection.npars p) hole in + (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc) | c -> (c,acc) in - decrec [] + decrec [] p let decomp sigma t = let rec decrec acc c = match EConstr.kind sigma c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc) + | Proj (p, c) -> + (* Hack: fake evar to generate [Everything] in the functions below *) + let hole = mkEvar (Evar.unsafe_of_int (-1), []) in + let params = List.make (Projection.npars p) hole in + (mkConst (Projection.constant p), params @ c :: acc) | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 167f7d4026..c3c61f6e51 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -402,11 +402,11 @@ let safe_meta_value sigma ev = (* Beta Reduction tools *) -let apply_subst recfun env sigma refold cst_l t stack = +let apply_subst recfun env sigma cst_l t stack = let rec aux env cst_l t stack = match (Stack.decomp stack, EConstr.kind sigma t) with | Some (h,stacktl), Lambda (_,_,c) -> - let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in + let cst_l' = Cst_stack.add_param h cst_l in aux (h::env) cst_l' c stacktl | _ -> recfun sigma cst_l (substl env t, stack) in aux env cst_l t stack @@ -453,50 +453,42 @@ let magically_constant_of_fixbody env sigma reference bd = function | None -> bd end -let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkCoFix (ind,typedbodies) else let bd = mkCoFix (ind,typedbodies) in - match env with + match reference with | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = +let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = let raw_answer = - let env = if refold then Some env else None in - contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + contract_cofix env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in apply_subst (fun sigma x (t,sk') -> - let t' = - if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in + let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in recfun x (t',sk')) - [] sigma refold Cst_stack.empty raw_answer sk + [] sigma Cst_stack.empty raw_answer sk (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) -let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) else let bd = mkFix ((recindices,ind),typedbodies) in - match env with + match reference with | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -504,18 +496,14 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) -let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = +let reduce_and_refold_fix recfun env sigma cst_l fix sk = let raw_answer = - let env = if refold then Some env else None in - contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + contract_fix env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> - let t' = - if refold then - Cst_stack.best_replace sigma (mkFix fix) cst_l t - else t - in recfun x (t',sk')) - [] sigma refold Cst_stack.empty raw_answer sk + let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in + recfun x (t',sk')) + [] sigma Cst_stack.empty raw_answer sk module CredNative = Reductionops.CredNative @@ -524,7 +512,7 @@ module CredNative = Reductionops.CredNative Here is where unfolded constant are stored in order to be eventually refolded. - If tactic_mode is true, it uses ReductionBehaviour, prefers + It uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants fix and cofix came from. @@ -558,7 +546,7 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = in Vars.substl subst (snd br) -let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = +let rec whd_state_gen ?csts flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = @@ -584,7 +572,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with | LocalDef (_,body,_) -> - whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) + whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) | _ -> fold ()) | Evar ev -> fold () | Meta ev -> @@ -600,10 +588,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | body -> begin let body = EConstr.of_constr body in - if not tactic_mode - then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) - (body, stack) - else (* Looks for ReductionBehaviour *) + (* Looks for ReductionBehaviour *) match ReductionBehaviour.get (GlobRef.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) | Some behavior -> @@ -652,10 +637,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let npars = Projection.npars p in - if not tactic_mode then - let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in - whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with + match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with | None -> let stack' = (c, Stack.Proj (p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in @@ -693,24 +675,24 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = end) | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> - apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack + apply_subst (fun _ -> whrec) [b] sigma cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> whrec - (if refold then Cst_stack.add_args cl cst_l else cst_l) + (Cst_stack.add_args cl cst_l) (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> - apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack + apply_subst (fun _ -> whrec) [] sigma cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na, t)) env in - let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in - (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with + let whrec' = whd_state_gen flags env' sigma in + (match EConstr.kind sigma (Stack.zip ~refold:true sigma (whrec' (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then - let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in + let (x', l') = whrec' (Array.last cl, Stack.empty) in match EConstr.kind sigma x', l' with | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in @@ -743,7 +725,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip sigma (x, args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in - reduce_and_refold_fix whrec env sigma refold cst_l f out_sk + reduce_and_refold_fix whrec env sigma cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> let x' = Stack.zip sigma (x, args) in begin match remains with @@ -755,7 +737,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some body -> let const = (fst const, EInstance.make (snd const)) in let body = EConstr.of_constr body in - whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) + whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> let stack = s' @ (Stack.append_app [|x'|] s'') in @@ -778,7 +760,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> - reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack + reduce_and_refold_cofix whrec env sigma cst_l cofix stack |_ -> fold () else fold () @@ -812,12 +794,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in fun xs -> let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in - if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res + (Stack.best_state sigma s cst_l) let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty)) - in + let state = whd_state_gen flags env sigma (t, Stack.empty) in Stack.zip ~refold:true sigma state let norm_cbn flags env sigma t = diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 20c557b282..5df9fab236 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -359,9 +359,6 @@ let e_search_auto debug (in_depth,p) lems db_list = tclIDTAC gl end -(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) -(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) - let eauto_with_bases ?(debug=Off) np lems db_list = Hints.wrap_hint_warning (e_search_auto debug np lems db_list) diff --git a/tactics/hints.ml b/tactics/hints.ml index 5e9c3baeb1..31b276bb3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -320,7 +320,7 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> - (match Recordops.find_primitive_projection cst with + (match Structures.PrimitiveProjections.find_opt cst with | Some p -> let p = Projection.make p false in let npars = Projection.npars p in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5338e0eef5..783a317b3a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -293,31 +293,34 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if Coqlib.check_ind_ref "core.eq.type" ind then - Some (build_coq_eq_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.identity.type" ind then - Some (build_coq_identity_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if Coqlib.check_ind_ref "core.JMeq.type" ind then - Some (build_coq_jmeq_data()),hdapp, - HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nconstr = Array.length mip.mind_consnames in - if Int.equal nconstr 1 then - let (ctx, cty) = constr_types.(0) in - let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - if is_matching env sigma coq_refl_leibniz1_pattern cty then - None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern cty then - None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern cty then - None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else raise NoEquationFound - else raise NoEquationFound - | _ -> raise NoEquationFound + (try + if Coqlib.check_ind_ref "core.eq.type" ind then + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.identity.type" ind then + Some (build_coq_identity_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.JMeq.type" ind then + Some (build_coq_jmeq_data()),hdapp, + HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else + let (mib,mip) = Global.lookup_inductive ind in + let constr_types = mip.mind_nf_lc in + let nconstr = Array.length mip.mind_consnames in + if Int.equal nconstr 1 then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then + None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) + else if is_matching env sigma coq_refl_leibniz2_pattern cty then + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if is_matching env sigma coq_refl_jm_pattern cty then + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound + else raise NoEquationFound + with UserError _ -> + raise NoEquationFound) + | _ -> raise NoEquationFound (* Note: An "equality type" is any type with a single argument-free constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 68afd9a128..2d69047d1e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -683,15 +683,6 @@ module New = struct let tclPROGRESS t = Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) - (* Select a subset of the goals *) - let tclSELECT = let open Goal_select in function - | SelectNth i -> Proofview.tclFOCUS i i - | SelectList l -> Proofview.tclFOCUSLIST l - | SelectId id -> Proofview.tclFOCUSID id - | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") - | SelectAlreadyFocused -> - anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") - (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = @@ -905,4 +896,6 @@ module New = struct let (sigma, t) = Typing.type_of ?refresh env sigma c in Proofview.Unsafe.tclEVARS sigma <*> tac sigma t) + let tclSELECT = Goal_select.tclSELECT + end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 19d08dcc36..c09d268c40 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -206,7 +206,6 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic @@ -250,4 +249,7 @@ module New : sig val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic val tclTYPEOFTHEN : ?refresh:bool -> constr -> (evar_map -> types -> unit Proofview.tactic) -> unit Proofview.tactic + + val tclSELECT : ?nosuchgoal:'a tactic -> Goal_select.t -> 'a tactic -> 'a tactic + [@@ocaml.deprecated "Use [Goal_select.tclSELECT]"] end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cbf12ac22f..c24520b371 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1555,7 +1555,7 @@ let make_projection env sigma params cstr sign elim i n c u = | Some proj -> let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = - match Recordops.find_primitive_projection proj with + match Structures.PrimitiveProjections.find_opt proj with | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) | None -> @@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let params = List.map EConstr.of_constr params in let cstr = (get_constructors env indf).(0) in let elim = - try DefinedRecord (Recordops.lookup_projections ind) + try DefinedRecord (Structures.Structure.find_projections ind) with Not_found -> let u = EInstance.kind sigma u in let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in @@ -1886,12 +1886,6 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) -(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) - -(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) -(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) - let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) @@ -2796,7 +2790,24 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in let decls,cl = decompose_prod_n_assum sigma i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in + let newdecls,_ = + let c = Termops.collapse_appl sigma c in + let arity = Array.length (snd (Termops.decompose_app_vect sigma c)) in + let cache = ref Int.Map.empty in + let eq sigma k t = + let c = + try Int.Map.find k !cache + with Not_found -> + let c = EConstr.Vars.lift k c in + let () = cache := Int.Map.add k c !cache in + c + in + (* We use a nounivs equality because generalize morally takes a pattern as + argument, so we have to ignore freshly generated sorts. *) + EConstr.eq_constr_nounivs sigma c t + in + decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) dummy_prod) + in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name env sigma c t ids cl' na in let r = Retyping.relevance_of_type env sigma t in |