From a9541e2ee557c04c4bc3476a36a87bc7fcdb06bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Jun 2020 12:49:46 +0200 Subject: Ensure statically that Hint Extern comes with a pattern. --- tactics/auto.ml | 3 +-- tactics/class_tactics.ml | 2 +- tactics/eauto.ml | 2 +- tactics/hints.ml | 14 +++++++------- tactics/hints.mli | 2 +- 5 files changed, 11 insertions(+), 12 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 0ab1adda4b..0b11c1e79f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -105,7 +105,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 = @@ -349,8 +349,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 } } @@ -969,7 +968,7 @@ let make_extern pri pat tacast = 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 @@ -1133,9 +1132,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 @@ -1415,7 +1415,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; -- cgit v1.2.3 From c5e68b50c6b4d7301acb437d0a439136f025868f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Jun 2020 15:50:16 +0200 Subject: Simplify the computation of the head global for hint patterns. Instead of having to go through the pattern translation, we compute the pattern directly from the term. --- tactics/hints.ml | 49 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 34 insertions(+), 15 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 0b11c1e79f..9a7141ddb8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -55,6 +55,23 @@ let head_constr_bound sigma t = | Proj (p, _) -> ConstRef (Projection.constant p) | _ -> raise Bound +(* Slightly different from above, can they be merged? *) +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 _ -> + raise Bound +| CoFix _ | Int _ | Float _ | Array _ -> + anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") + let head_constr sigma c = try head_constr_bound sigma c with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \ @@ -801,12 +818,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 = @@ -827,15 +838,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; @@ -849,16 +860,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, @@ -961,7 +973,14 @@ 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; -- cgit v1.2.3 From dc8b5beeb1d12d5c0e30143db468599ce0f1c1cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Jun 2020 16:15:46 +0200 Subject: Replace Hints.head_constr_bound with Hints.head_bound. The two implementations are essentially the same except for potential interleaving of let-bindings and pattern-matchings. The only place the removed function was called probably does not rely on this difference of behaviour. --- tactics/hints.ml | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 9a7141ddb8..4532f97a27 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -42,20 +42,6 @@ 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 - -(* Slightly different from above, can they be merged? *) let rec head_bound sigma t = match EConstr.kind sigma t with | Prod (_, _, b) -> head_bound sigma b | LetIn (_, _, _, b) -> head_bound sigma b @@ -67,13 +53,11 @@ let rec head_bound sigma t = match EConstr.kind sigma t with | Var id -> GlobRef.VarRef id | Proj (p, _) -> GlobRef.ConstRef (Projection.constant p) | Cast (c, _, _) -> head_bound sigma c -| Evar _ | Rel _ | Meta _ | Sort _ | Fix _ | Lambda _ -> - raise Bound -| CoFix _ | Int _ | Float _ | Array _ -> - anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") +| 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.") @@ -1121,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 -- cgit v1.2.3 From 46cdf9a67deb9f6e29e937f146598ba020188b74 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 18 Jul 2020 12:36:50 +0200 Subject: Add overlay. --- dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh new file mode 100644 index 0000000000..56a69abbf7 --- /dev/null +++ b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then + + coqhammer_CI_REF=hint-pattern-out + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi -- cgit v1.2.3