Quelle ssrcommon.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 is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)

open Names
open Environ
open Evd
open Constrexpr
open Ssrast

open Ltac_plugin

open Ssrmatching_plugin

val allocc : ssrocc

(******************************** hyps ************************************)

val hyp_id : ssrhyp -> Id.t
val hyps_ids : ssrhyps -> Id.t list
val check_hyp_exists : ('a, 'b, 'r) Context.Named.pt -> ssrhyp -> unit
val test_hyp_exists : ('a, 'b, 'r) Context.Named.pt -> ssrhyp -> bool
val check_hyps_uniq : Id.t list -> ssrhyps -> unit
val not_section_id : Id.t -> bool
val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a
val hoik : (ssrhyp -> 'a) -> ssrhyp_or_id -> 'a
val hoi_id : ssrhyp_or_id -> Id.t

(******************************* hints ***********************************)

val mk_hint : 'a -> 'a ssrhint
val mk_orhint : 'a -> bool * 'a
val nullhint : bool * 'a list
val nohint : 'a ssrhint

(******************************** misc ************************************)

val errorstrm : Pp.t -> 'a
val anomaly : string -> 'a

val array_app_tl : 'a array -> 'a list -> 'a list
val array_list_of_tl : 'a array -> 'a list
val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b

val option_assert_get : 'a option -> Pp.t -> 'a

(************************ ssr tactic arguments ******************************)

(*********************** Misc helpers *****************************)
val mkRHole : Glob_term.glob_constr
val mkRHoles : int -> Glob_term.glob_constr list
val isRHoles : Glob_term.glob_constr list -> bool
val mkRApp : Glob_term.glob_constr -> Glob_term.glob_constr list -> Glob_term.glob_constr
val mkRVar : Id.t -> Glob_term.glob_constr
val mkRltacVar : Id.t -> Glob_term.glob_constr
val mkRCast : Glob_term.glob_constr ->  Glob_term.glob_constr ->  Glob_term.glob_constr
val mkRType : Glob_term.glob_constr
val mkRProp : Glob_term.glob_constr
val mkRArrow : Glob_term.glob_constr ->  Glob_term.glob_constr ->  Glob_term.glob_constr
val mkRConstruct : Names.constructor -> Glob_term.glob_constr
val mkRInd : Names.inductive -> Glob_term.glob_constr
val mkRLambda : Name.t -> Glob_term.glob_constr ->  Glob_term.glob_constr ->  Glob_term.glob_constr
val mkRnat : int -> Glob_term.glob_constr

val mkCHole : Loc.t option -> constr_expr
val mkCHoles : ?loc:Loc.t -> int -> constr_expr list
val mkCVar : ?loc:Loc.t -> Id.t -> constr_expr
val mkCCast : ?loc:Loc.t -> constr_expr ->  constr_expr ->  constr_expr
val mkCType : Loc.t option -> constr_expr
val mkCProp : Loc.t option -> constr_expr
val mkCArrow : ?loc:Loc.t -> constr_expr ->  constr_expr ->  constr_expr
val mkCLambda : ?loc:Loc.t -> Name.t -> constr_expr ->  constr_expr ->  constr_expr

val isCHoles : constr_expr list -> bool
val isCxHoles : (constr_expr * 'a option) list -> bool

val intern_term :
  Tacinterp.interp_sign -> env ->
    ssrterm -> Glob_term.glob_constr

val interp_term :
  Environ.env -> Evd.evar_map ->
  Tacinterp.interp_sign ->
    ssrterm -> evar_map * EConstr.t

val interp_hyp : ist -> env -> evar_map -> ssrhyp -> ssrhyp
val interp_hyps : ist -> env -> evar_map -> ssrhyps -> ssrhyps

val interp_refine :
  Environ.env -> Evd.evar_map -> Tacinterp.interp_sign -> concl:EConstr.constr ->
    Glob_term.glob_constr -> evar_map * EConstr.constr

val interp_open_constr :
  Environ.env -> Evd.evar_map ->
  Tacinterp.interp_sign ->
    Genintern.glob_constr_and_expr -> evar_map * EConstr.t

val splay_open_constr :
           Environ.env ->
           evar_map * EConstr.t ->
           (Names.Name.t EConstr.binder_annot * EConstr.t) list * EConstr.t
val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool

val mk_term : ssrtermkind -> constr_expr -> ssrterm
val mk_lterm : constr_expr -> ssrterm

val mk_ast_closure_term :
  [ `None | `Parens | `DoubleParens | `At ] ->
  Constrexpr.constr_expr -> ast_closure_term
val interp_ast_closure_term : Geninterp.interp_sign -> env -> evar_map -> ast_closure_term -> ast_closure_term
val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
val ssrterm_of_ast_closure_term : ast_closure_term -> ssrterm

val ssrdgens_of_parsed_dgens :
  (ssrdocc * Ssrmatching.cpattern) list list * ssrclear -> ssrdgens

val is_internal_name : string -> bool
val add_internal_name : (string -> bool) -> unit
val mk_internal_id : string -> Id.t
val mk_tagged_id : string -> int -> Id.t
val mk_evar_name : int -> Name.t
val ssr_anon_hyp : string
val type_id : Environ.env -> Evd.evar_map -> EConstr.types -> Id.t

val abs_evars :
           Environ.env -> Evd.evar_map -> ?rigid:Evar.t list ->
           evar_map * EConstr.t ->
           EConstr.t * Evar.t list *
           UState.t
val abs_cterm :
           Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t

val constr_name : evar_map -> EConstr.t -> Name.t

val mkSsrRef : string -> GlobRef.t
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
val mkSsrConst : Environ.env -> Evd.evar_map -> string -> Evd.evar_map * EConstr.t

val is_discharged_id : Id.t -> bool
val mk_discharged_id : Id.t -> Id.t
val is_tagged : string -> string -> bool
val has_discharged_tag : string -> bool
val ssrqid : string -> Libnames.qualid
val mk_anon_id : string -> Id.t list -> Id.t
val nbargs_open_constr : Environ.env -> Evd.evar_map * EConstr.t -> int
val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int

val ssrevaltac :
  Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic

val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic

val red_safe :
  Reductionops.reduction_function ->
  env -> evar_map -> EConstr.t -> EConstr.t

val red_product_skip_id :
  env -> evar_map -> EConstr.t -> EConstr.t

val ssrautoprop_tac :
           unit Proofview.tactic ref

val mkProt :
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  EConstr.t ->
  Evd.evar_map * EConstr.t

val mkEtaApp : EConstr.t -> int -> int -> EConstr.t

val mkRefl :
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  EConstr.t ->
  Evd.evar_map * EConstr.t

val discharge_hyp :
           Id.t * (Id.t * string) -> unit Proofview.tactic

val view_error : string -> ssrterm -> 'a Proofview.tactic

val top_id : Id.t

val abs_ssrterm :
           ?resolve_typeclasses:bool ->
           ist ->
           Environ.env -> Evd.evar_map ->
           ssrterm ->
           Evd.evar_map * EConstr.t * int

val pf_interp_ty :
           ?resolve_typeclasses:bool ->
           Environ.env ->
           Evd.evar_map ->
           Tacinterp.interp_sign ->
           Ssrast.ssrtermkind *
           (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
           Evd.evar_map * int * EConstr.t * EConstr.t

val ssr_n_tac : string -> int -> unit Proofview.tactic
val donetac : int -> unit Proofview.tactic

exception NotEnoughProducts
val saturate :
           ?beta:bool ->
           ?bi_types:bool ->
           env ->
           evar_map ->
           EConstr.constr ->
           ?ty:EConstr.types ->
           int ->
           EConstr.constr * EConstr.types * (int * EConstr.constr * EConstr.types) list * evar_map
val refine_with :
           ?first_goes_last:bool ->
           ?beta:bool ->
           ?with_evars:bool ->
           evar_map * EConstr.t -> unit Proofview.tactic

val resolve_typeclasses :
  Environ.env -> Evd.evar_map ->
  where:EConstr.t ->
  fail:bool -> Evd.evar_map

(*********************** Wrapped Rocq tactics *****************************)

val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> unit Proofview.tactic

type name_hint = (int * EConstr.types array) option ref

val gentac :
   Ssrast.ssrdocc * Ssrmatching.cpattern -> unit Proofview.tactic

val genstac :
  ((Ssrast.ssrhyp list option * Ssrmatching.occ) *
     Ssrmatching.cpattern)
    list * Ssrast.ssrhyp list ->
  unit Proofview.tactic

val interp_gen :
  Environ.env ->
  Evd.evar_map ->
  concl:EConstr.t ->
  bool ->
  (Ssrast.ssrhyp list option * Ssrmatching.occ) *
    Ssrmatching.cpattern ->
  Evd.evar_map * (EConstr.t * EConstr.t * Ssrast.ssrhyp list)

(** Basic tactics *)

val introid : ?orig:Name.t ref -> Id.t -> unit Proofview.tactic
val intro_anon : unit Proofview.tactic

val interp_clr :
  evar_map -> ssrhyps option * (ssrtermkind * EConstr.t) -> ssrhyps

val genclrtac :
  EConstr.constr ->
  EConstr.constr list -> Ssrast.ssrhyp list -> unit Proofview.tactic
val cleartac : ssrhyps -> unit Proofview.tactic

val tclMULT : int * ssrmmod -> unit Proofview.tactic -> unit Proofview.tactic

val unprotecttac : unit Proofview.tactic
val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool

val abs_wgen :
  Environ.env ->
  Evd.evar_map ->
  bool ->
  (Id.t -> Id.t) ->
  'a *
    ((Ssrast.ssrhyp_or_id * string) *
       Ssrmatching.cpattern option)
      option ->
  EConstr.t list * EConstr.t ->
  Evd.evar_map * EConstr.t list * EConstr.t

val clr_of_wgen :
  ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option ->
  unit Proofview.tactic list -> unit Proofview.tactic list

val unfold : EConstr.t list -> unit Proofview.tactic

(* New code ****************************************************************)

val tclINTERP_AST_CLOSURE_TERM_AS_CONSTR :
  ast_closure_term -> EConstr.t list Proofview.tactic

val tacTYPEOF : EConstr.t -> EConstr.types Proofview.tactic

val tclINTRO_ID : Id.t -> unit Proofview.tactic
val tclINTRO_ANON : ?seed:string -> unit -> unit Proofview.tactic

(* Lower level API, calls conclusion with the name taken from the prod *)
type intro_id =
  | Anon
  | Id of Id.t
  | Seed of string

val tclINTRO :
  id:intro_id ->
  conclusion:(orig_name:Name.t -> new_name:Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclRENAME_HD_PROD : Name.t -> unit Proofview.tactic

(* calls the tactic only if there are more than 0 goals *)
val tcl0G : default:'a -> 'a Proofview.tactic -> 'a Proofview.tactic

(* like tclFIRST but with 'a tactic *)
val tclFIRSTa : 'a Proofview.tactic list -> 'a Proofview.tactic
val tclFIRSTi : (int -> 'a Proofview.tactic) -> int -> 'a Proofview.tactic

val tacCONSTR_NAME : ?name:Name.t -> EConstr.t -> Name.t Proofview.tactic

(* [tacMKPROD t name ctx] (where ctx is a term possibly containing an unbound
* Rel 1) builds [forall name : ty_t, ctx] *)
val tacMKPROD :
  EConstr.t -> ?name:Name.t -> EConstr.types -> EConstr.types Proofview.tactic

val tacINTERP_CPATTERN : Ssrmatching.cpattern -> Ssrmatching.pattern Proofview.tactic
val tacUNIFY : EConstr.t -> EConstr.t -> unit Proofview.tactic

(* if [(t : eq _ _ _)] then we can inject it *)
val tacIS_INJECTION_CASE : ?ty:EConstr.types -> EConstr.t -> bool Proofview.tactic

(** 1 shot, hands-on the top of the stack, eg for [=> ->] *)
val tclWITHTOP : (EConstr.t -> unit Proofview.tactic) -> unit Proofview.tactic

val tacMK_SSR_CONST : string -> EConstr.t Proofview.tactic

module type StateType = sig
  type state
  val init : state
  val name : string
end

module MakeState(S : StateType) : sig

  val tclGET : (S.state -> unit Proofview.tactic) -> unit Proofview.tactic
  val tclGET1 : (S.state -> 'a Proofview.tactic) -> 'a Proofview.tactic
  val tclSET : S.state -> unit Proofview.tactic
  val tacUPDATE : (S.state -> S.state Proofview.tactic) -> unit Proofview.tactic

  val get : Proofview.Goal.t -> S.state

end

val is_ind_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_construct_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_const_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool

quality99%

¤ Dauer der Verarbeitung: 0.7 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.