GMake (p.coq-core.8.18.0.doc.coq-core.gramlib.Gramlib.Grammar.GMake)

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

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

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 ->
  ('a, norec, 'c) Symbol.t option

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

Sourcetype 's add_kw = {

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

}

Source

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

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

Sourcemodule Unsafe : sig ... end