diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-27 13:43:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-27 13:43:41 +0000 |
| commit | f90fde30288f67b167b68bfd32363eaa20644c5f (patch) | |
| tree | 00faf9b0c6aa8749d3ec67b8fdc4f14044535b1c | |
| parent | 3f40ddb52ed52ea1e1939feaecf952269335500f (diff) | |
- Cleaning (unification of ML names, removal of obsolete code,
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
35 files changed, 742 insertions, 701 deletions
@@ -18,6 +18,10 @@ Tactics - Tactic "tauto" now proves classical tautologies as soon as classical logic (i.e. library Classical_Prop or Classical) is loaded. +Tactic Language + +- Support for parsing non-empty lists with separators in tactic notations. + Vernacular commands - New command "Timeout <n> <command>." interprets a command and a timeout diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a9673664a..c82e1e652 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,10 @@ = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= +** Cleaning in parsing extensions (commit ) + +Many moves and renamings, one new file (Extrawit, that contains wit_tactic). + ** Cleaning in tactical.mli tclLAST_HYP -> onLastHyp diff --git a/dev/printers.mllib b/dev/printers.mllib index 25ec05fba..f4b3d7f6c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -112,6 +112,7 @@ Tactic_debug Decl_mode Ppconstr Extend +Extrawit Pcoq Printer Pptactic diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 5e3fbb616..4881c3eef 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -400,12 +400,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintConstr" - [[TacTerm "PrintConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] let _ = try @@ -419,12 +417,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintPureConstr" - [[TacTerm "PrintPureConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintPureConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) open Names diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 666f9022b..32595cdc6 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -890,6 +890,12 @@ let rec prod_constr_expr c = function List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) +let coerce_reference_to_id = function + | Ident (_,id) -> id + | Qualid (loc,_) -> + user_err_loc (loc, "coerce_reference_to_id", + str "This expression should be a simple identifier.") + let coerce_to_id = function | CRef (Ident (loc,id)) -> (loc,id) | a -> user_err_loc @@ -903,6 +909,7 @@ let coerce_to_name = function (constr_loc a,"coerce_to_name", str "This expression should be a name.") + (* Used in correctness and interface *) let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1982a08fd..0b6cf46c5 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -200,6 +200,7 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr +val coerce_reference_to_id : reference -> identifier val coerce_to_id : constr_expr -> identifier located val coerce_to_name : constr_expr -> name located diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 40cffadb7..481b9f8d4 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -23,7 +23,6 @@ let join_loc loc1 loc2 = else Stdpp.encl_loc loc1 loc2 type token = string*string type lexer = token Token.glexer -let using l x = l.Token.tok_using x end ELSE IFDEF OCAML308 THEN module M = struct @@ -43,7 +42,6 @@ let join_loc loc1 loc2 = else (fst loc1, snd loc2) type token = Token.t type lexer = Token.lexer -let using l x = l.Token.using x end ELSE module M = struct @@ -56,7 +54,6 @@ let join_loc loc1 loc2 = else (fst loc1, snd loc2) type token = Token.t type lexer = Token.lexer -let using l x = l.Token.using x end END END @@ -68,4 +65,3 @@ let unloc = M.unloc let join_loc = M.join_loc type token = M.token type lexer = M.lexer -let using = M.using diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 7f2a6dd48..aa0c3c771 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -13,6 +13,7 @@ open Genarg open Q_util open Q_coqast +open Egrammar let join_loc = Util.join_loc let loc = Util.dummy_loc @@ -96,18 +97,24 @@ let rec make_wit loc = function let make_act loc act pil = let rec make = function | [] -> <:expr< Gramext.action (fun loc -> ($act$ : 'a)) >> - | None :: tl -> <:expr< Gramext.action (fun _ -> $make tl$) >> - | Some (p, t) :: tl -> + | GramNonTerminal (_,t,_,Some p) :: tl -> + let p = Names.string_of_id p in <:expr< Gramext.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) - >> in + >> + | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> + <:expr< Gramext.action (fun _ -> $make tl$) >> in make (List.rev pil) +let make_prod_item = function + | GramTerminal s -> <:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >> + | GramNonTerminal (_,_,g,_) -> + <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >> + let make_rule loc (prods,act) = - let (symbs,pil) = List.split prods in - <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >> + <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >> let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = let rawtyp, rawpr = match rawtyppr with @@ -144,6 +151,8 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< declare + open Pcoq; + open Extrawit; value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = Genarg.create_arg $se$; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; @@ -174,6 +183,8 @@ let declare_vernac_argument loc s pr cl = | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in <:str_item< declare + open Pcoq; + open Extrawit; 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$; @@ -227,7 +238,7 @@ EXTEND [ e = argtype; LIDENT "list" -> List0ArgType e | e = argtype; LIDENT "option" -> OptArgType e ] | "0" - [ e = LIDENT -> fst (interp_entry_name loc e "") + [ e = LIDENT -> fst (interp_entry_name None e "") | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -235,13 +246,15 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name loc e "" in (g, Some (s,t)) + let t, g = interp_entry_name None e "" in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name loc e sep in (g, Some (s,t)) + let t, g = interp_entry_name None e sep in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - Compat.using Pcoq.lexer ("", s); - (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None) + Lexer.add_token ("", s); + GramTerminal s ] ] ; END diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index b784acdc3..6ce6c2c09 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -12,6 +12,7 @@ open Pp open Util open Pcoq open Extend +open Ppextend open Topconstr open Genarg open Libnames @@ -55,10 +56,9 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) | Name id -> CPatAtom (loc,Some (Ident (loc,id))) -type prod_item = - | Term of Token.pattern - | NonTerm of constr_production_entry * - (Names.identifier * constr_production_entry) option +type grammar_constr_prod_item = + | GramConstrTerminal of Token.pattern + | GramConstrNonTerminal of constr_prod_entry_key * identifier option type 'a action_env = 'a list * 'a list list @@ -111,10 +111,10 @@ let make_cases_pattern_action make ([],[]) (List.rev pil) let make_constr_prod_item univ assoc from forpat = function - | Term tok -> (Gramext.Stoken tok, None) - | NonTerm (nt, ovar) -> - let eobj = symbol_of_production assoc from forpat nt in - (eobj, ovar) + | GramConstrTerminal tok -> (Gramext.Stoken tok, None) + | GramConstrNonTerminal (nt, ovar) -> + let eobj = symbol_of_constr_prod_entry_key assoc from forpat nt in + (eobj, Option.map (fun x -> (x,nt)) ovar) let prepare_empty_levels entry (pos,p4assoc,name,reinit) = grammar_extend entry pos reinit [(name, p4assoc, [])] @@ -139,11 +139,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt = let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,env) in - let e = get_constr_entry false (ETConstr (n,())) in + let e = interp_constr_entry_key false (ETConstr (n,())) in extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule; (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,env) in - let e = get_constr_entry true (ETConstr (n,())) in + let e = interp_constr_entry_key true (ETConstr (n,())) in extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rule @@ -169,22 +169,19 @@ let make_rule univ f g pt = (**********************************************************************) (** Grammar extensions declared at ML level *) -type grammar_tactic_production = - | TacTerm of string - | TacNonTerm of - loc * (Gram.te Gramext.g_symbol * argument_type) * string option +type grammar_prod_item = + | GramTerminal of string + | GramNonTerminal of + loc * argument_type * Gram.te prod_entry_key * identifier option let make_prod_item = function - | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None) - | TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po) + | GramTerminal s -> (Gramext.Stoken (Lexer.terminal s), None) + | GramNonTerminal (_,t,e,po) -> + (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po) (* Tactic grammar extensions *) -let tac_exts = ref [] -let get_extend_tactic_grammars () = !tac_exts - let extend_tactic_grammar s gl = - tac_exts := (s,gl) :: !tac_exts; 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 @@ -205,52 +202,6 @@ let extend_vernac_command_grammar s gl = (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) -(* Interpretation of the grammar entry names *) - -let find_index s t = - let t,n = repr_ident (id_of_string t) in - if s <> t or n = None then raise Not_found; - Option.get n - -let rec interp_entry_name up_level s = - let l = String.length s in - if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in - List1ArgType t, Gramext.Slist1 g - else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in - List0ArgType t, Gramext.Slist0 g - else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in - OptArgType t, Gramext.Sopt g - else - let s = if s = "hyp" then "var" else s in - try - let i = find_index "tactic" s in - ExtraArgType s, - if up_level<>5 && i=up_level then Gramext.Sself else - if up_level<>5 && i=up_level-1 then Gramext.Snext else - Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i) - with Not_found -> - let e = - (* Qualified entries are no longer in use *) - try get_entry (get_univ "tactic") s - with _ -> - try get_entry (get_univ "prim") s - with _ -> - try get_entry (get_univ "constr") s - with _ -> error ("Unknown entry "^s^".") - in - let o = object_of_typed_entry e in - let t = type_of_typed_entry e in - t,Gramext.Snterm (Pcoq.Gram.Entry.obj o) - -let make_vprod_item n = function - | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None) - | VNonTerm (loc, nt, po) -> - let (etyp, e) = interp_entry_name n nt in - e, Option.map (fun p -> (p,etyp)) po - let get_tactic_entry n = if n = 0 then weaken_entry Tactic.simple_tactic, None @@ -263,24 +214,23 @@ let get_tactic_entry n = (* Declaration of the tactic grammar rule *) -let head_is_ident = function VTerm _::_ -> true | _ -> false +let head_is_ident = function GramTerminal _::_ -> true | _ -> false let add_tactic_entry (key,lev,prods,tac) = let univ = get_univ "tactic" in let entry, pos = get_tactic_entry lev in - let mkprod = make_vprod_item lev in let rules = if lev = 0 then begin if not (head_is_ident prods) then error "Notation for simple tactic must start with an identifier."; let mkact s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in - make_rule univ (mkact key tac) mkprod prods + make_rule univ (mkact key tac) make_prod_item prods end else let mkact s tac loc l = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in - make_rule univ (mkact key tac) mkprod prods 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])] @@ -288,13 +238,13 @@ let add_tactic_entry (key,lev,prods,tac) = (** State of the grammar extensions *) type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list + int * Gramext.g_assoc option * notation * grammar_constr_prod_item list type all_grammar_command = - | Notation of Notation.level * notation_grammar + | Notation of (precedence * tolerability list) * notation_grammar | TacticGrammar of - (string * int * grammar_production list * - (Names.dir_path * Tacexpr.glob_tactic_expr)) + (string * int * grammar_prod_item list * + (dir_path * Tacexpr.glob_tactic_expr)) let (grammar_state : all_grammar_command list ref) = ref [] @@ -304,14 +254,6 @@ let extend_grammar gram = | TacticGrammar g -> add_tactic_entry g); grammar_state := gram :: !grammar_state -let reset_extend_grammars_v8 () = - let te = List.rev !tac_exts in - let tv = List.rev !vernac_exts in - tac_exts := []; - vernac_exts := []; - List.iter (fun (s,gl) -> print_string ("Resinstalling "^s); flush stdout; extend_tactic_grammar s gl) te; - List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv - let recover_notation_grammar ntn prec = let l = map_succeed (function | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e99741a6e..e632e5bb8 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -10,12 +10,14 @@ (*i*) open Util +open Names open Topconstr open Pcoq open Extend open Vernacexpr open Ppextend open Rawterm +open Genarg open Mod_subst (*i*) @@ -24,44 +26,40 @@ open Mod_subst and for ML-level tactic and vernac extensions *) -type prod_item = - | Term of Token.pattern - | NonTerm of constr_production_entry * - (Names.identifier * constr_production_entry) option +(* For constr notations *) + +type grammar_constr_prod_item = + | GramConstrTerminal of Token.pattern + | GramConstrNonTerminal of constr_prod_entry_key * identifier option type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list + int * Gramext.g_assoc option * notation * grammar_constr_prod_item 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 + +(* Adding notations *) type all_grammar_command = | Notation of (precedence * tolerability list) * notation_grammar | TacticGrammar of - (string * int * grammar_production list * - (Names.dir_path * Tacexpr.glob_tactic_expr)) + (string * int * grammar_prod_item list * + (dir_path * Tacexpr.glob_tactic_expr)) val extend_grammar : all_grammar_command -> unit -(* Add grammar rules for tactics *) - -type grammar_tactic_production = - | TacTerm of string - | TacNonTerm of - loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option - val extend_tactic_grammar : - string -> grammar_tactic_production list list -> unit + string -> grammar_prod_item list list -> unit val extend_vernac_command_grammar : - string -> grammar_tactic_production list list -> unit -(* -val get_extend_tactic_grammars : - unit -> (string * grammar_tactic_production list list) list -*) + string -> grammar_prod_item list list -> unit + val get_extend_vernac_grammars : - unit -> (string * grammar_tactic_production list list) list -(* -val reset_extend_grammars_v8 : unit -> unit -*) -val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol + unit -> (string * grammar_prod_item list list) list val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_grammar diff --git a/parsing/extend.ml b/parsing/extend.ml index 36e1000b1..2121671a8 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -6,52 +6,53 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) open Util -open Pp -open Gramext -open Names -open Ppextend -open Topconstr -open Genarg (**********************************************************************) -(* constr entry keys *) +(* 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 *) type side = Left | Right type production_position = - | BorderProd of side * Gramext.g_assoc option (* true=left; false=right *) + | BorderProd of side * Gramext.g_assoc option | InternalProd type production_level = | NextLevel | NumLevel of int -type ('lev,'pos) constr_entry_key = +type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Token.pattern list -type constr_production_entry = - (production_level,production_position) constr_entry_key -type constr_entry = - (int,unit) constr_entry_key -type simple_constr_production_entry = - (production_level,unit) constr_entry_key - -(**********************************************************************) -(* syntax modifiers *) - -type syntax_modifier = - | SetItemLevel of string list * production_level - | SetLevel of int - | SetAssoc of Gramext.g_assoc - | SetEntryType of string * simple_constr_production_entry - | SetOnlyParsing - | SetFormat of string located - +type constr_prod_entry_key = + (production_level,production_position) constr_entry_key_gen +type constr_entry_key = + (int,unit) constr_entry_key_gen +type simple_constr_prod_entry_key = + (production_level,unit) constr_entry_key_gen diff --git a/parsing/extend.mli b/parsing/extend.mli index 61fee077a..0ca073956 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -11,40 +11,49 @@ open Util (**********************************************************************) -(* constr entry keys *) +(* 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 *) type side = Left | Right type production_position = - | BorderProd of side * Gramext.g_assoc option (* true=left; false=right *) + | BorderProd of side * Gramext.g_assoc option | InternalProd type production_level = | NextLevel | NumLevel of int -type ('lev,'pos) constr_entry_key = +type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Token.pattern list -type constr_production_entry = - (production_level,production_position) constr_entry_key -type constr_entry = - (int,unit) constr_entry_key -type simple_constr_production_entry = - (production_level,unit) constr_entry_key - -(**********************************************************************) -(* syntax modifiers *) - -type syntax_modifier = - | SetItemLevel of string list * production_level - | SetLevel of int - | SetAssoc of Gramext.g_assoc - | SetEntryType of string * simple_constr_production_entry - | SetOnlyParsing - | SetFormat of string located +type constr_prod_entry_key = + (production_level,production_position) constr_entry_key_gen +type constr_entry_key = + (int,unit) constr_entry_key_gen +type simple_constr_prod_entry_key = + (production_level,unit) constr_entry_key_gen diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml new file mode 100644 index 000000000..122730f72 --- /dev/null +++ b/parsing/extrawit.ml @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Util +open Genarg + +(* This file defines extra argument types *) + +(* Tactics as arguments *) + +let tactic_main_level = 5 + +let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0" +let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1" +let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2" +let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3" +let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4" +let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5" + +let wit_tactic = function + | 0 -> wit_tactic0 + | 1 -> wit_tactic1 + | 2 -> wit_tactic2 + | 3 -> wit_tactic3 + | 4 -> wit_tactic4 + | 5 -> wit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let globwit_tactic = function + | 0 -> globwit_tactic0 + | 1 -> globwit_tactic1 + | 2 -> globwit_tactic2 + | 3 -> globwit_tactic3 + | 4 -> globwit_tactic4 + | 5 -> globwit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let rawwit_tactic = function + | 0 -> rawwit_tactic0 + | 1 -> rawwit_tactic1 + | 2 -> rawwit_tactic2 + | 3 -> rawwit_tactic3 + | 4 -> rawwit_tactic4 + | 5 -> rawwit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let tactic_genarg_level s = + if String.length s = 7 && String.sub s 0 6 = "tactic" then + let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) + else None + else None + +let is_tactic_genarg = function +| ExtraArgType s -> tactic_genarg_level s <> None +| _ -> false diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli new file mode 100644 index 000000000..9eff5dc13 --- /dev/null +++ b/parsing/extrawit.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Util +open Genarg +open Tacexpr + +(* This file defines extra argument types *) + +(* Tactics as arguments *) + +val tactic_main_level : int + +val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type + +val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type + +val is_tactic_genarg : argument_type -> bool + +val tactic_genarg_level : string -> int option diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 8db62c392..f91f0170c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -80,9 +80,6 @@ let mk_fix(loc,kw,id,dcls) = let mk_single_fix (loc,kw,dcl) = let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) -let binder_constr = - create_constr_entry (get_univ "constr") "binder_constr" - (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let lpar_id_coloneq = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f656fb32e..56c00ca78 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -16,13 +16,13 @@ open Pp open Util open Names open Topconstr +open Extend open Vernacexpr open Pcoq open Decl_mode open Tactic open Decl_kinds open Genarg -open Extend open Ppextend open Goptions @@ -471,17 +471,17 @@ GEXTEND Gram | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> - let s = coerce_global_to_id qid in + let s = coerce_reference_to_id qid in VernacDefinition ((Global,false,CanonicalStructure),(dummy_loc,s),d, (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> - let s = coerce_global_to_id qid in + let s = coerce_reference_to_id qid in VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> - let s = coerce_global_to_id qid in + let s = coerce_reference_to_id qid in VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> @@ -851,15 +851,16 @@ GEXTEND Gram ; syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference - | IDENT "bigint" -> ETBigint + | IDENT "bigint" -> ETBigint ] ] ; opt_scope: [ [ "_" -> None | sc = IDENT -> Some sc ] ] ; production_item: - [ [ s = ne_string -> VTerm s - | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] -> - VNonTerm (loc,nt,po) ] ] + [ [ s = ne_string -> TacTerm s + | nt = IDENT; + po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; + ")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ] ; END diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 128ca9445..9e714352b 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -64,10 +64,12 @@ Tacexpr Lexer Extend Vernacexpr +Extrawit Pcoq Q_util Q_coqast +Egrammar Argextend Tacextend Vernacextend @@ -75,4 +77,4 @@ Vernacextend G_prim G_tactic G_ltac -G_constr
\ No newline at end of file +G_constr diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 045c2ecca..c827ab381 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,13 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - - -(*i camlp4use: "pr_o.cmo" i*) +(*i camlp4use: "pr_o.cmo pa_macro.cmo" i*) (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with * ast-based camlp4 *) +(*i $Id$ i*) + open Pp open Util open Token @@ -512,14 +511,36 @@ let token_text = function | (con, "") -> con | (con, prm) -> con ^ " \"" ^ prm ^ "\"" -let tparse (p_con, p_prm) = - None - (*i was - if p_prm = "" then - (parser [< '(con, prm) when con = p_con >] -> prm) - else - (parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm) - i*) +(* The lexer of Coq *) + +(* 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 + env/metasyntax.ml). Therefore, instead of removing tokens one by one, + we unfreeze the state of the lexer. This restores the behaviour of the + lexer. B.B. *) + +IFDEF CAMLP5 THEN + +let lexer = { + Token.tok_func = func; + Token.tok_using = add_token; + Token.tok_removing = (fun _ -> ()); + Token.tok_match = default_match; + Token.tok_comm = None; + Token.tok_text = token_text } + +ELSE + +let lexer = { + Token.func = func; + Token.using = add_token; + Token.removing = (fun _ -> ()); + Token.tparse = (fun _ -> None); + Token.text = token_text } + +END (* Terminal symbols interpretation *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 84f25ca5e..1a3a10aaa 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -23,7 +23,6 @@ exception Error of error val add_token : string * string -> unit val is_keyword : string -> bool -val func : char Stream.t -> (string * string) Stream.t * (int -> loc) val location_function : int -> loc (* for coqdoc *) @@ -34,10 +33,6 @@ val restore_location_table : location_table -> unit val check_ident : string -> unit val check_keyword : string -> unit -val tparse : string * string -> ((string * string) Stream.t -> string) option - -val token_text : string * string -> string - type frozen_t val freeze : unit -> frozen_t val unfreeze : frozen_t -> unit @@ -50,3 +45,7 @@ val restore_com_state: com_state -> unit val set_xml_output_comment : (string -> unit) -> unit val terminal : string -> string * string + +(* The lexer of Coq *) + +val lexer : Compat.lexer diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index c705e45cd..c0c1817d1 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,4 +1,5 @@ Extend +Extrawit Pcoq Egrammar G_xml diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 8f7567595..99c6d8528 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -19,55 +19,28 @@ open Rawterm open Topconstr open Genarg open Tacexpr +open Extrawit open Ppextend -(* The lexer of Coq *) - -(* 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 - env/metasyntax.ml). Therefore, instead of removing tokens one by one, - we unfreeze the state of the lexer. This restores the behaviour of the - lexer. B.B. *) +(* The parser of Coq *) IFDEF CAMLP5 THEN -let lexer = { - Token.tok_func = Lexer.func; - Token.tok_using = Lexer.add_token; - Token.tok_removing = (fun _ -> ()); - Token.tok_match = Token.default_match; - (* Token.parse = Lexer.tparse; *) - Token.tok_comm = None; - Token.tok_text = Lexer.token_text } - module L = struct type te = string * string - let lexer = lexer + let lexer = Lexer.lexer end -(* The parser of Coq *) - module G = Grammar.GMake(L) ELSE -let lexer = { - Token.func = Lexer.func; - Token.using = Lexer.add_token; - Token.removing = (fun _ -> ()); - Token.tparse = Lexer.tparse; - Token.text = Lexer.token_text } - module L = struct - let lexer = lexer + let lexer = Lexer.lexer end -(* The parser of Coq *) - module G = Grammar.Make(L) END @@ -134,12 +107,17 @@ end open Gramtypes +type camlp4_rule = + Compat.token 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 + type ext_kind = | ByGrammar of - grammar_object G.Entry.e * Gramext.position option * - (string option * Gramext.g_assoc option * - (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list * - Gramext.g_assoc option + grammar_object G.Entry.e * Gramext.position option * + camlp4_entry_rules list * Gramext.g_assoc option | ByGEXTEND of (unit -> unit) * (unit -> unit) let camlp4_state = ref [] @@ -212,14 +190,14 @@ let map_entry f en = let parse_string f x = let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm) -type gram_universe = (string, typed_entry) Hashtbl.t +type gram_universe = string * (string, typed_entry) Hashtbl.t let trace = ref false -(* The univ_tab is not part of the state. It contains all the grammar that +(* The univ_tab is not part of the state. It contains all the grammars that exist or have existed before in the session. *) -let univ_tab = (Hashtbl.create 7 : (string, string * gram_universe) Hashtbl.t) +let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t) let create_univ s = let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u @@ -229,49 +207,27 @@ let uconstr = create_univ "constr" let utactic = create_univ "tactic" let uvernac = create_univ "vernac" -let create_univ_if_new s = - (* compatibilite *) - let s = if s = "command" then (warning "'command' grammar universe is obsolete; use name 'constr' instead"; "constr") else s in +let get_univ s = try Hashtbl.find univ_tab s - with Not_found -> - if !trace then begin - Printf.eprintf "[Creating univ %s]\n" s; flush stderr; () - end; - let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u + with Not_found -> + anomaly ("Unknown grammar universe: "^s) -let get_univ = create_univ_if_new +let get_entry (u, utab) s = Hashtbl.find utab s -let get_entry (u, utab) s = - try - Hashtbl.find utab s - with Not_found -> +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 Hashtbl.add utab s e; e -let entry_type (u, utab) s = - try - let e = Hashtbl.find utab s in - Some (type_of_typed_entry e) - with Not_found -> None - -let get_entry_type (u,n) = type_of_typed_entry (get_entry (get_univ u) n) - -let create_entry_if_new (u, utab) s etyp = - try - if type_of_typed_entry (Hashtbl.find utab s) <> etyp then - failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type") - with Not_found -> - if !trace then begin - Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () - end; - let _ = new_entry etyp (u, utab) s in () - let create_entry (u, utab) s etyp = try let e = Hashtbl.find utab s in @@ -279,105 +235,13 @@ let create_entry (u, utab) s etyp = failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); e with Not_found -> - if !trace then begin - Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () - end; new_entry etyp (u, utab) s -let create_constr_entry u s = - outGramObj rawwit_constr (create_entry u s ConstrArgType) - -let create_generic_entry s wit = - let (u,utab) = utactic in - let etyp = unquote wit in - try - let e = Hashtbl.find utab s in - if type_of_typed_entry e <> etyp then - failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); - outGramObj wit e - with Not_found -> - if !trace then begin - Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () - end; - let e = Gram.Entry.create s in - Hashtbl.add utab s (inGramObj wit e); e - -let get_generic_entry s = - let (u,utab) = utactic in - try - object_of_typed_entry (Hashtbl.find utab s) - with Not_found -> - error ("Unknown grammar entry "^u^":"^s^".") - -let get_generic_entry_type (u,utab) s = - try type_of_typed_entry (Hashtbl.find utab s) - with Not_found -> - error ("Unknown grammar entry "^u^":"^s^".") - -let force_entry_type (u, utab) s etyp = - try - let entry = Hashtbl.find utab s in - let extyp = type_of_typed_entry entry in - if etyp = extyp then - entry - else begin - prerr_endline - ("Grammar entry " ^ u ^ ":" ^ s ^ - " redefined with another type;\n older entry hidden."); - Hashtbl.remove utab s; - new_entry etyp (u, utab) s - end - with Not_found -> - new_entry etyp (u, utab) s - -(* Tactics as arguments *) - -let tactic_main_level = 5 - -let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0" -let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1" -let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2" -let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3" -let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4" -let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5" - -let wit_tactic = function - | 0 -> wit_tactic0 - | 1 -> wit_tactic1 - | 2 -> wit_tactic2 - | 3 -> wit_tactic3 - | 4 -> wit_tactic4 - | 5 -> wit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) - -let globwit_tactic = function - | 0 -> globwit_tactic0 - | 1 -> globwit_tactic1 - | 2 -> globwit_tactic2 - | 3 -> globwit_tactic3 - | 4 -> globwit_tactic4 - | 5 -> globwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) - -let rawwit_tactic = function - | 0 -> rawwit_tactic0 - | 1 -> rawwit_tactic1 - | 2 -> rawwit_tactic2 - | 3 -> rawwit_tactic3 - | 4 -> rawwit_tactic4 - | 5 -> rawwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) - -let tactic_genarg_level s = - if String.length s = 7 && String.sub s 0 6 = "tactic" then - let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) - else None - else None - -let is_tactic_genarg = function -| ExtraArgType s -> tactic_genarg_level s <> None -| _ -> false +let create_constr_entry s = + outGramObj rawwit_constr (create_entry uconstr s ConstrArgType) +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 *) @@ -386,7 +250,7 @@ let make_gen_entry (u,univ) rawwit s = let e = Gram.Entry.create (u ^ ":" ^ s) in Hashtbl.add univ s (inGramObj rawwit e); e -(* Grammar entries *) +(* Initial grammar entries *) module Prim = struct @@ -421,7 +285,6 @@ module Prim = end - module Constr = struct let gec_constr = make_gen_entry uconstr rawwit_constr @@ -432,7 +295,7 @@ module Constr = let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr let lconstr = gec_constr "lconstr" - let binder_constr = create_constr_entry uconstr "binder_constr" + let binder_constr = create_constr_entry "binder_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" @@ -489,8 +352,6 @@ module Tactic = end - - module Vernac_ = struct let gec_vernac s = Gram.Entry.create ("vernac:" ^ s) @@ -500,24 +361,22 @@ module Vernac_ = let gallina_ext = gec_vernac "gallina_ext" let command = gec_vernac "command" let syntax = gec_vernac "syntax_command" - let vernac = gec_vernac "Vernac_.vernac" - - (* MMode *) - + let vernac = gec_vernac "Vernac.vernac" let proof_instr = Gram.Entry.create "proofmode:instr" - (* /MMode *) - let vernac_eoi = eoi_entry vernac - end -let main_entry = Gram.Entry.create "vernac" + (* Main vernac entry *) + let main_entry = Gram.Entry.create "vernac" + GEXTEND Gram + main_entry: + [ [ a = vernac -> Some (loc,a) | EOI -> None ] ] + ; + END -GEXTEND Gram - main_entry: - [ [ a = Vernac_.vernac -> Some (loc,a) | EOI -> None ] ] - ; -END + end + +let main_entry = Vernac_.main_entry (**********************************************************************) (* This determines (depending on the associativity of the current @@ -643,6 +502,9 @@ let find_position forpat assoc level = let synchronize_level_positions () = let _ = find_position true None None in () +(**********************************************************************) +(* Binding constr entry keys to entries *) + (* 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 @@ -698,11 +560,11 @@ let compute_entry allow_create adjust forpat = function let u = get_univ u in let e = try get_entry u n - with e when allow_create -> create_entry u n ConstrArgType in + with Not_found when allow_create -> create_entry u n ConstrArgType in object_of_typed_entry e, None, true (* This computes the name of the level where to add a new rule *) -let get_constr_entry forpat = function +let interp_constr_entry_key forpat = function | ETConstr(200,()) when not forpat -> weaken_entry Constr.binder_constr, None | e -> @@ -711,9 +573,12 @@ let get_constr_entry forpat = function (* This computes the name to give to a production knowing the name and associativity of the level where it must be added *) -let get_constr_production_entry ass from forpat en = +let interp_constr_prod_entry_key ass from forpat en = compute_entry false (adjust_level ass from) forpat en +(**********************************************************************) +(* Binding constr entry keys to symbols *) + let is_self from e = match from, e with ETConstr(n,()), ETConstr(NumLevel n', @@ -730,7 +595,7 @@ let is_binder_level from e = ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true | _ -> false -let rec symbol_of_production assoc from forpat typ = +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") @@ -741,28 +606,87 @@ let rec symbol_of_production assoc from forpat typ = else match typ with | ETConstrList (typ',[]) -> - Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ')) + Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) | ETConstrList (typ',tkl) -> Gramext.Slist1sep - (symbol_of_production assoc from forpat (ETConstr typ'), + (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), Gramext.srules [List.map (fun x -> Gramext.Stoken x) tkl, List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl (Gramext.action (fun loc -> ()))]) | _ -> - match get_constr_production_entry assoc from forpat typ with + 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,Some (Some (lev,cur)),_) -> Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev) -(*****************************) -(* Coercions between entries *) - -let coerce_reference_to_id = function - | Ident (_,id) -> id - | Qualid (loc,_) -> - user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier.") +(**********************************************************************) +(* Binding general entry keys to symbol *) + +let rec symbol_of_prod_entry_key = function + | Alist1 s -> Gramext.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) + | Alist0sep (s,sep) -> + Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) + | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s) + | Amodifiers s -> + Gramext.srules + [([], Gramext.action(fun _loc -> [])); + ([Gramext.Stoken ("", "("); + Gramext.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) + | Atactic n -> + Gramext.Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) + | Agram s -> Gramext.Snterm s + | Aentry (u,s) -> + Gramext.Snterm (Gram.Entry.obj + (object_of_typed_entry (get_entry (get_univ u) s))) -let coerce_global_to_id = coerce_reference_to_id +(**********************************************************************) +(* Interpret entry names of the form "ne_constr_list" as entry keys *) + +let rec interp_entry_name up_level s sep = + let l = String.length s in + if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then + let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) "" in + List1ArgType t, Alist1 g + else if l > 12 & String.sub s 0 3 = "ne_" & + String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name up_level (String.sub s 3 (l-12)) "" in + List1ArgType t, Alist1sep (g,sep) + else if l > 5 & String.sub s (l-5) 5 = "_list" then + let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) "" in + List0ArgType t, Alist0 g + else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name up_level (String.sub s 0 (l-9)) "" in + List0ArgType t, Alist0sep (g,sep) + else if l > 4 & String.sub s (l-4) 4 = "_opt" then + let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) "" in + OptArgType t, Aopt g + else if l > 5 & String.sub s (l-5) 5 = "_mods" then + let t, g = interp_entry_name up_level (String.sub s 0 (l-1)) "" in + List0ArgType t, Amodifiers g + else + let s = if s = "hyp" then "var" else s in + let t, se = + match Extrawit.tactic_genarg_level s with + | Some n when Some n = up_level & up_level <> Some 5 -> None, Aself + | Some n when Some (n+1) = up_level & up_level <> Some 5 -> None, Anext + | Some n -> None, Atactic n + | None -> + try Some (get_entry uprim s), Aentry ("prim",s) with Not_found -> + try Some (get_entry uconstr s), Aentry ("constr",s) with Not_found -> + try Some (get_entry utactic s), Aentry ("tactic",s) with Not_found -> + None, Aentry ("",s) in + let t = + match t with + | Some t -> type_of_typed_entry t + | None -> ExtraArgType s in + t, se diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 97a47dcc4..02db8d55d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -12,41 +12,125 @@ open Util open Names open Rawterm open Extend +open Vernacexpr open Genarg open Topconstr open Tacexpr -open Vernacexpr open Libnames -(* The lexer and parser of Coq. *) - -val lexer : Compat.lexer +(**********************************************************************) +(* The parser of Coq *) module Gram : Grammar.S with type te = Compat.token +(**********************************************************************) +(* 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) + - static rules explicitly defined in files g_*.ml4 + - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and + VERNAC EXTEND (see e.g. file extratactics.ml4) +*) + +(* Dynamic extension of rules + + For constr notations, dynamic addition of new rules is done in + several steps: + + - "x + y" (user gives a notation string of type Topconstr.notation) + | (together with a constr entry level, e.g. 50, and indications of) + | (subentries, e.g. x in constr next level and y constr same level) + | + | spliting into tokens by Metasyntax.split_notation_string + V + [String "x"; String "+"; String "y"] : symbol_token list + | + | interpreted as a mixed parsing/printing production + | by Metasyntax.analyse_notation_tokens + V + [NonTerminal "x"; Terminal "+"; NonTerminal "y"] : symbol list + | + | translated to a parsing production by Metasyntax.make_production + V + [GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Left,LeftA)), + Some "x"); + GramConstrTerminal ("","+"); + GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)), + Some "y")] + : grammar_constr_prod_item list + | + | Egrammar.make_constr_prod_item + V + Gramext.g_symbol list which is sent to camlp4 + + For user level tactic notations, dynamic addition of new rules is + also done in several steps: + + - "f" constr(x) (user gives a Tactic Notation command) + | + | parsing + V + [TacTerm "f"; TacNonTerm ("constr", Some "x")] + : grammar_tactic_prod_item_expr list + | + | Metasyntax.interp_prod_item + V + [GramTerminal "f"; + GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] + : grammar_prod_item list + | + | Egrammar.make_prod_item + V + Gramext.g_symbol list + + For TACTIC/VERNAC/ARGUMENT EXTEND, addition of new rules is done as follows: + + - "f" constr(x) (developer gives an EXTEND rule) + | + | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4 + V + [GramTerminal "f"; + GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] + | + | Egrammar.make_prod_item + V + Gramext.g_symbol list + +*) + (* The superclass of all grammar entries *) type grammar_object +type camlp4_rule = + Compat.token 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 + +(* Remove the last n extensions *) +val remove_grammars : int -> unit + + + + (* The type of typed grammar objects *) type typed_entry +(* The possible types for extensible grammars *) type entry_type = argument_type val type_of_typed_entry : typed_entry -> entry_type val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e -val get_constr_entry : - bool -> constr_entry -> grammar_object Gram.Entry.e * int option - -val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> - (* for reinitialization if ever: *) Gramext.g_assoc option -> - (string option * Gramext.g_assoc option * - (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list - -> unit - -val remove_grammars : int -> unit +(* Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -56,73 +140,28 @@ 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 -(* Entry types *) - -(* Table of Coq's grammar entries *) +(**********************************************************************) +(* Table of Coq statically defined grammar entries *) type gram_universe -val create_univ_if_new : string -> string * gram_universe -val get_univ : string -> string * gram_universe -val get_entry : string * gram_universe -> string -> typed_entry - -val entry_type : string * gram_universe -> string -> entry_type option - -val get_entry_type : string * string -> entry_type -val create_entry_if_new : - string * gram_universe -> string -> entry_type -> unit -val create_entry : - string * gram_universe -> string -> entry_type -> typed_entry -val force_entry_type : - string * gram_universe -> string -> entry_type -> typed_entry - -val create_constr_entry : - string * gram_universe -> string -> constr_expr Gram.Entry.e -val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.Entry.e -val get_generic_entry : string -> grammar_object Gram.Entry.e -val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type - -(* Tactics as arguments *) +(* There are four predefined universes: "prim", "constr", "tactic", "vernac" *) -val tactic_main_level : int +val get_univ : string -> gram_universe -val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type +val uprim : gram_universe +val uconstr : gram_universe +val utactic : gram_universe +val uvernac : gram_universe -val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type +(* +val get_entry : gram_universe -> string -> typed_entry +val get_entry_type : gram_universe -> string -> entry_type +*) -val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type - -val is_tactic_genarg : argument_type -> bool - -val tactic_genarg_level : string -> int option - -(* The main entry: reads an optional vernac command *) - -val main_entry : (loc * vernac_expr) option Gram.Entry.e - -(* Initial state of the grammar *) +val create_entry : gram_universe -> string -> entry_type -> typed_entry +val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> + 'a Gram.Entry.e module Prim : sig @@ -204,22 +243,38 @@ module Vernac_ : val command : vernac_expr Gram.Entry.e val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e - - (* MMode *) - + val vernac_eoi : vernac_expr Gram.Entry.e val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e + end - (*/ MMode *) +(* The main entry: reads an optional vernac command *) +val main_entry : (loc * vernac_expr) option Gram.Entry.e - val vernac_eoi : vernac_expr Gram.Entry.e - end +(**********************************************************************) +(* Mapping formal entries into concrete ones *) -(* Binding entry names to campl4 entries *) +(* Binding constr entry keys to entries and symbols *) -val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Compat.token Gramext.g_symbol +val interp_constr_entry_key : bool (* true for cases_pattern *) -> + constr_entry_key -> grammar_object Gram.Entry.e * int option -(* Registering/resetting the level of an entry *) +val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> + constr_entry_key -> bool -> constr_prod_entry_key -> + Compat.token Gramext.g_symbol + +(* Binding general entry keys to symbols *) + +val symbol_of_prod_entry_key : + Gram.te prod_entry_key -> Gram.te Gramext.g_symbol + +(**********************************************************************) +(* Interpret entry names of the form "ne_constr_list" as entry keys *) + +val interp_entry_name : int option -> string -> string -> + entry_type * Gram.te 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 *) -> @@ -234,5 +289,3 @@ val register_empty_levels : bool -> int list -> string option * Gramext.g_assoc option) list val remove_levels : int -> unit - -val coerce_global_to_id : reference -> identifier diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 801c0334b..357a572be 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -555,12 +555,6 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "using tdb" | false -> mt () -let rec pr_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - let pr_then () = str ";" let ltop = (5,E) @@ -1086,7 +1080,7 @@ let _ = Tactic_debug.set_match_rule_printer (fun rl -> pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl) -open Pcoq +open Extrawit let pr_tac_polymorphic n _ _ prtac = prtac (n,E) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 0054326e4..be04f584d 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -73,7 +73,7 @@ let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac let rec extract_signature = function | [] -> [] - | Egrammar.TacNonTerm (_,(_,t),_) :: l -> t :: extract_signature l + | Egrammar.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l | _::l -> extract_signature l let rec match_vernac_rule tys = function @@ -119,9 +119,11 @@ let strip_meta id = else id let pr_production_item = function - | VNonTerm (loc,nt,Some p) -> str nt ++ str"(" ++ pr_id (strip_meta p) ++ str")" - | VNonTerm (loc,nt,None) -> str nt - | VTerm s -> qs s + | TacNonTerm (loc,nt,Some (p,sep)) -> + let pp_sep = if sep <> "" then str "," ++ quote (str sep) else mt () in + str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" + | TacNonTerm (loc,nt,None) -> str nt + | TacTerm s -> qs s let pr_comment pr_c = function | CommentConstr c -> pr_c c @@ -811,7 +813,7 @@ let rec pr_vernac = function ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in pr_raw_tactic_env - (idl @ List.map coerce_global_to_id + (idl @ List.map coerce_reference_to_id (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l))) (Global.env()) body in @@ -945,15 +947,15 @@ and pr_extend s cl = let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with - | Egrammar.TacTerm s :: rl -> str s, rl, cl - | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl + | Egrammar.GramTerminal s :: rl -> str s, rl, cl + | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left (fun (strm,args) pi -> let pp,args = match pi with - | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args) - | Egrammar.TacTerm s -> (str s, args) in + | Egrammar.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) + | Egrammar.GramTerminal s -> (str s, args) in (strm ++ spc() ++ pp), args) (start,cl) rl in hov 1 pp diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 9b59ba8e5..469449749 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -13,6 +13,8 @@ (* This file defines standard combinators to build ml expressions *) open Util +open Extrawit +open Pcoq let not_impl name x = let desc = @@ -78,64 +80,16 @@ open Vernacexpr open Pcoq open Genarg -let modifiers e = -<:expr< Gramext.srules - [([], Gramext.action(fun _loc -> [])); - ([Gramext.Stoken ("", "("); - Gramext.Slist1sep ($e$, Gramext.Stoken ("", ",")); - Gramext.Stoken ("", ")")], - Gramext.action (fun _ l _ _loc -> l))] - >> - -let rec interp_entry_name loc s sep = - let l = String.length s in - if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 3 (l-8)) "" in - List1ArgType t, <:expr< Gramext.Slist1 $g$ >> - else if l > 12 & String.sub s 0 3 = "ne_" & - String.sub s (l-9) 9 = "_list_sep" then - let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in - let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in - List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >> - else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in - List0ArgType t, <:expr< Gramext.Slist0 $g$ >> - else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then - let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in - let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in - List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >> - else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in - OptArgType t, <:expr< Gramext.Sopt $g$ >> - else if l > 5 & String.sub s (l-5) 5 = "_mods" then - let t, g = interp_entry_name loc (String.sub s 0 (l-1)) "" in - List0ArgType t, modifiers g - else - let s = if s = "hyp" then "var" else s in - let t, se, lev = - match tactic_genarg_level s with - | Some 5 -> - Some (ExtraArgType s), <:expr< Tactic. binder_tactic >>, None - | Some n -> - Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n - | None -> - match Pcoq.entry_type (Pcoq.get_univ "prim") s with - | Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None - | None -> - match Pcoq.entry_type (Pcoq.get_univ "constr") s with - | Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None - | None -> - match Pcoq.entry_type (Pcoq.get_univ "tactic") s with - | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None - | None -> None, <:expr< $lid:s$ >>, None in - let t = - match t with - | Some t -> t - | None -> ExtraArgType s in - let entry = match lev with - | Some n -> - let s = string_of_int n in - <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >> - | None -> - <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >> - in t, entry +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$ >> diff --git a/parsing/q_util.mli b/parsing/q_util.mli index a160310e4..7c0fec9a2 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -32,5 +32,4 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val interp_entry_name : Util.loc -> string -> string -> - Pcoq.entry_type * MLast.expr +val mlexpr_of_prod_entry_key : Pcoq.Gram.te Extend.prod_entry_key -> MLast.expr diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 03c704758..fc499241c 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -15,20 +15,21 @@ open Genarg open Q_util open Q_coqast open Argextend - -type grammar_tactic_production_expr = - | TacTerm of string - | TacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option +open Pcoq +open Extrawit +open Egrammar let rec make_patt = function | [] -> <:patt< [] >> - | TacNonTerm(loc',_,_,Some p)::l -> + | GramNonTerminal(loc',_,_,Some p)::l -> + let p = Names.string_of_id p in <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_when loc = function | [] -> <:expr< True >> - | TacNonTerm(loc',t,_,Some p)::l -> + | GramNonTerminal(loc',t,_,Some p)::l -> + let p = Names.string_of_id p in let l = make_when loc l in let loc = join_loc loc' loc in let t = mlexpr_of_argtype loc' t in @@ -37,14 +38,15 @@ let rec make_when loc = function let rec make_let e = function | [] -> e - | TacNonTerm(loc,t,_,Some p)::l -> + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in let v = (* Special case for tactics which must be stored in algebraic form to avoid marshalling closures and to be reprinted *) - if Pcoq.is_tactic_genarg t then + if is_tactic_genarg t then <:expr< ($v$, Tacinterp.eval_tactic $v$) >> else v in <:expr< let $lid:p$ = $v$ in $e$ >> @@ -57,7 +59,7 @@ let add_clause s (pt,e) l = let rec extract_signature = function | [] -> [] - | TacNonTerm (_,t,_,_) :: l -> t :: extract_signature l + | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l | _::l -> extract_signature l let check_unicity s l = @@ -75,13 +77,15 @@ let make_clauses s l = let rec make_args = function | [] -> <:expr< [] >> - | TacNonTerm(loc,t,_,Some p)::l -> + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> | _::l -> make_args l let rec make_eval_tactic e = function | [] -> e - | TacNonTerm(loc,tag,_,Some p)::l when Pcoq.is_tactic_genarg tag -> + | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag -> + let p = Names.string_of_id p in let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_eval_tactic e l in (* Special case for tactics which must be stored in algebraic @@ -91,26 +95,27 @@ let rec make_eval_tactic e = function let rec make_fun e = function | [] -> e - | TacNonTerm(loc,_,_,Some p)::l -> + | GramNonTerminal(loc,_,_,Some p)::l -> + let p = Names.string_of_id p in <:expr< fun $lid:p$ -> $make_fun e l$ >> | _::l -> make_fun e l -let mlexpr_of_grammar_production = function - | TacTerm s -> - <:expr< Egrammar.TacTerm $mlexpr_of_string s$ >> - | TacNonTerm (loc,nt,g,sopt) -> - <:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >> +let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function + | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >> + | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >> -let mlexpr_terminals_of_grammar_production = function - | TacTerm s -> <:expr< Some $mlexpr_of_string s$ >> - | TacNonTerm (loc,nt,g,sopt) -> <:expr< None >> +let make_prod_item = function + | GramTerminal s -> <:expr< Egrammar.GramTerminal $str:s$ >> + | GramNonTerminal (loc,nt,g,sopt) -> + <:expr< Egrammar.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ + $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> let mlexpr_of_clause = - mlexpr_of_list (fun (a,b) -> mlexpr_of_list mlexpr_of_grammar_production a) + mlexpr_of_list (fun (a,b) -> mlexpr_of_list make_prod_item a) let rec make_tags loc = function | [] -> <:expr< [] >> - | TacNonTerm(loc',t,_,Some p)::l -> + | GramNonTerminal(loc',t,_,Some p)::l -> let l = make_tags loc l in let loc = join_loc loc' loc in let t = mlexpr_of_argtype loc' t in @@ -120,7 +125,7 @@ let rec make_tags loc = function let make_one_printing_rule se (pt,e) = let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in - let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in + let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in <:expr< ($se$, $make_tags loc pt$, ($level$, $prods$)) >> let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) @@ -133,10 +138,10 @@ let rec contains_epsilon = function | ExtraArgType("hintbases") -> true | _ -> false let is_atomic = function - | TacTerm s :: l when + | GramTerminal s :: l when List.for_all (function - TacTerm _ -> false - | TacNonTerm(_,t,_,_) -> contains_epsilon t) l + GramTerminal _ -> false + | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l -> [s] | _ -> [] @@ -162,6 +167,7 @@ let declare_tactic loc s cl = <:str_item< declare open Pcoq; + open Extrawit; declare $list:hidden$ end; try let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in @@ -189,7 +195,7 @@ EXTEND tacrule: [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" -> - if match List.hd l with TacNonTerm _ -> true | _ -> false then + if match List.hd l with GramNonTerminal _ -> true | _ -> false then (* En attendant la syntaxe de tacticielles *) failwith "Tactic syntax must start with an identifier"; (l,e) @@ -197,14 +203,14 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = Q_util.interp_entry_name loc e "" in - TacNonTerm (loc, t, g, Some s) + let t, g = interp_entry_name None e "" in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = Q_util.interp_entry_name loc e sep in - TacNonTerm (loc, t, g, Some s) + let t, g = interp_entry_name None e sep in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | s = STRING -> if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal."); - TacTerm s + GramTerminal s ] ] ; END diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index dd6b9e8bf..be9e0e422 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -15,28 +15,14 @@ open Genarg open Q_util open Q_coqast open Argextend - -type grammar_tactic_production_expr = - | VernacTerm of string - | VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option -let rec make_patt = function - | [] -> <:patt< [] >> - | VernacNonTerm(_,_,_,Some p)::l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_when loc = function - | [] -> <:expr< True >> - | VernacNonTerm(loc',t,_,Some p)::l -> - let l = make_when loc l in - let loc = join_loc loc' loc in - let t = mlexpr_of_argtype loc' t in - <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> - | _::l -> make_when loc l +open Tacextend +open Pcoq +open Egrammar let rec make_let e = function | [] -> e - | VernacNonTerm(loc,t,_,Some p)::l -> + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> @@ -47,11 +33,6 @@ let add_clause s (_,pt,e) l = let w = Some (make_when (MLast.loc_of_expr e) pt) in (p, w, make_let e pt)::l -let rec extract_signature = function - | [] -> [] - | VernacNonTerm (_,t,_,_) :: l -> t :: extract_signature l - | _::l -> extract_signature l - let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in if not (Util.list_distinct l') then @@ -65,22 +46,9 @@ let make_clauses s l = (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in List.fold_right (add_clause s) l [default] -let rec make_fun e = function - | [] -> e - | VernacNonTerm(loc,_,_,Some p)::l -> - <:expr< fun $lid:p$ -> $make_fun e l$ >> - | _::l -> make_fun e l - -let mlexpr_of_grammar_production = function - | VernacTerm s -> - <:expr< Egrammar.TacTerm $mlexpr_of_string s$ >> - | VernacNonTerm (loc,nt,g,sopt) -> - <:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >> - let mlexpr_of_clause = mlexpr_of_list - (fun (a,b,c) -> - mlexpr_of_list mlexpr_of_grammar_production (VernacTerm a::b)) + (fun (a,b,c) -> mlexpr_of_list make_prod_item (GramTerminal a::b)) let declare_command loc s cl = let gl = mlexpr_of_clause cl in @@ -88,6 +56,7 @@ let declare_command loc s cl = <: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$ $gl$; @@ -113,13 +82,13 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = Q_util.interp_entry_name loc e "" in - VernacNonTerm (loc, t, g, Some s) + let t, g = interp_entry_name None e "" in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = Q_util.interp_entry_name loc e sep in - VernacNonTerm (loc, t, g, Some s) + let t, g = interp_entry_name None e sep in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | s = STRING -> - VernacTerm s + GramTerminal s ] ] ; END diff --git a/plugins/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4 index aad3a765d..79c5fe8a8 100644 --- a/plugins/interface/debug_tac.ml4 +++ b/plugins/interface/debug_tac.ml4 @@ -9,6 +9,7 @@ open Util;; open Proof_type;; open Tacexpr;; open Genarg;; +open Extrawit;; let pr_glob_tactic = Pptactic.pr_glob_tactic (Global.env()) @@ -239,9 +240,9 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti by the list of integers given as extra arguments. *) -let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level -let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level -let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level +let rawwit_main_tactic = rawwit_tactic tactic_main_level +let globwit_main_tactic = globwit_tactic tactic_main_level +let wit_main_tactic = wit_tactic tactic_main_level let on_then = function [t1;t2;l] -> diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 64a9b5c8c..d1e2b03ef 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -694,7 +694,7 @@ let xlate_with_names = function None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) -let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level +let rawwit_main_tactic = Extrawit.rawwit_tactic Extrawit.tactic_main_level let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = function @@ -1342,9 +1342,9 @@ and coerce_genarg_to_TARG x = (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula (snd (out_gen (rawwit_open_constr_gen b) x)))) - | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = Option.get (Pcoq.tactic_genarg_level s) in - let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in + | ExtraArgType s as y when Extrawit.is_tactic_genarg y -> + let n = Option.get (Extrawit.tactic_genarg_level s) in + let t = xlate_tactic (out_gen (Extrawit.rawwit_tactic n) x) in CT_coerce_TACTIC_COM_to_TARG t | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" | BindingsArgType -> xlate_error "TODO: generic with bindings" @@ -1437,9 +1437,9 @@ let coerce_genarg_to_VARG x = (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x))) | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" - | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = Option.get (Pcoq.tactic_genarg_level s) in - let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in + | ExtraArgType s as y when Extrawit.is_tactic_genarg y -> + let n = Option.get (Extrawit.tactic_genarg_level s) in + let t = xlate_tactic (out_gen (Extrawit.rawwit_tactic n) x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) | OpenConstrArgType _ -> xlate_error "TODO: generic open constr" | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" @@ -1576,24 +1576,24 @@ let xlate_level = function | Extend.NextLevel -> CT_next_level;; let xlate_syntax_modifier = function - Extend.SetItemLevel((s::sl), level) -> + SetItemLevel((s::sl), level) -> CT_set_item_level (CT_id_ne_list(CT_ident s, List.map (fun s -> CT_ident s) sl), xlate_level level) - | Extend.SetItemLevel([], _) -> assert false - | Extend.SetLevel level -> CT_set_level (CT_int level) - | Extend.SetAssoc Gramext.LeftA -> CT_lefta - | Extend.SetAssoc Gramext.RightA -> CT_righta - | Extend.SetAssoc Gramext.NonA -> CT_nona - | Extend.SetEntryType(x,typ) -> + | SetItemLevel([], _) -> assert false + | SetLevel level -> CT_set_level (CT_int level) + | SetAssoc Gramext.LeftA -> CT_lefta + | SetAssoc Gramext.RightA -> CT_righta + | SetAssoc Gramext.NonA -> CT_nona + | SetEntryType(x,typ) -> CT_entry_type(CT_ident x, match typ with Extend.ETName -> CT_ident "ident" | Extend.ETReference -> CT_ident "global" | Extend.ETBigint -> CT_ident "bigint" | _ -> xlate_error "syntax_type not parsed") - | Extend.SetOnlyParsing -> CT_only_parsing - | Extend.SetFormat(_,s) -> CT_format(CT_string s);; + | SetOnlyParsing -> CT_only_parsing + | SetFormat(_,s) -> CT_format(CT_string s);; let rec xlate_module_type = function diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index da7ae038a..5342f961d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -46,6 +46,7 @@ open Inductiveops open Syntax_def open Pretyping open Pretyping.Default +open Extrawit open Pcoq let safe_msgnl s = @@ -1659,6 +1660,10 @@ let interp_message ist l = are raised now and not at printing time *) prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l) +let intro_pattern_list_of_Vlist loc env = function + | VList l -> List.map (fun a -> loc,coerce_to_intro_pattern env a) l + | _ -> raise Not_found + let rec interp_intro_pattern ist gl = function | loc, IntroOrAndPattern l -> loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l) @@ -1670,7 +1675,14 @@ let rec interp_intro_pattern ist gl = function as x -> x and interp_or_and_intro_pattern ist gl = - List.map (List.map (interp_intro_pattern ist gl)) + List.map (interp_intro_pattern_list_as_list ist gl) + +and interp_intro_pattern_list_as_list ist gl = function + | [loc,IntroIdentifier id] as l -> + (try intro_pattern_list_of_Vlist loc (pf_env gl) (List.assoc id ist.lfun) + with Not_found | CannotCoerceTo _ -> + List.map (interp_intro_pattern ist gl) l) + | l -> List.map (interp_intro_pattern ist gl) l let interp_in_hyp_as ist gl (id,ipat) = (interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat) @@ -2216,7 +2228,7 @@ and interp_tactic ist tac gl = and interp_atomic ist gl = function (* Basic tactics *) | TacIntroPattern l -> - h_intro_patterns (List.map (interp_intro_pattern ist gl) l) + h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> @@ -2374,9 +2386,8 @@ and interp_atomic ist gl = function VIntroPattern (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType b -> - VIntroPattern - (IntroIdentifier - (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))) + value_of_ident (interp_fresh_ident ist gl + (out_gen (globwit_ident_gen b) x)) | VarArgType -> mk_hyp_value ist gl (out_gen globwit_var x) | RefArgType -> @@ -2405,6 +2416,10 @@ and interp_atomic ist gl = function | List0ArgType IntOrVarArgType -> let wit = wit_list0 globwit_int_or_var in VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) + | List0ArgType (IdentArgType b) -> + let wit = wit_list0 (globwit_ident_gen b) in + let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + VList (List.map mk_ident (out_gen wit x)) | List1ArgType ConstrArgType -> let wit = wit_list1 globwit_constr in VList (List.map (mk_constr_value ist gl) (out_gen wit x)) @@ -2417,6 +2432,10 @@ and interp_atomic ist gl = function | List1ArgType IntOrVarArgType -> let wit = wit_list1 globwit_int_or_var in VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) + | List1ArgType (IdentArgType b) -> + let wit = wit_list1 (globwit_ident_gen b) in + let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + VList (List.map mk_ident (out_gen wit x)) | StringArgType | BoolArgType | QuantHypArgType | RedExprArgType | OpenConstrArgType _ | ConstrWithBindingsArgType @@ -2840,7 +2859,7 @@ let make_absolute_name ident repl = try let id, kn = if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident)) - else let id = Pcoq.coerce_global_to_id ident in + else let id = coerce_reference_to_id ident in Some id, Lib.make_kn id in if Gmap.mem kn !mactab then diff --git a/toplevel/command.ml b/toplevel/command.ml index ed21213ef..4fb56dfd6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -939,7 +939,7 @@ in | InSet -> "_rec_nodep" | InType -> "_rect_nodep") ) in - let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in + let newid = (string_of_id (coerce_reference_to_id y))^suffix in let newref = (dummy_loc,id_of_string newid) in ((newref,x,y,z)::l1),l2 | EqualityScheme x -> l1,(x::l2) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c0105c8b3..09b76d3f3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -28,7 +28,7 @@ open Notation (**********************************************************************) (* Tokens *) -let cache_token (_,s) = Compat.using Pcoq.lexer ("", s) +let cache_token (_,s) = add_token ("", s) let (inToken, outToken) = declare_object {(default_object "TOKEN") with @@ -43,15 +43,20 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s) (**********************************************************************) (* Tactic Notation *) +let interp_prod_item lev = function + | TacTerm s -> GramTerminal s + | TacNonTerm (loc, nt, po) -> + let sep = match po with Some (_,sep) -> sep | _ -> "" in + let (etyp, e) = interp_entry_name (Some lev) nt sep in + GramNonTerminal (loc, etyp, e, Option.map fst po) + let make_terminal_status = function - | VTerm s -> Some s - | VNonTerm _ -> None - -let rec make_tags lev = function - | VTerm s :: l -> make_tags lev l - | VNonTerm (loc, nt, po) :: l -> - let (etyp, _) = Egrammar.interp_entry_name lev nt in - etyp :: make_tags lev l + | GramTerminal s -> Some s + | GramNonTerminal _ -> None + +let rec make_tags = function + | GramTerminal s :: l -> make_tags l + | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l | [] -> [] let cache_tactic_notation (_,(pa,pp)) = @@ -73,11 +78,11 @@ let (inTacticGrammar, outTacticGrammar) = export_function = (fun x -> Some x)} let cons_production_parameter l = function - | VTerm _ -> l - | VNonTerm (_,_,ido) -> Option.List.cons ido l + | GramTerminal _ -> l + | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l let rec tactic_notation_key = function - | VTerm id :: _ -> id + | GramTerminal id :: _ -> id | _ :: l -> tactic_notation_key l | [] -> "terminal_free_notation" @@ -86,7 +91,8 @@ let rec next_key_away key t = else key let add_tactic_notation (n,prods,e) = - let tags = make_tags n prods in + let prods = List.map (interp_prod_item n) prods in + let tags = make_tags prods in let key = next_key_away (tactic_notation_key prods) tags in let pprule = (key,tags,(n,List.map make_terminal_status prods)) in let ids = List.fold_left cons_production_parameter [] prods in @@ -570,19 +576,19 @@ let is_not_small_constr = function | _ -> false let rec define_keywords_aux = function - NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l + GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",k) :: l when is_not_small_constr e -> message ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - n1 :: Term("",k) :: define_keywords_aux l + n1 :: GramConstrTerminal("",k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] let define_keywords = function - Term("IDENT",k)::l -> + GramConstrTerminal("IDENT",k)::l -> message ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - Term("",k) :: define_keywords_aux l + GramConstrTerminal("",k) :: define_keywords_aux l | l -> define_keywords_aux l let make_production etyps symbols = @@ -591,9 +597,9 @@ let make_production etyps symbols = (fun t l -> match t with | NonTerminal m -> let typ = List.assoc m etyps in - NonTerm (typ, Some (m,typ)) :: l + GramConstrNonTerminal (typ, Some m) :: l | Terminal s -> - Term (terminal s) :: l + GramConstrTerminal (terminal s) :: l | Break _ -> l | SProdList (x,sl) -> @@ -606,7 +612,7 @@ let make_production etyps symbols = | _ -> error "Component of recursive patterns in notation must be constr." in let typ = ETConstrList (y,sl) in - NonTerm (typ, Some (x,typ)) :: l) + GramConstrNonTerminal (typ, Some x) :: l) symbols [] in define_keywords prod diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index d4b61eb00..4973cdfe6 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -24,7 +24,7 @@ val add_token_obj : string -> unit (* Adding a tactic notation in the environment *) val add_tactic_notation : - int * grammar_production list * raw_tactic_expr -> unit + int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit (* Adding a (constr) notation in the environment*) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 94ebce9ea..47b36ede0 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -171,9 +171,17 @@ type inductive_expr = type module_binder = bool option * lident list * module_type_ast -type grammar_production = - | VTerm of string - | VNonTerm of loc * string * Names.identifier option +type grammar_tactic_prod_item_expr = + | TacTerm of string + | TacNonTerm of loc * string * (Names.identifier * string) option + +type syntax_modifier = + | SetItemLevel of string list * production_level + | SetLevel of int + | SetAssoc of Gramext.g_assoc + | SetEntryType of string * simple_constr_prod_entry_key + | SetOnlyParsing + | SetFormat of string located type proof_end = | Admitted @@ -191,7 +199,7 @@ type vernac_expr = | VernacTimeout of int * vernac_expr (* Syntax *) - | VernacTacticNotation of int * grammar_production list * raw_tactic_expr + | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring |