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

This module is the signature of any backend of the ASL interpreter.

type 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

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 : SCOPE

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.