Module Ortac_qcheck_stm.IrSource

Sourcetype term = {
  1. term : Gospel.Tterm.term;
  2. text : string;
}
Sourceval term : prj_txt:('a -> string) -> prj_loc:('a -> Ppxlib.Location.t) -> 'a -> Gospel.Tterm.term -> term
Sourcetype new_state_formulae = {
  1. model : Ident.t;
  2. description : Gospel.Tterm.term;
}
Sourcetype indexed_term = int * term
Sourcetype next_state = {
  1. formulae : (int * new_state_formulae) list;
  2. modifies : (Ident.t * Ppxlib.Location.t) list;
}
Sourcetype postcond = {
  1. normal : indexed_term list;
  2. exceptional : xpost list;
  3. checks : term list;
}
Sourcetype value = {
  1. id : Ident.t;
  2. ty : Ppxlib.core_type;
  3. inst : (string * Ppxlib.core_type) list;
  4. sut_vars : Ident.t list;
  5. fun_vars : Ident.t list;
  6. args : (Ppxlib.core_type * Ident.t option) list;
  7. ret : Ident.t list;
  8. ret_values : term list list;
  9. next_states : (Ident.t * next_state) list;
  10. precond : Gospel.Tterm.term list;
  11. postcond : postcond;
}
Sourcetype init_state = {
  1. arguments : (Gospel.Tast.lb_arg * Ppxlib.expression) list;
  2. returned_sut : Ident.t;
  3. descriptions : new_state_formulae list;
}
Sourceval get_return_type : value -> Ppxlib.core_type
Sourceval value : Ident.t -> Ppxlib.core_type -> (string * Ppxlib.core_type) list -> Ident.t 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
Sourcetype t = {
  1. state : (Ident.t * Ppxlib.core_type) list;
  2. invariants : (Ident.t * term list) option;
  3. init_state : init_state;
  4. ghost_functions : Gospel.Tast.function_ list;
  5. ghost_types : (Gospel.Tast.rec_flag * Gospel.Tast.type_declaration list) list;
  6. values : value list;
}