From 7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 20 May 2018 18:59:00 +0200 Subject: [api] Make `vernac/` self-contained. We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor. --- parsing/pcoq.ml | 41 ----------------------------------------- 1 file changed, 41 deletions(-) (limited to 'parsing/pcoq.ml') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 258c4bb11..b78c35c26 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -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 @@ -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 *) -- cgit v1.2.3