aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/compat.ml473
-rw-r--r--parsing/egramcoq.ml151
-rw-r--r--parsing/egramcoq.mli35
-rw-r--r--parsing/egramml.ml75
-rw-r--r--parsing/egramml.mli20
-rw-r--r--parsing/entry.ml30
-rw-r--r--parsing/entry.mli23
-rw-r--r--parsing/g_constr.ml464
-rw-r--r--parsing/g_ltac.ml4260
-rw-r--r--parsing/g_prim.ml47
-rw-r--r--parsing/g_proofs.ml414
-rw-r--r--parsing/g_tactic.ml4149
-rw-r--r--parsing/g_vernac.ml4177
-rw-r--r--parsing/highparsing.mllib2
-rw-r--r--parsing/lexer.ml477
-rw-r--r--parsing/lexer.mli4
-rw-r--r--parsing/parsing.mllib1
-rw-r--r--parsing/pcoq.ml (renamed from parsing/pcoq.ml4)501
-rw-r--r--parsing/pcoq.mli88
-rw-r--r--parsing/tok.ml33
-rw-r--r--parsing/tok.mli5
21 files changed, 763 insertions, 1026 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index eba1d2b8f..c482c694e 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -238,6 +238,69 @@ end
END
+(** Some definitions are grammar-specific in Camlp4, so we use a functor to
+ depend on it while taking a dummy argument in Camlp5. *)
+
+module GramextMake (G : GrammarSig) :
+sig
+ val stoken : Tok.t -> G.symbol
+ val sself : G.symbol
+ val snext : G.symbol
+ val slist0 : G.symbol -> G.symbol
+ val slist0sep : G.symbol * G.symbol -> G.symbol
+ val slist1 : G.symbol -> G.symbol
+ val slist1sep : G.symbol * G.symbol -> G.symbol
+ val sopt : G.symbol -> G.symbol
+ val snterml : G.internal_entry * string -> G.symbol
+ val snterm : G.internal_entry -> G.symbol
+ val snterml_level : G.symbol -> string
+end =
+struct
+
+IFDEF CAMLP5 THEN
+ let stoken tok =
+ let pattern = match tok with
+ | Tok.KEYWORD s -> "", s
+ | Tok.IDENT s -> "IDENT", s
+ | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
+ | Tok.FIELD s -> "FIELD", s
+ | Tok.INT s -> "INT", s
+ | Tok.INDEX s -> "INDEX", s
+ | Tok.STRING s -> "STRING", s
+ | Tok.LEFTQMARK -> "LEFTQMARK", ""
+ | Tok.BULLET s -> "BULLET", s
+ | Tok.EOI -> "EOI", ""
+ in
+ Gramext.Stoken pattern
+ELSE
+ module Gramext = G
+ let stoken tok = match tok with
+ | Tok.KEYWORD s -> Gramext.Skeyword s
+ | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok)
+END
+
+IFDEF CAMLP5_6_00 THEN
+ let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
+ let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
+ELSE
+ let slist0sep (x, y) = Gramext.Slist0sep (x, y)
+ let slist1sep (x, y) = Gramext.Slist1sep (x, y)
+END
+
+ let snterml (x, y) = Gramext.Snterml (x, y)
+ let snterm x = Gramext.Snterm x
+ let sself = Gramext.Sself
+ let snext = Gramext.Snext
+ let slist0 x = Gramext.Slist0 x
+ let slist1 x = Gramext.Slist1 x
+ let sopt x = Gramext.Sopt x
+
+ let snterml_level = function
+ | Gramext.Snterml (_, l) -> l
+ | _ -> failwith "snterml_level"
+
+end
+
(** Misc functional adjustments *)
@@ -323,3 +386,11 @@ let qualified_name loc path name =
let path = List.fold_right fold path (Ast.IdLid (loc, name)) in
Ast.ExId (loc, path)
END
+
+IFDEF CAMLP5 THEN
+let warning_verbose = Gramext.warning_verbose
+ELSE
+(* TODO: this is a workaround, since there isn't such
+ [warning_verbose] in new camlp4. *)
+let warning_verbose = ref true
+END
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index d9eb5d412..f0c12ab8e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -167,10 +167,9 @@ let rec make_constr_prod_item assoc from forpat = function
[]
let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
- let entry =
- if forpat then weaken_entry Constr.pattern
- else weaken_entry Constr.operconstr in
- grammar_extend entry reinit (pos,[(name, p4assoc, [])])
+ let empty = (pos, [(name, p4assoc, [])]) in
+ if forpat then grammar_extend Constr.pattern reinit empty
+ else grammar_extend Constr.operconstr reinit empty
let pure_sublevels level symbs =
let filter s =
@@ -189,13 +188,10 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
let symbs = make_constr_prod_item assoc n forpat pt in
let pure_sublevels = pure_sublevels level symbs in
let needed_levels = register_empty_levels forpat pure_sublevels in
- let map_level (pos, ass1, name, ass2) =
- (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in
- let needed_levels = List.map map_level needed_levels in
let pos,p4assoc,name,reinit = find_position forpat assoc level in
let nb_decls = List.length needed_levels + 1 in
List.iter (prepare_empty_levels forpat) needed_levels;
- grammar_extend entry reinit (Option.map of_coq_position pos,
+ unsafe_grammar_extend entry reinit (Option.map of_coq_position pos,
[(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
nb_decls) 0 rules
@@ -210,109 +206,59 @@ type notation_grammar = {
let extend_constr_constr_notation ng =
let level = ng.notgram_level in
let mkact loc env = CNotation (loc, ng.notgram_notation, env) in
- let e = interp_constr_entry_key false (ETConstr (level, ())) in
+ let e = interp_constr_entry_key false level in
let ext = (ETConstr (level, ()), ng.notgram_assoc) in
extend_constr e ext (make_constr_action mkact) false ng.notgram_prods
let extend_constr_pat_notation ng =
let level = ng.notgram_level in
let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in
- let e = interp_constr_entry_key true (ETConstr (level, ())) in
+ let e = interp_constr_entry_key true level in
let ext = ETConstr (level, ()), ng.notgram_assoc in
extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
-let extend_constr_notation ng =
+let extend_constr_notation (_, ng) =
(* Add the notation in constr *)
let nb = extend_constr_constr_notation ng in
(* Add the notation in cases_pattern *)
let nb' = extend_constr_pat_notation ng in
nb + nb'
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level) *)
-
-let get_tactic_entry n =
- if Int.equal n 0 then
- weaken_entry Tactic.simple_tactic, None
- else if Int.equal n 5 then
- weaken_entry Tactic.binder_tactic, None
- else if 1<=n && n<5 then
- weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
- else
- error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
-
-(**********************************************************************)
-(** State of the grammar extensions *)
-
-type tactic_grammar = {
- tacgram_level : int;
- tacgram_prods : grammar_prod_item list;
-}
-
-type all_grammar_command =
- | Notation of Notation.level * notation_grammar
- | TacticGrammar of KerName.t * tactic_grammar
- | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
-(** ML Tactic grammar extensions *)
-
-let add_ml_tactic_entry name prods =
- let entry = weaken_entry Tactic.simple_tactic in
- let mkact i loc l : raw_tactic_expr =
- let open Tacexpr in
- let entry = { mltac_name = name; mltac_index = i } in
- TacML (loc, entry, List.map snd l)
- in
- let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
- synchronize_level_positions ();
- grammar_extend entry None (None ,[(None, None, List.rev rules)]);
- 1
+let grammar_interp = ref GrammarInterpMap.empty
-(* Declaration of the tactic grammar rule *)
+let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
+type 'a grammar_command = 'a GrammarCommand.tag
-(** Tactic grammar extensions *)
+let create_grammar_command name interp : _ grammar_command =
+ let obj = GrammarCommand.create name in
+ let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+ obj
-let add_tactic_entry kn tg =
- let entry, pos = get_tactic_entry tg.tacgram_level in
- let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in
- let () =
- if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
- error "Notation for simple tactic must start with an identifier."
- in
- let rules = make_rule mkact tg.tacgram_prods in
- synchronize_level_positions ();
- grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
- 1
-
-let (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
- let nb = match gram with
- | Notation (_,a) -> extend_constr_notation a
- | TacticGrammar (kn, g) -> add_tactic_entry kn g
- | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
- in
- grammar_state := (nb,gram) :: !grammar_state
+let extend_grammar tag g =
+ let nb = GrammarInterpMap.find tag !grammar_interp g in
+ grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
-let extend_constr_grammar pr ntn =
- extend_grammar (Notation (pr, ntn))
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
-let extend_tactic_grammar kn ntn =
- extend_grammar (TacticGrammar (kn, ntn))
+let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+ create_grammar_command "Notation" extend_constr_notation
-let extend_ml_tactic_grammar name ntn =
- extend_grammar (MLTacticGrammar (name, ntn))
+let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
let recover_constr_grammar ntn prec =
- let filter = function
- | _, Notation (prec', ng) when
- Notation.level_eq prec prec' &&
- String.equal ntn ng.notgram_notation -> Some ng
- | _ -> None
+ let filter (_, gram) : notation_grammar option = match gram with
+ | GrammarCommand.Dyn (tag, obj) ->
+ match GrammarCommand.eq tag constr_grammar with
+ | None -> None
+ | Some Refl ->
+ let (prec', ng) = obj in
+ if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+ else None
in
match List.map_filter filter !grammar_state with
| [x] -> x
@@ -321,7 +267,7 @@ let recover_constr_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
@@ -340,7 +286,7 @@ let unfreeze (grams, lex) =
remove_levels n;
grammar_state := common;
Lexer.unfreeze lex;
- List.iter extend_grammar (List.rev_map snd redo)
+ List.iter extend_dyn_grammar (List.rev_map snd redo)
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
@@ -360,30 +306,3 @@ let with_grammar_rule_protection f x =
let reraise = Errors.push reraise in
let () = unfreeze fs in
iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations *)
-
-let ltac_quotations = ref String.Set.empty
-
-let create_ltac_quotation name cast wit e =
- let () =
- if String.Set.mem name !ltac_quotations then
- failwith ("Ltac quotation " ^ name ^ " already registered")
- in
- let () = ltac_quotations := String.Set.add name !ltac_quotations in
-(* let level = Some "1" in *)
- let level = None in
- let assoc = Some (of_coq_assoc Extend.RightA) in
- let rule = [
- gram_token_of_string name;
- gram_token_of_string ":";
- symbol_of_prod_entry_key (Agram (Gram.Entry.name e));
- ] in
- let action v _ _ loc =
- let loc = !@loc in
- let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in
- TacArg (loc, arg)
- in
- let gram = (level, assoc, [rule, Gram.action action]) in
- maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 2b0f7da8c..6ec106626 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -36,34 +36,27 @@ type notation_grammar = {
notgram_typs : notation_var_internalization_type list;
}
-type tactic_grammar = {
- tacgram_level : int;
- tacgram_prods : grammar_prod_item list;
-}
+(** {5 Extending the parser with Summary-synchronized commands} *)
+
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+ marshallable. *)
+
+val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The function
+ should modify the parser state and return the number of grammar extensions
+ performed. *)
+
+val extend_grammar : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
(** {5 Adding notations} *)
val extend_constr_grammar : Notation.level -> notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
- tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
- TacML tactic with the provided string as name. *)
-
val recover_constr_grammar : notation -> Notation.level -> notation_grammar
(** For a declared grammar, returns the rule + the ordered entry types
of variables in the rule (for use in the interpretation) *)
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) ->
- ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit
-(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is,
- Ltac grammar now accepts arguments of the form ["name" ":" <e>], and
- generates a generic argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 8fe03b363..37fccdb3c 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,39 +9,60 @@
open Util
open Compat
open Names
+open Extend
open Pcoq
open Genarg
open Vernacexpr
-(** Making generic actions in type generic_argument *)
-
-let make_generic_action
- (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
- let rec make env = function
- | [] ->
- Gram.action (fun loc -> f (to_coqloc loc) env)
- | None :: tl -> (* parse a non-binding item *)
- Gram.action (fun _ -> make env tl)
- | Some (p, t) :: tl -> (* non-terminal *)
- Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in
- make [] (List.rev pil)
-
(** Grammar extensions declared at ML level *)
-type grammar_prod_item =
+type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal of
- Loc.t * argument_type * prod_entry_key * Id.t option
+ | GramNonTerminal :
+ Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+
+type 'a ty_arg = ('a -> raw_generic_argument)
+
+type ('self, _, 'r) ty_rule =
+| TyStop : ('self, 'r, 'r) ty_rule
+| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option ->
+ ('self, 'b -> 'a, 'r) ty_rule
+
+type ('self, 'r) any_ty_rule =
+| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+
+let rec ty_rule_of_gram = function
+| [] -> AnyTyRule TyStop
+| GramTerminal s :: rem ->
+ let AnyTyRule rem = ty_rule_of_gram rem in
+ let tok = Atoken (Lexer.terminal s) in
+ let r = TyNext (rem, tok, None) in
+ AnyTyRule r
+| GramNonTerminal (_, t, tok) :: rem ->
+ let AnyTyRule rem = ty_rule_of_gram rem in
+ let inj = Some (fun obj -> Genarg.in_gen t obj) in
+ let r = TyNext (rem, tok, inj) in
+ AnyTyRule r
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+| TyStop -> Extend.Stop
+| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
+
+type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
-let make_prod_item = function
- | GramTerminal s -> (gram_token_of_string s, None)
- | GramNonTerminal (_,t,e,po) ->
- (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
+let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+| TyStop -> fun f loc -> f loc []
+| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
+| TyNext (rem, tok, Some inj) -> fun f x ->
+ let f loc args = f loc (inj x :: args) in
+ ty_eval rem f
-let make_rule mkact pt =
- let (symbs,ntl) = List.split (List.map make_prod_item pt) in
- let act = make_generic_action mkact ntl in
- (symbs, act)
+let make_rule f prod =
+ let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in
+ let symb = ty_erase ty_rule in
+ let f loc l = f loc (List.rev l) in
+ let act = ty_eval ty_rule f in
+ Extend.Rule (symb, act)
(** Vernac grammar extensions *)
@@ -58,6 +79,6 @@ let get_extend_vernac_rule (s, i) =
let extend_vernac_command_grammar s nt gl =
let nt = Option.default Vernac_.command nt in
vernac_exts := (s,gl) :: !vernac_exts;
- let mkact loc l = VernacExtend (s,List.map snd l) in
+ let mkact loc l = VernacExtend (s, l) in
let rules = [make_rule mkact gl] in
- maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
+ grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 9ebb5b83b..1ad947200 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -1,29 +1,31 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Vernacexpr
+
(** Mapping of grammar productions to camlp4 actions. *)
(** This is the part specific to vernac extensions.
For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
-type grammar_prod_item =
+type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal of Loc.t * Genarg.argument_type *
- Pcoq.prod_entry_key * Names.Id.t option
+ | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+ ('s, 'a) Extend.symbol -> 's grammar_prod_item
val extend_vernac_command_grammar :
- Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
- grammar_prod_item list -> unit
+ Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+ vernac_expr grammar_prod_item list -> unit
-val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list
+val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
(** Utility function reused in Egramcoq : *)
val make_rule :
- (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) ->
- grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
+ (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
+ 'a grammar_prod_item list -> 'a Extend.production_rule
diff --git a/parsing/entry.ml b/parsing/entry.ml
new file mode 100644
index 000000000..b7c6c23fa
--- /dev/null
+++ b/parsing/entry.ml
@@ -0,0 +1,30 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Errors
+open Util
+
+type 'a t = string
+
+(** Entries are registered with a unique name *)
+
+let entries = ref String.Set.empty
+
+let create name =
+ let () =
+ if String.Set.mem name !entries then
+ anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
+ in
+ let () = entries := String.Set.add name !entries in
+ name
+
+let unsafe_of_name name =
+ assert (String.Set.mem name !entries);
+ name
+
+let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
new file mode 100644
index 000000000..4c73fe204
--- /dev/null
+++ b/parsing/entry.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Typed grammar entries *)
+
+type 'a t
+(** Typed grammar entries. We need to defined them here so that they are
+ marshallable and defined before the Pcoq.Gram module. They are basically
+ unique names. They should be kept synchronized with the {!Pcoq} entries. *)
+
+val create : string -> 'a t
+(** Create an entry. They should be synchronized with the entries defined in
+ {!Pcoq}. *)
+
+(** {5 Meta-programming} *)
+
+val repr : 'a t -> string
+val unsafe_of_name : string -> 'a t
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e47e3fb1e..7e470e844 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -132,10 +132,7 @@ GEXTEND Gram
closed_binder open_binders binder binders binders_fixannot
record_declaration typeclass_constraint pattern appl_arg;
Constr.ident:
- [ [ id = Prim.ident -> id
-
- (* This is used in quotations and Syntax *)
- | id = METAIDENT -> Id.of_string id ] ]
+ [ [ id = Prim.ident -> id ] ]
;
Prim.name:
[ [ "_" -> (!@loc, Anonymous) ] ]
@@ -153,12 +150,12 @@ GEXTEND Gram
[ [ "Set" -> GSet
| "Prop" -> GProp
| "Type" -> GType []
- | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+ | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
] ]
;
universe:
- [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
- | id = ident -> [id]
+ [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
+ | id = identref -> [id]
] ]
;
lconstr:
@@ -218,17 +215,23 @@ GEXTEND Gram
CGeneralization (!@loc, Implicit, None, c)
| "`("; c = operconstr LEVEL "200"; ")" ->
CGeneralization (!@loc, Explicit, None, c)
- | "$("; tac = Tactic.tactic; ")$" ->
+ | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" ->
let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
CHole (!@loc, None, IntroAnonymous, Some arg)
] ]
;
record_declaration:
- [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
-(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
-(* CRecord (!@loc, Some c, fs) *)
+ [ [ fs = record_fields -> CRecord (!@loc, fs) ] ]
+ ;
+
+ record_fields:
+ [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
+ | f = record_field_declaration; ";" -> [f]
+ | f = record_field_declaration -> [f]
+ | -> []
] ]
;
+
record_field_declaration:
[ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
(id, abstract_constr_expr c (binders_of_lidents params)) ] ]
@@ -258,14 +261,14 @@ GEXTEND Gram
CLetTuple (!@loc,lb,po,c1,c2)
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)])
+ CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)])
+ CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)])
+ CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -302,7 +305,7 @@ GEXTEND Gram
[ [ "Set" -> GSet
| "Prop" -> GProp
| "Type" -> GType None
- | id = ident -> GType (Some (Id.to_string id))
+ | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
] ]
;
fix_constr:
@@ -329,11 +332,10 @@ GEXTEND Gram
br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ]
;
case_item:
- [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
- ;
- pred_pattern:
- [ [ ona = OPT ["as"; id=name -> id];
- ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ]
+ [ [ c=operconstr LEVEL "100";
+ ona = OPT ["as"; id=name -> id];
+ ty = OPT ["in"; t=pattern -> t] ->
+ (c,ona,ty) ] ]
;
case_type:
[ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
@@ -356,9 +358,16 @@ GEXTEND Gram
[ [ pll = LIST1 mult_pattern SEP "|";
"=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
;
- recordpattern:
+ record_pattern:
[ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
;
+ record_patterns:
+ [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
+ | p = record_pattern; ";" -> [p]
+ | p = record_pattern-> [p]
+ | -> []
+ ] ]
+ ;
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
@@ -370,19 +379,22 @@ GEXTEND Gram
| "10" RIGHTA
[ p = pattern; lp = LIST1 NEXT ->
(match p with
- | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
+ | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
+ | CPatCstr (_, r, None, l2) -> Errors.user_err_loc
+ (cases_pattern_expr_loc p, "compound_pattern",
+ Pp.str "Nested applications not supported.")
| CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
| CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
| _ -> Errors.user_err_loc
(cases_pattern_expr_loc p, "compound_pattern",
Pp.str "Such pattern cannot have arguments."))
- |"@"; r = Prim.reference; lp = LIST1 NEXT ->
- CPatCstr (!@loc, r, lp, []) ]
+ |"@"; r = Prim.reference; lp = LIST0 NEXT ->
+ CPatCstr (!@loc, r, Some lp, []) ]
| "1" LEFTA
[ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
| "0"
[ r = Prim.reference -> CPatAtom (!@loc,Some r)
- | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+ | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
| "_" -> CPatAtom (!@loc,None)
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
deleted file mode 100644
index a4dba506d..000000000
--- a/parsing/g_ltac.ml4
+++ /dev/null
@@ -1,260 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Compat
-open Constrexpr
-open Tacexpr
-open Misctypes
-open Genarg
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-open Pcoq
-open Pcoq.Prim
-open Pcoq.Tactic
-
-let fail_default_value = ArgArg 0
-
-let arg_of_expr = function
- TacArg (loc,a) -> a
- | e -> Tacexp (e:raw_tactic_expr)
-
-let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
-let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
-
-(* Tactics grammar rules *)
-
-GEXTEND Gram
- GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
- constr_may_eval constr_eval;
-
- tactic_then_last:
- [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
- Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
- | -> [||]
- ] ]
- ;
- tactic_then_gen:
- [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
- | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
- | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
- | ta = tactic_expr -> ([ta], None)
- | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
- | -> ([TacId []], None)
- ] ]
- ;
- tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
- for [TacExtend] *)
- [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ]
- ;
- tactic_expr:
- [ "5" RIGHTA
- [ te = binder_tactic -> te ]
- | "4" LEFTA
- [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
- | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1)
- | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" ->
- match l , tail with
- | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
- | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
- | false , None -> TacThen (ta0,TacDispatch first)
- | true , None -> TacThens (ta0,first) ]
- | "3" RIGHTA
- [ IDENT "try"; ta = tactic_expr -> TacTry ta
- | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
- | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
- | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta)
- | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
- | IDENT "progress"; ta = tactic_expr -> TacProgress ta
- | IDENT "once"; ta = tactic_expr -> TacOnce ta
- | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
- | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
-(*To do: put Abstract in Refiner*)
- | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
- | IDENT "abstract"; tc = NEXT; "using"; s = ident ->
- TacAbstract (tc,Some s) ]
-(*End of To do*)
- | "2" RIGHTA
- [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
- | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1)
- | IDENT "tryif" ; ta = tactic_expr ;
- "then" ; tat = tactic_expr ;
- "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae)
- | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
- | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
- | "1" RIGHTA
- [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
- TacMatchGoal (b,false,mrl)
- | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
- mrl = match_context_list; "end" ->
- TacMatchGoal (b,true,mrl)
- | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
- TacMatch (b,c,mrl)
- | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
- TacFirst l
- | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
- TacSolve l
- | IDENT "idtac"; l = LIST0 message_token -> TacId l
- | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ];
- l = LIST0 message_token -> TacFail (g,n,l)
- | st = simple_tactic -> st
- | IDENT "constr"; ":"; c = Constr.constr ->
- TacArg(!@loc,ConstrMayEval(ConstrTerm c))
- | a = tactic_top_or_arg -> TacArg(!@loc,a)
- | r = reference; la = LIST0 tactic_arg ->
- TacArg(!@loc,TacCall (!@loc,r,la)) ]
- | "0"
- [ "("; a = tactic_expr; ")" -> a
- | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
- begin match tail with
- | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
- | None -> TacDispatch tf
- end
- | a = tactic_atom -> TacArg (!@loc,a) ] ]
- ;
- failkw:
- [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
- ;
- (* binder_tactic: level 5 of tactic_expr *)
- binder_tactic:
- [ RIGHTA
- [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
- TacFun (it,body)
- | "let"; isrec = [IDENT "rec" -> true | -> false];
- llc = LIST1 let_clause SEP "with"; "in";
- body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body)
- | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
- ;
- (* Tactic arguments *)
- tactic_arg:
- [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
- | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
- | a = tactic_top_or_arg -> a
- | r = reference -> Reference r
- | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
- (* Unambigous entries: tolerated w/o "ltac:" modifier *)
- | id = METAIDENT -> MetaIdArg (!@loc,true,id)
- | "()" -> TacGeneric (genarg_of_unit ()) ] ]
- ;
- (* Can be used as argument and at toplevel in tactic expressions. *)
- tactic_top_or_arg:
- [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c
- | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
- TacGeneric (genarg_of_ipattern ipat)
- | c = constr_eval -> ConstrMayEval c
- | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
- | IDENT "type_term"; c=uconstr -> TacPretype c
- | IDENT "numgoals" -> TacNumgoals ] ]
- ;
- (* If a qualid is given, use its short name. TODO: have the shortest
- non ambiguous name where dots are replaced by "_"? Probably too
- verbose most of the time. *)
- fresh_id:
- [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
- | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ]
- ;
- constr_eval:
- [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
- ConstrEval (rtc,c)
- | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
- ConstrContext (id,c)
- | IDENT "type"; IDENT "of"; c = Constr.constr ->
- ConstrTypeOf c ] ]
- ;
- constr_may_eval: (* For extensions *)
- [ [ c = constr_eval -> c
- | c = Constr.constr -> ConstrTerm c ] ]
- ;
- tactic_atom:
- [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id)
- | n = integer -> TacGeneric (genarg_of_int n)
- | r = reference -> TacCall (!@loc,r,[])
- | "()" -> TacGeneric (genarg_of_unit ()) ] ]
- ;
- match_key:
- [ [ "match" -> Once
- | "lazymatch" -> Select
- | "multimatch" -> General ] ]
- ;
- input_fun:
- [ [ "_" -> None
- | l = ident -> Some l ] ]
- ;
- let_clause:
- [ [ id = identref; ":="; te = tactic_expr ->
- (id, arg_of_expr te)
- | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
- (id, arg_of_expr (TacFun(args,te))) ] ]
- ;
- match_pattern:
- [ [ IDENT "context"; oid = OPT Constr.ident;
- "["; pc = Constr.lconstr_pattern; "]" ->
- let mode = not (!Flags.tactic_context_compat) in
- Subterm (mode, oid, pc)
- | IDENT "appcontext"; oid = OPT Constr.ident;
- "["; pc = Constr.lconstr_pattern; "]" ->
- msg_warning (strbrk "appcontext is deprecated");
- Subterm (true,oid, pc)
- | pc = Constr.lconstr_pattern -> Term pc ] ]
- ;
- match_hyps:
- [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp)
- | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt)
- | na = name; ":="; mpv = match_pattern ->
- let t, ty =
- match mpv with
- | Term t -> (match t with
- | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
- | _ -> mpv, None)
- | _ -> mpv, None
- in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
- ] ]
- ;
- match_context_rule:
- [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "=>"; te = tactic_expr -> Pat (largs, mp, te)
- | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
- | "_"; "=>"; te = tactic_expr -> All te ] ]
- ;
- match_context_list:
- [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
- | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
- ;
- match_rule:
- [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
- | "_"; "=>"; te = tactic_expr -> All te ] ]
- ;
- match_list:
- [ [ mrl = LIST1 match_rule SEP "|" -> mrl
- | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
- ;
- message_token:
- [ [ id = identref -> MsgIdent id
- | s = STRING -> MsgString s
- | n = integer -> MsgInt n ] ]
- ;
-
- ltac_def_kind:
- [ [ ":=" -> false
- | "::=" -> true ] ]
- ;
-
- (* Definitions for tactics *)
- tacdef_body:
- [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
- (name, redef, TacFun (it, body))
- | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
- (name, redef, body) ] ]
- ;
- tactic:
- [ [ tac = tactic_expr -> tac ] ]
- ;
- END
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 84da9c424..5e67e9957 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -32,7 +32,7 @@ let my_int_of_string loc s =
GEXTEND Gram
GLOBAL:
- bigint natural integer identref name ident var preident
+ bigint natural index integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
ne_string string pattern_ident pattern_identref by_notation smart_global;
preident:
@@ -113,6 +113,9 @@ GEXTEND Gram
natural:
[ [ i = INT -> my_int_of_string (!@loc) i ] ]
;
+ index:
+ [ [ i = INDEX -> my_int_of_string (!@loc) i ] ]
+ ;
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> (Bigint.of_string i) ] ]
;
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16b..422384f3d 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -37,12 +37,12 @@ GEXTEND Gram
command:
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
| IDENT "Proof" ->
- VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+ VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; "with"; ta = tactic;
- l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
- VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
- | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+ l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+ VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+ | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
ta = OPT [ "with"; ta = tactic -> ta ] ->
VernacProof (ta,Some l)
| IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -73,8 +73,10 @@ GEXTEND Gram
| IDENT "Unfocused" -> VernacUnfocused
| IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
| IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
+ | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
+ | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
| IDENT "Show"; IDENT "Goal"; n = string ->
- VernacShow (ShowGoal (GoalId n))
+ VernacShow (ShowGoal (GoalUid n))
| IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
VernacShow (ShowGoalImplicitly n)
| IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 69593f993..0c90a8bca 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -44,6 +44,20 @@ let test_lpar_id_coloneq =
| _ -> err ())
| _ -> err ())
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+ Gram.Entry.of_parser "lpar_id_coloneq"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ")" -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
Gram.Entry.of_parser "test_lpar_idnum_coloneq"
@@ -217,15 +231,16 @@ GEXTEND Gram
[ [ id = identref -> id ] ]
;
open_constr:
- [ [ c = constr -> ((),c) ] ]
+ [ [ c = constr -> c ] ]
;
uconstr:
[ [ c = constr -> c ] ]
;
induction_arg:
[ [ n = natural -> (None,ElimOnAnonHyp n)
- | c = constr_with_bindings -> (None,induction_arg_of_constr c)
- | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c)
+ | test_lpar_id_rpar; c = constr_with_bindings ->
+ (Some false,induction_arg_of_constr c)
+ | c = constr_with_bindings_arg -> on_snd induction_arg_of_constr c
] ]
;
constr_with_bindings_arg:
@@ -266,19 +281,23 @@ GEXTEND Gram
intropatterns:
[ [ l = LIST0 nonsimple_intropattern -> l ]]
;
+ ne_intropatterns:
+ [ [ l = LIST1 nonsimple_intropattern -> l ]]
+ ;
or_and_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc
- | "()" -> [[]]
- | "("; si = simple_intropattern; ")" -> [[si]]
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
+ | "()" -> IntroAndPattern []
+ | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
| "("; si = simple_intropattern; ",";
- tc = LIST1 simple_intropattern SEP "," ; ")" -> [si::tc]
+ tc = LIST1 simple_intropattern SEP "," ; ")" ->
+ IntroAndPattern (si::tc)
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
- | ([]|[_]|[_;_]) as l -> [l]
- | t::q -> [[t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (pairify q)))]]
- in pairify (si::tc) ] ]
+ | ([]|[_]|[_;_]) as l -> l
+ | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+ in IntroAndPattern (pairify (si::tc)) ] ]
;
equality_intropattern:
[ [ "->" -> IntroRewrite true
@@ -296,11 +315,18 @@ GEXTEND Gram
| "**" -> !@loc, IntroForthcoming false ]]
;
simple_intropattern:
+ [ [ pat = simple_intropattern_closed;
+ l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
+ let loc0,pat = pat in
+ let f c pat =
+ let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
+ IntroAction (IntroApplyOn (c,(loc,pat))) in
+ !@loc, List.fold_right f l pat ] ]
+ ;
+ simple_intropattern_closed:
[ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
| pat = equality_intropattern -> !@loc, IntroAction pat
| "_" -> !@loc, IntroAction IntroWildcard
- | pat = simple_intropattern; "/"; c = constr ->
- !@loc, IntroAction (IntroApplyOn (c,pat))
| pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
;
simple_binding:
@@ -339,21 +365,6 @@ GEXTEND Gram
| d = delta_flag -> all_with d
] ]
;
- red_tactic:
- [ [ IDENT "red" -> Red false
- | IDENT "hnf" -> Hnf
- | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
- | IDENT "cbv"; s = strategy_flag -> Cbv s
- | IDENT "cbn"; s = strategy_flag -> Cbn s
- | IDENT "lazy"; s = strategy_flag -> Lazy s
- | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
- | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
- | IDENT "fold"; cl = LIST1 constr -> Fold cl
- | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
- ;
- (* This is [red_tactic] including possible extensions *)
red_expr:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
@@ -414,7 +425,7 @@ GEXTEND Gram
| -> [] ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
| -> None ] ]
;
orient:
@@ -443,25 +454,6 @@ GEXTEND Gram
[ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
;
- hintbases:
- [ [ "with"; "*" -> None
- | "with"; l = LIST1 [ x = IDENT -> x] -> Some l
- | -> Some [] ] ]
- ;
- auto_using:
- [ [ "using"; l = LIST1 constr SEP "," -> l
- | -> [] ] ]
- ;
- trivial:
- [ [ IDENT "trivial" -> Off
- | IDENT "info_trivial" -> Info
- | IDENT "debug"; IDENT "trivial" -> Debug ] ]
- ;
- auto:
- [ [ IDENT "auto" -> Off
- | IDENT "info_auto" -> Info
- | IDENT "debug"; IDENT "auto" -> Debug ] ]
- ;
eliminator:
[ [ "using"; el = constr_with_bindings -> el ] ]
;
@@ -502,12 +494,12 @@ GEXTEND Gram
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
rewriter :
- [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c))
+ [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
| ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
- | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c))
+ | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
| n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
| n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
- | c = constr_with_bindings -> (Precisely 1, (None,c))
+ | c = constr_with_bindings_arg -> (Precisely 1, c)
] ]
;
oriented_rewriter :
@@ -535,7 +527,10 @@ GEXTEND Gram
simple_tactic:
[ [
(* Basic tactics *)
- IDENT "intros"; pl = intropatterns -> TacAtom (!@loc, TacIntroPattern pl)
+ IDENT "intros"; pl = ne_intropatterns ->
+ TacAtom (!@loc, TacIntroPattern pl)
+ | IDENT "intros" ->
+ TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
| IDENT "intro"; id = ident; hto = move_location ->
TacAtom (!@loc, TacIntroMove (Some id, hto))
| IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
@@ -560,12 +555,8 @@ GEXTEND Gram
TacAtom (!@loc, TacElim (true,cl,el))
| IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
| IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
- | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n))
- | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n))
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
- | "cofix" -> TacAtom (!@loc, TacCofix None)
- | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id))
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
@@ -612,7 +603,6 @@ GEXTEND Gram
na = as_name;
l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
- | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c)
(* Derived basic tactics *)
| IDENT "induction"; ic = induction_clause_list ->
@@ -626,28 +616,9 @@ GEXTEND Gram
| IDENT "edestruct"; icl = induction_clause_list ->
TacAtom (!@loc, TacInductionDestruct(false,true,icl))
- (* Automation tactic *)
- | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
- | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacAuto (d,n,lems,db))
-
(* Context management *)
- | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
- | IDENT "clear"; l = LIST0 id_or_meta ->
- let is_empty = match l with [] -> true | _ -> false in
- TacAtom (!@loc, TacClear (is_empty, l))
- | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l)
- | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
- TacAtom (!@loc, TacMove (hfrom,hto))
| IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
- (* Constructors *)
- | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll))
- | IDENT "eexists"; bll = opt_bindings ->
- TacAtom (!@loc, TacSplit (true,bll))
- (* Equivalence relations *)
- | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl)
-
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
@@ -677,7 +648,31 @@ GEXTEND Gram
TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
(* Conversion *)
- | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
+ | IDENT "red"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Red false, cl))
+ | IDENT "hnf"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Hnf, cl))
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+ | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv s, cl))
+ | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbn s, cl))
+ | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Lazy s, cl))
+ | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvVm po, cl))
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvNative po, cl))
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Unfold ul, cl))
+ | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Fold l, cl))
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
let p,cl = merge_occurrences (!@loc) cl oc in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5a6dfa547..1c39858ea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -34,8 +34,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw
let query_command = Gram.entry_create "vernac:query_command"
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let noedit_mode = Gram.entry_create "vernac:noedit_command"
let subprf = Gram.entry_create "vernac:subprf"
let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -46,22 +44,7 @@ let record_field = Gram.entry_create "vernac:record_field"
let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
-
-let command_entry = ref noedit_mode
-let set_command_entry e = command_entry := e
-let get_command_entry () = !command_entry
-
-
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
- proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let set_tactic_mode () = set_command_entry tactic_mode
-let set_noedit_mode () = set_command_entry noedit_mode
-let _ = Proof_global.register_proof_mode {Proof_global.
- name = "Classic" ;
- set = set_tactic_mode ;
- reset = set_noedit_mode
- }
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
let make_bullet s =
let n = String.length s in
@@ -71,15 +54,11 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
-let default_command_entry =
- Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
-
GEXTEND Gram
- GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
+ GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
vernac: FIRST
- [ [ IDENT "Time"; l = vernac_list -> VernacTime l
- | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
+ [ [ IDENT "Time"; c = located_vernac -> VernacTime c
+ | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
| IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac -> VernacFail v
@@ -117,28 +96,13 @@ GEXTEND Gram
| c = subprf -> c
] ]
;
- vernac_list:
- [ [ c = located_vernac -> [c] ] ]
- ;
vernac_aux: LAST
- [ [ prfcom = default_command_entry -> prfcom ] ]
+ [ [ prfcom = command_entry -> prfcom ] ]
;
noedit_mode:
[ [ c = subgoal_command -> c None] ]
;
- selector:
- [ [ n=natural; ":" -> SelectNth n
- | "["; id = ident; "]"; ":" -> SelectId id
- | IDENT "all" ; ":" -> SelectAll
- | IDENT "par" ; ":" -> SelectAllParallel ] ]
- ;
-
- tactic_mode:
- [ [ gln = OPT selector;
- tac = subgoal_command -> tac gln ] ]
- ;
-
subprf:
[ [ s = BULLET -> VernacBullet (make_bullet s)
| "{" -> VernacSubproof None
@@ -153,26 +117,20 @@ GEXTEND Gram
| None -> c None
| _ ->
VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
- end
- | info = OPT [IDENT "Info";n=natural -> n];
- tac = Tactic.tactic;
- use_dft_tac = [ "." -> false | "..." -> true ] ->
- (fun g ->
- let g = Option.default (Proof_global.get_default_goal_selector ()) g in
- VernacSolve(g,info,tac,use_dft_tac)) ] ]
+ end ] ]
;
located_vernac:
[ [ v = vernac -> !@loc, v ] ]
;
END
-let test_plurial_form = function
+let test_plural_form = function
| [(_,([_],_))] ->
Flags.if_verbose msg_warning
(strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
| _ -> ()
-let test_plurial_form_types = function
+let test_plural_form_types = function
| [([_],_)] ->
Flags.if_verbose msg_warning
(strbrk "Keywords Implicit Types expect more than one type")
@@ -181,24 +139,24 @@ let test_plurial_form_types = function
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- record_field decl_notation rec_definition;
+ record_field decl_notation rec_definition pidentref;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
+ [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
l = LIST0
- [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
+ [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
(Some id,(bl,c,None)) ] ->
VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| stre = assumptions_token; nl = inline; bl = assum_list ->
- test_plurial_form bl;
+ test_plural_form bl;
VernacAssumption (stre, nl, bl)
- | d = def_token; id = identref; b = def_body ->
+ | d = def_token; id = pidentref; b = def_body ->
VernacDefinition (d, id, b)
| IDENT "Let"; id = identref; b = def_body ->
- VernacDefinition ((Some Discharge, Definition), id, b)
+ VernacDefinition ((Some Discharge, Definition), (id, None), b)
(* Gallina inductive declarations *)
| priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
@@ -257,6 +215,9 @@ GEXTEND Gram
| IDENT "Inline" -> DefaultInline
| -> NoInline] ]
;
+ pidentref:
+ [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
+ ;
univ_constraint:
[ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
r = identref -> (l, ord, r) ] ]
@@ -301,7 +262,7 @@ GEXTEND Gram
| -> RecordDecl (None, []) ] ]
;
inductive_definition:
- [ [ oc = opt_coercion; id = identref; indpar = binders;
+ [ [ oc = opt_coercion; id = pidentref; indpar = binders;
c = OPT [ ":"; c = lconstr -> c ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
@@ -311,9 +272,9 @@ GEXTEND Gram
| id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
Constructors ((c id)::l)
| id = identref ; c = constructor_type -> Constructors [ c id ]
- | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+ | cstr = identref; "{"; fs = record_fields; "}" ->
RecordDecl (Some cstr,fs)
- | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+ | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
| -> Constructors [] ] ]
;
(*
@@ -327,14 +288,14 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = identref;
+ [ [ id = pidentref;
bl = binders_fixannot;
ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = identref; bl = binders; ty = type_cstr;
+ [ [ id = pidentref; bl = binders; ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -375,6 +336,13 @@ GEXTEND Gram
[ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
ntn = decl_notation -> (bd,pri),ntn ] ]
;
+ record_fields:
+ [ [ f = record_field; ";"; fs = record_fields -> f :: fs
+ | f = record_field; ";" -> [f]
+ | f = record_field -> [f]
+ | -> []
+ ] ]
+ ;
record_binder_body:
[ [ l = binders; oc = of_type_with_opt_coercion;
t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
@@ -399,7 +367,7 @@ GEXTEND Gram
[ [ "("; a = simple_assum_coe; ")" -> a ] ]
;
simple_assum_coe:
- [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
+ [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
(not (Option.is_empty oc),(idl,c)) ] ]
;
@@ -426,20 +394,24 @@ GEXTEND Gram
;
END
-let only_identrefs =
- Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+ Gram.Entry.of_parser "test_only_starredidentrefs"
(fun strm ->
let rec aux n =
match get_tok (Util.stream_nth n strm) with
| KEYWORD "." -> ()
| KEYWORD ")" -> ()
- | IDENT _ -> aux (n+1)
+ | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
| _ -> raise Stream.Failure in
aux 0)
+let starredidentreflist_to_expr l =
+ match l with
+ | [] -> SsEmpty
+ | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
(* Modules and Sections *)
GEXTEND Gram
- GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+ GLOBAL: gallina_ext module_expr module_type section_subset_expr;
gallina_ext:
[ [ (* Interactive module declaration *)
@@ -462,7 +434,7 @@ GEXTEND Gram
| IDENT "End"; id = identref -> VernacEndSegment id
(* Naming a set of section hyps *)
- | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+ | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
VernacNameSectionHypSet (id, expr)
(* Requiring an already compiled module *)
@@ -553,22 +525,32 @@ GEXTEND Gram
CMwith (!@loc,mty,decl)
] ]
;
- section_subset_descr:
- [ [ IDENT "All" -> SsAll
- | "Type" -> SsType
- | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
- | e = section_subset_expr -> SsExpr e ] ]
- ;
+ (* Proof using *)
section_subset_expr:
+ [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+ starredidentreflist_to_expr l
+ | e = ssexpr -> e ]]
+ ;
+ starredidentref:
+ [ [ i = identref -> SsSingl i
+ | i = identref; "*" -> SsFwdClose(SsSingl i)
+ | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+ | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+ ;
+ ssexpr:
[ "35"
- [ "-"; e = section_subset_expr -> SsCompl e ]
+ [ "-"; e = ssexpr -> SsCompl e ]
| "50"
- [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
- | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+ [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+ | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
| "0"
- [ i = identref -> SsSet [i]
- | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
- | "("; e = section_subset_expr; ")"-> e ] ]
+ [ i = starredidentref -> i
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+ starredidentreflist_to_expr l
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+ SsFwdClose(starredidentreflist_to_expr l)
+ | "("; e = ssexpr; ")"-> e
+ | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
;
END
@@ -594,15 +576,15 @@ GEXTEND Gram
d = def_body ->
let s = coerce_reference_to_id qid in
VernacDefinition
- ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
+ ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (true, f, s, t)
@@ -701,7 +683,7 @@ GEXTEND Gram
VernacReserve bl
| IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
- test_plurial_form_types bl;
+ test_plural_form_types bl;
VernacReserve bl
| IDENT "Generalizable";
@@ -748,10 +730,10 @@ GEXTEND Gram
| IDENT "transparent" -> Conv_oracle.transparent ] ]
;
instance_name:
- [ [ name = identref; sup = OPT binders ->
- (let (loc,id) = name in (loc, Name id)),
+ [ [ name = pidentref; sup = OPT binders ->
+ (let ((loc,id),l) = name in ((loc, Name id),l)),
(Option.default [] sup)
- | -> (!@loc, Anonymous), [] ] ]
+ | -> ((!@loc, Anonymous), None), [] ] ]
;
reserv_list:
[ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
@@ -769,11 +751,7 @@ GEXTEND Gram
GLOBAL: command query_command class_rawexpr;
command:
- [ [ IDENT "Ltac";
- l = LIST1 tacdef_body SEP "with" ->
- VernacDeclareTacticDefinition (true, l)
-
- | IDENT "Comments"; l = LIST0 comment -> VernacComments l
+ [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
(* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
@@ -908,7 +886,6 @@ GEXTEND Gram
| IDENT "Classes" -> PrintClasses
| IDENT "TypeClasses" -> PrintTypeClasses
| IDENT "Instances"; qid = smart_global -> PrintInstances qid
- | IDENT "Ltac"; qid = global -> PrintLtac qid
| IDENT "Coercions" -> PrintCoercions
| IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
-> PrintCoercionPaths (s,t)
@@ -919,7 +896,6 @@ GEXTEND Gram
| IDENT "Hint"; qid = smart_global -> PrintHint qid
| IDENT "Hint"; "*" -> PrintHintDb
| IDENT "HintDb"; s = IDENT -> PrintHintDbName s
- | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
| IDENT "Scopes" -> PrintScopes
| IDENT "Scope"; s = IDENT -> PrintScope s
| IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
@@ -1067,10 +1043,6 @@ GEXTEND Gram
| IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
VernacNotationAddFormat (n,s,fmt)
- | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
- pil = LIST1 production_item; ":="; t = Tactic.tactic
- -> VernacTacticNotation (n,pil,t)
-
| IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
Metasyntax.check_infix_modifiers l;
@@ -1096,9 +1068,6 @@ GEXTEND Gram
obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
;
- tactic_level:
- [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
- ;
level:
[ [ IDENT "level"; n = natural -> NumLevel n
| IDENT "next"; IDENT "level" -> NextLevel ] ]
@@ -1130,10 +1099,4 @@ GEXTEND Gram
| IDENT "closed"; IDENT "binder" -> ETBinder false
] ]
;
- production_item:
- [ [ s = ne_string -> TacTerm s
- | nt = IDENT;
- po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
- ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
- ;
END
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 13ed80464..8df519b56 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -3,5 +3,3 @@ G_vernac
G_prim
G_proofs
G_tactic
-G_ltac
-G_obligations
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 8e8392961..8b8b38c34 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,6 @@
open Pp
open Util
-open Compat
open Tok
(* Dictionaries: trees annotated with string options, each node being a map
@@ -70,7 +69,7 @@ let ttree_remove ttree str =
remove ttree 0
-(* Errors occuring while lexing (explained as "Lexer error: ...") *)
+(* Errors occurring while lexing (explained as "Lexer error: ...") *)
module Error = struct
@@ -81,6 +80,7 @@ module Error = struct
| Undefined_token
| Bad_token of string
| UnsupportedUnicode of int
+ | IncorrectIndex of char list
exception E of t
@@ -93,7 +93,16 @@ module Error = struct
| Undefined_token -> "Undefined token"
| Bad_token tok -> Format.sprintf "Bad token %S" tok
| UnsupportedUnicode x ->
- Printf.sprintf "Unsupported Unicode character (0x%x)" x)
+ Printf.sprintf "Unsupported Unicode character (0x%x)" x
+ | IncorrectIndex l ->
+ let l = List.map (fun c -> Char.code c - 48) l in
+ let s = match l with
+ | c::d::l ->
+ let l = List.map string_of_int (List.rev l) in
+ String.concat "" l ^ CString.ordinal (10 * d + c)
+ | [c] -> CString.ordinal c
+ | [] -> assert false in
+ Printf.sprintf "%s expected" s)
(* Require to fix the Camlp4 signature *)
let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
@@ -263,9 +272,38 @@ let rec ident_tail len = parser
ident_tail (nstore n len s) s
| _ -> len
-let rec number len = parser
- | [< ' ('0'..'9' as c); s >] -> number (store len c) s
- | [< >] -> len
+let check_no_char s =
+ match Stream.npeek 3 s with
+ | [_;_;('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_')] -> false
+ | [_;_;_] -> true
+ | [_;_] -> true
+ | _ -> assert false
+
+let is_teen = function
+ | _::'1'::l -> true
+ | _ -> false
+
+let is_gt3 = function
+ | c::_ when c == '1' || c == '2' || c == '3' -> false
+ | _ -> true
+
+let check_gt3 l loc len =
+ if not (l == ['0']) && (is_teen l || is_gt3 l) then (false, len)
+ else err loc (IncorrectIndex l)
+
+let check_n n l loc len =
+ if List.hd l == n && not (is_teen l) then (false, len)
+ else err loc (IncorrectIndex l)
+
+let rec number_or_index bp l len = parser
+ | [< ' ('0'..'9' as c); s >] -> number_or_index bp (c::l) (store len c) s
+ | [< s >] ep ->
+ match Stream.npeek 2 s with
+ | ['s';'t'] when check_no_char s -> njunk 2 s; check_n '1' l (bp,ep) len
+ | ['n';'d'] when check_no_char s -> njunk 2 s; check_n '2' l (bp,ep) len
+ | ['r';'d'] when check_no_char s -> njunk 2 s; check_n '3' l (bp,ep) len
+ | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 l (bp,ep) len
+ | _ -> true, len
let rec string in_comments bp len = parser
| [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
@@ -298,6 +336,9 @@ let rec string in_comments bp len = parser
| [< 'c; s >] -> string in_comments bp (store len c) s
| [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
+(* Hook for exporting comment into xml theory files *)
+let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
+
(* Utilities for comments in beautify *)
let comment_begin = ref None
let comm_loc bp = match !comment_begin with
@@ -340,6 +381,9 @@ let null_comment s =
let comment_stop ep =
let current_s = Buffer.contents current in
+ if !Flags.xml_export && Buffer.length current > 0 &&
+ (!between_com || not(null_comment current_s)) then
+ Hook.get f_xml_output_comment current_s;
(if Flags.do_beautify() && Buffer.length current > 0 &&
(!between_com || not(null_comment current_s)) then
let bp = match !comment_begin with
@@ -449,7 +493,6 @@ let process_chars bp c cs =
err (bp, ep') Undefined_token
let token_of_special c s = match c with
- | '$' -> METAIDENT s
| '.' -> FIELD s
| _ -> assert false
@@ -488,8 +531,6 @@ let blank_or_eof cs =
let rec next_token = parser bp
| [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
comm_loc bp; push_char c; next_token s
- | [< ''$' as c; t = parse_after_special c bp >] ep ->
- comment_stop bp; (t, (ep, bp))
| [< ''.' as c; t = parse_after_special c bp; s >] ep ->
comment_stop bp;
(* We enforce that "." should either be part of a larger keyword,
@@ -514,9 +555,9 @@ let rec next_token = parser bp
let id = get_buff len in
comment_stop bp;
(try find_keyword id s with Not_found -> IDENT id), (bp, ep)
- | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
+ | [< ' ('0'..'9' as c); (b,len) = number_or_index bp [c] (store 0 c) >] ep ->
comment_stop bp;
- (INT (get_buff len), (bp, ep))
+ (if b then INT (get_buff len) else INDEX (get_buff len)), (bp, ep)
| [< ''\"'; len = string None bp 0 >] ep ->
comment_stop bp;
(STRING (get_buff len), (bp, ep))
@@ -565,7 +606,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc
let current_location_table = ref (loct_create ())
-type location_table = (int, CompatLoc.t) Hashtbl.t
+type location_table = (int, Compat.CompatLoc.t) Hashtbl.t
let location_table () = !current_location_table
let restore_location_table t = current_location_table := t
@@ -602,7 +643,7 @@ let func cs =
Stream.from
(fun i ->
let (tok, loc) = next_token cs in
- loct_add loct i (make_loc loc); Some tok)
+ loct_add loct i (Compat.make_loc loc); Some tok)
in
current_location_table := loct;
(ts, loct_func loct)
@@ -622,10 +663,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *)
module M_ = Camlp4.ErrorHandler.Register (Error)
-module Loc = CompatLoc
+module Loc = Compat.CompatLoc
module Token = struct
include Tok (* Cf. tok.ml *)
- module Loc = CompatLoc
+ module Loc = Compat.CompatLoc
module Error = Camlp4.Struct.EmptyError
module Filter = struct
type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
@@ -643,7 +684,7 @@ let mk () _init_loc(*FIXME*) cs =
let rec self =
parser i
[< (tok, loc) = next_token; s >] ->
- let loc = make_loc loc in
+ let loc = Compat.make_loc loc in
loct_add loct i loc;
[< '(tok, loc); self s >]
| [< >] -> [< >]
@@ -683,7 +724,7 @@ let strip s =
let terminal s =
let s = strip s in
- let () = match s with "" -> Errors.error "empty token." | _ -> () in
+ let () = match s with "" -> failwith "empty token." | _ -> () in
if is_ident_not_keyword s then IDENT s
else if is_number s then INT s
else KEYWORD s
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 2b9bd37df..24b0ec847 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -29,6 +29,8 @@ type com_state
val com_state: unit -> com_state
val restore_com_state: com_state -> unit
+val xml_output_comment : (string -> unit) Hook.t
+
val terminal : string -> Tok.t
(** The lexer of Coq: *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index a0cb83193..024d8607f 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,7 @@
Tok
Compat
Lexer
+Entry
Pcoq
Egramml
Egramcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml
index 797b031fe..802c24eef 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -20,37 +20,11 @@ open Tok (* necessary for camlp4 *)
module G = GrammarMake (Lexer)
-(* TODO: this is a workaround, since there isn't such
- [warning_verbose] in new camlp4. In camlp5, this ref
- gets hidden by [Gramext.warning_verbose] *)
-let warning_verbose = ref true
-
-IFDEF CAMLP5 THEN
-open Gramext
-ELSE
-open PcamlSig.Grammar
-open G
-END
-
-(** Compatibility with Camlp5 6.x *)
-
-IFDEF CAMLP5_6_00 THEN
-let slist0sep x y = Slist0sep (x, y, false)
-let slist1sep x y = Slist1sep (x, y, false)
-ELSE
-let slist0sep x y = Slist0sep (x, y)
-let slist1sep x y = Slist1sep (x, y)
-END
-
-let gram_token_of_token tok =
-IFDEF CAMLP5 THEN
- Stoken (Tok.to_pattern tok)
-ELSE
- match tok with
- | KEYWORD s -> Skeyword s
- | tok -> Stoken ((=) tok, to_string tok)
-END
+let warning_verbose = Compat.warning_verbose
+module Symbols = GramextMake(G)
+
+let gram_token_of_token = Symbols.stoken
let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
let camlp4_verbosity silent f x =
@@ -62,26 +36,6 @@ let camlp4_verbosity silent f x =
let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
- | Alist1 of prod_entry_key
- | Alist1sep of prod_entry_key * string
- | Alist0 of prod_entry_key
- | Alist0sep of prod_entry_key * string
- | Aopt of prod_entry_key
- | Amodifiers of prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of string
- | Aentry of string * string
-
(** [grammar_object] is the superclass of all grammar entries *)
module type Gramobj =
@@ -98,32 +52,11 @@ end
(** Grammar entries with associated types *)
-type entry_type = argument_type
type grammar_object = Gramobj.grammar_object
-type typed_entry = argument_type * grammar_object G.entry
-let in_typed_entry t e = (t,Gramobj.weaken_entry e)
-let type_of_typed_entry (t,e) = t
-let object_of_typed_entry (t,e) = e
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> typed_entry
+let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
let weaken_entry x = Gramobj.weaken_entry x
-module type Gramtypes =
-sig
- val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
- val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry
-end
-
-module Gramtypes : Gramtypes =
-struct
- let inGramObj rawwit = in_typed_entry (unquote rawwit)
- let outGramObj (a:'a raw_abstract_argument_type) o =
- if not (argument_type_eq (type_of_typed_entry o) (unquote a))
- then anomaly ~label:"outGramObj" (str "wrong type");
- (* downcast from grammar_object *)
- Obj.magic (object_of_typed_entry o)
-end
-
-open Gramtypes
-
(** Grammar extensions *)
(** NB: [extend_statment =
@@ -158,7 +91,10 @@ let grammar_delete e reinit (pos,rls) =
(List.rev rls);
match reinit with
| Some (a,ext) ->
- let lev = match pos with Some (Level n) -> n | _ -> assert false in
+ let lev = match Option.map Compat.to_coq_position pos with
+ | Some (Level n) -> n
+ | _ -> assert false
+ in
maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
| None -> ()
@@ -190,7 +126,7 @@ module Gram =
(** This extension command is used by the Grammar constr *)
-let grammar_extend e reinit ext =
+let unsafe_grammar_extend e reinit ext =
camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
camlp4_verbose (maybe_uncurry (G.extend e)) ext
@@ -215,22 +151,22 @@ let rec remove_grammars n =
redo();
camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+let make_rule r = [None, None, r]
+
(** An entry that checks we reached the end of the input. *)
let eoi_entry en =
let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
- GEXTEND Gram
- e: [ [ x = en; EOI -> x ] ]
- ;
- END;
+ let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
+ let act = Gram.action (fun _ x loc -> x) in
+ maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
let map_entry f en =
let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
- GEXTEND Gram
- e: [ [ x = en -> f x ] ]
- ;
- END;
+ let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
+ let act = Gram.action (fun x loc -> f x) in
+ maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
(* Parse a string, does NOT check if the entire string was read
@@ -239,58 +175,74 @@ let map_entry f en =
let parse_string f x =
let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
-type gram_universe = string * (string, typed_entry) Hashtbl.t
+type gram_universe = string
+
+let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
+ Hashtbl.create 97
-let trace = ref false
+let create_universe u =
+ let table = Hashtbl.create 97 in
+ let () = Hashtbl.add utables u table in
+ u
-(* The univ_tab is not part of the state. It contains all the grammars that
- exist or have existed before in the session. *)
+let uprim = create_universe "prim"
+let uconstr = create_universe "constr"
+let utactic = create_universe "tactic"
+let uvernac = create_universe "vernac"
-let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t)
+let get_univ u =
+ if Hashtbl.mem utables u then u
+ else raise Not_found
-let create_univ s =
- let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+let get_utable u =
+ try Hashtbl.find utables u
+ with Not_found -> assert false
-let uprim = create_univ "prim"
-let uconstr = create_univ "constr"
-let utactic = create_univ "tactic"
-let uvernac = create_univ "vernac"
+let get_entry u s =
+ let utab = get_utable u in
+ Hashtbl.find utab s
-let get_univ s =
- try
- Hashtbl.find univ_tab s
- with Not_found ->
- anomaly (Pp.str ("Unknown grammar universe: "^s))
+(** A table associating grammar to entries *)
+let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
-let get_entry (u, utab) s = Hashtbl.find utab s
+let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
+ Obj.magic (String.Map.find (Entry.repr e) !gtable)
-let new_entry etyp (u, utab) s =
- if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
+let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
+ assert (not (String.Map.mem (Entry.repr e) !gtable));
+ gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
+
+let new_entry etyp u s =
+ let utab = get_utable u in
let ename = u ^ ":" ^ s in
- let e = in_typed_entry etyp (Gram.entry_create ename) in
- Hashtbl.add utab s e; e
-
-let create_entry (u, utab) s etyp =
- try
- let e = Hashtbl.find utab s in
- if not (argument_type_eq (type_of_typed_entry e) etyp) then
- failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
- e
- with Not_found ->
- new_entry etyp (u, utab) s
+ let entry = Entry.create ename in
+ let e = Gram.entry_create ename in
+ let () = set_grammar entry e in
+ Hashtbl.add utab s (TypedEntry (etyp, e)); e
-let create_constr_entry s =
- outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
+let make_gen_entry u rawwit s = new_entry rawwit u s
-let create_generic_entry s wit =
- outGramObj wit (create_entry utactic s (unquote wit))
+module GrammarObj =
+struct
+ type ('r, _, _) obj = 'r Gram.entry
+ let name = "grammar"
+ let default _ = None
+end
-(* [make_gen_entry] builds entries extensible by giving its name (a string) *)
-(* For entries extensible only via the ML name, Gram.entry_create is enough *)
+module Grammar = Register(GrammarObj)
-let make_gen_entry (u,univ) rawwit s =
- let e = Gram.entry_create (u ^ ":" ^ s) in
- Hashtbl.add univ s (inGramObj rawwit e); e
+let register_grammar = Grammar.register0
+let genarg_grammar = Grammar.obj
+
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+ let utab = get_utable u in
+ if Hashtbl.mem utab s then
+ failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists")
+ else
+ let e = new_entry etyp u s in
+ let Rawwit t = etyp in
+ let () = Grammar.register0 t e in
+ e
(* Initial grammar entries *)
@@ -298,11 +250,12 @@ module Prim =
struct
let gec_gen x = make_gen_entry uprim x
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic or vernac extensions *)
let preident = gec_gen (rawwit wit_pre_ident) "preident"
let ident = gec_gen (rawwit wit_ident) "ident"
let natural = gec_gen (rawwit wit_int) "natural"
+ let index = gec_gen (rawwit wit_int) "index"
let integer = gec_gen (rawwit wit_int) "integer"
let bigint = Gram.entry_create "Prim.bigint"
let string = gec_gen (rawwit wit_string) "string"
@@ -315,6 +268,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
+ let pidentref = Gram.entry_create "Prim.pidentref"
let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
@@ -334,12 +288,12 @@ module Constr =
struct
let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
let constr = gec_constr "constr"
let operconstr = gec_constr "operconstr"
let constr_eoi = eoi_entry constr
let lconstr = gec_constr "lconstr"
- let binder_constr = create_constr_entry "binder_constr"
+ let binder_constr = gec_constr "binder_constr"
let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
let global = make_gen_entry uconstr (rawwit wit_ref) "global"
let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
@@ -367,7 +321,7 @@ module Tactic =
(* Main entry for extensions *)
let simple_tactic = Gram.entry_create "tactic:simple_tactic"
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
@@ -377,7 +331,7 @@ module Tactic =
make_gen_entry utactic (rawwit wit_bindings) "bindings"
let hypident = Gram.entry_create "hypident"
let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
- let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
+ let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval"
let uconstr =
make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
let quantified_hypothesis =
@@ -392,17 +346,14 @@ module Tactic =
(* Main entries for ltac *)
let tactic_arg = Gram.entry_create "tactic:tactic_arg"
- let tactic_expr = Gram.entry_create "tactic:tactic_expr"
- let binder_tactic = Gram.entry_create "tactic:binder_tactic"
+ let tactic_expr = make_gen_entry utactic (rawwit wit_tactic) "tactic_expr"
+ let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic"
let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
- (* For Ltac definition *)
- let tacdef_body = Gram.entry_create "tactic:tacdef_body"
-
end
module Vernac_ =
@@ -419,17 +370,29 @@ module Vernac_ =
let rec_definition = gec_vernac "Vernac.rec_definition"
(* Main vernac entry *)
let main_entry = Gram.entry_create "vernac"
-
- GEXTEND Gram
- main_entry:
- [ [ a = vernac -> Some (!@loc, a) | EOI -> None ] ]
- ;
- END
+ let noedit_mode = gec_vernac "noedit_command"
+
+ let () =
+ let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
+ let act_eoi = Gram.action (fun _ loc -> None) in
+ let rule = [
+ ([ Symbols.stoken Tok.EOI ], act_eoi);
+ ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
+ ] in
+ maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
+
+ let command_entry_ref = ref noedit_mode
+ let command_entry =
+ Gram.Entry.of_parser "command_entry"
+ (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
end
let main_entry = Vernac_.main_entry
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
(**********************************************************************)
(* This determines (depending on the associativity of the current
level and on the expected associativity) if a reference to constr_n is
@@ -614,7 +577,7 @@ let adjust_level assoc from = function
| ETConstr (p,()) -> Some (Some (n, Int.equal n p))
| _ -> Some (Some (n,false))
-let compute_entry allow_create adjust forpat = function
+let compute_entry adjust forpat = function
| ETConstr (n,q) ->
(if forpat then weaken_entry Constr.pattern
else weaken_entry Constr.operconstr),
@@ -631,24 +594,19 @@ let compute_entry allow_create adjust forpat = function
| ETPattern -> weaken_entry Constr.pattern, None, false
| ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
| ETOther (u,n) ->
- let u = get_univ u in
- let e =
- try get_entry u n
- with Not_found when allow_create -> create_entry u n ConstrArgType in
+ let e = get_entry u n in
object_of_typed_entry e, None, true
(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key forpat = function
- | ETConstr(200,()) when not forpat ->
- weaken_entry Constr.binder_constr, None
- | e ->
- let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in
- (e, level)
+let interp_constr_entry_key forpat level =
+ if level = 200 && not forpat then weaken_entry Constr.binder_constr, None
+ else if forpat then weaken_entry Constr.pattern, Some level
+ else weaken_entry Constr.operconstr, Some level
(* This computes the name to give to a production knowing the name and
associativity of the level where it must be added *)
let interp_constr_prod_entry_key ass from forpat en =
- compute_entry false (adjust_level ass from) forpat en
+ compute_entry (adjust_level ass from) forpat en
(**********************************************************************)
(* Binding constr entry keys to symbols *)
@@ -679,158 +637,133 @@ let make_sep_rules tkl =
let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
if is_binder_level from typ then
if forpat then
- Snterml (Gram.Entry.obj Constr.pattern,"200")
+ Symbols.snterml (Gram.Entry.obj Constr.pattern,"200")
else
- Snterml (Gram.Entry.obj Constr.operconstr,"200")
+ Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200")
else if is_self from typ then
- Sself
+ Symbols.sself
else
match typ with
| ETConstrList (typ',[]) ->
- Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+ Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
| ETConstrList (typ',tkl) ->
- slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
- (make_sep_rules tkl)
+ Symbols.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
+ make_sep_rules tkl)
| ETBinderList (false,[]) ->
- Slist1
+ Symbols.slist1
(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
| ETBinderList (false,tkl) ->
- slist1sep
- (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
- (make_sep_rules tkl)
+ Symbols.slist1sep
+ (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
+ make_sep_rules tkl)
| _ ->
match interp_constr_prod_entry_key assoc from forpat typ with
- | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
- | (eobj,Some None,_) -> Snext
+ | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj)
+ | (eobj,Some None,_) -> Symbols.snext
| (eobj,Some (Some (lev,cur)),_) ->
- Snterml (Gram.Entry.obj eobj,constr_level lev)
+ Symbols.snterml (Gram.Entry.obj eobj,constr_level lev)
(** Binding general entry keys to symbol *)
-let rec symbol_of_prod_entry_key = function
- | Alist1 s -> Slist1 (symbol_of_prod_entry_key s)
+let tuplify l =
+ List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l
+
+let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function
+| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu)))
+| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f)
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
+ | Atoken t -> Symbols.stoken t
+ | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
| Alist1sep (s,sep) ->
- slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
- | Alist0 s -> Slist0 (symbol_of_prod_entry_key s)
+ Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
| Alist0sep (s,sep) ->
- slist0sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
- | Aopt s -> Sopt (symbol_of_prod_entry_key s)
- | Amodifiers s ->
- Gram.srules'
- [([], Gram.action (fun _loc -> []));
- ([gram_token_of_string "(";
- slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ",");
- gram_token_of_string ")"],
- Gram.action (fun _ l _ _loc -> l))]
- | Aself -> Sself
- | Anext -> Snext
- | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
- | Atactic n ->
- Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
- | Agram s ->
- let e =
- try
- (** ppedrot: we should always generate Agram entries which have already
- been registered, so this should not fail. *)
- let (u, s) = match String.split ':' s with
- | u :: s :: [] -> (u, s)
- | _ -> raise Not_found
- in
- get_entry (get_univ u) s
- with Not_found ->
- Errors.anomaly (str "Unregistered grammar entry: " ++ str s)
- in
- Snterm (Gram.Entry.obj (object_of_typed_entry e))
- | Aentry (u,s) ->
- let e = get_entry (get_univ u) s in
- Snterm (Gram.Entry.obj (object_of_typed_entry e))
+ Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
+ | Aself -> Symbols.sself
+ | Anext -> Symbols.snext
+ | Aentry e ->
+ let e = get_grammar e in
+ Symbols.snterm (Gram.Entry.obj (weaken_entry e))
+ | Aentryl (e, n) ->
+ let e = get_grammar e in
+ Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
+ | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
+
+and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+
+and symbol_of_rules : type a. a Extend.rules -> _ = function
+| Rule0 -> fun accu _ -> accu
+| RuleS (r, e, rs) -> fun accu f ->
+ let symb = symbol_of_rule r [] in
+ let act = adj e [] f in
+ symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x))
+
+let level_of_snterml e = int_of_string (Symbols.snterml_level e)
+
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function
+| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc))
+| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x))
+
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+
+let of_coq_single_extend_statement (lvl, assoc, rule) =
+ (lvl, Option.map of_coq_assoc 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)
-let level_of_snterml = function
- | Snterml (_,l) -> int_of_string l
- | _ -> failwith "level_of_snterml"
+let grammar_extend e reinit ext =
+ let ext = of_coq_extend_statement ext in
+ unsafe_grammar_extend e reinit ext
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
-let tactic_level s =
- if Int.equal (String.length s) 7 && coincide s "tactic" 0 then
- let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
- else None
- else None
-
-let type_of_entry u s =
- type_of_typed_entry (get_entry u s)
-
-let rec interp_entry_name static up_level s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
- ListArgType t, Alist1 g
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
- ListArgType t, Alist1sep (g,sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
- ListArgType t, Alist0 g
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
- ListArgType t, Alist0sep (g,sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
- OptArgType t, Aopt g
- else if l > 5 && coincide s "_mods" (l-5) then
- let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
- ListArgType t, Amodifiers g
- else
- let s = match s with "hyp" -> "var" | _ -> s in
- let check_lvl n = match up_level with
- | None -> false
- | Some m -> Int.equal m n
- && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
- && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
- in
- let t, se =
- match tactic_level s with
- | Some n ->
- (** Quite ad-hoc *)
- let t = unquote (rawwit wit_tactic) in
- let se =
- if check_lvl n then Aself
- else if check_lvl (n + 1) then Anext
- else Atactic n
- in
- (Some t, se)
- | None ->
- try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
- try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
- try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
- if static then
- error ("Unknown entry "^s^".")
- else
- None, Aentry ("",s) in
- let t =
- match t with
- | Some t -> t
- | None -> ExtraArgType s in
- t, se
+let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
let list_entry_names () =
- let add_entry key (entry, _) accu = (key, entry) :: accu in
- let ans = Hashtbl.fold add_entry (snd uprim) [] in
- let ans = Hashtbl.fold add_entry (snd uconstr) ans in
- Hashtbl.fold add_entry (snd utactic) ans
+ let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
+ let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
+ let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
+ Hashtbl.fold add_entry (get_utable utactic) ans
+
+let epsilon_value f e =
+ let r = Rule (Next (Stop, e), fun x _ -> f x) in
+ let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+ let entry = G.entry_create "epsilon" in
+ let () = maybe_uncurry (Gram.extend entry) ext in
+ try Some (parse_string entry "") with _ -> None
+
+(** Registering grammar of generic arguments *)
+
+let () =
+ let open Stdarg in
+ let open Constrarg in
+(* Grammar.register0 wit_unit; *)
+(* Grammar.register0 wit_bool; *)
+ Grammar.register0 wit_int (Prim.integer);
+ Grammar.register0 wit_string (Prim.string);
+ Grammar.register0 wit_pre_ident (Prim.preident);
+ Grammar.register0 wit_int_or_var (Tactic.int_or_var);
+ Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern);
+ Grammar.register0 wit_ident (Prim.ident);
+ Grammar.register0 wit_var (Prim.var);
+ Grammar.register0 wit_ref (Prim.reference);
+ Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
+ Grammar.register0 wit_sort (Constr.sort);
+ Grammar.register0 wit_constr (Constr.constr);
+ Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval);
+ Grammar.register0 wit_uconstr (Tactic.uconstr);
+ Grammar.register0 wit_open_constr (Tactic.open_constr);
+ Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
+ Grammar.register0 wit_bindings (Tactic.bindings);
+(* Grammar.register0 wit_hyp_location_flag; *)
+ Grammar.register0 wit_red_expr (Tactic.red_expr);
+ Grammar.register0 wit_tactic (Tactic.tactic);
+ Grammar.register0 wit_ltac (Tactic.tactic);
+ Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
+ ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 2146ad964..afe888909 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -14,13 +14,12 @@ open Genarg
open Constrexpr
open Tacexpr
open Libnames
-open Compat
open Misctypes
open Genredexpr
(** The parser of Coq *)
-module Gram : GrammarSig
+module Gram : Compat.GrammarSig
(** The parser of Coq is built from three kinds of rule declarations:
@@ -106,28 +105,27 @@ type grammar_object
(** Type of reinitialization data *)
type gram_reinit = gram_assoc * gram_position
+(** General entry keys *)
+
+(** This intermediate abstract representation of entries can
+ both be reified into mlexpr for the ML extensions and
+ dynamically interpreted as entries for the Coq level extensions
+*)
+
(** Add one extension at some camlp4 position of some camlp4 entry *)
-val grammar_extend :
+val unsafe_grammar_extend :
grammar_object Gram.entry ->
gram_reinit option (** for reinitialization if ever needed *) ->
Gram.extend_statment -> unit
+val grammar_extend :
+ 'a Gram.entry ->
+ gram_reinit option (** for reinitialization if ever needed *) ->
+ 'a Extend.extend_statment -> unit
+
(** Remove the last n extensions *)
val remove_grammars : int -> unit
-
-
-
-(** The type of typed grammar objects *)
-type typed_entry
-
-(** The possible types for extensible grammars *)
-type entry_type = argument_type
-
-val type_of_typed_entry : typed_entry -> entry_type
-val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
-val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
-
(** Temporary activate camlp4 verbosity *)
val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
@@ -138,12 +136,8 @@ val parse_string : 'a Gram.entry -> string -> 'a
val eoi_entry : 'a Gram.entry -> 'a Gram.entry
val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
-(** Table of Coq statically defined grammar entries *)
-
type gram_universe
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
-
val get_univ : string -> gram_universe
val uprim : gram_universe
@@ -151,9 +145,12 @@ val uconstr : gram_universe
val utactic : gram_universe
val uvernac : gram_universe
-val create_entry : gram_universe -> string -> entry_type -> typed_entry
-val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
- 'a Gram.entry
+val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+
+val create_generic_entry : gram_universe -> string ->
+ ('a, rlevel) abstract_argument_type -> 'a Gram.entry
module Prim :
sig
@@ -163,10 +160,12 @@ module Prim :
val ident : Id.t Gram.entry
val name : Name.t located Gram.entry
val identref : Id.t located Gram.entry
+ val pidentref : (Id.t located * (Id.t located list) option) Gram.entry
val pattern_ident : Id.t Gram.entry
val pattern_identref : Id.t located Gram.entry
val base_ident : Id.t Gram.entry
val natural : int Gram.entry
+ val index : int Gram.entry
val bigint : Bigint.bigint Gram.entry
val integer : int Gram.entry
val string : string Gram.entry
@@ -212,7 +211,7 @@ module Module :
module Tactic :
sig
- val open_constr : open_constr_expr Gram.entry
+ val open_constr : constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
@@ -230,7 +229,6 @@ module Tactic :
val binder_tactic : raw_tactic_expr Gram.entry
val tactic : raw_tactic_expr Gram.entry
val tactic_eoi : raw_tactic_expr Gram.entry
- val tacdef_body : (reference * bool * raw_tactic_expr) Gram.entry
end
module Vernac_ :
@@ -242,54 +240,40 @@ module Vernac_ :
val vernac : vernac_expr Gram.entry
val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
val vernac_eoi : vernac_expr Gram.entry
+ val noedit_mode : vernac_expr Gram.entry
+ val command_entry : vernac_expr Gram.entry
end
(** The main entry: reads an optional vernac command *)
val main_entry : (Loc.t * vernac_expr) option Gram.entry
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
+
(** Mapping formal entries into concrete ones *)
(** Binding constr entry keys to entries and symbols *)
val interp_constr_entry_key : bool (** true for cases_pattern *) ->
- constr_entry_key -> grammar_object Gram.entry * int option
+ int -> grammar_object Gram.entry * int option
val symbol_of_constr_prod_entry_key : gram_assoc option ->
constr_entry_key -> bool -> constr_prod_entry_key ->
Gram.symbol
-(** General entry keys *)
+val name_of_entry : 'a Gram.entry -> 'a Entry.t
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
- | Alist1 of prod_entry_key
- | Alist1sep of prod_entry_key * string
- | Alist0 of prod_entry_key
- | Alist0sep of prod_entry_key * string
- | Aopt of prod_entry_key
- | Amodifiers of prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of string
- | Aentry of string * string
+val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** Binding general entry keys to symbols *)
-val symbol_of_prod_entry_key :
- prod_entry_key -> Gram.symbol
-
-(** Interpret entry names of the form "ne_constr_list" as entry keys *)
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-val interp_entry_name : bool (** true to fail on unknown entry *) ->
- int option -> string -> string -> entry_type * prod_entry_key
+val get_entry : gram_universe -> string -> typed_entry
(** Recover the list of all known tactic notation entries. *)
-val list_entry_names : unit -> (string * entry_type) list
+val list_entry_names : unit -> (string * argument_type) list
(** Registering/resetting the level of a constr entry *)
diff --git a/parsing/tok.ml b/parsing/tok.ml
index efd57968d..df7e7c2a6 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,28 +8,31 @@
(** The type of token for the Coq lexer and parser *)
+let string_equal (s1 : string) s2 = s1 = s2
+
type t =
| KEYWORD of string
- | METAIDENT of string
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
| INT of string
+ | INDEX of string
| STRING of string
| LEFTQMARK
| BULLET of string
| EOI
let equal t1 t2 = match t1, t2 with
-| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
-| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
-| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
-| IDENT s1, IDENT s2 -> CString.equal s1 s2
-| FIELD s1, FIELD s2 -> CString.equal s1 s2
-| INT s1, INT s2 -> CString.equal s1 s2
-| STRING s1, STRING s2 -> CString.equal s1 s2
+| IDENT s1, KEYWORD s2 -> string_equal s1 s2
+| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2
+| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
+| IDENT s1, IDENT s2 -> string_equal s1 s2
+| FIELD s1, FIELD s2 -> string_equal s1 s2
+| INT s1, INT s2 -> string_equal s1 s2
+| INDEX s1, INDEX s2 -> string_equal s1 s2
+| STRING s1, STRING s2 -> string_equal s1 s2
| LEFTQMARK, LEFTQMARK -> true
-| BULLET s1, BULLET s2 -> CString.equal s1 s2
+| BULLET s1, BULLET s2 -> string_equal s1 s2
| EOI, EOI -> true
| _ -> false
@@ -37,10 +40,10 @@ let extract_string = function
| KEYWORD s -> s
| IDENT s -> s
| STRING s -> s
- | METAIDENT s -> s
| PATTERNIDENT s -> s
| FIELD s -> s
| INT s -> s
+ | INDEX s -> s
| LEFTQMARK -> "?"
| BULLET s -> s
| EOI -> ""
@@ -48,10 +51,10 @@ let extract_string = function
let to_string = function
| KEYWORD s -> Format.sprintf "%S" s
| IDENT s -> Format.sprintf "IDENT %S" s
- | METAIDENT s -> Format.sprintf "METAIDENT %S" s
| PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
| FIELD s -> Format.sprintf "FIELD %S" s
| INT s -> Format.sprintf "INT %s" s
+ | INDEX s -> Format.sprintf "INDEX %s" s
| STRING s -> Format.sprintf "STRING %S" s
| LEFTQMARK -> "LEFTQMARK"
| BULLET s -> Format.sprintf "STRING %S" s
@@ -71,10 +74,10 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok)
let of_pattern = function
| "", s -> KEYWORD s
| "IDENT", s -> IDENT s
- | "METAIDENT", s -> METAIDENT s
| "PATTERNIDENT", s -> PATTERNIDENT s
| "FIELD", s -> FIELD s
| "INT", s -> INT s
+ | "INDEX", s -> INDEX s
| "STRING", s -> STRING s
| "LEFTQMARK", _ -> LEFTQMARK
| "BULLET", s -> BULLET s
@@ -84,10 +87,10 @@ let of_pattern = function
let to_pattern = function
| KEYWORD s -> "", s
| IDENT s -> "IDENT", s
- | METAIDENT s -> "METAIDENT", s
| PATTERNIDENT s -> "PATTERNIDENT", s
| FIELD s -> "FIELD", s
| INT s -> "INT", s
+ | INDEX s -> "INDEX", s
| STRING s -> "STRING", s
| LEFTQMARK -> "LEFTQMARK", ""
| BULLET s -> "BULLET", s
@@ -98,10 +101,10 @@ let match_pattern =
function
| "", "" -> (function KEYWORD s -> s | _ -> err ())
| "IDENT", "" -> (function IDENT s -> s | _ -> err ())
- | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ())
| "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
| "FIELD", "" -> (function FIELD s -> s | _ -> err ())
| "INT", "" -> (function INT s -> s | _ -> err ())
+ | "INDEX", "" -> (function INDEX s -> s | _ -> err ())
| "STRING", "" -> (function STRING s -> s | _ -> err ())
| "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ())
| "BULLET", "" -> (function BULLET s -> s | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index feee1983d..54b747952 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -10,16 +10,17 @@
type t =
| KEYWORD of string
- | METAIDENT of string
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
| INT of string
+ | INDEX of string
| STRING of string
| LEFTQMARK
| BULLET of string
| EOI
+val equal : t -> t -> bool
val extract_string : t -> string
val to_string : t -> string
(* Needed to fit Camlp4 signature *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 01:42:19 +0000