sig
type exec_mode = Exec_giant_steps | Exec_normal
val pp_mode : Stdlib.Format.formatter -> Pinterp_core.Log.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 *
Pinterp_core.Log.exec_mode)
| Exec_pure of (Term.lsymbol * Pinterp_core.Log.exec_mode)
| Exec_any of (Expr.rsymbol option * Pinterp_core.Value.value Term.Mvs.t)
| Iter_loop of Pinterp_core.Log.exec_mode
| Exec_main of
(Expr.rsymbol * Pinterp_core.Log.value_or_invalid Term.Mls.t *
Pinterp_core.Value.value Term.Mvs.t *
Pinterp_core.Log.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 : Pinterp_core.Log.log_entry_desc;
log_loc : Loc.position option;
}
type exec_log = Pinterp_core.Log.log_entry list
type log_uc
val log_val :
Pinterp_core.Log.log_uc ->
Ident.ident -> Pinterp_core.Value.value -> Loc.position option -> unit
val log_const :
Pinterp_core.Log.log_uc -> Ident.ident -> Loc.position option -> unit
val log_call :
Pinterp_core.Log.log_uc ->
Expr.rsymbol option ->
Pinterp_core.Value.value Term.Mvs.t ->
Pinterp_core.Log.exec_mode -> Loc.position option -> unit
val log_pure_call :
Pinterp_core.Log.log_uc ->
Term.lsymbol -> Pinterp_core.Log.exec_mode -> Loc.position option -> unit
val log_any_call :
Pinterp_core.Log.log_uc ->
Expr.rsymbol option ->
Pinterp_core.Value.value Term.Mvs.t -> Loc.position option -> unit
val log_iter_loop :
Pinterp_core.Log.log_uc ->
Pinterp_core.Log.exec_mode -> Loc.position option -> unit
val log_exec_main :
Pinterp_core.Log.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 :
Pinterp_core.Log.log_uc ->
string ->
Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit
val log_stucked :
Pinterp_core.Log.log_uc ->
string ->
Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit
val log_exec_ended : Pinterp_core.Log.log_uc -> Loc.position option -> unit
val empty_log_uc : unit -> Pinterp_core.Log.log_uc
val empty_log : Pinterp_core.Log.exec_log
val get_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
val flush_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
val sort_log_by_loc :
Pinterp_core.Log.exec_log ->
Pinterp_core.Log.log_entry list Wstdlib.Mint.t Wstdlib.Mstr.t
val json_log : Pinterp_core.Log.exec_log -> Json_base.json
val print_log : ?verb_lvl:int -> Pinterp_core.Log.exec_log Pp.pp
val get_exec_calls_and_loops :
Env.env -> Pinterp_core.Log.exec_log -> Pinterp_core.Log.log_entry list
end