Annotated King Reference Manual/Types

This page is work in progress.

Type Declarations edit

Some general principles:

  • All scalar subtypes have a default value. For bounded numeric and enumeration subtypes, this is the 'First of the subtype, unless a different value is specified with the Default_Value aspect. For unbounded numeric subtypes, the Default_Value aspect must be specified. Note that an unbounded numeric type can have bounded subtypes.
  • The Predicate aspect may be specified for all subtypes.
  • All scalar types have the attributes 'Image, 'Value, 'Min, 'Max, 'Previous, and 'Next.
  • Integer and enumeration types have the attributes 'Position, 'Value (integer), 'Representation, and 'From_Representation. For integer types, 'Position and 'Representation both give the value of the parameter, and 'Value (integer) and 'From_Representation give the value of the type with the value of the parameter (if that exists); this is similar to 'Pos and "Val for integer types in Ada.
  • 'Image <=>, 'Value (string) are inverses of each other, as are 'Position <=> 'Value (integer)

Syntax edit

type_declaration ::= full_type_declaration | hidden_type_declaration

full_type_declaration ::=
          type defining_identifier [known_discriminant_part] is type_definition
             [aspect_specification];

hidden_type_declaration ::=
          type defining_identifier [discriminant_part] is hidden
             [aspect_specification];

discriminant_part ::= unknown_discriminant_part | known_discriminant_part

unknown_discriminant_part ::= (<>)

known_discriminant_part ::= (discriminant_specification {; discriminant_specification})

discriminant_specification ::=
          defining_identifier : subtype_mark [<- default_expression]  

type_definition ::=
            enumeration_type_definition
          | integer_type_definition
          | real_type_definition
          | map_type_definition
          | sequence_type_definition
          | set_type_definition
          | record_type_definition
          | derived_type_definition
          | module_type_definition
          | task_type_definition

Rationale edit

-

Discussion edit

-

Enumeration Types edit

Examples edit

type Suit is (Spade, Club, Heart, Diamond);

type Philosopher_ID is (Archimedes, Descartes, Hegel, Kant, Socrates);

Syntax edit

enumeration_type_definition ::=
         (enumeration_literal_specification {, enumeration_literal_specification})

enumeration_literal_specification ::= defining_identifier | defining_character_literal

Operators edit

= /= < <= > >=

Attributes edit

First, Last, Position, From_Representation, Representation, Image, Value, Min, Max, Previous, Next

Aspects edit

Bit_Size, Byte_Size

Object declaration edit

My_Card : Suit;

Rationale edit

-

Discussion edit

-

Integer Types edit

Examples edit

Bounded integer types edit

type Day is range 1 .. 31;

Unbounded integer types edit

type Factorial is range <> with Default_Value => 0;

Syntax edit

integer_type_definition ::= bounded_integer_type_definition | unbounded_integer_type_definition

bounded_integer_type_definition ::= range static_simple_expression .. static_simple_expression

unbounded_integer_type_definition ::= range <>

Operators edit

+ - * / rem mod ^ = /= < <= > >= and or xor not

Attributes edit

First, Last, Bit_Wise_Operators, Image, Value, Min, Max, Previous, Next, Valid

Additional attributes with Bit_Wise_Operators = True:

Shift_Left, Shift_Right, Rotate_Left, Rotate_Right, Mod

Aspects edit

Default_Value, Predicate, Signed_Representation, Overflow_Checking

Object declaration edit

N : Factorial;

Rationale edit

Bit-wise operations are available for the base type of all bounded integer types that fit in a single hardware integer.

Discussion edit

-

Real Types edit

Syntax edit

real_type_definition ::= floating_point_definition | fixed_point_definition

Floating Point Types edit

Examples edit

Bounded floating-Point Types edit
type Risk is digits 7 range 0 .. 1;
Unbounded floating-Point Types edit
type Rational is digits <> with Default_Value => 0;

Syntax edit

floating_point_definition ::=
          bounded_floating_point_definition | unbounded_floating_point_definition

bounded_floating_point_definition ::= digits static_expression [real_range_specification]

real_range_specification ::= range static_simple_expression .. static_simple_expression

unbounded_floating_point_definition ::= digits <>

Operators edit

+ - * / ^ = /= < <= > >=

Attributes edit

Image, Value, Min, Max, Previous, Next, Valid, digits

Aspects edit

Default_Value, Predicate

Object declaration edit

Speed : Rational;

Rationale edit

-

Discussion edit

-

Fixed Point Types edit

Examples edit

Bounded fixed-Point Types edit
type Angle is delta 0.01 range -3.14 .. 3.14;
Unbounded fixed-Point Types edit
type Duration is delta 10.0 ^ -9 range <> with Default_Value => 0;

Syntax edit

fixed_point_definition ::= bounded_fixed_point_definition | unbounded_fixed_point_definition

bounded_fixed_point_definition ::= delta static_expression real_range_specification

unbounded_fixed_point_definition ::= delta static_expression range <>

Operators edit

+ - * / ^ = /= < <= > >=

Attributes edit

Image, Value, Min, Max, Previous, Next, Valid, delta

Aspects edit

Default_Value, Predicate

Object declaration edit

Bearing : Angle;

Rationale edit

Shouldn't decimal types be available, in order to cover the corresponding available type of Ada?

A King fixed-point type with a delta that is a power of 10 is equivalent to an Ada decimal fixed-point type.

type Money is delta 0.01 digits 14;

The above would be equivalent to:

type Money is delta 0.01 range -999_999_999_999.99 .. 999_999_999_999.99;

Discussion edit

-

Map Types edit

Examples edit

type Store is map Part_Key => Stock_Info;

Syntax edit

map_type_definition := map key_subtype_mark => value_subtype_mark

Operators edit

= /=

"=" is only defined if it is defined for the value subtype.

Attributes edit

-

Operations edit

Delete, Clear, Defined, Size

Aspects edit

-

Object declaration edit

My_Store : Store;

Component deference edit

My_Store (K99)

Aggregates edit

Store'(K1 => SI1, KE => SIE)

Store'(null) -- Empty map

Iteration edit

for K in My_Store'range

for E of My_Store

Rationale edit

Maps may also be implemented by functions, so King uses a common notation for both.

Discussion edit

-

Sequence Types edit

Examples edit

type Stack is sequence of Message;

Syntax edit

sequence_type_definition := sequence of element_subtype_mark

Operators edit

= /= &

"=" is only defined if it is defined for the value subtype.

Attributes edit

-

Operations edit

Delete, Clear, Length

Aspects edit

-

Object declaration edit

My_Stack : Stack;

Component deference edit

My_Stack [Curent]

Aggregates edit

My_Stack'[MC, ML, MZ]

My_Stack'[null] -- Empty sequence

Iteration edit

for P in [reverse] My_Stack'range

for E of [reverse] My_Stack

Rationale edit

-

Discussion edit

-

Set Types edit

Examples edit

type File_Mask is set of File_Mode;

Syntax edit

set_type_definition := set of element_subtype_mark

Operators edit

+ - * / = /= < <= > >= [not] in

Attributes edit

-

Operations edit

Size

Aspects edit

-

Object declaration edit

My_Mask : File_Mask:

Component deference edit

-

Aggregates edit

My_Mask'{Read, Exec}

My_Mask'{null} -- Empty set

My_Mask'{all} -- Full set

Iteration edit

for M of My_Mask

Rationale edit

-

Discussion edit

-

Record Types edit

Examples edit

type Complex is record
   Re : Float;
   Im : Float;
end record Complex;

Syntax edit

record_type_definition ::= record_definition

record_definition ::=
           record
              component_list
           end record record_identifier

component_list ::=
            component_item {component_item}
          | {component_item} variant_part
          | null;

component_item ::= component_declaration

component_declaration ::= defining_identifier : component_definition [<- default_expression]
                          [aspect_specification];

component_definition ::= subtype_indication

variant_part ::= case discriminant_direct_name is
                   variant
                   {variant}
                 end case;

variant ::= when discrete_choice_list =>
               component_list

discrete_choice_list ::= discrete_choice {| discrete_choice}

discrete_choice ::= choice_expression | discrete_subtype_indication | range_specification | others

Operators edit

= /=

Attributes edit

-

Aspects edit

-

Object declaration edit

Z : Complex;

Component deference edit

Z.Re

Rationale edit

-

Discussion edit

-

Derived Types edit

Examples edit

type Boxes (Length : Position_Value) is record
   Box_A : Receive_Box (Max_Length => Length);
   Box_B : Receive_Box (Max_Length => Length);
end record;
type Boxes_4 is new Boxes (Length => 4);

Syntax edit

derived_type_definition ::= new parent_subtype_indication

Operators edit

-

Attributes edit

-

Aspects edit

-

Rationale edit

The operations, attributes, and so on are based on the parent type.

Discussion edit

-

Module Types edit

Examples edit

type Strings is module
   Set : procedure (S : String);
   Index : function (Pattern : String; Going : Direction <- Forward) return Position_Value;
   Head : function (Count : Natural; Pad : Unicode <- Space) return String;
   -- ...
end module Strings;

Syntax edit

module_type_definition ::= module
                              subprogram_declaration {subprogram_declaration}
                           end module module_identifier

Operators edit

-

Attributes edit

-

Aspects edit

-

Rationale edit

-

Discussion edit

-

Active Task Types edit

Examples edit

type Philosopher (ID : Philosopher_ID <- Archimedes) is task;

Syntax edit

task_type_definition ::= task

Operators edit

= /=

Attributes edit

-

Aspects edit

-

Object declaration edit

T1 : Philosopher;

Rationale edit

-

Discussion edit

-

Passive Task Types edit

Examples edit

type Semaphore is task
   Secure : procedure;
   Release : procedure;
end task Semaphore;

Syntax edit

task_type_definition ::= task
                            subprogram_declaration {subprogram_declaration}
                         end task task_identifier

Operators edit

= /=

Attributes edit

-

Aspects edit

-

Object declaration edit

S1 : Semaphore;

Rationale edit

Passive tasks are the only way that active tasks may communicate.

Discussion edit

-