diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 514 |
1 files changed, 136 insertions, 378 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index d531f25..e525f23 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -8,7 +8,8 @@ with - Ada.Unchecked_Deallocation; + Ada.Unchecked_Deallocation, + Kompsos.Collector; package body Kompsos is @@ -52,6 +53,40 @@ package body Kompsos is + -- Worlds -- + + procedure Free is new Ada.Unchecked_Deallocation (World_Component, World_Component_Access); + + + procedure Initialize + (This : in out World) is + begin + This.Actual := null; + end Initialize; + + + procedure Adjust + (This : in out World) is + begin + if This.Actual /= null then + This.Actual.Counter := This.Actual.Counter + 1; + end if; + end Adjust; + + + procedure Finalize + (This : in out World) is + begin + if This.Actual /= null then + This.Actual.Counter := This.Actual.Counter - 1; + if This.Actual.Counter = 0 then + Free (This.Actual); + end if; + end if; + end Finalize; + + + ----------------- -- Datatypes -- @@ -156,31 +191,18 @@ package body Kompsos is -- Worlds -- - function Hold - (This : in World) - return World_Holders.Holder is - begin - return World_Holders.To_Holder (World_Root'Class (This)); - end Hold; - - - function Ptr - (This : in out World_Holders.Holder) - return World_Access is - begin - return World (This.Reference.Element.all)'Unchecked_Access; - end Ptr; - - - procedure Swap - (Left, Right : in out World_Holders.Holder) + function Static + (Item : in State) + return World'Class is - Temp : World_Holders.Holder; + use type State_Vectors.Vector; begin - Temp.Move (Left); - Left.Move (Right); - Right.Move (Temp); - end Swap; + 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; @@ -203,255 +225,6 @@ package body Kompsos is - -- Unification -- - - function Fully_Contains - (This : in State; - Item : in Term'Class) - return Boolean is - begin - case Item.Kind is - when Null_Term | Atom_Term => - return True; - when Var_Term => - return This.Ident.Contains (Item.Var.Ident); - when Pair_Term => - return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right); - end case; - end Fully_Contains; - - - function Walk - (This : in State; - Item : in Term'Class) - return Term'Class is - begin - if Item.Kind = Var_Term and then - This.Subst.Contains (This.Ident.Element (Item.Var.Ident)) - then - return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident))); - else - return Item; - end if; - end Walk; - - - function Do_Unify - (Potential : in State; - Left, Right : in Term'Class; - Extended : out State) - return Boolean - is - Real_Left : Term'Class := Left; - Real_Right : Term'Class := Right; - begin - -- Check for Variable validity with respect to State - if not Fully_Contains (Potential, Real_Left) or - not Fully_Contains (Potential, Real_Right) - then - return False; - end if; - - -- Resolve Variable substitution - if Left.Kind = Var_Term then - Real_Left := Walk (Potential, Real_Left); - end if; - if Right.Kind = Var_Term then - Real_Right := Walk (Potential, Real_Right); - end if; - - -- Unify equal Variable/Atom/Null Terms - if (Real_Left.Kind = Var_Term and then - Real_Right.Kind = Var_Term and then - Real_Left = Real_Right) or else - (Real_Left.Kind = Atom_Term and then - Real_Right.Kind = Atom_Term and then - Real_Left = Real_Right) or else - (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term) - then - Extended := Potential; - return True; - end if; - - -- Unify Variable and other Terms by introducing a new substitution - if Real_Left.Kind = Var_Term then - Extended := Potential; - Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right)); - return True; - end if; - if Real_Right.Kind = Var_Term then - Extended := Potential; - Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left)); - return True; - end if; - - -- Unify Pair Terms by unifying each corresponding part - if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then - declare - Middle : State; - begin - return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then - Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended); - end; - end if; - - -- Not sure how things get here, but if all else fails - return False; - end Do_Unify; - - - - -- Lazy World Generation -- - - function Call_Lazy - (This : in World; - Data : in Lazy_Holders.Holder) - return World - is - Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference; - begin - case Ref.Kind is - when Zero_Arg => - return Ref.ZFunc (This); - when One_Arg => - return Ref.OFunc (This, Ref.OInput); - when Many_Arg => - return Ref.MFunc (This, Term_Array_Holders.Constant_Reference (Ref.MInput)); - end case; - end Call_Lazy; - - - function Has_State - (This : in out World; - Index : in Positive) - return Boolean is - begin - This.Roll_Until (Index); - return This.Possibles.Last_Index >= Index; - end Has_State; - - - procedure Roll_Fresh_Gen - (This : in out World) is - begin - Ptr (This.Engine.Frs_World).Rollover; - for Potential of Ptr (This.Engine.Frs_World).Possibles loop - Potential.LVars.Append (This.Engine.Frs_Name); - Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index); - This.Possibles.Append (Potential); - end loop; - if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then - This.Engine := (Kind => No_Gen); - else - Ptr (This.Engine.Frs_World).Possibles.Clear; - end if; - end Roll_Fresh_Gen; - - - procedure Roll_Unify_Gen - (This : in out World) - is - Extended : State; - begin - Ptr (This.Engine.Uni_World).Rollover; - for Potential of Ptr (This.Engine.Uni_World).Possibles loop - if Do_Unify (Potential, This.Engine.Uni_Term1, This.Engine.Uni_Term2, Extended) then - This.Possibles.Append (Extended); - end if; - end loop; - if Ptr (This.Engine.Uni_World).Engine.Kind = No_Gen then - This.Engine := (Kind => No_Gen); - else - Ptr (This.Engine.Uni_World).Possibles.Clear; - end if; - end Roll_Unify_Gen; - - - procedure Roll_Disjunct_Gen - (This : in out World) is - begin - Ptr (This.Engine.Dis_World1).Rollover; - This.Possibles.Append (Ptr (This.Engine.Dis_World1).Possibles); - if Ptr (This.Engine.Dis_World1).Engine.Kind = No_Gen then - Ptr (This.Engine.Dis_World2).Rollover; -- why is this line needed? - This.Possibles.Append (Ptr (This.Engine.Dis_World2).Possibles); - This.Engine := World (This.Engine.Dis_World2.Element).Engine; - else - Ptr (This.Engine.Dis_World1).Possibles.Clear; - Swap (This.Engine.Dis_World1, This.Engine.Dis_World2); - end if; - end Roll_Disjunct_Gen; - - - procedure Roll_Conjunct_Gen - (This : in out World) - is - use type Ada.Containers.Count_Type; - begin - Ptr (This.Engine.Con_World).Rollover; - if Ptr (This.Engine.Con_World).Possibles.Length > 0 then - declare - So_Far : constant World := - ((Possibles => Ptr (This.Engine.Con_World).Possibles, - Engine => (Kind => No_Gen))); - begin - Ptr (This.Engine.Con_World).Possibles.Clear; - This := Disjunct (Call_Lazy (So_Far, This.Engine.Con_Data), This); - end; - elsif Ptr (This.Engine.Con_World).Engine.Kind = No_Gen then - This.Engine := (Kind => No_Gen); - end if; - end Roll_Conjunct_Gen; - - - procedure Roll_Recurse_Gen - (This : in out World) is - begin - Ptr (This.Engine.Rec_World).Rollover; - if Ptr (This.Engine.Rec_World).Possibles.Last_Index < This.Engine.Rec_Index then - if Ptr (This.Engine.Rec_World).Engine.Kind = No_Gen then - if This.Engine.Rec_Index = 1 then - This.Engine := (Kind => No_Gen); - else - This.Engine.Rec_Index := 1; - end if; - end if; - return; - end if; - for Index in Integer range - This.Engine.Rec_Index .. Ptr (This.Engine.Rec_World).Possibles.Last_Index - loop - This.Possibles.Append (Ptr (This.Engine.Rec_World).Possibles (Index)); - end loop; - This.Engine.Rec_Index := Ptr (This.Engine.Rec_World).Possibles.Last_Index + 1; - end Roll_Recurse_Gen; - - - procedure Rollover - (This : in out World) is - begin - case This.Engine.Kind is - when No_Gen => null; - when Fresh_Gen => This.Roll_Fresh_Gen; - when Unify_Gen => This.Roll_Unify_Gen; - when Disjunct_Gen => This.Roll_Disjunct_Gen; - when Conjunct_Gen => This.Roll_Conjunct_Gen; - when Recurse_Gen => This.Roll_Recurse_Gen; - end case; - end Rollover; - - - procedure Roll_Until - (This : in out World; - Index : in Positive) is - begin - while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop - This.Rollover; - end loop; - end Roll_Until; - - - ------------------- -- microKanren -- @@ -481,15 +254,15 @@ package body Kompsos is Name : in Nametag) return Term is - My_ID : constant Generator_ID_Number := Next_Gen; - begin - return My_Term : constant Term := Term (T (Variable'(Ident => My_ID, Name => Name))) do - This.Engine := - (Kind => Fresh_Gen, - Frs_Ident => My_ID, - Frs_World => Hold (This), - Frs_Name => Name); - This.Possibles := State_Vectors.Empty_Vector; + My_ID : constant Generator_ID_Number := Next_Gen; + 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)); end return; end Fresh; @@ -552,13 +325,13 @@ package body Kompsos is Left, Right : in Term'Class) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Unify_Gen, - Uni_World => Hold (This), + return Result : constant World := (Ada.Finalization.Controlled with + Actual => new World_Component'( + (Kind => Unify_Node, + Counter => 1, + Uni_World => This, Uni_Term1 => Term (Left), - Uni_Term2 => Term (Right))); + Uni_Term2 => Term (Right)))); end Unify; @@ -577,12 +350,12 @@ package body Kompsos is (Left, Right : in World) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Disjunct_Gen, - Dis_World1 => Hold (Left), - Dis_World2 => Hold (Right))); + return Result : constant World := (Ada.Finalization.Controlled with + Actual => new World_Component'( + (Kind => Disjunct_Node, + Counter => 1, + Dis_World1 => Left, + Dis_World2 => Right))); end Disjunct; @@ -599,18 +372,20 @@ package body Kompsos is return World is begin if Inputs'Length = 0 then - return Failed : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => (Kind => No_Gen)); + return Result : constant World := (Ada.Finalization.Controlled with + Actual => new World_Component'( + (Kind => Static_Node, + Counter => 1, + Stc_States => State_Vectors.Empty_Vector))); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Disjunct_Gen, - Dis_World1 => Hold (Inputs (Inputs'First)), - Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); + 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))))); end if; end Disjunct; @@ -631,12 +406,12 @@ package body Kompsos is Func : in Junction_Zero_Func) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Conjunct_Gen, - Con_World => Hold (This), - Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func)))); + 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))))); end Conjunct; @@ -654,15 +429,15 @@ package body Kompsos is Input : in Term'Class) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Conjunct_Gen, - Con_World => Hold (This), + 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 => One_Arg, OFunc => Func, - OInput => Term (Input))))); + OInput => Term (Input)))))); end Conjunct; @@ -681,15 +456,15 @@ package body Kompsos is Inputs : in Term_Array) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Conjunct_Gen, - Con_World => Hold (This), + 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 => Many_Arg, MFunc => Func, - MInput => Term_Array_Holders.To_Holder (Inputs))))); + MInput => Term_Array_Holders.To_Holder (Inputs)))))); end Conjunct; @@ -714,12 +489,11 @@ package body Kompsos is (This : in World) return World is begin - return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Engine => - (Kind => Recurse_Gen, - Rec_World => Hold (This), - Rec_Index => 1)); + return Result : constant World := (Ada.Finalization.Controlled with + Actual => new World_Component'( + (Kind => Recurse_Node, + Counter => 1, + Rec_World => This))); end Recurse; @@ -731,71 +505,55 @@ package body Kompsos is - -- Forced Evaluation -- + -- Evaluation -- function Take - (This : in out World; - Count : in Positive) - return State_Array is + (This : in World; + Count : in Positive) + return State_Array + is + Result : State_Array (1 .. Count); + Valid : Natural := 0; + + package Collect is new Collector (This); begin - This.Force (Count); - return Result : State_Array (1 .. Integer'Min (Count, This.Possibles.Last_Index)) do - for Index in Result'Range loop - Result (Index) := This.Possibles.Element (Index); - end loop; - end return; + for Item of Result loop + exit when not Collect.Has_Next; + Item := Collect.Next; + Valid := Valid + 1; + end loop; + return Result (1 .. Valid); end Take; function Take_First - (This : in out World) - return State is + (This : in World) + return State + is + package Collect is new Collector (This); begin - This.Force (1); - if This.Possibles.Is_Empty then - return Empty_State; - else - return This.Possibles.First_Element; - end if; + return Collect.Next (Empty_State); end Take_First; function Take_All - (This : in out World) - return State_Array is - begin - This.Force_All; - return Result : State_Array (1 .. Natural (This.Possibles.Length)) do - for Index in Result'Range loop - Result (Index) := This.Possibles.Element (Index); - end loop; - end return; - end Take_All; - - - procedure Force - (This : in out World; - Count : in Positive) is - begin - This.Roll_Until (Count); - end Force; - - - procedure Force_All - (This : in out World) is - begin - while This.Engine.Kind /= No_Gen loop - This.Rollover; - end loop; - end Force_All; - + (This : in World) + return State_Array + is + package Collect is new Collector (This); - function Failed - (This : in out World) - return Boolean is + function Do_Take + return State_Array is + begin + if Collect.Has_Next then + return Collect.Next & Do_Take; + else + return Result : State_Array (1 .. 0); + end if; + end Do_Take; begin - return not This.Has_State (1); - end Failed; + return Do_Take; + end Take_All; |