aboutsummaryrefslogtreecommitdiff
path: root/src/kompsos.ads
diff options
context:
space:
mode:
Diffstat (limited to 'src/kompsos.ads')
-rw-r--r--src/kompsos.ads96
1 files changed, 34 insertions, 62 deletions
diff --git a/src/kompsos.ads b/src/kompsos.ads
index dc9341f..ab50a08 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -8,7 +8,8 @@
private with
- Ada.Containers.Indefinite_Holders,
+ Ada.Containers.Hashed_Maps,
+ Ada.Containers.Vectors,
Ada.Finalization;
@@ -212,16 +213,6 @@ package Kompsos is
-- Auxiliary Helpers --
-------------------------
- -- Infinite State Loops --
-
- function Recurse
- (This : in Goal)
- return Goal;
-
- procedure Recurse
- (This : in out Goal);
-
-
-- Evaluation --
function Run
@@ -393,16 +384,8 @@ package Kompsos is
with Pre => Inputs'Length = 3;
- -- anyo --
- -- Skipped due to Recurse doing the same thing
-
-
- -- nevero --
- -- Skipped since it just creates a failed Goal
-
-
- -- alwayso --
- -- Skipped due to Recurse doing the same thing
+ -- anyo, nevero, alwayso --
+ -- Skipped since these seem to be artifacts of conde, which isn't used here
private
@@ -411,7 +394,7 @@ private
-- Variables --
-- Around 2^31 possible Variables per Goal should be enough for anybody, right?
subtype Long_Natural is Long_Integer range 0 .. Long_Integer'Last;
- subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
+ subtype Long_Positive is Long_Integer range 1 .. Long_Natural'Last;
type Variable is new Long_Natural;
@@ -460,7 +443,7 @@ private
Empty_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);
- package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);
+ type Term_Array_Access is access Term_Array;
-- States --
@@ -470,40 +453,29 @@ private
Value : Term;
end record;
- type Binding_Array is array (Positive range <>) of Binding;
-
- -- Values of 2, 3, 4 here are honestly fairly similar, but of those, 4 seems to work best
- Unroll_Max : constant Integer := 4;
-
- subtype Valid_Count is Integer range 1 .. Unroll_Max;
-
- type State_Component is limited record
- Counter : Natural;
- Valid : Valid_Count;
- Data : Binding_Array (Valid_Count'Range);
- Next : State;
- end record;
-
- type State_Component_Access is access State_Component;
-
- type State_Control is new Ada.Finalization.Controlled with record
- Actual : State_Component_Access := null;
- end record;
-
- overriding procedure Initialize
- (This : in out State_Control);
+ package Binding_Vectors is new Ada.Containers.Vectors
+ (Index_Type => Long_Positive,
+ Element_Type => Binding);
- overriding procedure Adjust
- (This : in out State_Control);
+ function Variable_Index_Hash
+ (Key : in Variable)
+ return Ada.Containers.Hash_Type;
- overriding procedure Finalize
- (This : in out State_Control);
+ package Variable_Index_Maps is new Ada.Containers.Hashed_Maps
+ (Key_Type => Variable,
+ Element_Type => Long_Positive,
+ Hash => Variable_Index_Hash,
+ Equivalent_Keys => "=");
type State is record
- Ctrl : State_Control := (Ada.Finalization.Controlled with Actual => null);
+ Binds : Binding_Vectors.Vector;
+ Refs : Variable_Index_Maps.Map;
end record;
- type State_Access is access State;
+ procedure Insert
+ (This : in out State;
+ Key : in Variable;
+ Value : in Term'Class);
function Lookup
(This : in State;
@@ -511,7 +483,13 @@ private
Value : out Term'Class)
return Boolean;
- Empty_State : constant State := (Ctrl => (Ada.Finalization.Controlled with Actual => null));
+ procedure Truncate
+ (This : in out State;
+ Length : in Long_Natural);
+
+ Empty_State : constant State :=
+ (Binds => Binding_Vectors.Empty_Vector,
+ Refs => Variable_Index_Maps.Empty_Map);
-- Goals --
@@ -544,17 +522,13 @@ private
OInput : Term;
when Many_Arg =>
MFunc : Junction_Many_Func;
- MInput : Term_Array_Holders.Holder;
+ MInput : Term_Array_Access;
end case;
end record;
- package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);
+ type Lazy_Data_Access is access Lazy_Data;
- type Node_Kind is
- (Unify_Node,
- Disjunct_Node,
- Conjunct_Node,
- Recurse_Node);
+ type Node_Kind is (Unify_Node, Disjunct_Node, Conjunct_Node);
type Graph_Component (Kind : Node_Kind) is limited record
Counter : Natural;
@@ -568,9 +542,7 @@ private
Dis_Goal2 : aliased Goal_Graph;
when Conjunct_Node =>
Con_Goal : aliased Goal_Graph;
- Con_Data : Lazy_Holders.Holder;
- when Recurse_Node =>
- Rec_Goal : aliased Goal_Graph;
+ Con_Data : Lazy_Data_Access;
end case;
end record;