From f99f60902d7492902110fb091c52e58e1ed9cd32 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 19 Oct 2017 18:17:33 +0200 Subject: Use a homebrew parser to replace the GEXTEND extension points of Camlp5. The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one. --- parsing/extend.ml | 2 +- parsing/pcoq.ml | 11 ++++++++++- parsing/pcoq.mli | 3 +++ 3 files changed, 14 insertions(+), 2 deletions(-) (limited to 'parsing') diff --git a/parsing/extend.ml b/parsing/extend.ml index 6805a96ed..f57e32c88 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -101,7 +101,7 @@ type ('self, 'a) symbol = | Aself : ('self, 'self) symbol | Anext : ('self, 'self) symbol | Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * int -> ('self, 'a) symbol +| Aentryl : 'a entry * string -> ('self, 'a) symbol | Arules : 'a rules list -> ('self, 'a) symbol and ('self, _, 'r) rule = diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 6fdd9ea9b..171276a70 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -17,9 +17,17 @@ let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) +let ploc_file_of_coq_file = function +| Loc.ToplevelInput -> "" +| Loc.InFile f -> f + let coq_file_of_ploc_file s = if s = "" then Loc.ToplevelInput else Loc.InFile s +let of_coqloc loc = + let open Loc in + Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) "" + let to_coqloc loc = { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); Loc.line_nb = Ploc.line_nb loc; @@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aentry e -> Symbols.snterm (G.Entry.obj e) | Aentryl (e, n) -> - Symbols.snterml (G.Entry.obj e, string_of_int n) + Symbols.snterml (G.Entry.obj e, n) | Arules rs -> G.srules' (List.map symbol_of_rules rs) @@ -328,6 +336,7 @@ module Gram = I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil + let safe_extend e ext = grammar_extend e None ext end (** Remove extensions diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f959bd80c..48604e188 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -80,6 +80,8 @@ module type S = (* Get comment parsing information from the Lexer *) val comment_state : coq_parsable -> ((int * int) * string) list + val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit + (* Apparently not used *) val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a @@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) +val of_coqloc : Loc.t -> Ploc.t val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t -- cgit v1.2.3