GMake (coq-core.Gramlib.Grammar.GMake)

Parameters

module L : Plexing.S

Signature

module EState : sig ... end

module 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

type ty_pattern =

| TPattern : 'a L.pattern -> ty_pattern

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

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 ->
  ( 'a, 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 L.pattern -> 's;

}

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

val safe_delete_rule : EState.t -> 'a Entry.t -> 'a Production.t -> EState.t

module Unsafe : sig ... end