ortac-qcheck-stm 0.2.0 · OCaml Package

module Cfg = Config

module Ident = Gospel.Identifier.Ident

val ty_default : Ppxlib.core_type_desc

val pat_default : Ppxlib__.Import.pattern

val exp_default : Ppxlib__.Import.expression

val res_default : Ident.t

val list_append : Ppxlib.expression list -> Ppxlib.expression

val res : Ppxlib.longident Ppxlib.loc

val eeither : 
  string ->
  Ppxlib__.Import.expression ->
  Ppxlib__.Import.expression

val eleft : Ppxlib__.Import.expression -> Ppxlib__.Import.expression

val eright : Ppxlib__.Import.expression -> Ppxlib__.Import.expression

val eprotect : Ppxlib.expression -> Ppxlib__.Import.expression

val may_raise_exception : Ir.value -> bool

val subst_core_type : 
  (string * Ppxlib.core_type) list ->
  Ppxlib.core_type ->
  Ppxlib.core_type

val lazy_force : Gospel.Tterm.term -> Gospel.Tterm.term

val ocaml_of_term : 
  Cfg.t ->
  Gospel.Tterm.term ->
  Ppxlib.expression Reserr.reserr

val subst_term : 
  (Gospel.Tterm.Ident.t * 'a) list ->
  ?out_of_scope:Gospel.Tterm.Ident.t list ->
  gos_t:Gospel.Tterm.Ident.t ->
  ?old_lz:bool ->
  old_t:Gospel.Symbols.Ident.t option ->
  ?new_lz:bool ->
  new_t:Gospel.Symbols.Ident.t option ->
  Gospel.Tterm.term ->
  Gospel.Tterm.term Reserr.reserr

subst_term state ~gos_t ?old_lz ~old_t ?new_lz ~new_t trm will substitute occurrences of gos_t with new_t or old_t depending on whether the occurrence appears above or under the old operator, adding a Lazy.force if the corresponding xxx_lz is true (defaults to false). gos_t must always be in a position in which it is applied to one of its model fields. Calling subst_term with new_t and old_t as None will check that the term does not contain gos_t

val translate_checks : 
  Cfg.t ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  Ir.value ->
  Gospel.Symbols.Ident.t ->
  Ir.term ->
  Ppxlib.expression Reserr.reserr

val str_of_ident : Ident.t -> string

val longident_loc_of_ident : Ident.t -> Ppxlib.longident Ppxlib.loc

val mk_cmd_pattern : Ir.value -> Ppxlib__.Import.pattern

val munge_longident : 
  bool ->
  Astlib__.Ast_414.Parsetree.core_type ->
  Ppxlib.longident Ppxlib.loc ->
  string Reserr.reserr

val pat_of_core_type : 
  (string * Ppxlib.core_type) list ->
  Astlib__.Ast_414.Parsetree.core_type ->
  Ppxlib__.Import.pattern Reserr.reserr

val exp_of_core_type : 
  (string * Ppxlib.core_type) list ->
  Astlib__.Ast_414.Parsetree.core_type ->
  Ppxlib__.Import.expression Reserr.reserr

val exp_of_ident : Ident.t -> Ppxlib__.Import.expression

val arb_cmd_case : Ir.value -> Ppxlib__.Import.expression Reserr.reserr

val arb_cmd : Ir.t -> Ppxlib__.Import.structure_item Reserr.reserr

val run_case : 
  Cfg.t ->
  string ->
  Ir.value ->
  Ppxlib__.Import.case Reserr.reserr

val run : Cfg.t -> Ir.t -> Ppxlib__.Import.structure_item Reserr.reserr

val next_state_case : 
  (Gospel.Tterm.Ident.t * 'a) list ->
  Cfg.t ->
  Ident.t ->
  int ->
  Ir.value ->
  (int list * Ppxlib__.Import.case) Reserr.reserr

val next_state : 
  Cfg.t ->
  Ir.t ->
  ((Gospel.Identifier.Ident.t * int list) list * Ppxlib__.Import.structure_item)
    Reserr.reserr

val precond_case : 
  Cfg.t ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  Gospel.Symbols.Ident.t ->
  Ir.value ->
  Ppxlib__.Import.case Reserr.reserr

val precond : Cfg.t -> Ir.t -> Ppxlib__.Import.structure_item Reserr.reserr

val expected_returned_value : 
  (Ir.term ->
    Ppxlib__.Import.expression Ppxlib__Ast_builder_intf.without_location
      Reserr.reserr) ->
  Ir.value ->
  Ppxlib__.Import.expression option

val postcond_case : 
  Cfg.t ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  (Gospel.Tterm.Ident.t * Ir.term list) option ->
  int list ->
  Gospel.Symbols.Ident.t ->
  Gospel.Symbols.Ident.t ->
  Ir.value ->
  Ppxlib__.Import.case Reserr.reserr

val postcond : 
  Cfg.t ->
  (Gospel.Identifier.Ident.t * int list) list ->
  Ir.t ->
  Ppxlib__.Import.structure_item Reserr.reserr

val dummy_postcond : Ppxlib__.Import.structure_item

val cmd_constructor : Ir.value -> Ppxlib__.Import.constructor_declaration

val state_type : Ir.t -> Ppxlib__.Import.structure_item

val cmd_type : Ir.t -> Ppxlib__.Import.structure_item

val pp_cmd_case : Cfg.t -> Ir.value -> Ppxlib__.Import.case Reserr.reserr

val cmd_show : Cfg.t -> Ir.t -> Ppxlib__.Import.structure_item Reserr.reserr

val sut_type : Cfg.t -> Ppxlib__.Import.structure_item

val init_state : Cfg.t -> Ir.t -> Ppxlib__.Import.structure_item Reserr.reserr

val check_init_state : 
  Cfg.t ->
  Ir.t ->
  Ppxlib__.Import.structure_item Reserr.reserr

val ghost_function : 
  Cfg.t ->
  Gospel.Tast.function_ ->
  (Cfg.t * Ppxlib__.Import.structure_item) Reserr.reserr

val ghost_functions : 
  Cfg.t ->
  Gospel.Tast.function_ list ->
  (Cfg.t * Ppxlib.structure_item list) Reserr.reserr

val agree_prop : Ppxlib_ast.Ast.structure_item

val stm : 
  string option ->
  Cfg.t ->
  Ir.t ->
  Ppxlib_ast.Ast.structure_item list Reserr.reserr

package ortac-qcheck-stm