diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/kompsos-advanced_reify.adb | 147 | ||||
| -rw-r--r-- | src/kompsos-advanced_reify.ads | 69 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 14 | ||||
| -rw-r--r-- | src/kompsos.adb | 99 | ||||
| -rw-r--r-- | src/kompsos.ads | 30 |
5 files changed, 349 insertions, 10 deletions
diff --git a/src/kompsos-advanced_reify.adb b/src/kompsos-advanced_reify.adb new file mode 100644 index 0000000..42df1e7 --- /dev/null +++ b/src/kompsos-advanced_reify.adb @@ -0,0 +1,147 @@ + + +-- Programmed by Jedidiah Barber +-- Licensed under the Sunset License v1.0 + +-- See license.txt for further details + + +package body Kompsos.Advanced_Reify is + + + -- Term->Array Conversion -- + + function Flatten + (Item : in Term) + return Element_Array is + begin + case Item.Kind is + when Null_Term => + return (1 => Null_Element); + when Atom_Term => + return (1 => Item.Atom); + when Var_Term => + return (1 => Variable_Convert (Item)); + when Pair_Term => + if Item.Right = Empty_Term then + return Flatten (Item.Left); + else + return Flatten (Item.Left) & Flatten (Item.Right); + end if; + end case; + end Flatten; + + + + -- Term->Tree Conversion -- + + function To_Tree + (Item : in Term) + return Element_Trees.Tree is + begin + return Result : Element_Trees.Tree := Element_Trees.Empty_Tree do + case Item.Kind is + when Null_Term => + Result.Append_Child (Result.Root, Null_Element); + when Atom_Term => + Result.Append_Child (Result.Root, Item.Atom); + when Var_Term => + Result.Append_Child (Result.Root, Variable_Convert (Item)); + when Pair_Term => + declare + The_Subtree : Element_Trees.Tree := To_Tree (Item.Left); + The_Place : Element_Trees.Cursor; + begin + if Item.Left.Kind = Pair_Term then + Result.Insert_Child + (Result.Root, + Element_Trees.No_Element, + Null_Element, + The_Place); + else + The_Place := Result.Root; + end if; + Result.Splice_Children + (The_Place, + Element_Trees.No_Element, + The_Subtree, + The_Subtree.Root); + if Item.Right /= Empty_Term then + The_Subtree := To_Tree (Item.Right); + Result.Splice_Children + (Result.Root, + Element_Trees.No_Element, + The_Subtree, + The_Subtree.Root); + end if; + end; + end case; + end return; + end To_Tree; + + + + -- Tree Reification -- + + function Treeify + (Item : in Term; + Subst : in State) + return Element_Trees.Tree is + begin + return To_Tree (Item.Resolve (Subst)); + end Treeify; + + + function Treeify_First + (Subst : in State) + return Element_Trees.Tree is + begin + if Subst.LVars.Is_Empty then + return Element_Trees.Empty_Tree; + end if; + for Iter in Subst.Ident.Iterate loop + if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then + return Treeify (Term (T (Variable'( + Ident => ID_Number_Maps.Key (Iter), + Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), + Subst); + end if; + end loop; + return Element_Trees.Empty_Tree; + end Treeify_First; + + + function Treeify_First + (Subst : in State; + Name : in String) + return Element_Trees.Tree is + begin + return Treeify_First (Subst, +Name); + end Treeify_First; + + + function Treeify_First + (Subst : in State; + Name : in Nametag) + return Element_Trees.Tree + is + Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name); + begin + if Name_Index = Name_Vectors.No_Index then + return Element_Trees.Empty_Tree; + end if; + for Iter in Subst.Ident.Iterate loop + if ID_Number_Maps.Element (Iter) = Name_Index then + return Treeify (Term (T (Variable'( + Ident => ID_Number_Maps.Key (Iter), + Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), + Subst); + end if; + end loop; + return Element_Trees.Empty_Tree; + end Treeify_First; + + +end Kompsos.Advanced_Reify; + + diff --git a/src/kompsos-advanced_reify.ads b/src/kompsos-advanced_reify.ads new file mode 100644 index 0000000..ecda1c9 --- /dev/null +++ b/src/kompsos-advanced_reify.ads @@ -0,0 +1,69 @@ + + +-- Programmed by Jedidiah Barber +-- Licensed under the Sunset License v1.0 + +-- See license.txt for further details + + +with + + Ada.Containers.Multiway_Trees; + + +generic + type Element_Array is array (Positive range <>) of Element_Type; + + Null_Element : Element_Type; + + with function Variable_Convert + (Item : in Term) + return Element_Type is <>; + + -- Element_Trees must be passed in rather than instantiated inside the generic + -- due to an issue with implementation-defined Disable_Controlled aspect in GNAT. + with package Element_Trees is new Ada.Containers.Multiway_Trees + (Element_Type => Element_Type, + "=" => "="); +package Kompsos.Advanced_Reify is + + + -- Term->Array Conversion -- + + function Flatten + (Item : in Term) + return Element_Array; + + + -- Term->Tree Conversion -- + + function To_Tree + (Item : in Term) + return Element_Trees.Tree; + + + -- Tree Reification -- + + function Treeify + (Item : in Term; + Subst : in State) + return Element_Trees.Tree; + + function Treeify_First + (Subst : in State) + return Element_Trees.Tree; + + function Treeify_First + (Subst : in State; + Name : in String) + return Element_Trees.Tree; + + function Treeify_First + (Subst : in State; + Name : in Nametag) + return Element_Trees.Tree; + + +end Kompsos.Advanced_Reify; + + diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index 3d5963e..73e50db 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -14,12 +14,12 @@ package Kompsos.Pretty_Print is function Image - (Item : in Term) + (Item : in Integer) return String; function Image - (Item : in out World) + (Item : in Term) return String; @@ -33,6 +33,11 @@ package Kompsos.Pretty_Print is return String; + function Image + (Item : in out World) + return String; + + function Image_Constant (Item : in World) return String; @@ -42,11 +47,6 @@ private function Image - (Item : in Integer) - return String; - - - function Image (Item : in ID_Number) return String; diff --git a/src/kompsos.adb b/src/kompsos.adb index 1370f37..d973452 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -35,9 +35,9 @@ package body Kompsos is function T (Item : in Variable) - return Term is + return Term'Class is begin - return (Actual => Term_Holders.To_Holder (Term_Component'( + return Term'(Actual => Term_Holders.To_Holder (Term_Component'( Kind => Var_Term, Refer => Item))); end T; @@ -436,7 +436,7 @@ package body Kompsos is is My_ID : constant Generator_ID_Number := Next_Gen; begin - return My_Term : constant Term := T (Variable'(Ident => My_ID, Name => Name)) do + return My_Term : constant Term := Term (T (Variable'(Ident => My_ID, Name => Name))) do This.Engine := (Kind => Fresh_Gen, Frs_Ident => My_ID, @@ -706,6 +706,19 @@ package body Kompsos is end Take_First; + function Take_All + (This : in out World) + return State_Array is + begin + This.Force_All; + return Result : State_Array (1 .. Natural (This.Possibles.Length)) do + for Index in Result'Range loop + Result (Index) := This.Possibles.Element (Index); + end loop; + end return; + end Take_All; + + procedure Force (This : in out World; Count : in Positive) is @@ -732,6 +745,86 @@ package body Kompsos is + -- Reification -- + + function Resolve + (This : in Term; + Subst : in State) + return Term + is + use type SU.Unbounded_String; + begin + case This.Kind is + when Null_Term | Atom_Term => + return This; + when Var_Term => + if Subst.Ident.Contains (This.Var.Ident) and then + Subst.Ident.Element (This.Var.Ident) in + Subst.LVars.First_Index .. Subst.LVars.Last_Index and then + Subst.LVars.Element (Subst.Ident.Element (This.Var.Ident)) = This.Name and then + Subst.Subst.Contains (Subst.Ident.Element (This.Var.Ident)) + then + return Subst.Subst.Element (Subst.Ident.Element (This.Var.Ident)).Resolve (Subst); + else + return This; + end if; + when Pair_Term => + return T (This.Left.Resolve (Subst), This.Right.Resolve (Subst)); + end case; + end Resolve; + + + function Resolve_First + (Subst : in State) + return Term is + begin + if Subst.LVars.Is_Empty then + return Empty_Term; + end if; + for Iter in Subst.Ident.Iterate loop + if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then + return Resolve (Term (T (Variable'( + Ident => ID_Number_Maps.Key (Iter), + Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), + Subst); + end if; + end loop; + return Empty_Term; + end Resolve_First; + + + function Resolve_First + (Subst : in State; + Name : in String) + return Term is + begin + return Resolve_First (Subst, +Name); + end Resolve_First; + + + function Resolve_First + (Subst : in State; + Name : in Nametag) + return Term + is + Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name); + begin + if Name_Index = Name_Vectors.No_Index then + return Empty_Term; + end if; + for Iter in Subst.Ident.Iterate loop + if ID_Number_Maps.Element (Iter) = Name_Index then + return Resolve (Term (T (Variable'( + Ident => ID_Number_Maps.Key (Iter), + Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), + Subst); + end if; + end loop; + return Empty_Term; + end Resolve_First; + + + -------------------------- -- miniKanren Prelude -- diff --git a/src/kompsos.ads b/src/kompsos.ads index 89ea88b..3164996 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -256,6 +256,10 @@ package Kompsos is (This : in out World) return State; + function Take_All + (This : in out World) + return State_Array; + procedure Force (This : in out World; Count : in Positive); @@ -268,6 +272,28 @@ package Kompsos is return Boolean; + -- Reification -- + + function Resolve + (This : in Term; + Subst : in State) + return Term; + + function Resolve_First + (Subst : in State) + return Term; + + function Resolve_First + (Subst : in State; + Name : in String) + return Term; + + function Resolve_First + (Subst : in State; + Name : in Nametag) + return Term; + + -------------------------- @@ -474,6 +500,10 @@ private Actual : Term_Holders.Holder; end record; + function T + (Item : in Variable) + return Term'Class; + function Var (This : in Term'Class) return Variable |