diff options
Diffstat (limited to 'src/kompsos.ads')
| -rw-r--r-- | src/kompsos.ads | 334 |
1 files changed, 283 insertions, 51 deletions
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)); |