diff options
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r-- | parsing/pcoq.ml | 61 |
1 files changed, 10 insertions, 51 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 258c4bb11..6fdd9ea9b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -79,10 +79,10 @@ module type S = type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action type production_rule = symbol list * action - type single_extend_statment = + type single_extend_statement = string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list + type extend_statement = + Gramext.position option * single_extend_statement list type coq_parsable val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable @@ -105,10 +105,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action type production_rule = symbol list * action - type single_extend_statment = + type single_extend_statement = string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list + type extend_statement = + Gramext.position option * single_extend_statement list type coq_parsable = parsable * CLexer.lexer_state ref @@ -145,7 +145,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct end - let warning_verbose = Gramext.warning_verbose let of_coq_assoc = function @@ -208,9 +207,9 @@ let camlp5_verbosity silent f x = (** Grammar extensions *) -(** NB: [extend_statment = - gram_position option * single_extend_statment list] - and [single_extend_statment = +(** NB: [extend_statement = + gram_position option * single_extend_statement list] + and [single_extend_statement = string option * gram_assoc option * production_rule list] and [production_rule = symbol list * action] @@ -264,7 +263,7 @@ let of_coq_extend_statement (pos, st) = type gram_reinit = gram_assoc * gram_position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule type ext_kind = | ByGrammar of extend_rule @@ -387,7 +386,6 @@ let create_universe u = let uprim = create_universe "prim" let uconstr = create_universe "constr" let utactic = create_universe "tactic" -let uvernac = create_universe "vernac" let get_univ u = if Hashtbl.mem utables u then u @@ -493,44 +491,6 @@ module Module = let module_type = Gram.entry_create "module_type" end -module Vernac_ = - struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) - - (* The different kinds of vernacular commands *) - let gallina = gec_vernac "gallina" - let gallina_ext = gec_vernac "gallina_ext" - let command = gec_vernac "command" - let syntax = gec_vernac "syntax_command" - let vernac_control = gec_vernac "Vernac.vernac_control" - let rec_definition = gec_vernac "Vernac.rec_definition" - let red_expr = make_gen_entry utactic "red_expr" - let hint_info = gec_vernac "hint_info" - (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" - let noedit_mode = gec_vernac "noedit_command" - - let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in - let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); - ] in - uncurry (Gram.extend main_entry) (None, make_rule rule) - - let command_entry_ref = ref noedit_mode - let command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) - - end - -let main_entry = Vernac_.main_entry - -let set_command_entry e = Vernac_.command_entry_ref := e -let get_command_entry () = !Vernac_.command_entry_ref - let epsilon_value f e = let r = Rule (Next (Stop, e), fun x _ -> f x) in let ext = of_coq_extend_statement (None, [None, None, [r]]) in @@ -635,7 +595,6 @@ let () = Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_red_expr (Vernac_.red_expr); () (** Registering extra grammar *) |