Module `Libsail.Interpreter`Source

Sourcemodule Document = Pretty_print_sail.Document

Sourcemodule Printer : sig ... end

Sourcetype gstate = {

registers : Value.value Ast_util.Bindings.t;
allow_registers : bool;
primops : (Value.value list -> Value.value) Value.StringMap.t;
letbinds : Type_check.tannot Ast.letbind list;
fundefs : Type_check.tannot Ast.fundef Ast_util.Bindings.t;
last_write_ea : (Value.value * Value.value * Value.value) option;
typecheck_env : Type_check.Env.t;

}

Sourcetype lstate = {

locals : Value.value Ast_util.Bindings.t;

}

Sourcetype state = lstate * gstate

Sourceval value_of_lit : Ast.lit -> Value.value

Sourceval is_value : 'a Ast.exp -> bool

Sourceval is_true : 'a Ast.exp -> bool

Sourceval is_false : 'a Ast.exp -> bool

Sourceval exp_of_value : Value.value -> Type_check.tannot Ast.exp

Sourceval value_of_exp : 'a Ast.exp -> Value.value

Sourceval fallthrough : Type_check.tannot Ast.pexp

Sourcetype return_value =

| Return_ok of Value.value
| Return_exception of Value.value

Sourcetype 'a response =

| Early_return of Value.value
| Exception of Value.value
| Assertion_failed of string
| Call of Ast.id * Value.value list * return_value -> 'a
| Fail of string
| Read_mem of Value.value * Value.value * Value.value * Value.value -> 'a
| Write_ea of Value.value * Value.value * Value.value * unit -> 'a
| Excl_res of bool -> 'a
| Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> 'a
| Barrier of Value.value * unit -> 'a
| Read_reg of string * Value.value -> 'a
| Write_reg of string * Value.value * unit -> 'a
| Get_primop of string * (Value.value list -> Value.value) -> 'a
| Get_local of string * Value.value -> 'a
| Put_local of string * Value.value * unit -> 'a
| Get_global_letbinds of Type_check.tannot Ast.letbind list -> 'a

Sourceand 'a monad =

| Pure of 'a
| Yield of 'a monad response

Sourceval map_response : ('a -> 'b) -> 'a response -> 'b response

Sourceval liftM : ('a -> 'b) -> 'a monad -> 'b monad

Sourceval return : 'a -> 'a monad

Sourceval bind : 'a monad -> ('a -> 'b monad) -> 'b monad

Sourceval (>>=) : 'a monad -> ('a -> 'b monad) -> 'b monad

Sourceval (>>) : unit monad -> 'a monad -> 'a monad

Sourcetype ('a, 'b) either =

| Left of 'a
| Right of 'b

Sourceval catch : 'a monad -> (Value.value, 'a) either monad

Sourceval throw : Value.value -> 'a monad

Sourceval call : Ast.id -> Value.value list -> return_value monad

Sourceval read_mem : Value.value -> Value.value -> Value.value -> Value.value monad

Sourceval write_ea : Value.value -> Value.value -> Value.value -> unit monad

Sourceval excl_res : unit -> bool monad

Source

val write_mem : 
  Value.value ->
  Value.value ->
  Value.value ->
  Value.value ->
  bool monad

Sourceval barrier : Value.value -> unit monad

Sourceval read_reg : string -> Value.value monad

Sourceval write_reg : string -> Value.value -> unit monad

Sourceval fail : string -> 'a monad

Sourceval get_primop : string -> (Value.value list -> Value.value) monad

Sourceval get_local : string -> Value.value monad

Sourceval put_local : string -> Value.value -> unit monad

Sourceval get_global_letbinds : unit -> Type_check.tannot Ast.letbind list monad

Sourceval early_return : Value.value -> 'a monad

Sourceval assertion_failed : string -> 'a monad

Sourceval liftM2 : ('a -> 'b -> 'c) -> 'a monad -> 'b monad -> 'c monad

Sourceval letbind_pat_ids : 'a Ast.letbind -> Ast_util.IdSet.t

Source

val subst : 
  Ast.id ->
  Value.value ->
  Type_check.tannot Ast.exp ->
  Type_check.tannot Ast.exp

Source

val local_variable : 
  Ast_util.Bindings.key ->
  lstate ->
  'a ->
  Type_check.tannot Ast.exp

Sourceval unit_exp : 'a Ast.exp_aux

Sourceval is_value_fexp : 'a Ast.fexp -> bool

Sourceval value_of_fexp : 'a Ast.fexp -> string * Value.value

Source

val build_letchain : 
  Ast_util.IdSet.elt ->
  'a Ast.letbind list ->
  'a Ast.exp ->
  'a Ast.exp

Sourceval is_interpreter_extern : Ast.id -> Type_check.Env.t -> bool

Sourceval get_interpreter_extern : Ast.id -> Type_check.Env.t -> string

Sourcetype partial_binding =

| Complete_binding of Value.value
| Partial_binding of (Value.value * Libsail.Value.Big_int.num * Libsail.Value.Big_int.num) list

Source

val combine : 
  'a ->
  partial_binding option ->
  partial_binding option ->
  partial_binding option

Source

val complete_bindings : 
  partial_binding Ast_util.Bindings.t ->
  Value.value Ast_util.Bindings.t

Sourceval step : Type_check.tannot Ast.exp -> Type_check.tannot Ast.exp monad

Sourceval exp_of_lexp : Ast_util.uannot Ast.lexp -> Ast_util.uannot Ast.exp

Source

val pattern_match : 
  Type_check.Env.t ->
  Type_check.tannot Ast.pat ->
  Value.value ->
  bool * partial_binding Ast_util.Bindings.t

Source

val exp_of_fundef : 
  Type_check.tannot Ast.fundef ->
  Value.value ->
  Type_check.tannot Ast.exp

Sourceval defs_letbinds : ('a, 'b) Ast.def list -> 'a Ast.letbind list

Sourceval initial_lstate : lstate

Sourceval stack_cont : ('a * 'b * 'c) -> 'c

Sourceval stack_string : ('a * 'b * 'c) -> 'a

Sourceval stack_state : ('a * 'b * 'c) -> 'b

Sourcetype frame =

| Done of state * Value.value
| Step of string Lazy.t * state * Type_check.tannot Ast.exp monad * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list
| Break of frame
| Effect_request of string Lazy.t * state * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * effect_request
| Fail of string Lazy.t * state * Type_check.tannot Ast.exp monad * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * string

Sourceand effect_request =

| Read_mem of Value.value * Value.value * Value.value * Value.value -> state -> frame
| Write_ea of Value.value * Value.value * Value.value * unit -> state -> frame
| Excl_res of bool -> state -> frame
| Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> state -> frame
| Barrier of Value.value * unit -> state -> frame
| Read_reg of string * Value.value -> state -> frame
| Write_reg of string * Value.value * unit -> state -> frame

Sourceval eval_frame' : frame -> frame

Sourceval eval_frame : frame -> frame

Sourceval default_effect_interp : state -> effect_request -> frame

Sourceval effect_interp : (state -> effect_request -> frame) ref

Sourceval set_effect_interp : (state -> effect_request -> frame) -> unit

Sourceval run_frame : frame -> Value.value

Sourceval eval_exp : state -> Type_check.tannot Ast.exp -> Value.value

Source

val initial_gstate : 
  (Value.value list -> Value.value) Value.StringMap.t ->
  (Type_check.tannot, 'a) Ast.def list ->
  Type_check.Env.t ->
  gstate

Source

val initialize_registers : 
  bool ->
  bool ->
  gstate ->
  (Type_check.tannot, 'a) Ast.def list ->
  gstate

Source

val initial_state : 
  ?registers:bool ->
  ?undef_registers:bool ->
  (Type_check.tannot, 'a) Ast_defs.ast ->
  Type_check.Env.t ->
  (Value.value list -> Value.value) Value.StringMap.t ->
  lstate * gstate

Sourcetype value_result =

| Value_success of Value.value
| Value_error of exn

Sourceval decode_instruction : state -> Ast.lit_aux list -> value_result

Source

val annot_exp_effect : 
  Type_check.tannot Ast.exp_aux ->
  Ast.l ->
  Type_check.Env.t ->
  Ast.typ ->
  Type_check.tannot Ast.exp

Source

val annot_exp : 
  Type_check.tannot Ast.exp_aux ->
  Ast.l ->
  Type_check.Env.t ->
  Ast.typ ->
  Type_check.tannot Ast.exp

Sourceval id_typ : string -> Ast.typ

Sourceval analyse_instruction : state -> Value.value -> frame

Sourceval execute_instruction : state -> Value.value -> frame

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/Interpreter/index.html

Module `Libsail.Interpreter`Source

package libsail

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/Interpreter/index.html

Module Libsail.InterpreterSource

Module `Libsail.Interpreter`Source