package herdtools7

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

Module Asllib.TypesSource

Type Algebra

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

Predicates on types

Sourceval is_builtin : AST.ty -> bool
Sourceval is_builtin_singular : AST.ty -> bool
Sourceval is_builtin_aggregate : AST.ty -> bool

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

Sourceval is_singular : env -> AST.ty -> bool
Sourceval is_aggregate : env -> AST.ty -> bool

Note that a type is either singular or aggregate.

Sourceval is_named : AST.ty -> bool

Types declared using the type syntax.

Sourceval is_anonymous : AST.ty -> bool

Those not declared using †he type syntax.

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

Sourceval is_primitive : AST.ty -> bool

Types that only use the builtin types.

Sourceval 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

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

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

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

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

Sourceval parameterized_ty : AST.identifier -> AST.ty

Builds an parameterized integer type from a declared variable.

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

Sourceval 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

Sourcemodule 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

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

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

Sourceval 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).

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

Subtype-satisfation as per Definition TRVR.

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

Type-satisfation as per Rule FMXK.

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

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

Subprogram clashing relation.

per Definition BTBR.

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

Lowest common ancestor.

As per Rule YZHM.

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

Equality in env for types.

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