Module Pinterp

module Pinterp: sig .. end

Interpretation of Why3 programs


Interpreter values

type float_mode 
type big_float 
module Value: sig .. end
module Mv: Extmap.S  with type key = Value.value
val v_ty : Value.value -> Ty.ty
val v_desc : Value.value -> Value.value_desc

non defensive API for building values: there are no checks that ity is compatible with the value being built

val int_value : BigInt.t -> Value.value
val range_value : Ity.ity -> BigInt.t -> Value.value
val string_value : string -> Value.value
val bool_value : bool -> Value.value
val proj_value : Ity.ity -> Term.lsymbol -> Value.value -> Value.value
val constr_value : Ity.ity ->
Expr.rsymbol ->
Expr.rsymbol list -> Value.value list -> Value.value
val purefun_value : result_ity:Ity.ity ->
arg_ity:Ity.ity ->
Value.value Mv.t ->
Value.value -> Value.value
val unit_value : Value.value
val undefined_value : Ity.ity -> Value.value
val field : Value.value -> Value.field
val field_get : Value.field -> Value.value
val field_set : Value.field -> Value.value -> unit
val default_value_of_type : Env.env -> Pdecl.known_map -> Ity.ity -> Value.value
val print_value : Stdlib.Format.formatter -> Value.value -> unit

Interpreter log

module type Log = sig .. end
module Log: Log 

Interpreter configuration

val init_real : int * int * int -> unit

Give a precision on real computation.

type rac_prover 

The configuration of the prover used for reducing terms in RAC

val rac_prover : command:string ->
Driver.driver -> Call_provers.resource_limit -> rac_prover
type rac_reduce_config 

The configuration for RAC, including (optionally) a transformation for reducing terms (usually: compute_in_goal), and a prover to be used if the transformation does not yield a truth value. When neither transformation nor prover are defined, then RAC does not progress.

val rac_reduce_config : ?trans:Task.task Trans.tlist ->
?prover:rac_prover ->
?try_negate:bool -> unit -> rac_reduce_config
val rac_reduce_config_lit : Whyconf.config ->
Env.env ->
?trans:string ->
?prover:string -> ?try_negate:bool -> unit -> rac_reduce_config

rac_reduce_config_lit cnf env ?trans ?prover ?try_negate () configures the term reduction of RAC. trans is the name of a transformation (usually "compute_in_goal"). prover is a prover string with optional, space-sparated time limit and memory limit. And with ~try_negate:true the negated term is dispatched to the prover if the prover didn't return a result for the positive form.

type import_value = ?name:string -> ?loc:Loc.position -> Ity.ity -> Value.value option 
type rac_config = private {
   do_rac : bool; (*

check assertions

*)
   rac_abstract : bool; (*

interpret abstractly

*)
   skip_cannot_compute : bool; (*

continue when term cannot be checked

*)
   rac_reduce : rac_reduce_config; (*

configuration for reducing terms

*)
   get_value : import_value; (*

import values when they are needed

*)
   log_uc : Log.log_uc; (*

log

*)
}
val rac_config : do_rac:bool ->
abstract:bool ->
?skip_cannot_compute:bool ->
?reduce:rac_reduce_config ->
?get_value:(?name:string ->
?loc:Loc.position -> Ity.ity -> Value.value option) ->
unit -> rac_config

Interpreter environment and results

type env = private {
   pmodule : Pmodule.pmodule;
   funenv : Expr.cexp Expr.Mrs.t;
   vsenv : Value.value Term.Mvs.t;
   rsenv : Value.value Expr.Mrs.t;
   env : Env.env;
   rac : rac_config;
}

Context for the interpreter

type result = private 
| Normal of Value.value
| Excep of Ity.xsymbol * Value.value
| Irred of Expr.expr

Result of the interpreter *

type cntr_ctx = private {
   c_desc : string;
   c_trigger_loc : Loc.position option;
   c_env : env;
}

Context of a contradiction during RAC

exception CannotCompute of {
   reason : string;
}

raised when interpretation cannot continue due to unsupported feature

exception Contr of cntr_ctx * Term.term

raised when a contradiction is detected during RAC.

exception RACStuck of env * Loc.position option

raised when an assumed property is not satisfied

Interpreter

val eval_global_fundef : rac_config ->
Env.env ->
Pmodule.pmodule ->
(Expr.rsymbol * Expr.cexp) list ->
Expr.expr ->
result * Value.value Term.Mvs.t *
Value.value Expr.Mrs.t

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

During RAC, annotations are first reduced by applying transformation rac.rac_trans, and if the transformation doesn't return to a trivial formula (true/false), the prover rac.rac_prover is applied. Pure expressions and pure executions are reduced only using rac.rac_trans. When neither ra.rac_trans or rac.rac_prover are defined, RAC does not progress.

raises Contr _ if rac.rac and a an assertion was violated.

raises CannotCompute _ if some term could not be reduced due to unsopported feature.

raises Failure _ if there is an unsopported feature.

raises RACStuck _ if a property that should be assumed is not satisfied in the current enviroment.

val report_cntr : Stdlib.Format.formatter -> cntr_ctx * Term.term -> unit
val report_cntr_body : Stdlib.Format.formatter -> cntr_ctx * Term.term -> unit

Report a contradiction context and term

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

Report an evaluation result

val eval_rs : rac_config ->
Env.env -> Pmodule.pmodule -> Expr.rsymbol -> result * env

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

raises Contr _ if rac.rac and a an assertion was violated.

raises CannotCompute _ if some term could not be reduced due to unsopported feature.

raises Failure _ if there is an unsopported feature.

raises RACStuck _ if a property that should be assumed is not satisfied in the current enviroment.