package herdtools7

  1. Overview
  2. Docs
package herdtools7
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Native.StaticBackendSource

Sourcetype value = native_value

The runtime values that the interpreter should use.

Sourceval debug_value : value -> string

A printer for value, should only be used for debugging.

Sourceval is_undetermined : value -> bool

is_undetermined v returns true when c is a non-constant value

Sourceval v_of_literal : AST.literal -> value

v_of_parsed_v constructs a value from a parsed value. Note that the prefered method to create records or any complex values is create_vector, and should be used for constructing complex values.

Sourceval v_of_int : int -> value

v_of_int is used to convert raw integers arising from the interpretation, and not parsed values.

Sourceval v_to_z : value -> Z.t option

v_to_z v returns, if possible, an integer corresponding to the value. Should be called only on values of type integer.

Sourceval v_to_label : value -> string

v_to_label v returns the identifier of the label nested in the literal inside v. Should be called only on values of type NV_Literal where the literal is of type L_Label.

Sourcetype 'a m = 'a

Main monad type to chain operations done by the interpreter.

Sourceval return : 'a -> 'a m

Monadic constructor.

Sourceval cutoffT : string -> 'a -> 'a m

Flag loop unrolling pruning

Sourceval bind_data : 'a m -> ('a -> 'b m) -> 'b m

Monadic bind operation, used when data from the first operation is needed to compute the second operation.

Sourceval bind_seq : 'a m -> ('a -> 'b m) -> 'b m

Monadic bind operation, but that only passes internal interpreter data. This should not create any data-dependency.

Sourceval bind_ctrl : 'a m -> ('a -> 'b m) -> 'b m

Monadic bind operation, but that creates a control dependency between the first argument and the result of the second one.

Sourceval prod_par : 'a m -> 'b m -> ('a * 'b) m

Monadic product operation, two monads are combined "in parallel".

Sourceval appl_data : 'a m -> ('a -> 'b) -> 'b m

Applicative map.

Creates a data dependency between the output events and the input events of the argument in the resulting monad.

Sourceval debugT : string -> 'a m -> 'a m

Print representation of monad on stderr

Sourceval commit : string option -> unit m

Branching event

Sourceval choice : value m -> 'b m -> 'b m -> 'b m

choice is a boolean if operator.

Sourceval delay : 'a m -> ('a -> 'a m -> 'b m) -> 'b m

delay operator spits monad into result 'a and hidden structure. This permits deciding on the monad value, while using hidden structure later

Special operations with vectors

Sourceval create_vector : value list -> value m

Creates a vector with this values.

Sourceval create_record : (AST.identifier * value) list -> value m

Creates a record, with the indicated names.

Sourceval create_exception : (AST.identifier * value) list -> value m

Creates an exception, with the indicated names.

Sourceval get_index : int -> value -> value m

get_i i vec returns value at index i inside vec.

Sourceval set_index : int -> value -> value -> value m

set_i i v vec returns vec with index i replaced by v.

Sourceval get_field : string -> value -> value m

get_field "foo" v is the value mapped by "foo" in the record v.

Sourceval set_field : string -> value -> value -> value m

set_field "foo" v record is record with "foo" mapping to v.

Other operations

Sourceval v_unknown_of_type : eval_expr_sef:(AST.expr -> value m) -> AST.ty -> value m

v_unknown_of_type ~eval_expr_sef t constructs an arbitrary value from a type.

Sourceval binop : AST.binop -> value -> value -> value m

Evaluates the binary operation on those two values.

Sourceval unop : AST.unop -> value -> value m

Evaluate this unary operation on this value.

Sourceval ternary : value -> (unit -> value m) -> (unit -> value m) -> value m

ternary v w1 w2 is w1 if v is true and w2 if v is false

Sourcemodule Scope = NoScope
Sourceval on_read_identifier : AST.identifier -> Scope.t -> value -> unit m

on_read_identifier is called when a value is read from the local environment.

Sourceval on_write_identifier : AST.identifier -> Scope.t -> value -> unit m

on_write_identifier is called when a value is read from the local environment.

Sourcetype value_range = value * value

Represents a range by its first accessed index and its length.

Sourceval read_from_bitvector : value_range list -> value -> value m

Read a slice (represented by a list of value ranges) from a bitvector.

Sourceval write_to_bitvector : value_range list -> value -> value -> value m

write_to_bitvector value_ranges w v writes the bits of w into v at the positions specified by value_range.

Sourceval concat_bitvectors : value list -> value m

Similar to Bitvector.concat, but monadic style obviously.

Sourceval bitvector_length : value -> value m

Get the length of a bitvector.

Sourcetype primitive = value m list -> value m list -> value m list m

primitive types that go with this AST. First argument is list of parameters, second argument is list of arguments.

Sourceval primitives : (AST.func * primitive) list

The list of primitives that a backend provides.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct