Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vernacexpr.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

open Names
open Constrexpr
open Libnames

(** Vernac expressions, produced by the parser *)
type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation

type goal_identifier = string
type scope_name = string

type goal_reference =
  | OpenSubgoals
  | NthGoal of int
  | GoalId of Id.t

type printable =
  | PrintTables
  | PrintFullContext
  | PrintSectionContext of qualid
  | PrintInspect of int
  | PrintGrammar of string
  | PrintCustomGrammar of string
  | PrintLoadPath of DirPath.t option
  | PrintModules
  | PrintModule of qualid
  | PrintModuleType of qualid
  | PrintNamespace of DirPath.t
  | PrintMLLoadPath
  | PrintMLModules
  | PrintDebugGC
  | PrintName of qualid or_by_notation * UnivNames.univ_name_list option
  | PrintGraph
  | PrintClasses
  | PrintTypeClasses
  | PrintInstances of qualid or_by_notation
  | PrintCoercions
  | PrintCoercionPaths of class_rawexpr * class_rawexpr
  | PrintCanonicalConversions
  | PrintUniverses of bool * qualid list option * string option
  | PrintHint of qualid or_by_notation
  | PrintHintGoal
  | PrintHintDbName of string
  | PrintHintDb
  | PrintScopes
  | PrintScope of string
  | PrintVisibility of string option
  | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
  | PrintImplicit of qualid or_by_notation
  | PrintAssumptions of bool * bool * qualid or_by_notation
  | PrintStrategy of qualid or_by_notation option
  | PrintRegistered

type search_about_item =
  | SearchSubPattern of constr_pattern_expr
  | SearchString of string * scope_name option

type searchable =
  | SearchPattern of constr_pattern_expr
  | SearchRewrite of constr_pattern_expr
  | SearchHead of constr_pattern_expr
  | SearchAbout of (bool * search_about_item) list

type locatable =
  | LocateAny of qualid or_by_notation
  | LocateTerm of qualid or_by_notation
  | LocateLibrary of qualid
  | LocateModule of qualid
  | LocateOther of string * qualid
  | LocateFile of string

type showable =
  | ShowGoal of goal_reference
  | ShowProof
  | ShowScript
  | ShowExistentials
  | ShowUniverses
  | ShowProofNames
  | ShowIntros of bool
  | ShowMatch of qualid

type comment =
  | CommentConstr of constr_expr
  | CommentString of string
  | CommentInt of int

type search_restriction =
  | SearchInside of qualid list
  | SearchOutside of qualid list

type rec_flag       = bool (* true = Rec;           false = NoRec          *)
type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
type instance_flag  = bool option
  (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
type export_flag    = bool (* true = Export;        false = Import         *)
type inductive_flag = Declarations.recursivity_kind
type onlyparsing_flag = Flags.compat_version option
(* Some v = Parse only;  None = Print also.
    If v<>Current, it contains the name of the coq version
    which this notation is trying to be compatible with *)
type locality_flag  = bool (* true = Local *)

type option_setting =
  | OptionUnset
  | OptionSetTrue
  | OptionSetInt of int
  | OptionSetString of string

type option_ref_value =
  | StringRefValue of string
  | QualidRefValue of qualid

(** Identifier and optional list of bound universes and constraints. *)

type sort_expr = Sorts.family

type definition_expr =
  | ProveBody of local_binder_expr list * constr_expr
  | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
      * constr_expr option

type fixpoint_expr =
    ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option

type cofixpoint_expr =
    ident_decl * local_binder_expr list * constr_expr * constr_expr option

type local_decl_expr =
  | AssumExpr of lname * constr_expr
  | DefExpr of lname * constr_expr * constr_expr option

type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
type decl_notation = lstring * constr_expr * scope_name option
type simple_binder = lident list  * constr_expr
type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
type 'a with_instance = instance_flag * 'a
type 'a with_notation = 'a * decl_notation list
type 'a with_priority = 'a * int option
type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
  | Constructors of constructor_expr list
  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
type inductive_expr =
  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
    constructor_list_or_record_decl_expr

type one_inductive_expr =
  lident * local_binder_expr list * constr_expr option * constructor_expr list

type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
and typeclass_context = typeclass_constraint list

type proof_expr =
  ident_decl * (local_binder_expr list * constr_expr)

type syntax_modifier =
  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
  | SetLevel of int
  | SetCustomEntry of string * int option
  | SetAssoc of Gramlib.Gramext.g_assoc
  | SetEntryType of string * Extend.simple_constr_prod_entry_key
  | SetOnlyParsing
  | SetOnlyPrinting
  | SetCompatVersion of Flags.compat_version
  | SetFormat of string * lstring

type proof_end =
  | Admitted
  (*                         name in `Save ident` when closing goal *)
  | Proved of Proof_global.opacity_flag * lident option

type scheme =
  | InductionScheme of bool * qualid or_by_notation * sort_expr
  | CaseScheme of bool * qualid or_by_notation * sort_expr
  | EqualityScheme of qualid or_by_notation

type section_subset_expr =
  | SsEmpty
  | SsType
  | SsSingl of lident
  | SsCompl of section_subset_expr
  | SsUnion of section_subset_expr * section_subset_expr
  | SsSubstr of section_subset_expr * section_subset_expr
  | SsFwdClose of section_subset_expr

(** Extension identifiers for the VERNAC EXTEND mechanism.

    {b ("Extraction", 0} indicates {b Extraction {i qualid}} command.

    {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command.

    {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command.

    {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command.

    {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command.

    {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command.

    {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands.

    {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command.

    {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command.

    {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command.

    {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command.

    {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
*)

(* This type allows registering the inlining of constants in native compiler.
   It will be extended with primitive inductive types and operators *)
type register_kind =
  | RegisterInline
  | RegisterCoqlib of qualid

(** {6 Types concerning the module layer} *)

type module_ast_inl = module_ast * Declaremods.inline
type module_binder = bool option * lident list * module_ast_inl

(** [Some b] if locally enabled/disabled according to [b], [None] if
    we should use the global flag. *)
type vernac_cumulative = VernacCumulative | VernacNonCumulative

(** {6 The type of vernacular expressions} *)

type vernac_argument_status = {
  name : Name.t;
  recarg_like : bool;
  notation_scope : string CAst.t option;
  implicit_status : Impargs.implicit_kind;
}

type extend_name =
  (* Name of the vernac entry where the tactic is defined, typically found
     after the VERNAC EXTEND statement in the source. *)
  string *
  (* Index of the extension in the VERNAC EXTEND statement. Each parsing branch
     is given an offset, starting from zero. *)
  int

type nonrec vernac_expr =

  | VernacLoad of verbose_flag * string
  (* Syntax *)
  | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
  | VernacOpenCloseScope of bool * scope_name
  | VernacDeclareScope of scope_name
  | VernacDelimiters of scope_name * string option
  | VernacBindScope of scope_name * class_rawexpr list
  | VernacInfix of (lstring * syntax_modifier list) *
      constr_expr * scope_name option
  | VernacNotation of
      constr_expr * (lstring * syntax_modifier list) *
      scope_name option
  | VernacNotationAddFormat of string * string * string
  | VernacDeclareCustomEntry of string

  (* Gallina *)
  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
  | VernacEndProof of proof_end
  | VernacExactProof of constr_expr
  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
      Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
  | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
  | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
  | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
  | VernacScheme of (lident option * scheme) list
  | VernacCombinedScheme of lident * lident list
  | VernacUniverse of lident list
  | VernacConstraint of Glob_term.glob_constraint list

  (* Gallina extensions *)
  | VernacBeginSection of lident
  | VernacEndSegment of lident
  | VernacRequire of
      qualid option * export_flag option * qualid list
  | VernacImport of export_flag * qualid list
  | VernacCanonical of qualid or_by_notation
  | VernacCoercion of qualid or_by_notation *
      class_rawexpr * class_rawexpr
  | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
  | VernacNameSectionHypSet of lident * section_subset_expr

  (* Type classes *)
  | VernacInstance of
      local_binder_expr list * (* super *)
        typeclass_constraint * (* instance name, class name, params *)
        (bool * constr_expr) option * (* props *)
        Hints.hint_info_expr

  | VernacDeclareInstance of
      local_binder_expr list * (* super *)
        (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *)
        Hints.hint_info_expr

  | VernacContext of local_binder_expr list

  | VernacExistingInstance of
    (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)

  | VernacExistingClass of qualid (* inductive or definition name *)

  (* Modules and Module Types *)
  | VernacDeclareModule of bool option * lident *
      module_binder list * module_ast_inl
  | VernacDefineModule of bool option * lident * module_binder list *
      module_ast_inl Declaremods.module_signature * module_ast_inl list
  | VernacDeclareModuleType of lident *
      module_binder list * module_ast_inl list * module_ast_inl list
  | VernacInclude of module_ast_inl list

  (* Solving *)

  | VernacSolveExistential of int * constr_expr

  (* Auxiliary file and library management *)
  | VernacAddLoadPath of rec_flag * string * DirPath.t option
  | VernacRemoveLoadPath of string
  | VernacAddMLPath of rec_flag * string
  | VernacDeclareMLModule of string list
  | VernacChdir of string option

  (* State management *)
  | VernacWriteState of string
  | VernacRestoreState of string

  (* Resetting *)
  | VernacResetName of lident
  | VernacResetInitial
  | VernacBack of int
  | VernacBackTo of int

  (* Commands *)
  | VernacCreateHintDb of string * bool
  | VernacRemoveHints of string list * qualid list
  | VernacHints of string list * Hints.hints_expr
  | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
      onlyparsing_flag
  | VernacArguments of qualid or_by_notation *
      vernac_argument_status list (* Main arguments status list *) *
        (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
      int option (* Number of args to trigger reduction *) *
        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
          `DefaultImplicits ] list
  | VernacReserve of simple_binder list
  | VernacGeneralizable of (lident list) option
  | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
  | VernacSetStrategy of
      (Conv_oracle.level * qualid or_by_notation list) list
  | VernacSetOption of export_flag * Goptions.option_name * option_setting
  | VernacAddOption of Goptions.option_name * option_ref_value list
  | VernacRemoveOption of Goptions.option_name * option_ref_value list
  | VernacMemOption of Goptions.option_name * option_ref_value list
  | VernacPrintOption of Goptions.option_name
  | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
  | VernacGlobalCheck of constr_expr
  | VernacDeclareReduction of string * Genredexpr.raw_red_expr
  | VernacPrint of printable
  | VernacSearch of searchable * Goal_select.t option * search_restriction
  | VernacLocate of locatable
  | VernacRegister of qualid * register_kind
  | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option
  | VernacComments of comment list

  (* Proof management *)
  | VernacAbort of lident option
  | VernacAbortAll
  | VernacRestart
  | VernacUndo of int
  | VernacUndoTo of int
  | VernacFocus of int option
  | VernacUnfocus
  | VernacUnfocused
  | VernacBullet of Proof_bullet.t
  | VernacSubproof of Goal_select.t option
  | VernacEndSubproof
  | VernacShow of showable
  | VernacCheckGuard
  | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
  | VernacProofMode of string

  (* For extension *)
  | VernacExtend of extend_name * Genarg.raw_generic_argument list

type vernac_control =
  | VernacExpr of Attributes.vernac_flags * vernac_expr
  (* boolean is true when the `-time` batch-mode command line flag was set.
     the flag is used to print differently in `-time` vs `Time foo` *)
  | VernacTime of bool * vernac_control CAst.t
  | VernacRedirect of string * vernac_control CAst.t
  | VernacTimeout of int * vernac_control CAst.t
  | VernacFail of vernac_control CAst.t

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.