From fee8efe62f55f7feb6162ba57b986f913ecead15 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Tue, 26 Sep 2023 16:58:00 +0100 Subject: [PATCH] Pages from c93f4eea3782d0560f0ce4fe08a7d99b8a7624f1 --- herdtools7/ASLTypingReference.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/herdtools7/ASLTypingReference.html b/herdtools7/ASLTypingReference.html index d068b8b14..524de5e25 100644 --- a/herdtools7/ASLTypingReference.html +++ b/herdtools7/ASLTypingReference.html @@ -1,5 +1,5 @@ -ASLTypingReference (herdtools7.ASLTypingReference)

ASL Typing Reference

Disclaimer

This material covers both ASLv0 (viz, the existing ASL pseudocode language which appears in the Arm Architecture Reference Manual) and ASLv1, a new, experimental, and as yet unreleased version of ASL.

This material is work in progress, more precisely at pre-Alpha quality as per Arm’s quality standards. In particular, this means that it would be premature to base any production tool development on this material.

However, any feedback, question, query and feature request would be most welcome; those can be sent to Arm’s Architecture Formal Team Lead Jade Alglave <jade.alglave@arm.com> or by raising issues or PRs to the herdtools7 github repository.

Type nomenclature

Named and Anonymous Types

Definitions

All types are either:

Examples

Primitive and Non-primitive types

Definitions

All types are either:

Examples

Structure of a type

Definition

The structure of a type is the primitive type it is equivalent to such that it can hold the same values.

Examples

type T1 of integer; is the named type T1 whose structure is integer.

type T2 of (integer, T1); is the named type T2 whose structure is (integer, integer). In this example, (integer, T1) is non-primitive since it uses T1.

In this example: var x: T1; the type of x is the named (hence non-primitive) type T1, whose structure is integer.

In this example: var y: integer; the type of y is the anonymous primitive type integer.

In this example: var z: (integer, T1); the type of z is the anonymous non-primitive type `(integer, T1)` whose structure is `(integer, integer)`.

Domain of Values for Types

Definition

The domain of a type is the set of values which storage elements of that type may hold.

Examples

The domain of integer is the infinite set of all integers.

The domain of bits(1) is the set {‘1’, ‘0’}.

The domain of integer {2,16} is the set containing the integers 2 and 16.

The domain of bits({2,16}) is the set containing all two bit and all sixteen bit values.

Typing Rules

Typing a program is typing its main function. Constructively, typing a program requires following its Abstract Syntax Tree and typing each of its components.

Formally, the types of a program are given by applying a set of annotate_<object> functions. Each annotate_<object> function describes how to annotate a specific object, as follows.

Typing of Expressions

annotate_expr specifies how to annotate an expression e in an environment env. Formally, the result of annotating the expression e in env is t,new_e and one of the following applies:

TypingRule.Lit

Rule

All of the following applies:

Examples

TypingRule.TypedExpr

Rule

All of the following applies:

Examples

TypingRule.ELocalVarConstant

Rule

All of the following applies:

Examples

TypingRule.ELocalVar

Rule

All of the following applies:

Examples

TypingRule.EGlobalVarConstantVal

Rule

All of the following applies:

Examples

TypingRule.EGlobalVar

Rule

All of the following applies:

Examples

TypingRule.EUndefIdent

Rule

All of the following applies:

Examples

TypingRule.Binop

Rule

All of the following applies:

Examples

TypingRule.Unop

Rule

All of the following applies:

Examples

TypingRule.ECond

Rule

All of the following applies:

Examples

TypingRule.ETuple

Rule

All of the following applies:

Examples

TypingRule.EConcatEmpty

Rule

All of the following applies:

Examples

TypingRule.EConcat

Rule

All of the following applies:

Examples

TypingRule.ERecordNotARecord

Rule

All of the following applies:

Examples

TypingRule.ERecordMissingField

Rule

All of the following applies:

Examples

TypingRule.ERecord

Rule

All of the following applies:

Examples

TypingRule.ECall

Rule

All of the following applies:

Examples

TypingRule.EUnknown

Rule

All of the following applies:

Examples

TypingRule.ESlice

Rule

All of the following applies:

Examples

TypingRule.EGetArray

Rule

All of the following applies:

Examples

TypingRule.EGetRecordField

Rule

All of the following applies:

Examples

TypingRule.EGetBadRecordField

Rule

All of the following applies:

Examples

TypingRule.EGetBadBitField

Rule

All of the following applies:

Examples

TypingRule.EGetBadField

Rule

All of the following applies:

Examples

TypingRule.EGetBitField

Rule

All of the following applies:

Examples

TypingRule.EGetBitFieldNested

Rule

All of the following applies:

Examples

TypingRule.EGetBitFieldTyped

Rule

All of the following applies:

Examples

TypingRule.EGetBitFields

Rule

<description>

Examples

<minimal example>

TypingRule.EPattern

Rule

All of the following applies:

Examples

Typing of Left-Hand-Side Expressions

annotate_lexpr version env le t_e is new_le and one of the following applies:

TypingRule.LEIgnore

Rule

All of the following applies:

Examples

TypingRule.LELocalVar

Rule

All of the following applies:

Examples

TypingRule.LEGlobalVar

Rule
Examples

TypingRule.LETuple

Rule

All of the following applies:

Examples

TypingRule.LESlice

Rule

All of the following applies:

Examples

TypingRule.LESetArray

Rule

All of the following applies:

Examples

TypingRule.LESetBadRecordField

Rule

All of the following applies:

Examples

TypingRule.LESetRecordField

Rule

All of the following applies:

Examples

TypingRule.LESetBadBitField

Rule

All of the following applies:

Examples

TypingRule.LESetBitField

Rule

All of the following applies:

Examples

TypingRule.LESetBitFieldNested

Rule

All of the following applies:

Examples

TypingRule.LESetBitFieldTyped

Rule

All of the following applies:

Examples

TypingRule.LESetBadField

Rule

All of the following applies:

Examples

TypingRule.LESetFields

Rule
Examples

TypingRule.LEConcat

Rule
Examples

Typing of Local Declarations

annotate_local_decl_item loc env ty ldk ldi is new_env, new_ldi and one of the following applies:

TypingRule.LDIgnoreNone

Rule

All of the following applies:

Examples

TypingRule.LDIgnoreSome

Rule

All of the following applies:

Examples

TypingRule.LDVar

Rule

All of the following applies:

Examples

TypingRule.LDUninitialisedTypedTuple

Rule

All of the following applies:

Examples

TypingRule.LDTuple

Rule
Examples

TypingRule.LDTypedTuple

Rule
Examples

Typing of Statements

annotate_stmt env s is a statement new_s and an environment new_env and one of the following applies:

TypingRule.SPass

Rule

All of the following applies:

Examples

TypingRule.SThen

Rule

All of the following applies:

Examples

TypingRule.SAssign

Rule

All of the following applies:

Examples

TypingRule.SCall

Rule

All of the following applies:

Examples

TypingRule.SReturnNone

Rule

All of the following applies:

Examples

TypingRule.SReturnOne

Rule

All of the following applies:

Examples

TypingRule.SReturnSome

Rule

All of the following applies:

Examples

TypingRule.SCond

Rule

All of the following applies:

Examples

TypingRule.SCase

Rule

All of the following applies:

Examples

TypingRule.SAssert

Rule

All of the following applies:

Examples

TypingRule.SWhile

Rule

All of the following applies:

Examples

TypingRule.SRepeat

Rule

All of the following applies:

Examples

TypingRule.SFor

Rule

All of the following applies:

Examples

TypingRule.SDeclSome

Rule

All of the following applies:

Examples

TypingRule.SDeclNone

Rule

All of the following applies:

Examples

TypingRule.SThrowNone

Rule

All of the following applies:

Examples

TypingRule.SThrowSome

Rule

All of the following applies:

Examples

TypingRule.STry

Rule

All of the following applies:

Examples

Typing of Slices

annotate_slices env slices is the pair (offset, length) and one of the following applies:

TypingRule.SliceLength

Rule

All of the following applies:

Examples

TypingRule.SliceSingle

Rule

All of the following applies:

Comments

R_GXKG: The notation bi is syntactic sugar for bi +: 1.

Examples

TypingRule.SliceRange

Rule

All of the following applies:

Comments

R_GXKG: The notation bj:i is syntactic sugar for bi +: j-i+1.

Examples

TypingRule.SliceStar

Rule

All of the following applies:

Comments

R_GXQG: The notation bi *: n is syntactic sugar for bi*n +: n

Examples

Typing of Patterns

annotate_pattern loc env t p is new_p and one of the following applies:

TypingRule.PAll

Rule

All of the following applies:

Examples

TypingRule.PAny

Rule

All of the following applies:

Examples

TypingRule.PNot

Rule

All of the following applies:

Examples

TypingRule.PSingle

Rule
Examples

TypingRule.PGeq

Rule

All of the following applies:

Examples

TypingRule.PLeq

Rule

All of the following applies:

Examples

TypingRule.PRange

Rule

All of the following applies:

Examples

TypingRule.PMask

Rule

All of the following applies:

Examples

TypingRule.PTupleBadArity

Rule

All of the following applies:

Examples

TypingRule.PTuple

Rule

All of the following applies:

Examples

TypingRule.PTupleConflict

Rule

All of the following applies:

Examples

Typing of Blocks

TypingRule.Block

Rule

annotate_block env return_type s is the result of annotating the statement s in env.

Comments

A local identifier declared with var, let or constant is in scope from the point immediately after its declaration until the end of the immediately enclosing block.

From that follows that we can discard the environment at the end of an enclosing block.

Examples

@asl{ +ASLTypingReference (herdtools7.ASLTypingReference)

ASL Typing Reference

Disclaimer

This material covers both ASLv0 (viz, the existing ASL pseudocode language which appears in the Arm Architecture Reference Manual) and ASLv1, a new, experimental, and as yet unreleased version of ASL.

This material is work in progress, more precisely at pre-Alpha quality as per Arm’s quality standards. In particular, this means that it would be premature to base any production tool development on this material.

However, any feedback, question, query and feature request would be most welcome; those can be sent to Arm’s Architecture Formal Team Lead Jade Alglave <jade.alglave@arm.com> or by raising issues or PRs to the herdtools7 github repository.

Type nomenclature

Singular and Aggregate Types

All types are either singular or aggregate.

TypingDefinition.SingularType

The builtin singular types are:

  • integer;
  • real;
  • string;
  • boolean;
  • bit;
  • bits;
  • enumeration.

TypingDefinition.AggregateType

The builtin aggregate types are:

  • tuple;
  • array;
  • record;
  • exception.

Named and Anonymous Types

Definitions

All types are either:

  • named types: those which are declared using the type syntax;
  • or anonymous types: those which are not declared using the type syntax.

Comments

A named type is singular if it has the structure of a singular type, otherwise it is aggregate.

Examples

Primitive and Non-primitive types

Definitions

All types are either:

  • primitive types: those which only uses the builtin types;
  • or non-primitive types: those which are named types or which make use of named types.

Examples

Structure of a type

Definition

The structure of a type is the primitive type it is equivalent to such that it can hold the same values.

Examples

type T1 of integer; is the named type T1 whose structure is integer.

type T2 of (integer, T1); is the named type T2 whose structure is (integer, integer). In this example, (integer, T1) is non-primitive since it uses T1.

In this example: var x: T1; the type of x is the named (hence non-primitive) type T1, whose structure is integer.

In this example: var y: integer; the type of y is the anonymous primitive type integer.

In this example: var z: (integer, T1); the type of z is the anonymous non-primitive type `(integer, T1)` whose structure is `(integer, integer)`.

Domain of Values for Types

Definition

The domain of a type is the set of values which storage elements of that type may hold.

Examples

The domain of integer is the infinite set of all integers.

The domain of bits(1) is the set {‘1’, ‘0’}.

The domain of integer {2,16} is the set containing the integers 2 and 16.

The domain of bits({2,16}) is the set containing all two bit and all sixteen bit values.

Typing Rules

Typing a program is typing its main function. Constructively, typing a program requires following its Abstract Syntax Tree and typing each of its components.

Formally, the types of a program are given by applying a set of annotate_<object> functions. Each annotate_<object> function describes how to annotate a specific object, as follows.

  • annotate_expr annotates expressions;
  • annotate_slices annotates slices;
  • annotate_pattern annotates pattern;
  • annotate_local_decl_item annotates local declarations;
  • annotate_lexpr annotates left-hand sides of assignments;
  • annotate_stmt annotates statements;
  • annotate_block annotates blocks;
  • annotate_catcher annotates catchers;
  • annotate_call annotates functions calls;
  • annotate_func annotates functions.

Typing of Expressions

annotate_expr specifies how to annotate an expression e in an environment env. Formally, the result of annotating the expression e in env is t,new_e and one of the following applies:

TypingRule.Lit

Rule

All of the following applies:

  • e is a Literal v;
  • t is the type of v;
  • new_e is e.
Examples

TypingRule.TypedExpr

Rule

All of the following applies:

  • e is a typed expression (e',t');
  • t'',e'' is the result of annotating e' in env;
  • One of the following applies:
  • All of the following applies:
  • t'' is a structural subtype of t' in env;
  • t'' is a domain subtype of t' in env;
  • t is t';
  • new_e is e''.
  • All of the following applies:
  • t'' is a structural subtype of t' in env;
  • t'' is not a domain subtype of t' in env;
  • an execution-time check that the expression evaluates to a value in the domain of the required type is required.
  • All of the following applies:
  • t'' is not a structural subtype of t' in env;
  • a "ConflictingTypes" error is raised.
Examples

TypingRule.ELocalVarConstant

Rule

All of the following applies:

  • e is a variable x;
  • x maps to a type ty in the storage_types of the local environment given by env;
  • x maps to a local constant v;
  • t is ty;
  • new_e is the Literal v.
Examples

TypingRule.ELocalVar

Rule

All of the following applies:

  • e is a variable x;
  • x maps to a type ty in the storage_types of the local environment given by env;
  • x does not map to a local constant;
  • t is ty;
  • new_e is e.
Examples

TypingRule.EGlobalVarConstantVal

Rule

All of the following applies:

  • e is a variable x;
  • x maps to a type ty in the constant_values of the global environment given by env;
  • x maps to a global constant;
  • x maps to a value v;
  • t is ty;
  • new_e is E_Literal v.
Examples

TypingRule.EGlobalVar

Rule

All of the following applies:

  • e is a variable x;
  • x maps to a type ty in the constant_values of the global environment given by env;
  • x does not map to a global constant;
  • t is ty;
  • new_e is e.
Examples

TypingRule.EUndefIdent

Rule

All of the following applies:

  • e is a variable x;
  • x is not bound in env;
  • an error "Undefined Identifier" is raised.
Examples

TypingRule.Binop

Rule

All of the following applies:

  • e denotes a binary operation op over two expressions e1 and e2;
  • t1,e1' is the result of annotating e1 in env;
  • t2,e2' is the result of annotating e2 in env;
  • t is the result of checking compatibility of op with t1 and t2;
  • new_e denotes op over e1' and e2'.
Examples

TypingRule.Unop

Rule

All of the following applies:

  • e denotes a unary operation op over an expression e';
  • t'',e'' is the result of annotating e' in env;
  • t is the result of checking compatibility of op with t'';
  • new_e denotes op over e''.
Examples

TypingRule.ECond

Rule

All of the following applies:

  • e denotes a condition e_cond with two options e_true and e_false;
  • t_cond, e'_cond is the result of annotating e_cond in env;
  • t_true, e'_true is the result of annotating e_true in env;
  • t_false, e'_false is the result of annotating e_false in env;
  • One of the following applies:
  • All of the following applies:
  • t is the lowest common ancestor of t_true and t_false;
  • new_e is the condition e'_cond with two options e'_true and e'_false.
  • All of the following applies:
  • there is no lowest common ancestor of t_true and t_false;
  • an error "Unreconciliable Types" is raised.
Examples

TypingRule.ETuple

Rule

All of the following applies:

  • e denotes a tuple li;
  • ts, es is the result of annotating in env each expression in li;
  • t is ts;
  • new_e is es.
Examples

TypingRule.EConcatEmpty

Rule

All of the following applies:

  • e denotes the empty concatenation;
  • t is bits(0);
  • new_e is e.
Examples

TypingRule.EConcat

Rule

All of the following applies:

  • e denotes the concatenation of a non-empty list of expressions li;
  • ts, es is the result of annotating li in env;
  • w is the sum of the widths of the bitvector types ts;
  • t is bits(w);
  • new_e is es.
Examples

TypingRule.ERecordNotARecord

Rule

All of the following applies:

  • e denotes the record expression of type ty with fields fields;
  • ty is neither a record nor an exception type;
  • an error "Conflicting Types" is raised.
Examples

TypingRule.ERecordMissingField

Rule

All of the following applies:

  • e denotes the record expression of type ty with fields fields;
  • ty is the name of a record type with fields field_types;
  • one field in field_types is not initialised by fields;
  • an error "Bad Fields" is raised.
Examples

TypingRule.ERecord

Rule

All of the following applies:

  • e denotes the record expression of type ty with fields fields;
  • ty is the name of a record type with fields field_types;
  • For each field named name associated with the expression e' in field_types, all of the following applies:
  • t',e'' is the result of annotating e' in env;
  • t_spec' is the type associated to name in field_types;
  • t' type-satisfies t_spec';
  • fields' associates name to e'';
  • t is ty;
  • new_e is the record expression of type ty with fields fields'.
Examples

TypingRule.ECall

Rule

All of the following applies:

  • e denotes a call to a function named name with arguments args and parameters eqs;
  • name', args', eqs', ty is the result of annotating the call of that function in env;
  • t is ty;
  • new_e is the call the function named name' with arguments args' and parameters eqs'.
Examples

TypingRule.EUnknown

Rule

All of the following applies:

  • e denotes an unknown expression of type ty;
  • ty' is the structure of ty in env;
  • t is ty;
  • new_e is an unknown expression of type ty'.
Examples

TypingRule.ESlice

Rule

All of the following applies:

  • e denotes the slicing of expression e' by the slices slices;
  • t_e',e' is the result of annotating the expression e' in env;
  • t_e' has the structure of an integer or a bitvector;
  • w is the width of slices;
  • slices' is the result of annotating slices in env;
  • t is the bitvector type of width w;
  • new_e is the slicing of expression e' by the slices slices'.
Examples

TypingRule.EGetArray

Rule

All of the following applies:

  • e denotes the slicing of expression e' by the slices slices;
  • t_e',e' is the result of annotating the expression e' in env;
  • t_e' has the structure of an array of size size and type t;
  • One of the following applies:
  • wanted_t_index is an enumeration type of name size;
  • wanted_t_index is the type integer {0..size-1};
  • slices is a single expression e_index;
  • t_index', e_index' is the result of annotating e_index in env;
  • t_index' type-satisfies wanted_t_index;
  • new_e is an access to array e' at index e_index'.
Examples

TypingRule.EGetRecordField

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is an Exception or a Record type with fields fields;
  • field_name is declared in fields;
  • t is the type corresponding to field_name in fields;
  • new_e is the access of field field_name on expression e2.
Examples

TypingRule.EGetBadRecordField

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is an Exception or a Record type with fields fields;
  • field_name is not declared in fields;
  • an error "Bad Field" is raised.
Examples

TypingRule.EGetBadBitField

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is a bitvector type with bitfields bitfields;
  • field_name is not declared in bitfields;
  • an error "Bad Field" is raised.
Examples

TypingRule.EGetBadField

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e1 does not have the structure of a record or an exception or a bitvector type;
  • an error "Conflicting Types" is raised.
Examples

TypingRule.EGetBitField

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is a bitvector type with bitfields bitfields;
  • field_name is declared in bitfields;
  • slices gives the slices corresponding to the bitfield field_name in bitfields;
  • e3 denotes the slicing of the expression e2 by the slices slices;
  • t,new_e is the result of annotating e3.
Examples

TypingRule.EGetBitFieldNested

Rule

All of the following applies:

  • e denotes the access of field field_name on expression e1;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is a bitvector type with bitfields bitfields;
  • field_name is declared in bitfields;
  • slices gives the slices corresponding to the bitfield field_name in bitfields;
  • e3 denotes the slicing of the expression e2 by the slices slices;
  • t4, e4 is the result of annotating e3 in env;
  • bitfields' gives the bitfields corresponding to the bitfield field_name in bitfields;
  • t is the bitvector type with the width of t4 and the bitfields bitfields'
  • new_e is e4.
Examples

TypingRule.EGetBitFieldTyped

Rule

All of the following applies:

  • e denotes e1, field_name;
  • t_e1, e2 is the result of annotating e1 in env;
  • t_e2 is the anonymous type corresponding to t_e1 in env;
  • t_e2 is a bitvector type with bitfields bitfields;
  • field_name is declared in bitfields;
  • slices gives the slices corresponding to the bitfield field_name in bitfields;
  • t_e3,e3 is the result of annotating e2,slices in env;
  • t gives the type corresponding to the bitfield field_name in bitfields;
  • t_e3 type-satisfies t in env;
  • new_e is e3.
Examples

TypingRule.EGetBitFields

Rule

<description>

Examples

<minimal example>

TypingRule.EPattern

Rule

All of the following applies:

  • e denotes whether the expression e' matches patterns;
  • t_e', e'' is the result of annotating e' in env;
  • patterns' is the result of annotating patterns in env;
  • t is boolean;
  • new_e denotes whether the expression e'' matches patterns'.
Examples

Typing of Left-Hand-Side Expressions

annotate_lexpr version env le t_e is new_le and one of the following applies:

TypingRule.LEIgnore

Rule

All of the following applies:

  • le denotes an expression which can be ignored;
  • new_le is le.
Examples

TypingRule.LELocalVar

Rule

All of the following applies:

  • le denotes a local variable x of type ty;
  • x is locally declared as a variable of type ty in env;
  • new_le is le.
Examples

TypingRule.LEGlobalVar

Rule
Examples

TypingRule.LETuple

Rule

All of the following applies:

  • le denotes a tuple les;
  • t_e denotes a tuple type sub_tys;
  • One of the following applies:
  • All of the following applies:
  • les and sub_tys have the same length;
  • new_le is the result of annotating les with sub_tys in env
  • All of the following applies:
  • les and sub_tys do not have the same length;
  • an error "Bad Arity Tuple Unpacking" is raised.
Examples

TypingRule.LESlice

Rule

All of the following applies:

  • le denotes the slicing of a left-hand-side expression le1 by the slices slices;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • t_le1 has the structure of a bitvector type;
  • le2 is the result of annotating le1 in env;
  • width is the width of the slices slices in env;
  • t is the bitvector type of width width;
  • slices2 is the result of annotating slices in env;
  • new_le is the slicing of le2 by slices2.
Examples

TypingRule.LESetArray

Rule

All of the following applies:

  • le denotes the slicing of a left-hand-side expression le1 by the slices slices;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • t_le1 has the structure of an array type of size size and item type t;
  • le2 is the result of annotating le1 in env;
  • One of the following applies:
  • wanted_t_index is an enumeration type of name size;
  • wanted_t_index is the type integer {0..size-1};
  • slices is a single expression e_index;
  • t_index', e_index' is the result of annotating e_index in env;
  • t_index' type-satisfies wanted_t_index;
  • new_le is an access to array le2 at index e_index'.
Examples

TypingRule.LESetBadRecordField

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of an exception or a record type with fields fields;
  • field is not declared in fields;
  • an error "Bad Field" is raised.
Examples

TypingRule.LESetRecordField

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of an exception or a record type with fields fields;
  • field is bound to type t in fields;
  • t_e type-satisfies t;
  • new_le is the access to the field field in le2.
Examples

TypingRule.LESetBadBitField

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of a bitvector with bitfields bitfields;
  • field is not declared in bitfields;
  • an error "Bad Field" is raised.
Examples

TypingRule.LESetBitField

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of a bitvector with bitfields bitfields;
  • field is declared in bitfields;
  • slices gives the slices corresponding to the bitfield field in bitfields;
  • w is the width of slices;
  • t is the bitvector type of width w;
  • t_e type-satisfies t;
  • le2 is the slicing of le1 by slices;
  • new_le is the result of annotating le2 in env.
Examples

TypingRule.LESetBitFieldNested

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of a bitvector with bitfields bitfields;
  • slices gives the slices corresponding to the bitfield field in bitfields;
  • w is the width of slices;
  • bitfields' gives the bitfields corresponding to field in bitfields;
  • t is the bitvector type of width w and bitfields bitfields';
  • t_e type-satisfies t;
  • le2 is the slicing of le1 by slices;
  • new_le is the result of annotating le2 in env.
Examples

TypingRule.LESetBitFieldTyped

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 has the structure of a bitvector with bitfields bitfields;
  • slices gives the slices corresponding to the bitfield field in bitfields;
  • w is the width of slices;
  • t' is the bitvector type of width w;
  • t gives the type corresponding to the bitfield field in bitfields;
  • t' type-satisfies t;
  • t_e type-satisfies t;
  • le2 is the slicing of le1 by slices;
  • new_le is the result of annotating le2 in env.
Examples

TypingRule.LESetBadField

Rule

All of the following applies:

  • le denotes the access to the field named field in le1;
  • t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;
  • le2 is the result of annotating le1 in env;
  • t_le1 does not have the structure of a record, or an exception or a bitvector type;
  • an error "Conflicting Types" is raised.
Examples

TypingRule.LESetFields

Rule
Examples

TypingRule.LEConcat

Rule
Examples

Typing of Local Declarations

annotate_local_decl_item loc env ty ldk ldi is new_env, new_ldi and one of the following applies:

TypingRule.LDIgnoreNone

Rule

All of the following applies:

  • ldi is a local declaration which can be ignored;
  • no type is given;
  • new_env is env;
  • new_ldi is ldi.
Examples

TypingRule.LDIgnoreSome

Rule

All of the following applies:

  • ldi is a local declaration which can be ignored;
  • a type t is given;
  • One of the following applies:
  • All of the following applies:
  • t can be initialised with ty in env;
  • new_env is env;
  • new_ldi is ldi.
  • All of the following applies:
  • t cannot be initialised with ty in env;
  • an error "Conflicting Types" is raised.
Examples

TypingRule.LDVar

Rule

All of the following applies:

  • ldi denotes a variable x with an optional type ty_opt;
  • x is not declared in env;
  • One of the following applies:
  • All of the following applies:
  • ty_opt is None;
  • t is ty
  • All of the following applies:
  • ty_opt is Some t;
  • t can be initialized with ty in env;
  • new_env is env modified so that x is locally declared of type t;
  • new_ldi is the declaration of variable x with type t.
Examples

TypingRule.LDUninitialisedTypedTuple

Rule

All of the following applies:

  • ldi denotes a singleton list ld;
  • new_env, new_ldi is the result of annotating the local declaration ld with ty in env.
Examples

TypingRule.LDTuple

Rule
Examples

TypingRule.LDTypedTuple

Rule
Examples

Typing of Statements

annotate_stmt env s is a statement new_s and an environment new_env and one of the following applies:

TypingRule.SPass

Rule

All of the following applies:

  • s is a pass statement;
  • new_s is s;
  • new_env is env.
Examples

TypingRule.SThen

Rule

All of the following applies:

  • s is a then statement over two statements s1 and s2;
  • new_s1, env1 is the result of annotating s1 in env;
  • new_s2, env2 is the result of annotating s2 in env1;
  • new_s is a then statement over two statements new_s1 and new_s2;
  • new_env is env2.
Examples

TypingRule.SAssign

Rule

All of the following applies:

  • s is an assignment le = re under language version ver;
  • t_e, e1 is the result of annotating e in env;
  • reduced is the result of potential result of inlining a setter call in le;
  • One of the following applies:
  • All of the following applies:
  • reduced gives a statement s;
  • new_s is s;
  • new_env is env.
  • All of the following applies:
  • reduced does not give a statement s;
  • One of the following applies:
  • All of the following applies:
  • ver is ASLv1;
  • env1 is env;
  • All of the following applies:
  • ver is ASLv0;
  • env1 is the result of annotating undeclared variables by using the first assignments to such variables as declarations;
  • le1 is the result of annotating le in env1;
  • new_s is the assignment le1 = e1;
  • new_env is env1.
Examples

TypingRule.SCall

Rule

All of the following applies:

  • s is a call to a function named name with arguments args and parameters eqs;
  • new_name, new_args, new_eqs is the result of annotating the call to the procedure name with arguments args and parameters eqs;
  • new_s is the call to a function named new_name with arguments new_args and parameters new_eqs;
  • new_env is env.
Examples

TypingRule.SReturnNone

Rule

All of the following applies:

  • s is a return statement with no value and no return type;
  • new_s is a return statement with no value;
  • the enclosing function does not have a return type (it is either a setter or a procedure);
  • new_env is env.
Examples

TypingRule.SReturnOne

Rule

All of the following applies:

  • One of the following applies:
  • All of the following applies:
  • s is a return statement with some value;
  • the enclosing function does not have a return type;
  • All of the following applies:
  • s is a return statement with no value;
  • the enclosing function has a return type;
  • An error "Bad Return Statement" is raised.
Examples

TypingRule.SReturnSome

Rule

All of the following applies:

  • s is a return statement with some value e;
  • the enclosing function has a return type t;
  • t_e',e' is the result of annotating e in env;
  • t_e' type-satisfies t;
  • new_s is a return statement with value e';
  • new_env is env.
Examples

TypingRule.SCond

Rule

All of the following applies:

  • s is a condition e with two statements s1 and s2;
  • t_cond, e_cond is the result of annotating e in env;
  • t_cond type-satisfies t_bool;
  • s1' is the result of annotating s1 in env;
  • s2' is the result of annotating s2 in env;
  • new_s is the condition e_cond with two statements s1' and s2';
  • new_env is env.
Examples

TypingRule.SCase

Rule

All of the following applies:

  • s is a case statement with expression e and cases cases;
  • t_e, e1 is the result of annotating e in env;
  • cases1, env1 is the result of annotating each case in cases;
  • new_s is a case statement with expression e1 and cases cases1;
  • new_env is env1.
Examples

TypingRule.SAssert

Rule

All of the following applies:

  • s is an assert statement with expression e;
  • t_e',e' is the result of annotating e in env;
  • t_e' type-satisfies t_bool;
  • new_s is an assert statement with expression e';
  • new_env is env.
Examples

TypingRule.SWhile

Rule

All of the following applies:

  • s is a while statement with expression e1 and statement s1;
  • t, e2 is the result of annotating e1 in env;
  • t type-satisfies t_bool;
  • s2 is the result of annotating s1 in env;
  • new_s is a while statement with expression e2 and statement s2;
  • new_env is env.
Examples

TypingRule.SRepeat

Rule

All of the following applies:

  • s is a repeat statement with expression e1 and statement s1;
  • s2 is the result of annotating s1 in env;
  • t, e2 is the result of annotating e1 in env;
  • t type-satisfies t_bool;
  • new_s is a repeat statement with expression e2 and statement s2;
  • new_env is env.
Examples

TypingRule.SFor

Rule

All of the following applies:

  • s is a for statement with index id, direction dir, two expressions e1 and e2 and a statement s';
  • t1,e1' is the result of annotating e1 in env;
  • t2,e2' is the result of annotating e2 in env;
  • t1 has the structure of an integer type;
  • t2 has the structure of an integer type;
  • ty is ;
  • s'' is the result of annotating s' in env;
  • new_s is a for statement with index id, direction dir, two expressions e1' and e2' and statement s'';
  • new_env is env.
Examples

TypingRule.SDeclSome

Rule

All of the following applies:

  • s is a declaration with ldk, ldi and an expression e;
  • t_e,e' is the result of annotating e in env;
  • env', ldi' is the result of declaring the local identifiers of ldi in env;
  • new_s is a declaration with ldk, ldi' and an expression e';
  • new_env is env'.
Examples

TypingRule.SDeclNone

Rule

All of the following applies:

  • s is a declaration statement with ldk, ldi and no initial expression;
  • env', s' is the result of annotating uninitialised local declarations ldi in env;
  • new_s is s';
  • new_env is env'.
Examples

TypingRule.SThrowNone

Rule

All of the following applies:

  • s is a throw statement with no expression;
  • new_s is s;
  • new_env is env.
Examples

TypingRule.SThrowSome

Rule

All of the following applies:

  • s is a throw statement with expression e;
  • t_e,e' is the result of annotating e in env;
  • t_e has the structure of an exception type;
  • new_s is a throw statement with expression e' and type t_e;
  • new_env is env.
Examples

TypingRule.STry

Rule

All of the following applies:

  • s is a try statement with statement s', catchers catchers and block otherwise;
  • s'' is the result of annotating s' in env;
  • otherwise' is the result of annotating otherwise in env;
  • catchers' is the result of annotating catchers in env;
  • new_s is a try statement with statement s'', catchers catchers' and block otherwise';
  • new_env is env.
Examples

Typing of Slices

annotate_slices env slices is the pair (offset, length) and one of the following applies:

TypingRule.SliceLength

Rule

All of the following applies:

  • slices gives offset and length;
  • t_offset, offset' is the result of annotating offset in env;
  • t_length, length' is the result of annotating length in env;
  • t_offset has the structure of an integer type;
  • t_length has the structure of an integer type;
  • length is pure.
Examples

TypingRule.SliceSingle

Rule

All of the following applies:

  • slices gives an index i;
  • (offset, length) is the result of applying TypingRule.SliceLength to i, i+:1.
Comments

R_GXKG: The notation bi is syntactic sugar for bi +: 1.

Examples

TypingRule.SliceRange

Rule

All of the following applies:

  • slices gives a range (j, i);
  • pre_length is i +: j-i+1;
  • offset, length is the result of applying TypingRule.SliceLength to i,pre_length.
Comments

R_GXKG: The notation bj:i is syntactic sugar for bi +: j-i+1.

Examples

TypingRule.SliceStar

Rule

All of the following applies:

  • slices gives (factor, pre_length);
  • pre_offset is factor * pre_length;
  • offset, length is the result of applying TypingRule.SliceLength to (pre_offset, pre_length).
Comments

R_GXQG: The notation bi *: n is syntactic sugar for bi*n +: n

Examples

Typing of Patterns

annotate_pattern loc env t p is new_p and one of the following applies:

TypingRule.PAll

Rule

All of the following applies:

  • p is the pattern matching everything;
  • new_p is p.
Examples

TypingRule.PAny

Rule

All of the following applies:

  • p is the pattern which matches anything in a list li;
  • new_li is the result of mapping the result of annotating p in env onto li;
  • new_p is the pattern which matches anything in new_li.
Examples

TypingRule.PNot

Rule

All of the following applies:

  • p is the pattern which matches the negation of a pattern q;
  • new_q is the result of annotating q in env;
  • new_p is pattern which matches the negation of new_q.
Examples

TypingRule.PSingle

Rule
Examples

TypingRule.PGeq

Rule

All of the following applies:

  • p is the pattern which matches anything greater than or equal to an expression e;
  • t_e, e' is the result of annotating e in env;
  • e' is a compile-time constant;
  • t has the structure of an integer;
  • t_e has the structure of an integer;
  • new_p is the pattern which matches anything greater than or equal to e'.
Examples

TypingRule.PLeq

Rule

All of the following applies:

  • p is the pattern which matches anything lesser than or equal to an expression e;
  • t_e, e' is the result of annotating e in env;
  • e' is a compile-time constant;
  • t has the structure of an integer;
  • t_e has the structure of an integer;
  • new_p is the pattern which matches anything lesser than or equal to e'.
Examples

TypingRule.PRange

Rule

All of the following applies:

  • p is the pattern which matches anything within the range given by expressions e1 and e2;
  • t_e1, e1' is the result of annotating e1 in env;
  • t_e2, e2' is the result of annotating e2 in env;
  • t has the structure of an integer;
  • t_e1 has the structure of an integer;
  • t_e2 has the structure of an integer;
  • e1' and e2' are compile-time constants;
  • new_p is the pattern which matches anything within the range given by expressions e1' and e2'.
Examples

TypingRule.PMask

Rule

All of the following applies:

  • p is the pattern which matches a mask m;
  • t has the structure of a bitvector type;
  • n is the length of mask m;
  • t_m is the bitvector type of width n;
  • t type-satisfies t_m;
  • new_p is p.
Examples

TypingRule.PTupleBadArity

Rule

All of the following applies:

  • p is the pattern which matches a tuple li;
  • t has the type structure of a tuple type ts;
  • ts is a list of different size to the size of li;
  • an error "Bad Arity" is raised.
Examples

TypingRule.PTuple

Rule

All of the following applies:

  • p is the pattern which matches a tuple li;
  • t_struct is the type structure of t;
  • t_struct is a tuple ts;
  • ts is a list of same size to the size of li;
  • new_li is the result of annotating li with ts;
  • new_p is the pattern which matches the tuple new_li.
Examples

TypingRule.PTupleConflict

Rule

All of the following applies:

  • p is the pattern which matches a tuple li;
  • t_struct is the type structure of t;
  • t_struct is not a tuple type;
  • an error "Conflicting Types" is raised.
Examples

Typing of Blocks

TypingRule.Block

Rule

annotate_block env return_type s is the result of annotating the statement s in env.

Comments

A local identifier declared with var, let or constant is in scope from the point immediately after its declaration until the end of the immediately enclosing block.

From that follows that we can discard the environment at the end of an enclosing block.

Examples

@asl{ func main () => integer begin if UNKNOWN: boolean then