coq 8.7.2 · OCaml Package

type te = Tok.t

type parsable

val tokens : string -> (string * int) list

val glexer : te Plexing.lexer

val set_algorithm : Grammar.parse_algorithm -> unit

module Entry : sig ... end

type ('self, 'a) ty_symbol

type ('self, 'f, 'r) ty_rule

type 'a ty_production

val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol

val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol

val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol

val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol

val s_list0sep : 
  ('self, 'a) ty_symbol ->
  ('self, 'b) ty_symbol ->
  bool ->
  ('self, 'a list) ty_symbol

val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol

val s_list1sep : 
  ('self, 'a) ty_symbol ->
  ('self, 'b) ty_symbol ->
  bool ->
  ('self, 'a list) ty_symbol

val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol

val s_flag : ('self, 'a) ty_symbol -> ('self, bool) ty_symbol

val s_self : ('self, 'self) ty_symbol

val s_next : ('self, 'self) ty_symbol

val s_token : Plexing.pattern -> ('self, string) ty_symbol

val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol

val s_vala : 
  string list ->
  ('self, 'a) ty_symbol ->
  ('self, 'a Ploc.vala) ty_symbol

val r_stop : ('self, 'r, 'r) ty_rule

val r_next : 
  ('self, 'a, 'r) ty_rule ->
  ('self, 'b) ty_symbol ->
  ('self, 'b -> 'a, 'r) ty_rule

val r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule

val production : (('a, 'f, Ploc.t -> 'a) ty_rule * 'f) -> 'a ty_production

module Unsafe : sig ... end

val extend : 
  'a Entry.e ->
  Gramext.position option ->
  (string option
   * Gramext.g_assoc option
   * (te Gramext.g_symbol list * Gramext.g_action) list)
    list ->
  unit

val safe_extend : 
  'a Entry.e ->
  Gramext.position option ->
  (string option * Gramext.g_assoc option * 'a ty_production list) list ->
  unit

val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit

val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit

type 'a entry = 'a Entry.e

type internal_entry = Tok.t Gramext.g_entry

type symbol = Tok.t Gramext.g_symbol

type action = Gramext.g_action

type production_rule = symbol list * action

type single_extend_statment =
  string option * Gramext.g_assoc option * production_rule list

type extend_statment = Gramext.position option * single_extend_statment list

type coq_parsable

val parsable : ?file:string -> char Stream.t -> coq_parsable

val action : 'a -> action

val entry_create : string -> 'a entry

val entry_parse : 'a entry -> coq_parsable -> 'a

val entry_print : Format.formatter -> 'a entry -> unit

val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b

val srules' : production_rule list -> symbol

val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a

package coq