Module `Ortac_qcheck_stm.Stm_of_ir`Source

Sourcemodule Cfg = Config

Sourcemodule Ident = Gospel.Identifier.Ident

Sourceval is_a_function : Ppxlib.core_type -> bool

Sourceval ty_default_name : string

Sourceval ty_default : Ppxlib.core_type_desc

Sourceval pat_default : Ppxlib__.Import.pattern

Sourceval exp_default_name : string

Sourceval exp_default : Ppxlib__.Import.expression

Sourceval res_default : Ident.t

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

Sourceval res : Ppxlib.longident Ppxlib.loc

Sourceval fn_apply_name : Ident.t

Source

val eexpected_value : 
  string ->
  Ppxlib__.Import.expression ->
  Ppxlib_ast.Ast.expression

Sourceval evalue : Ppxlib__.Import.expression -> Ppxlib_ast.Ast.expression

Sourceval eprotected : Ppxlib__.Import.expression -> Ppxlib_ast.Ast.expression

Sourceval eexception : Ppxlib__.Import.expression -> Ppxlib_ast.Ast.expression

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

Sourceval may_raise_exception : Ir.value -> bool

Source

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

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

Source

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

Source

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

Source

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

Source

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

subst_term state ~gos_t ?old_lz ~old_t ?new_lz ~new_t ~fun_vars trm will substitute occurrences in gos_t with the associated values from 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 the empty list will check that the term does not contain gos_t

Source

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

Sourceval str_of_ident : Ident.t -> string

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

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

Source

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

Source

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

Sourceval prefix_identifier : prefix:string -> string -> Ppxlib__.Import.expression

Source

val exp_of_core_type : 
  ?use_small:bool ->
  (string * Ppxlib.core_type) list ->
  Ppxlib.core_type ->
  Ppxlib__.Import.expression Reserr.reserr

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

Source

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

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

Source

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

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

Source

val pop_states : 
  Ident.t ->
  Ir.value ->
  Ppxlib__.Import.value_binding list * (Ident.t * Ident.t) list

Source

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

Source

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

Source

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

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

Source

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

Source

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

Source

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

Sourceval dummy_postcond : Ppxlib__.Import.structure_item

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

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

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

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

Sourceval get_max_suts : Ir.t -> int

Sourceval sut_module : Cfg.t -> Ppxlib_ast.Ast.structure

Sourceval sut_defs : Ir.t -> Ppxlib_ast.Ast.structure_item list

Sourceval init_state : Cfg.t -> Ir.t -> Ppxlib_ast.Ast.structure_item Reserr.reserr

Source

val model_module : 
  Cfg.t ->
  Ir.t ->
  Ppxlib_ast.Ast.structure_item list Reserr.reserr

Sourceval state_defs : Ir.t -> Ppxlib_ast.Ast.structure_item list

Source

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

Source

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

Source

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

Source

val ghost_types : 
  Cfg.t ->
  (Gospel.Tast.rec_flag * Gospel.Tast.type_declaration list) list ->
  Ppxlib__.Import.structure_item list Reserr.reserr

Sourceval agree_prop : Ppxlib_ast.Ast.structure_item

Source

val prepend_include_in_module : 
  string ->
  Astlib.Longident.t Astlib.Location.loc ->
  Ppxlib__.Import.structure_item list ->
  Ppxlib__.Import.structure_item list

Sourceval qcheck : Cfg.t -> Ppxlib__.Import.structure_item list

Sourceval util : Cfg.t -> Ppxlib__.Import.structure_item list

Sourceval gen_tuple_ty : int list -> Ppxlib__.Import.structure_item

Sourceval gen_tuple_constr : int list -> Ppxlib__.Import.structure_item

Sourceval tuple_types : Ir.t -> Ppxlib__.Import.structure_item list

Sourceval integer_ty_ext : Ppxlib_ast.Ast.structure_item list

Source

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

Source

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

Sourceval sut_stm_ty_defs : Cfg.t -> Ir.t -> Ppxlib_ast.Ast.structure

Sourceval stm : Cfg.t -> Ir.t -> Ppxlib_ast.Ast.structure_item list Reserr.reserr

package ortac-qcheck-stm

Module Ortac_qcheck_stm.Stm_of_irSource

Module `Ortac_qcheck_stm.Stm_of_ir`Source