package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. 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/module-type-S/index.html

Module type Grammar.SSource

type keyword_state
type te
type 'c pattern
type ty_pattern =
  1. | TPattern : 'a pattern -> ty_pattern
type peek_error = unit
type '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

type 'a with_gstate

Reader of grammar state

type 'a with_kwstate

Read keyword state

type 'a with_estate

Read entry state

type 'a mod_estate

Read/write entry state

module Parsable : sig ... end
module Entry : sig ... end
module Symbol : sig ... end
module Rule : sig ... end
module Rules : sig ... end
module Production : sig ... end
type 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list
type '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.

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

If the symbol is nterml returns the level, otherwise None