package herdtools7

  1. Overview
  2. Docs

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 under_constrained_ty : AST.identifier -> AST.ty

From a declared variable, builds an under-constrained integer.

val to_well_constrained : AST.ty -> AST.ty

Transform an under-constrained 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 set of values which storagbe element of that type may hold.

Orders on types

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

Subtype-satisfation as per Definition TRVR.

val domain_subtype_satisfies : env -> AST.ty -> AST.ty -> bool
val structural_subtype_satisfies : env -> AST.ty -> AST.ty -> bool
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.

OCaml

Innovation. Community. Security.