diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 526 |
1 files changed, 462 insertions, 64 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index cb2f775..c1d63da 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -55,10 +55,9 @@ package body Kompsos is - -- World_Holders -- - procedure Free is new Ada.Unchecked_Deallocation (Mu_World'Class, World_Access); + procedure Free is new Ada.Unchecked_Deallocation (World'Class, World_Access); procedure Initialize @@ -71,7 +70,7 @@ package body Kompsos is procedure Adjust (This : in out World_Holder) is begin - This.Ptr := new Mu_World'Class'(This.Ptr.all); + This.Ptr := new World'Class'(This.Ptr.all); end Adjust; @@ -83,10 +82,10 @@ package body Kompsos is function Hold - (This : in Mu_World'Class) + (This : in World'Class) return World_Holder is begin - return (Ada.Finalization.Controlled with Ptr => new Mu_World'Class'(This)); + return (Ada.Finalization.Controlled with Ptr => new World'Class'(This)); end Hold; @@ -102,9 +101,11 @@ package body Kompsos is - ------------- + ----------------- + -- Datatypes -- + ----------------- + -- Terms -- - ------------- function "=" (Left, Right : in Term) @@ -341,11 +342,10 @@ package body Kompsos is - -- Lazy World Generation -- function Has_State - (This : in out Mu_World; + (This : in out World; Index : in Positive) return Boolean is begin @@ -355,7 +355,7 @@ package body Kompsos is procedure Roll_Fresh_Gen - (This : in out Mu_World) is + (This : in out World) is begin This.Engine.Frs_World.Ptr.Rollover; for Potential of This.Engine.Frs_World.Ptr.Possibles loop @@ -371,7 +371,7 @@ package body Kompsos is procedure Roll_Unify_Gen - (This : in out Mu_World) + (This : in out World) is Extended : State; begin @@ -390,7 +390,7 @@ package body Kompsos is procedure Roll_Buffer_Gen - (This : in out Mu_World) is + (This : in out World) is begin This.Engine.Buff_World.Ptr.Rollover; This.Possibles.Append (This.Engine.Buff_World.Ptr.Possibles); @@ -403,7 +403,7 @@ package body Kompsos is procedure Roll_Disjunct_Gen - (This : in out Mu_World) is + (This : in out World) is begin This.Engine.Dis_World1.Ptr.Rollover; This.Possibles.Append (This.Engine.Dis_World1.Ptr.Possibles); @@ -416,8 +416,67 @@ package body Kompsos is end Roll_Disjunct_Gen; + procedure Roll_Conjunct_Zero_Gen + (This : in out World) + is + use type Ada.Containers.Count_Type; + begin + This.Engine.ConZ_World.Ptr.Rollover; + if This.Engine.ConZ_World.Ptr.Possibles.Length > 0 then + declare + Next : constant World := This.Engine.ConZ_Func + (World (This.Engine.ConZ_World.Ptr.all)); + begin + This := Next; + end; + elsif This.Engine.ConZ_World.Ptr.Engine.Kind = No_Gen then + This.Engine := (Kind => No_Gen); + end if; + end Roll_Conjunct_Zero_Gen; + + + procedure Roll_Conjunct_One_Gen + (This : in out World) + is + use type Ada.Containers.Count_Type; + begin + This.Engine.ConO_World.Ptr.Rollover; + if This.Engine.ConO_World.Ptr.Possibles.Length > 0 then + declare + Next : constant World := This.Engine.ConO_Func + (World (This.Engine.ConO_World.Ptr.all), + This.Engine.ConO_Input); + begin + This := Next; + end; + elsif This.Engine.ConO_World.Ptr.Engine.Kind = No_Gen then + This.Engine := (Kind => No_Gen); + end if; + end Roll_Conjunct_One_Gen; + + + procedure Roll_Conjunct_Many_Gen + (This : in out World) + is + use type Ada.Containers.Count_Type; + begin + This.Engine.ConM_World.Ptr.Rollover; + if This.Engine.ConM_World.Ptr.Possibles.Length > 0 then + declare + Next : constant World := This.Engine.ConM_Func + (World (This.Engine.ConM_World.Ptr.all), + This.Engine.ConM_Inputs.Constant_Reference); + begin + This := Next; + end; + elsif This.Engine.ConM_World.Ptr.Engine.Kind = No_Gen then + This.Engine := (Kind => No_Gen); + end if; + end Roll_Conjunct_Many_Gen; + + procedure Roll_Recurse_Gen - (This : in out Mu_World) is + (This : in out World) is begin This.Engine.Rec_World.Ptr.Rollover; if This.Engine.Rec_World.Ptr.Possibles.Last_Index < This.Engine.Rec_Index then @@ -440,21 +499,24 @@ package body Kompsos is procedure Rollover - (This : in out Mu_World) is + (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 Buffer_Gen => This.Roll_Buffer_Gen; - when Disjunct_Gen => This.Roll_Disjunct_Gen; - when Recurse_Gen => This.Roll_Recurse_Gen; + when No_Gen => null; + when Fresh_Gen => This.Roll_Fresh_Gen; + when Unify_Gen => This.Roll_Unify_Gen; + when Buffer_Gen => This.Roll_Buffer_Gen; + when Disjunct_Gen => This.Roll_Disjunct_Gen; + when Conjunct_Zero_Gen => This.Roll_Conjunct_Zero_Gen; + when Conjunct_One_Gen => This.Roll_Conjunct_One_Gen; + when Conjunct_Many_Gen => This.Roll_Conjunct_Many_Gen; + when Recurse_Gen => This.Roll_Recurse_Gen; end case; end Rollover; procedure Roll_Until - (This : in out Mu_World; + (This : in out World; Index : in Positive) is begin while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop @@ -465,14 +527,14 @@ package body Kompsos is - ----------------------------- - -- Public API Operations -- - ----------------------------- + ------------------- + -- microKanren -- + ------------------- - -- Fresh -- + -- Variable Introduction -- function Fresh - (This : in out Mu_World'Class) + (This : in out World'Class) return Term is begin return This.Fresh (+""); @@ -480,7 +542,7 @@ package body Kompsos is function Fresh - (This : in out Mu_World'Class; + (This : in out World'Class; Name : in String) return Term is begin @@ -489,7 +551,7 @@ package body Kompsos is function Fresh - (This : in out Mu_World'Class; + (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) return Term is begin @@ -505,21 +567,20 @@ package body Kompsos is - - -- Unify -- + -- Unification -- function Unify - (This : in Mu_World; + (This : in World; Left : in Term'Class; Right : in Element_Type) - return Mu_World is + return World is begin return This.Unify (Left, T (Right)); end Unify; procedure Unify - (This : in out Mu_World; + (This : in out World; Left : in Term'Class; Right : in Element_Type) is begin @@ -528,11 +589,11 @@ package body Kompsos is function Unify - (This : in Mu_World; + (This : in World; Left, Right : in Term'Class) - return Mu_World is + return World is begin - return Result : constant Mu_World := + return Result : constant World := (Possibles => State_Vectors.Empty_Vector, Next_Ident => This.Next_Ident, Engine => @@ -544,7 +605,7 @@ package body Kompsos is procedure Unify - (This : in out Mu_World; + (This : in out World; Left, Right : in Term'Class) is begin This := This.Unify (Left, Right); @@ -552,14 +613,13 @@ package body Kompsos is - - -- Disjunct -- + -- Combining / Disjunction -- function Disjunct - (Left, Right : in Mu_World) - return Mu_World is + (Left, Right : in World) + return World is begin - return Result : constant Mu_World := + return Result : constant World := (Possibles => State_Vectors.Empty_Vector, Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident), Engine => @@ -570,26 +630,26 @@ package body Kompsos is procedure Disjunct - (This : in out Mu_World; - Right : in Mu_World) is + (This : in out World; + Right : in World) is begin This := Disjunct (This, Right); end Disjunct; function Disjunct - (Inputs : in Mu_World_Array) - return Mu_World is + (Inputs : in World_Array) + return World is begin if Inputs'Length = 0 then - return Failed : constant Mu_World := + return Failed : constant World := (Possibles => State_Vectors.Empty_Vector, Next_Ident => 0, Engine => (Kind => No_Gen)); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : Mu_World := + return Result : World := (Possibles => State_Vectors.Empty_Vector, Next_Ident => 0, -- dummy Engine => @@ -606,22 +666,104 @@ package body Kompsos is procedure Disjunct - (This : in out Mu_World; - Inputs : in Mu_World_Array) is + (This : in out World; + Inputs : in World_Array) is begin This := Disjunct (This & Inputs); end Disjunct; + -- Lazy Sequencing / Conjunction -- + + function Conjunct + (This : in World; + Func : in Conjunct_Zero_Func) + return World is + begin + return Result : constant World := + (Possibles => State_Vectors.Empty_Vector, + Next_Ident => 0, -- dummy + Engine => + (Kind => Conjunct_Zero_Gen, + ConZ_World => Hold (This), + ConZ_Func => Func)); + end Conjunct; + + + procedure Conjunct + (This : in out World; + Func : in Conjunct_Zero_Func) is + begin + This := This.Conjunct (Func); + end Conjunct; - -- Recurse -- + + function Conjunct + (This : in World; + Func : in Conjunct_One_Func; + Input : in Term'Class) + return World is + begin + return Result : constant World := + (Possibles => State_Vectors.Empty_Vector, + Next_Ident => 0, -- dummy + Engine => + (Kind => Conjunct_One_Gen, + ConO_World => Hold (This), + ConO_Func => Func, + ConO_Input => Term (Input))); + end Conjunct; + + + procedure Conjunct + (This : in out World; + Func : in Conjunct_One_Func; + Input : in Term'Class) is + begin + This := This.Conjunct (Func, Input); + end Conjunct; + + + function Conjunct + (This : in World; + Func : in Conjunct_Many_Func; + Inputs : in Term_Array) + return World is + begin + return Result : constant World := + (Possibles => State_Vectors.Empty_Vector, + Next_Ident => 0, -- dummy + Engine => + (Kind => Conjunct_Many_Gen, + ConM_World => Hold (This), + ConM_Func => Func, + ConM_Inputs => Term_Array_Holders.To_Holder (Inputs))); + end Conjunct; + + + procedure Conjunct + (This : in out World; + Func : in Conjunct_Many_Func; + Inputs : in Term_Array) is + begin + This := This.Conjunct (Func, Inputs); + end Conjunct; + + + + + ------------------------- + -- Auxiliary Helpers -- + ------------------------- + + -- Infinite State Loops -- function Recurse - (This : in Mu_World) - return Mu_World is + (This : in World) + return World is begin - return Result : constant Mu_World := + return Result : constant World := (Possibles => State_Vectors.Empty_Vector, Next_Ident => This.Next_Ident, Engine => @@ -632,20 +774,19 @@ package body Kompsos is procedure Recurse - (This : in out Mu_World) is + (This : in out World) is begin This := This.Recurse; end Recurse; - -- Forced Evaluation -- function Take - (This : in Mu_World; + (This : in World; Count : in Natural) - return Mu_World is + return World is begin if Count = 0 then return @@ -653,7 +794,7 @@ package body Kompsos is Next_Ident => ID_Number'First, Engine => (Kind => No_Gen)); end if; - return Result : Mu_World := This do + return Result : World := This do Result.Roll_Until (Count); if Result.Possibles.Last_Index > Count then Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count)); @@ -664,7 +805,7 @@ package body Kompsos is procedure Take - (This : in out Mu_World; + (This : in out World; Count : in Natural) is begin This := This.Take (Count); @@ -672,7 +813,7 @@ package body Kompsos is procedure Force - (This : in out Mu_World; + (This : in out World; Count : in Positive) is begin This.Roll_Until (Count); @@ -680,7 +821,7 @@ package body Kompsos is procedure Force_All - (This : in out Mu_World) is + (This : in out World) is begin while This.Engine.Kind /= No_Gen loop This.Rollover; @@ -689,13 +830,270 @@ package body Kompsos is function Failed - (This : in out Mu_World) + (This : in out World) return Boolean is begin return not This.Has_State (1); end Failed; + + + -------------------------- + -- miniKanren Prelude -- + -------------------------- + + -- caro -- + + function Head + (This : in World; + Inputs : in Term_Array) + return World + is + List_Term : Term renames Inputs (1); + Head_Term : Term renames Inputs (2); + begin + return Result : World := This do + Result.Unify (T (Head_Term, Result.Fresh), List_Term); + end return; + end Head; + + + procedure Head + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Head (Inputs); + end Head; + + + + -- cdro -- + + function Tail + (This : in World; + Inputs : in Term_Array) + return World + is + List_Term : Term renames Inputs (1); + Tail_Term : Term renames Inputs (2); + begin + return Result : World := This do + Result.Unify (T (Result.Fresh, Tail_Term), List_Term); + end return; + end Tail; + + + procedure Tail + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Tail (Inputs); + end Tail; + + + + -- conso -- + + function Cons + (This : in World; + Inputs : in Term_Array) + return World + 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 + Result.Unify (T (Head_Term, Tail_Term), List_Term); + end return; + end Cons; + + + procedure Cons + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Cons (Inputs); + end Cons; + + + + -- nullo -- + + function Nil + (This : in World; + Nil_Term : in Term'Class) + return World is + begin + return Result : World := This do + Result.Unify (Null_Term, Nil_Term); + end return; + end Nil; + + + procedure Nil + (This : in out World; + Nil_Term : in Term'Class) is + begin + This := This.Nil (Nil_Term); + end Nil; + + + + -- pairo -- + + function Pair + (This : in World; + Pair_Term : in Term'Class) + return World is + begin + return Result : World := This do + Result.Cons (Result.Fresh & Result.Fresh & Term (Pair_Term)); + end return; + end Pair; + + + procedure Pair + (This : in out World; + Pair_Term : in Term'Class) is + begin + This := This.Pair (Pair_Term); + end Pair; + + + + -- listo -- + + function Linked_List + (This : in World; + List_Term : in Term'Class) + return World + is + One, Two : World := This; + Ref_Term : constant Term := Two.Fresh; + begin + One.Nil (List_Term); + + Two.Pair (List_Term); + Two.Tail (Term (List_Term) & Ref_Term); + Two.Conjunct (Linked_List'Access, Ref_Term); + + return Disjunct (One, Two); + end Linked_List; + + + procedure Linked_List + (This : in out World; + List_Term : in Term'Class) is + begin + This := This.Linked_List (List_Term); + end Linked_List; + + + + -- membero -- + + function Member + (This : in World; + Inputs : in Term_Array) + return World + is + Item_Term : Term renames Inputs (1); + List_Term : Term renames Inputs (2); + + One, Two : World := This; + Ref_Term : constant Term := Two.Fresh; + begin + One.Head (List_Term & Item_Term); + + Two.Tail (List_Term & Ref_Term); + Two.Conjunct (Member'Access, Item_Term & Ref_Term); + + return Disjunct (One, Two); + end Member; + + + procedure Member + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Member (Inputs); + end Member; + + + + -- rembero -- + + function Remove + (This : in World; + Inputs : in Term_Array) + return World + is + Item_Term : Term renames Inputs (1); + List_Term : Term renames Inputs (2); + Out_Term : Term renames Inputs (3); + + One, Two : World := This; + Left : constant Term := Two.Fresh; + Right : constant Term := Two.Fresh; + Rest : constant Term := Two.Fresh; + begin + One.Head (List_Term & Item_Term); + One.Tail (List_Term & Out_Term); + + Two.Cons (Left & Right & List_Term); + Two.Conjunct (Remove'Access, Item_Term & Right & Rest); + Two.Cons (Left & Rest & Out_Term); + + return Disjunct (One, Two); + end Remove; + + + procedure Remove + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Remove (Inputs); + end Remove; + + + + -- appendo -- + + function Append + (This : in World; + Inputs : in Term_Array) + return World + is + List_Term : Term renames Inputs (1); + Item_Term : Term renames Inputs (2); + Out_Term : Term renames Inputs (3); + + One, Two : World := This; + Left : constant Term := Two.Fresh; + Right : constant Term := Two.Fresh; + Rest : constant Term := Two.Fresh; + begin + One.Nil (List_Term); + One.Unify (Item_Term, Out_Term); + + Two.Cons (Left & Right & List_Term); + Two.Cons (Left & Rest & Out_Term); + Two.Conjunct (Append'Access, Right & Item_Term & Rest); + + return Disjunct (One, Two); + end Append; + + + procedure Append + (This : in out World; + Inputs : in Term_Array) is + begin + This := This.Append (Inputs); + end Append; + + end Kompsos; |