diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 432 |
1 files changed, 237 insertions, 195 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ff5213ef..075440f1 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -1,77 +1,96 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) - -(*i $Id: pcoq.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp +open Compat +open Tok open Util open Names open Extend open Libnames -open Rawterm +open Glob_term open Topconstr open Genarg 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 = string * string - let lexer = Lexer.lexer - end +(** Compatibility with Camlp5 6.x *) -module G = Grammar.GMake(L) +IFDEF CAMLP5_6_00 THEN +let slist0sep x y = Slist0sep (x, y, false) +let slist1sep x y = Slist1sep (x, y, false) +ELSE +let slist0sep x y = Slist0sep (x, y) +let slist1sep x y = Slist1sep (x, y) +END +let gram_token_of_token tok = +IFDEF CAMLP5 THEN + Stoken (Tok.to_pattern tok) ELSE + match tok with + | KEYWORD s -> Skeyword s + | tok -> Stoken ((=) tok, to_string tok) +END -module L = - struct - let lexer = Lexer.lexer - end +let gram_token_of_string s = gram_token_of_token (Lexer.terminal s) -module G = Grammar.Make(L) +let camlp4_verbosity silent f x = + let a = !warning_verbose in + warning_verbose := silent; + f x; + warning_verbose := a -END +let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x -let grammar_delete e pos reinit rls = - List.iter - (fun (n,ass,lev) -> - (* 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. *) +(** General entry keys *) - 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,[]]; +(** 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 G.internal_entry + | Aentry of string * string + +(** [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 = @@ -80,9 +99,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 @@ -91,8 +112,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 = @@ -107,82 +128,107 @@ end open Gramtypes -type camlp4_rule = - Compat.token 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 -IFDEF CAMLP5_6_02_1 THEN -let entry_print x = Gram.Entry.print !Pp_control.std_ft x -ELSE -let entry_print = Gram.Entry.print -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 - -(* This extension command is used by the Grammar constr *) +let grammar_extend e reinit ext = + camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) ext -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 +(** Remove extensions -(* 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 ] ] ; @@ -190,7 +236,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 ] ] ; @@ -201,7 +247,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 @@ -228,17 +274,10 @@ let get_univ s = let get_entry (u, utab) s = Hashtbl.find utab s -let get_entry_type (u, utab) s = - try - type_of_typed_entry (get_entry (u, utab) s) - with Not_found -> - errorlabstrm "Pcoq.get_entry" - (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") - 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 = @@ -257,10 +296,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 *) @@ -269,44 +308,43 @@ 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 module Constr = struct 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 @@ -315,31 +353,31 @@ 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 closed_binder = Gram.Entry.create "constr:closed_binder" - let binder = Gram.Entry.create "constr:binder" - let binders = Gram.Entry.create "constr:binders" - let open_binders = Gram.Entry.create "constr:open_binders" - let binders_fixannot = Gram.Entry.create "constr:binders_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 closed_binder = Gram.entry_create "constr:closed_binder" + let binder = Gram.entry_create "constr:binder" + let binders = Gram.entry_create "constr:binders" + let open_binders = Gram.entry_create "constr:open_binders" + let binders_fixannot = Gram.entry_create "constr:binders_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" @@ -358,9 +396,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" @@ -371,7 +409,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" @@ -379,12 +417,11 @@ module Vernac_ = let command = gec_vernac "command" let syntax = gec_vernac "syntax_command" let vernac = gec_vernac "Vernac.vernac" - let proof_instr = Gram.Entry.create "proofmode:instr" - let vernac_eoi = eoi_entry vernac - + let rec_definition = gec_vernac "Vernac.rec_definition" (* 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 ] ] @@ -411,23 +448,24 @@ 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; + 9,RightA,false; + 1,LeftA,false; + 0,RightA,false] let level_stack = ref [(default_levels, default_pattern_levels)] @@ -438,19 +476,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 " ++ @@ -484,18 +522,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 @@ -524,8 +562,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 @@ -540,20 +578,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 *) @@ -604,7 +642,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 @@ -618,69 +656,73 @@ let is_binder_level from e = | _ -> false let make_sep_rules tkl = - Gramext.srules - [List.map (fun x -> Gramext.Stoken x) tkl, - List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl - (Gramext.action (fun loc -> ()))] + Gram.srules' + [List.map gram_token_of_token tkl, + List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl + (Gram.action (fun loc -> ()))] 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) -> - Compat.slist1sep + slist1sep (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) (make_sep_rules tkl) | ETBinderList (false,[]) -> - Gramext.Slist1 + Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) | ETBinderList (false,tkl) -> - Compat.slist1sep + slist1sep (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) (make_sep_rules tkl) + | _ -> match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> 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) -> - Compat.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) -> - Compat.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 -> [])); - ([Gramext.Stoken ("", "("); - Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ",")); - Gramext.Stoken ("", ")")], - Gramext.action (fun _ l _ _loc -> l))] - | Aself -> Gramext.Sself - | Anext -> Gramext.Snext - | Atactic 5 -> Gramext.Snterm (Gram.Entry.obj Tactic.binder_tactic) + Gram.srules' + [([], Gram.action (fun _loc -> [])); + ([gram_token_of_string "("; + slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ","); + gram_token_of_string ")"], + Gram.action (fun _ l _ _loc -> l))] + | Aself -> Sself + | Anext -> Snext + | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic) | Atactic n -> - 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 *) |