package rocq-runtime

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

Module Grammar.GMakeSource

Parameters

module L : Plexing.S

Signature

Sourcemodule EState : sig ... end
Sourcemodule GState : sig ... end
include S with type keyword_state := L.keyword_state and type 'a with_gstate := GState.t -> 'a and type 'a with_kwstate := L.keyword_state -> 'a and type 'a with_estate := EState.t -> 'a and type 'a mod_estate := EState.t -> EState.t * 'a with type te := L.te with type 'c pattern := 'c L.pattern
Sourcetype ty_pattern =
  1. | TPattern : 'a L.pattern -> ty_pattern
Sourcetype peek_error = unit
Sourcetype 'a parser_v = ('a, peek_error) result

Recoverable parsing errors are signaled use Error. To be correctly recovered we must not have consumed any tokens since the last choice point, ie we only peeked at the stream.

Other errors are signaled using the ParseError exception or even arbitrary exceptions.

Type combinators to factor the module type between explicit state passing in Grammar and global state in Procq

Sourcemodule Parsable : sig ... end
Sourcemodule Entry : sig ... end
Sourcemodule Symbol : sig ... end
Sourcemodule Rule : sig ... end
Sourcemodule Rules : sig ... end
Sourcemodule Production : sig ... end
Sourcetype 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list
Sourcetype 'a extend_statement =
  1. | Reuse of string option * 'a Production.t list
    (*

    Extend an existing level by its optional given name. If None, picks the topmost level.

    *)
  2. | Fresh of Gramext.position * 'a single_extend_statement list
    (*

    Create a level at the given position.

    *)
Sourceval generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('b, norec, 'c) Symbol.t option
Sourceval level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
Sourcetype 's add_kw = {
  1. add_kw : 'c. 's -> 'c L.pattern -> 's;
}
Sourceval safe_extend : 's add_kw -> EState.t -> 's -> 'a Entry.t -> 'a extend_statement -> EState.t * 's
Sourcemodule Unsafe : sig ... end