package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.11.0.0.11.0.tbz
sha256=59d38d716fda7cb1d89e2e1519c93d22deaf14da4f0f2feccd45886317f3424c
sha512=21b0ccaf75b497e13662c3fa2c618413dfccf6abfaabbab1d27926836447a0fcdc0e2a92929401359321018a4a867124caad27e9db52c4f3e5040aff698999ef

doc/serlib_ssr/Serlib_ssr/Ser_ssrast/index.html

Module Serlib_ssr.Ser_ssrast

module Loc = Serlib.Ser_loc
module Names = Serlib.Ser_names
module Locus = Serlib.Ser_locus
module Constrexpr = Serlib.Ser_constrexpr
module Genintern = Serlib.Ser_genintern
module Geninterp = Serlib.Ser_geninterp
module Ssrmatching_plugin : sig ... end
module Ltac_plugin : sig ... end
module Proofview : sig ... end
type ssrhyp = Ssrast.ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
val ssrhyp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp
val sexp_of_ssrhyp : ssrhyp -> Ppx_sexp_conv_lib.Sexp.t
type ssrhyp_or_id = Ssrast.ssrhyp_or_id =
  1. | Hyp of ssrhyp
  2. | Id of ssrhyp
val ssrhyp_or_id_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp_or_id
val sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Ppx_sexp_conv_lib.Sexp.t
type ssrhyps = ssrhyp list
val ssrhyps_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyps
val sexp_of_ssrhyps : ssrhyps -> Ppx_sexp_conv_lib.Sexp.t
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
  1. | L2R
  2. | R2L
val ssrdir_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdir
val sexp_of_ssrdir : ssrdir -> Ppx_sexp_conv_lib.Sexp.t
type ssrsimpl = Ssrast.ssrsimpl =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
val ssrsimpl_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrsimpl
val sexp_of_ssrsimpl : ssrsimpl -> Ppx_sexp_conv_lib.Sexp.t
type ssrmmod = Ssrast.ssrmmod =
  1. | May
  2. | Must
  3. | Once
val ssrmmod_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmmod
val sexp_of_ssrmmod : ssrmmod -> Ppx_sexp_conv_lib.Sexp.t
type ssrmult = int * ssrmmod
val ssrmult_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmult
val sexp_of_ssrmult : ssrmult -> Ppx_sexp_conv_lib.Sexp.t
type ssrocc = (bool * int list) option
val ssrocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrocc
val sexp_of_ssrocc : ssrocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrindex = int Locus.or_var
val ssrindex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrindex
val sexp_of_ssrindex : ssrindex -> Ppx_sexp_conv_lib.Sexp.t
type ssrclear = ssrhyps
val ssrclear_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclear
val sexp_of_ssrclear : ssrclear -> Ppx_sexp_conv_lib.Sexp.t
type ssrdocc = ssrclear option * ssrocc
val ssrdocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdocc
val sexp_of_ssrdocc : ssrdocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrtermkind = char
val ssrtermkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrtermkind
val sexp_of_ssrtermkind : ssrtermkind -> Ppx_sexp_conv_lib.Sexp.t
val ssrterm_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrterm
val sexp_of_ssrterm : ssrterm -> Ppx_sexp_conv_lib.Sexp.t
type ast_closure_term = Ssrast.ast_closure_term = {
  1. body : Constrexpr.constr_expr;
  2. glob_env : Genintern.glob_sign option;
  3. interp_env : Geninterp.interp_sign option;
  4. annotation : [ `At | `DoubleParens | `Parens | `None ];
}
val ast_closure_term_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_closure_term
val sexp_of_ast_closure_term : ast_closure_term -> Ppx_sexp_conv_lib.Sexp.t
type ssrview = ast_closure_term list
val ssrview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrview
val sexp_of_ssrview : ssrview -> Ppx_sexp_conv_lib.Sexp.t
type anon_kind = Ssrast.anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
val anon_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> anon_kind
val sexp_of_anon_kind : anon_kind -> Ppx_sexp_conv_lib.Sexp.t
type id_block = Ssrast.id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
val id_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> id_block
val sexp_of_id_block : id_block -> Ppx_sexp_conv_lib.Sexp.t
type ssripat = Ssrast.ssripat =
  1. | IPatNoop
  2. | IPatId of Names.Id.t
  3. | IPatAnon of anon_kind
  4. | IPatDispatch of ssripatss_or_block
  5. | IPatCase of ssripatss_or_block
  6. | IPatInj of ssripatss
  7. | IPatRewrite of ssrocc * ssrdir
  8. | IPatView of ssrview
  9. | IPatClear of ssrclear
  10. | IPatSimpl of ssrsimpl
  11. | IPatAbstractVars of Names.Id.t list
  12. | IPatFastNondep
and ssripats = ssripat list
and ssripatss = ssripats list
and ssripatss_or_block = Ssrast.ssripatss_or_block =
  1. | Block of id_block
  2. | Regular of ssripats list
val ssripat_of_sexp : Sexplib0__.Sexp.t -> ssripat
val ssripats_of_sexp : Sexplib0__.Sexp.t -> ssripats
val ssripatss_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss
val ssripatss_or_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss_or_block
val sexp_of_ssripat : ssripat -> Sexplib0__.Sexp.t
val sexp_of_ssripats : ssripats -> Sexplib0__.Sexp.t
val sexp_of_ssripatss : ssripatss -> Ppx_sexp_conv_lib.Sexp.t
val sexp_of_ssripatss_or_block : ssripatss_or_block -> Ppx_sexp_conv_lib.Sexp.t
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
val ssrhpats_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats
val sexp_of_ssrhpats : ssrhpats -> Ppx_sexp_conv_lib.Sexp.t
type ssrhpats_wtransp = bool * ssrhpats
val ssrhpats_wtransp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats_wtransp
val sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_sexp_conv_lib.Sexp.t
val ssrintrosarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrintrosarg
val sexp_of_ssrintrosarg : ssrintrosarg -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdid = Names.Id.t
val ssrfwdid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdid
val sexp_of_ssrfwdid : ssrfwdid -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbind = 'term Ssrast.ssrbind =
  1. | Bvar of Names.Name.t
  2. | Bdecl of Names.Name.t list * 'term
  3. | Bdef of Names.Name.t * 'term option * 'term
  4. | Bstruct of Names.Name.t
  5. | Bcast of 'term
val ssrbind_of_sexp : 'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) -> Ppx_sexp_conv_lib.Sexp.t -> 'term ssrbind
val sexp_of_ssrbind : 'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) -> 'term ssrbind -> Ppx_sexp_conv_lib.Sexp.t
type ssrbindfmt = Ssrast.ssrbindfmt =
  1. | BFvar
  2. | BFdecl of int
  3. | BFcast
  4. | BFdef
  5. | BFrec of bool * bool
val ssrbindfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrbindfmt
val sexp_of_ssrbindfmt : ssrbindfmt -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbindval = 'term ssrbind list * 'term
val ssrbindval_of_sexp : 'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) -> Ppx_sexp_conv_lib.Sexp.t -> 'term ssrbindval
val sexp_of_ssrbindval : 'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) -> 'term ssrbindval -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdkind = Ssrast.ssrfwdkind =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose
val ssrfwdkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdkind
val sexp_of_ssrfwdkind : ssrfwdkind -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
val ssrfwdfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdfmt
val sexp_of_ssrfwdfmt : ssrfwdfmt -> Ppx_sexp_conv_lib.Sexp.t
type ssrclseq = Ssrast.ssrclseq =
  1. | InGoal
  2. | InHyps
  3. | InHypsGoal
  4. | InHypsSeqGoal
  5. | InSeqGoal
  6. | InHypsSeq
  7. | InAll
  8. | InAllHyps
val ssrclseq_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclseq
val sexp_of_ssrclseq : ssrclseq -> Ppx_sexp_conv_lib.Sexp.t
type 'tac ssrhint = bool * 'tac option list
val ssrhint_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac ssrhint
val sexp_of_ssrhint : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac ssrhint -> Ppx_sexp_conv_lib.Sexp.t
type 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
val fwdbinders_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac fwdbinders
val sexp_of_fwdbinders : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac fwdbinders -> Ppx_sexp_conv_lib.Sexp.t
type 'tac ffwbinders = ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
val ffwbinders_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac ffwbinders
val sexp_of_ffwbinders : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac ffwbinders -> Ppx_sexp_conv_lib.Sexp.t
type clause = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
val clause_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clause
val sexp_of_clause : clause -> Ppx_sexp_conv_lib.Sexp.t
type clauses = clause list * ssrclseq
val clauses_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clauses
val sexp_of_clauses : clauses -> Ppx_sexp_conv_lib.Sexp.t
type wgen = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
val wgen_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> wgen
val sexp_of_wgen : wgen -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
val ssrdoarg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrdoarg
val sexp_of_ssrdoarg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrdoarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
val ssrseqarg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrseqarg
val sexp_of_ssrseqarg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrseqarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssragens = (ssrdocc * 'a) list list * ssrclear
val ssragens_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssragens
val sexp_of_ssragens : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssragens -> Ppx_sexp_conv_lib.Sexp.t
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
val ssrapplyarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrapplyarg
val sexp_of_ssrapplyarg : ssrapplyarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrcasearg = ssripat option * ('a * ssripats)
val ssrcasearg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrcasearg
val sexp_of_ssrcasearg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrcasearg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrmovearg = ssrview * 'a ssrcasearg
val ssrmovearg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrmovearg
val sexp_of_ssrmovearg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrmovearg -> Ppx_sexp_conv_lib.Sexp.t