diff options
Diffstat (limited to 'src/kompsos-prelude.adb')
| -rw-r--r-- | src/kompsos-prelude.adb | 244 |
1 files changed, 0 insertions, 244 deletions
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; - - |