aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
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-26 14:49:27 +0000