diff options
38 files changed, 214 insertions, 474 deletions
diff --git a/META.coq.in b/META.coq.in index 25c0b666f4..b3a96a8303 100644 --- a/META.coq.in +++ b/META.coq.in @@ -146,7 +146,7 @@ package "gramlib" ( description = "Coq Grammar Engine" version = "8.10" - requires = "" + requires = "coq.lib" directory = "gramlib__pack" archive(byte) = "gramlib.cma" diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh new file mode 100644 index 0000000000..3600f1cd3e --- /dev/null +++ b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then + + elpi_CI_REF=vernac+remove_empty_hooks + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + equations_CI_REF=vernac+remove_empty_hooks + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + paramcoq_CI_REF=vernac+remove_empty_hooks + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + plugin_tutorial_CI_REF=vernac+remove_empty_hooks + plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials + + mtac2_CI_REF=vernac+remove_empty_hooks + mtac2_CI_GITURL=https://github.com/ejgallego/mtac2 + +fi diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh new file mode 100644 index 0000000000..e9daa7a44e --- /dev/null +++ b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then + + elpi_CI_REF=gramlib+no_ploc + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/gramlib/dune b/gramlib/dune index 6a9e622b4c..8ca6aff25a 100644 --- a/gramlib/dune +++ b/gramlib/dune @@ -1,3 +1,4 @@ (library (name gramlib) - (public_name coq.gramlib)) + (public_name coq.gramlib) + (libraries coq.lib)) diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index c35c4bd18e..46c2688f05 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -8,7 +8,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t type 'te grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - mutable glexer : 'te Plexing.lexer } + glexer : 'te Plexing.lexer } type 'te g_entry = { egram : 'te grammar; @@ -52,7 +52,6 @@ type position = | Last | Before of string | After of string - | Like of string | Level of string let rec derive_eps = @@ -154,27 +153,6 @@ let is_level_labelled n lev = Some n1 -> n = n1 | None -> false -let rec token_exists_in_level f lev = - token_exists_in_tree f lev.lprefix || token_exists_in_tree f lev.lsuffix -and token_exists_in_tree f = - function - Node n -> - token_exists_in_symbol f n.node || token_exists_in_tree f n.brother || - token_exists_in_tree f n.son - | LocAct (_, _) | DeadEnd -> false -and token_exists_in_symbol f = - function - | Slist0 sy -> token_exists_in_symbol f sy - | Slist0sep (sy, sep, _) -> - token_exists_in_symbol f sy || token_exists_in_symbol f sep - | Slist1 sy -> token_exists_in_symbol f sy - | Slist1sep (sy, sep, _) -> - token_exists_in_symbol f sy || token_exists_in_symbol f sep - | Sopt sy -> token_exists_in_symbol f sy - | Stoken tok -> f tok - | Stree t -> token_exists_in_tree f t - | Snterm _ | Snterml (_, _) | Snext | Sself -> false - let insert_level ~warning entry_name e1 symbols action slev = match e1 with true -> @@ -265,58 +243,11 @@ let get_level ~warning entry position levs = let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in get levs - | Some (Like n) -> - let f (tok, prm) = n = tok || n = prm in - let rec get = - function - [] -> - eprintf "No level with \"%s\" in entry \"%s\"\n" n entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: 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 ~warning lev "<top>", levs | [] -> [], empty_lev, [] -let rec check_gram entry = - function - Snterm e -> - if e.egram != entry.egram then - begin - eprintf "\ -Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n" - entry.ename e.ename; - flush stderr; - failwith "Grammar.extend error" - end - | Snterml (e, _) -> - if e.egram != entry.egram then - begin - eprintf "\ -Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n" - entry.ename e.ename; - flush stderr; - failwith "Grammar.extend error" - end - | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s - | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s - | Slist0 s -> check_gram entry s - | Slist1 s -> check_gram entry s - | Sopt s -> check_gram entry s - | Stree t -> tree_check_gram entry t - | Snext | Sself | Stoken _ -> () -and tree_check_gram entry = - function - Node {node = n; brother = bro; son = son} -> - check_gram entry n; tree_check_gram entry bro; tree_check_gram entry son - | LocAct (_, _) | DeadEnd -> () - let change_to_self entry = function Snterm e when e == entry -> Sself @@ -373,7 +304,6 @@ let levels_of_rules ~warning entry position rules = List.fold_left (fun lev (symbols, action) -> let symbols = List.map (change_to_self entry) symbols in - List.iter (check_gram entry) symbols; let (e1, symbols) = get_initial entry symbols in insert_tokens entry.egram symbols; insert_level ~warning entry.ename e1 symbols action lev) diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index ecb95ec61b..f1e294fb4c 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -6,7 +6,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t type 'te grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - mutable glexer : 'te Plexing.lexer } + glexer : 'te Plexing.lexer } type 'te g_entry = { egram : 'te grammar; @@ -50,7 +50,6 @@ type position = | Last | Before of string | After of string - | Like of string | Level of string val levels_of_rules : warning:(string -> unit) option -> diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 285c14ec62..0ad11d075f 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -130,7 +130,7 @@ let loc_of_token_interval bp ep = if bp == ep then if bp == 0 then Ploc.dummy else Ploc.after (!floc (bp - 1)) 0 1 else - let loc1 = !floc bp in let loc2 = !floc (pred ep) in Ploc.encl loc1 loc2 + let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2 let name_of_symbol entry = function @@ -186,84 +186,6 @@ and name_of_tree_failed entry = end | DeadEnd | LocAct (_, _) -> "???" -let search_tree_in_entry prev_symb tree = - function - Dlevels levels -> - let rec search_levels = - function - [] -> tree - | level :: levels -> - match search_level level with - Some tree -> tree - | None -> search_levels levels - and search_level level = - match search_tree level.lsuffix with - Some t -> Some (Node {node = Sself; son = t; brother = DeadEnd}) - | None -> search_tree level.lprefix - and search_tree t = - if tree <> DeadEnd && t == tree then Some t - else - match t with - Node n -> - begin match search_symbol n.node with - Some symb -> - Some (Node {node = symb; son = n.son; brother = DeadEnd}) - | None -> - match search_tree n.son with - Some t -> - Some (Node {node = n.node; son = t; brother = DeadEnd}) - | None -> search_tree n.brother - end - | LocAct (_, _) | DeadEnd -> None - and search_symbol symb = - match symb with - Snterm _ | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) | - Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ | Stree _ - when symb == prev_symb -> - Some symb - | Slist0 symb -> - begin match search_symbol symb with - Some symb -> Some (Slist0 symb) - | None -> None - end - | Slist0sep (symb, sep, b) -> - begin match search_symbol symb with - Some symb -> Some (Slist0sep (symb, sep, b)) - | None -> - match search_symbol sep with - Some sep -> Some (Slist0sep (symb, sep, b)) - | None -> None - end - | Slist1 symb -> - begin match search_symbol symb with - Some symb -> Some (Slist1 symb) - | None -> None - end - | Slist1sep (symb, sep, b) -> - begin match search_symbol symb with - Some symb -> Some (Slist1sep (symb, sep, b)) - | None -> - match search_symbol sep with - Some sep -> Some (Slist1sep (symb, sep, b)) - | None -> None - end - | Sopt symb -> - begin match search_symbol symb with - Some symb -> Some (Sopt symb) - | None -> None - end - | Stree t -> - begin match search_tree t with - Some t -> Some (Stree t) - | None -> None - end - | _ -> None - in - search_levels levels - | Dparser _ -> tree - -let error_verbose = ref false - let tree_failed entry prev_symb_result prev_symb tree = let txt = name_of_tree_failed entry tree in let txt = @@ -295,18 +217,6 @@ let tree_failed entry prev_symb_result prev_symb tree = | Sopt _ | Stree _ -> txt ^ " expected" | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb in - if !error_verbose then - begin let tree = search_tree_in_entry prev_symb tree entry.edesc in - let ppf = err_formatter in - fprintf ppf "@[<v 0>@,"; - fprintf ppf "----------------------------------@,"; - fprintf ppf "Parse error in entry [%s], rule:@;<0 2>" entry.ename; - fprintf ppf "@["; - print_level ppf pp_force_newline (flatten_tree tree); - fprintf ppf "@]@,"; - fprintf ppf "----------------------------------@,"; - fprintf ppf "@]@." - end; txt ^ " (in [" ^ entry.ename ^ "])" let symb_failed entry prev_symb_result prev_symb symb = @@ -374,11 +284,8 @@ let do_recover parser_of_tree entry nlevn alevn bp a s son continue entry bp a s son (parser_of_tree entry nlevn alevn son) strm__ -let strict_parsing = ref false - let recover parser_of_tree entry nlevn alevn bp a s son strm = - if !strict_parsing then raise (Stream.Error (tree_failed entry a s son)) - else do_recover parser_of_tree entry nlevn alevn bp a s son strm + do_recover parser_of_tree entry nlevn alevn bp a s son strm let token_count = ref 0 @@ -794,8 +701,6 @@ let tokens g con = g.gtokens; !list -let glexer g = g.glexer - type 'te gen_parsable = { pa_chr_strm : char Stream.t; pa_tok_strm : 'te Stream.t; @@ -816,7 +721,7 @@ let parse_parsable entry p = let cnt = Stream.count ts in let loc = fun_loc cnt in if !token_count - 1 <= cnt then loc - else Ploc.encl loc (fun_loc (!token_count - 1)) + else Loc.merge loc (fun_loc (!token_count - 1)) with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1) in floc := fun_loc; @@ -851,7 +756,6 @@ module type S = type parsable val parsable : char Stream.t -> parsable val tokens : string -> (string * int) list - val glexer : te Plexing.lexer module Entry : sig type 'a e @@ -884,7 +788,7 @@ module type S = val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule - val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production + val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig val clear_entry : 'a Entry.e -> unit @@ -906,7 +810,6 @@ module GMake (L : GLexerType) = let (ts, lf) = L.lexer.Plexing.tok_func cs in {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} let tokens = tokens gram - let glexer = glexer gram module Entry = struct type 'a e = te g_entry @@ -946,7 +849,7 @@ module GMake (L : GLexerType) = let r_stop = [] let r_next r s = r @ [s] let production - (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production = + (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production = Obj.magic p module Unsafe = struct diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 0c585a7c0d..bde07ddc48 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -25,7 +25,6 @@ module type S = type parsable val parsable : char Stream.t -> parsable val tokens : string -> (string * int) list - val glexer : te Plexing.lexer module Entry : sig type 'a e @@ -58,7 +57,7 @@ module type S = val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule - val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production + val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index 986363ec1f..f99a3c2480 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -6,14 +6,13 @@ type pattern = string * string exception Error of string -type location = Ploc.t -type location_function = int -> location +type location_function = int -> Loc.t type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function type 'te lexer = { tok_func : 'te lexer_func; tok_using : pattern -> unit; tok_removing : pattern -> unit; - mutable tok_match : pattern -> 'te -> string; + tok_match : pattern -> 'te -> string; tok_text : pattern -> string; - mutable tok_comm : location list option } + } diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 96b432a8ad..eed4082e00 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -28,10 +28,10 @@ type 'te lexer = { tok_func : 'te lexer_func; tok_using : pattern -> unit; tok_removing : pattern -> unit; - mutable tok_match : pattern -> 'te -> string; + tok_match : pattern -> 'te -> string; tok_text : pattern -> string; - mutable tok_comm : Ploc.t list option } + } and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function -and location_function = int -> Ploc.t +and location_function = int -> Loc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index 082686db01..9342fc6c1d 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -2,60 +2,23 @@ (* ploc.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -type t = - { fname : string; - line_nb : int; - bol_pos : int; - line_nb_last : int; - bol_pos_last : int; - bp : int; - ep : int; - comm : string; - ecomm : string } - -let make_loc fname line_nb bol_pos (bp, ep) comm = - {fname = fname; line_nb = line_nb; bol_pos = bol_pos; - line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; - comm = comm; ecomm = ""} +open Loc let make_unlined (bp, ep) = - {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = bp; ep = ep; comm = ""; ecomm = ""} let dummy = - {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; comm = ""; ecomm = ""} -let file_name loc = loc.fname -let first_pos loc = loc.bp -let last_pos loc = loc.ep -let line_nb loc = loc.line_nb -let bol_pos loc = loc.bol_pos -let line_nb_last loc = loc.line_nb_last -let bol_pos_last loc = loc.bol_pos_last -let comment loc = loc.comm -let comment_last loc = loc.ecomm - (* *) -let encl loc1 loc2 = - if loc1.bp < loc2.bp then - if loc1.ep < loc2.ep then - {fname = loc1.fname; line_nb = loc1.line_nb; bol_pos = loc1.bol_pos; - line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last; - bp = loc1.bp; ep = loc2.ep; comm = loc1.comm; ecomm = loc2.comm} - else loc1 - else if loc2.ep < loc1.ep then - {fname = loc2.fname; line_nb = loc2.line_nb; bol_pos = loc2.bol_pos; - line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last; - bp = loc2.bp; ep = loc1.ep; comm = loc2.comm; ecomm = loc1.comm} - else loc2 -let shift sh loc = {loc with bp = sh + loc.bp; ep = sh + loc.ep} let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} let with_comment loc comm = {loc with comm = comm} -exception Exc of t * exn +exception Exc of Loc.t * exn let raise loc exc = match exc with diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 2ce6382183..766e96fdfc 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -2,85 +2,36 @@ (* ploc.mli,v *) (* Copyright (c) INRIA 2007-2017 *) -(** Locations and some pervasive type and value. *) - -type t - (* located exceptions *) -exception Exc of t * exn +exception Exc of Loc.t * exn (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with the input location [loc]. To be used to specify a location for an error. This exception must not be raised by [raise] but rather by [Ploc.raise] (see below), to prevent the risk of several encapsulations of [Ploc.Exc]. *) -val raise : t -> exn -> 'a +val raise : Loc.t -> exn -> 'a (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc], re-raise it (ignoring the new location [loc]), else raise the exception [Ploc.Exc loc e]. *) -(* making locations *) - -val make_loc : string -> int -> int -> int * int -> string -> t - (** [Ploc.make_loc fname line_nb bol_pos (bp, ep) comm] creates a location - starting at line number [line_nb], where the position of the beginning - of the line is [bol_pos] and between the positions [bp] (included) and - [ep] excluded. And [comm] is the comment before the location. The - positions are in number of characters since the begin of the stream. *) -val make_unlined : int * int -> t +val make_unlined : int * int -> Loc.t (** [Ploc.make_unlined] is like [Ploc.make] except that the line number is not provided (to be used e.g. when the line number is unknown. *) -val dummy : t +val dummy : Loc.t (** [Ploc.dummy] is a dummy location, used in situations when location has no meaning. *) -(* getting location info *) - -val file_name : t -> string - (** [Ploc.file_name loc] returns the file name of the location. *) -val first_pos : t -> int - (** [Ploc.first_pos loc] returns the position of the begin of the location - in number of characters since the beginning of the stream. *) -val last_pos : t -> int - (** [Ploc.last_pos loc] returns the position of the first character not - in the location in number of characters since the beginning of the - stream. *) -val line_nb : t -> int - (** [Ploc.line_nb loc] returns the line number of the location or [-1] if - the location does not contain a line number (i.e. built with - [Ploc.make_unlined]. *) -val bol_pos : t -> int - (** [Ploc.bol_pos loc] returns the position of the beginning of the line - of the location in number of characters since the beginning of - the stream, or [0] if the location does not contain a line number - (i.e. built with [Ploc.make_unlined]. *) -val line_nb_last : t -> int -val bol_pos_last : t -> int - (** Return the line number and the position of the beginning of the line - of the last position. *) -val comment : t -> string - (** [Ploc.comment loc] returns the comment before the location. *) -val comment_last : t -> string - (** [Ploc.comment loc] returns the last comment of the location. *) - (* combining locations *) -val encl : t -> t -> t - (** [Ploc.encl loc1 loc2] returns the location starting at the - smallest start of [loc1] and [loc2] and ending at the greatest end - of them. In other words, it is the location enclosing [loc1] and - [loc2]. *) -val shift : int -> t -> t - (** [Ploc.shift sh loc] returns the location [loc] shifted with [sh] - characters. The line number is not recomputed. *) -val sub : t -> int -> int -> t +val sub : Loc.t -> int -> int -> Loc.t (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh] characters and with length [len]. The previous ending position of the location is lost. *) -val after : t -> int -> int -> t +val after : Loc.t -> int -> int -> Loc.t (** [Ploc.after loc sh len] is the location just after loc (starting at the end position of [loc]) shifted with [sh] characters and of length [len]. *) -val with_comment : t -> string -> t +val with_comment : Loc.t -> string -> Loc.t (** Change the comment part of the given location *) diff --git a/lib/loc.ml b/lib/loc.ml index 1a09091bff..c08648911b 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -22,15 +22,19 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) + comm : string; (** start comment *) + ecomm : string (** end comment *) } let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; - line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } + line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; + comm = ""; ecomm = "" } let make_loc (bp, ep) = { fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = bp; ep = ep; } + bp = bp; ep = ep; + comm = ""; ecomm = "" } let mergeable loc1 loc2 = loc1.fname = loc2.fname @@ -45,7 +49,8 @@ let merge loc1 loc2 = bol_pos = loc1.bol_pos; line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last; - bp = loc1.bp; ep = loc2.ep; } + bp = loc1.bp; ep = loc2.ep; + comm = loc1.comm; ecomm = loc2.comm } else loc1 else if loc2.ep < loc1.ep then { fname = loc2.fname; @@ -53,7 +58,9 @@ let merge loc1 loc2 = bol_pos = loc2.bol_pos; line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last; - bp = loc2.bp; ep = loc1.ep; } + bp = loc2.bp; ep = loc1.ep; + comm = loc2.comm; ecomm = loc1.comm + } else loc2 let merge_opt l1 l2 = match l1, l2 with diff --git a/lib/loc.mli b/lib/loc.mli index 23df1ebd9a..c46311b639 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -22,6 +22,8 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) + comm : string; (** start comment *) + ecomm : string (** end comment *) } (** {5 Location manipulation} *) diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index d81ee475b5..c2b7fa117d 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -13,28 +13,6 @@ open Util open Tok open Gramlib -(** Location utilities *) -let ploc_file_of_coq_file = function -| Loc.ToplevelInput -> "" -| Loc.InFile f -> f - -let coq_file_of_ploc_file s = - if s = "" then Loc.ToplevelInput else Loc.InFile s - -let from_coqloc fname line_nb bol_pos bp ep = - Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) "" - -let to_coqloc loc = - { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); - Loc.line_nb = Ploc.line_nb loc; - Loc.bol_pos = Ploc.bol_pos loc; - Loc.bp = Ploc.first_pos loc; - Loc.ep = Ploc.last_pos loc; - Loc.line_nb_last = Ploc.line_nb_last loc; - Loc.bol_pos_last = Ploc.bol_pos_last loc; } - -let (!@) = to_coqloc - (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) @@ -128,18 +106,22 @@ module Error = struct end open Error -let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str) +let err loc str = Loc.raise ~loc (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) (* Update a loc without allocating an intermediate pair *) let set_loc_pos loc bp ep = - Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp) + Ploc.sub loc (bp - loc.Loc.bp) (ep - bp) (* Increase line number by 1 and update position of beginning of line *) let bump_loc_line loc bol_pos = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + Loc.{ loc with + line_nb = loc.line_nb + 1; + line_nb_last = loc.line_nb + 1; + bol_pos; + bol_pos_last = bol_pos; + } (* Same as [bump_loc_line], but for the last line in location *) (* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop, @@ -147,19 +129,25 @@ let bump_loc_line loc bol_pos = (* Warning: [bump_loc_line_last] changes the end position. You may need to call [set_loc_pos] to fix it. *) let bump_loc_line_last loc bol_pos = - let loc' = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos - (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc) - in - Ploc.encl loc loc' + let open Loc in + let loc' = { loc with + line_nb = loc.line_nb_last + 1; + line_nb_last = loc.line_nb_last + 1; + bol_pos; + bol_pos_last = bol_pos; + bp = loc.bp + 1; + ep = loc.ep + 1; + } in + Loc.merge loc loc' (* For some reason, the [Ploc.after] function of Camlp5 does not update line numbers, so we define our own function that does it. *) let after loc = - let line_nb = Ploc.line_nb_last loc in - let bol_pos = Ploc.bol_pos_last loc in - Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos - (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + Loc.{ loc with + line_nb = loc.line_nb_last; + bol_pos = loc.bol_pos_last; + bp = loc.ep; + } (** Lexer conventions on tokens *) @@ -324,7 +312,7 @@ let rec ident_tail loc len s = match Stream.peek s with | Utf8Token (st, n) when Unicode.is_unknown st -> let id = get_buff len in let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in - warn_unrecognized_unicode ~loc:!@loc (u,id); len + warn_unrecognized_unicode ~loc (u,id); len | _ -> len let rec number len s = match Stream.peek s with @@ -368,7 +356,7 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with Stream.junk s; let () = match comm_level with | Some 0 -> - warn_comment_terminator_in_string ~loc:!@loc () + warn_comment_terminator_in_string ~loc () | _ -> () in let comm_level = Option.map pred comm_level in @@ -757,7 +745,7 @@ let token_text = function let func cs = let loct = loct_create () in - let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in + let cur_loc = ref (Loc.create !current_file 1 0 0 0) in let ts = Stream.from (fun i -> @@ -775,7 +763,6 @@ let lexer = { | _ -> ()); Plexing.tok_removing = (fun _ -> ()); Plexing.tok_match = Tok.match_pattern; - Plexing.tok_comm = None; Plexing.tok_text = token_text } (** Terminal symbols interpretation *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 816a02a6aa..923147ba2e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,29 +14,6 @@ open Extend open Genarg open Gramlib -(** Location Utils *) -let ploc_file_of_coq_file = function -| Loc.ToplevelInput -> "" -| Loc.InFile f -> f - -let coq_file_of_ploc_file s = - if s = "" then Loc.ToplevelInput else Loc.InFile s - -let of_coqloc loc = - let open Loc in - Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) "" - -let to_coqloc loc = - { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); - Loc.line_nb = Ploc.line_nb loc; - Loc.bol_pos = Ploc.bol_pos loc; - Loc.bp = Ploc.first_pos loc; - Loc.ep = Ploc.last_pos loc; - Loc.line_nb_last = Ploc.line_nb_last loc; - Loc.bol_pos_last = Ploc.bol_pos_last loc; } - -let (!@) = to_coqloc - (** The parser of Coq *) module G : sig @@ -112,7 +89,7 @@ end with type 'a Entry.e = 'a Extend.entry = struct with Ploc.Exc (loc,e) -> CLexer.drop_lexer_state (); let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in + let loc = match loc' with None -> loc | Some loc -> loc in Loc.raise ~loc e let comment_state (p,state) = @@ -197,8 +174,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol 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)) +and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function +| Stop -> Casted (G.r_stop, fun act loc -> act loc) | Next (r, s) -> let Casted (r, cast) = symbol_of_rule r in Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x))) @@ -209,7 +186,7 @@ and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function G.production (symb, cast act) (** FIXME: This is a hack around a deficient camlp5 API *) -type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production +type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 69ba57d516..352857d4cd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,7 +13,6 @@ open Extend open Genarg open Constrexpr open Libnames -open Gramlib (** The parser of Coq *) @@ -261,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b -(** Location Utils *) -val of_coqloc : Loc.t -> Ploc.t -val to_coqloc : Ploc.t -> Loc.t -val (!@) : Ploc.t -> Loc.t - type frozen_t val parser_summary_tag : frozen_t Summary.Dyn.tag diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef1d1af199..3b95423067 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1005,8 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd - lemma_type - (Lemmas.mk_hook (fun _ _ -> ())); + lemma_type; ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5ba9735690..4cdfc6fac5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -310,7 +310,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) - hook ; (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in @@ -326,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin match entries with | [entry] -> discard_current (); - (id,(entry,persistence)), CEphemeron.create hook + (id,(entry,persistence)), hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") end @@ -386,7 +385,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind hook + save false new_princ_name entry g_kind ~hook with e when CErrors.noncritical e -> begin begin diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 35acbea488..3a04c753ea 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -415,7 +415,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~program_mode:false fname (Decl_kinds.Global,false,Decl_kinds.Definition) pl - bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); + bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c864bfe9f7..19f954c10d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,_,kind) hook = +let save with_clean id const ?hook (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + Lemmas.call_hook ?hook ~fix_exn l r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index c9d153d89f..9584649cff 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,8 +42,7 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - Lemmas.declaration_hook CEphemeron.key -> unit +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d1a227d517..95e2e9f6e5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -806,8 +806,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd - typ - (Lemmas.mk_hook (fun _ _ -> ())); + typ; ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); @@ -867,8 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + (fst lemmas_types_infos.(i)); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6e5e3f9353..38f27f760b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1372,7 +1372,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type - (Lemmas.mk_hook hook); + ~hook:(Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then ignore (by (Proofview.V82.tactic (tclIDTAC))) @@ -1418,7 +1418,7 @@ let com_terminate let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1474,8 +1474,7 @@ let (com_eqn : int -> Id.t -> (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evd - (EConstr.of_constr equation_lemma_type) - (Lemmas.mk_hook (fun _ _ -> ())); + (EConstr.of_constr equation_lemma_type); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fee469032c..06783de614 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; + Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism atts binders m s n = diff --git a/stm/stm.ml b/stm/stm.ml index 94405924b7..3444229735 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1543,7 +1543,7 @@ end = struct (* {{{ *) let pobject, _ = Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop @@ -1682,9 +1682,8 @@ end = struct (* {{{ *) `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) - Proof_global.set_terminator - (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + let opaque = Proof_global.Opaque in let proof = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in diff --git a/vernac/classes.ml b/vernac/classes.ml index 7d6bd1ca64..d0cf1c6bee 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -163,10 +163,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let hook = Obligations.mk_univ_hook hook in + let univ_hook = Obligations.mk_univ_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -176,7 +176,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) - (Lemmas.mk_hook + ~hook:(Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then @@ -423,8 +423,7 @@ let context poly l = | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let hook = Lemmas.mk_hook (fun _ _ -> ()) in - let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in + let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9c80f1d2f5..79d45880fc 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved env evd; ce -let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = +let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in @@ -108,8 +108,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in - let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in + let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls) else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook) + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 58007e6a88..0ac5762f71 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,9 +17,10 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> + ?hook:Lemmas.declaration_hook -> Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> - constr_expr option -> Lemmas.declaration_hook -> unit + constr_expr option -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 274c99107f..77227b64e6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -261,7 +261,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(false,indexes,init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -296,7 +296,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(true,[],init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index ebedfb1e0d..e62ae99159 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Obligations.mk_univ_hook (hook sigma) in + let univ_hook = Obligations.mk_univ_hook (hook sigma) in (* XXX: Grounding non-ground terms here... bad bad *) let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in @@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~hook) + evars_typ ctx evars ~univ_hook) let out_def = function | Some def -> def diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2fe03a8ec5..74b59735a9 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,7 +33,7 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ident (local, p, k) ce pl imps hook = +let declare_definition ident (local, p, k) ?hook ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> @@ -49,8 +49,8 @@ let declare_definition ident (local, p, k) ce pl imps hook = in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in - Lemmas.call_hook fix_exn hook local gr; gr + Lemmas.call_hook ~fix_exn ?hook local gr; gr let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ())) + declare_definition f kind ce pl imps diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index da11d4d9c0..b5dacf9ea0 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -14,8 +14,9 @@ open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool val declare_definition : Id.t -> definition_kind -> + ?hook:Lemmas.declaration_hook -> Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> - Lemmas.declaration_hook -> GlobRef.t + GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> UnivNames.universe_binders -> Entries.constant_universes_entry -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 28e80a74aa..1a6eda446c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -36,11 +36,12 @@ module NamedDecl = Context.Named.Declaration type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit let mk_hook hook = hook -let call_hook fix_exn hook l c = - try hook l c +let call_hook ?hook ?fix_exn l c = + try Option.iter (fun hook -> hook l c) hook with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (fix_exn e) + let e = Option.cata (fun fix -> fix e) e fix_exn in + iraise e (* Support for mutually proved theorems *) @@ -202,7 +203,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = gr in definition_message id; - call_hook (fun exn -> exn) hook locality r + call_hook ?hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -288,7 +289,7 @@ let warn_let_as_axiom = (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let admit (id,k,e) pl hook () = +let admit ?hook (id,k,e) pl () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () @@ -296,16 +297,17 @@ let admit (id,k,e) pl hook () = in let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) pl; - call_hook (fun exn -> exn) hook Global (ConstRef kn) + call_hook ?hook Global (ConstRef kn) (* Starting a goal *) -let universe_proof_terminator compute_guard hook = +let universe_proof_terminator ?univ_hook compute_guard = let open Proof_global in make_terminator begin function | Admitted (id,k,pe,ctx) -> - admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); - Feedback.feedback Feedback.AddedAxiom + let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in + admit ?hook (id,k,pe) (UState.universe_binders ctx) (); + Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> let is_opaque, export_seff = match opaque with | Transparent -> false, true @@ -315,13 +317,15 @@ let universe_proof_terminator compute_guard hook = let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - save ~export_seff id const universes compute_guard persistence (hook (Some universes)) + let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in + save ~export_seff id const universes compute_guard persistence hook | Proved (opaque,idopt, _ ) -> CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end -let standard_proof_terminator compute_guard hook = - universe_proof_terminator compute_guard (fun _ -> hook) +let standard_proof_terminator ?hook compute_guard = + let univ_hook = Option.map (fun hook _ -> hook) hook in + universe_proof_terminator ?univ_hook compute_guard let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -331,10 +335,10 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = +let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = let terminator = match terminator with - | None -> standard_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook + | None -> standard_proof_terminator ?hook compute_guard + | Some terminator -> terminator ?hook compute_guard in let sign = match sign with @@ -344,10 +348,11 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let goals = [ Global.env_of_context sign , c ] in Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c = let terminator = match terminator with - | None -> universe_proof_terminator compute_guard hook - | Some terminator -> terminator compute_guard hook + | None -> + universe_proof_terminator ?univ_hook compute_guard + | Some terminator -> terminator ?univ_hook compute_guard in let sign = match sign with @@ -371,7 +376,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind sigma decl recguard thms snl hook = +let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> @@ -405,14 +410,14 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; - call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + call_hook ?hook strength ref) thms_data in + start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with | None -> p,(true,[]) | Some tac -> Proof.run_tactic Global.(env ()) tac p)) -let start_proof_com ?inference_hook kind thms hook = +let start_proof_com ?inference_hook ?hook kind thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -444,7 +449,7 @@ let start_proof_com ?inference_hook kind thms hook = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_proof_with_initialization kind evd decl recguard thms snl hook + start_proof_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 246d8cbe6d..3ac12d3b0b 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -12,41 +12,45 @@ open Names open Decl_kinds type declaration_hook + val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook -val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit +val call_hook : + ?hook:declaration_hook -> ?fix_exn:Future.fix_exn -> + Decl_kinds.locality -> GlobRef.t -> unit val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> EConstr.types -> + ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> - declaration_hook -> unit + ?hook:declaration_hook -> EConstr.types -> unit val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> EConstr.types -> + ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> - (UState.t option -> declaration_hook) -> unit + ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit val start_proof_com : ?inference_hook:Pretyping.inference_hook -> - goal_kind -> Vernacexpr.proof_expr list -> - declaration_hook -> unit + ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list -> + unit val start_proof_with_initialization : + ?hook:declaration_hook -> goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * - (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list - -> int list option -> declaration_hook -> unit + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> + int list option -> unit val universe_proof_terminator : + ?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> - (UState.t option -> declaration_hook) -> - Proof_global.proof_terminator + Proof_global.proof_terminator val standard_proof_terminator : - Proof_global.lemma_possible_guards -> declaration_hook -> - Proof_global.proof_terminator + ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> + Proof_global.proof_terminator val fresh_name_for_anonymous_theorem : unit -> Id.t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4926b8c3e1..f18227039f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -22,11 +22,12 @@ open Util type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit let mk_univ_hook f = f -let call_univ_hook fix_exn hook uctx trans l c = - try hook uctx trans l c +let call_univ_hook ?univ_hook ?fix_exn uctx trans l c = + try Option.iter (fun hook -> hook uctx trans l c) univ_hook with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (fix_exn e) + let e = Option.cata (fun fix -> fix e) e fix_exn in + iraise e module NamedDecl = Context.Named.Declaration @@ -320,7 +321,7 @@ type program_info_aux = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : univ_declaration_hook; + prg_hook : univ_declaration_hook option; prg_opaque : bool; prg_sign: named_context_val; } @@ -481,9 +482,9 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in + let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx obls l r ; ())) + prg.prg_kind ce ubinders prg.prg_implicits ~hook let rec lam_index n t acc = match Constr.kind t with @@ -564,7 +565,7 @@ let declare_mutual_definition l = List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - call_univ_hook fix_exn first.prg_hook first.prg_ctx obls local gr; + call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; List.iter progmap_remove l; gr let decompose_lam_prod c ty = @@ -662,8 +663,8 @@ let declare_obligation prg obl body ty uctx = in true, { obl with obl_body = body } -let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind - notations obls impls kind reduce hook = +let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind + notations obls impls kind reduce = let obls', b = match b with | None -> @@ -688,7 +689,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; prg_opaque = opaque; + prg_hook = univ_hook; prg_opaque = opaque; prg_sign = sign } let map_cardinal m = @@ -843,9 +844,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator name num guard hook auto pf = +let obligation_terminator ?univ_hook name num guard auto pf = let open Proof_global in - let term = Lemmas.universe_proof_terminator guard hook in + let term = Lemmas.universe_proof_terminator ?univ_hook guard in match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin @@ -968,11 +969,11 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator guard hook = + let terminator ?univ_hook guard = Proof_global.make_terminator - (obligation_terminator prg.prg_name num guard hook auto) in - let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in + (obligation_terminator ?univ_hook prg.prg_name num guard auto) in + let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac @@ -1109,10 +1110,10 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) obls = + ?(reduce=reduce) ?univ_hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -1129,13 +1130,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) notations fixkind = + ?univ_hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps kind reduce hook + notations obls imps kind reduce ?univ_hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 57040b3f7c..c670e3a3b5 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -14,8 +14,10 @@ open Evd open Names type univ_declaration_hook -val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook -val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit +val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> + univ_declaration_hook +val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn -> + UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof @@ -56,14 +58,14 @@ type progress = (* Resolution status of a program *) val default_tactic : unit Proofview.tactic ref -val add_definition : Names.Id.t -> ?term:constr -> types -> +val add_definition : Names.Id.t -> ?term:constr -> types -> UState.t -> ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> - ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress + ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -80,7 +82,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> - ?hook:univ_declaration_hook -> ?opaque:bool -> + ?univ_hook:univ_declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 39be6af179..f5d68a2199 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -492,7 +492,7 @@ let vernac_custom_entry ~module_local s = (***********) (* Gallina *) -let start_proof_and_print k l hook = +let start_proof_and_print ?hook k l = let inference_hook = if Flags.is_program_mode () then let hook env sigma ev = @@ -514,18 +514,16 @@ let start_proof_and_print k l hook = in Some hook else None in - start_proof_com ?inference_hook k l hook - -let no_hook = Lemmas.mk_hook (fun _ _ -> ()) + start_proof_com ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> - Class.add_coercion_hook p + Some (Class.add_coercion_hook p) | CanonicalStructure -> - Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure) + Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)) | SubClass -> - Class.add_subclass_hook p -| _ -> no_hook + Some (Class.add_subclass_hook p) +| _ -> None let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let open DefAttributes in @@ -549,7 +547,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) - [(CAst.make ?loc name, pl), (bl, t)] hook + ?hook [(CAst.make ?loc name, pl), (bl, t)] | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -557,7 +555,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in ComDefinition.do_definition ~program_mode name - (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) + (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook) let vernac_start_proof ~atts kind l = let open DefAttributes in @@ -565,7 +563,7 @@ let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook + start_proof_and_print (local, atts.polymorphic, Proof kind) l let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted |