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 term = {

term : Gospel.Tterm.term;
text : string;

}

val term : 
  prj_txt:('a -> string) ->
  prj_loc:('a -> Ppxlib.Location.t) ->
  'a ->
  Gospel.Tterm.term ->
  term

val term_val : Gospel.Tast.val_spec -> Gospel.Tterm.term -> term

val term_type : Gospel.Tast.type_spec -> Gospel.Tterm.term -> term

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

type new_state_formulae = {

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

}

type indexed_term = int * term

type next_state = {

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

}

type postcond = {

normal : indexed_term list;
exceptional : xpost list;
checks : term list;

}

type value = {

id : Ident.t;
ty : Ppxlib.core_type;
inst : (string * Ppxlib.core_type) list;
sut_vars : Ident.t list;
args : (Ppxlib.core_type * Ident.t option) list;
ret : Ident.t list;
ret_values : term list list;
next_states : (Ident.t * next_state) list;
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 list ->
  (Ppxlib.core_type * Ident.t option) list ->
  Ident.t list ->
  term list list ->
  (Ident.t * next_state) list ->
  Gospel.Tterm.term list ->
  postcond ->
  value

type t = {

state : (Ident.t * Ppxlib.core_type) list;
invariants : (Ident.t * term list) option;
init_state : init_state;
ghost_functions : Gospel.Tast.function_ list;
ghost_types : (Gospel.Tast.rec_flag * Gospel.Tast.type_declaration list) list;
values : value list;

}