diff options
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r-- | parsing/pcoq.ml | 362 |
1 files changed, 243 insertions, 119 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7dc02190..258c4bb1 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -1,46 +1,211 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp -open Compat open CErrors open Util open Extend open Genarg +let curry f x y = f (x, y) +let uncurry f (x,y) = f x y + +(** Location Utils *) +let coq_file_of_ploc_file s = + if s = "" then Loc.ToplevelInput else Loc.InFile s + +let to_coqloc loc = + { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); + Loc.line_nb = Ploc.line_nb loc; + Loc.bol_pos = Ploc.bol_pos loc; + Loc.bp = Ploc.first_pos loc; + Loc.ep = Ploc.last_pos loc; + Loc.line_nb_last = Ploc.line_nb_last loc; + Loc.bol_pos_last = Ploc.bol_pos_last loc; } + +let (!@) = to_coqloc + (** The parser of Coq *) +module G : sig + + include Grammar.S with type te = Tok.t + +(* where Grammar.S + +module type S = + sig + type te = 'x; + type parsable = 'x; + value parsable : Stream.t char -> parsable; + value tokens : string -> list (string * int); + value glexer : Plexing.lexer te; + value set_algorithm : parse_algorithm -> unit; + module Entry : + sig + type e 'a = 'y; + value create : string -> e 'a; + value parse : e 'a -> parsable -> 'a; + value parse_token : e 'a -> Stream.t te -> 'a; + value name : e 'a -> string; + value of_parser : string -> (Stream.t te -> 'a) -> e 'a; + value print : Format.formatter -> e 'a -> unit; + external obj : e 'a -> Gramext.g_entry te = "%identity"; + end + ; + module Unsafe : + sig + value gram_reinit : Plexing.lexer te -> unit; + value clear_entry : Entry.e 'a -> unit; + end + ; + value extend : + Entry.e 'a -> option Gramext.position -> + list + (option string * option Gramext.g_assoc * + list (list (Gramext.g_symbol te) * Gramext.g_action)) -> + unit; + value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; + end + *) + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + string option * Gramext.g_assoc option * production_rule list + type extend_statment = + Gramext.position option * single_extend_statment list + type coq_parsable + + val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable + val action : 'a -> action + val entry_create : string -> 'a entry + val entry_parse : 'a entry -> coq_parsable -> 'a + val entry_print : Format.formatter -> 'a entry -> unit + + val comment_state : coq_parsable -> ((int * int) * string) list + + val srules' : production_rule list -> symbol + val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + +end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct + + include Grammar.GMake(CLexer) + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + string option * Gramext.g_assoc option * production_rule list + type extend_statment = + Gramext.position option * single_extend_statment list + + type coq_parsable = parsable * CLexer.lexer_state ref + + let parsable ?(file=Loc.ToplevelInput) c = + let state = ref (CLexer.init_lexer_state file) in + CLexer.set_lexer_state !state; + let a = parsable c in + state := CLexer.get_lexer_state (); + (a,state) + + let action = Gramext.action + let entry_create = Entry.create + + let entry_parse e (p,state) = + CLexer.set_lexer_state !state; + try + let c = Entry.parse e p in + state := CLexer.get_lexer_state (); + c + with Ploc.Exc (loc,e) -> + CLexer.drop_lexer_state (); + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in + Loc.raise ~loc e + + let comment_state (p,state) = + CLexer.get_comment_state !state + + let entry_print ft x = Entry.print ft x + + (* Not used *) + let srules' = Gramext.srules + let parse_tokens_after_filter = Entry.parse_token + +end -module G = GrammarMake (CLexer) -let warning_verbose = Compat.warning_verbose +let warning_verbose = Gramext.warning_verbose let of_coq_assoc = function -| Extend.RightA -> CompatGramext.RightA -| Extend.LeftA -> CompatGramext.LeftA -| Extend.NonA -> CompatGramext.NonA +| Extend.RightA -> Gramext.RightA +| Extend.LeftA -> Gramext.LeftA +| Extend.NonA -> Gramext.NonA let of_coq_position = function -| Extend.First -> CompatGramext.First -| Extend.Last -> CompatGramext.Last -| Extend.Before s -> CompatGramext.Before s -| Extend.After s -> CompatGramext.After s -| Extend.Level s -> CompatGramext.Level s +| Extend.First -> Gramext.First +| Extend.Last -> Gramext.Last +| Extend.Before s -> Gramext.Before s +| Extend.After s -> Gramext.After s +| Extend.Level s -> Gramext.Level s + +module Symbols : sig + val stoken : Tok.t -> G.symbol + val sself : G.symbol + val snext : G.symbol + val slist0 : G.symbol -> G.symbol + val slist0sep : G.symbol * G.symbol -> G.symbol + val slist1 : G.symbol -> G.symbol + val slist1sep : G.symbol * G.symbol -> G.symbol + val sopt : G.symbol -> G.symbol + val snterml : G.internal_entry * string -> G.symbol + val snterm : G.internal_entry -> G.symbol +end = struct + + let stoken tok = + let pattern = match tok with + | Tok.KEYWORD s -> "", s + | Tok.IDENT s -> "IDENT", s + | Tok.PATTERNIDENT s -> "PATTERNIDENT", s + | Tok.FIELD s -> "FIELD", s + | Tok.INT s -> "INT", s + | Tok.STRING s -> "STRING", s + | Tok.LEFTQMARK -> "LEFTQMARK", "" + | Tok.BULLET s -> "BULLET", s + | Tok.EOI -> "EOI", "" + in + Gramext.Stoken pattern -module Symbols = GramextMake(G) + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) -let camlp4_verbosity silent f x = + let snterml (x, y) = Gramext.Snterml (x, y) + let snterm x = Gramext.Snterm x + let sself = Gramext.Sself + let snext = Gramext.Snext + let slist0 x = Gramext.Slist0 x + let slist1 x = Gramext.Slist1 x + let sopt x = Gramext.Sopt x + +end + +let camlp5_verbosity silent f x = let a = !warning_verbose in warning_verbose := silent; f x; warning_verbose := a -let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x - (** Grammar extensions *) (** NB: [extend_statment = @@ -55,7 +220,7 @@ let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x (** Binding general entry keys to symbol *) let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function -| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc)) +| Stop -> fun f -> G.action (fun loc -> f (!@ loc)) | Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function @@ -107,7 +272,7 @@ type ext_kind = (** The list of extensions *) -let camlp4_state = ref [] +let camlp5_state = ref [] (** Deletion *) @@ -121,10 +286,10 @@ let grammar_delete e reinit (pos,rls) = let a = of_coq_assoc a in let ext = of_coq_position ext in let lev = match pos with - | Some (CompatGramext.Level n) -> n + | Some (Gramext.Level n) -> n | _ -> assert false in - maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + (G.extend e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -132,13 +297,13 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in - camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in + camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = - camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; - camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; + camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -147,21 +312,21 @@ module Gram = struct include G let extend e = - maybe_curry - (fun ext -> - camlp4_state := - (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> maybe_uncurry (G.extend e) ext))) - :: !camlp4_state; - maybe_uncurry (G.extend e) ext) + curry + (fun ext -> + camlp5_state := + (ByEXTEND ((fun () -> grammar_delete e None ext), + (fun () -> uncurry (G.extend e) ext))) + :: !camlp5_state; + uncurry (G.extend e) ext) let delete_rule e pil = (* spiwack: if you use load an ML module which contains GDELETE_RULE - in a section, God kills a kitty. As it would corrupt remove_grammars. + in a section, God kills a kitty. As it would corrupt remove_grammars. There does not seem to be a good way to undo a delete rule. As deleting - takes fewer arguments than extending. The production rule isn't returned - by delete_rule. If we could retrieve the necessary information, then - ByEXTEND provides just the framework we need to allow this in section. - I'm not entirely sure it makes sense, but at least it would be more correct. + takes fewer arguments than extending. The production rule isn't returned + by delete_rule. If we could retrieve the necessary information, then + ByEXTEND provides just the framework we need to allow this in section. + I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil end @@ -173,18 +338,18 @@ module Gram = let rec remove_grammars n = if n>0 then - (match !camlp4_state with - | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") + (match !camlp5_state with + | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); - camlp4_state := t; + camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> undo(); - camlp4_state := t; + camlp5_state := t; remove_grammars n; redo(); - camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state) let make_rule r = [None, None, r] @@ -194,14 +359,14 @@ let eoi_entry en = let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in let act = Gram.action (fun _ x loc -> x) in - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e let map_entry f en = let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in let symbs = [Symbols.snterm (Gram.Entry.obj en)] in let act = Gram.action (fun x loc -> f x) in - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e (* Parse a string, does NOT check if the entire string was read @@ -267,6 +432,7 @@ module Prim = let integer = gec_gen "integer" let bigint = Gram.entry_create "Prim.bigint" let string = gec_gen "string" + let lstring = Gram.entry_create "Prim.lstring" let reference = make_gen_entry uprim "reference" let by_notation = Gram.entry_create "by_notation" let smart_global = Gram.entry_create "smart_global" @@ -276,7 +442,8 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" - let pidentref = Gram.entry_create "Prim.pidentref" + let univ_decl = Gram.entry_create "Prim.univ_decl" + let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" @@ -306,6 +473,7 @@ module Constr = let global = make_gen_entry uconstr "global" let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" + let sort_family = make_gen_entry uconstr "sort_family" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" @@ -325,48 +493,6 @@ module Module = let module_type = Gram.entry_create "module_type" end -module Tactic = - struct - (* Main entry for extensions *) - let simple_tactic = Gram.entry_create "tactic:simple_tactic" - - (* Entries that can be referred via the string -> Gram.entry table *) - (* Typically for tactic user extensions *) - let open_constr = - make_gen_entry utactic "open_constr" - let constr_with_bindings = - make_gen_entry utactic "constr_with_bindings" - let bindings = - make_gen_entry utactic "bindings" - let hypident = Gram.entry_create "hypident" - let constr_may_eval = make_gen_entry utactic "constr_may_eval" - let constr_eval = make_gen_entry utactic "constr_eval" - let uconstr = - make_gen_entry utactic "uconstr" - let quantified_hypothesis = - make_gen_entry utactic "quantified_hypothesis" - let destruction_arg = make_gen_entry utactic "destruction_arg" - let int_or_var = make_gen_entry utactic "int_or_var" - let red_expr = make_gen_entry utactic "red_expr" - let simple_intropattern = - make_gen_entry utactic "simple_intropattern" - let in_clause = make_gen_entry utactic "in_clause" - let clause_dft_concl = - make_gen_entry utactic "clause" - - - (* Main entries for ltac *) - let tactic_arg = Gram.entry_create "tactic:tactic_arg" - let tactic_expr = make_gen_entry utactic "tactic_expr" - let binder_tactic = make_gen_entry utactic "binder_tactic" - - let tactic = make_gen_entry utactic "tactic" - - (* Main entry for quotations *) - let tactic_eoi = eoi_entry tactic - - end - module Vernac_ = struct let gec_vernac s = Gram.entry_create ("vernac:" ^ s) @@ -376,22 +502,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" - let vernac_eoi = eoi_entry vernac + 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 (!@loc, v)) in + 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) ], act_vernac ); + ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); ] in - maybe_uncurry (Gram.extend main_entry) (None, make_rule rule) + uncurry (Gram.extend main_entry) (None, make_rule rule) let command_entry_ref = ref noedit_mode let command_entry = @@ -409,16 +535,16 @@ 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 let entry = G.entry_create "epsilon" in - let () = maybe_uncurry (G.extend entry) ext in + let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) -module GramState = Store.Make(struct end) +module GramState = Store.Make () type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t -module GrammarCommand = Dyn.Make(struct end) +module GrammarCommand = Dyn.Make () module GrammarInterp = struct type 'a t = 'a grammar_extension end module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) @@ -458,9 +584,9 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command ta (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t +type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state -let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) +let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -475,7 +601,7 @@ let unfreeze (grams, lex) = let n = number_of_entries undo in remove_grammars n; grammar_stack := common; - CLexer.unfreeze lex; + CLexer.set_keyword_state lex; List.iter extend_dyn_grammar (List.rev_map pi2 redo) (** No need to provide an init function : the grammar state is @@ -483,8 +609,8 @@ let unfreeze (grams, lex) = the lexer state should not be resetted, since it contains keywords declared in g_*.ml4 *) -let _ = - Summary.declare_summary "GRAMMAR_LEXER" +let parser_summary_tag = + Summary.declare_summary_tag "GRAMMAR_LEXER" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = Summary.nop } @@ -501,27 +627,25 @@ let with_grammar_rule_protection f x = let () = let open Stdarg in - let open Constrarg in -(* Grammar.register0 wit_unit; *) -(* Grammar.register0 wit_bool; *) Grammar.register0 wit_int (Prim.integer); Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); - Grammar.register0 wit_int_or_var (Tactic.int_or_var); - Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern); Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); - Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); + Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_uconstr (Tactic.uconstr); - Grammar.register0 wit_open_constr (Tactic.open_constr); - Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); - Grammar.register0 wit_bindings (Tactic.bindings); -(* Grammar.register0 wit_hyp_location_flag; *) - Grammar.register0 wit_red_expr (Tactic.red_expr); - Grammar.register0 wit_tactic (Tactic.tactic); - Grammar.register0 wit_ltac (Tactic.tactic); - Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); - Grammar.register0 wit_destruction_arg (Tactic.destruction_arg); + Grammar.register0 wit_red_expr (Vernac_.red_expr); () + +(** Registering extra grammar *) + +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty + +let register_grammars_by_name name grams = + grammar_names := String.Map.add name grams !grammar_names + +let find_grammars_by_name name = + String.Map.find name !grammar_names |