ortac-qcheck-stm 0.2.0 (latest)

module Cfg = Config

module Ident = Gospel.Identifier.Ident

val ty_default : Ppxlib.core_type_desc

val pat_default : Astlib.Ast_500.Parsetree.pattern

val exp_default : Astlib.Ast_500.Parsetree.expression

val res_default : Ident.t

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

val res : Ppxlib.longident Ppxlib.loc

val eeither : 
  string ->
  Astlib.Ast_500.Parsetree.expression ->
  Astlib.Ast_500.Parsetree.expression

val eleft : 
  Astlib.Ast_500.Parsetree.expression ->
  Astlib.Ast_500.Parsetree.expression

val eright : 
  Astlib.Ast_500.Parsetree.expression ->
  Astlib.Ast_500.Parsetree.expression

val eprotect : Ppxlib.expression -> Astlib.Ast_500.Parsetree.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 -> Astlib.Ast_500.Parsetree.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 ->
  Astlib.Ast_500.Parsetree.pattern Reserr.reserr

val exp_of_core_type : 
  (string * Ppxlib.core_type) list ->
  Astlib.Ast_414.Parsetree.core_type ->
  Astlib.Ast_500.Parsetree.expression Reserr.reserr

val exp_of_ident : Ident.t -> Astlib.Ast_500.Parsetree.expression

val arb_cmd_case : 
  Ir.value ->
  Astlib.Ast_500.Parsetree.expression Reserr.reserr

val arb_cmd : Ir.t -> Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

val run_case : 
  Cfg.t ->
  string ->
  Ir.value ->
  Astlib.Ast_500.Parsetree.case Reserr.reserr

val run : 
  Cfg.t ->
  Ir.t ->
  Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

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

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

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

val precond : 
  Cfg.t ->
  Ir.t ->
  Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

val expected_returned_value : 
  (Ir.term -> Astlib.Ast_500.Parsetree.expression Reserr.reserr) ->
  Ir.value ->
  Astlib.Ast_500.Parsetree.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 ->
  Astlib.Ast_500.Parsetree.case Reserr.reserr

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

val dummy_postcond : Astlib.Ast_500.Parsetree.structure_item

val cmd_constructor : 
  Ir.value ->
  Astlib.Ast_500.Parsetree.constructor_declaration

val state_type : Ir.t -> Astlib.Ast_500.Parsetree.structure_item

val cmd_type : Ir.t -> Astlib.Ast_500.Parsetree.structure_item

val pp_cmd_case : 
  Cfg.t ->
  Ir.value ->
  Astlib.Ast_500.Parsetree.case Reserr.reserr

val cmd_show : 
  Cfg.t ->
  Ir.t ->
  Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

val sut_type : Cfg.t -> Astlib.Ast_500.Parsetree.structure_item

val init_state : 
  Cfg.t ->
  Ir.t ->
  Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

val check_init_state : 
  Cfg.t ->
  Ir.t ->
  Astlib.Ast_500.Parsetree.structure_item Reserr.reserr

val ghost_function : 
  Cfg.t ->
  Gospel.Tast.function_ ->
  (Cfg.t * Astlib.Ast_500.Parsetree.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