package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CLexerSource

Sourcetype starts_quotation =
  1. | NoQuotation
  2. | Quotation

When one registers a keyword she can declare it starts a quotation. In particular using QUOTATION("name:") in a grammar rule declares "name:" as a keyword and the token QUOTATION is matched whenever the keyword is followed by an identifier or a parenthesized text. Eg

constr:x string:.... ltac:(....) ltac:....

The delimiter is made of 1 or more occurrences of the same parenthesis, eg ((.....)) or [[[....]]]. The idea being that if the text happens to contain the closing delimiter, one can make the delimiter longer and avoid confusion (no escaping). Eg

string:[ .. ']' .. ]

Nesting the delimiter is allowed, eg ((..((...))..)) is OK.

Keywords don't need to end in ':'

Sourcetype keyword_state
Sourceval empty_keyword_state : keyword_state
Sourceval add_keyword : ?quotation:starts_quotation -> keyword_state -> string -> keyword_state
Sourceval is_keyword : keyword_state -> string -> bool
Sourceval check_ident : string -> unit
Sourceval is_ident : string -> bool
Sourceval check_keyword : string -> unit
Sourceval add_keyword_tok : keyword_state -> 'c Tok.p -> keyword_state
Sourceval terminal : keyword_state -> string -> string Tok.p

When string is not an ident, returns a keyword.

Sourceval terminal_number : string -> NumTok.Unsigned.t Tok.p

Precondition: the input is a number (c.f. NumTok.t)

Sourceval after : Loc.t -> Loc.t

after loc Will advance a lexing location as the lexer does; this can be used to implement parsing resumption from a given position:

  let loc = Pcoq.Parsable.loc pa |> after in
  let str = Gramlib.Stream.of_string text in
  (* Stream.count being correct is critical for Coq's lexer *)
  Gramlib.Stream.njunk loc.ep str;
  let pa = Pcoq.Parsable.make ~loc str in
  (* ready to resume parsing *)

The lexer of Coq:

Sourcemodule Lexer : Gramlib.Plexing.S with type keyword_state = keyword_state and type te = Tok.t and type 'c pattern = 'c Tok.p
Sourcemodule Error : sig ... end

LexerDiff ensures that, ignoring white space, the concatenated tokens equal the input string. Specifically:

  • for strings, return the enclosing quotes as tokens and treat the quoted value as if it was unquoted, possibly becoming multiple tokens.
  • for comments, return the "(\*" (\ to be kind to syntax highlighters) as a token and treat the contents of the comment as if it was not in a comment, possibly becoming multiple tokens.
  • return any unrecognized Ascii or UTF-8 character as a string.
Sourcemodule LexerDiff : Gramlib.Plexing.S with type keyword_state = keyword_state and type te = Tok.t and type 'c pattern = 'c Tok.p
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct