package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.2.0.tar.gz

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.gramlib/Gramlib/Grammar/module-type-ExtS/index.html

Module type `Grammar.ExtS`Source

type keyword_state

module EState : sig ... end

module GState : sig ... end

include S
  with type keyword_state := keyword_state
   and type 'a with_gstate := GState.t -> 'a
   and type 'a with_kwstate := keyword_state -> 'a
   and type 'a with_estate := EState.t -> 'a
   and type 'a mod_estate := EState.t -> EState.t * 'a

type te

type 'c pattern

type ty_pattern =

| 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

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 =

| 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.
*)

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

val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option

type 's add_kw = {

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

}

val safe_extend : 
  's add_kw ->
  EState.t ->
  's ->
  'a Entry.t ->
  'a extend_statement ->
  EState.t * 's

module Unsafe : sig ... end