diff options
| -rw-r--r-- | gramlib/grammar.ml | 15 | ||||
| -rw-r--r-- | gramlib/grammar.mli | 15 | ||||
| -rw-r--r-- | gramlib/plexing.ml | 13 | ||||
| -rw-r--r-- | gramlib/plexing.mli | 13 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 4 |
5 files changed, 28 insertions, 32 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 814844508b..834850082e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -8,19 +8,6 @@ open Util (* Functorial interface *) -module type GLexerType = sig - include Plexing.Lexer - - module State : sig - type t - val init : unit -> t - val set : t -> unit - val get : unit -> t - val drop : unit -> unit - val get_comments : t -> ((int * int) * string) list - end -end - type norec type mayrec @@ -115,7 +102,7 @@ end (* Implementation *) -module GMake (L : GLexerType) = struct +module GMake (L : Plexing.S) = struct type te = L.te type 'c pattern = 'c L.pattern diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 16e147de3b..0872321da0 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -17,18 +17,6 @@ (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) -module type GLexerType = sig - include Plexing.Lexer - - module State : sig - type t - val init : unit -> t - val set : t -> unit - val get : unit -> t - val drop : unit -> unit - val get_comments : t -> ((int * int) * string) list - end -end type norec type mayrec @@ -130,5 +118,4 @@ end type (instead of (string * string)); the module parameter must specify a way to show them as (string * string) *) -module GMake (L : GLexerType) : - S with type te = L.te and type 'c pattern = 'c L.pattern +module GMake (L : Plexing.S) : S with type te = L.te and type 'c pattern = 'c L.pattern diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index e881ab3350..ce3e38ff08 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -5,7 +5,7 @@ type location_function = int -> Loc.t type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function -module type Lexer = sig +module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option @@ -15,4 +15,15 @@ module type Lexer = sig val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string + + (* State for the comments, at some point we should make it functional *) + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end + end diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 521eba7446..0c190af635 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -15,7 +15,7 @@ and location_function = int -> Loc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) -module type Lexer = sig +module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option @@ -25,4 +25,15 @@ module type Lexer = sig val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string + + (* State for the comments, at some point we should make it functional *) + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end + end diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 67b8310bde..ac2c5bcfe2 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -55,7 +55,7 @@ val terminal_numeral : string -> NumTok.Unsigned.t Tok.p (** The lexer of Coq: *) module Lexer : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p module Error : sig type t @@ -74,4 +74,4 @@ it was not in a comment, possibly becoming multiple tokens *) module LexerDiff : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p |