aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-19 15:29:48 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-19 15:29:48 +0000
commit1b089eb0231b4bd6d4cafb30f9e051bb53665978 (patch)
tree489e0f8ce7b4a80db388c63219b9cf4380b7f185 /parsing
parent259dde7928696593c2d3c6de474f5cf50fa4417d (diff)
Add (almost) compatibility with camlp4, without breaking support for camlp5
The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml466
-rw-r--r--parsing/egrammar.ml65
-rw-r--r--parsing/egrammar.mli7
-rw-r--r--parsing/extend.ml35
-rw-r--r--parsing/extend.mli38
-rw-r--r--parsing/g_constr.ml419
-rw-r--r--parsing/g_ltac.ml41
-rw-r--r--parsing/g_prim.ml44
-rw-r--r--parsing/g_proofs.ml43
-rw-r--r--parsing/g_tactic.ml439
-rw-r--r--parsing/g_vernac.ml449
-rw-r--r--parsing/g_xml.ml47
-rw-r--r--parsing/lexer.ml4147
-rw-r--r--parsing/lexer.mli13
-rw-r--r--parsing/pcoq.ml4383
-rw-r--r--parsing/pcoq.mli201
-rw-r--r--parsing/ppvernac.ml21
-rw-r--r--parsing/q_constr.ml44
-rw-r--r--parsing/q_coqast.ml468
-rw-r--r--parsing/q_util.ml449
-rw-r--r--parsing/q_util.mli4
-rw-r--r--parsing/tacextend.ml440
-rw-r--r--parsing/vernacextend.ml435
23 files changed, 690 insertions, 608 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index fd4952a52..e156bdc26 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -8,10 +8,10 @@
open Genarg
open Q_util
-open Q_coqast
open Egrammar
+open Pcoq
+open Compat
-let join_loc = Util.join_loc
let loc = Util.dummy_loc
let default_loc = <:expr< Util.dummy_loc >>
@@ -92,16 +92,16 @@ let rec make_wit loc = function
let make_act loc act pil =
let rec make = function
- | [] -> <:expr< Gramext.action (fun loc -> ($act$ : 'a)) >>
+ | [] -> <:expr< Gram.action (fun loc -> ($act$ : 'a)) >>
| GramNonTerminal (_,t,_,Some p) :: tl ->
let p = Names.string_of_id p in
<:expr<
- Gramext.action
+ Gram.action
(fun $lid:p$ ->
let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
>>
| (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl ->
- <:expr< Gramext.action (fun _ -> $make tl$) >> in
+ <:expr< Gram.action (fun _ -> $make tl$) >> in
make (List.rev pil)
let make_prod_item = function
@@ -145,13 +145,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
let globwit = <:expr< $lid:"globwit_"^s$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
- <:str_item<
- declare
- open Pcoq;
- open Extrawit;
+ declare_str_items loc
+ [ <:str_item<
value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
- Genarg.create_arg $se$;
- value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
+ Genarg.create_arg $se$ >>;
+ <:str_item<
+ value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+ <:str_item< do {
Tacinterp.add_interp_genarg $se$
((fun e x ->
(Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
@@ -159,14 +159,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
(Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))),
(fun subst x ->
(Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
- Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None
- [(None, None, $rules$)];
+ Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
+ (None, [(None, None, $rules$)]);
Pptactic.declare_extra_genarg_pprule
($rawwit$, $lid:rawpr$)
($globwit$, $lid:globpr$)
- ($wit$, $lid:pr$);
- end
- >>
+ ($wit$, $lid:pr$) }
+ >> ]
let declare_vernac_argument loc s pr cl =
let se = mlexpr_of_string s in
@@ -177,31 +176,31 @@ let declare_vernac_argument loc s pr cl =
let pr_rules = match pr with
| None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
| Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
- <:str_item<
- declare
- open Pcoq;
- open Extrawit;
+ declare_str_items loc
+ [ <:str_item<
value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
- $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
- value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
- Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None
- [(None, None, $rules$)];
+ $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>;
+ <:str_item<
+ value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+ <:str_item< do {
+ Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
+ (None, [(None, None, $rules$)]);
Pptactic.declare_extra_genarg_pprule
($rawwit$, $pr_rules$)
($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer")
- ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer");
- end
- >>
+ ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer") }
+ >> ]
open Vernacexpr
open Pcoq
open Pcaml
+open PcamlSig
EXTEND
GLOBAL: str_item;
str_item:
- [ [ "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+ [ [ "ARGUMENT"; "EXTEND"; s = entry_name;
"TYPED"; "AS"; typ = argtype;
"PRINTED"; "BY"; pr = LIDENT;
f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
@@ -216,15 +215,11 @@ EXTEND
"GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
OPT "|"; l = LIST1 argrule SEP "|";
"END" ->
- if String.capitalize s = s then
- failwith "Argument entry names must be lowercase";
declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
- | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+ | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name;
pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
OPT "|"; l = LIST1 argrule SEP "|";
"END" ->
- if String.capitalize s = s then
- failwith "Argument entry names must be lowercase";
declare_vernac_argument loc s pr l ] ]
;
argtype:
@@ -253,5 +248,10 @@ EXTEND
GramTerminal s
] ]
;
+ entry_name:
+ [ [ s = LIDENT -> s
+ | UIDENT -> failwith "Argument entry names must be lowercase"
+ ] ]
+ ;
END
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index a07c52e84..a32bfdec4 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -7,6 +7,7 @@
(************************************************************************)
open Pp
+open Compat
open Util
open Pcoq
open Extend
@@ -67,25 +68,25 @@ let make_constr_action
(f : loc -> constr_expr action_env -> constr_expr) pil =
let rec make (env,envlist as fullenv : constr_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc fullenv)
+ Gram.action (fun loc -> f loc fullenv)
| (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
(* parse a non-binding item *)
- Gramext.action (fun _ -> make fullenv tl)
+ Gram.action (fun _ -> make fullenv tl)
| GramConstrNonTerminal (typ, Some _) :: tl ->
(* parse a binding non-terminal *)
(match typ with
| (ETConstr _| ETOther _) ->
- Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
+ Gram.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
| ETReference ->
- Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
+ Gram.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
| ETName ->
- Gramext.action (fun (na:name located) ->
+ Gram.action (fun (na:name located) ->
make (constr_expr_of_name na :: env, envlist) tl)
| ETBigint ->
- Gramext.action (fun (v:Bigint.bigint) ->
+ Gram.action (fun (v:Bigint.bigint) ->
make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| ETConstrList (_,n) ->
- Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+ Gram.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
| ETPattern ->
failwith "Unexpected entry of type cases pattern")
| GramConstrListMark (n,b) :: tl ->
@@ -100,26 +101,26 @@ let make_cases_pattern_action
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc fullenv)
+ Gram.action (fun loc -> f loc fullenv)
| (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
(* parse a non-binding item *)
- Gramext.action (fun _ -> make fullenv tl)
+ Gram.action (fun _ -> make fullenv tl)
| GramConstrNonTerminal (typ, Some _) :: tl ->
(* parse a binding non-terminal *)
(match typ with
| ETConstr _ -> (* pattern non-terminal *)
- Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+ Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
| ETReference ->
- Gramext.action (fun (v:reference) ->
+ Gram.action (fun (v:reference) ->
make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
| ETName ->
- Gramext.action (fun (na:name located) ->
+ Gram.action (fun (na:name located) ->
make (cases_pattern_expr_of_name na :: env, envlist) tl)
| ETBigint ->
- Gramext.action (fun (v:Bigint.bigint) ->
+ Gram.action (fun (v:Bigint.bigint) ->
make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| ETConstrList (_,_) ->
- Gramext.action (fun (vl:cases_pattern_expr list) ->
+ Gram.action (fun (vl:cases_pattern_expr list) ->
make (env, vl :: envlist) tl)
| (ETPattern | ETOther _) ->
failwith "Unexpected entry of type cases pattern or other")
@@ -143,17 +144,18 @@ let rec make_constr_prod_item assoc from forpat = function
[]
let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
- let entry =
+ let entry =
if forpat then weaken_entry Constr.pattern
else weaken_entry Constr.operconstr in
- grammar_extend entry pos reinit [(name, p4assoc, [])]
+ grammar_extend entry reinit (pos,[(name, p4assoc, [])])
let pure_sublevels level symbs =
- map_succeed (function
- | Gramext.Snterml (_,n) when Some (int_of_string n) <> level ->
- int_of_string n
- | _ ->
- failwith "") symbs
+ map_succeed
+ (function s ->
+ let i = level_of_snterml s in
+ if level = Some i then failwith "";
+ i)
+ symbs
let extend_constr (entry,level) (n,assoc) mkact forpat rules =
List.iter (fun pt ->
@@ -162,7 +164,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
let needed_levels = register_empty_levels forpat pure_sublevels in
let pos,p4assoc,name,reinit = find_position forpat assoc level in
List.iter (prepare_empty_levels forpat) needed_levels;
- grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules
+ grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])])) rules
let extend_constr_notation (n,assoc,ntn,rules) =
(* Add the notation in constr *)
@@ -182,11 +184,11 @@ let make_generic_action
(f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
let rec make env = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gram.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gram.action (fun _ -> make env tl)
| Some (p, t) :: tl -> (* non-terminal *)
- Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
+ Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in
make [] (List.rev pil)
let make_rule univ f g pt =
@@ -200,7 +202,7 @@ let make_rule univ f g pt =
type grammar_prod_item =
| GramTerminal of string
| GramNonTerminal of
- loc * argument_type * Gram.te prod_entry_key * identifier option
+ loc * argument_type * prod_entry_key * identifier option
let make_prod_item = function
| GramTerminal s -> (gram_token_of_string s, None)
@@ -213,7 +215,8 @@ let extend_tactic_grammar s gl =
let univ = get_univ "tactic" in
let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
let rules = List.map (make_rule univ mkact make_prod_item) gl in
- Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
+ maybe_uncurry (Gram.extend Tactic.simple_tactic)
+ (None,[(None, None, List.rev rules)])
(* Vernac grammar extensions *)
@@ -226,7 +229,7 @@ let extend_vernac_command_grammar s nt gl =
let univ = get_univ "vernac" in
let mkact loc l = VernacExtend (s,List.map snd l) in
let rules = List.map (make_rule univ mkact make_prod_item) gl in
- Gram.extend nt None [(None, None, List.rev rules)]
+ maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
(**********************************************************************)
(** Grammar declaration for Tactic Notation (Coq level) *)
@@ -237,7 +240,7 @@ let get_tactic_entry n =
else if n = 5 then
weaken_entry Tactic.binder_tactic, None
else if 1<=n && n<5 then
- weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
+ weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n))
else
error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
@@ -261,13 +264,13 @@ let add_tactic_entry (key,lev,prods,tac) =
(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
make_rule univ (mkact key tac) make_prod_item prods in
synchronize_level_positions ();
- grammar_extend entry pos None [(None, None, List.rev [rules])]
+ grammar_extend entry None (pos,[(None, None, List.rev [rules])])
(**********************************************************************)
(** State of the grammar extensions *)
type notation_grammar =
- int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
+ int * gram_assoc option * notation * grammar_constr_prod_item list list
type all_grammar_command =
| Notation of (precedence * tolerability list) * notation_grammar
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 874aed570..a0004ce38 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,6 +6,7 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+open Compat
open Util
open Names
open Topconstr
@@ -32,14 +33,14 @@ type grammar_constr_prod_item =
concat with last parsed list if true *)
type notation_grammar =
- int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
+ int * gram_assoc option * notation * grammar_constr_prod_item list list
(** For tactic and vernac notations *)
type grammar_prod_item =
| GramTerminal of string
| GramNonTerminal of loc * argument_type *
- Gram.te prod_entry_key * identifier option
+ prod_entry_key * identifier option
(** Adding notations *)
@@ -55,7 +56,7 @@ val extend_tactic_grammar :
string -> grammar_prod_item list list -> unit
val extend_vernac_command_grammar :
- string -> vernac_expr Gram.Entry.e option -> grammar_prod_item list list -> unit
+ string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit
val get_extend_vernac_grammars :
unit -> (string * grammar_prod_item list list) list
diff --git a/parsing/extend.ml b/parsing/extend.ml
index cc3551d32..4674a7c90 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,35 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Compat
open Util
-(**********************************************************************)
-(* 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 'a prod_entry_key =
- | Alist1 of 'a prod_entry_key
- | Alist1sep of 'a prod_entry_key * string
- | Alist0 of 'a prod_entry_key
- | Alist0sep of 'a prod_entry_key * string
- | Aopt of 'a prod_entry_key
- | Amodifiers of 'a prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of 'a Gramext.g_entry
- | Aentry of string * string
-
-(**********************************************************************)
-(* Entry keys for constr notations *)
+(** Entry keys for constr notations *)
type side = Left | Right
type production_position =
- | BorderProd of side * Gramext.g_assoc option
+ | BorderProd of side * gram_assoc option
| InternalProd
type production_level =
@@ -48,14 +28,17 @@ type ('lev,'pos) constr_entry_key_gen =
| ETOther of string * string
| ETConstrList of ('lev * 'pos) * Tok.t list
-(* Entries level (left-hand-side of grammar rules) *)
+(** Entries level (left-hand-side of grammar rules) *)
+
type constr_entry_key =
(int,unit) constr_entry_key_gen
-(* Entries used in productions (in right-hand-side of grammar rules) *)
+(** Entries used in productions (in right-hand-side of grammar rules) *)
+
type constr_prod_entry_key =
(production_level,production_position) constr_entry_key_gen
-(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+
type simple_constr_prod_entry_key =
(production_level,unit) constr_entry_key_gen
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 99b83785c..597ff69a5 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -6,35 +6,14 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-open Util
-
-(*********************************************************************
- 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 'a prod_entry_key =
- | Alist1 of 'a prod_entry_key
- | Alist1sep of 'a prod_entry_key * string
- | Alist0 of 'a prod_entry_key
- | Alist0sep of 'a prod_entry_key * string
- | Aopt of 'a prod_entry_key
- | Amodifiers of 'a prod_entry_key
- | Aself
- | Anext
- | Atactic of int
- | Agram of 'a Gramext.g_entry
- | Aentry of string * string
-
-(*********************************************************************
- Entry keys for constr notations *)
+open Compat
+
+(** Entry keys for constr notations *)
type side = Left | Right
type production_position =
- | BorderProd of side * Gramext.g_assoc option
+ | BorderProd of side * gram_assoc option
| InternalProd
type production_level =
@@ -48,14 +27,17 @@ type ('lev,'pos) constr_entry_key_gen =
| ETOther of string * string
| ETConstrList of ('lev * 'pos) * Tok.t list
-(* Entries level (left-hand-side of grammar rules) *)
+(** Entries level (left-hand-side of grammar rules) *)
+
type constr_entry_key =
(int,unit) constr_entry_key_gen
-(* Entries used in productions (in right-hand-side of grammar rules) *)
+(** Entries used in productions (in right-hand-side of grammar rules) *)
+
type constr_prod_entry_key =
(production_level,production_position) constr_entry_key_gen
-(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+
type simple_constr_prod_entry_key =
(production_level,unit) constr_entry_key_gen
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9ce65226d..ef18ad4eb 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,6 +17,7 @@ open Libnames
open Topconstr
open Util
open Tok
+open Compat
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
@@ -74,11 +75,11 @@ let err () = raise Stream.Failure
let lpar_id_coloneq =
Gram.Entry.of_parser "test_lpar_id_coloneq"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "(" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| IDENT s ->
- (match stream_nth 2 strm with
+ (match get_tok (stream_nth 2 strm) with
| KEYWORD ":=" ->
stream_njunk 3 strm;
Names.id_of_string s
@@ -89,9 +90,9 @@ let lpar_id_coloneq =
let impl_ident =
Gram.Entry.of_parser "impl_ident"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "{" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| IDENT ("wf"|"struct"|"measure") -> err ()
| IDENT s ->
stream_njunk 2 strm;
@@ -102,9 +103,9 @@ let impl_ident =
let ident_colon =
Gram.Entry.of_parser "ident_colon"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| IDENT s ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| KEYWORD ":" ->
stream_njunk 2 strm;
Names.id_of_string s
@@ -114,9 +115,9 @@ let ident_colon =
let ident_with =
Gram.Entry.of_parser "ident_with"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| IDENT s ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| KEYWORD "with" ->
stream_njunk 2 strm;
Names.id_of_string s
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index bfdd0773a..6ea55f874 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -15,6 +15,7 @@ open Vernacexpr
open Pcoq
open Prim
open Tactic
+open Tok
let fail_default_value = ArgArg 0
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b1a2fa54b..9b962e823 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -10,6 +10,8 @@ open Pcoq
open Names
open Libnames
open Topconstr
+open Tok
+open Compat
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
let _ = List.iter Lexer.add_keyword prim_kw
@@ -41,7 +43,7 @@ GEXTEND Gram
[ [ s = IDENT -> id_of_string s ] ]
;
pattern_ident:
- [ [ s = LEFTQMARK; id = ident -> id ] ]
+ [ [ LEFTQMARK; id = ident -> id ] ]
;
pattern_identref:
[ [ id = pattern_ident -> (loc, id) ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index dfb59a19d..aef2f05eb 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -15,6 +15,7 @@ open Topconstr
open Vernacexpr
open Prim
open Constr
+open Tok
let thm_token = G_vernac.thm_token
@@ -29,7 +30,7 @@ GEXTEND Gram
;
opt_hintbases:
[ [ -> []
- | ":"; l = LIST1 IDENT -> l ] ]
+ | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
;
command:
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b39ea5770..0bff5ca8b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -16,6 +16,7 @@ open Topconstr
open Libnames
open Termops
open Tok
+open Compat
let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
@@ -29,11 +30,11 @@ let err () = raise Stream.Failure
let test_lpar_id_coloneq =
Gram.Entry.of_parser "lpar_id_coloneq"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "(" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| IDENT _ ->
- (match stream_nth 2 strm with
+ (match get_tok (stream_nth 2 strm) with
| KEYWORD ":=" -> ()
| _ -> err ())
| _ -> err ())
@@ -43,11 +44,11 @@ let test_lpar_id_coloneq =
let test_lpar_idnum_coloneq =
Gram.Entry.of_parser "test_lpar_idnum_coloneq"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "(" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| IDENT _ | INT _ ->
- (match stream_nth 2 strm with
+ (match get_tok (stream_nth 2 strm) with
| KEYWORD ":=" -> ()
| _ -> err ())
| _ -> err ())
@@ -57,11 +58,11 @@ let test_lpar_idnum_coloneq =
let test_lpar_id_colon =
Gram.Entry.of_parser "lpar_id_colon"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "(" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| IDENT _ ->
- (match stream_nth 2 strm with
+ (match get_tok (stream_nth 2 strm) with
| KEYWORD ":" -> ()
| _ -> err ())
| _ -> err ())
@@ -72,33 +73,33 @@ let check_for_coloneq =
Gram.Entry.of_parser "lpar_id_colon"
(fun strm ->
let rec skip_to_rpar p n =
- match list_last (Stream.npeek n strm) with
+ match get_tok (list_last (Stream.npeek n strm)) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
| KEYWORD ")" -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
| KEYWORD "." -> err ()
| _ -> skip_to_rpar p (n+1) in
let rec skip_names n =
- match list_last (Stream.npeek n strm) with
+ match get_tok (list_last (Stream.npeek n strm)) with
| IDENT _ | KEYWORD "_" -> skip_names (n+1)
| KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
| _ -> err () in
let rec skip_binders n =
- match list_last (Stream.npeek n strm) with
+ match get_tok (list_last (Stream.npeek n strm)) with
| KEYWORD "(" -> skip_binders (skip_names (n+1))
| IDENT _ | KEYWORD "_" -> skip_binders (n+1)
| KEYWORD ":=" -> ()
| _ -> err () in
- match Stream.npeek 1 strm with
- | [KEYWORD "("] -> skip_binders 2
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" -> skip_binders 2
| _ -> err ())
let guess_lpar_ipat s strm =
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD "(" ->
- (match stream_nth 1 strm with
+ (match get_tok (stream_nth 1 strm) with
| KEYWORD ("("|"[") -> ()
| IDENT _ ->
- (match stream_nth 2 strm with
+ (match get_tok (stream_nth 2 strm) with
| KEYWORD s' when s = s' -> ()
| _ -> err ())
| _ -> err ())
@@ -113,7 +114,7 @@ let guess_lpar_colon =
let lookup_at_as_coma =
Gram.Entry.of_parser "lookup_at_as_coma"
(fun strm ->
- match stream_nth 0 strm with
+ match get_tok (stream_nth 0 strm) with
| KEYWORD (","|"at"|"as") -> ()
| _ -> err ())
@@ -450,7 +451,7 @@ GEXTEND Gram
;
hintbases:
[ [ "with"; "*" -> None
- | "with"; l = LIST1 IDENT -> Some l
+ | "with"; l = LIST1 [ x = IDENT -> x] -> Some l
| -> Some [] ] ]
;
auto_using:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e213660d9..cbeb7a01e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -10,6 +10,8 @@
open Pp
+open Compat
+open Tok
open Util
open Names
open Topconstr
@@ -33,20 +35,20 @@ let _ = List.iter Lexer.add_keyword vernac_kw
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
-let check_command = Gram.Entry.create "vernac:check_command"
+let check_command = Gram.entry_create "vernac:check_command"
-let tactic_mode = Gram.Entry.create "vernac:tactic_command"
-let noedit_mode = Gram.Entry.create "vernac:noedit_command"
+let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let noedit_mode = Gram.entry_create "vernac:noedit_command"
-let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
-let thm_token = Gram.Entry.create "vernac:thm_token"
-let def_body = Gram.Entry.create "vernac:def_body"
-let decl_notation = Gram.Entry.create "vernac:decl_notation"
-let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
-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 class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
+let thm_token = Gram.entry_create "vernac:thm_token"
+let def_body = Gram.entry_create "vernac:def_body"
+let decl_notation = Gram.entry_create "vernac:decl_notation"
+let typeclass_context = Gram.entry_create "vernac:typeclass_context"
+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 command_entry = ref noedit_mode
let set_command_entry e = command_entry := e
@@ -65,7 +67,7 @@ let _ = Proof_global.register_proof_mode {Proof_global.
let default_command_entry =
Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm)
+ (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
let no_hook _ _ = ()
GEXTEND Gram
@@ -758,7 +760,7 @@ GEXTEND Gram
| "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
| IDENT "Scopes" -> PrintScopes
| IDENT "Scope"; s = IDENT -> PrintScope s
- | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
+ | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
| IDENT "Implicit"; qid = smart_global -> PrintImplicit qid
| IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
| IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid)
@@ -784,7 +786,7 @@ GEXTEND Gram
| s = STRING -> StringRefValue s ] ]
;
option_table:
- [ [ fl = LIST1 IDENT -> fl ]]
+ [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]]
;
as_dirpath:
[ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
@@ -911,16 +913,17 @@ GEXTEND Gram
| IDENT "next"; IDENT "level" -> NextLevel ] ]
;
syntax_modifier:
- [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
- | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at";
+ [ [ "at"; IDENT "level"; n = natural -> SetLevel n
+ | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA
+ | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
+ | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
+ | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
+ | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s
+ | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
- | "at"; IDENT "level"; n = natural -> SetLevel n
- | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
- | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
- | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
+ | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
| x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
- | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
- | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
+ ] ]
;
syntax_extension_type:
[ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 901f7ff10..2e2796a22 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -18,6 +18,7 @@ open Libnames
open Nametab
open Detyping
+open Tok
(* Generic xml parser without raw data *)
@@ -29,7 +30,7 @@ let check_tags loc otag ctag =
user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
str "does not match open xml tag " ++ str otag ++ str ".")
-let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e)
+let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
GEXTEND Gram
GLOBAL: xml_eoi;
@@ -273,5 +274,5 @@ let rec interp_xml_tactic_arg = function
let parse_tactic_arg ch =
interp_xml_tactic_arg
- (Pcoq.Gram.Entry.parse xml_eoi
- (Pcoq.Gram.parsable (Stream.of_channel ch)))
+ (Pcoq.Gram.entry_parse xml_eoi
+ (Pcoq.Gram.parsable (Stream.of_channel ch)))
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 175ce16a4..ba5a8c425 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -8,7 +8,7 @@
open Pp
open Util
-open Token
+open Compat
open Tok
(* Dictionaries: trees annotated with string options, each node being a map
@@ -71,18 +71,34 @@ let ttree_remove ttree str =
(* Errors occuring while lexing (explained as "Lexer error: ...") *)
-type error =
- | Illegal_character
- | Unterminated_comment
- | Unterminated_string
- | Undefined_token
- | Bad_token of string
+module Error = struct
-exception Error of error
+ type t =
+ | Illegal_character
+ | Unterminated_comment
+ | Unterminated_string
+ | Undefined_token
+ | Bad_token of string
-let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str)
+ exception E of t
-let bad_token str = raise (Error (Bad_token str))
+ let to_string x =
+ "Syntax Error: Lexer: " ^
+ (match x with
+ | Illegal_character -> "Illegal character"
+ | Unterminated_comment -> "Unterminated comment"
+ | Unterminated_string -> "Unterminated string"
+ | Undefined_token -> "Undefined token"
+ | Bad_token tok -> Format.sprintf "Bad token %S" tok)
+
+ let print ppf x = Format.fprintf ppf "%s@." (to_string x)
+
+end
+open Error
+
+let err loc str = Loc.raise (make_loc loc) (Error.E str)
+
+let bad_token str = raise (Error.E (Bad_token str))
(* Lexer conventions on tokens *)
@@ -175,7 +191,7 @@ let check_ident str =
let check_keyword str =
try check_special_token str
- with Error _ -> check_ident str
+ with Error.E _ -> check_ident str
(* Keyword and symbol dictionary *)
let token_tree = ref empty_ttree
@@ -379,7 +395,7 @@ let find_keyword id s =
let tt = ttree_find !token_tree id in
match progress_further tt.node 0 tt s with
| None -> raise Not_found
- | Some c -> c
+ | Some c -> KEYWORD c
(* Must be a special token *)
let process_chars bp c cs =
@@ -438,7 +454,7 @@ let rec next_token = parser bp
len = ident_tail (store 0 c); s >] ep ->
let id = get_buff len in
comment_stop bp;
- (try KEYWORD (find_keyword id s) with Not_found -> IDENT id), (bp, ep)
+ (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
| [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
comment_stop bp;
(INT (get_buff len), (bp, ep))
@@ -461,7 +477,7 @@ let rec next_token = parser bp
let id = get_buff len in
let ep = Stream.count s in
comment_stop bp;
- (try KEYWORD (find_keyword id s) with Not_found -> IDENT id), (bp, ep)
+ (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
| AsciiChar | Utf8Token ((UnicodeSymbol | UnicodeIdentPart), _) ->
let t = process_chars bp (Stream.next s) s in
comment_stop bp; t
@@ -473,53 +489,23 @@ let rec next_token = parser bp
let locerr () = invalid_arg "Lexer: location function"
-let tsz = 256 (* up to 2^29 entries on a 32-bit machine, 2^61 on 64-bit *)
-
-let loct_create () = ref [| [| |] |]
+let loct_create () = Hashtbl.create 207
let loct_func loct i =
- match
- if i < 0 || i/tsz >= Array.length !loct then None
- else if !loct.(i/tsz) = [| |] then None
- else !loct.(i/tsz).(i mod tsz)
- with
- | Some loc -> Util.make_loc loc
- | _ -> locerr ()
-
-let loct_add loct i loc =
- while i/tsz >= Array.length !loct do
- let new_tmax = Array.length !loct * 2 in
- let new_loct = Array.make new_tmax [| |] in
- Array.blit !loct 0 new_loct 0 (Array.length !loct);
- loct := new_loct;
- done;
- if !loct.(i/tsz) = [| |] then !loct.(i/tsz) <- Array.make tsz None;
- !loct.(i/tsz).(i mod tsz) <- Some loc
-
-let current_location_table = ref (ref [| [| |] |])
-
-let location_function n =
- loct_func !current_location_table n
+ try Hashtbl.find loct i with Not_found -> locerr ()
-let func cs =
- let loct = loct_create () in
- let ts =
- Stream.from
- (fun i ->
- let (tok, loc) = next_token cs in
- loct_add loct i loc; Some tok)
- in
- current_location_table := loct;
- (ts, loct_func loct)
+let loct_add loct i loc = Hashtbl.add loct i loc
-type location_table = (int * int) option array array ref
+let current_location_table = ref (loct_create ())
+
+type location_table = (int, loc) Hashtbl.t
let location_table () = !current_location_table
let restore_location_table t = current_location_table := t
+let location_function n = loct_func !current_location_table n
+(** {6 The lexer of Coq} *)
-(* The lexer of Coq *)
-
-(* Note: removing a token.
+(** Note: removing a token.
We do nothing because [remove_token] is called only when removing a grammar
rule with [Grammar.delete_rule]. The latter command is called only when
unfreezing the state of the grammar entries (see GRAMMAR summary, file
@@ -529,7 +515,9 @@ let restore_location_table t = current_location_table := t
IFDEF CAMLP5 THEN
-(* Names of tokens, for this lexer, used in Grammar error messages *)
+type te = Tok.t
+
+(** Names of tokens, for this lexer, used in Grammar error messages *)
let token_text = function
| ("", t) -> "'" ^ t ^ "'"
@@ -542,15 +530,23 @@ let token_text = function
| (con, "") -> con
| (con, prm) -> con ^ " \"" ^ prm ^ "\""
-(* Adding a new token (keyword or special token). *)
-
-let add_token pat = match Tok.of_pattern pat with
- | KEYWORD s -> add_keyword s
- | _ -> ()
+let func cs =
+ let loct = loct_create () in
+ let ts =
+ Stream.from
+ (fun i ->
+ let (tok, loc) = next_token cs in
+ loct_add loct i (make_loc loc); Some tok)
+ in
+ current_location_table := loct;
+ (ts, loct_func loct)
let lexer = {
Token.tok_func = func;
- Token.tok_using = add_token;
+ Token.tok_using =
+ (fun pat -> match Tok.of_pattern pat with
+ | KEYWORD s -> add_keyword s
+ | _ -> ());
Token.tok_removing = (fun _ -> ());
Token.tok_match = Tok.match_pattern;
Token.tok_comm = None;
@@ -558,11 +554,38 @@ let lexer = {
ELSE (* official camlp4 for ocaml >= 3.10 *)
-TODO
+module M_ = Camlp4.ErrorHandler.Register (Error)
+
+module Loc = Loc
+module Token = struct
+ include Tok (* Cf. tok.ml *)
+ module Loc = Loc
+ module Error = Camlp4.Struct.EmptyError
+ module Filter = struct
+ type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
+ type t = unit
+ let mk _is_kwd = ()
+ let keyword_added () kwd _ = add_keyword kwd
+ let keyword_removed () _ = ()
+ let filter () x = x
+ let define_filter () _ = ()
+ end
+end
+
+let mk () _init_loc(*FIXME*) cs =
+ let loct = loct_create () in
+ let rec self =
+ parser i
+ [< (tok, loc) = next_token; s >] ->
+ let loc = make_loc loc in
+ loct_add loct i loc;
+ [< '(tok, loc); self s >]
+ | [< >] -> [< >]
+ in current_location_table := loct; self cs
END
-(* Terminal symbols interpretation *)
+(** Terminal symbols interpretation *)
let is_ident_not_keyword s =
match s.[0] with
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 7f7d36b74..a8ae46fec 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -9,15 +9,6 @@
open Pp
open Util
-type error =
- | Illegal_character
- | Unterminated_comment
- | Unterminated_string
- | Undefined_token
- | Bad_token of string
-
-exception Error of error
-
val add_keyword : string -> unit
val remove_keyword : string -> unit
val is_keyword : string -> bool
@@ -45,6 +36,6 @@ val set_xml_output_comment : (string -> unit) -> unit
val terminal : string -> Tok.t
-(** The lexer of Coq *)
+(** The lexer of Coq: *)
-val lexer : Compat.lexer
+include Compat.LexerSig
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7d78f5371..a20c0d1ef 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -7,6 +7,8 @@
(************************************************************************)
open Pp
+open Compat
+open Tok
open Util
open Names
open Extend
@@ -18,54 +20,67 @@ open Tacexpr
open Extrawit
open Ppextend
-(* The parser of Coq *)
+(** The parser of Coq *)
+
+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 G
+END
-module L =
- struct
- type te = Tok.t
- let lexer = Lexer.lexer
- 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
-module G = Grammar.GMake(L)
+let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
-ELSE (* official camlp4 of ocaml >= 3.10 *)
+let camlp4_verbosity silent f x =
+ let a = !warning_verbose in
+ warning_verbose := silent;
+ f x;
+ warning_verbose := a
-TODO
+let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
-END
-let gram_token_of_token tok = Gramext.Stoken (Tok.to_pattern tok)
-let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
+(** General entry keys *)
-let grammar_delete e pos reinit rls =
- List.iter
- (fun (n,ass,lev) ->
+(** 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
+*)
- (* Caveat: deletion is not the converse of extension: when an
- empty level is extended, deletion removes the level instead
- of keeping it empty. This has an effect on the empty levels 8,
- 99 and 200. We didn't find a good solution to this problem
- (e.g. using G.extend to know if the level exists results in a
- printed error message as side effect). As a consequence an
- extension at 99 or 8 (and for pattern 200 too) inside a section
- corrupts the parser. *)
+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 G.internal_entry
+ | Aentry of string * string
- List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
- (List.rev rls);
- if reinit <> None then
- let lev = match pos with Some (Gramext.Level n) -> n | _ -> assert false in
- let pos =
- if lev = "200" then Gramext.First
- else Gramext.After (string_of_int (int_of_string lev + 1)) in
- G.extend e (Some pos) [Some lev,reinit,[]];
+(** [grammar_object] is the superclass of all grammar entries *)
-(* grammar_object is the superclass of all grammar entries *)
module type Gramobj =
sig
type grammar_object
- val weaken_entry : 'a G.Entry.e -> grammar_object G.Entry.e
+ val weaken_entry : 'a G.entry -> grammar_object G.entry
end
module Gramobj : Gramobj =
@@ -74,9 +89,11 @@ struct
let weaken_entry e = Obj.magic e
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.e
+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
@@ -85,8 +102,8 @@ let weaken_entry x = Gramobj.weaken_entry x
module type Gramtypes =
sig
open Decl_kinds
- val inGramObj : 'a raw_abstract_argument_type -> 'a G.Entry.e -> typed_entry
- val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.Entry.e
+ 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 =
@@ -101,77 +118,107 @@ end
open Gramtypes
-type camlp4_rule =
- Tok.t Gramext.g_symbol list * Gramext.g_action
+(** Grammar extensions *)
+
+(** NB: [extend_statment =
+ gram_position option * single_extend_statment list]
+ and [single_extend_statment =
+ string option * gram_assoc option * production_rule list]
+ and [production_rule = symbol list * action]
-type camlp4_entry_rules =
- (* first two parameters are name and assoc iff a level is created *)
- string option * Gramext.g_assoc option * camlp4_rule list
+ In [single_extend_statement, first two parameters are name and
+ assoc iff a level is created *)
type ext_kind =
| ByGrammar of
- grammar_object G.Entry.e * Gramext.position option *
- camlp4_entry_rules list * Gramext.g_assoc option
- | ByGEXTEND of (unit -> unit) * (unit -> unit)
+ grammar_object G.entry
+ * gram_assoc option (** for reinitialization if ever needed *)
+ * G.extend_statment
+ | ByEXTEND of (unit -> unit) * (unit -> unit)
+
+(** The list of extensions *)
let camlp4_state = ref []
-(* The apparent parser of Coq; encapsulate G to keep track of the
- extensions. *)
+(** Deletion
+
+ Caveat: deletion is not the converse of extension: when an
+ empty level is extended, deletion removes the level instead
+ of keeping it empty. This has an effect on the empty levels 8,
+ 99 and 200. We didn't find a good solution to this problem
+ (e.g. using G.extend to know if the level exists results in a
+ printed error message as side effect). As a consequence an
+ extension at 99 or 8 (and for pattern 200 too) inside a section
+ corrupts the parser. *)
+
+let grammar_delete e reinit (pos,rls) =
+ List.iter
+ (fun (n,ass,lev) ->
+ List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+ (List.rev rls);
+ if reinit <> None then
+ let lev = match pos with Some (Level n) -> n | _ -> assert false in
+ let pos =
+ if lev = "200" then First
+ else After (string_of_int (int_of_string lev + 1)) in
+ maybe_uncurry (G.extend e) (Some pos, [Some lev,reinit,[]])
+
+(** The apparent parser of Coq; encapsulate G to keep track
+ of the extensions. *)
+
module Gram =
struct
include G
- let extend e pos rls =
- camlp4_state :=
- (ByGEXTEND ((fun () -> grammar_delete e pos None rls),
- (fun () -> G.extend e pos rls)))
- :: !camlp4_state;
- G.extend e pos rls
+ let extend e =
+ maybe_curry
+ (fun ext ->
+ camlp4_state :=
+ (ByEXTEND ((fun () -> grammar_delete e None ext),
+ (fun () -> maybe_uncurry (G.extend e) ext)))
+ :: !camlp4_state;
+ maybe_uncurry (G.extend e) ext)
let delete_rule e pil =
(* spiwack: if you use load an ML module which contains GDELETE_RULE
in a section, God kills a kitty. As it would corrupt remove_grammars.
There does not seem to be a good way to undo a delete rule. As deleting
takes fewer arguments than extending. The production rule isn't returned
by delete_rule. If we could retrieve the necessary information, then
- ByGEXTEND provides just the framework we need to allow this in section.
+ ByEXTEND provides just the framework we need to allow this in section.
I'm not entirely sure it makes sense, but at least it would be more correct.
*)
G.delete_rule e pil
end
+(** This extension command is used by the Grammar constr *)
-let camlp4_verbosity silent f x =
- let a = !Gramext.warning_verbose in
- Gramext.warning_verbose := silent;
- f x;
- Gramext.warning_verbose := a
+let grammar_extend e reinit ext =
+ camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
+ camlp4_verbose (maybe_uncurry (G.extend e)) ext
-(* This extension command is used by the Grammar constr *)
+(** Remove extensions
-let grammar_extend te pos reinit rls =
- camlp4_state := ByGrammar (weaken_entry te,pos,rls,reinit) :: !camlp4_state;
- camlp4_verbosity (Flags.is_verbose ()) (G.extend te pos) rls
-
-(* n is the number of extended entries (not the number of Grammar commands!)
+ [n] is the number of extended entries (not the number of Grammar commands!)
to remove. *)
+
let rec remove_grammars n =
if n>0 then
(match !camlp4_state with
| [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
- | ByGrammar(g,pos,rls,reinit)::t ->
- grammar_delete g pos reinit rls;
+ | ByGrammar(g,reinit,ext)::t ->
+ grammar_delete g reinit ext;
camlp4_state := t;
remove_grammars (n-1)
- | ByGEXTEND (undo,redo)::t ->
+ | ByEXTEND (undo,redo)::t ->
undo();
camlp4_state := t;
remove_grammars n;
redo();
- camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state)
+ camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+
+(** An entry that checks we reached the end of the input. *)
-(* 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
+ let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
GEXTEND Gram
e: [ [ x = en; EOI -> x ] ]
;
@@ -179,7 +226,7 @@ let eoi_entry en =
e
let map_entry f en =
- let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_map") in
+ let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
GEXTEND Gram
e: [ [ x = en -> f x ] ]
;
@@ -190,7 +237,7 @@ let map_entry f en =
(use eoi_entry) *)
let parse_string f x =
- let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
+ let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
type gram_universe = string * (string, typed_entry) Hashtbl.t
@@ -227,7 +274,7 @@ let get_entry_type (u, utab) s =
let new_entry etyp (u, utab) s =
if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
let ename = u ^ ":" ^ s in
- let e = in_typed_entry etyp (Gram.Entry.create ename) 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 =
@@ -246,10 +293,10 @@ let create_generic_entry s wit =
outGramObj wit (create_entry utactic s (unquote wit))
(* [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 *)
+(* For entries extensible only via the ML name, Gram.entry_create is enough *)
let make_gen_entry (u,univ) rawwit s =
- let e = Gram.Entry.create (u ^ ":" ^ s) in
+ let e = Gram.entry_create (u ^ ":" ^ s) in
Hashtbl.add univ s (inGramObj rawwit e); e
(* Initial grammar entries *)
@@ -258,35 +305,35 @@ module Prim =
struct
let gec_gen x = make_gen_entry uprim x
- (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ (* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic or vernac extensions *)
let preident = gec_gen rawwit_pre_ident "preident"
let ident = gec_gen rawwit_ident "ident"
let natural = gec_gen rawwit_int "natural"
let integer = gec_gen rawwit_int "integer"
- let bigint = Gram.Entry.create "Prim.bigint"
+ let bigint = Gram.entry_create "Prim.bigint"
let string = gec_gen rawwit_string "string"
let reference = make_gen_entry uprim rawwit_ref "reference"
- let by_notation = Gram.Entry.create "by_notation"
- let smart_global = Gram.Entry.create "smart_global"
+ let by_notation = Gram.entry_create "by_notation"
+ let smart_global = Gram.entry_create "smart_global"
(* parsed like ident but interpreted as a term *)
let var = gec_gen rawwit_var "var"
- let name = Gram.Entry.create "Prim.name"
- let identref = Gram.Entry.create "Prim.identref"
+ let name = Gram.entry_create "Prim.name"
+ let identref = Gram.entry_create "Prim.identref"
let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident"
- let pattern_identref = Gram.Entry.create "pattern_identref"
+ let pattern_identref = Gram.entry_create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
- let base_ident = Gram.Entry.create "Prim.base_ident"
+ let base_ident = Gram.entry_create "Prim.base_ident"
- let qualid = Gram.Entry.create "Prim.qualid"
- let fullyqualid = Gram.Entry.create "Prim.fullyqualid"
- let dirpath = Gram.Entry.create "Prim.dirpath"
+ let qualid = Gram.entry_create "Prim.qualid"
+ let fullyqualid = Gram.entry_create "Prim.fullyqualid"
+ let dirpath = Gram.entry_create "Prim.dirpath"
- let ne_string = Gram.Entry.create "Prim.ne_string"
- let ne_lstring = Gram.Entry.create "Prim.ne_lstring"
+ let ne_string = Gram.entry_create "Prim.ne_string"
+ let ne_lstring = Gram.entry_create "Prim.ne_lstring"
end
@@ -295,7 +342,7 @@ module Constr =
let gec_constr = make_gen_entry uconstr rawwit_constr
let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr)
- (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ (* Entries that can be refered via the string -> Gram.entry table *)
let constr = gec_constr "constr"
let operconstr = gec_constr "operconstr"
let constr_eoi = eoi_entry constr
@@ -304,30 +351,30 @@ module Constr =
let ident = make_gen_entry uconstr rawwit_ident "ident"
let global = make_gen_entry uconstr rawwit_ref "global"
let sort = make_gen_entry uconstr rawwit_sort "sort"
- let pattern = Gram.Entry.create "constr:pattern"
+ let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
- let binder = Gram.Entry.create "constr:binder"
- let binder_let = Gram.Entry.create "constr:binder_let"
- let binders_let = Gram.Entry.create "constr:binders_let"
- let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
- let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
- let record_declaration = Gram.Entry.create "constr:record_declaration"
- let appl_arg = Gram.Entry.create "constr:appl_arg"
+ let binder = Gram.entry_create "constr:binder"
+ let binder_let = Gram.entry_create "constr:binder_let"
+ let binders_let = Gram.entry_create "constr:binders_let"
+ let binders_let_fixannot = Gram.entry_create "constr:binders_let_fixannot"
+ let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
+ let record_declaration = Gram.entry_create "constr:record_declaration"
+ let appl_arg = Gram.entry_create "constr:appl_arg"
end
module Module =
struct
- let module_expr = Gram.Entry.create "module_expr"
- let module_type = Gram.Entry.create "module_type"
+ let module_expr = Gram.entry_create "module_expr"
+ let module_type = Gram.entry_create "module_type"
end
module Tactic =
struct
(* Main entry for extensions *)
- let simple_tactic = Gram.Entry.create "tactic:simple_tactic"
+ let simple_tactic = Gram.entry_create "tactic:simple_tactic"
- (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ (* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
@@ -346,9 +393,9 @@ module Tactic =
make_gen_entry utactic rawwit_intro_pattern "simple_intropattern"
(* 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_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 = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
@@ -359,7 +406,7 @@ module Tactic =
module Vernac_ =
struct
- let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
+ let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
(* The different kinds of vernacular commands *)
let gallina = gec_vernac "gallina"
@@ -370,7 +417,8 @@ module Vernac_ =
let vernac_eoi = eoi_entry vernac
(* Main vernac entry *)
- let main_entry = Gram.Entry.create "vernac"
+ let main_entry = Gram.entry_create "vernac"
+
GEXTEND Gram
main_entry:
[ [ a = vernac -> Some (loc,a) | EOI -> None ] ]
@@ -397,23 +445,23 @@ let main_entry = Vernac_.main_entry
let constr_level = string_of_int
let default_levels =
- [200,Gramext.RightA,false;
- 100,Gramext.RightA,false;
- 99,Gramext.RightA,true;
- 90,Gramext.RightA,false;
- 10,Gramext.RightA,false;
- 9,Gramext.RightA,false;
- 8,Gramext.RightA,true;
- 1,Gramext.LeftA,false;
- 0,Gramext.RightA,false]
+ [200,RightA,false;
+ 100,RightA,false;
+ 99,RightA,true;
+ 90,RightA,false;
+ 10,RightA,false;
+ 9,RightA,false;
+ 8,RightA,true;
+ 1,LeftA,false;
+ 0,RightA,false]
let default_pattern_levels =
- [200,Gramext.RightA,true;
- 100,Gramext.RightA,false;
- 99,Gramext.RightA,true;
- 10,Gramext.LeftA,false;
- 1,Gramext.LeftA,false;
- 0,Gramext.RightA,false]
+ [200,RightA,true;
+ 100,RightA,false;
+ 99,RightA,true;
+ 10,LeftA,false;
+ 1,LeftA,false;
+ 0,RightA,false]
let level_stack =
ref [(default_levels, default_pattern_levels)]
@@ -424,19 +472,19 @@ let level_stack =
open Ppextend
let admissible_assoc = function
- | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
- | Gramext.RightA, Some Gramext.LeftA -> false
+ | LeftA, Some (RightA | NonA) -> false
+ | RightA, Some LeftA -> false
| _ -> true
let create_assoc = function
- | None -> Gramext.RightA
+ | None -> RightA
| Some a -> a
let error_level_assoc p current expected =
let pr_assoc = function
- | Gramext.LeftA -> str "left"
- | Gramext.RightA -> str "right"
- | Gramext.NonA -> str "non" in
+ | LeftA -> str "left"
+ | RightA -> str "right"
+ | NonA -> str "non" in
errorlabstrm ""
(str "Level " ++ int p ++ str " is already declared " ++
pr_assoc current ++ str " associative while it is now expected to be " ++
@@ -470,18 +518,18 @@ let find_position_gen forpat ensure assoc lev =
let assoc = create_assoc assoc in
if !init = None then
(* Create the entry *)
- (if !after = None then Some Gramext.First
- else Some (Gramext.After (constr_level (Option.get !after)))),
+ (if !after = None then Some First
+ else Some (After (constr_level (Option.get !after)))),
Some assoc, Some (constr_level n), None
else
(* The reinit flag has been updated *)
- Some (Gramext.Level (constr_level n)), None, None, !init
+ Some (Level (constr_level n)), None, None, !init
with
(* Nothing has changed *)
Exit ->
level_stack := current :: !level_stack;
(* Just inherit the existing associativity and name (None) *)
- Some (Gramext.Level (constr_level n)), None, None, None
+ Some (Level (constr_level n)), None, None, None
let remove_levels n =
level_stack := list_skipn n !level_stack
@@ -510,8 +558,8 @@ let synchronize_level_positions () =
(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
let camlp4_assoc = function
- | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA
- | None | Some Gramext.LeftA -> Gramext.LeftA
+ | Some NonA | Some RightA -> RightA
+ | None | Some LeftA -> LeftA
(* [adjust_level assoc from prod] where [assoc] and [from] are the name
and associativity of the level where to add the rule; the meaning of
@@ -526,20 +574,20 @@ let adjust_level assoc from = function
| (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
(* Compute production name on the right side *)
(* If NonA or LeftA on the right-hand side, set to NEXT *)
- | (NumLevel n,BorderProd (Right,Some (Gramext.NonA|Gramext.LeftA))) ->
+ | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
Some None
(* If RightA on the right-hand side, set to the explicit (current) level *)
- | (NumLevel n,BorderProd (Right,Some Gramext.RightA)) ->
+ | (NumLevel n,BorderProd (Right,Some RightA)) ->
Some (Some (n,true))
(* Compute production name on the left side *)
(* If NonA on the left-hand side, adopt the current assoc ?? *)
- | (NumLevel n,BorderProd (Left,Some Gramext.NonA)) -> None
+ | (NumLevel n,BorderProd (Left,Some NonA)) -> None
(* If the expected assoc is the current one, set to SELF *)
| (NumLevel n,BorderProd (Left,Some a)) when a = camlp4_assoc assoc ->
None
(* Otherwise, force the level, n or n-1, according to expected assoc *)
| (NumLevel n,BorderProd (Left,Some a)) ->
- if a = Gramext.LeftA then Some (Some (n,true)) else Some None
+ if a = LeftA then Some (Some (n,true)) else Some None
(* None means NEXT *)
| (NextLevel,_) -> Some None
(* Compute production name elsewhere *)
@@ -585,7 +633,7 @@ let interp_constr_prod_entry_key ass from forpat en =
let is_self from e =
match from, e with
ETConstr(n,()), ETConstr(NumLevel n',
- BorderProd(Right, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false
+ BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false
| ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> n=n'
| (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
| ETPattern, ETPattern) -> true
@@ -601,57 +649,60 @@ let is_binder_level from e =
let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
if is_binder_level from typ then
if forpat then
- Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200")
+ Snterml (Gram.Entry.obj Constr.pattern,"200")
else
- Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
+ Snterml (Gram.Entry.obj Constr.operconstr,"200")
else if is_self from typ then
- Gramext.Sself
+ Sself
else
match typ with
| ETConstrList (typ',[]) ->
- Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+ Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
| ETConstrList (typ',tkl) ->
- Gramext.Slist1sep
+ Slist1sep
(symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
- Gramext.srules
+ Gram.srules'
[List.map gram_token_of_token tkl,
- List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
- (Gramext.action (fun loc -> ()))])
+ List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
+ (Gram.action (fun loc -> ()))])
| _ ->
match interp_constr_prod_entry_key assoc from forpat typ with
- | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
- | (eobj,Some None,_) -> Gramext.Snext
+ | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
+ | (eobj,Some None,_) -> Snext
| (eobj,Some (Some (lev,cur)),_) ->
- Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
+ Snterml (Gram.Entry.obj eobj,constr_level lev)
-(**********************************************************************)
-(* Binding general entry keys to symbol *)
+(** Binding general entry keys to symbol *)
let rec symbol_of_prod_entry_key = function
- | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
+ | Alist1 s -> Slist1 (symbol_of_prod_entry_key s)
| Alist1sep (s,sep) ->
- Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
- | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
+ Slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Alist0 s -> Slist0 (symbol_of_prod_entry_key s)
| Alist0sep (s,sep) ->
- Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
- | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
+ Slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
+ | Aopt s -> Sopt (symbol_of_prod_entry_key s)
| Amodifiers s ->
- Gramext.srules
- [([], Gramext.action(fun _loc -> []));
+ Gram.srules'
+ [([], Gram.action (fun _loc -> []));
([gram_token_of_string "(";
- Gramext.Slist1sep ((symbol_of_prod_entry_key s), gram_token_of_string ",");
+ Slist1sep ((symbol_of_prod_entry_key s), gram_token_of_string ",");
gram_token_of_string ")"],
- Gramext.action (fun _ l _ _loc -> l))]
- | Aself -> Gramext.Sself
- | Anext -> Gramext.Snext
- | Atactic 5 -> Gramext.Snterm (Gram.Entry.obj Tactic.binder_tactic)
+ Gram.action (fun _ l _ _loc -> l))]
+ | Aself -> Sself
+ | Anext -> Snext
+ | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
| Atactic n ->
- Gramext.Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
- | Agram s -> Gramext.Snterm s
+ Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
+ | Agram s -> Snterm s
| Aentry (u,s) ->
- Gramext.Snterm (Gram.Entry.obj
+ Snterm (Gram.Entry.obj
(object_of_typed_entry (get_entry (get_univ u) s)))
+let level_of_snterml = function
+ | Snterml (_,l) -> int_of_string l
+ | _ -> failwith "level_of_snterml"
+
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ada016094..3ec149256 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -15,13 +15,13 @@ open Genarg
open Topconstr
open Tacexpr
open Libnames
+open Compat
(** The parser of Coq *)
-module Gram : Grammar.S with type te = Tok.t
+module Gram : GrammarSig
-(**
- The parser of Coq is built from three kinds of rule declarations:
+(** The parser of Coq is built from three kinds of rule declarations:
- dynamic rules declared at the evaluation of Coq files (using
e.g. Notation, Infix, or Tactic Notation)
@@ -96,24 +96,17 @@ module Gram : Grammar.S with type te = Tok.t
*)
-val gram_token_of_token : Tok.t -> Tok.t Gramext.g_symbol
-val gram_token_of_string : string -> Tok.t Gramext.g_symbol
+val gram_token_of_token : Tok.t -> Gram.symbol
+val gram_token_of_string : string -> Gram.symbol
(** The superclass of all grammar entries *)
type grammar_object
-type camlp4_rule =
- Tok.t Gramext.g_symbol list * Gramext.g_action
-
-type camlp4_entry_rules =
- (** first two parameters are name and assoc iff a level is created *)
- string option * Gramext.g_assoc option * camlp4_rule list
-
(** Add one extension at some camlp4 position of some camlp4 entry *)
val grammar_extend :
- grammar_object Gram.Entry.e -> Gramext.position option ->
- (** for reinitialization if ever needed: *) Gramext.g_assoc option ->
- camlp4_entry_rules list -> unit
+ grammar_object Gram.entry ->
+ gram_assoc option (** for reinitialization if ever needed *) ->
+ Gram.extend_statment -> unit
(** Remove the last n extensions *)
val remove_grammars : int -> unit
@@ -128,8 +121,8 @@ type typed_entry
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.e
-val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
+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 *)
@@ -137,9 +130,9 @@ val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
(** Parse a string *)
-val parse_string : 'a Gram.Entry.e -> string -> 'a
-val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
-val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
+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 *)
@@ -161,130 +154,152 @@ val get_entry_type : gram_universe -> string -> entry_type
val create_entry : gram_universe -> string -> entry_type -> typed_entry
val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
- 'a Gram.Entry.e
+ 'a Gram.entry
module Prim :
sig
open Util
open Names
open Libnames
- val preident : string Gram.Entry.e
- val ident : identifier Gram.Entry.e
- val name : name located Gram.Entry.e
- val identref : identifier located Gram.Entry.e
- val pattern_ident : identifier Gram.Entry.e
- val pattern_identref : identifier located Gram.Entry.e
- val base_ident : identifier Gram.Entry.e
- val natural : int Gram.Entry.e
- val bigint : Bigint.bigint Gram.Entry.e
- val integer : int Gram.Entry.e
- val string : string Gram.Entry.e
- val qualid : qualid located Gram.Entry.e
- val fullyqualid : identifier list located Gram.Entry.e
- val reference : reference Gram.Entry.e
- val by_notation : (loc * string * string option) Gram.Entry.e
- val smart_global : reference or_by_notation Gram.Entry.e
- val dirpath : dir_path Gram.Entry.e
- val ne_string : string Gram.Entry.e
- val ne_lstring : string located Gram.Entry.e
- val var : identifier located Gram.Entry.e
+ val preident : string Gram.entry
+ val ident : identifier Gram.entry
+ val name : name located Gram.entry
+ val identref : identifier located Gram.entry
+ val pattern_ident : identifier Gram.entry
+ val pattern_identref : identifier located Gram.entry
+ val base_ident : identifier Gram.entry
+ val natural : int Gram.entry
+ val bigint : Bigint.bigint Gram.entry
+ val integer : int Gram.entry
+ val string : string Gram.entry
+ val qualid : qualid located Gram.entry
+ val fullyqualid : identifier list located Gram.entry
+ val reference : reference Gram.entry
+ val by_notation : (loc * string * string option) Gram.entry
+ val smart_global : reference or_by_notation Gram.entry
+ val dirpath : dir_path Gram.entry
+ val ne_string : string Gram.entry
+ val ne_lstring : string located Gram.entry
+ val var : identifier located Gram.entry
end
module Constr :
sig
- val constr : constr_expr Gram.Entry.e
- val constr_eoi : constr_expr Gram.Entry.e
- val lconstr : constr_expr Gram.Entry.e
- val binder_constr : constr_expr Gram.Entry.e
- val operconstr : constr_expr Gram.Entry.e
- val ident : identifier Gram.Entry.e
- val global : reference Gram.Entry.e
- val sort : rawsort Gram.Entry.e
- val pattern : cases_pattern_expr Gram.Entry.e
- val constr_pattern : constr_expr Gram.Entry.e
- val lconstr_pattern : constr_expr Gram.Entry.e
- val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
- val binder_let : local_binder list Gram.Entry.e
- val binders_let : local_binder list Gram.Entry.e
- val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
- val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
- val record_declaration : constr_expr Gram.Entry.e
- val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
+ val constr : constr_expr Gram.entry
+ val constr_eoi : constr_expr Gram.entry
+ val lconstr : constr_expr Gram.entry
+ val binder_constr : constr_expr Gram.entry
+ val operconstr : constr_expr Gram.entry
+ val ident : identifier Gram.entry
+ val global : reference Gram.entry
+ val sort : rawsort Gram.entry
+ val pattern : cases_pattern_expr Gram.entry
+ val constr_pattern : constr_expr Gram.entry
+ val lconstr_pattern : constr_expr Gram.entry
+ val binder : (name located list * binder_kind * constr_expr) Gram.entry
+ val binder_let : local_binder list Gram.entry
+ val binders_let : local_binder list Gram.entry
+ val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
+ val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
+ val record_declaration : constr_expr Gram.entry
+ val appl_arg : (constr_expr * explicitation located option) Gram.entry
end
module Module :
sig
- val module_expr : module_ast Gram.Entry.e
- val module_type : module_ast Gram.Entry.e
+ val module_expr : module_ast Gram.entry
+ val module_type : module_ast Gram.entry
end
module Tactic :
sig
open Rawterm
- val open_constr : open_constr_expr Gram.Entry.e
- val casted_open_constr : open_constr_expr Gram.Entry.e
- val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
- val bindings : constr_expr bindings Gram.Entry.e
- val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.Entry.e
- val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
- val int_or_var : int or_var Gram.Entry.e
- val red_expr : raw_red_expr Gram.Entry.e
- val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
- val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e
- val tactic_arg : raw_tactic_arg Gram.Entry.e
- val tactic_expr : raw_tactic_expr Gram.Entry.e
- val binder_tactic : raw_tactic_expr Gram.Entry.e
- val tactic : raw_tactic_expr Gram.Entry.e
- val tactic_eoi : raw_tactic_expr Gram.Entry.e
+ val open_constr : open_constr_expr Gram.entry
+ val casted_open_constr : open_constr_expr Gram.entry
+ val constr_with_bindings : constr_expr with_bindings Gram.entry
+ val bindings : constr_expr bindings Gram.entry
+ val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+ val quantified_hypothesis : quantified_hypothesis Gram.entry
+ val int_or_var : int or_var Gram.entry
+ val red_expr : raw_red_expr Gram.entry
+ val simple_tactic : raw_atomic_tactic_expr Gram.entry
+ val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry
+ val tactic_arg : raw_tactic_arg Gram.entry
+ val tactic_expr : raw_tactic_expr Gram.entry
+ val binder_tactic : raw_tactic_expr Gram.entry
+ val tactic : raw_tactic_expr Gram.entry
+ val tactic_eoi : raw_tactic_expr Gram.entry
end
module Vernac_ :
sig
open Decl_kinds
- val gallina : vernac_expr Gram.Entry.e
- val gallina_ext : vernac_expr Gram.Entry.e
- val command : vernac_expr Gram.Entry.e
- val syntax : vernac_expr Gram.Entry.e
- val vernac : vernac_expr Gram.Entry.e
- val vernac_eoi : vernac_expr Gram.Entry.e
+ val gallina : vernac_expr Gram.entry
+ val gallina_ext : vernac_expr Gram.entry
+ val command : vernac_expr Gram.entry
+ val syntax : vernac_expr Gram.entry
+ val vernac : vernac_expr Gram.entry
+ val vernac_eoi : vernac_expr Gram.entry
end
(** The main entry: reads an optional vernac command *)
-val main_entry : (loc * vernac_expr) option Gram.Entry.e
+val main_entry : (loc * vernac_expr) option Gram.entry
(** 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.e * int option
+ constr_entry_key -> grammar_object Gram.entry * int option
-val symbol_of_constr_prod_entry_key : Gramext.g_assoc option ->
+val symbol_of_constr_prod_entry_key : gram_assoc option ->
constr_entry_key -> bool -> constr_prod_entry_key ->
- Tok.t Gramext.g_symbol
+ Gram.symbol
+
+(** 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 Gram.internal_entry
+ | Aentry of string * string
(** Binding general entry keys to symbols *)
val symbol_of_prod_entry_key :
- Gram.te prod_entry_key -> Gram.te Gramext.g_symbol
+ prod_entry_key -> Gram.symbol
(** Interpret entry names of the form "ne_constr_list" as entry keys *)
val interp_entry_name : bool (** true to fail on unknown entry *) ->
- int option -> string -> string -> entry_type * Gram.te prod_entry_key
+ int option -> string -> string -> entry_type * prod_entry_key
(** Registering/resetting the level of a constr entry *)
val find_position :
bool (** true if for creation in pattern entry; false if in constr entry *) ->
- Gramext.g_assoc option -> int option ->
- Gramext.position option * Gramext.g_assoc option * string option *
- (** for reinitialization: *) Gramext.g_assoc option
+ gram_assoc option -> int option ->
+ gram_position option * gram_assoc option * string option *
+ (** for reinitialization: *) gram_assoc option
val synchronize_level_positions : unit -> unit
val register_empty_levels : bool -> int list ->
- (Gramext.position option * Gramext.g_assoc option *
- string option * Gramext.g_assoc option) list
+ (gram_position option * gram_assoc option *
+ string option * gram_assoc option) list
val remove_levels : int -> unit
+
+val level_of_snterml : Gram.symbol -> int
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a120253c1..5d21d26d8 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -10,6 +10,7 @@ open Pp
open Names
open Nameops
open Nametab
+open Compat
open Util
open Extend
open Vernacexpr
@@ -93,15 +94,15 @@ let pr_ne_sep sep pr = function
| l -> sep() ++ pr l
let pr_entry_prec = function
- | Some Gramext.LeftA -> str"LEFTA "
- | Some Gramext.RightA -> str"RIGHTA "
- | Some Gramext.NonA -> str"NONA "
+ | Some LeftA -> str"LEFTA "
+ | Some RightA -> str"RIGHTA "
+ | Some NonA -> str"NONA "
| None -> mt()
let pr_prec = function
- | Some Gramext.LeftA -> str", left associativity"
- | Some Gramext.RightA -> str", right associativity"
- | Some Gramext.NonA -> str", no associativity"
+ | Some LeftA -> str", left associativity"
+ | Some RightA -> str", right associativity"
+ | Some NonA -> str", no associativity"
| None -> mt()
let pr_set_entry_type = function
@@ -398,9 +399,9 @@ let pr_syntax_modifier = function
prlist_with_sep sep_v2 str l ++
spc() ++ str"at level" ++ spc() ++ int n
| SetLevel n -> str"at level" ++ spc() ++ int n
- | SetAssoc Gramext.LeftA -> str"left associativity"
- | SetAssoc Gramext.RightA -> str"right associativity"
- | SetAssoc Gramext.NonA -> str"no associativity"
+ | SetAssoc LeftA -> str"left associativity"
+ | SetAssoc RightA -> str"right associativity"
+ | SetAssoc NonA -> str"no associativity"
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
| SetOnlyParsing -> str"only parsing"
| SetFormat s -> str"format " ++ pr_located qs s
@@ -778,7 +779,7 @@ let rec pr_vernac = function
(match b with None -> mt () | Some Dash -> str"-" | Some Star -> str"*" | Some Plus -> str"+") ++
pr_raw_tactic tac
++ (try if deftac then str ".." else mt ()
- with UserError _|Stdpp.Exc_located _ -> mt())
+ with UserError _|Loc.Exc_located _ -> mt())
| VernacSolveExistential (i,c) ->
str"Existential " ++ int i ++ pr_lconstrarg c
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 4c86e4415..fb34a5aa2 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -12,7 +12,9 @@ open Names
open Pattern
open Q_util
open Util
+open Compat
open Pcaml
+open PcamlSig
let loc = dummy_loc
let dloc = <:expr< Util.dummy_loc >>
@@ -40,7 +42,7 @@ EXTEND
[ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ]
;
string:
- [ [ UIDENT | LIDENT ] ]
+ [ [ s = UIDENT -> s | s = LIDENT -> s ] ]
;
constr:
[ "200" RIGHTA
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6d3e8e03a..d78486a0b 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -10,6 +10,7 @@ open Util
open Names
open Libnames
open Q_util
+open Compat
let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -18,9 +19,7 @@ let purge_str s =
else String.sub s 1 (String.length s - 1)
let anti loc x =
- let e = <:expr< $lid:purge_str x$ >>
- in
- <:expr< $anti:e$ >>
+ expl_anti loc <:expr< $lid:purge_str x$ >>
(* We don't give location for tactic quotation! *)
let loc = dummy_loc
@@ -411,12 +410,6 @@ let rec mlexpr_of_atomic_tactic = function
let lems = mlexpr_of_list mlexpr_of_constr lems in
<:expr< Tacexpr.TacTrivial $lems$ $l$ >>
-(*
- | Tacexpr.TacExtend (s,l) ->
- let l = mlexpr_of_list mlexpr_of_tactic_arg l in
- let $dloc$ = MLast.loc_of_expr l in
- <:expr< Tacexpr.TacExtend $mlexpr_of_string s$ $l$ >>
-*)
| _ -> failwith "Quotation of atomic tactic expressions: TODO"
and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
@@ -492,18 +485,47 @@ and mlexpr_of_tactic_arg = function
<:expr< Tacexpr.Reference $mlexpr_of_reference r$ >>
| _ -> failwith "mlexpr_of_tactic_arg: TODO"
+
+IFDEF CAMLP5 THEN
+
+let not_impl x =
+ let desc =
+ if Obj.is_block (Obj.repr x) then
+ "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
+ else "int_val = " ^ string_of_int (Obj.magic x)
+ in
+ failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc)
+
+(* The following function is written without quotation
+ in order to be parsable even by camlp4. The version with
+ quotation can be found in revision <= 12972 of [q_util.ml4] *)
+
+open MLast
+
+let rec patt_of_expr e =
+ let loc = loc_of_expr e in
+ match e with
+ | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2)
+ | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2)
+ | ExLid (_, "loc") -> PaAny loc
+ | ExLid (_, s) -> PaLid (loc, s)
+ | ExUid (_, s) -> PaUid (loc, s)
+ | ExStr (_, s) -> PaStr (loc, s)
+ | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e)
+ | _ -> not_impl e
+
let fconstr e =
let ee s =
- mlexpr_of_constr (Pcoq.Gram.Entry.parse e
- (Pcoq.Gram.parsable (Stream.of_string s)))
+ mlexpr_of_constr (Pcoq.Gram.entry_parse e
+ (Pcoq.Gram.parsable (Stream.of_string s)))
in
let ep s = patt_of_expr (ee s) in
Quotation.ExAst (ee, ep)
let ftac e =
let ee s =
- mlexpr_of_tactic (Pcoq.Gram.Entry.parse e
- (Pcoq.Gram.parsable (Stream.of_string s)))
+ mlexpr_of_tactic (Pcoq.Gram.entry_parse e
+ (Pcoq.Gram.parsable (Stream.of_string s)))
in
let ep s = patt_of_expr (ee s) in
Quotation.ExAst (ee, ep)
@@ -512,3 +534,23 @@ let _ =
Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi);
Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi);
Quotation.default := "constr"
+
+ELSE
+
+open Pcaml
+
+let expand_constr_quot_expr loc _loc_name_opt contents =
+ mlexpr_of_constr
+ (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents)
+
+let expand_tactic_quot_expr loc _loc_name_opt contents =
+ mlexpr_of_tactic
+ (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents)
+
+let _ =
+ (* FIXME: for the moment, we add quotations in expressions only, not pattern *)
+ Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr;
+ Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr;
+ Quotation.default := "constr"
+
+END
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 94319cc73..f90de041a 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -8,30 +8,9 @@
(* This file defines standard combinators to build ml expressions *)
-open Util
open Extrawit
-open Pcoq
-
-let not_impl name x =
- let desc =
- if Obj.is_block (Obj.repr x) then
- "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
- else
- "int_val = " ^ string_of_int (Obj.magic x)
- in
- failwith ("<Q_util." ^ name ^ ", not impl: " ^ desc)
-
-let rec patt_of_expr e =
- let loc = MLast.loc_of_expr e in
- match e with
- | <:expr< $e1$.$e2$ >> -> <:patt< $patt_of_expr e1$.$patt_of_expr e2$ >>
- | <:expr< $e1$ $e2$ >> -> <:patt< $patt_of_expr e1$ $patt_of_expr e2$ >>
- | <:expr< loc >> -> <:patt< _ >>
- | <:expr< $lid:s$ >> -> <:patt< $lid:s$ >>
- | <:expr< $uid:s$ >> -> <:patt< $uid:s$ >>
- | <:expr< $str:s$ >> -> <:patt< $str:s$ >>
- | <:expr< $anti:e$ >> -> <:patt< $anti:patt_of_expr e$ >>
- | _ -> not_impl "patt_of_expr" e
+open Compat
+open Util
let mlexpr_of_list f l =
List.fold_right
@@ -77,15 +56,15 @@ open Pcoq
open Genarg
let rec mlexpr_of_prod_entry_key = function
- | Extend.Alist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Alist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Alist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Alist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Aopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key s$ >>
- | Extend.Amodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key s$ >>
- | Extend.Aself -> <:expr< Extend.Aself >>
- | Extend.Anext -> <:expr< Extend.Anext >>
- | Extend.Atactic n -> <:expr< Extend.Atactic $mlexpr_of_int n$ >>
- | Extend.Agram s -> anomaly "Agram not supported"
- | Extend.Aentry ("",s) -> <:expr< Extend.Agram (Gram.Entry.obj $lid:s$) >>
- | Extend.Aentry (u,s) -> <:expr< Extend.Aentry $str:u$ $str:s$ >>
+ | Alist1 s -> <:expr< Alist1 $mlexpr_of_prod_entry_key s$ >>
+ | Alist1sep (s,sep) -> <:expr< Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+ | Alist0 s -> <:expr< Alist0 $mlexpr_of_prod_entry_key s$ >>
+ | Alist0sep (s,sep) -> <:expr< Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+ | Aopt s -> <:expr< Aopt $mlexpr_of_prod_entry_key s$ >>
+ | Amodifiers s -> <:expr< Amodifiers $mlexpr_of_prod_entry_key s$ >>
+ | Aself -> <:expr< Aself >>
+ | Anext -> <:expr< Anext >>
+ | Atactic n -> <:expr< Atactic $mlexpr_of_int n$ >>
+ | Agram s -> Util.anomaly "Agram not supported"
+ | Aentry ("",s) -> <:expr< Agram (Gram.Entry.obj $lid:s$) >>
+ | Aentry (u,s) -> <:expr< Aentry $str:u$ $str:s$ >>
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 59b3f334c..c19a0ecf5 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -6,7 +6,7 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
-val patt_of_expr : MLast.expr -> MLast.patt
+open Compat
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr
@@ -30,4 +30,4 @@ val mlexpr_of_string : string -> MLast.expr
val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
-val mlexpr_of_prod_entry_key : Pcoq.Gram.te Extend.prod_entry_key -> MLast.expr
+val mlexpr_of_prod_entry_key : Pcoq.prod_entry_key -> MLast.expr
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index fb1425e0e..f64c8f700 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -14,6 +14,7 @@ open Argextend
open Pcoq
open Extrawit
open Egrammar
+open Compat
let rec make_patt = function
| [] -> <:patt< [] >>
@@ -48,11 +49,6 @@ let rec make_let e = function
<:expr< let $lid:p$ = $v$ in $e$ >>
| _::l -> make_let e l
-let add_clause s (pt,e) l =
- let p = make_patt pt in
- let w = Some (make_when (MLast.loc_of_expr e) pt) in
- (p, w, make_let e pt)::l
-
let rec extract_signature = function
| [] -> []
| GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
@@ -65,11 +61,14 @@ let check_unicity s l =
("Two distinct rules of tactic entry "^s^" have the same\n"^
"non-terminals in the same order: put them in distinct tactic entries")
-let make_clauses s l =
+let make_clause (pt,e) =
+ (make_patt pt,
+ Some (make_when (MLast.loc_of_expr e) pt),
+ make_let e pt)
+
+let make_fun_clauses loc s l =
check_unicity s l;
- let default =
- (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
- List.fold_right (add_clause s) l [default]
+ Compat.make_fun loc (List.map make_clause l)
let rec make_args = function
| [] -> <:expr< [] >>
@@ -160,13 +159,11 @@ let declare_tactic loc s cl =
let atomic_tactics =
mlexpr_of_list mlexpr_of_string
(List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
- <:str_item<
- declare
- open Pcoq;
- open Extrawit;
- declare $list:hidden$ end;
+ declare_str_items loc
+ (hidden @
+ [ <:str_item< do {
try
- let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
+ let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
List.iter
(fun s -> Tacinterp.add_primitive_tactic s
(Tacexpr.TacAtom($default_loc$,
@@ -174,16 +171,16 @@ let declare_tactic loc s cl =
$atomic_tactics$
with e -> Pp.pp (Cerrors.explain_exn e);
Egrammar.extend_tactic_grammar $se$ $gl$;
- List.iter Pptactic.declare_extra_tactic_pprule $pp$;
- end
- >>
+ List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
+ ])
open Pcaml
+open PcamlSig
EXTEND
GLOBAL: str_item;
str_item:
- [ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
+ [ [ "TACTIC"; "EXTEND"; s = tac_name;
OPT "|"; l = LIST1 tacrule SEP "|";
"END" ->
declare_tactic loc s l ] ]
@@ -209,5 +206,10 @@ EXTEND
GramTerminal s
] ]
;
+ tac_name:
+ [ [ s = LIDENT -> s
+ | s = UIDENT -> s
+ ] ]
+ ;
END
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index d8b6fba31..1fa0e7e99 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -14,6 +14,7 @@ open Argextend
open Tacextend
open Pcoq
open Egrammar
+open Compat
let rec make_let e = function
| [] -> e
@@ -24,11 +25,6 @@ let rec make_let e = function
<:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
| _::l -> make_let e l
-let add_clause s (_,pt,e) l =
- let p = make_patt pt in
- let w = Some (make_when (MLast.loc_of_expr e) pt) in
- (p, w, make_let e pt)::l
-
let check_unicity s l =
let l' = List.map (fun (_,l,_) -> extract_signature l) l in
if not (Util.list_distinct l') then
@@ -36,11 +32,14 @@ let check_unicity s l =
("Two distinct rules of entry "^s^" have the same\n"^
"non-terminals in the same order: put them in distinct vernac entries")
-let make_clauses s l =
+let make_clause (_,pt,e) =
+ (make_patt pt,
+ Some (make_when (MLast.loc_of_expr e) pt),
+ make_let e pt)
+
+let make_fun_clauses loc s l =
check_unicity s l;
- let default =
- (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
- List.fold_right (add_clause s) l [default]
+ Compat.make_fun loc (List.map make_clause l)
let mlexpr_of_clause =
mlexpr_of_list
@@ -49,18 +48,16 @@ let mlexpr_of_clause =
let declare_command loc s nt cl =
let gl = mlexpr_of_clause cl in
- let icl = make_clauses s cl in
- <:str_item<
- declare
- open Pcoq;
- open Extrawit;
- try Vernacinterp.vinterp_add $mlexpr_of_string s$ (fun [ $list:icl$ ])
- with e -> Pp.pp (Cerrors.explain_exn e);
- Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$;
- end
- >>
+ let funcl = make_fun_clauses loc s cl in
+ declare_str_items loc
+ [ <:str_item< do {
+ try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$
+ with e -> Pp.pp (Cerrors.explain_exn e);
+ Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$
+ } >> ]
open Pcaml
+open PcamlSig
EXTEND
GLOBAL: str_item;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 19:39:16 +0000