diff options
Diffstat (limited to 'src/kompsos.ads')
| -rw-r--r-- | src/kompsos.ads | 91 |
1 files changed, 9 insertions, 82 deletions
diff --git a/src/kompsos.ads b/src/kompsos.ads index 862b345..19cfeb8 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -6,10 +6,6 @@ -- See license.txt for further details -with - - Ada.Strings.Unbounded; - private with Ada.Containers.Indefinite_Holders, @@ -27,12 +23,6 @@ package Kompsos is -- Datatypes -- ----------------- - -- Variable Names -- - - subtype Nametag is Ada.Strings.Unbounded.Unbounded_String; - type Nametag_Array is array (Positive range <>) of Nametag; - - -- Terms -- type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term); @@ -67,11 +57,6 @@ package Kompsos is return Element_Type with Pre => This.Kind = Atom_Term; - function Name - (This : in Term) - return Nametag - with Pre => This.Kind = Var_Term; - function Left (This : in Term) return Term @@ -130,18 +115,6 @@ package Kompsos is with Post => Fresh'Result.Kind = Var_Term; function Fresh - (This : in out Goal'Class; - Name : in String) - return Term - with Post => Fresh'Result.Kind = Var_Term; - - function Fresh - (This : in out Goal'Class; - Name : in Nametag) - return Term - with Post => Fresh'Result.Kind = Var_Term; - - function Fresh (This : in out Goal'Class; Count : in Positive) return Term_Array @@ -149,14 +122,6 @@ package Kompsos is Fresh'Result'Length = Count and (for all Item of Fresh'Result => Item.Kind = Var_Term); - function Fresh - (This : in out Goal'Class; - Names : in Nametag_Array) - return Term_Array - with Post => - Fresh'Result'Length = Names'Length and - (for all Item of Fresh'Result => Item.Kind = Var_Term); - generic Verse : in out Goal; function Make_Fresh @@ -286,16 +251,6 @@ package Kompsos is (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; - @@ -452,33 +407,11 @@ package Kompsos is private - package SU renames Ada.Strings.Unbounded; - - - function "+" - (Item : in String) - return SU.Unbounded_String - renames SU.To_Unbounded_String; - - function "-" - (Item : in SU.Unbounded_String) - return String - renames SU.To_String; - - - - -- around 2^31 possible Variables should be enough for anybody, right? subtype Long_Natural is Long_Integer range 0 .. Long_Integer'Last; subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last; - type Generator_ID_Number is new Long_Natural; - type Variable_ID_Number is new Long_Natural; - - type Variable is record - Ident : Generator_ID_Number; - Name : Nametag; - end record; + type Variable is new Long_Natural; @@ -517,7 +450,8 @@ private function T (Item : in Variable) - return Term'Class; + return Term'Class + with Post => T'Result.Kind = Var_Term; function Var (This : in Term'Class) @@ -531,22 +465,16 @@ private - 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 => Nametag, - "=" => SU."="); + package Variable_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => Variable); package Binding_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Variable_ID_Number, + (Key_Type => Variable, Element_Type => Term); type State is record - Ident : ID_Number_Maps.Map; - LVars : Name_Vectors.Vector; + LVars : Variable_Vectors.Vector; Subst : Binding_Maps.Map; end record; @@ -555,8 +483,7 @@ private Element_Type => State); Empty_State : constant State := - (Ident => ID_Number_Maps.Empty_Map, - LVars => Name_Vectors.Empty_Vector, + (LVars => Variable_Vectors.Empty_Vector, Subst => Binding_Maps.Empty_Map); |