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 : Why3.Env.env -> Why3.Pmodule.pmodule0 -> Why3.Pinterp_core.env

Pinterp_core.env repeated here for convenience.

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

Pinterp_core.mk_rac repeated here for convenience.

val mk_ctx : Why3.Pinterp_core.env ->
       limits:Why3.Call_provers.resource_limits ->
       ?giant_steps:bool ->
       ?do_rac:bool ->
       ?rac:Why3.Pinterp_core.rac ->
       ?oracle:Why3.Pinterp_core.oracle ->
       ?compute_term:(Why3.Pinterp_core.env -> Why3.Term.term -> Why3.Term.term) ->
       unit -> ctx

Create an execution context.

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 -> Why3.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 -> Why3.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 Why3.Pinterp_core.Value.value`
`\|`	`Excep of Why3.Ity.xsymbol * Why3.Pinterp_core.Value.value`
`\|`	`Irred of Why3.Expr.expr`

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

val print_logic_result : result Why3.Pp.pp

Execution functions

val exec_rs : ctx -> Why3.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 ->
       (Why3.Expr.rsymbol * Why3.Expr.cexp) list ->
       Why3.Expr.rec_defn list option ->
       Why3.Expr.expr ->
       result * Why3.Pinterp_core.Value.value Why3.Term.Mvs.t *
       Why3.Pinterp_core.Value.value Stdlib.Lazy.t Why3.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 : Why3.Expr.expr ->
       Stdlib.Format.formatter ->
       result * Why3.Pinterp_core.Value.value Why3.Term.Mvs.t *
       Why3.Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t -> unit

Report an evaluation result

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