[Agda] Checking termination is not sufficiently exploratory.
Serge Leblanc
33dbqnxpy7if at gmail.com
Tue Aug 7 18:47:22 CEST 2018
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
--
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/20180807/add627b5/attachment.html>
-------------- next part --------------
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.String as String
hiding (fromList)
renaming (_==_ to _≛_ ; _++_ to _⊍_; show to showString) -- U+225B U+228D
open import Data.List as List hiding (_++_)
open import Relation.Nullary.Decidable
open import Data.Bool
open import Function
open import Codata.Colist
Costring : Size → Set
Costring = Colist Char
toCostring : String → Costring ∞
toCostring = fromList ∘′ toList
_:++_ : ∀ {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)
import Codata.Musical.Colist as CL
import Codata.Musical.Costring as CS
open import Coinduction using (♯_ ; ♭)
toMusical : Costring ∞ → CS.Costring
toMusical [] = CL.[]
toMusical (c ∷ cs) = c CL.∷ ♯ toMusical (cs .force)
open import IO using (run ; getContents ; _>>=_ ; putStrLn∞ ; mapM ; putStrLn)
main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘ toMusical ∘ coSplit″) (fromMusical s)
-------------- 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/20180807/add627b5/attachment.sig>
More information about the Agda
mailing list