diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 120 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 21 |
6 files changed, 87 insertions, 63 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 0931c3e61e..488bcb5208 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -369,8 +369,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) = let info = Exninfo.reify () in Tacticals.New.tclFAIL ~info 0 (str"Unbound reference") end - | Extern tacast -> - let p = FullHint.pattern h in + | Extern (p, tacast) -> conclPattern concl p tacast in let pr_hint env sigma = diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 36544883aa..378a3e718b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -359,7 +359,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm Tacticals.New.tclTHEN fst snd | Unfold_nth c -> Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c]) - | Extern tacast -> conclPattern concl p tacast + | Extern (p, tacast) -> conclPattern concl p tacast in let tac = FullHint.run h tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a554b117e..17e6a6edb4 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -126,7 +126,7 @@ and e_my_find_search env sigma db_list local_db secvars concl = Tacticals.New.tclTHEN (unify_e_resolve st h) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast + | Extern (pat, tacast) -> conclPattern concl pat tacast in let tac = FullHint.run h tac in (tac, b, lazy (FullHint.print env sigma h)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 41b200bb83..4532f97a27 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -42,21 +42,22 @@ type debug = Debug | Info | Off exception Bound -let head_constr_bound sigma t = - let t = strip_outer_cast sigma t in - let _,ccl = decompose_prod_assum sigma t in - let hd,args = decompose_app sigma ccl in - let open GlobRef in - match EConstr.kind sigma hd with - | Const (c, _) -> ConstRef c - | Ind (i, _) -> IndRef i - | Construct (c, _) -> ConstructRef c - | Var id -> VarRef id - | Proj (p, _) -> ConstRef (Projection.constant p) - | _ -> raise Bound +let rec head_bound sigma t = match EConstr.kind sigma t with +| Prod (_, _, b) -> head_bound sigma b +| LetIn (_, _, _, b) -> head_bound sigma b +| App (c, _) -> head_bound sigma c +| Case (_, _, _, c, _) -> head_bound sigma c +| Ind (ind, _) -> GlobRef.IndRef ind +| Const (c, _) -> GlobRef.ConstRef c +| Construct (c, _) -> GlobRef.ConstructRef c +| Var id -> GlobRef.VarRef id +| Proj (p, _) -> GlobRef.ConstRef (Projection.constant p) +| Cast (c, _, _) -> head_bound sigma c +| Evar _ | Rel _ | Meta _ | Sort _ | Fix _ | Lambda _ +| CoFix _ | Int _ | Float _ | Array _ -> raise Bound let head_constr sigma c = - try head_constr_bound sigma c + try head_bound sigma c with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \ (co)inductive type, (co)inductive type constructor, or projection.") @@ -105,7 +106,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Genarg.glob_generic_argument (* Hint Extern *) + | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *) type 'a hints_path_atom_gen = @@ -237,10 +238,38 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0 type stored_data = int * full_hint (* First component is the index of insertion in the table, to keep most recent first semantics. *) -module Bounded_net = Btermdn.Make(struct - type t = stored_data - let compare = pri_order_int - end) +module Bounded_net : +sig + type t + val empty : t + val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t + val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list +end = +struct + module Data = struct type t = stored_data let compare = pri_order_int end + module Bnet = Btermdn.Make(Data) + + type diff = TransparentState.t option * Pattern.constr_pattern * stored_data + type data = Bnet of Bnet.t | Diff of diff * data ref + type t = data ref + + let empty = ref (Bnet Bnet.empty) + + let add st net p v = ref (Diff ((st, p, v), net)) + + let rec force net = match !net with + | Bnet dn -> dn + | Diff ((st, p, v), rem) -> + let dn = force rem in + let p = Bnet.pattern st p in + let dn = Bnet.add dn p v in + let () = net := (Bnet dn) in + dn + + let lookup sigma st net p = + let dn = force net in + Bnet.lookup sigma st dn p +end type search_entry = { sentry_nopat : stored_data list; @@ -263,18 +292,17 @@ let add_tac pat t se = | None -> if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat } - | Some pat -> + | Some (st, pat) -> if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se else { se with sentry_pat = List.insert pri_order t se.sentry_pat; - sentry_bnet = Bounded_net.add se.sentry_bnet pat t; } + sentry_bnet = Bounded_net.add st se.sentry_bnet pat t; } let rebuild_dn st se = let dn' = List.fold_left (fun dn (id, t) -> - let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in - Bounded_net.add dn pat (id, t)) + Bounded_net.add (Some st) dn (Option.get t.pat) (id, t)) Bounded_net.empty se.sentry_pat in { se with sentry_bnet = dn' } @@ -322,8 +350,7 @@ let instantiate_hint env sigma p = | Res_pf_THEN_trivial_fail c -> Res_pf_THEN_trivial_fail (mk_clenv c) | Give_exact c -> Give_exact (mk_clenv c) - | Unfold_nth e -> Unfold_nth e - | Extern t -> Extern t + | (Unfold_nth _ | Extern _) as h -> h in { p with code = { p.code with obj = code } } @@ -650,7 +677,7 @@ struct if not db.use_dn && is_exact v.code.obj then None else let dnst = if db.use_dn then Some db.hintdb_state else None in - Option.map (fun p -> Bounded_net.pattern dnst p) v.pat + Option.map (fun p -> (dnst, p)) v.pat in let oval = find gr db in { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map } @@ -775,12 +802,6 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with (* adding and removing tactics in the search table *) -let try_head_pattern c = - try head_pattern_bound c - with BoundPattern -> - user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \ - an if, case, or let expression, an application, or a projection.") - let with_uid c = { obj = c; uid = fresh_key () } let secvars_of_idset s = @@ -801,15 +822,15 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_exact_entry" + try head_bound sigma cty + with Bound -> failwith "make_exact_entry" in let pri = match info.hint_priority with None -> 0 | Some p -> p in let pat = match info.hint_pattern with | Some pat -> snd pat - | None -> pat + | None -> + Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in (Some hd, { pri; pat = Some pat; name; @@ -823,16 +844,17 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry" in + try head_bound ce.evd c' + with Bound -> failwith "make_apply_entry" in let miss = clenv_missing ce in let nmiss = List.length miss in let secvars = secvars_of_constr env sigma c in let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in let pat = match info.hint_pattern with - | Some p -> snd p | None -> pat + | Some p -> snd p + | None -> + Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in if Int.equal nmiss 0 then (Some hd, @@ -935,14 +957,21 @@ let make_unfold eref = code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = - let hdconstr = Option.map try_head_pattern pat in + let hdconstr = match pat with + | None -> None + | Some c -> + try Some (head_pattern_bound c) + with BoundPattern -> + user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \ + an if, case, or let expression, an application, or a projection.") + in (hdconstr, { pri = pri; pat = pat; name = PathAny; db = None; secvars = Id.Pred.empty; (* Approximation *) - code = with_uid (Extern tacast) }) + code = with_uid (Extern (pat, tacast)) }) let make_mode ref m = let open Term in @@ -1076,7 +1105,7 @@ let subst_autohint (subst, obj) = match t with | None -> gr' | Some t -> - (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value) + (try head_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value) with Bound -> gr') in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in @@ -1106,9 +1135,10 @@ let subst_autohint (subst, obj) = | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' - | Extern tac -> + | Extern (pat, tac) -> + let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in let tac' = Genintern.generic_substitute subst tac in - if tac==tac' then data.code.obj else Extern tac' + if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac') in let name' = subst_path_atom subst data.name in let uid' = subst_kn subst data.code.uid in @@ -1388,7 +1418,7 @@ let pr_hint env sigma h = match h.obj with (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> str"unfold " ++ pr_evaluable_reference c - | Extern tac -> + | Extern (_, tac) -> str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac let pr_id_hint env sigma (id, v) = diff --git a/tactics/hints.mli b/tactics/hints.mli index f0fed75828..0b9da27ab3 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -37,7 +37,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Genarg.glob_generic_argument (* Hint Extern *) + | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *) type hint = private { hint_term : constr; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f553a290f9..cb2e607012 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -117,7 +117,7 @@ let unsafe_intro env decl b = Refine.refine ~typecheck:false begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in - let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in + let inst = identity_subst_val (named_context_val env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in @@ -338,7 +338,7 @@ let rename_hyp repl = let nhyps = List.map map hyps in let nconcl = subst concl in let nctx = val_of_named_context nhyps in - let instance = List.map (NamedDecl.get_id %> mkVar) hyps in + let instance = EConstr.identity_subst_val (Environ.named_context_val env) in Refine.refine ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in sigma, mkEvar (ev, instance) @@ -437,11 +437,6 @@ let clear_hyps2 env sigma ids sign t cl = with Evarutil.ClearDependencyError (id,err,inglobal) -> error_replacing_dependency env sigma id err inglobal -let new_evar_from_context ?principal sign evd typ = - let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in - let (evd, evk) = Evarutil.new_pure_evar sign evd typ in - (evd, mkEvar (evk, instance)) - let internal_cut ?(check=true) replace id t = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -449,22 +444,22 @@ let internal_cut ?(check=true) replace id t = let concl = Proofview.Goal.concl gl in let sign = named_context_val env in let r = Retyping.relevance_of_type env sigma t in - let sign',t,concl,sigma = + let env',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in - sign',t,concl,sigma + Environ.reset_with_named_context sign' env,t,concl,sigma else (if check && mem_named_context_val id sign then user_err (str "Variable " ++ Id.print id ++ str " is already declared."); - push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in + push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> - let (sigma, ev) = new_evar_from_context sign sigma nf_t in - let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in + let (sigma, ev) = Evarutil.new_evar env sigma nf_t in + let (sigma, ev') = Evarutil.new_evar ~principal:true env' sigma concl in let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in (sigma, term) end) @@ -2788,7 +2783,7 @@ let pose_tac na c = let id = make_annot id Sorts.Relevant in let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in - let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in + let inst = EConstr.identity_subst_val hyps in let body = mkEvar (ev, mkRel 1 :: inst) in (sigma, mkLetIn (map_annot Name.mk_name id, c, t, body)) end |