[Agda] Checking termination is not sufficiently exploratory.

[Guillaume Allais]

Hi Serge,

Using the new-style codata based on sized types which is available in the
latest standard library, you could write something like [see below].

Notice the type of `_:++_`: the second argument is a `Thunk` and because
the string is non-empty it's fine: we can guarantee it'll be used in a
guarded position.

Cheers,
--
gallais

==========================================================================
module Costring where

open import Size
open import Codata.Thunk
open import Data.Nat as Nat
open import Data.Char
open import Data.String hiding (fromList ; _++_ ; _==_)
open import Data.List as List hiding (_++_)
open import Relation.Nullary.Decidable
open import Data.Bool
open import Function

data Costring (i : Size) : Set where
  []  : Costring i
  _∷_ : Char → Thunk Costring i → Costring i

fromList : List Char → Costring ∞
fromList []       = []
fromList (x ∷ xs) = x ∷ λ where .force → fromList xs

toCostring : String → Costring ∞
toCostring = fromList ∘′ toList

_++_ : ∀ {i} → Costring i → Costring i → Costring i
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys

_:++_ : ∀ {i} (str : List Char) {_ : False (List.length str Nat.≟ 0)} →
       Thunk Costring i → Costring i
_:++_ []        {()} xs
_:++_ (x ∷ str) {pr} xs = x ∷ λ where .force → fromList str ++ xs .force

coSplit″ : ∀ {i} → Costring i → Costring i
coSplit″ [] = []
coSplit″ (x ∷ xs) with x == '!'
... | false = x ∷ λ where .force → coSplit″ (xs .force)
... | true = toList ">>" :++ λ where .force → coSplit″ (xs .force)
==========================================================================

On 03/08/18 20:57, Serge Leblanc wrote:
> Would an expert help me to improve the termination checking algorithm?
> Does someone already work to improve the algorithm?
> 
> Ĉu spertulo bonvolus helpi min aldoni ŝanĝon al la finiĝokontrola algoritmo?
> Ĉu iu jam laboras por plibonigi la algoritmon?
> 
> Sincere
> 
>  
> On 2018-07-31 03:02, Serge Leblanc wrote:
>> In my opinion, a normal form verification phase could be added without
>> changing the termination checking algorithm.
>> Laŭ mi, normala kontrola fazo povus esti aldonita sen ŝangi la finiĝan
>> kontrolan algoritmon.
>>
>> Sincere
>>
>>
>> On 2018-07-30 20:06, a.j.rouvoet wrote:
>>>
>>> I believe that you are right that the two snippets are equivalent,
>>> but it requires some computation to show that this is the case.
>>> The check that Agda runs on the other hand is very syntactic. This is
>>> indeed a limitation, but at least it ensures that checking for
>>> termination terminates ;-)
>>>
>>> On 07/30/2018 06:04 PM, Serge Leblanc wrote:
>>>> Yes, but you translat the code (toCostring ">>") ++ coSplit "(♭ xs)
>>>> to its normal form, it equals to '>' ∷ ♯ ('>' ∷ ♯ coSplit '(♭ xs)).
>>>> Right?
>>>> So, the recursive call is well protected by a constructor.
>>>>
>>>> Jes, sed vi plenumas la kodon (toCostring ">>") ++ coSplit″ (♭ xs)
>>>> ĝis sia normala formo, ĝi egalas al  '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭
>>>> xs)). Ĉu ne ?
>>>> Do, la memsinkceva alvoko estas bone ŝirmi per konstruisto.
>>>>
>>>> On 2018-07-30 16:59, a.j.rouvoet wrote:
>>>>>
>>>>> For coSplit to pass the checker, the recursive invocation must
>>>>> appear guarded by a constructor.
>>>>> This is clearly the case in coSplit', but not necessarily in
>>>>> coSplit'' (e.g. when toString ">>" returns the empty costring).
>>>>>
>>>>>
>>>>> On 07/30/2018 04:55 PM, Serge Leblanc wrote:
>>>>>> Dear all,
>>>>>> Why the checking termination rejects the coSplit" function
>>>>>> although the coSplit' function is accepted ?
>>>>>> Why the checking termination so suspicious?
>>>>>> Sincerely
>>>>>>
>>>>>> Estimataj ĉiuj,
>>>>>> Kial la finiĝa kontrolo malakceptas la funkcion coSplit″ kvankam
>>>>>> la funkcio coSplit′ trafas ?
>>>>>> Kial la finiĝa kontrolo estas tiel malakceptanda ?
>>>>>> Sincere
>>>>>>
>>>>>>   coSplit′ : Costring → Costring
>>>>>>   coSplit′ [] = []
>>>>>>   coSplit′ (x ∷ xs) with x ≐ '!'
>>>>>>   ... | false = x ∷ ♯ coSplit′ (♭ xs)
>>>>>>   ... | true = '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs))
>>>>>>
>>>>>>   coSplit″ : Costring → Costring
>>>>>>   coSplit″ [] = []
>>>>>>   coSplit″ (x ∷ xs) with x ≐ '!'
>>>>>>   ... | false = x ∷ ♯ coSplit″ (♭ xs)
>>>>>>   ... | true = (toCostring ">>") ++ coSplit″ (♭ xs)
>>>>>>
>>>>>>   main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘ coSplit′) s
>>>>>>
>>>>>> -- 
>>>>>> Serge Leblanc
>>>>>> ------------------------------------------------------------------------
>>>>>> gpg --search-keys 0x67B17A3F
>>>>>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>>>>>
>>>>>>
>>>>>> _______________________________________________
>>>>>> Agda mailing list
>>>>>> Agda at lists.chalmers.se
>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda at lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>> -- 
>>>> Serge Leblanc
>>>> ------------------------------------------------------------------------
>>>> gpg --search-keys 0x67B17A3F
>>>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>>>
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>> -- 
>> Serge Leblanc
>> ------------------------------------------------------------------------
>> gpg --search-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>