<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Thanks , Guillaume.<br>
Now, I have a problem to print the result due to the IO functions
requesting Codata.Musical.Costring.<br>
I fail to write a function: Costring ∞ → Codata.Musical.Costring<br>
<br>
Dankon, Guillaume.<br>
Nun, mi havas problemon por afiŝi la resulton pro la IO-funkcioj
petas Codata.Musical.Costring.<br>
Mi fiaskas skribi funkcion: Costring ∞ → Codata.Musical.Costring
<p>Sincere,<br>
</p>
<div class="moz-cite-prefix">On 2018-08-05 10:24, Guillaume Allais
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:079d7494-f9ff-5fc0-fea1-9c4fa3a0c908@ens-lyon.org">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">
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:
</pre>
<blockquote type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">
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:
</pre>
<blockquote type="cite">
<pre wrap="">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
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr>
gpg --search-keys 0x67B17A3F
<br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
</body>
</html>