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-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
>>>>>>>>>> ***@lists.chalmers.se
>>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>>>
>>>>>>>>> _______________________________________________
>>>>>>>>> Agda mailing list
>>>>>>>>> ***@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
>>>>>>>> ***@lists.chalmers.se
>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> ***@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
>>>>> ***@lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> ***@lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> ***@lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> ***@lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> ***@lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>