Skip to content

Commit

Permalink
Merge branch 'topic/1046' into 'master'
Browse files Browse the repository at this point in the history
Add support for container aggregates

Closes #1046

See merge request eng/libadalang/libadalang!1366
  • Loading branch information
thvnx committed Oct 2, 2023
2 parents 6f6d86d + b50baa1 commit 2a7252f
Show file tree
Hide file tree
Showing 10 changed files with 1,156 additions and 4 deletions.
142 changes: 138 additions & 4 deletions ada/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -6002,7 +6002,13 @@ def is_view_of_type(comp_view=T.BaseTypeDecl.entity):

@langkit_property(dynamic_vars=[origin], return_type=Bool)
def is_array_or_rec():
return Not(Self.is_null) & (Entity.is_array | Entity.is_record_type)
return And(
Not(Self.is_null),
(Entity.is_array | Entity.is_record_type
# Also consider container aggregates as array or rec
| (origin.is_a(T.BracketAggregate)
& Entity.has_aspect('Aggregate')))
)

@langkit_property(public=True, return_type=Bool)
def is_inherited_primitive(p=T.BasicDecl.entity):
Expand Down Expand Up @@ -10629,7 +10635,7 @@ def xref_equation():
target = Var(Self.parent.parent.parent)
return Cond(
# Iterable aspect
Entity.id.name_is('Iterable'),
Entity.id.name_symbol.any_of('Aggregate', 'Iterable'),
Entity.expr.cast(T.Aggregate).assocs.unpacked_params.logic_all(
lambda sa:
sa.assoc.expr
Expand Down Expand Up @@ -13589,6 +13595,7 @@ def xref_equation():
Self.in_aspect('Global') | Self.in_aspect('Refined_Global')
| Self.in_aspect('Depends') | Self.in_aspect('Refined_Depends')
| Self.in_aspect('Test_Case') | Self.in_aspect('Refined_State')
| Self.in_aspect('Aggregate')
# Careful: normal aggregates can appear inside a contract_cases
# aspect's expression, so we must only special case the direct
# aggregate of that aspect.
Expand Down Expand Up @@ -13819,6 +13826,83 @@ class Aggregate(BaseAggregate):
Aggregate that is not a ``null record`` aggregate (:rmlink:`4.3`).
"""

@langkit_property()
def add_named_param_at(index=T.Int):
"""
Return the ``Add_Named`` subprogram parameter specified by ``index``.
This aggregate must be a container aggregate aspect specification.
"""
# `Add_Named`denotes exactly one procedure that has three parameters,
# the first an in out parameter of the container type, the second an in
# parameter of a nonlimited type (the key type of the container type),
# and the third, an in parameter of a nonlimited type that is called
# the element type of the container type (so index should be an Int
# between 0 and 2).
add_named = Var(
Entity.assocs.find(
lambda assoc: assoc.cast(T.AggregateAssoc).names.at(0)
.cast(T.Name).name_is('Add_Named')
)
)
add_named_params = Var(
add_named.then(
lambda an:
an.expr.cast(T.Name).referenced_decl.subp_spec_or_null.params
)
)

return add_named.then(
lambda _:
add_named_params.at(index).type_expression.designated_type_decl
)

@langkit_property()
def element_type():
"""
Return the element type of that Aggregate. This aggregate must be a
container aggregate aspect specification.
"""
# Position container case: `Add_Unnamed` should be specified. It
# denotes exactly one procedure that has two parameters, the first an
# in out parameter of the container type, and the second an in
# parameter of some nonlimited type, called the element type of the
# container type.
add_unnamed = Var(
Entity.assocs.find(
lambda assoc: assoc.cast(T.AggregateAssoc).names.at(0)
.cast(T.Name).name_is('Add_Unnamed')
)
)
unnamed_element_type = Var(
add_unnamed.then(
lambda au: au.expr.cast(T.Name).referenced_decl
.subp_spec_or_null.params.at(1).type_expression
.designated_type_decl
)
)

# Named container case: `Add_Named` should be specified
named_element_type = Var(Entity.add_named_param_at(2))

return If(
add_unnamed.is_null, named_element_type, unnamed_element_type
)

@langkit_property()
def key_type():
"""
Return the key type of that Aggregate. This aggregate must be a
container aggregate aspect specification.
"""
# Named container case: `Add_Named` should be specified
key_type = Var(Entity.add_named_param_at(1))

return key_type._or(
# If add_named is not specified, key_type is the universal integer
# type used for indexed aggregates.
Entity.universal_int_type
)


class NullRecordAggregate(BaseAggregate):
"""
Expand Down Expand Up @@ -15666,6 +15750,9 @@ def xref_equation():
agg.in_aspect('Contract_Cases'),
Entity.contract_cases_assoc_equation,

agg.is_a(T.BracketAggregate) & td._.has_aspect('Aggregate'),
Entity.container_aggregate_equation(td),

agg.parent.is_a(AspectClause, AspectAssoc, PragmaArgumentAssoc),
LogicTrue(),

Expand All @@ -15674,6 +15761,34 @@ def xref_equation():
Entity.array_assoc_equation(atd, mra)
)

@langkit_property(return_type=Equation, dynamic_vars=[env, origin])
def container_aggregate_equation(td=BaseTypeDecl.entity):
"""
Equation for the case where this is an aggregate assoc for a
container type. This is an Ada 2022 feature (:rmlink:`4.3.5`).
"""
aggregate_aspect = Var(
td.get_aspect('Aggregate').value.cast(T.Aggregate)
)
entity_name = Var(Entity.names._.at(0).cast(T.Name))
element_type = Var(aggregate_aspect.element_type)
key_type = Var(aggregate_aspect.key_type)

return And(
Bind(Entity.expr.expected_type_var, element_type),
Entity.expr.sub_equation,
Entity.expr.matches_expected_type,
If(
entity_name.is_null,
LogicTrue(),
And(
Bind(entity_name.expected_type_var, key_type),
entity_name.as_entity.sub_equation,
entity_name.matches_expected_type
)
)
)

@langkit_property(return_type=Equation, dynamic_vars=[env, origin])
def record_assoc_equation():
"""
Expand Down Expand Up @@ -15907,6 +16022,25 @@ def xref_equation():

array_type_def = Var(type_decl._.array_def)

# The iterated assoc can also be in a container aggregate
container_aggregate = Var(
type_decl.get_aspect('Aggregate').value.cast(T.Aggregate)
)
# Get the "component" type of the array or container
comp_type = Var(
array_type_def.then(
lambda atd: atd.comp_type,
default_val=container_aggregate.element_type
)
)
# Get the index type of the array or container
index_type = Var(
array_type_def.then(
lambda atd: atd.index_type(root_agg.rank),
default_val=container_aggregate.key_type
)
)

# NOTE: we need to resolve the spec first so that the indexing variable
# has a type when resolving `r_expr`.
# NOTE: if the form of the iterated_component_association is
Expand All @@ -15916,7 +16050,7 @@ def xref_equation():
spec_success = Var(Entity.spec.resolve_names_internal_with_eq(
If(Self.spec.loop_type.is_a(IterType.alt_in),
Bind(Entity.spec.iter_expr.cast(Expr).expected_type_var,
array_type_def.index_type(root_agg.rank))
index_type)
& Entity.spec.iter_expr.cast(Expr).matches_expected_type,
LogicTrue())
))
Expand All @@ -15931,7 +16065,7 @@ def xref_equation():

# .. Then we want to match the component type
Entity.expr.sub_equation
& Bind(Entity.expr.expected_type_var, array_type_def.comp_type)
& Bind(Entity.expr.expected_type_var, comp_type)
& Entity.expr.matches_expected_type,

# .. Else we're on an intermediate dimension of a
Expand Down
184 changes: 184 additions & 0 deletions testsuite/tests/name_resolution/container_aggregate/ai12_0212.adb
Original file line number Diff line number Diff line change
@@ -0,0 +1,184 @@
-- Tests derived from the AI12-0212 description

pragma Ada_2022;

with Ada.Containers.Indefinite_Ordered_Maps;
with Ada.Containers.Indefinite_Vectors;
with Ada.Containers.Ordered_Sets;

procedure AI12_0212 is

package P is
-- Set_Type is a set-like container type
type Set_Type is private
with Aggregate => (Empty => Empty_Set,
Add_Unnamed => Include);

function Empty_Set return Set_Type;

subtype Small_Integer is Integer range -1000..1000;

procedure Include (S : in out Set_Type; N : Small_Integer) is null;

-- Map_Type is a map-like container type
type Map_Type is private
with Aggregate => (Empty => Empty_Map,
Add_Named => Add_To_Map);

procedure Add_To_Map (M : in out Map_Type; Key : Integer; Value : String);

Empty_Map : constant Map_Type;

-- Vector_Type is an extensible array-like container type
type Vector_Type is private
with Aggregate => (Empty => Empty_Vector,
Add_Unnamed => Append_One,
New_Indexed => New_Vector,
Assign_Indexed => Assign_Element);

type Count_Type is new Natural;

function Empty_Vector (Capacity : Count_Type := 0) return Vector_Type;

procedure Append_One (V : in out Vector_Type; New_Item : String) is null;

procedure Assign_Element (V : in out Vector_Type; Index : Positive;
Item : String) is null;

function New_Vector (First, Last : Positive) return Vector_Type
with Pre => First = Positive'First;
private

package Int_Sets is
new Ada.Containers.Ordered_Sets
(Element_Type => Small_Integer);
type Set_Type is new Int_Sets.Set with null record;

Empty_S : constant Set_Type :=
(Int_Sets.Empty_Set with null record);

package Int_String_Maps is
new Ada.Containers.Indefinite_Ordered_Maps
(Key_Type => Integer, Element_Type => String);

type Map_Type is new Int_String_Maps.Map with null record;

procedure Add_To_Map (M : in out Map_Type; Key : Integer; Value : String)
renames Insert;

Empty_Map : constant Map_Type :=
(Int_String_Maps.Empty_Map with null record);

package String_Vectors is
new Ada.Containers.Indefinite_Vectors
(Index_Type => Positive, Element_Type => String);

type Vector_Type is new String_Vectors.Vector with null record;

Empty_V : constant Vector_Type :=
(String_Vectors.Empty_Vector with null record);
end P;

package body P is
function Empty_Vector (Capacity : Count_Type := 0) return Vector_Type is
begin
return Empty_V;
end Empty_Vector;

function New_Vector (First, Last : Positive) return Vector_Type is
begin
return Empty_V;
end New_Vector;

function Empty_Set return Set_Type is
begin
return Empty_S;
end Empty_Set;
end P;

use P;

S : Set_Type;
M : Map_Type;
V : Vector_Type;

-- Define a table of pairs
type Pair is record
Key : Integer;
Value : access constant String;
end record;

Table : constant array(Positive range <>) of Pair :=
[(Key => 33, Value => new String'("a nice string")),
(Key => 44, Value => new String'("an even better string"))];

-- Create an image table for an array of integers
Keys : constant array (Positive range <>) of Integer := [2, 3, 5, 7, 11];
begin
-- Example aggregates using Set_Type

-- Assign the empty set to S:
S := [];
pragma Test_Statement;

-- A positional set aggregate
S := [1, 2];
pragma Test_Statement;

-- A set aggregate with an iterated_element_association
S := [for Item in 1 .. 5 => Item * 2];
pragma Test_Statement;

-- A set aggregate consisting of two iterated_element_associations
S := [for Item in 1 .. 5 => Item,
for Item in 1 .. 5 => -Item];
pragma Test_Statement;

-- Example aggregates using Map_Type

-- Create an empty map
M := [];
pragma Test_Statement;

-- A simple named map aggregate
M := [12 => "house", 14 => "beige"];
pragma Test_Statement;

-- A map aggregate using an iterated_element_association
-- and a key expression, built from from a table of key/value pairs:
-- M:= [for P of M use P.Key => P.Value];
-- !!! Can't compile this example with GNAT.

-- A map aggregate where the values produced by the
-- iterated_element_association are of the same type as the key
-- (eliminating the need for a separate key_expression):
-- M:= [for Key of Keys => Integer'Image (Key)];
-- !!! Make GNAT crash.

-- The above could have been written using an explicit key_expression:
-- M:= [for Key of Keys use Key => Integer'Image (Key)];
-- This example is not supported by LAL ([use key_expression] not parsed)
-- TODO: fix LAL, see libadalang#1050.

-- Example aggregates using Vector_Type

-- Create an empty vector aggregate
V := [];
pragma Test_Statement;

-- A positional vector aggregate
V := ["abc", "def"];
pragma Test_Statement;

-- An indexed vector aggregate
V := [1 => "this", 2 => "is", 3 => "a", 4 => "test"];
pragma Test_Statement;

-- A vector of images of dynamic length
V := [for I in 1 .. 5 => Integer'Image (I)];
pragma Test_Statement;

-- A vector made from the elements of a map
-- V:= [for Elem of M => Elem];
-- !!! Can't compile this example with GNAT.
end AI12_0212;
Loading

0 comments on commit 2a7252f

Please sign in to comment.