package ortac-qcheck-stm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type init_state_error =
  1. | Not_a_function_call of string
  2. | No_specification of string
  3. | No_appropriate_specifications of string * string list
  4. | No_translatable_specification of string
  5. | Not_returning_sut of string
  6. | Qualified_name of string
  7. | Mismatch_number_of_arguments of string
type W.kind +=
  1. | Constant_value of string
  2. | Returning_sut of string
  3. | No_sut_argument of string
  4. | Multiple_sut_arguments of string
  5. | No_sut_type of string
  6. | No_init_function of string
  7. | Syntax_error_in_type of string
  8. | Syntax_error_in_init_sut of string
  9. | Sut_type_not_supported of string
  10. | Type_parameter_not_instantiated of string
  11. | Type_not_supported_for_sut_parameter of string
  12. | Incompatible_type of string * string
  13. | Sut_type_not_specified of string
  14. | No_models of string
  15. | No_spec of string
  16. | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel | `OutOfScope ]
  17. | Ignored_modifies
  18. | Ensures_not_found_for_next_state of string * string
  19. | Type_not_supported of string
  20. | Impossible_init_state_generation of init_state_error
  21. | Functional_argument of string
  22. | Returned_tuple of string
  23. | Ghost_values of string * [ `Arg | `Ret ]
  24. | Incompatible_sut of string
  25. | Incomplete_ret_val_computation of string
type 'a reserr
val ok : 'a -> 'a reserr
val error : W.t -> 'a reserr
val warns : W.t list -> unit reserr
val warn : W.t -> unit reserr
val let* : 'a reserr -> ('a -> 'b reserr) -> 'b reserr
val (>>=) : 'a reserr -> ('a -> 'b reserr) -> 'b reserr
val and* : 'a reserr -> 'b reserr -> ('a * 'b) reserr
val sequence : 'a reserr list -> 'a list reserr

sequence rs returns ok of the list of 'a iff there is no error in rs

val promote : 'a reserr list -> 'a list reserr

promote rs filters rs and returns ok of the list of 'a iff there is no errors of level Error in rs and store the errors of level Warning in the warnings list

val promote_opt : 'a reserr -> 'a option reserr

promote_opt r is promote for a unique value

val of_option : default:W.t -> 'a option -> 'a reserr
val to_option : 'a reserr -> 'a option
val map : ('a -> 'b reserr) -> 'a list -> 'b list reserr
val concat_map : ('a -> 'b list reserr) -> 'a list -> 'b list reserr
val fmap : ('a -> 'b) -> 'a reserr -> 'b reserr
val (<$>) : ('a -> 'b) -> 'a reserr -> 'b reserr
val app : ('a -> 'b) reserr -> 'a reserr -> 'b reserr
val (<*>) : ('a -> 'b) reserr -> 'a reserr -> 'b reserr
val pp : bool -> 'a Fmt.t -> 'a reserr Fmt.t