package ortac-qcheck-stm

You can search for identifiers within the package.

in-package search v0.2.0

ortac-qcheck-stm.plugin
- Ortac_qcheck_stm
  - Config
  - Ir
  - Ir_of_gospel
  - Plugin
  - Reserr
  - Stm_of_ir

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Ident = Gospel.Identifier.Ident

type xpost =
  Gospel.Ttypes.xsymbol * Gospel.Tterm.pattern option * Gospel.Tterm.term

type new_state_formulae = {

model : Ident.t;
description : Gospel.Tterm.term;

}

type term = int * Gospel.Tterm.term

type next_state = {

formulae : (int * new_state_formulae) list;
modifies : (Ident.t * Ppxlib.Location.t) list;

}

type postcond = {

normal : term list;
exceptional : xpost list;
checks : Gospel.Tterm.term list;

}

type value = {

id : Ident.t;
ty : Ppxlib.core_type;
inst : (string * Ppxlib.core_type) list;
sut_var : Ident.t;
args : (Ppxlib.core_type * Ident.t option) list;
ret : Ident.t list;
next_state : next_state;
precond : Gospel.Tterm.term list;
postcond : postcond;

}

type init_state = {

arguments : (Gospel.Tast.lb_arg * Ppxlib.expression) list;
returned_sut : Ident.t;
descriptions : new_state_formulae list;

}

val get_return_type : value -> Ppxlib.core_type

val value : 
  Ident.t ->
  Ppxlib.core_type ->
  (string * Ppxlib.core_type) list ->
  Ident.t ->
  (Ppxlib.core_type * Ident.t option) list ->
  Ident.t list ->
  next_state ->
  Gospel.Tterm.term list ->
  postcond ->
  value

type t = {

state : (Ident.t * Ppxlib.core_type) list;
init_state : init_state;
ghost_functions : Gospel.Tast.function_ list;
values : value list;

}

val pp_state : 
  Stdlib.Format.formatter ->
  (Ident.t * Astlib.Ast_414.Parsetree.core_type) list ->
  unit

val pp_inst : 
  Stdlib.Format.formatter ->
  (string * Astlib.Ast_414.Parsetree.core_type) list ->
  unit

val pp_value : Stdlib.Format.formatter -> value -> unit

val pp : Stdlib.Format.formatter -> t -> unit