Module Pinterp_core.Log

module Log: sig .. end

type exec_mode =

`\|`	`Exec_giant_steps`
`\|`	`Exec_normal`

val pp_mode : Stdlib.Format.formatter -> exec_mode -> unit

type value_or_invalid =

`\|`	`Value of Pinterp_core.Value.value`
`\|`	`Invalid`

type log_entry_desc = private

`\|`	`Val_assumed of (Ident.ident * Pinterp_core.Value.value)`
`\|`	`Res_assumed of (Expr.rsymbol option * Pinterp_core.Value.value)`
`\|`	`Const_init of Ident.ident`
`\|`	`Exec_call of (Expr.rsymbol option * Pinterp_core.Value.value Term.Mvs.t * exec_mode)`
`\|`	`Exec_pure of (Term.lsymbol * exec_mode)`
`\|`	`Exec_any of (Expr.rsymbol option * Pinterp_core.Value.value Term.Mvs.t)`
`\|`	`Iter_loop of exec_mode`
`\|`	`Exec_main of (Expr.rsymbol * value_or_invalid Term.Mls.t * Pinterp_core.Value.value Term.Mvs.t * value_or_invalid Expr.Mrs.t)`
`\|`	`Exec_stucked of (string * Pinterp_core.Value.value Ident.Mid.t)`
`\|`	`Exec_failed of (string * Pinterp_core.Value.value Ident.Mid.t)`
`\|`	`Exec_ended`

type log_entry = private {

	`log_desc : log_entry_desc;`
	`log_loc : Loc.position option;`

}

type exec_log

type log_uc

val log_val : log_uc ->
       Ident.ident -> Pinterp_core.Value.value -> Loc.position option -> unit

val log_const : log_uc -> Ident.ident -> Loc.position option -> unit

val log_call : log_uc ->
       Expr.rsymbol option ->
       Pinterp_core.Value.value Term.Mvs.t ->
       exec_mode -> Loc.position option -> unit

val log_pure_call : log_uc ->
       Term.lsymbol -> exec_mode -> Loc.position option -> unit

val log_any_call : log_uc ->
       Expr.rsymbol option ->
       Pinterp_core.Value.value Term.Mvs.t -> Loc.position option -> unit

val log_iter_loop : log_uc ->
       exec_mode -> Loc.position option -> unit

val log_exec_main : log_uc ->
       Expr.rsymbol ->
       Pinterp_core.Value.value Stdlib.Lazy.t Term.Mls.t ->
       Pinterp_core.Value.value Term.Mvs.t ->
       Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t ->
       Loc.position option -> unit

val log_failed : log_uc ->
       string -> Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit

val log_stucked : log_uc ->
       string -> Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit

val log_exec_ended : log_uc -> Loc.position option -> unit

val empty_log_uc : unit -> log_uc

val empty_log : exec_log

val get_log : log_uc -> exec_log

Get the log

val flush_log : log_uc -> exec_log

Get the log and empty the log_uc

val sort_log_by_loc : exec_log ->
       log_entry list Wstdlib.Mint.t Wstdlib.Mstr.t

val json_log : exec_log -> Json_base.json

val print_log : ?verb_lvl:int -> json:bool -> exec_log Pp.pp

val get_exec_calls_and_loops : Env.env -> exec_log -> log_entry list

Used for counterexamples. Returns the list of function calls and loops that are executed in the log. The mlw builtins and functions from the stdlib are filtered out since they are not considered as suspects in the counterexamples.