summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/kompsos-prelude.adb148
-rw-r--r--src/kompsos-prelude.ads60
2 files changed, 204 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;
generated by cgit (git 2.30.0) at 2025-11-25 11:49:33 +0000