Quelle coqpp_ast.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type loc = {
  loc_start : Lexing.position;
  loc_end : Lexing.position;
}

type code = { code : string; loc : loc option; }

type user_symbol =
| Ulist1 of user_symbol
| Ulist1sep of user_symbol * string
| Ulist0 of user_symbol
| Ulist0sep of user_symbol * string
| Uopt of user_symbol
| Uentry of string
| Uentryl of string * int

type token_data =
| TokNone
| TokName of string

type ext_token =
| ExtTerminal of string
| ExtNonTerminal of user_symbol * token_data

type tactic_rule = {
  tac_toks : ext_token list;
  tac_body : code;
}

type level = string

type position =
| First
| Last
| Before of level
| After of level

type assoc =
| LeftA
| RightA
| NonA

type gram_symbol =
| GSymbString of string
| GSymbQualid of string * level option
| GSymbParen of gram_symbol list
| GSymbProd of gram_prod list

and gram_prod = {
  gprod_symbs : (string option * gram_symbol list) list;
  gprod_body : code;
}

type symb =
| SymbToken of string * string option
| SymbEntry of string * string option
| SymbSelf
| SymbNext
| SymbList0 of symb * symb option
| SymbList1 of symb * symb option
| SymbOpt of symb
| SymbRules of ((string option * symb) list * code) list
| SymbQuote of string (** Not used by GRAMMAR EXTEND *)

type gram_rule = {
  grule_label : string option;
  grule_assoc : assoc option;
  grule_prods : gram_prod list;
}

type grammar_rules =
| GDataFresh of position option * gram_rule list
| GDataReuse of string option * gram_prod list

type grammar_entry = {
  gentry_name : string;
  gentry_rules : grammar_rules;
}

type grammar_ext = {
  gramext_name : string;
  gramext_globals : string list;
  gramext_entries : grammar_entry list;
}

type tactic_ext = {
  tacext_name : string;
  tacext_level : int option;
  tacext_deprecated : code option;
  tacext_rules : tactic_rule list;
}

type classification =
| ClassifDefault
| ClassifCode of code
| ClassifName of string

type vernac_rule = {
  vernac_atts : (string * code) list option;
  vernac_state : string option;
  vernac_toks : ext_token list;
  vernac_class : code option;
  vernac_depr : bool;
  vernac_body : code;
  vernac_synterp : (string * code) option;
}

type vernac_ext = {
  vernacext_name : string;
  vernacext_entry : code option;
  vernacext_class : classification;
  vernacext_state : string option;
  vernacext_rules : vernac_rule list;
}

type vernac_argument_ext = {
  vernacargext_name : string;
  vernacargext_printer : code option;
  vernacargext_rules : tactic_rule list;
}

type argument_type =
| ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string

type argument_ext = {
  argext_name : string;
  argext_rules : tactic_rule list;
  argext_type : argument_type option;
  argext_interp : (string option * code) option;
  argext_glob : code option;
  argext_subst : code option;
  argext_rprinter : code option;
  argext_gprinter : code option;
  argext_tprinter : code option;
}

type node =
| Code of code
| Comment of string
| DeclarePlugin of string option
| GramExt of grammar_ext
| VernacExt of vernac_ext
| VernacArgumentExt of vernac_argument_ext
| TacticExt of tactic_ext
| ArgumentExt of argument_ext

type t = node list

quality100%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.