From 72faae829a789664eedbda930cf815663c41c591 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sat, 15 Nov 2025 08:03:12 +1300 Subject: Prelude combined into base, lazy Conjunct kinda working but still loops in some circumstances --- src/kompsos-prelude.adb | 244 -------------------- src/kompsos-prelude.ads | 158 ------------- src/kompsos-pretty_print.adb | 4 +- src/kompsos-pretty_print.ads | 2 +- src/kompsos.adb | 526 +++++++++++++++++++++++++++++++++++++------ src/kompsos.ads | 334 ++++++++++++++++++++++----- 6 files changed, 748 insertions(+), 520 deletions(-) delete mode 100644 src/kompsos-prelude.adb delete mode 100644 src/kompsos-prelude.ads (limited to 'src') diff --git a/src/kompsos-prelude.adb b/src/kompsos-prelude.adb deleted file mode 100644 index 896e918..0000000 --- a/src/kompsos-prelude.adb +++ /dev/null @@ -1,244 +0,0 @@ - - --- Programmed by Jedidiah Barber --- Licensed under the Sunset License v1.0 - --- See license.txt for further details - - -package body Kompsos.Prelude is - - - function Head - (This : in World; - Full_List, Head_Term : in Term'Class) - return World is - begin - return Result : World := This do - Result.Unify (T (Head_Term, Result.Fresh), Full_List); - end return; - end Head; - - - procedure Head - (This : in out World; - Full_List, Head_Term : in Term'Class) is - begin - This := This.Head (Full_List, Head_Term); - end Head; - - - - - function Tail - (This : in World; - Full_List, Tail_Term : in Term'Class) - return World is - begin - return Result : World := This do - Result.Unify (T (Result.Fresh, Tail_Term), Full_List); - end return; - end Tail; - - - procedure Tail - (This : in out World; - Full_List, Tail_Term : in Term'Class) is - begin - This := This.Tail (Full_List, Tail_Term); - end Tail; - - - - - function Cons - (This : in World; - Head_Term, Tail_Term, Full_List : in Term'Class) - return World is - begin - return Result : World := This do - Result.Unify (T (Head_Term, Tail_Term), Full_List); - end return; - end Cons; - - - procedure Cons - (This : in out World; - Head_Term, Tail_Term, Full_List : in Term'Class) is - begin - This := This.Cons (Head_Term, Tail_Term, Full_List); - end Cons; - - - - - 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; - - - - - 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, 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; - - - - - 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 (List_Term, Ref_Term); - if not Two.Failed then - Two.Linked_List (Ref_Term); - end if; - - 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; - - - - - function Member - (This : in World; - Item_Term, List_Term : in Term'Class) - return World - is - One, Two : World := This; - Ref_Term : constant Term := Two.Fresh; - begin - One.Head (List_Term, Item_Term); - - Two.Tail (List_Term, Ref_Term); - if not Two.Failed then - Two.Member (Item_Term, Ref_Term); - end if; - - return Disjunct (One, Two); - end Member; - - - procedure Member - (This : in out World; - Item_Term, List_Term : in Term'Class) is - begin - This := This.Member (Item_Term, List_Term); - end Member; - - - - - function Remove - (This : in World; - Item_Term, List_Term, Out_Term : in Term'Class) - return World - is - 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); - - -- infinite loops if run in reverse with vars for item and list - -- probably needs lazy conjunction to work properly - Two.Cons (Left, Right, List_Term); - if not Two.Failed then - Two.Remove (Item_Term, Right, Rest); - Two.Cons (Left, Rest, Out_Term); - end if; - - return Disjunct (One, Two); - end Remove; - - - procedure Remove - (This : in out World; - Item_Term, List_Term, Out_Term : in Term'Class) is - begin - This := This.Remove (Item_Term, List_Term, Out_Term); - end Remove; - - - - - function Append - (This : in World; - List_Term, Item_Term, Out_Term : in Term'Class) - return World - is - 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); - if not Two.Failed then - Two.Append (Right, Item_Term, Rest); - end if; - - return Disjunct (One, Two); - end Append; - - - procedure Append - (This : in out World; - List_Term, Item_Term, Out_Term : in Term'Class) is - begin - This := This.Append (List_Term, Item_Term, Out_Term); - end Append; - - -end Kompsos.Prelude; - - diff --git a/src/kompsos-prelude.ads b/src/kompsos-prelude.ads deleted file mode 100644 index 2ad2309..0000000 --- a/src/kompsos-prelude.ads +++ /dev/null @@ -1,158 +0,0 @@ - - --- Programmed by Jedidiah Barber --- Licensed under the Sunset License v1.0 - --- See license.txt for further details - - -generic -package Kompsos.Prelude is - - - type World is new Mu_World with private; - - Empty_World : constant World; - - - - - -- caro -- - - function Head - (This : in World; - Full_List, Head_Term : in Term'Class) - return World; - - procedure Head - (This : in out World; - Full_List, Head_Term : in Term'Class); - - - -- cdro -- - - function Tail - (This : in World; - Full_List, Tail_Term : in Term'Class) - return World; - - procedure Tail - (This : in out World; - Full_List, Tail_Term : in Term'Class); - - - -- conso -- - - function Cons - (This : in World; - Head_Term, Tail_Term, Full_List : in Term'Class) - return World; - - procedure Cons - (This : in out World; - Head_Term, Tail_Term, Full_List : in Term'Class); - - - -- nullo -- - - function Nil - (This : in World; - Nil_Term : in Term'Class) - return World; - - procedure Nil - (This : in out World; - Nil_Term : in Term'Class); - - - -- eqo -- - -- Skipped due to being a synonym for Unify - - - -- eq-caro -- - -- Skipped due to being a synonym for Head - - - -- pairo -- - - function Pair - (This : in World; - Pair_Term : in Term'Class) - return World; - - procedure Pair - (This : in out World; - Pair_Term : in Term'Class); - - - -- listo -- - - function Linked_List - (This : in World; - List_Term : in Term'Class) - return World; - - procedure Linked_List - (This : in out World; - List_Term : in Term'Class); - - - -- membero -- - - function Member - (This : in World; - Item_Term, List_Term : in Term'Class) - return World; - - procedure Member - (This : in out World; - Item_Term, List_Term : in Term'Class); - - - -- rembero -- - - function Remove - (This : in World; - Item_Term, List_Term, Out_Term : in Term'Class) - return World; - - procedure Remove - (This : in out World; - Item_Term, List_Term, Out_Term : in Term'Class); - - - -- appendo -- - - function Append - (This : in World; - List_Term, Item_Term, Out_Term : in Term'Class) - return World; - - procedure Append - (This : in out World; - List_Term, Item_Term, Out_Term : in Term'Class); - - - -- anyo -- - -- Skipped due to Recurse doing the same thing - - - -- nevero -- - -- Skipped since it just creates a failed World - - - -- alwayso -- - -- Skipped due to Recurse doing the same thing - - -private - - - type World is new Mu_World with null record; - - Empty_World : constant World := (Empty_Mu_World with null record); - - -end Kompsos.Prelude; - - diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 88c13c7..7ecbb75 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -125,11 +125,11 @@ package body Kompsos.Pretty_Print is function Image - (Item : in Mu_World'Class) + (Item : in World) return String is Result : SU.Unbounded_String; - Scratch : Mu_World'Class := Item; + Scratch : World := Item; Counter : Positive := 1; begin if not Scratch.Has_State (Counter) then diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index 1359d1f..ed9509a 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -19,7 +19,7 @@ package Kompsos.Pretty_Print is function Image - (Item : in Mu_World'Class) + (Item : in World) return String; 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; diff --git a/src/kompsos.ads b/src/kompsos.ads index f3f8470..0463f6f 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -12,6 +12,7 @@ with private with + Ada.Containers.Indefinite_Holders, Ada.Containers.Ordered_Maps, Ada.Containers.Vectors, Ada.Finalization; @@ -22,11 +23,13 @@ generic package Kompsos is + ----------------- + -- Datatypes -- + ----------------- + type Term is tagged private; type Term_Array is array (Positive range <>) of Term; - -- Can also be constructed by supplying an empty array to T - -- or just declaring a Term without initial value. Null_Term : constant Term; function "=" @@ -48,104 +51,317 @@ package Kompsos is -- Might include subprograms to retrieve Term contents later? - type Mu_World is tagged private; - type Mu_World_Array is array (Positive range <>) of Mu_World; + type World is tagged private; + type World_Array is array (Positive range <>) of World; + + Empty_World : constant World; + + + type Conjunct_Zero_Func is access function + (This : in World) + return World; - Empty_Mu_World : constant Mu_World; + type Conjunct_One_Func is access function + (This : in World; + Input : in Term'Class) + return World; + type Conjunct_Many_Func is access function + (This : in World; + Inputs : in Term_Array) + return World; + + ------------------- + -- microKanren -- + ------------------- + + -- Variable Introduction -- + function Fresh - (This : in out Mu_World'Class) + (This : in out World'Class) return Term; function Fresh - (This : in out Mu_World'Class; + (This : in out World'Class; Name : in String) return Term; function Fresh - (This : in out Mu_World'Class; + (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) return Term; - + -- Unification -- function Unify - (This : in Mu_World; + (This : in World; Left : in Term'Class; Right : in Element_Type) - return Mu_World; + return World; procedure Unify - (This : in out Mu_World; + (This : in out World; Left : in Term'Class; Right : in Element_Type); function Unify - (This : in Mu_World; + (This : in World; Left, Right : in Term'Class) - return Mu_World; + return World; procedure Unify - (This : in out Mu_World; + (This : in out World; Left, Right : in Term'Class); - + -- Combining / Disjunction -- function Disjunct - (Left, Right : in Mu_World) - return Mu_World; + (Left, Right : in World) + return World; procedure Disjunct - (This : in out Mu_World; - Right : in Mu_World); + (This : in out World; + Right : in World); function Disjunct - (Inputs : in Mu_World_Array) - return Mu_World; + (Inputs : in World_Array) + return World; procedure Disjunct - (This : in out Mu_World; - Inputs : in Mu_World_Array); + (This : in out World; + Inputs : in World_Array); + + + -- Lazy Sequencing / Conjunction -- + + function Conjunct + (This : in World; + Func : in Conjunct_Zero_Func) + return World; + + procedure Conjunct + (This : in out World; + Func : in Conjunct_Zero_Func); + + function Conjunct + (This : in World; + Func : in Conjunct_One_Func; + Input : in Term'Class) + return World; + + procedure Conjunct + (This : in out World; + Func : in Conjunct_One_Func; + Input : in Term'Class); + + function Conjunct + (This : in World; + Func : in Conjunct_Many_Func; + Inputs : in Term_Array) + return World; + procedure Conjunct + (This : in out World; + Func : in Conjunct_Many_Func; + Inputs : in Term_Array); + + ------------------------- + -- Auxiliary Helpers -- + ------------------------- + + -- Infinite State Loops -- + function Recurse - (This : in Mu_World) - return Mu_World; + (This : in World) + return World; procedure Recurse - (This : in out Mu_World); - + (This : in out World); + -- Forced Evaluation -- function Take - (This : in Mu_World; + (This : in World; Count : in Natural) - return Mu_World; + return World; procedure Take - (This : in out Mu_World; + (This : in out World; Count : in Natural); procedure Force - (This : in out Mu_World; + (This : in out World; Count : in Positive); procedure Force_All - (This : in out Mu_World); + (This : in out World); function Failed - (This : in out Mu_World) + (This : in out World) return Boolean; + + + -------------------------- + -- miniKanren Prelude -- + -------------------------- + + -- caro -- + -- Inputs = List_Term & Head_Term + function Head + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 2; + + -- Inputs = List_Term & Head_Term + procedure Head + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- cdro -- + -- Inputs = List_Term & Tail_Term + function Tail + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 2; + + -- Inputs = List_Term & Tail_Term + procedure Tail + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- conso -- + -- Inputs = Head_Term & Tail_Term & List_Term + function Cons + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 3; + + -- Inputs = Head_Term & Tail_Term & List_Term + procedure Cons + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- nullo -- + + function Nil + (This : in World; + Nil_Term : in Term'Class) + return World; + + procedure Nil + (This : in out World; + Nil_Term : in Term'Class); + + + -- eqo -- + -- Skipped due to being a synonym for Unify + + + -- eq-caro -- + -- Skipped due to being a synonym for Head + + + -- pairo -- + + function Pair + (This : in World; + Pair_Term : in Term'Class) + return World; + + procedure Pair + (This : in out World; + Pair_Term : in Term'Class); + + + -- listo -- + + function Linked_List + (This : in World; + List_Term : in Term'Class) + return World; + + procedure Linked_List + (This : in out World; + List_Term : in Term'Class); + + + -- membero -- + -- Inputs = Item_Term & List_Term + function Member + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 2; + + -- Inputs = Item_Term & List_Term + procedure Member + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- rembero -- + -- Inputs = Item_Term & List_Term & Out_Term + function Remove + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 3; + + -- Inputs = Item_Term & List_Term & Out_Term + procedure Remove + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- appendo -- + -- Inputs = List_Term & Item_Term & Out_Term + function Append + (This : in World; + Inputs : in Term_Array) + return World + with Pre => Inputs'Length = 3; + + -- Inputs = List_Term & Item_Term & Out_Term + procedure Append + (This : in out World; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- anyo -- + -- Skipped due to Recurse doing the same thing + + + -- nevero -- + -- Skipped since it just creates a failed World + + + -- alwayso -- + -- Skipped due to Recurse doing the same thing + + private @@ -207,6 +423,8 @@ private Null_Term : constant Term := (Ada.Finalization.Controlled with Actual => null); + package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array); + @@ -231,7 +449,7 @@ private - type World_Access is access Mu_World'Class; + type World_Access is access World'Class; type World_Holder is new Ada.Finalization.Controlled with record Ptr : World_Access; @@ -247,7 +465,7 @@ private (This : in out World_Holder); function Hold - (This : in Mu_World'Class) + (This : in World'Class) return World_Holder; procedure Swap @@ -259,6 +477,9 @@ private Unify_Gen, Buffer_Gen, Disjunct_Gen, + Conjunct_Zero_Gen, + Conjunct_One_Gen, + Conjunct_Many_Gen, Recurse_Gen); type Generator (Kind : Generator_Kind := No_Gen) is record @@ -266,20 +487,31 @@ private when No_Gen => null; when Fresh_Gen => - Frs_World : World_Holder; - Frs_Name : SU.Unbounded_String; + Frs_World : World_Holder; + Frs_Name : SU.Unbounded_String; when Unify_Gen => - Uni_World : World_Holder; - Uni_Term1 : Term; - Uni_Term2 : Term; + Uni_World : World_Holder; + Uni_Term1 : Term; + Uni_Term2 : Term; when Buffer_Gen => - Buff_World : World_Holder; + Buff_World : World_Holder; when Disjunct_Gen => - Dis_World1 : World_Holder; - Dis_World2 : World_Holder; + Dis_World1 : World_Holder; + Dis_World2 : World_Holder; + when Conjunct_Zero_Gen => + ConZ_World : World_Holder; + ConZ_Func : Conjunct_Zero_Func; + when Conjunct_One_Gen => + ConO_World : World_Holder; + ConO_Func : Conjunct_One_Func; + ConO_Input : Term; + when Conjunct_Many_Gen => + ConM_World : World_Holder; + ConM_Func : Conjunct_Many_Func; + ConM_Inputs : Term_Array_Holders.Holder; when Recurse_Gen => - Rec_World : World_Holder; - Rec_Index : Positive; + Rec_World : World_Holder; + Rec_Index : Positive; end case; end record; @@ -287,27 +519,27 @@ private (Index_Type => Positive, Element_Type => State); - type Mu_World is tagged record + type World is tagged record Possibles : State_Vectors.Vector; Next_Ident : ID_Number; Engine : Generator; end record; function Has_State - (This : in out Mu_World; + (This : in out World; Index : in Positive) return Boolean; procedure Rollover - (This : in out Mu_World); + (This : in out World); procedure Roll_Until - (This : in out Mu_World; + (This : in out World; Index : in Positive); use type State_Vectors.Vector; - Empty_Mu_World : constant Mu_World := + Empty_World : constant World := (Possibles => State_Vectors.Empty_Vector & Empty_State, Next_Ident => 0, Engine => (Kind => No_Gen)); -- cgit