package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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 ':'

val add_keyword : ?quotation:starts_quotation -> string -> unit

This should be functional but it is not due to the interface

val remove_keyword : string -> unit
val is_keyword : string -> bool
val keywords : unit -> CString.Set.t
type keyword_state
val set_keyword_state : keyword_state -> unit
val get_keyword_state : unit -> keyword_state
val check_ident : string -> unit
val is_ident : string -> bool
val check_keyword : string -> unit
val terminal : string -> string Tok.p

When string is not an ident, returns a keyword.

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

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

The lexer of Coq:

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

Create a lexer. true enables alternate handling for computing diffs. It 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 "(*" 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
module LexerDiff : Gramlib.Plexing.S with 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