package herdtools7

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Predicates on types
Relations on types

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 Algebra

Types are defined as AST.ty. This should map pretty-well with the current version of the Language Reference Manual.

type env = StaticEnv.env

Predicates on types

val is_builtin : AST.ty -> bool

val is_builtin_singular : AST.ty -> bool

val is_builtin_aggregate : AST.ty -> bool

Note that a builtin type is either builtin aggregate or builtin singular.

val is_singular : env -> AST.ty -> bool

val is_aggregate : env -> AST.ty -> bool

Note that a type is either singular or aggregate.

val is_named : AST.ty -> bool

Types declared using the type syntax.

val is_anonymous : AST.ty -> bool

Those not declared using †he type syntax.

Note that a type is either builtin, named or anonymous.

val is_primitive : AST.ty -> bool

Types that only use the builtin types.

val is_non_primitive : AST.ty -> bool

Types that are named types or which make use of named types.

Usually for all ty:

is_non_primitive ty = not (is_primitive ty)

Relations on types

Type transformations

val make_anonymous : env -> AST.ty -> AST.ty

Replace any named type by its declared type in the environment.

val get_structure : env -> AST.ty -> AST.ty

The structure of a type is the primitive type that can hold the same values.

val parameterized_ty : AST.identifier -> AST.ty

Builds an parameterized integer type from a declared variable.

val to_well_constrained : AST.ty -> AST.ty

Transform a parameterized integer type into a well-constrained integer equal to the parameter that have this type, and leave the other types (such as well-constrained integers) as they are.

val get_well_constrained_structure : env -> AST.ty -> AST.ty

get_well_constrained_structure env ty quivalent to get_structure env ty |> to_well_constrained.

Domains

module Domain : sig ... end

The domain of a type is the symbolic representation of the set of values which storage element of that type may hold.

Orders on types

val subtypes : env -> AST.ty -> AST.ty -> bool

subtypes env t1 t2 is true if and only if t1 is a declared subtype of t2.

val subtypes_names : env -> AST.identifier -> AST.identifier -> bool

subtypes_names env s1 s2 is true if and only if the type named s1 is a declared subtype of the type named s2.

Equivalent to subtypes env (T_Named s1 |> here) (T_Named s2 |> here).

val subtype_satisfies : env -> AST.ty -> AST.ty -> bool

Subtype-satisfation as per Definition TRVR.

val type_satisfies : env -> AST.ty -> AST.ty -> bool

Type-satisfation as per Rule FMXK.

val type_clashes : env -> AST.ty -> AST.ty -> bool

Type-clashing relation.

Notes:

T subtype-satisfies S implies T and S type-clash
This is an equivalence relation

per Definition VPZZ.

val subprogram_clashes : env -> AST.func -> AST.func -> bool

Subprogram clashing relation.

per Definition BTBR.

val lowest_common_ancestor : env -> AST.ty -> AST.ty -> AST.ty option

Lowest common ancestor.

As per Rule YZHM.

val type_equal : env -> AST.ty -> AST.ty -> bool

Equality in env for types.