diff options
33 files changed, 362 insertions, 773 deletions
@@ -18,6 +18,7 @@ CJ Bell <cj@csail.mit.edu> CJ Bell <siegebell@gmail.com> Yves Bertot <yves.bertot@inria.fr> bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> +Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@nardis.inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> @@ -33,6 +34,8 @@ Pierre Courtieu <Pierre.Courtieu@cnam.fr> courtieu <courtieu@85f007b7-5 David Delahaye <delahaye@gforge> delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> +Maxime Dénès <mail@maximedenes.fr> Maxime Dénès <maxime.denes@fondation-inria.fr> +Maxime Dénès <mail@maximedenes.fr> Maxime Dénès <maxime.denes@inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> İsmail Dönmez <ismail-s@users.noreply.github.com> Ismail <ismail-s@users.noreply.github.com> @@ -68,6 +71,7 @@ Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-5 Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> +Matej Košík <matej.kosik@inria.fr> Matej Košík <mail@matej-kosik.net> Ambroise Lafont <chaster_killer@hotmail.fr> amblaf <you@example.com> Ambroise Lafont <chaster_killer@hotmail.fr> Ambroise <chaster_killer@hotmail.fr> Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> @@ -87,6 +91,7 @@ Guillaume Melquiond <guillaume.melquiond@inria.fr> gmelquio <gmelquio@85f007b7-5 Guillaume Melquiond <guillaume.melquiond@inria.fr> Guillaume Melquiond <guillaume.melquiond@gmail.com> Alexandre Miquel <miquel@gforge> miquel <miquel@85f007b7-540e-0410-9357-904b9bb8a0f7> Benjamin Monate <monate@gforge> monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> +Erik Martin-Dorel <erik.martin-dorel@irit.fr> Erik Martin-Dorel <erik@martin-dorel.org> Julien Narboux <jnarboux@gforge> jnarboux <jnarboux@85f007b7-540e-0410-9357-904b9bb8a0f7> Julien Narboux <jnarboux@gforge> narboux <narboux@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Marc Notin <notin@gforge> notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty <notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -107,6 +112,7 @@ Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@g Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> +Pierre Roux <pierre@roux01.fr> Pierre Roux <pierre.roux@onera.fr> Matthew Ryan <mr_1993@hotmail.co.uk> mrmr1993 <mr_1993@hotmail.co.uk> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> @@ -126,8 +132,12 @@ Enrico Tassi <Enrico.Tassi@inria.fr> Enrico <gares@fettunta.org> Laurent Théry <laurent.thery@inria.fr> thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> Laurent Théry <laurent.thery@inria.fr> thery <thery@sophia.inria.fr> Laurent Théry <laurent.thery@inria.fr> Laurent Théry <thery@sophia.inria.fr> +Laurent Théry <laurent.thery@inria.fr> thery <Laurent.Thery@inria.fr> Anton Trunov <anton.a.trunov@gmail.com> Anton Trunov <anton.trunov@imdea.org> Benjamin Werner <werner@gforge> werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7> +Wang Zhuyang <hawnzug@gmail.com> hawnzug <hawnzug@gmail.com> +Beta Ziliani <beta@mpi-sws.org> Beta Ziliani <bziliani@famaf.unc.edu.ar> +Beta Ziliani <beta@mpi-sws.org> beta <beta@mpi-sws.org> Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Theo Zimmermann <theo.zimmermann@ens.fr> Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo.zimmi@gmail.com> diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4533a4dc01..9e0d47651e 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -203,12 +203,6 @@ Termops - Internal printing functions have been placed under the `Termops.Internal` namespace. -Notations: - -- Notation.availability_of_notation is not anymore needed: if a - delimiter is needed, it is provided by Notation.uninterp_notation - which fails in case the notation is not available. - ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 63df3d37bf..3ca1dda4d6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1040,8 +1040,6 @@ interpreted in the scope stack extended with the scope bound tokey. To remove a delimiting key of a scope, use the command :n:`Undelimit Scope @scope` -.. _ArgumentScopes: - Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1311,65 +1309,6 @@ Displaying information about scopes It also displays the delimiting key if any and the class to which the scope is bound, if any. -Impact of scopes on printing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When several notations are available for printing the same expression, -Coq will use the following rules for printing priorities: - -- If two notations are available in different scopes which are open, - the notation in the more recently opened scope takes precedence. - -- If two notations are available in the same scope, the more recently - defined (or imported) notation takes precedence. - -- Abbreviations and lonely notations, both of which have no scope, - take precedence over a notation in an open scope if and only if the - abbreviation or lonely notation was defined (or imported) more - recently than when the corresponding scope was open. They take - precedence over any notation not in an open scope, whether this scope - has a delimiter or not. - -- A scope is *active* for printing a term either because it was opened - with :cmd:`Open Scope`, or the term is the immediate argument of a - constant which temporarily opens a scope for this argument (see - :ref:`Arguments <ArgumentScopes>`) in which case this temporary - scope is the most recent open one. - -- In case no abbreviation, nor lonely notation, nor notation in an - explicitly open scope, nor notation in a temporarily open scope of - arguments, has been found, notations in those closed scopes which - have a delimiter are considered, giving priority to the most - recently defined (or imported) ones. The corresponding delimiter is - inserted, making the corresponding scope the most recent explicitly - open scope for all subterms of the current term. As an exception to - the insertion of the corresponding delimiter, when an expression is - statically known to be in a position expecting a type and the - notation is from scope ``type_scope``, and the latter is closed, the - delimiter is not inserted. This is because expressions statically - known to be in a position expecting a type are by default - interpreted with `type_scope` temporarily activated. Expressions - statically known to be in a position expecting a type typically - include being on the right-hand side of `:`, `<:`, `<<:` and after - the comma in a `forall` expression. - -- As a refinement of the previous rule, in the case of applied global - references, notations in a non-opened scope with delimiter - specifically defined for this applied global reference take priority - over notations in a non-opened scope with delimiter for generic - applications. For instance, in the presence of ``Notation "f ( x - )" := (f x) (at level 10, format "f ( x )") : app_scope`` and - ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : - mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being - bound to a delimiter *and* both not opened, the latter, more - specific notation will always take precedence over the first, more - generic one. - -- A scope can be closed by using :cmd:`Close Scope` and its delimiter - removed by using :cmd:`Undelimit Scope`. To remove automatic - temporary opening of scopes for arguments of a constant, use - :ref:`Arguments <ArgumentScopes>`. - .. _Abbreviations: Abbreviations diff --git a/engine/proofview.ml b/engine/proofview.ml index 316f02bc37..f278c83912 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -345,29 +345,19 @@ let tclBREAK = Proof.break exception NoSuchGoals of int -(* This hook returns a string to be appended to the usual message. - Primarily used to add a suggestion about the right bullet to use to - focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ()) -let set_nosuchgoals_hook f = nosuchgoals_hook := f - - - -(* This uses the hook above *) let _ = CErrors.register_handler begin function | NoSuchGoals n -> - let suffix = !nosuchgoals_hook n in - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) - | _ -> raise CErrors.Unhandled + CErrors.user_err + (str "No such " ++ str (String.plural n "goal") ++ str ".") + | _ -> raise CErrors.Unhandled end -(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where +(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where only the goals numbered [i] to [j] are focused (the rest of the goals is restored at the end of the tactic). If the range [i]-[j] is not valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *) -let tclFOCUS_gen nosuchgoal i j t = +let tclFOCUS ?nosuchgoal i j t = + let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in let open Proof in Pv.get >>= fun initial -> try @@ -378,10 +368,9 @@ let tclFOCUS_gen nosuchgoal i j t = return result with CList.IndexOutOfRange -> nosuchgoal -let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t -let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t +let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t -let tclFOCUSLIST l t = +let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = let open Proof in Comb.get >>= fun comb -> let n = CList.length comb in @@ -395,7 +384,7 @@ let tclFOCUSLIST l t = in let l = CList.map_filter sanitize l in match l with - | [] -> tclZERO (NoSuchGoals 0) + | [] -> nosuchgoal | (mi, _) :: _ -> (* Get the left-most goal to focus. This goal won't move, and we will then place all the other goals to focus to the right. *) @@ -412,7 +401,7 @@ let tclFOCUSLIST l t = (** Like {!tclFOCUS} but selects a single goal by name. *) -let tclFOCUSID id t = +let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = let open Proof in Pv.get >>= fun initial -> try @@ -432,7 +421,7 @@ let tclFOCUSID id t = t >>= fun result -> Comb.set initial.comb >> return result - with Not_found -> tclZERO (NoSuchGoals 1) + with Not_found -> nosuchgoal (** {7 Dispatching on goals} *) diff --git a/engine/proofview.mli b/engine/proofview.mli index c772525c86..9455dae643 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -244,15 +244,12 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** [tclFOCUS i j t] applies [t] after focusing on the goals number [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). this - exception is caught at toplevel with a default message + a hook - message that can be customized by [set_nosuchgoals_hook] below. - This hook is used to add a suggestion about bullets when - applicable. *) + existing goals, fails with the [nosuchgoal] argument, by default + raising [NoSuchGoals] (a user error). This exception is caught at + toplevel with a default message. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.t) -> unit -val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSLIST li t] applies [t] on the list of focused goals described by [li]. Each element of [li] is a pair [(i, j)] denoting @@ -261,13 +258,14 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic intervals. If the set of such goals is not a single range, then it will move goals such that it is a single range. (So, for instance, [[1, 3-5]; idtac.] is not the identity.) - If the set of such goals is empty, it will fail. *) -val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + If the set of such goals is empty, it will fail with [nosuchgoal], + by default raising [NoSuchGoals 0]. *) +val tclFOCUSLIST : ?nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its - number.*) -val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + number. Fails with [nosuchgoal], by default raising [NoSuchGoals 1]. *) +val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic (** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the specified range doesn't correspond to existing goals, behaves like diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 488c9a740f..e5bf52571c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -67,7 +67,10 @@ let print_no_symbol = ref false (**********************************************************************) (* Turning notations and scopes on and off for printing *) -module IRuleSet = InterpRuleSet +module IRuleSet = Set.Make(struct + type t = interp_rule + let compare x y = Pervasives.compare x y + end) let inactive_notations_table = Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty) @@ -107,13 +110,13 @@ let deactivate_notation nr = (* shouldn't we check wether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> - if not (exists_notation_interpretation_in_scope scopt ntn) then - user_err ~hdr:"Notation" + match availability_of_notation (scopt, ntn) (scopt, []) with + | None -> user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" ++ (match scopt with | None -> spc () ++ str "in the empty scope." | Some _ -> show_scope scopt ++ str ".")) - else + | Some _ -> if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () @@ -260,11 +263,6 @@ let rec insert_pat_coercion ?loc l c = match l with | [] -> c | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) -let add_lonely keyrule seen = - match keyrule with - | NotationRule (None,ntn) -> ntn::seen - | SynDefRule _ | NotationRule (Some _,_) -> seen - (**********************************************************************) (* conversion of references *) @@ -388,8 +386,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_pattern allscopes [] vars pat - (uninterp_cases_pattern_notations scopes pat) + extern_notation_pattern allscopes vars pat + (uninterp_cases_pattern_notations pat) with No_match -> let loc = pat.CAst.loc in match DAst.get pat with @@ -442,15 +440,18 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = insert_pat_coercion coercion pat and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) - (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars = + (custom, (tmp_scope, scopes) as allscopes) vars = function - | NotationRule (sc,ntn),key,need_delim -> + | NotationRule (sc,ntn) -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - let key = if need_delim || List.mem ntn lonely_seen then key else None in - let scopt = match key with Some _ -> sc | _ -> None in + match availability_of_notation (sc,ntn) (tmp_scope,scopes) with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -472,8 +473,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (insert_pat_delimiters ?loc (make_pat_notation ?loc ntn (l,ll) l2') key) end - | SynDefRule kn,key,need_delim -> - assert (key = None && need_delim = false); + | SynDefRule kn -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> @@ -491,9 +491,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) -and extern_notation_pattern allscopes lonely_seen vars t = function +and extern_notation_pattern allscopes vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in @@ -501,27 +501,22 @@ and extern_notation_pattern allscopes lonely_seen vars t = function | PatCstr (cstr,args,na) -> let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) - (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars - (keyrule,key,need_delim) in + (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation_pattern allscopes lonely_seen vars t rules + No_match -> extern_notation_pattern allscopes vars t rules -let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function +let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; apply_notation_to_pattern (IndRef ind) - (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim) + (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation_ind_pattern allscopes lonely_seen vars ind args rules + No_match -> extern_notation_ind_pattern allscopes vars ind args rules let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and @@ -533,8 +528,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes [] vars ind args - (uninterp_ind_pattern_notations scopes ind) + extern_notation_ind_pattern allscopes vars ind args + (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in @@ -778,32 +773,32 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx (custom,scopes as allscopes) vars r = +let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token allscopes) r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal - (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r)) + (fun r -> extern_notation scopes vars r (uninterp_notations r)) r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with - | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us) + | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) | c -> - match availability_of_entry_coercion custom InConstrEntrySomeLevel with + match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - let scopes = (InConstrEntrySomeLevel, scopes) in + let scopes = (InConstrEntrySomeLevel, snd scopes) in let c = match c with (* The remaining cases are only for the constr entry *) @@ -815,7 +810,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> - extern_evar n (List.map (on_snd (extern false allscopes vars)) l) + extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else @@ -1078,9 +1073,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function +and extern_notation (custom,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try if is_inactive_rule keyrule then raise No_match; @@ -1128,8 +1123,11 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - let key = if need_delim || List.mem ntn lonely_seen then key else None in - let scopt = match key with Some _ -> sc | None -> None in + match availability_of_notation (sc,ntn) scopes with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> let scopes' = Option.List.cons scopt (snd scopes) in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -1165,9 +1163,7 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function let args = extern_args (extern true) vars args in CAst.make ?loc @@ explicitize false argsimpls (None,e) args with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation allscopes lonely_seen vars t rules + No_match -> extern_notation allscopes vars t rules let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c diff --git a/interp/notation.ml b/interp/notation.ml index 56504db04e..a7bac96d31 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -21,7 +21,6 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration -open Classops (*i*) @@ -50,25 +49,15 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false -let notation_entry_level_compare s1 s2 = match (s1,s2) with -| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0 -| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> - pair_compare String.compare Int.compare (s1,n1) (s2,n2) -| InConstrEntrySomeLevel, _ -> -1 -| InCustomEntryLevel _, _ -> 1 - let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s -let notation_compare = - pair_compare notation_entry_level_compare String.compare - module NotationOrd = struct type t = notation - let compare = notation_compare + let compare = Pervasives.compare end module NotationSet = Set.Make(NotationOrd) @@ -167,8 +156,6 @@ let scope_eq s1 s2 = match s1, s2 with | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false -(* Scopes for interpretation *) - let scope_stack = ref [] let current_scopes () = !scope_stack @@ -178,102 +165,14 @@ let scope_is_open_in_scopes sc l = let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) -(* Uninterpretation tables *) - -type interp_rule = - | NotationRule of scope_name option * notation - | SynDefRule of KerName.t - -type scoped_notation_rule_core = scope_name * notation * interpretation * int option -type notation_rule_core = interp_rule * interpretation * int option -type notation_rule = notation_rule_core * delimiters option * bool - -let interp_rule_compare r1 r2 = match r1, r2 with - | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) -> - pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2) - | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2 - | (NotationRule _ | SynDefRule _), _ -> -1 - -module InterpRuleSet = Set.Make(struct - type t = interp_rule - let compare = interp_rule_compare - end) - -(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) - -type uninterp_scope_elem = - | UninterpScope of scope_name - | UninterpSingle of notation_rule_core - -let uninterp_scope_eq_weak s1 s2 = match s1, s2 with -| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2 -| UninterpSingle s1, UninterpSingle s2 -> false -| (UninterpSingle _ | UninterpScope _), _ -> false - -module ScopeOrd = - struct - type t = scope_name option - let compare = Pervasives.compare - end - -module ScopeMap = CMap.Make(ScopeOrd) - -let uninterp_scope_stack = ref [] - -let push_uninterp_scope sc scopes = UninterpScope sc :: scopes - -let push_uninterp_scopes = List.fold_right push_uninterp_scope - -(**********************************************************************) -(* Mapping classes to scopes *) - -type scope_class = cl_typ - -let scope_class_compare : scope_class -> scope_class -> int = - cl_typ_ord - -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in - cl - -module ScopeClassOrd = -struct - type t = scope_class - let compare = scope_class_compare -end - -module ScopeClassMap = Map.Make(ScopeClassOrd) - -let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.empty - -let scope_class_map = ref initial_scope_class_map - -let declare_scope_class sc cl = - scope_class_map := ScopeClassMap.add cl sc !scope_class_map - -let find_scope_class cl = - ScopeClassMap.find cl !scope_class_map - -let find_scope_class_opt = function - | None -> None - | Some cl -> try Some (find_scope_class cl) with Not_found -> None - -let current_type_scope_name () = - find_scope_class_opt (Some CL_SORT) - (* TODO: push nat_scope, z_scope, ... in scopes summary *) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = - if Int.equal i 1 then begin + if Int.equal i 1 then scope_stack := - if op then Scope sc :: !scope_stack - else List.except scope_eq (Scope sc) !scope_stack; - uninterp_scope_stack := - if op then UninterpScope sc :: !uninterp_scope_stack - else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack - end + if op then sc :: !scope_stack + else List.except scope_eq sc !scope_stack let cache_scope o = open_scope 1 o @@ -288,7 +187,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_name -> obj = +let inScope : bool * bool * scope_elem -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -297,7 +196,7 @@ let inScope : bool * bool * scope_name -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc)) + Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) let empty_scope_stack = [] @@ -305,20 +204,9 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope -let make_type_scope_soft tmp_scope = - if Option.equal String.equal tmp_scope (current_type_scope_name ()) then - true, None - else - false, tmp_scope - let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) -let make_current_uninterp_scopes (tmp_scope,scopes) = - let istyp,tmp_scope = make_type_scope_soft tmp_scope in - istyp,Option.fold_right push_uninterp_scope tmp_scope - (push_uninterp_scopes scopes !uninterp_scope_stack) - (**********************************************************************) (* Delimiters *) @@ -362,80 +250,40 @@ let find_delimiters_scope ?loc key = user_err ?loc ~hdr:"find_delimiters" (str "Unknown scope delimiting key " ++ str key ++ str ".") +(* Uninterpretation tables *) + +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of KerName.t + (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = | RefKey of GlobRef.t - | LambdaKey - | ProdKey | Oth let key_compare k1 k2 = match k1, k2 with | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 -| RefKey _, _ -> -1 -| _, RefKey _ -> 1 -| k1, k2 -> Pervasives.compare k1 k2 +| RefKey _, Oth -> -1 +| Oth, RefKey _ -> 1 +| Oth, Oth -> 0 module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -let keymap_add key sc interp (scope_map,global_map) = - (* Adding to scope keymap for printing based on open scopes *) - let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in - let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in - let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in - let scope_map = ScopeMap.add sc newscmap scope_map in - (* Adding to global keymap of scoped notations in case the scope is not open *) - let global_map = match interp with - | NotationRule (Some sc,ntn), interp, c -> - let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in - KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map - | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in - (scope_map, global_map) - -let keymap_extract istype keys sc map = - let keymap = - try ScopeMap.find (Some sc) map - with Not_found -> KeyMap.empty in - let delim = - if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then - (* A type is re-interpreted with type_scope on top, so never need a delimiter *) - None - else - (* Pass the delimiter so that it can be used if ever the notation is masked *) - (String.Map.find sc !scope_map).delimiters in - let add_scope rule = (rule,delim,false) in - List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys - -let find_with_delimiters istype = function - | None -> - None - | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) -> - (* This is in case type_scope (which by default is open in the - initial state) has been explicitly closed *) - Some None - | Some scope -> - match (String.Map.find scope !scope_map).delimiters with - | Some key -> Some (Some key) - | None -> None +type notation_rule = interp_rule * interpretation * int option -let rec keymap_extract_remainder istype scope_seen = function - | [] -> [] - | (sc,ntn,interp,c) :: l -> - if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l - else - match find_with_delimiters istype (Some sc) with - | None -> keymap_extract_remainder istype scope_seen l - | Some delim -> - let rule = (NotationRule (Some sc, ntn), interp, c) in - (rule,delim,true) :: keymap_extract_remainder istype scope_seen l +let keymap_add key interp map = + let old = try KeyMap.find key map with Not_found -> [] in + KeyMap.add key (interp :: old) map + +let keymap_find key map = + try KeyMap.find key map + with Not_found -> [] (* Scopes table : interpretation -> scope_name *) -let notations_key_table = - ref ((ScopeMap.empty, KeyMap.empty) : - notation_rule_core list KeyMap.t ScopeMap.t * - scoped_notation_rule_core list KeyMap.t) +let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -447,14 +295,12 @@ let glob_prim_constr_key c = match DAst.get c with | _ -> None let glob_constr_keys c = match DAst.get c with - | GRef (ref,_) -> [RefKey (canonical_gr ref)] | GApp (c, _) -> begin match DAst.get c with | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] | _ -> [Oth] end - | GLambda _ -> [LambdaKey] - | GProd _ -> [ProdKey] + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] let cases_pattern_key c = match DAst.get c with @@ -468,8 +314,6 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) - | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None - | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None | _ -> Oth, None (**********************************************************************) @@ -1211,31 +1055,37 @@ let check_required_module ?loc sc (sp,d) = (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) -let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function - | UninterpScope scope :: scopes -> +let find_with_delimiters = function + | None -> None + | Some scope -> + match (String.Map.find scope !scope_map).delimiters with + | Some key -> Some (Some scope, Some key) + | None -> None + +let rec find_without_delimiters find (ntn_scope,ntn) = function + | Scope scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with | Some scope' when String.equal scope scope' -> - Some None + Some (None,None) | _ -> (* If the most recently open scope has a notation/numeral printer but not the expected one then we need delimiters *) if find scope then - find_with_delimiters istype ntn_scope + find_with_delimiters ntn_scope else - find_without_delimiters find ntndata scopes + find_without_delimiters find (ntn_scope,ntn) scopes end - | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes -> + | SingleNotation ntn' :: scopes -> begin match ntn_scope, ntn with | None, Some ntn when notation_eq ntn ntn' -> - Some None + Some (None, None) | _ -> - find_without_delimiters find ntndata scopes + find_without_delimiters find (ntn_scope,ntn) scopes end - | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata scopes | [] -> (* Can we switch to [scope]? Yes if it has defined delimiters *) - find_with_delimiters istype ntn_scope + find_with_delimiters ntn_scope (* The mapping between notations and their interpretation *) @@ -1268,19 +1118,9 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = | Some _ -> () end -let scope_of_rule = function - | NotationRule (None,_) | SynDefRule _ -> None - | NotationRule (Some sc as sco,_) -> sco - -let uninterp_scope_to_add pat n = function - | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n)) - | NotationRule (Some sc,_) -> None - let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in - let sc = scope_of_rule rule in - notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table; - uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack + notations_key_table := keymap_add key (rule,pat,n) !notations_key_table let rec find_interpretation ntn find = function | [] -> raise Not_found @@ -1359,29 +1199,20 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") -let extract_notations (istype,scopes) keys = - if keys == [] then [] (* shortcut *) else - let scope_map, global_map = !notations_key_table in - let rec aux scopes seen = - match scopes with - | UninterpScope sc :: scopes -> keymap_extract istype keys sc scope_map @ aux scopes (String.Set.add sc seen) - | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen - | [] -> - let find key = try KeyMap.find key global_map with Not_found -> [] in - keymap_extract_remainder istype seen (List.flatten (List.map find keys)) - in aux scopes String.Set.empty +let uninterp_notations c = + List.map_append (fun key -> keymap_find key !notations_key_table) + (glob_constr_keys c) -let uninterp_notations scopes c = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes (glob_constr_keys c) +let uninterp_cases_pattern_notations c = + keymap_find (cases_pattern_key c) !notations_key_table -let uninterp_cases_pattern_notations scopes c = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes [cases_pattern_key c] +let uninterp_ind_pattern_notations ind = + keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table -let uninterp_ind_pattern_notations scopes ind = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes [RefKey (canonical_gr (IndRef ind))] +let availability_of_notation (ntn_scope,ntn) scopes = + let f scope = + NotationMap.mem ntn (String.Map.find scope !scope_map).notations in + find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1538,11 +1369,13 @@ let availability_of_prim_token n printer_scope local_scopes = | _ -> false with Not_found -> false in - let istype,scopes = make_current_uninterp_scopes local_scopes in - find_without_delimiters f (istype,Some printer_scope,None) scopes + let scopes = make_current_scopes local_scopes in + Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) (* Miscellaneous *) +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 @@ -1556,10 +1389,9 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) = +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = notation_entry_level_eq entry1 entry2 && - Option.equal String.equal tmpsc1 tmpsc2 && - List.equal String.equal scl1 scl2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = @@ -1574,17 +1406,46 @@ let exists_notation_in_scope scopt ntn onlyprint r = interpretation_eq n.not_interp r with Not_found -> false -let exists_notation_interpretation_in_scope scopt ntn = - let scope = match scopt with Some s -> s | None -> default_scope in - try - let sc = String.Map.find scope !scope_map in - let _ = NotationMap.find ntn sc.notations in - true - with Not_found -> false - let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) +(* Mapping classes to scopes *) + +open Classops + +type scope_class = cl_typ + +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord + +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in + cl + +module ScopeClassOrd = +struct + type t = scope_class + let compare = scope_class_compare +end + +module ScopeClassMap = Map.Make(ScopeClassOrd) + +let initial_scope_class_map : scope_name ScopeClassMap.t = + ScopeClassMap.empty + +let scope_class_map = ref initial_scope_class_map + +let declare_scope_class sc cl = + scope_class_map := ScopeClassMap.add cl sc !scope_class_map + +let find_scope_class cl = + ScopeClassMap.find cl !scope_class_map + +let find_scope_class_opt = function + | None -> None + | Some cl -> try Some (find_scope_class cl) with Not_found -> None + +(**********************************************************************) (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes sigma t = @@ -1604,6 +1465,9 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) let compute_type_scope sigma t = find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + let scope_class_of_class (x : cl_typ) : scope_class = x @@ -1960,7 +1824,7 @@ let locate_notation prglob ntn scope = str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in - prlist_with_sep fnl + prlist (fun (sc,r,(_,df)) -> hov 0 ( pr_notation_info prglob df r ++ @@ -2023,18 +1887,17 @@ let pr_visibility prglob = function (* Synchronisation with reset *) let freeze ~marshallable = - (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, + (!scope_map, !scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; - uninterp_scope_stack := uscs; - arguments_scope := asc; delimiters_map := dlm; + arguments_scope := asc; notations_key_table := fkm; scope_class_map := clsc; prim_token_interp_infos := ptii; @@ -2045,9 +1908,8 @@ let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = let init () = init_scope_map (); - uninterp_scope_stack := []; delimiters_map := String.Map.empty; - notations_key_table := (ScopeMap.empty,KeyMap.empty); + notations_key_table := KeyMap.empty; scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; prim_token_uninterp_infos := GlobRef.Map.empty diff --git a/interp/notation.mli b/interp/notation.mli index 57e2be16b9..a67948a778 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -216,8 +216,6 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t -module InterpRuleSet : Set.S with type elt = interp_rule - val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit @@ -227,28 +225,18 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule_core = - interp_rule (* kind of notation *) - * interpretation (* pattern associated to the notation *) - * int option (* number of expected arguments *) - -type notation_rule = - notation_rule_core - * delimiters option (* delimiter to possibly add *) - * bool (* true if the delimiter is mandatory *) +type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : inductive -> notation_rule list -(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option - *) (** {6 Miscellaneous} *) @@ -259,9 +247,6 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool -(** Checks for already existing notations *) -val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/lib/util.ml b/lib/util.ml index 0389336258..38d73d3453 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -20,12 +20,6 @@ let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) let on_pi3 f (a,b,c) = (a,b,f c) -(* Comparing pairs *) - -let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) = - if p1 == p2 then 0 else - let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c - (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index fa3b622621..1eb60f509a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,10 +17,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Comparing pairs *) - -val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int) - (** Mapping under triple *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 523c7c8305..ec5e46d89b 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -184,7 +184,7 @@ END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } +| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast } END { diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d40ba6562..99a9c1ab9a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> + convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = end | None, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_concl_no_check newt DEFAULTcast + convert_concl ~check:false newt DEFAULTcast in Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4802608fda..f3bc791b8d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -535,7 +535,7 @@ let focused_simpl path = let open Tacmach.New in Proofview.Goal.enter begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let focused_simpl path = focused_simpl path @@ -687,7 +687,7 @@ let simpl_coeffs path_init path_k = let n = Pervasives.(-) (List.length path_k) (List.length path_init) in let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let rec shuffle p (t1,t2) = @@ -1849,12 +1849,12 @@ let destructure_hyps = match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) | _ -> loop lit diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a05b1e3d81..a4caeb403c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -426,7 +426,7 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_string_soft (Bytes.to_string (loop (n - 1))) -let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = @@ -1409,8 +1409,6 @@ let tclINTRO_ANON ?seed () = | Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> - let convert_concl_no_check t = - Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index bbe7bde78b..17e4114958 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl = | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic - (Tactics.convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in + (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in let utacs = List.map utac (pf_hyps gl) in let ugtac gl' = Proofview.V82.of_tactic diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index ef4a74b273..4f36354f79 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -73,6 +73,7 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in + let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in let tac = let open Goal_select in match gi with | SelectAlreadyFocused -> let open Proofview.Notations in @@ -86,9 +87,9 @@ let solve ?with_end_tac gi info_lvl tac pr = in Proofview.tclZERO e - | SelectNth i -> Proofview.tclFOCUS i i tac - | SelectList l -> Proofview.tclFOCUSLIST l tac - | SelectId id -> Proofview.tclFOCUSID id tac + | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac + | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac + | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac | SelectAll -> tac in let tac = diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 2ca4f0afb4..640feb2f5b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -197,3 +197,15 @@ let put p b = let suggest p = (!current_behavior).suggest p + +(* Better printing for bullet exceptions *) +exception SuggestNoSuchGoals of int * Proof.t + +let _ = CErrors.register_handler begin function + | SuggestNoSuchGoals(n,proof) -> + let suffix = suggest proof in + CErrors.user_err + Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) + | _ -> raise CErrors.Unhandled + end diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 0fcc647a6f..6fdf818497 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -44,3 +44,5 @@ val register_behavior : behavior -> unit *) val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t + +exception SuggestNoSuchGoals of int * Proof.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 86d3d9601e..08b98d702a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,18 +348,3 @@ let update_global_env (pf : t) = let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in (p, ()))) pf in res - -(* XXX: This hook is used to provide a better error w.r.t. bullets, - however the proof engine [surprise!] knows nothing about bullets so - here we have a layering violation. The right fix is to modify the - entry point to handle this and reraise the exception with the - needed information. *) -(* let _ = - * let hook n = - * try - * let prf = give_me_the_proof pf in - * (Proof_bullet.suggest prf) - * with NoCurrentProof -> mt () - * in - * Proofview.set_nosuchgoals_hook hook *) - diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 3019fc0231..70854e6e3c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -515,6 +515,6 @@ let autounfold_one db cl = if did then match cl with | Some hyp -> change_in_hyp None (make_change_arg c') hyp - | None -> convert_concl_no_check c' DEFAULTcast + | None -> convert_concl ~check:false c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 066b9c7794..b70dd63211 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -614,18 +614,22 @@ let cofix id = mutual_cofix id [] 0 type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -let pf_reduce_decl redfun where decl gl = +let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = let open Context.Named.Declaration in - let redfun' c = Tacmach.New.pf_apply redfun gl c in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then user_err (Id.print id.binder_name ++ str " has no value."); - LocalAssum (id,redfun' ty) + let (sigma, ty') = redfun false env sigma ty in + (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> - let b' = if where != InHypTypeOnly then redfun' b else b in - let ty' = if where != InHypValueOnly then redfun' ty else ty in - LocalDef (id,b',ty') + let (sigma, b') = + if where != InHypTypeOnly then redfun true env sigma b else (sigma, b) + in + let (sigma, ty') = + if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty) + in + (sigma, LocalDef (id,b',ty')) (* Possibly equip a reduction with the occurrences mentioned in an occurrence clause *) @@ -695,41 +699,9 @@ let bind_red_expr_occurrences occs nbcl redexp = reduction function either to the conclusion or to a certain hypothesis *) -let reduct_in_concl (redfun,sty) = - Proofview.Goal.enter begin fun gl -> - convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty - end - -let reduct_in_hyp ?(check=false) redfun (id,where) = - Proofview.Goal.enter begin fun gl -> - convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl) - end - -let revert_cast (redfun,kind as r) = - if kind == DEFAULTcast then (redfun,REVERTcast) else r - -let reduct_option ?(check=false) redfun = function - | Some id -> reduct_in_hyp ~check (fst redfun) id - | None -> reduct_in_concl (revert_cast redfun) - (** Tactic reduction modulo evars (for universes essentially) *) -let pf_e_reduce_decl redfun where decl gl = - let open Context.Named.Declaration in - let sigma = Proofview.Goal.sigma gl in - let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in - match decl with - | LocalAssum (id,ty) -> - if where == InHypValueOnly then - user_err (Id.print id.binder_name ++ str " has no value."); - let (sigma, ty') = redfun sigma ty in - (sigma, LocalAssum (id, ty')) - | LocalDef (id,b,ty) -> - let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in - let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in - (sigma, LocalDef (id, b', ty')) - -let e_reduct_in_concl ~check (redfun, sty) = +let e_change_in_concl ?(check = false) (redfun, sty) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in @@ -737,53 +709,64 @@ let e_reduct_in_concl ~check (redfun, sty) = (convert_concl ~check c' sty) end -let e_reduct_in_hyp ?(check=false) redfun (id, where) = +let e_change_in_hyp ?(check = false) redfun (id,where) = Proofview.Goal.enter begin fun gl -> - let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in + let sigma = Proofview.Goal.sigma gl in + let hyp = Tacmach.New.pf_get_hyp id gl in + let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (convert_hyp ~check decl') + (convert_hyp ~check c) end -let e_reduct_option ?(check=false) redfun = function - | Some id -> e_reduct_in_hyp ~check (fst redfun) id - | None -> e_reduct_in_concl ~check (revert_cast redfun) - -(** Versions with evars to maintain the unification of universes resulting - from conversions. *) - -let e_change_in_concl (redfun,sty) = +let e_change_in_hyps ?(check=true) f args = Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (convert_concl_no_check c sty) + let fold (env, sigma) arg = + let (redfun, id, where) = f arg in + let hyp = + try lookup_named id env + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + in + let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in + let sign = Logic.convert_hyp check (named_context_val env) sigma d in + let env = reset_with_named_context sign env in + (env, sigma) + in + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let (env, sigma) = List.fold_left fold (env, sigma) args in + let ty = Proofview.Goal.concl gl in + Proofview.Unsafe.tclEVARS sigma + <*> + Refine.refine ~typecheck:false begin fun sigma -> + Evarutil.new_evar env sigma ~principal:true ty + end end -let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = - let open Context.Named.Declaration in - match decl with - | LocalAssum (id,ty) -> - if where == InHypValueOnly then - user_err (Id.print id.binder_name ++ str " has no value."); - let (sigma, ty') = redfun false env sigma ty in - (sigma, LocalAssum (id, ty')) - | LocalDef (id,b,ty) -> - let (sigma, b') = - if where != InHypTypeOnly then redfun true env sigma b else (sigma, b) - in - let (sigma, ty') = - if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty) - in - (sigma, LocalDef (id,b',ty')) +let e_reduct_in_concl = e_change_in_concl -let e_change_in_hyp redfun (id,where) = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let hyp = Tacmach.New.pf_get_hyp id gl in - let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (convert_hyp c) - end +let reduct_in_concl ?(check = false) (redfun, sty) = + let redfun env sigma c = (sigma, redfun env sigma c) in + e_change_in_concl ~check (redfun, sty) + +let e_reduct_in_hyp ?(check=false) redfun (id, where) = + let redfun _ env sigma c = redfun env sigma c in + e_change_in_hyp ~check redfun (id, where) + +let reduct_in_hyp ?(check = false) redfun (id, where) = + let redfun _ env sigma c = (sigma, redfun env sigma c) in + e_change_in_hyp ~check redfun (id, where) + +let revert_cast (redfun,kind as r) = + if kind == DEFAULTcast then (redfun,REVERTcast) else r + +let e_reduct_option ?(check=false) redfun = function + | Some id -> e_reduct_in_hyp ~check (fst redfun) id + | None -> e_change_in_concl ~check (revert_cast redfun) + +let reduct_option ?(check = false) (redfun, sty) where = + let redfun env sigma c = (sigma, redfun env sigma c) in + e_reduct_option ~check (redfun, sty) where type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr @@ -837,24 +820,35 @@ let change_on_subterm cv_pb deep t where env sigma c = (sigma, c) let change_in_concl occl t = - e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast) + e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast) let change_in_hyp occl t id = - e_change_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id - -let change_option occl t = function - | Some id -> change_in_hyp occl t id - | None -> change_in_concl occl t + (* FIXME: we set the [check] flag only to reorder hypotheses in case of + introduction of dependencies in new variables. We should separate this + check from the conversion function. *) + e_change_in_hyp ~check:true (fun x -> change_on_subterm Reduction.CONV x t occl) id + +let concrete_clause_of enum_hyps cl = match cl.onhyps with +| None -> + let f id = (id, AllOccurrences, InHyp) in + List.map f (enum_hyps ()) +| Some l -> + List.map (fun ((occs, id), w) -> (id, occs, w)) l let change chg c cls = Proofview.Goal.enter begin fun gl -> - let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in - Tacticals.New.tclMAP (function - | OnHyp (id,occs,where) -> - change_option (bind_change_occurrences occs chg) c (Some (id,where)) - | OnConcl occs -> - change_option (bind_change_occurrences occs chg) c None) - cls + let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + begin match cls.concl_occs with + | NoOccurrences -> Proofview.tclUNIT () + | occs -> change_in_concl (bind_change_occurrences occs chg) c + end + <*> + let f (id, occs, where) = + let occl = bind_change_occurrences occs chg in + let redfun deep env sigma t = change_on_subterm Reduction.CONV deep c occl env sigma t in + (redfun, id, where) + in + e_change_in_hyps ~check:true f hyps end let change_concl t = @@ -881,14 +875,6 @@ let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast) (* The main reduction function *) -let reduction_clause redexp cl = - let nbcl = List.length cl in - List.map (function - | OnHyp (id,occs,where) -> - (Some (id,where), bind_red_expr_occurrences occs nbcl redexp) - | OnConcl occs -> - (None, bind_red_expr_occurrences occs nbcl redexp)) cl - let reduce redexp cl = let trace env sigma = let open Printer in @@ -897,12 +883,24 @@ let reduce redexp cl = in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> - let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in - let redexps = reduction_clause redexp cl' in + let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in + let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - Tacticals.New.tclMAP (fun (where,redexp) -> - e_reduct_option ~check - (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps + begin match cl.concl_occs with + | NoOccurrences -> Proofview.tclUNIT () + | occs -> + let redexp = bind_red_expr_occurrences occs nbcl redexp in + let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + e_change_in_concl ~check (revert_cast redfun) + end + <*> + let f (id, occs, where) = + let redexp = bind_red_expr_occurrences occs nbcl redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let redfun _ env sigma c = redfun env sigma c in + (redfun, id, where) + in + e_change_in_hyps ~check f hyps end end @@ -2174,7 +2172,7 @@ let constructor_tac with_evars expctdnumopt i lbind = let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; Tacticals.New.tclTHENLIST [ - convert_concl_no_check redcl DEFAULTcast; + convert_concl ~check:false redcl DEFAULTcast; intros; constructor_core with_evars (ind, i) lbind ] @@ -2203,7 +2201,7 @@ let any_constructor with_evars tacopt = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; Tacticals.New.tclTHENLIST [ - convert_concl_no_check redcl DEFAULTcast; + convert_concl ~check:false redcl DEFAULTcast; intros; any_constr ind nconstr 1 () ] @@ -2647,9 +2645,9 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = in Tacticals.New.tclTHENLIST [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check newcl DEFAULTcast; + convert_concl ~check:false newcl DEFAULTcast; intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false; - Tacticals.New.tclMAP convert_hyp_no_check depdecls; + Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls; eq_tac ] end @@ -4799,7 +4797,7 @@ let symmetry_red allowred = match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN - (convert_concl_no_check concl DEFAULTcast) + (convert_concl ~check:false concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind end @@ -4894,7 +4892,7 @@ let transitivity_red allowred t = match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN - (convert_concl_no_check concl DEFAULTcast) + (convert_concl ~check:false concl DEFAULTcast) (match t with | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 75b5caaa36..e7b95a820e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -36,7 +36,9 @@ val introduction : Id.t -> unit Proofview.tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic +[@@ocaml.deprecated "use [Tactics.convert_concl]"] val convert_hyp_no_check : named_declaration -> unit Proofview.tactic +[@@ocaml.deprecated "use [Tactics.convert_hyp]"] val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t -> int -> unit Proofview.tactic @@ -152,8 +154,8 @@ type change_arg = patvar_map -> env -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic -val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic -val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic +val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic +val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 2ba02924c9..af202ea01c 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)". + "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index bec4fc1579..94b86fc222 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ (I 6)%bool +(false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ffc3b14e2..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. +Notation "! A" := (forall _:nat, A) (at level 60). Check ! (0=0). Check forall n, n=0. @@ -195,9 +195,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). -Check (false && I 3)%bool /\ (I 6)%bool. +Check (false && I 3)%bool /\ I 6. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 923caedace..bcb2468792 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). -Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 015dac2512..d32cf67e28 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,27 +128,25 @@ return (1, 2, 3, 4) : nat *(1.2) : nat -! '{{x, y}}, x + y = 0 +! '{{x, y}}, x.y = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0 : Prop -exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 +exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0 : Prop exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), (forall x : A, R x x) : Prop exists_true (x : nat) (A : Type) (R : A -> A -> Prop) -(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z +(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z : Prop {{{{True, nat -> True}}, nat -> True}} : Prop * Prop * Prop @@ -184,22 +182,22 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop myexists2 x : nat * nat, let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y : Prop -fun '({{x, y}} as z) => x + y = 0 /\ z = z +fun '({{x, y}} as z) => x.y = 0 /\ z = z : nat * nat -> Prop -myexists ({{x, y}} as z), x + y = 0 /\ z = z +myexists ({{x, y}} as z), x.y = 0 /\ z = z : Prop -exists '({{x, y}} as z), x + y = 0 /\ z = z +exists '({{x, y}} as z), x.y = 0 /\ z = z : Prop -∀ '({{x, y}} as z), x + y = 0 /\ z = z +∀ '({{x, y}} as z), x.y = 0 /\ z = z : Prop -fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y : nat * nat * bool -> nat myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y : Prop @@ -211,17 +209,17 @@ fun p : nat => if p is S n then n else 0 : nat -> nat fun p : comparison => if p is Lt then 1 else 0 : comparison -> nat -fun S : nat => [S | S + S] +fun S : nat => [S | S.S] : nat -> nat * (nat -> nat) -fun N : nat => [N | N + 0] +fun N : nat => [N | N.0] : nat -> nat * (nat -> nat) -fun S : nat => [[S | S + S]] +fun S : nat => [[S | S.S]] : nat -> nat * (nat -> nat) {I : nat | I = I} : Set {'I : True | I = I} : Prop -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop @@ -254,13 +252,3 @@ myfoo01 tt : nat myfoo01 tt : nat -[{0; 0}] - : list (list nat) -[{1; 2; 3}; - {4; 5; 6}; - {7; 8; 9}] - : list (list nat) -amatch = mmatch 0 (with 0 => 1| 1 => 2 end) - : unit -alist = [0; 1; 2] - : list nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 2caffad1d9..dcc8bd7165 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,13 +183,9 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) -Section S1. -Variable plus : nat -> nat -> nat. -Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. -End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -197,12 +193,10 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Section S2. -Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). Check (((id 1) + 2) + 3). Check (id (1 + 2)). -End S2. (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) @@ -416,58 +410,3 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. - -(* Test printing of notations guided by scope *) - -Module A. - -Declare Scope line_scope. -Delimit Scope line_scope with line. -Declare Scope matx_scope. -Notation "{ }" := nil (format "{ }") : line_scope. -Notation "{ x }" := (cons x nil) : line_scope. -Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. -Notation "[ ]" := nil (format "[ ]") : matx_scope. -Notation "[ l ]" := (cons l%line nil) : matx_scope. -Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) - (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. - -Open Scope matx_scope. -Check [[0;0]]. -Check [[1;2;3];[4;5;6];[7;8;9]]. - -End A. - -(* Example by Beta Ziliani *) - -Require Import Lists.List. - -Module B. - -Import ListNotations. - -Declare Scope pattern_scope. -Delimit Scope pattern_scope with pattern. - -Declare Scope patterns_scope. -Delimit Scope patterns_scope with patterns. - -Notation "a => b" := (a, b) (at level 201) : pattern_scope. -Notation "'with' p1 | .. | pn 'end'" := - ((cons p1%pattern (.. (cons pn%pattern nil) ..))) - (at level 91, p1 at level 210, pn at level 210) : patterns_scope. - -Definition mymatch (n:nat) (l : list (nat * nat)) := tt. -Arguments mymatch _ _%patterns. -Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). - -Close Scope patterns_scope. -Close Scope pattern_scope. - -Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. -Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) - -Definition alist := [0;1;2]. -Print alist. - -End B. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 5bf4ec7bfb..9d972a68f7 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -21,36 +21,10 @@ Let "x" e1 e2 : expr Let "x" e1 e2 : expr -fun x : nat => (# x)%nat - : nat -> nat -fun x : nat => ## x - : nat -> nat -fun x : nat => # x - : nat -> nat -fun x : nat => ### x - : nat -> nat -fun x : nat => ## x - : nat -> nat -fun x : nat => (x.-1)%pred - : nat -> nat -∀ a : nat, a = 0 - : Prop -((∀ a : nat, a = 0) -> True)%type - : Prop -# - : Prop -# -> True - : Prop -((∀ a : nat, a = 0) -> True)%type - : Prop -## - : Prop myAnd1 True True : Prop r 2 3 : Prop -Notation Cn := Foo.FooCn -Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn let v := 0%test17 in v : myint63 : myint63 fun y : nat => # (x, z) |-> y & y diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b33ad17ed4..81c64418cb 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -5,8 +5,8 @@ Module A. Declare Custom Entry myconstr. Notation "[ x ]" := x (x custom myconstr at level 6). -Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope. -Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope. +Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). +Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. @@ -95,76 +95,6 @@ Check (Let "x" e1 e2). End D. -(* Check fix of #8551: a delimiter should be inserted because the - lonely notation hides the scope nat_scope, even though the latter - is open *) - -Module E. - -Notation "# x" := (S x) (at level 20) : nat_scope. -Notation "# x" := (Some x). -Check fun x => (# x)%nat. - -End E. - -(* Other tests of precedence *) - -Module F. - -Notation "# x" := (S x) (at level 20) : nat_scope. -Notation "## x" := (S x) (at level 20). -Check fun x => S x. -Open Scope nat_scope. -Check fun x => S x. -Notation "### x" := (S x) (at level 20) : nat_scope. -Check fun x => S x. -Close Scope nat_scope. -Check fun x => S x. - -End F. - -(* Lower priority of generic application rules *) - -Module G. - -Declare Scope predecessor_scope. -Delimit Scope predecessor_scope with pred. -Declare Scope app_scope. -Delimit Scope app_scope with app. -Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope. -Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope. -Check fun x => pred x. - -End G. - -(* Checking arbitration between in the presence of a notation in type scope *) - -Module H. - -Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity, - format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. -Check forall a, a = 0. - -Close Scope type_scope. -Check ((forall a, a = 0) -> True)%type. -Open Scope type_scope. - -Notation "#" := (forall a, a = 0). -Check #. -Check # -> True. - -Close Scope type_scope. -Check (# -> True)%type. -Open Scope type_scope. - -Declare Scope my_scope. -Notation "##" := (forall a, a = 0) : my_scope. -Open Scope my_scope. -Check ##. - -End H. - (* Fixing bugs reported by G. Gonthier in #9207 *) Module I. @@ -181,23 +111,6 @@ Check r 2 3. End I. -(* Fixing a bug reported by G. Gonthier in #9207 *) - -Module J. - -Module Import Mfoo. -Module Foo. -Definition FooCn := 2. -Module Bar. -Notation Cn := FooCn. -End Bar. -End Foo. -Export Foo.Bar. -End Mfoo. -About Cn. - -End J. - Require Import Coq.Numbers.Cyclic.Int63.Int63. Module NumeralNotations. Module Test17. diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out new file mode 100644 index 0000000000..ed4892b389 --- /dev/null +++ b/test-suite/output/bug_9180.out @@ -0,0 +1,4 @@ +Notation +"n .+1" := S n : nat_scope (default interpretation) +forall x : nat, x.+1 = x.+1 + : Prop diff --git a/test-suite/output/bug_9180.v b/test-suite/output/bug_9180.v new file mode 100644 index 0000000000..f221a94a50 --- /dev/null +++ b/test-suite/output/bug_9180.v @@ -0,0 +1,11 @@ +Notation succn := (Datatypes.S). + +Notation "n .+1" := (succn n) (at level 2, left associativity, + format "n .+1") : nat_scope. + +Locate ".+1". +(* Notation *) +(* "n .+1" := S n : nat_scope (default interpretation) *) +(** so Coq does not apply succn notation *) + +Check forall x : nat, x.+1 = x.+1. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8fae561be8..15172b30f8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -220,7 +220,6 @@ let init_toplevel ~help ~init custom_init arglist = let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; let opts, extras = custom_init ~opts extras in - Flags.if_verbose print_header (); Mltop.init_known_plugins (); Global.set_engagement opts.impredicative_set; @@ -296,6 +295,7 @@ let rec coqc_deprecated_check args acc extras = let coqtop_init ~opts extra = init_color opts; CoqworkmgrApi.(init !async_proofs_worker_priority); + Flags.if_verbose print_header (); opts, extra let coqtop_toplevel = |