diff options
| -rw-r--r-- | src/kompsos-prelude.adb | 148 | ||||
| -rw-r--r-- | src/kompsos-prelude.ads | 60 | ||||
| -rw-r--r-- | test/membero.adb | 53 | ||||
| -rw-r--r-- | tests.gpr | 2 |
4 files changed, 259 insertions, 4 deletions
diff --git a/src/kompsos-prelude.adb b/src/kompsos-prelude.adb index 6cb8b2b..58b80f4 100644 --- a/src/kompsos-prelude.adb +++ b/src/kompsos-prelude.adb @@ -15,10 +15,11 @@ package body Kompsos.Prelude is return World is begin return Result : World := This do - Result.Unify (T (Head_Term & T (Result.Fresh)), Full_List); + Result.Unify (T (Term (Head_Term), T (Result.Fresh)), Full_List); end return; end Head; + procedure Head (This : in out World; Full_List, Head_Term : in Term'Class) is @@ -27,16 +28,19 @@ package body Kompsos.Prelude is 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 (T (Result.Fresh) & Tail_Term), Full_List); + Result.Unify (T (T (Result.Fresh), Term (Tail_Term)), Full_List); end return; end Tail; + procedure Tail (This : in out World; Full_List, Tail_Term : in Term'Class) is @@ -45,16 +49,19 @@ package body Kompsos.Prelude is 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); + Result.Unify (T (Term (Head_Term), 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 @@ -63,6 +70,8 @@ package body Kompsos.Prelude is end Cons; + + function Nil (This : in World; Nil_Term : in Term'Class) @@ -73,6 +82,7 @@ package body Kompsos.Prelude is end return; end Nil; + procedure Nil (This : in out World; Nil_Term : in Term'Class) is @@ -81,16 +91,19 @@ package body Kompsos.Prelude is end Nil; + + function Pair (This : in World; Pair_Term : in Term'Class) return World is begin return Result : World := This do - Result.Unify (T (T (Result.Fresh), T (Result.Fresh)), Pair_Term); + Cons (Result, T (Result.Fresh), T (Result.Fresh), Pair_Term); end return; end Pair; + procedure Pair (This : in out World; Pair_Term : in Term'Class) is @@ -99,6 +112,133 @@ package body Kompsos.Prelude is end Pair; + + + function Linked_List + (This : in World; + List_Term : in Term'Class) + return World + is + Result_Nil, Result_Pair : World := This; + Ref_Term : constant Term := T (Result_Pair.Fresh); + begin + Nil (Result_Nil, List_Term); + + Pair (Result_Pair, List_Term); + Tail (Result_Pair, List_Term, Ref_Term); + if not Result_Pair.Failed then + Linked_List (Result_Pair, Ref_Term); + end if; + + return Disjunct (Result_Nil, Result_Pair); + end Linked_List; + + + procedure Linked_List + (This : in out World; + List_Term : in Term'Class) is + begin + This := Linked_List (This, List_Term); + end Linked_List; + + + + + function Member + (This : in World; + Item_Term, List_Term : in Term'Class) + return World + is + Result_Head, Result_Rest : World := This; + Ref_Term : constant Term := T (Result_Rest.Fresh); + begin + Head (Result_Head, List_Term, Item_Term); + + Tail (Result_Rest, List_Term, Ref_Term); + if not Result_Rest.Failed then + Member (Result_Rest, Item_Term, Ref_Term); + end if; + + return Disjunct (Result_Head, Result_Rest); + end Member; + + + procedure Member + (This : in out World; + Item_Term, List_Term : in Term'Class) is + begin + This := Member (This, Item_Term, List_Term); + end Member; + + + + + function Remove + (This : in World; + Item_Term, List_Term, Out_Term : in Term'Class) + return World + is + Result_Head, Result_Rest : World := This; + Left : constant Term := T (Result_Rest.Fresh); + Right : constant Term := T (Result_Rest.Fresh); + Rest : constant Term := T (Result_Rest.Fresh); + begin + Head (Result_Head, List_Term, Item_Term); + Tail (Result_Head, List_Term, Out_Term); + + -- infinite loops if run in reverse with vars for item and list + -- probably needs lazy conjunction to work properly + Cons (Result_Rest, Left, Right, List_Term); + if not Result_Rest.Failed then + Remove (Result_Rest, Item_Term, Right, Rest); + Cons (Result_Rest, Left, Rest, Out_Term); + end if; + + return Disjunct (Result_Head, Result_Rest); + end Remove; + + + procedure Remove + (This : in out World; + Item_Term, List_Term, Out_Term : in Term'Class) is + begin + This := Remove (This, 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 + Result_Nil, Result_Rest : World := This; + Left : constant Term := T (Result_Rest.Fresh); + Right : constant Term := T (Result_Rest.Fresh); + Rest : constant Term := T (Result_Rest.Fresh); + begin + Nil (Result_Nil, List_Term); + Unify (Result_Nil, Item_Term, Out_Term); + + Cons (Result_Rest, Left, Right, List_Term); + Cons (Result_Rest, Left, Rest, Out_Term); + if not Result_Rest.Failed then + Append (Result_Rest, Right, Item_Term, Rest); + end if; + + return Disjunct (Result_Nil, Result_Rest); + end Append; + + + procedure Append + (This : in out World; + List_Term, Item_Term, Out_Term : in Term'Class) is + begin + This := Append (This, List_Term, Item_Term, Out_Term); + end Append; + + end Kompsos.Prelude; diff --git a/src/kompsos-prelude.ads b/src/kompsos-prelude.ads index 5dbc562..237edbf 100644 --- a/src/kompsos-prelude.ads +++ b/src/kompsos-prelude.ads @@ -78,6 +78,66 @@ package Kompsos.Prelude is 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 + + end Kompsos.Prelude; diff --git a/test/membero.adb b/test/membero.adb new file mode 100644 index 0000000..694410d --- /dev/null +++ b/test/membero.adb @@ -0,0 +1,53 @@ + + +-- Programmed by Jedidiah Barber +-- Licensed under the Sunset License v1.0 + +-- See license.txt for further details + + +with + + Ada.Strings.Unbounded, + Ada.Text_IO, + Kompsos.Prelude, + Kompsos.Pretty_Print; + + +procedure Membero is + + package SU renames Ada.Strings.Unbounded; + package TIO renames Ada.Text_IO; + + function "+" + (Item : in String) + return SU.Unbounded_String + renames SU.To_Unbounded_String; + + + package InKomp is new Kompsos (SU.Unbounded_String); + use InKomp; + + package Prelude is new InKomp.Prelude; + package Printer is new InKomp.Pretty_Print (SU.To_String); + + Verse : World := Empty_World; + + Test_Item : constant Term := T (T (+"one") & T (+"two") & T (+"three") & T (+"four")); + +begin + + TIO.Put_Line ("Test program to check if membero, and hence recursion, is working."); + TIO.Put_Line ("Not currently designed to check for infinite recursion."); + TIO.New_Line; + TIO.Put_Line ("Should find all possible members of (one two three four)"); + + TIO.New_Line; + + Prelude.Member (Verse, T (Verse.Fresh ("result")), Test_Item); + + TIO.Put_Line (Printer.Image (Verse)); + +end Membero; + + @@ -18,11 +18,13 @@ project Tests is for Main use ("ab.adb", "fivesix.adb", + "membero.adb", "pprint.adb"); package Builder is for Executable ("ab.adb") use "ab"; for Executable ("fivesix.adb") use "fivesix"; + for Executable ("membero.adb") use "membero"; for Executable ("pprint.adb") use "pprint"; for Default_Switches ("Ada") use |