Commit d4bc42b8 authored by Maxime Perrotin's avatar Maxime Perrotin

Introduce new generation of iterators

parent b0a70e95
...@@ -47,7 +47,7 @@ package body ASN1_Iterators.Exhaustive_Simulation is ...@@ -47,7 +47,7 @@ package body ASN1_Iterators.Exhaustive_Simulation is
package Loc_Maps is new Ordered_Maps(Key_Type => Hash_Type, package Loc_Maps is new Ordered_Maps(Key_Type => Hash_Type,
Element_Type => Boolean); Element_Type => Boolean);
package Evt_Lists is new Vectors(Element_Type => Event_ty, package Evt_Lists is new Vectors(Element_Type => Event_ty,
Index_Type => Vect_Count); Index_Type => Natural);
package Parent_Maps is new Ordered_Maps(Key_Type => Hash_Type, package Parent_Maps is new Ordered_Maps(Key_Type => Hash_Type,
Element_Type => Edge_ty); Element_Type => Edge_ty);
function Find_Path(From: Hash_Type) return Evt_Lists.Vector is function Find_Path(From: Hash_Type) return Evt_Lists.Vector is
...@@ -69,7 +69,7 @@ package body ASN1_Iterators.Exhaustive_Simulation is ...@@ -69,7 +69,7 @@ package body ASN1_Iterators.Exhaustive_Simulation is
for each_edge of State.Edges loop for each_edge of State.Edges loop
if not Loc_Visited.Contains(each_edge.state) then if not Loc_Visited.Contains(each_edge.state) then
Loc_Q.append(Each_Edge.state); Loc_Q.append(Each_Edge.state);
Loc_Visited.Include(Key => each_edge.state, Loc_Visited.Include(Key => Each_Edge.State,
New_Item => True); New_Item => True);
Parent_Map.Include(Key => Each_Edge.State, Parent_Map.Include(Key => Each_Edge.State,
New_Item => (State => Next_Hash, New_Item => (State => Next_Hash,
......
...@@ -29,9 +29,6 @@ package ASN1_Iterators.Exhaustive_Simulation is ...@@ -29,9 +29,6 @@ package ASN1_Iterators.Exhaustive_Simulation is
backup_hash : Hash_Type; backup_hash : Hash_Type;
start_hash : Hash_Type; start_hash : Hash_Type;
-- Set a maximum size for vectors (set of states and edges)
subtype Vect_Count is Positive range 1 .. 1000000;
-- An edge is made of a past state reference and an event to leave it -- An edge is made of a past state reference and an event to leave it
type Edge_ty is type Edge_ty is
record record
...@@ -40,7 +37,7 @@ package ASN1_Iterators.Exhaustive_Simulation is ...@@ -40,7 +37,7 @@ package ASN1_Iterators.Exhaustive_Simulation is
end record; end record;
package Edges_Pkg is new Vectors (Element_Type => Edge_ty, package Edges_Pkg is new Vectors (Element_Type => Edge_ty,
Index_Type => Vect_Count); Index_Type => Natural);
-- A state is made of a context and a set of edges leading to it -- A state is made of a context and a set of edges leading to it
type Global_State is type Global_State is
...@@ -78,7 +75,7 @@ package ASN1_Iterators.Exhaustive_Simulation is ...@@ -78,7 +75,7 @@ package ASN1_Iterators.Exhaustive_Simulation is
-- Vector of hashes (integers) used for the model checking -- Vector of hashes (integers) used for the model checking
package Lists is new Vectors (Element_Type => Hash_Type, package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count); Index_type => Natural);
package Sets is new Ordered_Sets(Element_Type => Hash_Type); package Sets is new Ordered_Sets(Element_Type => Hash_Type);
......
...@@ -4,6 +4,7 @@ with Ada.Finalization; ...@@ -4,6 +4,7 @@ with Ada.Finalization;
use Ada.Finalization; use Ada.Finalization;
with ASN1_Iterators.Generic_Basic; with ASN1_Iterators.Generic_Basic;
with ASN1_Iterators.SimpleTypes;
generic generic
with package P is new Generic_Basic (<>); with package P is new Generic_Basic (<>);
...@@ -17,6 +18,7 @@ package ASN1_Iterators.Generic_Fixed_SeqOf is ...@@ -17,6 +18,7 @@ package ASN1_Iterators.Generic_Fixed_SeqOf is
type ASN1_SeqOf_Ptr; type ASN1_SeqOf_Ptr;
type ASN1_SeqOf_It; type ASN1_SeqOf_It;
type ASN1_SeqOf (Size: Natural) is new Controlled type ASN1_SeqOf (Size: Natural) is new Controlled
with record with record
Length : Natural := Size; Length : Natural := Size;
......
package body ASN1_Iterators.Generic_Iterator is
procedure Initialize (Self: in out Generic_Iterator_Type) is
begin
Self.Item.Value := ASN1_Iterable.First(ASN1_Iterable.Iterable'Class(Self.Item));
end;
function First (Item : Iterator) return Cursor is
C: constant Cursor := Item.Ptr;
begin
C.Item.Value := ASN1_Iterable.First(ASN1_Iterable.Iterable'Class(Item.Ptr.all.Item));
return C;
end;
function Next (Item : Iterator;
Ptr : Cursor)
return Cursor is
C: constant Cursor := Item.Ptr;
begin
C.Item.Value := ASN1_Iterable.Next(ASN1_Iterable.Iterable'Class(Ptr.all.Item));
return C;
end;
function Iterate (self : Generic_Iterator_Type)
return Iterators.Forward_Iterator'Class is
begin
return I: Iterator do
I.Ptr := self'Unrestricted_Access;
end return;
end;
end;
with Ada.Iterator_Interfaces,
Ada.Finalization,
ASN1_Iterators.Iterable_Type;
use Ada.Finalization;
generic
type ASN1_Type is (<>);
with package ASN1_Iterable is new ASN1_Iterators.Iterable_Type (ASN1_Type);
type Actual_Iterable is new ASN1_Iterable.Iterable with private;
package ASN1_Iterators.Generic_Iterator is
type Generic_Iterator_Type is new Controlled with
record
Item: Actual_Iterable;
end record
with Default_Iterator => Iterate,
Iterator_Element => ASN1_Type,
Constant_Indexing => Element;
type Cursor is access all Generic_Iterator_Type;
function Element (Self : Generic_Iterator_Type;
Ptr : Cursor) return ASN1_Type is (Ptr.Item.Element);
function Has_Element (Ptr : Cursor) return Boolean is
(ASN1_Iterable.Has_Element(ASN1_Iterable.Iterable'Class(Ptr.all.Item)));
package Iterators is new Ada.Iterator_Interfaces (Cursor, Has_Element);
type Iterator is new Iterators.Forward_Iterator with record
Ptr : Cursor;
end record;
overriding
procedure Initialize (Self: in out Generic_Iterator_Type);
overriding
function First (Item : Iterator) return Cursor;
overriding
function Next (Item : Iterator;
Ptr : Cursor)
return Cursor;
function Iterate (self : Generic_Iterator_Type)
return Iterators.Forward_Iterator'Class;
end;
with Interfaces;
use Interfaces;
with ASN1_Iterators.Iterable_Type;
with ASN1_Iterators.Generic_Iterator;
generic
Min, Max: Integer_64;
package ASN1_Iterators.Iterable_Integer is
package Integer_Pkg is new ASN1_Iterators.Iterable_type (Integer_64);
type ASN1_Integer is new Integer_Pkg.Iterable with null record;
overriding
function Has_Element (It: ASN1_Integer) return Boolean is
(It.Value <= Max);
overriding
function First (It: ASN1_Integer) return Integer_64 is
(Min);
overriding
function Next (It: ASN1_Integer) return Integer_64 is
(It.Value + 1);
package Custom_Iterator is new ASN1_Iterators.Generic_Iterator
(ASN1_Type => Integer_64,
ASN1_Iterable => Integer_Pkg,
Actual_Iterable => ASN1_Integer);
subtype Instance is Custom_Iterator.Generic_Iterator_Type;
-- If it is needed to iterate manually, provide Cursor and Iterator:
subtype Cursor is Custom_Iterator.Cursor;
subtype Iterator is Custom_Iterator.Iterators.Forward_Iterator'Class;
function Has_Element (Ptr: Cursor) return Boolean
renames Custom_Iterator.Has_Element;
end;
with ASN1_Iterators.Iterable_Type;
use ASN1_Iterators.Iterable_Type;
generic
Min, Max: Natural;
type Element_Iterable is new ASN1_Iterators.Iterable_type (<>);
package ASN1_Iterators.Iterable_SeqOF is
type DataArray is array(natural range <>) of Element_Iterable;
type Generic_SeqOf (Max: Natural) is record
Length : Natural;
Data : DataArray (1..Max);
end record;
package SeqOf_Pkg is new ASN1_Iterators.Iterable_type (Generic_SeqOf);
type ASN1_SequenceOf is new SeqOf_Pkg.Iterable
with record
Length : Natural := Min;
-- Iterate on the length
-- LenVal : Length_ty.Instance;
-- LenIt : Length_Pkg.Iterator;
-- And on the value
-- RestVal : access P.ASN1_SeqOf;
-- RestIt : access P.ASN1_SeqOf_It;
end record;
overriding
procedure Initialize (It: in out ASN1_SequenceOf);
overriding
function Has_Element (It: ASN1_SequenceOf) return Boolean;
overriding
function First (It: ASN1_SequenceOf) return Generic_SeqOf;
overriding
function Next (It: ASN1_SequenceOf) return Generic_SeqOf;
package Custom_Iterator is new ASN1_Iterators.Generic_Iterator
(ASN1_Type => Generic_SeqOf,
ASN1_Iterable => SeqOf_Pkg,
Actual_Iterable => ASN1_SequenceOf);
subtype SeqOf_Iterator is Custom_Iterator.Generic_Iterator_Type;
end;
with Ada.Finalization;
use Ada.Finalization;
-- Set up a generic type that has a Value field, and member functions
-- Element, Has_Element, First, and Next
generic
type Element_Type is (<>);
package ASN1_Iterators.Iterable_Type is
type Iterable is abstract new Controlled
with record
Value: Element_Type;
end record;
type Iterable_Cursor is access all Iterable;
function Element (It : Iterable) return Element_Type
is (It.Value);
function Has_Element (It: Iterable) return boolean is abstract;
function First (It: Iterable) return Element_Type is abstract;
function Next (It: Iterable) return Element_Type is abstract;
end;
with ASN1_Iterators.Iterable_Integer,
Ada.Text_IO;
use ASN1_Iterators,
Ada.Text_IO;
procedure test_new_iterators is
package MyInt is new ASN1_Iterators.Iterable_Integer (5, 10);
It: MyInt.Instance;
Iter: MyInt.Iterator := It.Iterate;
C: MyInt.Cursor;
begin
Put_Line ("Hello");
Put_Line ("With 'for each of':");
for each of It loop
Put_Line (each'img);
end loop;
Put_Line ("With 'for each in':");
for each in It.Iterate loop
Put_Line (It.Element (each)'Img);
end loop;
-- With manual iterators:
Put_Line ("With manual iterators:");
C := Iter.First;
while MyInt.Has_Element (C) loop
Put_Line (It.Element (C)'Img);
C := Iter.Next (C);
end loop;
end;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment