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
-