package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz

sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.gramlib/Gramlib/Grammar/GMake/index.html

Module `Grammar.GMake`Source

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 =

| 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

Source

type 'a single_extend_statement =
  string option * Gramext.g_assoc option * 'a Production.t list

Sourcetype 'a extend_statement =

| Reuse of string option * 'a Production.t list
(*
Extend an existing level by its optional given name. If None, picks the topmost level.
*)
| Fresh of Gramext.position * 'a single_extend_statement list
(*
Create a level at the given position.
*)

Source

val generalize_symbol : 
  ('a, 'tr, 'c) Symbol.t ->
  ('b, norec, 'c) Symbol.t option

Sourceval level_of_nonterm : (_, _, _) Symbol.t -> string option

If the symbol is nterml returns the level, otherwise None

Sourceval safe_extend : EState.t -> 'a Entry.t -> 'a extend_statement -> EState.t

Sourcetype 's add_kw = {

add_kw : 'c. 's -> 'c L.pattern -> 's;

}

Sourceval add_extend_kws : 's add_kw -> 's -> _ extend_statement -> 's

Sourcemodule Unsafe : sig ... end