ortac-qcheck-stm 0.4.0 (latest)

module Cfg = Config

module Ident = Gospel.Identifier.Ident

val constant_test : Gospel.Tast.val_description -> unit Reserr.reserr

val no_functional_arg_or_big_tuple : 
  Gospel.Tast.val_description ->
  unit Reserr.reserr

val is_a_function : Ppxlib.core_type -> bool

val unify : 
  [< `Type of Gospel.Tast.type_declaration | `Value of string ] ->
  Astlib.Ast_414.Parsetree.core_type ->
  Ppxlib.core_type ->
  (string * Ppxlib.core_type) list Reserr.reserr

val ty_var_substitution : 
  Cfg.t ->
  Gospel.Tast.val_description ->
  (string * Ppxlib.core_type) list Reserr.reserr

val split_args : 
  Cfg.t ->
  Gospel.Tast.val_description ->
  Gospel.Tast.lb_arg list ->
  (Gospel.Symbols.Ident.t list
   * (Ppxlib.core_type * Gospel.Symbols.Ident.t option) list)
    Reserr.reserr

val get_state_description_with_index : 
  (Gospel.Symbols.vsymbol -> bool) ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  Gospel.Tast.val_spec ->
  (int * Ir.new_state_formulae) list

val next_states : 
  Gospel.Tterm.Ident.t list ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  Gospel.Tast.val_spec ->
  (Gospel.Tterm.Ident.t * Ir.next_state) list

val ret_next_state : 
  Cfg.t ->
  (Gospel.Symbols.Ident.t * 'a) list ->
  Gospel.Tast.val_description ->
  (Gospel.Symbols.Ident.t * Ir.next_state) option Reserr.reserr

val returned_value_description : 
  Gospel.Tast.val_spec ->
  Gospel.Symbols.Ident.t ->
  Ir.term list

val postcond : Gospel.Tast.val_spec -> Ir.postcond

val val_desc : 
  Cfg.t ->
  (Gospel.Symbols.Ident.t * 'a) list ->
  Gospel.Tast.val_description ->
  Ir.value Reserr.reserr

val sig_item : 
  Cfg.t ->
  (Gospel.Symbols.Ident.t * 'a) list ->
  Gospel.Tast.signature_item ->
  Ir.value Reserr.reserr option

val state_and_invariants : 
  Cfg.t ->
  Gospel.Tast.signature_item list ->
  ((Gospel.Symbols.Ident.t * Ppxlib.core_type) list
   * (Gospel.Symbols.Ident.t * Ir.term list) option)
    Reserr.reserr

val init_state : 
  Cfg.t ->
  (Gospel.Symbols.Ident.t * 'a) list ->
  Gospel.Tast.signature_item list ->
  Ir.init_state Reserr.reserr

val signature : 
  Cfg.t ->
  (Gospel.Symbols.Ident.t * 'a) list ->
  Gospel.Tast.signature_item list ->
  Ir.value list Reserr.reserr

val ghost_functions : 
  Gospel.Tast.signature_item list ->
  Gospel.Tast.function_ list

val ghost_types : 
  Gospel.Tast.signature_item list ->
  (Gospel.Tast.rec_flag * Gospel.Tast.type_declaration list) list

val run : Gospel.Tast.signature_item list -> Cfg.t -> Ir.t Reserr.reserr

package ortac-qcheck-stm