[PATCH] fix position in 'enterInCache'

[Qian Yun]

Although this 'enterInCache' is not used in Kernel (the other
signature is used), this is still a logical error.

Because of the usage of DIFF elsewhere, we can not assume
"1 + cache_use" is the biggest position.

Instead, we should use logic like elsewhere: bump position
by DIFF.

- Qian

[Waldek Hebisch]

It is not clear to me if we should consider this to be a bug,
AFAICS the intent was to choose and use one of 'enterInCache'
functions, not both together. And if you really what to
mix them, then adding DIFF is not enough. Multiplying by
DIFF probably would be enough. But more sensible approach
would be to remove first 'enterInCache' from SortedCache
and possibly create a now domain, say 'LinearCache'
which do not require order and uses linear search.

> diff --git a/src/algebra/kl.spad b/src/algebra/kl.spad
> index 0365b60f..143f73c4 100644
> --- a/src/algebra/kl.spad
> +++ b/src/algebra/kl.spad
> @@ -116,7 +116,11 @@ SortedCache(S : CachableSet) : Exports == Implementation where
>
> enterInCache(x : S, equal? : S -> Boolean) ==
> (res := linearSearch(equal?)) case S => res
> - setPosition(x, 1 + cache_use)
> + if cache_use = 0 then
> + pos : N := DIFF
> + else
> + pos : N := DIFF + position cache(cache_use - 1)
> + setPosition(x, pos)
> insertAtEnd(x)
> x
>


--
Waldek Hebisch

[Qian Yun]

On 5/22/26 6:57 AM, Waldek Hebisch wrote:
> On Tue, May 19, 2026 at 09:00:47PM +0800, Qian Yun wrote:
>> Although this 'enterInCache' is not used in Kernel (the other
>> signature is used), this is still a logical error.
>>
>> Because of the usage of DIFF elsewhere, we can not assume
>> "1 + cache_use" is the biggest position.
>>
>> Instead, we should use logic like elsewhere: bump position
>> by DIFF.
>
> It is not clear to me if we should consider this to be a bug,
> AFAICS the intent was to choose and use one of 'enterInCache'
> functions, not both together. And if you really what to
> mix them, then adding DIFF is not enough. Multiplying by
> DIFF probably would be enough.

It is adding DIFF to the position of last element.
Since cache is ordered by position, this will perfectly be fine.

- Qian

[Qian Yun]

There's further logical errors in it:

If linearSearch fails to find x, then we should insert
x in the middle of cache, not always insert it at end.

- Qian

[Qian Yun]

Oh, I understand now. With linearSearch, there is no sense
of order, so it is impossible to insert in the middle like
binarySearch.

Yes, those 2 "enterInCache" should not be mixed.

- Qian

[Waldek Hebisch]

On Fri, May 22, 2026 at 07:52:29AM +0800, Qian Yun wrote:
> Oh, I understand now. With linearSearch, there is no sense
> of order, so it is impossible to insert in the middle like
> binarySearch.
>
> Yes, those 2 "enterInCache" should not be mixed.

Just extra remark: the first 'enterInCache' is only used in
MakeCachableSet where there is no assumption of order.

--
Waldek Hebisch