[Agda] Checking termination is not sufficiently exploratory.

Tue Aug 7 21:08:23 CEST 2018

Wow this bug has been around since October 2016 and we somehow missed
Wen Kokke's report in February 2017.

I have pushed a fix:
https://github.com/agda/agda-stdlib/commit/81a7acad600dfe6d3958f5551e5f48432f98f1a2

Cheers,
--
gallais

On 07/08/18 18:47, Serge Leblanc wrote:
> HiGuillaume, the compilation fails :
> Saluton Guillaume, la kompilado fiaskas :
> 
> serge at serge-UX305FA:~/agda/parser$ agda --compile ./Costring.agda
> Compiling Costring in /home/serge/agda/parser/Costring.agdai to
> /home/serge/agda/parser/MAlonzo/Code/Costring.hs
> Calling: ghc -O -o /home/serge/agda/parser/Costring -Werror
> -i/home/serge/agda/parser -main-is MAlonzo.Code.Costring
> /home/serge/agda/parser/MAlonzo/Code/Costring.hs --make
> -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
> [88 of 91] Compiling MAlonzo.Code.Codata.Musical.Stream (
> MAlonzo/Code/Codata/Musical/Stream.hs,
> MAlonzo/Code/Codata/Musical/Stream.o )
> Compilation error:
> 
> MAlonzo/Code/Codata/Musical/Stream.hs:22:18: error:
>     • Expecting one fewer argument to ‘AgdaStream a0’
>       Expected kind ‘k1 -> k0’, but ‘AgdaStream a0’ has kind ‘*’
>     • In the type ‘AgdaStream a0 a1’
>       In the type declaration for ‘T10’
> 
> 
> On 2018-08-06 22:24, Guillaume Allais wrote:
>> Hi Serge,
>>
>> This is how I would do it:
>>
>> ===============================================================
>> open import Coinduction using (♯_)
>> import Codata.Musical.Colist as CL
>> import Codata.Musical.Costring as CS
>>
>> toMusical : Costring ∞ → CS.Costring
>> toMusical []       = CL.[]
>> toMusical (c ∷ cs) = c CL.∷ ♯ toMusical (cs .force)
>> ===============================================================
>>
>> Note that it's also probably worth replacing my ad-hoc definition of
>> `Costring` with `Colist Char` where `Colist` comes from `Codata.Colist`.
>> This way `fromList` and `_++_` are readily available. We also have
>> `fromMusical` but I see that we are missing `toMusical`. I'll send a PR.
>>
>> Cheers,
>> --
>> gallais
>>
>>
>>
>> On 06/08/18 18:50, Serge Leblanc wrote:
>>> 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
>>>
>>>
>>> _______________________________________________
>>> 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
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180807/5dd82dfe/attachment.sig>