Module Pinterp

module Pinterp: sig .. end

WhyML Program Interpreter

Interpreter configuration

val init_real : int * int * int -> unit

Give a precision on real computation.

Execution context

type ctx

The execution context

val mk_empty_env : Env.env -> Pmodule.pmodule -> Pinterp_core.env

Pinterp_core.env repeated here for convenience.

val mk_rac : ?ignore_incomplete:bool -> Pinterp_core.check_term -> Pinterp_core.rac

Pinterp_core.mk_rac repeated here for convenience.

val mk_ctx : Pinterp_core.env ->
       ?timelimit:float ->
       ?steplimit:int ->
       ?giant_steps:bool ->
       ?do_rac:bool ->
       ?rac:Pinterp_core.rac ->
       ?oracle:Pinterp_core.oracle ->
       ?compute_term:(Pinterp_core.env -> Term.term -> Term.term) ->
       unit -> ctx

Create an execution context.

timelimit : timeout in seconds for execution (disabled by default)

steplimit : steplimit for execution (disabled by default)

giant_steps : execute function calls and loops with giant steps (false by default)

do_rac : enable runtime-assertion checking (RAC) (false by default)

rac : the RAC engine (Pinterp_core.rac_dummy by default)

oracle : for values when they are needed (program parameters and giant steps

compute_term : callback to compute terms in pure expressions

val get_env : ctx -> Pinterp_core.env

Return the environment of an execution context.

val get_do_rac : ctx -> bool

Return true if RAC is enabled in the execution context.

val get_rac : ctx -> Pinterp_core.rac

Return the RAC engine of the execution context.

val get_giant_steps : ctx -> bool

Return true if the execution context is configured with giant steps.

Execution results

type result =

`\|`	`Normal of Pinterp_core.Value.value`
`\|`	`Excep of Ity.xsymbol * Pinterp_core.Value.value`
`\|`	`Irred of Expr.expr`

An execution may terminate normally, with an exception, or with an irreducible expression.

val print_logic_result : result Pp.pp

Execution functions

val exec_rs : ctx -> Expr.rsymbol -> result * ctx

eval_rs ~rac env pm rs evaluates the definition of rs and returns an evaluation result and a final environment.

Raises
- Fail if an assertion was violated during RAC
- Stuck if an assumption was violated during RAC or a giant step.
- Incomplete if there is an unsopported feature or some term could not be reduced.

val exec_global_fundef : ctx ->
       (Expr.rsymbol * Expr.cexp) list ->
       Expr.rec_defn list option ->
       Expr.expr ->
       result * Pinterp_core.Value.value Term.Mvs.t *
       Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t

eval_global_fundef ~rac env pkm dkm rcl rdl e evaluates e and returns an evaluation result and a final variable environment (for both local and global variables).

Same exceptions as exec_global_fundef.

Reporting, i.e. pretty printing

val report_eval_result : Expr.expr ->
       Stdlib.Format.formatter ->
       result * Pinterp_core.Value.value Term.Mvs.t *
       Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t -> unit

Report an evaluation result

val report_cntr : (Pinterp_core.cntr_ctx * Term.term) Pp.pp