diff options
Diffstat (limited to 'src/kompsos.ads')
| -rw-r--r-- | src/kompsos.ads | 60 |
1 files changed, 36 insertions, 24 deletions
diff --git a/src/kompsos.ads b/src/kompsos.ads index cf4ba31..c336a41 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -14,8 +14,7 @@ private with Ada.Containers.Indefinite_Holders, Ada.Containers.Ordered_Maps, - Ada.Containers.Vectors, - Ada.Finalization; + Ada.Containers.Vectors; generic @@ -27,9 +26,6 @@ package Kompsos is -- Datatypes -- ----------------- - type Variable is private; - - type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term); type Term is tagged private; @@ -58,9 +54,9 @@ package Kompsos is return Element_Type with Pre => This.Kind = Atom_Term; - function Var + function Name (This : in Term) - return Variable + return Ada.Strings.Unbounded.Unbounded_String with Pre => This.Kind = Var_Term; function Left @@ -105,17 +101,20 @@ package Kompsos is function Fresh (This : in out World'Class) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; function Fresh (This : in out World'Class; Name : in String) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; function Fresh (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; -- Unification -- @@ -404,11 +403,14 @@ private - -- 2^32 possible Variables per World is enough for anybody, right? - type ID_Number is mod 2 ** 32; + -- around 2^31 possible Variables should be enough for anybody, right? + type ID_Number is new Long_Integer range 0 .. Long_Integer'Last; + + type Generator_ID_Number is new ID_Number; + type Variable_ID_Number is new ID_Number; type Variable is record - Ident : ID_Number; + Ident : Generator_ID_Number; Name : SU.Unbounded_String; end record; @@ -436,6 +438,11 @@ private Actual : Term_Holders.Holder; end record; + function Var + (This : in Term'Class) + return Variable + with Pre => This.Kind = Var_Term; + Empty_Term : constant Term := (Actual => Term_Holders.To_Holder (Term_Component'(Kind => Null_Term))); @@ -444,22 +451,28 @@ private - package Name_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => ID_Number, + package ID_Number_Maps is new Ada.Containers.Ordered_Maps + (Key_Type => Generator_ID_Number, + Element_Type => Variable_ID_Number); + + package Name_Vectors is new Ada.Containers.Vectors + (Index_Type => Variable_ID_Number, Element_Type => SU.Unbounded_String, "=" => SU."="); package Binding_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => ID_Number, + (Key_Type => Variable_ID_Number, Element_Type => Term); type State is record - LVars : Name_Maps.Map; + Ident : ID_Number_Maps.Map; + LVars : Name_Vectors.Vector; Subst : Binding_Maps.Map; end record; Empty_State : constant State := - (LVars => Name_Maps.Empty_Map, + (Ident => ID_Number_Maps.Empty_Map, + LVars => Name_Vectors.Empty_Vector, Subst => Binding_Maps.Empty_Map); @@ -501,6 +514,7 @@ private when No_Gen => null; when Fresh_Gen => + Frs_Ident : Generator_ID_Number; Frs_World : World_Holders.Holder; Frs_Name : SU.Unbounded_String; when Unify_Gen => @@ -534,9 +548,8 @@ private Element_Type => State); type World is new World_Root with record - Possibles : State_Vectors.Vector; - Next_Ident : ID_Number; - Engine : Generator; + Possibles : State_Vectors.Vector; + Engine : Generator; end record; function Has_State @@ -554,9 +567,8 @@ private use type State_Vectors.Vector; Empty_World : constant World := - (Possibles => State_Vectors.Empty_Vector & Empty_State, - Next_Ident => 0, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector & Empty_State, + Engine => (Kind => No_Gen)); end Kompsos; |