diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 307 |
1 files changed, 146 insertions, 161 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index 476eb86..56c22cd 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -55,20 +55,20 @@ package body Kompsos is - -- Worlds -- + -- Goals -- - procedure Free is new Ada.Unchecked_Deallocation (World_Component, World_Component_Access); + procedure Free is new Ada.Unchecked_Deallocation (Goal_Component, Goal_Component_Access); procedure Initialize - (This : in out World) is + (This : in out Goal) is begin This.Actual := null; end Initialize; procedure Adjust - (This : in out World) is + (This : in out Goal) is begin if This.Actual /= null then This.Actual.Counter := This.Actual.Counter + 1; @@ -77,7 +77,7 @@ package body Kompsos is procedure Finalize - (This : in out World) is + (This : in out Goal) is begin if This.Actual /= null then This.Actual.Counter := This.Actual.Counter - 1; @@ -215,36 +215,22 @@ package body Kompsos is - -- Worlds -- + -- Goals -- - package World_Convert is new System.Address_To_Access_Conversions (World_Component); + package Goal_Convert is new System.Address_To_Access_Conversions (Goal_Component); function "<" - (Left, Right : in World_Component_Access) + (Left, Right : in Goal_Component_Access) return Boolean is use System.Storage_Elements; begin return - To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Left))) < - To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Right))); + To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Left))) < + To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Right))); end "<"; - function Static - (Item : in State) - return World'Class - is - use type State_Vectors.Vector; - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Static_Node, - Counter => 1, - Stc_States => State_Vectors.Empty_Vector & Item))); - end Static; - - ------------------------ @@ -273,7 +259,7 @@ package body Kompsos is -- Variable Introduction -- function Fresh - (This : in out World'Class) + (This : in out Goal'Class) return Term is begin return This.Fresh (+""); @@ -281,7 +267,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in String) return Term is begin @@ -290,7 +276,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in Nametag) return Term is @@ -298,17 +284,17 @@ package body Kompsos is My_Var : constant Variable := (Ident => My_ID, Name => Name); begin return My_Term : constant Term := Term (T (My_Var)) do - This.Actual := new World_Component'( - (Kind => Fresh_Node, - Counter => 1, - Frs_World => World (This), - Frs_Var => My_Var)); + This.Actual := new Goal_Component'( + (Kind => Fresh_Node, + Counter => 1, + Frs_Goal => Goal (This), + Frs_Var => My_Var)); end return; end Fresh; function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Count : in Positive) return Term_Array is @@ -319,7 +305,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Names : in Nametag_Array) return Term_Array is begin @@ -342,17 +328,17 @@ package body Kompsos is -- Unification -- function Unify - (This : in World; + (This : in Goal; Left : in Term'Class; Right : in Element_Type) - return World is + return Goal is begin return This.Unify (Left, T (Right)); end Unify; procedure Unify - (This : in out World; + (This : in out Goal; Left : in Term'Class; Right : in Element_Type) is begin @@ -361,22 +347,22 @@ package body Kompsos is function Unify - (This : in World; + (This : in Goal; Left, Right : in Term'Class) - return World is + return Goal is begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( (Kind => Unify_Node, Counter => 1, - Uni_World => This, + Uni_Goal => This, Uni_Term1 => Term (Left), Uni_Term2 => Term (Right)))); end Unify; procedure Unify - (This : in out World; + (This : in out Goal; Left, Right : in Term'Class) is begin This := This.Unify (Left, Right); @@ -387,52 +373,48 @@ package body Kompsos is -- Combining / Disjunction -- function Disjunct - (Left, Right : in World) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_World1 => Left, - Dis_World2 => Right))); + (Left, Right : in Goal) + return Goal is + begin + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Disjunct_Node, + Counter => 1, + Dis_Goal1 => Left, + Dis_Goal2 => Right))); end Disjunct; procedure Disjunct - (This : in out World; - Right : in World) is + (This : in out Goal; + Right : in Goal) is begin This := Disjunct (This, Right); end Disjunct; function Disjunct - (Inputs : in World_Array) - return World is + (Inputs : in Goal_Array) + return Goal is begin if Inputs'Length = 0 then - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Static_Node, - Counter => 1, - Stc_States => State_Vectors.Empty_Vector))); + return (Ada.Finalization.Controlled with Actual => null); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_World1 => Inputs (Inputs'First), - Dis_World2 => Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Disjunct_Node, + Counter => 1, + Dis_Goal1 => Inputs (Inputs'First), + Dis_Goal2 => Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); end if; end Disjunct; procedure Disjunct - (This : in out World; - Inputs : in World_Array) is + (This : in out Goal; + Inputs : in Goal_Array) is begin This := Disjunct (This & Inputs); end Disjunct; @@ -442,21 +424,21 @@ package body Kompsos is -- Lazy Sequencing / Conjunction -- function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Zero_Func) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))); + return Goal is + begin + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This, + Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))); end Conjunct; procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Zero_Func) is begin This := This.Conjunct (Func); @@ -464,17 +446,17 @@ package body Kompsos is function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_One_Func; Input : in Term'Class) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder + return Goal is + begin + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This, + Con_Data => Lazy_Holders.To_Holder ((Kind => One_Arg, OFunc => Func, OInput => Term (Input)))))); @@ -482,7 +464,7 @@ package body Kompsos is procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_One_Func; Input : in Term'Class) is begin @@ -491,17 +473,17 @@ package body Kompsos is function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Many_Func; Inputs : in Term_Array) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder + return Goal is + begin + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This, + Con_Data => Lazy_Holders.To_Holder ((Kind => Many_Arg, MFunc => Func, MInput => Term_Array_Holders.To_Holder (Inputs)))))); @@ -509,7 +491,7 @@ package body Kompsos is procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Many_Func; Inputs : in Term_Array) is begin @@ -526,19 +508,19 @@ package body Kompsos is -- Infinite State Loops -- function Recurse - (This : in World) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Recurse_Node, - Counter => 1, - Rec_World => This))); + (This : in Goal) + return Goal is + begin + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Recurse_Node, + Counter => 1, + Rec_Goal => This))); end Recurse; procedure Recurse - (This : in out World) is + (This : in out Goal) is begin This := This.Recurse; end Recurse; @@ -547,15 +529,16 @@ package body Kompsos is -- Evaluation -- - function Take - (This : in World; - Count : in Positive) + function Run + (This : in Goal; + Count : in Positive; + Base : in State := Empty_State) return State_Array is Result : State_Array (1 .. Count); Valid : Natural := 0; - package Collect is new Collector (This); + package Collect is new Collector (This, Base); begin for Item of Result loop exit when not Collect.Has_Next; @@ -563,37 +546,39 @@ package body Kompsos is Valid := Valid + 1; end loop; return Result (1 .. Valid); - end Take; + end Run; - function Take_First - (This : in World) + function Run + (This : in Goal; + Base : in State := Empty_State) return State is - package Collect is new Collector (This); + package Collect is new Collector (This, Base); begin return Collect.Next (Empty_State); - end Take_First; + end Run; - function Take_All - (This : in World) + function Run_All + (This : in Goal; + Base : in State := Empty_State) return State_Array is - package Collect is new Collector (This); + package Collect is new Collector (This, Base); - function Do_Take + function Do_Run return State_Array is begin if Collect.Has_Next then - return Collect.Next & Do_Take; + return Collect.Next & Do_Run; else return Result : State_Array (1 .. 0); end if; - end Do_Take; + end Do_Run; begin - return Do_Take; - end Take_All; + return Do_Run; + end Run_All; @@ -685,21 +670,21 @@ package body Kompsos is -- caro -- function Head - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Head_Term : Term renames Inputs (2); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Head_Term, Result.Fresh), List_Term); end return; end Head; procedure Head - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Head (Inputs); @@ -710,21 +695,21 @@ package body Kompsos is -- cdro -- function Tail - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Tail_Term : Term renames Inputs (2); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Result.Fresh, Tail_Term), List_Term); end return; end Tail; procedure Tail - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Tail (Inputs); @@ -735,22 +720,22 @@ package body Kompsos is -- conso -- function Cons - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Head_Term : Term renames Inputs (1); Tail_Term : Term renames Inputs (2); List_Term : Term renames Inputs (3); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Head_Term, Tail_Term), List_Term); end return; end Cons; procedure Cons - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Cons (Inputs); @@ -761,18 +746,18 @@ package body Kompsos is -- nullo -- function Nil - (This : in World; + (This : in Goal; Nil_Term : in Term'Class) - return World is + return Goal is begin - return Result : World := This do + return Result : Goal := This do Result.Unify (Empty_Term, Nil_Term); end return; end Nil; procedure Nil - (This : in out World; + (This : in out Goal; Nil_Term : in Term'Class) is begin This := This.Nil (Nil_Term); @@ -783,18 +768,18 @@ package body Kompsos is -- pairo -- function Pair - (This : in World; + (This : in Goal; Pair_Term : in Term'Class) - return World is + return Goal is begin - return Result : World := This do + return Result : Goal := This do Result.Cons (Result.Fresh & Result.Fresh & Term (Pair_Term)); end return; end Pair; procedure Pair - (This : in out World; + (This : in out Goal; Pair_Term : in Term'Class) is begin This := This.Pair (Pair_Term); @@ -805,11 +790,11 @@ package body Kompsos is -- listo -- function Linked_List - (This : in World; + (This : in Goal; List_Term : in Term'Class) - return World + return Goal is - One, Two : World := This; + One, Two : Goal := This; Ref_Term : constant Term := Two.Fresh; begin One.Nil (List_Term); @@ -823,7 +808,7 @@ package body Kompsos is procedure Linked_List - (This : in out World; + (This : in out Goal; List_Term : in Term'Class) is begin This := This.Linked_List (List_Term); @@ -834,14 +819,14 @@ package body Kompsos is -- membero -- function Member - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Item_Term : Term renames Inputs (1); List_Term : Term renames Inputs (2); - One, Two : World := This; + One, Two : Goal := This; Ref_Term : constant Term := Two.Fresh; begin One.Head (List_Term & Item_Term); @@ -854,7 +839,7 @@ package body Kompsos is procedure Member - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Member (Inputs); @@ -865,15 +850,15 @@ package body Kompsos is -- rembero -- function Remove - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Item_Term : Term renames Inputs (1); List_Term : Term renames Inputs (2); Out_Term : Term renames Inputs (3); - One, Two : World := This; + One, Two : Goal := This; Left : constant Term := Two.Fresh; Right : constant Term := Two.Fresh; Rest : constant Term := Two.Fresh; @@ -890,7 +875,7 @@ package body Kompsos is procedure Remove - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Remove (Inputs); @@ -901,15 +886,15 @@ package body Kompsos is -- appendo -- function Append - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Item_Term : Term renames Inputs (2); Out_Term : Term renames Inputs (3); - One, Two : World := This; + One, Two : Goal := This; Left : constant Term := Two.Fresh; Right : constant Term := Two.Fresh; Rest : constant Term := Two.Fresh; @@ -926,7 +911,7 @@ package body Kompsos is procedure Append - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Append (Inputs); |