diff options
39 files changed, 457 insertions, 330 deletions
diff --git a/.gitignore b/.gitignore index 0c7a8f70f6..557655317c 100644 --- a/.gitignore +++ b/.gitignore @@ -92,6 +92,7 @@ test-suite/coqdoc/coqdoc.css test-suite/output/MExtraction.out test-suite/output/*.out.real test-suite/oUnit-anon.cache +test-suite/redirect_test.out test-suite/unit-tests/**/*.test # documentation diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index cdf00f4767..475f812b5a 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -349,7 +349,7 @@ ######################################################################## # perennial ######################################################################## -: "${perennial_CI_REF:=master}" +: "${perennial_CI_REF:=coq/tested}" : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh new file mode 100644 index 0000000000..ced0d95945 --- /dev/null +++ b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then + + fiat_parsers_CI_REF="factor-hint-flags" + fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat + +fi diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst new file mode 100644 index 0000000000..975c917b19 --- /dev/null +++ b/doc/changelog/04-tactics/12552-zify-pre-hook.rst @@ -0,0 +1,4 @@ +- **Added:** + Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c4947e6b3a..c01e6a5aa6 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -278,7 +278,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. - :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`. + :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are + respectively run in the first and the last steps of :tacn:`zify`. + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6290620ee1..4af3ebc47b 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3045,7 +3045,7 @@ following: For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. -.. tacn:: {? @strategy_flag } +.. tacn:: cbv {? @strategy_flag } lazy {? @strategy_flag } :name: cbv; lazy diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index f872c1b2e3..9ac3d2adda 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -1,3 +1,5 @@ +.. index:: coqdoc + .. _coqdoc: Documenting |Coq| files with coqdoc diff --git a/engine/eConstr.ml b/engine/eConstr.ml index ca681e58f8..42c9359ff0 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -733,6 +733,11 @@ let map_rel_context_in_env f env sign = in aux env [] (List.rev sign) +let match_named_context_val : + named_context_val -> (named_declaration * lazy_val * named_context_val) option = + match unsafe_eq with + | Refl -> match_named_context_val + let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, t diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 9a73c3e3f5..aea441b90b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -322,6 +322,9 @@ val lookup_named_val : variable -> named_context_val -> named_declaration val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context +val match_named_context_val : + named_context_val -> (named_declaration * lazy_val * named_context_val) option + (* XXX Missing Sigma proxy *) val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 5fcadfcef7..eea7e38f87 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -287,7 +287,7 @@ let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c = EConstr.of_constr c type ext_named_context = - csubst * Id.Set.t * EConstr.named_context + csubst * Id.Set.t * named_context_val let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } = let s = Int.Map.add n (Constr.mkVar id) s in @@ -325,22 +325,22 @@ type naming_mode = let push_rel_decl_to_named_context ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) - sigma decl (subst, avoid, nc) = + sigma decl ((subst, avoid, nc) : ext_named_context) = let open EConstr in let open Vars in let map_decl f d = NamedDecl.map_constr f d in - let rec replace_var_named_declaration id0 id = function - | [] -> [] - | decl :: nc -> + let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with + | None -> empty_named_context_val + | Some (decl, _, nc) -> if Id.equal id0 (NamedDecl.get_id decl) then (* Stop here, the variable cannot occur before its definition *) - (NamedDecl.set_id id decl) :: nc + push_named_context_val (NamedDecl.set_id id decl) nc else let nc = replace_var_named_declaration id0 id nc in let vsubst = [id0 , mkVar id] in - map_decl (fun c -> replace_vars vsubst c) decl :: nc + push_named_context_val (map_decl (fun c -> replace_vars vsubst c) decl) nc in let extract_if_neq id = function | Anonymous -> None @@ -372,7 +372,7 @@ let push_rel_decl_to_named_context let subst = update_var id0 id subst in let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = replace_var_named_declaration id0 id nc in - (push_var id0 subst, Id.Set.add id avoid, d :: nc) + (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc) | Some id0 when hypnaming = FailIfConflict -> user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> @@ -381,7 +381,7 @@ let push_rel_decl_to_named_context the new binder has name [id]. Which amounts to the same behaviour than when [id=id0]. *) let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in - (push_var id subst, Id.Set.add id avoid, d :: nc) + (push_var id subst, Id.Set.add id avoid, push_named_context_val d nc) let push_rel_context_to_named_context ?hypnaming env sigma typ = (* compute the instances relative to the named context and rel_context *) @@ -399,8 +399,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc) - (rel_context env) ~init:(empty_csubst, avoid, named_context env) in - (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) + (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in + (env, csubst_subst subst typ, inst_rels@inst_vars, subst) (*------------------------------------* * Entry points to define new evars * diff --git a/engine/evarutil.mli b/engine/evarutil.mli index b5c7ccb283..b3c94e6b3b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -268,7 +268,7 @@ val empty_csubst : csubst val csubst_subst : csubst -> constr -> constr type ext_named_context = - csubst * Id.Set.t * named_context + csubst * Id.Set.t * named_context_val val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context diff --git a/engine/evd.ml b/engine/evd.ml index ff13676818..f0ee8ae68f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1174,12 +1174,34 @@ let meta_declare mv v ?(name=Anonymous) evd = let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in set_metas evd metas +(* If the meta is defined then forget its name *) +let meta_name evd mv = + try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous + +let evar_source_of_meta mv evd = + match meta_name evd mv with + | Anonymous -> Loc.tag Evar_kinds.GoalEvar + | Name id -> Loc.tag @@ Evar_kinds.VarInstance id + +let use_meta_source evd mv v = + match Constr.kind v with + | Evar (evk,_) -> + let f = function + | None -> None + | Some evi as x -> + match evi.evar_source with + | None, Evar_kinds.GoalEvar -> Some { evi with evar_source = evar_source_of_meta mv evd } + | _ -> x in + { evd with undf_evars = EvMap.update evk f evd.undf_evars } + | _ -> evd + let meta_assign mv (v, pb) evd = let modify _ = function | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty) | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.") in let metas = Metamap.modify mv modify evd.metas in + let evd = use_meta_source evd mv v in set_metas evd metas let meta_reassign mv (v, pb) evd = @@ -1190,10 +1212,6 @@ let meta_reassign mv (v, pb) evd = let metas = Metamap.modify mv modify evd.metas in set_metas evd metas -(* If the meta is defined then forget its name *) -let meta_name evd mv = - try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous - let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge ?(with_univs = true) evd1 evd2 = @@ -1217,11 +1235,6 @@ let retract_coercible_metas evd = let metas = Metamap.Smart.mapi map evd.metas in !mc, set_metas evd metas -let evar_source_of_meta mv evd = - match meta_name evd mv with - | Anonymous -> Loc.tag Evar_kinds.GoalEvar - | Name id -> Loc.tag @@ Evar_kinds.VarInstance id - let dependent_evar_ident ev evd = let evi = find evd ev in match evi.evar_source with diff --git a/engine/univSubst.ml b/engine/univSubst.ml index a691239ee2..92211d5f3d 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -131,9 +131,9 @@ let nf_evars_and_universes_opt_subst f subst = let rec aux c = match kind c with | Evar (evk, args) -> - let args = List.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> mkEvar (evk, args) + let args' = List.Smart.map aux args in + (match try f (evk, args') with Not_found -> None with + | None -> if args == args' then c else mkEvar (evk, args') | Some c -> aux c) | Const pu -> let pu' = subst_univs_fn_puniverses lsubst pu in diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b3a4bd7471..59ae8c0745 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -130,7 +130,7 @@ type comp_env = { nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) - in_stack : int list; (* position in the stack *) + in_stack : int Range.t; (* position in the stack *) nb_rec : int; (* number of mutually recursive functions *) pos_rec : instruction list; (* instruction d'acces pour les variables *) (* de point fix ou de cofix *) @@ -158,7 +158,7 @@ let empty_comp_env ()= { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 0; @@ -188,13 +188,13 @@ let ensure_stack_capacity f x = (*i Creation functions for comp_env *) let rec add_param n sz l = - if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) + if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l) let comp_env_fun ?(univs=0) arity = { arity; nb_uni_stack = univs ; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = 0; pos_rec = []; offset = 1; @@ -206,7 +206,7 @@ let comp_env_fix_type rfv = { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 1; @@ -221,7 +221,7 @@ let comp_env_fix ndef curr_pos arity rfv = { arity; nb_uni_stack = 0; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = ndef; pos_rec = !prec; offset = 2 * (ndef - curr_pos - 1)+1; @@ -232,7 +232,7 @@ let comp_env_cofix_type ndef rfv = { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 1+ndef; @@ -247,7 +247,7 @@ let comp_env_cofix ndef arity rfv = { arity; nb_uni_stack = 0; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = ndef; pos_rec = !prec; offset = ndef+1; @@ -264,7 +264,7 @@ let push_param n sz r = let push_local sz r = { r with nb_stack = r.nb_stack + 1; - in_stack = (sz + 1) :: r.in_stack } + in_stack = Range.cons (sz + 1) r.in_stack } (*i Compilation of variables *) let find_at fv env = FvMap.find fv env.fv_fwd @@ -280,7 +280,7 @@ let pos_named id r = let pos_rel i r sz = if i <= r.nb_stack then - Kacc(sz - (List.nth r.in_stack (i-1))) + Kacc(sz - (Range.get r.in_stack (i-1))) else let i = i - r.nb_stack in if i <= r.nb_rec then diff --git a/kernel/environ.mli b/kernel/environ.mli index 79e632daa0..f489b13a3b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -176,6 +176,8 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a +val match_named_context_val : named_context_val -> (named_declaration * lazy_val * named_context_val) option + (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 3dd5059e5d..db3631daa4 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -205,10 +205,10 @@ open Hints let extend_with_auto_hints env sigma l seq = let f (seq,sigma) p_a_t = - match repr_hint p_a_t.code with - | Res_pf (c,_) | Give_exact (c,_) - | Res_pf_THEN_trivial_fail (c,_) -> - let (c, _, _) = c in + match FullHint.repr p_a_t with + | Res_pf c | Give_exact c + | Res_pf_THEN_trivial_fail c -> + let c = c.hint_term in (match EConstr.destRef sigma c with | exception Constr.DestKO -> seq, sigma | gr, _ -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 29a9c65561..da623703a2 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -389,17 +389,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl - with _ -> + with e when CErrors.noncritical e -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with | App (hd, args) -> let hd_ty = Retyping.get_type_of env sigma hd in - let names = let rec aux t = function 0 -> [] | n -> + let names = let rec aux env t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in let open EConstr in match kind_of_type sigma t with - | ProdType (name, _, t) -> name.binder_name :: aux t (n-1) - | _ -> assert false in aux hd_ty (Array.length args) in + | ProdType (name, ty, t) -> + name.binder_name :: + aux (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (name,ty)) env) t (n-1) + | _ -> + (* In the case the head is an HO constant it may accept more arguments *) + CList.init n (fun _ -> Names.Name.Anonymous) in aux env hd_ty (Array.length args) in hd_ty, Util.List.map_filter (fun (t, name) -> let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index fad41614b4..05abb86f46 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -33,6 +33,8 @@ type t = { (** For locating indices *) renamed_env : env; (** For name management *) + renamed_vars : EConstr.t list Lazy.t; + (** Identity instance of named_context of renamed_env, to maximize sharing *) extra : ext_named_context Lazy.t; (** Delay the computation of the evar extended environment *) lvar : ltac_var_map; @@ -42,10 +44,12 @@ let make ~hypnaming env sigma lvar = let get_extra env sigma = let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc) - (rel_context env) ~init:(empty_csubst, avoid, named_context env) in + (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in + let open Context.Named.Declaration in { static_env = env; renamed_env = env; + renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env)); extra = lazy (get_extra env sigma); lvar = lvar; } @@ -67,10 +71,12 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id = let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) let push_rel ~hypnaming sigma d env = - let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in + let open Context.Rel.Declaration in + let d' = map_name (ltac_interp_name env.lvar) d in let env = { static_env = push_rel d env.static_env; renamed_env = push_rel d' env.renamed_env; + renamed_vars = env.renamed_vars; extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra)); lvar = env.lvar; } in @@ -83,6 +89,7 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env = let env = { static_env = push_rel_context ctx env.static_env; renamed_env = push_rel_context ctx' env.renamed_env; + renamed_vars = env.renamed_vars; extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra)); lvar = env.lvar; } in @@ -95,13 +102,14 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env = Array.map get_annot ctx, env let new_evar env sigma ?src ?naming typ = - let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in - let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in - let (subst, _, nc) = Lazy.force env.extra in + let lazy inst_vars = env.renamed_vars in + let rec rel_list n accu = + if n <= 0 then accu + else rel_list (n - 1) (mkRel n :: accu) + in + let instance = rel_list (nb_rel env.renamed_env) inst_vars in + let (subst, _, sign) = Lazy.force env.extra in let typ' = csubst_subst subst typ in - let instance = inst_rels @ inst_vars in - let sign = val_of_named_context nc in new_evar_instance sign sigma typ' ?src ?naming instance let new_type_evar env sigma ~src = diff --git a/tactics/auto.ml b/tactics/auto.ml index 681c4e910f..f041af1db1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -29,7 +29,7 @@ open Hints (* tactics with a trace mechanism for automatic search *) (**************************************************************************) -let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l +let priority l = List.filter (fun (_, hint) -> Int.equal (FullHint.priority hint) 0) l let compute_secvars gl = let hyps = Proofview.Goal.hyps gl in @@ -69,7 +69,8 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv ~poly (c, _, ctx) clenv gl = +let connect_hint_clenv h gl = + let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in (* [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) @@ -77,7 +78,7 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl = let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in (* Still, we need to update the universes *) let clenv, c = - if poly then + if h.hint_poly then (* Refresh the instance of the hint *) let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in @@ -95,22 +96,22 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl = { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c -let unify_resolve ~poly flags ((c : raw_hint), clenv) = +let unify_resolve flags (h : hint) = Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv ~poly c clenv gl in + let clenv, c = connect_hint_clenv h gl in let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine clenv end -let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h +let unify_resolve_nodelta h = unify_resolve auto_unif_flags h -let unify_resolve_gen ~poly = function - | None -> unify_resolve_nodelta poly - | Some flags -> unify_resolve ~poly flags +let unify_resolve_gen = function + | None -> unify_resolve_nodelta + | Some flags -> unify_resolve flags -let exact poly (c,clenv) = +let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (exact_check c) @@ -381,16 +382,16 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) -and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = +and tac_of_hint dbg db_list local_db concl (flags, h) = let tactic = function - | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl) + | Res_pf h -> unify_resolve_gen flags h | ERes_pf _ -> Proofview.Goal.enter (fun gl -> let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info (str "eres_pf")) - | Give_exact (c, cl) -> exact poly (c, cl) - | Res_pf_THEN_trivial_fail (c,cl) -> + | Give_exact h -> exact h + | Res_pf_THEN_trivial_fail h -> Tacticals.New.tclTHEN - (unify_resolve_gen ~poly flags (c,cl)) + (unify_resolve_gen flags h) (* With "(debug) trivial", we shouldn't end here, and with "debug auto" we don't display the details of inner trivial *) (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db) @@ -403,16 +404,17 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= Tacticals.New.tclFAIL ~info 0 (str"Unbound reference") end | Extern tacast -> + let p = FullHint.pattern h in conclPattern concl p tacast in let pr_hint env sigma = - let origin = match dbname with + let origin = match FullHint.database h with | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint env sigma t ++ origin + FullHint.print env sigma h ++ origin in - tclLOG dbg pr_hint (run_hint t tactic) + tclLOG dbg pr_hint (FullHint.run h tactic) and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = try diff --git a/tactics/auto.mli b/tactics/auto.mli index 33deefd0bd..903da143d2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -24,10 +24,10 @@ val default_search_depth : int ref val auto_flags_of_state : TransparentState.t -> Unification.unify_flags val connect_hint_clenv - : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr + : hint -> Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic +val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index eaefa2947a..cc56de066d 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -212,60 +212,37 @@ let inHintRewrite : string * HintDN.t -> Libobject.obj = ~cache:cache_hintrewrite ~subst:(Some subst_hintrewrite) -open Clenv - type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; + hyp_ty : EConstr.types; + hyp_pat : EConstr.constr; } -let decompose_applied_relation metas env sigma c ctype left2right = +let decompose_applied_relation env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in - let eqclause = - if metas then eqclause - else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)) - in - let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> raise Not_found - in - try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in - (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) - let open EConstr in - let hyp_ty = Unsafe.to_constr ty in - let hyp_car = Unsafe.to_constr ty1 in - let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in - let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in - let hyp_left = Unsafe.to_constr @@ c1 in - let hyp_right = Unsafe.to_constr @@ c2 in -(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) -(* else *) - Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; } - with Not_found -> None + (* FIXME: this is nonsense, we generate evars and then we drop the + corresponding evarmap. This sometimes works because [Term_dnet] performs + evar surgery via [Termops.filtering]. *) + let sigma, ty = Clenv.make_evar_clause env sigma ty in + let (_, args) = Termops.decompose_app_vect sigma ty.Clenv.cl_concl in + let len = Array.length args in + if 2 <= len then + let c1 = args.(len - 2) in + let c2 = args.(len - 1) in + Some (if left2right then c1 else c2) + else None in match find_rel ctype with - | Some c -> Some c + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' ctx) with - | Some c -> Some c + let ctype = it_mkProd_or_LetIn t' ctx in + match find_rel ctype with + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> None -let find_applied_relation ?loc metas env sigma c left2right = +let find_applied_relation ?loc env sigma c left2right = let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in - match decompose_applied_relation metas env sigma c ctype left2right with + match decompose_applied_relation env sigma c ctype left2right with | Some c -> c | None -> user_err ?loc ~hdr:"decompose_applied_relation" @@ -283,9 +260,9 @@ let add_rew_rules base lrul = List.fold_left (fun dn {CAst.loc;v=((c,ctx),b,t)} -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation ?loc false env sigma c b in - let pat = if b then info.hyp_left else info.hyp_right in - let rul = { rew_lemma = c; rew_type = info.hyp_ty; + let info = find_applied_relation ?loc env sigma c b in + let pat = EConstr.Unsafe.to_constr info.hyp_pat in + let rul = { rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; rew_tac = Option.map intern t} in incr counter; diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 8f7a1c8fcf..974aef8e8f 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -43,22 +43,3 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic val print_rewrite_hintdb : string -> Pp.t - -open Clenv - - -type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; -} - -val find_applied_relation : - ?loc:Loc.t -> bool -> - Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo - diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 195073d7aa..484aab2f00 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -144,13 +144,13 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = resolve_evars = false } -let e_give_exact flags poly (c,clenv) = +let e_give_exact flags h = + let { hint_term = c; hint_clnv = clenv } = h in let open Tacmach.New in Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let (c, _, _) = c in let c, sigma = - if poly then + if h.hint_poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in let c = Vars.subst_univs_level_constr subst c in @@ -173,23 +173,24 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end -let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> - let clenv', c = connect_hint_clenv ~poly c clenv gls in +let unify_e_resolve flags = begin fun gls (h, _) -> + let clenv', c = connect_hint_clenv h gls in clenv_unique_resolver_tac true ~flags clenv' end -let unify_resolve poly flags = begin fun gls (c,_,clenv) -> - let clenv', _ = connect_hint_clenv ~poly c clenv gls in +let unify_resolve flags = begin fun gls (h, _) -> + let clenv', _ = connect_hint_clenv h gls in clenv_unique_resolver_tac false ~flags clenv' end (** Application of a lemma using [refine] instead of the old [w_unify] *) -let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = +let unify_resolve_refine flags gls (h, n) = + let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in let open Clenv in let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in Refine.refine ~typecheck:false begin fun sigma -> let sigma, term, ty = - if poly then + if h.hint_poly then let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in @@ -206,9 +207,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = env sigma' cl.cl_concl concl) in (sigma', term) end -let unify_resolve_refine poly flags gl clenv = +let unify_resolve_refine flags gl clenv = Proofview.tclORELSE - (unify_resolve_refine poly flags gl clenv) + (unify_resolve_refine flags gl clenv) (fun (exn,info) -> match exn with | Evarconv.UnableToUnify _ -> @@ -221,8 +222,8 @@ let unify_resolve_refine poly flags gl clenv = (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. *) -let clenv_of_prods poly nprods (c, clenv) gl = - let (c, _, _) = c in +let clenv_of_prods nprods h gl = + let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in if poly || Int.equal nprods 0 then Some (None, clenv) else let sigma = Tacmach.New.project gl in @@ -234,20 +235,22 @@ let clenv_of_prods poly nprods (c, clenv) gl = mk_clenv_from_n gl (Some diff) (c,ty)) else None -let with_prods nprods poly (c, clenv) f = +let with_prods nprods h f = if get_typeclasses_limit_intros () then Proofview.Goal.enter begin fun gl -> - try match clenv_of_prods poly nprods (c, clenv) gl with + try match clenv_of_prods nprods h gl with | None -> let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info (str"Not enough premisses") - | Some (diff, clenv') -> f gl (c, diff, clenv') + | Some (diff, clenv') -> + let h = { h with hint_clnv = clenv' } in + f gl (h, diff) with e when CErrors.noncritical e -> let e, info = Exninfo.capture e in Tacticals.New.tclZEROMSG ~info (CErrors.print e) end else Proofview.Goal.enter begin fun gl -> - if Int.equal nprods 0 then f gl (c, None, clenv) + if Int.equal nprods 0 then f gl (h, None) else Tacticals.New.tclZEROMSG (str"Not enough premisses") end let matches_pattern concl pat = @@ -346,44 +349,47 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm with e when CErrors.noncritical e -> AllowAll in let tac_of_hint = - fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) -> + fun (flags, h) -> + let b = FullHint.priority h in + let p = FullHint.pattern h in + let name = FullHint.name h in let tac = function - | Res_pf (term,cl) -> + | Res_pf h -> if get_typeclasses_filtered_unification () then let tac = - with_prods nprods poly (term,cl) + with_prods nprods h (fun gl clenv -> matches_pattern concl p <*> - unify_resolve_refine poly flags gl clenv) + unify_resolve_refine flags gl clenv) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods poly (term,cl) (unify_resolve poly flags) in + with_prods nprods h (unify_resolve flags) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) - | ERes_pf (term,cl) -> + | ERes_pf h -> if get_typeclasses_filtered_unification () then - let tac = (with_prods nprods poly (term,cl) + let tac = (with_prods nprods h (fun gl clenv -> matches_pattern concl p <*> - unify_resolve_refine poly flags gl clenv)) in + unify_resolve_refine flags gl clenv)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in + with_prods nprods h (unify_e_resolve flags) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) - | Give_exact (c,clenv) -> + | Give_exact h -> if get_typeclasses_filtered_unification () then let tac = matches_pattern concl p <*> Proofview.Goal.enter - (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in + (fun gl -> unify_resolve_refine flags gl (h, None)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else - e_give_exact flags poly (c,clenv) - | Res_pf_THEN_trivial_fail (term,cl) -> - let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in + e_give_exact flags h + | Res_pf_THEN_trivial_fail h -> + let fst = with_prods nprods h (unify_e_resolve flags) in let snd = if complete then Tacticals.New.tclIDTAC else e_trivial_fail_db only_classes db_list local_db secvars in Tacticals.New.tclTHEN fst snd @@ -391,7 +397,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c]) | Extern tacast -> conclPattern concl p tacast in - let tac = run_hint t tac in + let tac = FullHint.run h tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in let pp = match p with @@ -399,9 +405,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat | _ -> mt () in - match repr_hint t with - | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) - | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) + match FullHint.repr h with + | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp)) + | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp)) in let hint_of_db = hintmap_of sigma hdc secvars concl in let hintl = List.map_filter (fun db -> match hint_of_db db with @@ -499,7 +505,7 @@ let evars_to_goals p evm = else Some (goals, nongoals) (** Making local hints *) -let make_resolve_hyp env sigma st flags only_classes pri decl = +let make_resolve_hyp env sigma st only_classes pri decl = let id = NamedDecl.get_id decl in let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in let rec iscl env ty = @@ -524,13 +530,11 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (List.map_append (fun (path,info,c) -> let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in - make_resolves env sigma ~name:(PathHints path) - (true,false,not !Flags.quiet) info ~check:true ~poly:false - h) + make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h) hints) else [] in - (hints @ make_resolves env sigma flags pri ~name ~check:false ~poly:false (IsGlobRef id)) + (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id)) else [] let make_hints g (modes,st) only_classes sign = @@ -546,7 +550,7 @@ let make_hints g (modes,st) only_classes sign = in if consider then let hint = - pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp + pf_apply make_resolve_hyp g st only_classes empty_hint_info hyp in hint @ hints else hints) ([]) sign @@ -793,7 +797,7 @@ module Search = struct let decl = Tacmach.New.pf_last_hyp gl in let hint = make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints) - (true,false,false) info.search_only_classes empty_hint_info decl in + info.search_only_classes empty_hint_info decl in let ldb = Hint_db.add_list env sigma hint info.search_hints in let info' = { info with search_hints = ldb; last_tac = lazy (str"intro"); @@ -1246,7 +1250,8 @@ let autoapply c i = (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> + let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in + unify_e_resolve flags gl (h, 0) <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c2eabffd44..0ff90bc046 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -65,9 +65,9 @@ open Auto (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) -let unify_e_resolve poly flags (c,clenv) = +let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv h gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) @@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl = else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) -let e_exact poly flags (c,clenv) = +let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (e_give_exact c) @@ -120,23 +120,23 @@ and e_my_find_search env sigma db_list local_db secvars concl = List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) in let tac_of_hint = - fun (st, {pri = b; pat = p; code = t; poly = poly}) -> - let b = match Hints.repr_hint t with + fun (st, h) -> + let b = match FullHint.repr h with | Unfold_nth _ -> 1 - | _ -> b + | _ -> FullHint.priority h in let tac = function - | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> e_exact poly st (c,cl) - | Res_pf_THEN_trivial_fail (term,cl) -> - Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) + | Res_pf h -> unify_resolve st h + | ERes_pf h -> unify_e_resolve st h + | Give_exact h -> e_exact st h + | Res_pf_THEN_trivial_fail h -> + 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 p tacast + | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast in - let tac = run_hint t tac in - (tac, b, lazy (pr_hint env sigma t)) + let tac = FullHint.run h tac in + (tac, b, lazy (FullHint.print env sigma h)) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index 0c23532e12..7a5615dd8e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -135,15 +135,20 @@ type 'a with_uid = { uid : KerName.t; } -type raw_hint = constr * types * Univ.ContextSet.t - -type hint = (raw_hint * clausenv) hint_ast with_uid +type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *) + +type hint = { + hint_term : constr; + hint_type : types; + hint_uctx : Univ.ContextSet.t; + hint_clnv : clausenv; + hint_poly : bool; + (** Is the hint polymorpic and hence should be refreshed at each application *) +} type 'a with_metadata = { pri : int (** A number lower is higher priority *) - ; poly : bool - (** Is the hint polymorpic and hence should be refreshed at each application *) ; pat : constr_pattern option (** A pattern for the concl of the Goal *) ; name : hints_path_atom @@ -156,7 +161,7 @@ type 'a with_metadata = (** the tactic to apply when the concl matches pat *) } -type full_hint = hint with_metadata +type full_hint = hint hint_ast with_uid with_metadata type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata @@ -300,19 +305,21 @@ let strip_params env sigma c = | _ -> c let instantiate_hint env sigma p = - let mk_clenv (c, cty, ctx) = + let mk_clenv (c, cty, ctx, poly) = let sigma = Evd.merge_context_set univ_flexible sigma ctx in let cl = mk_clenv_from_env env sigma None (c,cty) in - {cl with templval = + let cl = {cl with templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; env = empty_env} + in + { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly } in let code = match p.code.obj with - | Res_pf c -> Res_pf (c, mk_clenv c) - | ERes_pf c -> ERes_pf (c, mk_clenv c) + | Res_pf c -> Res_pf (mk_clenv c) + | ERes_pf c -> ERes_pf (mk_clenv c) | Res_pf_THEN_trivial_fail c -> - Res_pf_THEN_trivial_fail (c, mk_clenv c) - | Give_exact c -> Give_exact (c, mk_clenv 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 in @@ -489,7 +496,6 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t -val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> @@ -800,9 +806,9 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = | None -> pat in (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (Give_exact (c, cty, ctx)); }) + code = with_uid (Give_exact (c, cty, ctx, poly)); }) let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -824,10 +830,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( in if Int.equal nmiss 0 then (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (Res_pf(c,cty,ctx)); }) + code = with_uid (Res_pf(c,cty,ctx,poly)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then begin @@ -843,9 +849,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( ) end; (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) + code = with_uid (ERes_pf(c,cty,ctx,poly)); }) end | _ -> failwith "make_apply_entry" @@ -916,7 +922,6 @@ let make_unfold eref = let g = global_of_evaluable_reference eref in (Some g, { pri = 4; - poly = false; pat = None; name = PathHints [g]; db = None; @@ -927,7 +932,6 @@ let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri = pri; - poly = false; pat = pat; name = PathAny; db = None; @@ -954,12 +958,11 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; - poly = poly; pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); name = name; db = None; secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) }) @@ -1070,29 +1073,30 @@ let subst_autohint (subst, obj) = (try head_constr_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 + let subst_aux ((c, t, ctx, poly) as h) = + let c' = subst_mps subst c in + let t' = subst_mps subst t in + if c==c' && t'==t then h else (c', t', ctx, poly) + in let subst_hint (k,data as hint) = let k' = Option.Smart.map subst_key k in let env = Global.env () in let sigma = Evd.from_env env in let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in - let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with - | Res_pf (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx) - | ERes_pf (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) - | Give_exact (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) - | Res_pf_THEN_trivial_fail (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx) + | Res_pf h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Res_pf h' + | ERes_pf h -> + let h' = subst_aux h in + if h == h' then data.code.obj else ERes_pf h' + | Give_exact h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Give_exact h' + | Res_pf_THEN_trivial_fail h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Res_pf_THEN_trivial_fail h' | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' @@ -1336,6 +1340,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun (poly, lem) -> make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems +let make_resolves env sigma info ~check ~poly ?name hint = + make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in let lems = List.map map lems in @@ -1365,13 +1372,13 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c +let pr_hint_elt env sigma h = pr_econstr_env env sigma h.hint_term let pr_hint env sigma h = match h.obj with - | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) - | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) - | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) - | Res_pf_THEN_trivial_fail (c, _) -> + | Res_pf c -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf c -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact c -> (str"exact " ++ pr_hint_elt env sigma c) + | Res_pf_THEN_trivial_fail c -> (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> str"unfold " ++ pr_evaluable_reference c @@ -1574,4 +1581,15 @@ let run_hint tac k = match warn_hint () with let info = Exninfo.reify () in Proofview.tclZERO ~info (UserError (None, (str "Tactic failure."))) -let repr_hint h = h.obj +module FullHint = +struct + type t = full_hint + let priority (h : t) = h.pri + let pattern (h : t) = h.pat + let database (h : t) = h.db + let run (h : t) k = run_hint h.code k + let print env sigma (h : t) = pr_hint env sigma h.code + let name (h : t) = h.name + + let repr (h : t) = h.code.obj +end diff --git a/tactics/hints.mli b/tactics/hints.mli index 6c8b7fed75..8243716624 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -15,7 +15,6 @@ open Environ open Evd open Tactypes open Clenv -open Pattern open Typeclasses (** {6 General functions. } *) @@ -40,8 +39,13 @@ type 'a hint_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hint -type raw_hint = constr * types * Univ.ContextSet.t +type hint = { + hint_term : constr; + hint_type : types; + hint_uctx : Univ.ContextSet.t; + hint_clnv : clausenv; + hint_poly : bool; +} type 'a hints_path_atom_gen = | PathHints of 'a list @@ -51,26 +55,20 @@ type 'a hints_path_atom_gen = type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string -type 'a with_metadata = private - { pri : int - (** A number lower is higher priority *) - ; poly : bool - (** Is the hint polymorpic and hence should be refreshed at each application *) - ; pat : constr_pattern option - (** A pattern for the concl of the Goal *) - ; name : hints_path_atom - (** A potential name to refer to the hint *) - ; db : string option - (** The database from which the hint comes *) - ; secvars : Id.Pred.t - (** The set of section variables the hint depends on *) - ; code : 'a - (** the tactic to apply when the concl matches pat *) - } - -type full_hint = hint with_metadata - -type search_entry +module FullHint : +sig + type t + val priority : t -> int + val pattern : t -> Pattern.constr_pattern option + val database : t -> string option + val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic + val name : t -> hints_path_atom + val print : env -> evar_map -> t -> Pp.t + + (** This function is for backward compatibility only, not to use in newly + written code. *) + val repr : t -> hint hint_ast +end (** The head may not be bound. *) @@ -117,42 +115,41 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t - val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that * can be used in the hint. *) - val map_none : secvars:Id.Pred.t -> t -> full_hint list + val map_none : secvars:Id.Pred.t -> t -> FullHint.t list (** All hints associated to the reference *) - val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> FullHint.t list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. Returns a [ModeMismatch] if there are declared modes and none matches. *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode + (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. Returns a [ModeMismatch] if there are declared modes and none matches. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode (** All hints associated to the reference. Precondition: no evars should appear in the arguments, so no modes are checked. *) val map_auto : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> FullHint.t list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t val remove_one : GlobRef.t -> t -> t val remove_list : GlobRef.t list -> t -> t val iter : (GlobRef.t option -> - hint_mode array list -> full_hint list -> unit) -> t -> unit + hint_mode array list -> FullHint.t list -> unit) -> t -> unit - val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a + val fold : (GlobRef.t option -> hint_mode array list -> FullHint.t list -> 'a -> 'a) -> t -> 'a -> 'a val use_dn : t -> bool val transparent_state : t -> TransparentState.t @@ -214,7 +211,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> + env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. @@ -225,19 +222,6 @@ val make_resolves : val make_resolve_hyp : env -> evar_map -> named_declaration -> hint_entry list -(** [make_extern pri pattern tactic_expr] *) - -val make_extern : - int -> constr_pattern option -> Genarg.glob_generic_argument - -> hint_entry - -val run_hint : hint -> - ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic - -(** This function is for backward compatibility only, not to use in newly - written code. *) -val repr_hint : hint -> (raw_hint * clausenv) hint_ast - (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) @@ -262,4 +246,3 @@ val pr_applicable_hint : Proof.t -> Pp.t val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t -val pr_hint : env -> evar_map -> hint -> Pp.t diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index 8fd7398638..a12623c3c0 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -159,7 +159,7 @@ Require Import ZifyClasses. Require Import ZifyInst. Instance Zero : CstOp (@zero znat : nat) := Op_O. -Add CstOp Zero. +Add Zify CstOp Zero. Goal @zero znat = 0%nat. @@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0. Proof. intros. lia. Qed. + +Ltac Zify.zify_pre_hook ::= unfold is_true in *. + +Goal forall x y : nat, is_true (Nat.eqb x 1) -> + is_true (Nat.eqb y 0) -> + is_true (Nat.eqb (x + y) 1). +Proof. +lia. +Qed. diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out index 9ca3fa3357..2e69b94505 100644 --- a/test-suite/output-coqtop/DependentEvars.out +++ b/test-suite/output-coqtop/DependentEvars.out @@ -77,14 +77,14 @@ p14 < 3 focused subgoals p123 : (P1 -> P2) -> P3 p34 : P3 -> P4 ============================ - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 2 is: - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 3 is: ?P -(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11) p14 < Coq < diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out index 29ebba7c86..63bfafa88d 100644 --- a/test-suite/output-coqtop/DependentEvars2.out +++ b/test-suite/output-coqtop/DependentEvars2.out @@ -90,13 +90,13 @@ Try unfocusing with "}". (shelved: 2) subgoal 1 is: - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 2 is: - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 3 is: ?P -(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:) +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:) p14 < 3 focused subgoals (shelved: 2) @@ -106,14 +106,14 @@ p14 < 3 focused subgoals p123 : (P1 -> P2) -> P3 p34 : P3 -> P4 ============================ - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 2 is: - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 3 is: ?P -(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11) p14 < Coq < diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out index dfd755da61..cf31871e5a 100644 --- a/test-suite/output/unification.out +++ b/test-suite/output/unification.out @@ -9,3 +9,27 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate The command has indeed failed with message: The term "id" has type "ID" while it is expected to have type "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). +1 focused subgoal +(shelved: 1) + + H : forall x : nat, S (S (S x)) = x + ============================ + ?x = 0 +1 focused subgoal +(shelved: 1) + + H : forall x : nat, S (S (S x)) = x + ============================ + ?x = 0 +1 focused subgoal +(shelved: 1) + + H : forall x : nat, S (S (S x)) = x + ============================ + ?x = 0 +1 focused subgoal +(shelved: 1) + + H : forall x : nat, S x = x + ============================ + ?y = 0 diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v index ff99f2e23c..fe7366a97d 100644 --- a/test-suite/output/unification.v +++ b/test-suite/output/unification.v @@ -10,3 +10,29 @@ Fail Check fun x => match x return ?[X] with C a => a end. Fail Check (id:Type -> _). End A. + +(* Choice of evar names *) + +Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0. +eexists. +rewrite H. +Show. +Undo 2. +eexists ?[x]. +rewrite H. +Show. +Undo 2. +eexists ?[y]. +rewrite H. +Show. +reflexivity. +Qed. + +(* Preserve the name if there is one *) + +Goal (forall x, S x = x) -> exists x, S x = 0. +eexists ?[y]. +rewrite H. +Show. +reflexivity. +Qed. diff --git a/test-suite/ssr/rewrtite_err_msg.v b/test-suite/ssr/rewrtite_err_msg.v new file mode 100644 index 0000000000..2bbbff433c --- /dev/null +++ b/test-suite/ssr/rewrtite_err_msg.v @@ -0,0 +1,30 @@ +Require Import ssreflect ssrbool. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Axiom finGroupType : Type. +Axiom group : finGroupType -> Type. +Axiom abelian : forall gT : finGroupType, group gT -> Prop. +Arguments abelian {_} _. +Axiom carrier : finGroupType -> Type. +Coercion carrier : finGroupType >-> Sortclass. +Axiom mem : forall gT : finGroupType, gT -> group gT -> Prop. +Arguments mem {_} _ _. +Axiom mul : forall gT : finGroupType, gT -> gT -> gT. +Arguments mul {_} _ _. +Definition centralised gT (G : group gT) (x : gT) := forall y, mul x y = mul y x. +Arguments centralised {gT} _. +Axiom b : bool. + +Axiom centsP : forall (gT : finGroupType) (A B : group gT), + reflect (forall a, mem a A -> centralised B a) b. +Arguments centsP {_ _ _}. + +Lemma commute_abelian (gT : finGroupType) (G : group gT) + (G_abelian : abelian G) (g g' : gT) (gG : mem g G) (g'G : mem g' G) : + mul g g' = mul g' g. +Proof. +Fail rewrite (centsP _). (* fails but without an anomaly *) +Abort. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index b46ddaa32b..5862a08838 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -264,7 +264,7 @@ Class DependentEliminationPackage (A : Type) := Ltac elim_tac tac p := let ty := type of p in - let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in + let eliminator := eval simpl in (@elim _ (_ : DependentEliminationPackage ty)) in tac p eliminator. (** Specialization to do case analysis or induction. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 33e40a115b..4fa8b3216a 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1774,6 +1774,28 @@ Proof. now rewrite <- INR_IPR, SuccNat2Pos.id_succ. Qed. +Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)). +Proof. + reflexivity. +Qed. + +(** The three following lemmas map the default form of numerical + constants to their representation in terms of the axioms of + [R]. This can be a useful intermediate representation for reifying + to another axiomatics of the reals. It is however generally more + convenient to keep constants represented under an [IZR z] form when + working within [R]. *) + +Lemma IZR_POS_xO : forall p, IZR (Zpos (xO p)) = (1+1) * (IZR (Zpos p)). +Proof. + intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial. +Qed. + +Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + (1+1) * IZR (Zpos p). +Proof. + intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial. +Qed. + Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 2df3c57d32..183fd6a914 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -11,12 +11,15 @@ Require Import ZifyClasses ZifyInst. Declare ML Module "zify_plugin". -(** [zify_post_hook] is there to be redefined. *) +(** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *) +Ltac zify_pre_hook := idtac. + Ltac zify_post_hook := idtac. Ltac iter_specs := zify_iter_specs. Ltac zify := intros; + zify_pre_hook ; zify_elim_let ; zify_op ; (zify_iter_specs) ; diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2c5faa4df7..79de3c86b6 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -499,7 +499,7 @@ let rec vernac_loop ~state = if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); resynch_buffer top_buffer; let state, drop = read_and_execute ~state in - if drop then state else vernac_loop ~state + if drop then state else (vernac_loop [@ocaml.tailcall]) ~state (* Default toplevel loop, machinery for drop is below *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c4c8492a4a..92e664d56b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -110,7 +110,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let state = Flags.silently (interp_vernac ~check ~interactive ~state) ast in - loop state (state.sid :: ids) + (loop [@ocaml.tailcall]) state (state.sid :: ids) in try loop state [] with any -> (* whatever the exception *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 95489c9132..e490b33dde 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -60,23 +60,28 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } +exception Same of Id.t + let check_all_names_different indl = + let rec elements = function + | [] -> Id.Set.empty + | id :: l -> + let s = elements l in + if Id.Set.mem id s then raise (Same id) else Id.Set.add id s + in let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in - let l = List.duplicates Id.equal ind_names in - let () = match l with - | [] -> () - | t :: _ -> raise (InductiveError (SameNamesTypes t)) + let ind_names = match elements ind_names with + | s -> s + | exception (Same t) -> raise (InductiveError (SameNamesTypes t)) in - let l = List.duplicates Id.equal cstr_names in - let () = match l with - | [] -> () - | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l))) + let cstr_names = match elements cstr_names with + | s -> s + | exception (Same c) -> raise (InductiveError (SameNamesConstructors c)) in - let l = List.intersect Id.equal ind_names cstr_names in - match l with - | [] -> () - | _ -> raise (InductiveError (SameNamesOverlap l)) + let l = Id.Set.inter ind_names cstr_names in + if not (Id.Set.is_empty l) then + raise (InductiveError (SameNamesOverlap (Id.Set.elements l))) (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 7d25e6b852..7ab21141df 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -166,8 +166,6 @@ let rec interp_expr ~atts ~st c = interp_typed_vernac ~stack fv and vernac_load ~verbosely fname = - let exception End_of_input in - (* Note that no proof should be open here, so the state here is just token for now *) let st = Vernacstate.freeze_interp_state ~marshallable:false in let fname = @@ -180,20 +178,15 @@ and vernac_load ~verbosely fname = (* Parsing loop *) let v_mod = if verbosely then Flags.verbosely else Flags.silently in let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing - (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with - | Some x -> x - | None -> raise End_of_input) in + (Pcoq.Entry.parse (Pvernac.main_entry proof_mode)) + in let rec load_loop ~stack = - try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in - let stack = - v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) - (parse_sentence proof_mode input) in - load_loop ~stack - with - End_of_input -> - stack + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + match parse_sentence proof_mode input with + | None -> stack + | Some stm -> + let stack = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) stm in + (load_loop [@ocaml.tailcall]) ~stack in let stack = load_loop ~stack:st.Vernacstate.lemmas in (* If Load left a proof open, we fail too. *) |