package herdtools7

You can search for identifiers within the package.

in-package search v0.2.0

package herdtools7

herdtools7.asllib
- Asllib
  - AST
  - ASTUtils
    
    IMap
    
    ISet
    
    Infix
  - Asl_stdlib
  - Backend
    
    S
    
    Scope
    
    SCOPE
  - Bitvector
  - Builder
  - Desugar
  - Diet
    
    ELT
    
    INTERVAL_SET
    
    Interval
    
    Int
    
    Interval
    
    Int64
    
    Interval
    
    Make
    
    Elt
    
    Interval
    
    Z
    
    Interval
  - Env
    
    RunTime
    
    C
    
    Scope
    
    RunTimeConf
    
    Scope
    
    S
    
    Scope
  - Error
    
    ERROR_PRINTER_CONFIG
    
    ErrorPrinter
    
    C
    
    PPrint
  - Gparser0
  - Instrumentation
    
    SEMBUFFER
    
    SEMINSTR
    
    SemMake
    
    Buffer
    
    SemanticsCmp
    
    SemanticsMap
    
    SemanticsNoBuffer
    
    SemanticsNoInstr
    
    SemanticsRule
    
    SemanticsSet
    
    SemanticsSingleBuffer
    
    SemanticsSingleInstr
    
    SemanticsSingleSetBuffer
    
    SemanticsSingleSetInstr
    
    TYPBUFFER
    
    TYPINSTR
    
    TypMake
    
    Buffer
    
    TypingCmp
    
    TypingNoBuffer
    
    TypingNoInstr
    
    TypingRule
    
    TypingSet
    
    TypingSingleBuffer
    
    TypingSingleInstr
    
    TypingSingleSetBuffer
    
    TypingSingleSetInstr
    
    TypingsMap
  - Interpreter
    
    Config
    
    Instr
    
    Make
    
    B
    
    Scope
    
    C
    
    Instr
    
    IEnv
    
    S
    
    B
    
    Scope
    
    IEnv
  - Lexer
    
    CONFIG
    
    Make
    
    Config
  - Lexer0
  - Native
    
    DeterministicBackend
    
    DeterministicInterpreter
    
    C
    
    Instr
    
    IEnv
    
    NoScope
    
    StaticBackend
  - Operations
  - PP
  - Parser
    
    Make
    
    Config
  - Parser0
    
    Incremental
    
    MenhirInterpreter
  - ParserConfig
    
    CONFIG
  - RepeatableLexer
  - Serialize
  - SideEffect
    
    SES
    
    SESet
    
    TimeFrame
  - SimpleLexer0
  - Splitasl
  - StaticEnv
  - StaticInterpreter
  - StaticModel
  - StaticOperations
    
    CONFIG
    
    Make
    
    C
  - Storage
  - Tokens
  - TopoSort
    
    ASTFold
    
    Make
    
    O
    
    Properties
    
    OrderedHashedType
  - Types
    
    Domain
  - Typing
    
    ANNOTATE_CONFIG
    
    Annotate
    
    C
    
    S
    
    TypeCheckDefault
  - Version

Legend:
Library
Module
Module type
Parameter
Class
Class type

type value = native_value

The runtime values that the interpreter should use.

val debug_value : value -> string

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

val is_undetermined : value -> bool

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

val 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.

val v_of_int : int -> value

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

val 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.

val 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.

type 'a m = 'a

Main monad type to chain operations done by the interpreter.

val return : 'a -> 'a m

Monadic constructor.

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

Flag loop unrolling pruning

val 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.

val 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.

val 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.

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

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

val 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.

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

Print representation of monad on stderr

val commit : string option -> unit m

Branching event

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

choice is a boolean if operator.

val 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

val create_vector : value list -> value m

Creates a vector with this values.

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

Creates a record, with the indicated names.

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

Creates an exception, with the indicated names.

val get_index : int -> value -> value m

get_i i vec returns value at index i inside vec.

val set_index : int -> value -> value -> value m

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

val get_field : string -> value -> value m

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

val set_field : string -> value -> value -> value m

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

Other operations

val 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.

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

Evaluates the binary operation on those two values.

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

Evaluate this unary operation on this value.

val 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

module Scope = NoScope

val on_read_identifier : AST.identifier -> Scope.t -> value -> unit m

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

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

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

type value_range = value * value

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

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

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

val 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.

val concat_bitvectors : value list -> value m

Similar to Bitvector.concat, but monadic style obviously.

val bitvector_length : value -> value m

Get the length of a bitvector.

type 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.

val primitives : (AST.func * primitive) list

The list of primitives that a backend provides.