Natools

Check-in [ec19d3153c]
Login

Check-in [ec19d3153c]

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:smaz_generic: brind the predicate back as a separate function

Since Smaz dictionaries are meant to be global hard-coded constant objects, it makes sense to check the precondition only once, e.g. in a test suite, and not for each and every subprogram call.

Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1: ec19d3153c5a00753d16e48b082c52910c5d07a2
User & Date: nat 2016-12-14 20:01:08.776
Context
2016-12-15
20:12
tools/smaz: use the new validation function instead of ad-hoc code check-in: 3a95d52c86 user: nat tags: trunk
2016-12-14
20:01
smaz_generic: brind the predicate back as a separate function

Since Smaz dictionaries are meant to be global hard-coded constant objects, it makes sense to check the precondition only once, e.g. in a test suite, and not for each and every subprogram call. check-in: ec19d3153c user: nat tags: trunk

2016-12-13
22:09
smaz_generic: remove the too-costly dynamic predicate check-in: 7ae85f4e93 user: nat tags: trunk
Changes
Unified Diff Ignore Whitespace Patch
Changes to src/natools-smaz_generic.ads.
︙︙
111
112
113
114
115
116
117













118
119
120
121
122
123
124

     (Dict : in Dictionary;
      Code : in Dictionary_Code)
     return Positive
     is (1 + Code_Last (Dict.Offsets, Code, Dict.Values'Last)
           - Code_First (Dict.Offsets, Code, Dict.Values'First))
     with Pre => Is_Valid_Code (Dict, Code);
      --  Return the length of the string for at the given Index in Dict















   function Compressed_Upper_Bound
     (Dict : in Dictionary;
      Input : in String)
     return Ada.Streams.Stream_Element_Count;
      --  Return the maximum number of bytes needed to encode Input








>
>
>
>
>
>
>
>
>
>
>
>
>








111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

     (Dict : in Dictionary;
      Code : in Dictionary_Code)
     return Positive
     is (1 + Code_Last (Dict.Offsets, Code, Dict.Values'Last)
           - Code_First (Dict.Offsets, Code, Dict.Values'First))
     with Pre => Is_Valid_Code (Dict, Code);
      --  Return the length of the string for at the given Index in Dict

   function Is_Valid (Dictionary : in Smaz_Generic.Dictionary) return Boolean
     is ((for all Code in Dictionary.Offsets'Range
            => Dictionary.Offsets (Code) in Dictionary.Values'Range)
        and then (for all Code in Dictionary_Code'First .. Dictionary.Last_Code
            => Code_Last (Dictionary.Offsets, Code, Dictionary.Values'Last) + 1
               - Code_First (Dictionary.Offsets, Code, Dictionary.Values'First)
               in 1 .. Dictionary.Max_Word_Length)
        and then (for all Code in Dictionary_Code'First .. Dictionary.Last_Code
            => Dictionary_Code'Val (Dictionary.Hash
                                      (Dict_Entry (Dictionary, Code)))
               = Code));
      --  Check all the assumptions made on Dictionary objects.


   function Compressed_Upper_Bound
     (Dict : in Dictionary;
      Input : in String)
     return Ada.Streams.Stream_Element_Count;
      --  Return the maximum number of bytes needed to encode Input
︙︙