ortac-qcheck-stm 0.1.0 · OCaml Package

module Cfg = Config

module Ident = Gospel.Identifier.Ident

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

val no_functional_arg_or_returned_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
   * (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_state : 
  Gospel.Symbols.Ident.t ->
  (Gospel.Tterm.Ident.t * 'a) list ->
  Gospel.Tast.val_spec ->
  Ir.next_state Reserr.reserr

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

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

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

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

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

val signature : 
  Cfg.t ->
  string ->
  (Gospel.Tterm.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 run : Gospel.Tast.signature_item list -> Cfg.t -> Ir.t Reserr.reserr

package ortac-qcheck-stm