Quelle ssripats.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)         *)
(************************************************************************)

(* This file implements:
   - the [=>] tactical
   - the [:] pseudo-tactical for move, case, elim and abstract

   Putting these two features in the same file lets one hide much of the
   interaction between [tac E:] and [=>] ([E] has to be processed by [=>],
   not by [:]
*)

open Ssrast

(* Atomic operations for the IPat machine. Use this if you are "patching" an
* ipat written by the user, since patching it at he AST level and then
* compiling it may have tricky effects, eg adding a clear in front of a view
* also has the effect of disposing the view (the compilation phase takes care
* of this, by using the compiled ipats you can be more precise *)
type ssriop =
  | IOpId of Names.Id.t
  | IOpDrop
  | IOpTemporay
  | IOpInaccessible of string option
  | IOpInaccessibleAll
  | IOpAbstractVars of Names.Id.t list
  | IOpFastNondep

  | IOpInj of ssriops list

  | IOpDispatchBlock of id_block
  | IOpDispatchBranches of ssriops list

  | IOpCaseBlock of id_block
  | IOpCaseBranches of ssriops list

  | IOpRewrite of ssrocc * ssrdir
  | IOpView of ssrclear option * ssrview (* extra clears to be performed *)

  | IOpClear of ssrclear * ssrhyp option
  | IOpSimpl of ssrsimpl

  | IOpEqGen of unit Proofview.tactic (* generation of eqn *)

  | IOpNoop

and ssriops = ssriop list

val tclCompileIPats : ssripats -> ssriops

(* The => tactical *)
val tclIPAT : ssriops -> unit Proofview.tactic

(* As above but with the SSR exception: first case is dispatch *)
val tclIPATssr : ssripats -> unit Proofview.tactic

(* Wrappers to deal with : and eqn generation/naming:
     [tac E: gens => ipats]
   where [E] is injected into [ipats] (at the right place) and [gens] are
   generalized before calling [tac] *)
val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic

(* The implementation of abstract: is half here, for the [[: var ]]
* ipat, and in ssrfwd for the integration with [have] *)
val ssrabstract : ssrdgens -> unit Proofview.tactic

module Internal : sig
val examine_abstract :
  Environ.env -> Evd.evar_map -> EConstr.t -> Evd.evar_map * (EConstr.types * EConstr.t array)
val find_abstract_proof :
  Environ.env -> Evd.evar_map -> bool -> EConstr.constr -> Evar.t
end

quality88%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.