diff options
38 files changed, 276 insertions, 335 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d52bd39d72..8d728b5b51 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -146,16 +146,16 @@ let print_local fmt ext = fprintf fmt "in@ " let print_position fmt pos = match pos with -| First -> fprintf fmt "Extend.First" -| Last -> fprintf fmt "Extend.Last" -| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s -| After s -> fprintf fmt "Extend.After@ \"%s\"" s -| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s +| First -> fprintf fmt "Gramlib.Gramext.First" +| Last -> fprintf fmt "Gramlib.Gramext.Last" +| Before s -> fprintf fmt "Gramlib.Gramext.Before@ \"%s\"" s +| After s -> fprintf fmt "Gramlib.Gramext.After@ \"%s\"" s +| Level s -> fprintf fmt "Gramlib.Gramext.Level@ \"%s\"" s let print_assoc fmt = function -| LeftA -> fprintf fmt "Extend.LeftA" -| RightA -> fprintf fmt "Extend.RightA" -| NonA -> fprintf fmt "Extend.NonA" +| LeftA -> fprintf fmt "Gramlib.Gramext.LeftA" +| RightA -> fprintf fmt "Gramlib.Gramext.RightA" +| NonA -> fprintf fmt "Gramlib.Gramext.NonA" let is_token s = match string_split s with | [s] -> is_uident s diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh new file mode 100644 index 0000000000..2df8affd14 --- /dev/null +++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then + + elpi_CI_REF=ltac+remove_aliases + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 65df89da6c..1c53f5981d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1380,147 +1380,147 @@ Numeral notations .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. :name: Numeral Notation - This command allows the user to customize the way numeral literals - are parsed and printed. + This command allows the user to customize the way numeral literals + are parsed and printed. - The token :n:`@ident__1` should be the name of an inductive type, - while :n:`@ident__2` and :n:`@ident__3` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@ident__2` should have one of the following types: + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: - * :n:`Decimal.int -> @ident__1` - * :n:`Decimal.int -> option @ident__1` - * :n:`Decimal.uint -> @ident__1` - * :n:`Decimal.uint -> option @ident__1` - * :n:`Z -> @ident__1` - * :n:`Z -> option @ident__1` + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` - And the printing function :n:`@ident__3` should have one of the - following types: + And the printing function :n:`@ident__3` should have one of the + following types: - * :n:`@ident__1 -> Decimal.int` - * :n:`@ident__1 -> option Decimal.int` - * :n:`@ident__1 -> Decimal.uint` - * :n:`@ident__1 -> option Decimal.uint` - * :n:`@ident__1 -> Z` - * :n:`@ident__1 -> option Z` + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` - When parsing, the application of the parsing function - :n:`@ident__2` to the number will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). - When a literal larger than :token:`num` is parsed, a warning - message about possible stack overflow, resulting from evaluating - :n:`@ident__2`, will be displayed. + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). - When a literal :g:`m` larger than :token:`num` is parsed, the - result will be :n:`(@ident__2 m)`, without reduction of this - application to a normal form. Here :g:`m` will be a - :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the - type of the parsing function :n:`@ident__2`. This allows for a - more compact representation of literals in types such as :g:`nat`, - and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`num` - is parsed. Note that :n:`(abstract after @num)` has no effect - when :n:`@ident__2` lands in an :g:`option` type. + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. - .. exn:: Cannot interpret this number as a value of type @type + .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support - the given numeral. This error is given when the interpretation - function returns :g:`None`, or if the interpretation is registered - for only non-negative integers, and the given numeral is negative. + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The parsing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The printing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @type is not an inductive type. + .. exn:: @type is not an inductive type. - Numeral notations can only be declared for inductive types with no - arguments. + Numeral notations can only be declared for inductive types with no + arguments. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a numeral notation. - Parsing functions must always return ground terms, made up of - applications of constructors and inductive types. Parsing - functions may not return terms containing axioms, bare - (co)fixpoints, lambdas, etc. + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a numeral notation. - Parsing functions expected to return an :g:`option` must always - return a concrete :g:`Some` or :g:`None` when applied to a - concrete numeral expressed as a decimal. They may not return - opaque constants. + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. - .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. - The inductive type used to register the numeral notation is no - longer available in the environment. Most likely, this is because - the numeral notation was declared inside a functor for an - inductive type inside the functor. This use case is not currently - supported. + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. - Alternatively, you might be trying to use a primitive token - notation from a plugin which forgot to specify which module you - must :g:`Require` for access to that notation. + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. - .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`Numeral Notation` must be a single - identifier. + The type passed to :cmd:`Numeral Notation` must be a single + identifier. - .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`Numeral Notation` must be single - identifiers. + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. - .. exn:: The reference @ident was not found in the current environment. + .. exn:: The reference @ident was not found in the current environment. - Identifiers passed to :cmd:`Numeral Notation` must exist in the - global environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. - .. exn:: @ident is bound to a notation that does not denote a reference. + .. exn:: @ident is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`Numeral Notation` must be global - references, or notations which denote to single identifiers. + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. - .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. - .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. - Typically, this indicates that the fully computed representation - of numerals can be so large that non-tail-recursive OCaml - functions run out of stack space when trying to walk them. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. - For example + For example - .. coqtop:: all + .. coqtop:: all - Check 90000. + Check 90000. - .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. - As noted above, the :n:`(abstract after @num)` directive has no - effect when :n:`@ident__2` lands in an :g:`option` type. + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 43a70ca13b..c35c4bd18e 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -55,8 +55,6 @@ type position = | Like of string | Level of string -let warning_verbose = ref true - let rec derive_eps = function Slist0 _ -> true @@ -96,7 +94,7 @@ let is_before s1 s2 = | Stoken _, _ -> true | _ -> false -let insert_tree entry_name gsymbols action tree = +let insert_tree ~warning entry_name gsymbols action tree = let rec insert symbols tree = match symbols with s :: sl -> insert_in_tree s sl tree @@ -105,14 +103,16 @@ let insert_tree entry_name gsymbols action tree = Node {node = s; son = son; brother = bro} -> Node {node = s; son = son; brother = insert [] bro} | LocAct (old_action, action_list) -> - if !warning_verbose then - begin - eprintf "<W> Grammar extension: "; - if entry_name <> "" then eprintf "in [%s], " entry_name; - eprintf "some rule has been masked\n"; - flush stderr - end; - LocAct (action, old_action :: action_list) + begin match warning with + | None -> () + | Some warn_fn -> + let msg = + "<W> Grammar extension: " ^ + (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ + "some rule has been masked" in + warn_fn msg + end; + LocAct (action, old_action :: action_list) | DeadEnd -> LocAct (action, []) and insert_in_tree s sl tree = match try_insert s sl tree with @@ -141,10 +141,10 @@ let insert_tree entry_name gsymbols action tree = in insert gsymbols tree -let srules rl = +let srules ~warning rl = let t = List.fold_left - (fun tree (symbols, action) -> insert_tree "" symbols action tree) + (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) DeadEnd rl in Stree t @@ -175,15 +175,15 @@ and token_exists_in_symbol f = | Stree t -> token_exists_in_tree f t | Snterm _ | Snterml (_, _) | Snext | Sself -> false -let insert_level entry_name e1 symbols action slev = +let insert_level ~warning entry_name e1 symbols action slev = match e1 with true -> {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree entry_name symbols action slev.lsuffix; + lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix; lprefix = slev.lprefix} | false -> {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree entry_name symbols action slev.lprefix} + lprefix = insert_tree ~warning entry_name symbols action slev.lprefix} let empty_lev lname assoc = let assoc = @@ -193,27 +193,33 @@ let empty_lev lname assoc = in {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev lev n lname assoc = +let change_lev ~warning lev n lname assoc = let a = match assoc with None -> lev.assoc | Some a -> - if a <> lev.assoc && !warning_verbose then - begin - eprintf "<W> Changing associativity of level \"%s\"\n" n; - flush stderr - end; + if a <> lev.assoc then + begin + match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Changing associativity of level \""^n^"\"") + end; a in begin match lname with Some n -> - if lname <> lev.lname && !warning_verbose then - begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end + if lname <> lev.lname then + begin match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Level label \""^n^"\" ignored") + end; | None -> () end; {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} -let get_level entry position levs = +let get_level ~warning entry position levs = match position with Some First -> [], empty_lev, levs | Some Last -> levs, empty_lev, [] @@ -226,7 +232,7 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if is_level_labelled n lev then [], change_lev lev n, levs + if is_level_labelled n lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in @@ -268,14 +274,14 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if token_exists_in_level f lev then [], change_lev lev n, levs + if token_exists_in_level f lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in get levs | None -> match levs with - lev :: levs -> [], change_lev lev "<top>", levs + lev :: levs -> [], change_lev ~warning lev "<top>", levs | [] -> [], empty_lev, [] let rec check_gram entry = @@ -347,7 +353,7 @@ let insert_tokens gram symbols = in List.iter insert symbols -let levels_of_rules entry position rules = +let levels_of_rules ~warning entry position rules = let elev = match entry.edesc with Dlevels elev -> elev @@ -358,7 +364,7 @@ let levels_of_rules entry position rules = in if rules = [] then elev else - let (levs1, make_lev, levs2) = get_level entry position elev in + let (levs1, make_lev, levs2) = get_level ~warning entry position elev in let (levs, _) = List.fold_left (fun (levs, make_lev) (lname, assoc, level) -> @@ -370,7 +376,7 @@ let levels_of_rules entry position rules = List.iter (check_gram entry) symbols; let (e1, symbols) = get_initial entry symbols in insert_tokens entry.egram symbols; - insert_level entry.ename e1 symbols action lev) + insert_level ~warning entry.ename e1 symbols action lev) lev level in lev :: levs, empty_lev) diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index 8361e21645..ecb95ec61b 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -53,15 +53,14 @@ type position = | Like of string | Level of string -val levels_of_rules : +val levels_of_rules : warning:(string -> unit) option -> 'te g_entry -> position option -> (string option * g_assoc option * ('te g_symbol list * g_action) list) list -> 'te g_level list -val srules : ('te g_symbol list * g_action) list -> 'te g_symbol + +val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : 'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list - -val warning_verbose : bool ref diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index dfce26a33a..285c14ec62 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -755,9 +755,9 @@ let init_entry_functions entry = let f = continue_parser_of_entry entry in entry.econtinue <- f; f lev bp a strm) -let extend_entry entry position rules = +let extend_entry ~warning entry position rules = try - let elev = Gramext.levels_of_rules entry position rules in + let elev = Gramext.levels_of_rules ~warning entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry with Plexing.Error s -> Printf.eprintf "Lexer initialization error:\n- %s\n" s; @@ -841,8 +841,6 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () -let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer - (* Functorial interface *) module type GLexerType = sig type te val lexer : te Plexing.lexer end @@ -881,7 +879,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -889,10 +887,9 @@ module type S = val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> @@ -945,7 +942,7 @@ module GMake (L : GLexerType) = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t) + let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t) let r_stop = [] let r_next r s = r @ [s] let production @@ -953,15 +950,12 @@ module GMake (L : GLexerType) = Obj.magic p module Unsafe = struct - let gram_reinit = gram_reinit gram let clear_entry = clear_entry end - let extend = extend_entry - let safe_extend e pos + let safe_extend ~warning e pos (r : (string option * Gramext.g_assoc option * Obj.t ty_production list) list) = - extend e pos (Obj.magic r) - let delete_rule e r = delete_rule (Entry.obj e) r - let safe_delete_rule = delete_rule + extend_entry ~warning e pos (Obj.magic r) + let safe_delete_rule e r = delete_rule (Entry.obj e) r end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 1e14e557bc..0c585a7c0d 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -53,7 +53,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -62,10 +62,9 @@ module type S = module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 8c4649fc39..0793a1cc1c 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -37,9 +37,8 @@ let reroute_stdout_stderr () = Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr -(* We also provide specific kill and interrupt functions. *) +(* We also provide a specific interrupt function. *) -external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c index c09bf37dee..f430c9f2b6 100644 --- a/ide/ide_win32_stubs.c +++ b/ide/ide_win32_stubs.c @@ -4,22 +4,6 @@ #include <caml/memory.h> #include <windows.h> -/* Win32 emulation of kill -9 */ - -/* The pid returned by Unix.create_process is actually a pseudo-pid, - made via a cast of the obtained HANDLE, (cf. win32unix/createprocess.c - in the sources of ocaml). Since we're still in the caller process, - we simply cast back to get an handle... - The 0 is the exit code we want for the terminated process. -*/ - -CAMLprim value win32_kill(value pseudopid) { - CAMLparam1(pseudopid); - TerminateProcess((HANDLE)(Long_val(pseudopid)), 0); - CAMLreturn(Val_unit); -} - - /* Win32 emulation of a kill -2 (SIGINT) */ /* This code rely of the fact that coqide is now without initial console. diff --git a/parsing/extend.ml b/parsing/extend.ml index 5caeab535a..050ed49622 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -14,17 +14,8 @@ type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e type side = Left | Right -type gram_assoc = NonA | RightA | LeftA - -type gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type production_position = - | BorderProd of side * gram_assoc option + | BorderProd of side * Gramlib.Gramext.g_assoc option | InternalProd type production_level = @@ -116,11 +107,11 @@ type 'a production_rule = type 'a single_extend_statement = string option * (** Level *) - gram_assoc option * + Gramlib.Gramext.g_assoc option * (** Associativity *) 'a production_rule list (** Symbol list with the interpretation function *) type 'a extend_statement = - gram_position option * + Gramlib.Gramext.position option * 'a single_extend_statement list diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index d8c08803b6..fc5feba58b 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -32,7 +32,7 @@ type grammar_constr_prod_item = type one_notation_grammar = { notgram_level : level; - notgram_assoc : Extend.gram_assoc option; + notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; } diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 170df6ad09..816a02a6aa 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,8 +14,6 @@ open Extend open Genarg open Gramlib -let uncurry f (x,y) = f x y - (** Location Utils *) let ploc_file_of_coq_file = function | Loc.ToplevelInput -> "" @@ -82,7 +80,6 @@ module type S = end *) - type 'a entry = 'a Entry.e type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable @@ -91,12 +88,10 @@ module type S = val comment_state : coq_parsable -> ((int * int) * string) list -end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct +end with type 'a Entry.e = 'a Extend.entry = struct include Grammar.GMake(CLexer) - type 'a entry = 'a Entry.e - type coq_parsable = parsable * CLexer.lexer_state ref let coq_parsable ?(file=Loc.ToplevelInput) c = @@ -146,20 +141,6 @@ struct end -let warning_verbose = Gramext.warning_verbose - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - module Symbols : sig val stoken : Tok.t -> ('s, string) G.ty_symbol val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol @@ -184,12 +165,6 @@ end = struct let slist1sep x y = G.s_list1sep x y false end -let camlp5_verbosity silent f x = - let a = !warning_verbose in - warning_verbose := silent; - f x; - warning_verbose := a - (** Grammar extensions *) (** NB: [extend_statement = @@ -218,7 +193,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol | Anext -> G.s_next | Aentry e -> G.s_nterm e | Aentryl (e, n) -> G.s_nterml e n -| Arules rs -> G.s_rules (List.map symbol_of_rules rs) +| Arules rs -> + let warning msg = Feedback.msg_warning Pp.(str msg) in + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function | Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) @@ -240,10 +217,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> a any_productio AnyProduction (symb, cast act) let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + (lvl, assoc, List.map of_coq_production_rule rule) let of_coq_extend_statement (pos, st) = - (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (pos, List.map of_coq_single_extend_statement st) let fix_extend_statement (pos, st) = let fix_single_extend_statement (lvl, assoc, rules) = @@ -253,19 +230,19 @@ let fix_extend_statement (pos, st) = (pos, List.map fix_single_extend_statement st) (** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () -module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end +module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) - | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind (** The list of extensions *) @@ -282,13 +259,12 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let a = of_coq_assoc a in - let ext = of_coq_position ext in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in - (G.safe_extend e) (Some ext) [Some lev,Some a,[]] + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -296,15 +272,15 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let ext = fix_extend_statement ext in - let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in + let pos, ext = fix_extend_statement ext in + let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - let ext = fix_extend_statement (of_coq_extend_statement ext) in - camlp5_verbosity false (uncurry (G.safe_extend e)) ext + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -352,14 +328,16 @@ let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in let act = fun _ x loc -> x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = G.r_next G.r_stop (G.s_nterm en) in let act = fun x loc -> f x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e (* Parse a string, does NOT check if the entire string was read @@ -489,7 +467,8 @@ let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in - let () = G.safe_extend entry None ext in + let warning msg = Feedback.msg_warning Pp.(str msg) in + let () = G.safe_extend ~warning:(Some warning) entry None ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -542,7 +521,7 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty @@ -574,7 +553,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e64c614149..69ba57d516 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -26,7 +26,7 @@ sig end module Entry : sig - type 'a t = 'a Grammar.GMake(CLexer).Entry.e + type 'a t = 'a Extend.entry val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit @@ -110,10 +110,6 @@ end *) -(** Temporarily activate camlp5 verbosity *) - -val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit - (** Parse a string *) val parse_string : 'a Entry.t -> string -> 'a @@ -202,7 +198,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) val grammar_extend : 'a Entry.t -> gram_reinit option -> diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fa70235975..0509d6ae71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Genintern open Tacexpr open Names open Constrexpr @@ -28,22 +29,22 @@ val wit_natural : int Genarg.uniform_genarg_type val wit_glob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lglob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lconstr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val wit_casted_constr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val glob : constr_expr Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 7fb9a19a0c..4576562634 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -14,4 +14,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) -val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic +val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index f7375a0f01..31fb1c9abf 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -16,6 +16,7 @@ open Names open Locus open Constrexpr open Glob_term +open Genintern open Geninterp open Extraargs open Tacmach @@ -37,8 +38,8 @@ DECLARE PLUGIN "ltac_plugin" { type constr_expr_with_bindings = constr_expr with_bindings -type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings -type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings +type glob_constr_with_bindings = glob_constr_and_expr with_bindings +type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = let _, env = Pfedit.get_current_context () in @@ -70,7 +71,7 @@ END { type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 50cfb6d004..55e58187b0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -26,6 +26,7 @@ open Pputils open Ppconstr open Printer +open Genintern open Tacexpr open Tacarg open Tactics diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6c09e447a5..0ab9e501bc 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -17,6 +17,7 @@ open Names open Environ open Constrexpr open Notation_gram +open Genintern open Tacexpr open Tactypes diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 4f46e78c71..2457b265f0 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -13,6 +13,7 @@ open Environ open EConstr open Constrexpr open Evd +open Genintern open Tactypes open Tacexpr open Tacinterp diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bdb0be03cf..0c7096a4de 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,6 +11,7 @@ open Genarg open EConstr open Constrexpr +open Genintern open Tactypes open Tacexpr diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d2ae92f6ce..b04c3b9f4e 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -53,7 +53,7 @@ val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ac2d88dec2..2aee809eb6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -119,7 +119,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 9435d0b911..2bd21f9d7a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -93,19 +93,8 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +268,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 1527724420..0c27f3bfe2 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -92,20 +92,8 @@ type ml_tactic_entry = { } (** Composite types *) - -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +267,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 178f6af71d..978ad4dd24 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,6 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr +open Genintern open Tactypes (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index f9883e4441..d9c80bb835 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } +open Genintern + val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index d406686c56..4487604dca 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,6 +11,7 @@ open Tacexpr open Mod_subst open Genarg +open Genintern open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 175341df09..91e8510b92 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 0722c68783..457c4e0b9a 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -35,7 +35,7 @@ val match_term : Environ.env -> Evd.evar_map -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic (** [match_goal env sigma hyps concl rules] matches the goal @@ -48,5 +48,5 @@ val match_goal: Evd.evar_map -> EConstr.named_context -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index a786b9953d..bb8a0faf2e 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -47,7 +47,7 @@ type ssrdocc = ssrclear option * ssrocc (* OLD ssr terms *) type ssrtermkind = char (* FIXME, make algebraic *) -type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr +type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e25c93bf0a..824827e90c 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -146,7 +146,7 @@ val interp_refine : val interp_open_constr : Tacinterp.interp_sign -> Goal.goal Evd.sigma -> - Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) + Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : Goal.goal Evd.sigma -> diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 8cb0a8b463..6497b6ff98 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -896,7 +896,7 @@ let interp_rpattern s = function let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG let cpattern_of_term (c, t) ist = c, t, Some ist diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 93a8c48435..8672c55767 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -5,9 +5,7 @@ open Goal open Environ open Evd open Constr - -open Ltac_plugin -open Tacexpr +open Genintern (** ******** Small Scale Reflection pattern matching facilities ************* *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 16101396cf..43abc0a200 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -33,24 +33,24 @@ open Pcoq let constr_level = string_of_int let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,false; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 9,Gramlib.Gramext.RightA,false; + 8,Gramlib.Gramext.RightA,true; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,true; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_constr_levels = (default_levels, default_pattern_levels) @@ -70,28 +70,28 @@ let save_levels levels custom lev = (* first LeftA, then RightA and NoneA together *) let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false + | Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false + | Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false | _ -> true let create_assoc = function - | None -> Extend.RightA + | None -> Gramlib.Gramext.RightA | Some a -> a let error_level_assoc p current expected = let open Pp in let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in + | Gramlib.Gramext.LeftA -> str "left" + | Gramlib.Gramext.RightA -> str "right" + | Gramlib.Gramext.NonA -> str "non" in user_err (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ pr_assoc expected ++ str " associative.") let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) + | None -> Gramlib.Gramext.First + | Some lev -> Gramlib.Gramext.After (constr_level lev) let find_position_gen current ensure assoc lev = match lev with @@ -121,13 +121,13 @@ let find_position_gen current ensure assoc lev = updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - updated, (Some (Extend.Level (constr_level n)), None, None, !init) + updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) end with (* Nothing has changed *) Exit -> (* Just inherit the existing associativity and name (None) *) - current, (Some (Extend.Level (constr_level n)), None, None, None) + current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) let rec list_mem_assoc_triple x = function | [] -> false @@ -186,15 +186,18 @@ let find_position accu custom forpat assoc level = (* Binding constr entry keys to entries *) (* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp5_assoc = function - | Some NonA | Some RightA -> RightA - | None | Some LeftA -> LeftA - -let assoc_eq al ar = match al, ar with -| NonA, NonA -| RightA, RightA -| LeftA, LeftA -> true -| _, _ -> false +let camlp5_assoc = + let open Gramlib.Gramext in function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = + let open Gramlib.Gramext in + match al, ar with + | NonA, NonA + | RightA, RightA + | LeftA, LeftA -> true + | _, _ -> false (* [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of @@ -204,7 +207,7 @@ let assoc_eq al ar = match al, ar with Some None = NEXT Some (Some (n,cur)) = constr LEVEL n s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function +let adjust_level assoc from = let open Gramlib.Gramext in function (* Associativity is None means force the level *) | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) (* Compute production name on the right side *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index e3f6a87541..22528a607f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1175,9 +1175,9 @@ GRAMMAR EXTEND Gram | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) } | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural -> { SetCustomEntry (x,Some n) } - | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA } - | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA } - | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA } + | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA } + | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA } + | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA } | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting } | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing } | IDENT "compat"; s = STRING -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5ab877fae2..82434afbbd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -287,7 +287,7 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = function +let prec_assoc = let open Gramlib.Gramext in function | RightA -> (L,E) | LeftA -> (E,L) | NonA -> (L,L) @@ -685,7 +685,7 @@ let border = function | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a | _ -> None -let recompute_assoc typs = +let recompute_assoc typs = let open Gramlib.Gramext in match border typs, border (List.rev typs) with | Some LeftA, Some RightA -> assert false | Some LeftA, _ -> Some LeftA @@ -802,7 +802,7 @@ let inSyntaxExtension : syntax_extension_obj -> obj = module NotationMods = struct type notation_modifier = { - assoc : gram_assoc option; + assoc : Gramlib.Gramext.g_assoc option; level : int option; custom : notation_entry; etyps : (Id.t * simple_constr_prod_entry_key) list; @@ -1230,7 +1230,7 @@ let compute_syntax_data local df modifiers = let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); - let assoc = Option.append mods.assoc (Some NonA) in + let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in let _ = check_useless_entry_types recvars mainvars mods.etyps in let _ = check_binder_type recvars mods.etyps in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2ddd210365..e7c1e29beb 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -380,7 +380,7 @@ open Pputils let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) - let pr_syntax_modifier = function + let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ pr_opt pr_constr_as_binder_kind bko diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 122005e011..1e6c40c829 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,7 +167,7 @@ type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option | SetLevel of int | SetCustomEntry of string * int option - | SetAssoc of Extend.gram_assoc + | SetAssoc of Gramlib.Gramext.g_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting |