[Agda] Checking termination is not sufficiently exploratory.

[Serge Leblanc]

Thanks , Guillaume.
Now, I have a problem to print the result due to the IO functions
requesting Codata.Musical.Costring.
I fail to write a function: Costring ∞ → Codata.Musical.Costring

Dankon, Guillaume.
Nun, mi havas problemon por afiŝi la resulton pro la IO-funkcioj petas
Codata.Musical.Costring.
Mi fiaskas skribi funkcion: Costring ∞ → Codata.Musical.Costring

Sincere,

On 2018-08-05 10:24, Guillaume Allais wrote:
> 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
>>
> _______________________________________________
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180806/7fed6e3b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180806/7fed6e3b/attachment.sig>