One other trick might be to have your parsing function return something like:<div><br></div><div>data ParseError (s : String) : Set where</div><div>-- no constructor</div><div><br></div><div>then your error message could even contain a string error message depending on what went wrong. Might be overkill here, but it could help if you have complicated parse errors.</div>
<div><br><div class="gmail_quote">On Thu, Dec 15, 2011 at 7:02 PM, Peter Thiemann <span dir="ltr"><<a href="mailto:thiemann@informatik.uni-freiburg.de">thiemann@informatik.uni-freiburg.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks to all who responded for your insightful suggestions!<br>
I'm settling for a variant of Alan's code because it's very simple and<br>
yields the most informative error message:<br>
<br>
record ParsedAs (E : Element) : Set where<br>
field<br>
s : String<br>
ok : T (s parsesAs E)<br>
<br>
⟪ : (E : Element) → (s : String) → (p : T (s parsesAs E)) → ParsedAs E<br>
⟪ E s p = record { s = s ; ok = p }<br>
⟫ = tt<br>
<br>
-- ok:bb42 = ⟪ Int "42" ⟫<br>
-- err:bbxx = ⟪ Int "xx" ⟫<br>
<br>
with the error message for err:bbxx being<br>
⊤ !=< ⊥ of type Set<br>
when checking that the expression ⟫ has type T ("xx" parsesAs Int)<span class="HOEnZb"><font color="#888888"><br>
<br>
-Peter</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On 12/16/11 3:32 AM, Alan Jeffrey wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Peter,<br>
<br>
Whenever I've done this, I've just used the yellow-ink version. Since Agda by default doesn't allow code with unsolved metas to be imported or compiled, it's not so bad.<br>
<br>
If you really really want a type error, the best I've managed to come up with is to use a variant of your code, but where p is an explicit parameter to intLiteral:<br>
<br>
intLiteral :<br>
(s : String) → (p : isTrue (isIntLiteral s)) → Parsed isIntLiteral<br>
intLiteral s p = record { s = s; yes = p }<br>
<br>
then define some shorthands:<br>
<br>
⟪ = intLiteral<br>
⟫ = tt<br>
<br>
so you can write:<br>
<br>
ok = ⟪"0"⟫<br>
nok = ⟪"a"⟫<br>
<br>
Not exactly brilliant, but it does give a type error for nok.<br>
<br>
A.<br>
<br>
On 12/14/2011 08:01 PM, Peter Thiemann wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi all,<br>
<br>
I want to statically ensure that a string constant has a certain format.<br>
That is, I want an ill-formatted constant to be a typing error.<br>
<br>
For example, suppose I wanted to ensure that certain string constants<br>
can be parsed as integers.<br>
Then there should be a function like this<br>
<br>
intLiteral : String -> ParsedIntLiteral<br>
<br>
such that<br>
<br>
intLiteral "42"<br>
<br>
is accepted, but<br>
<br>
intLiteral "foo"<br>
<br>
is a type error.<br>
<br>
I made a few attempts, but did not find a satisfactory solution, yet.<br>
Here is one:<br>
----------------<br>
<br>
isTrue : Bool → Set<br>
isTrue true = ⊤<br>
isTrue false = ⊥<br>
<br>
record Parsed (p : String → Bool) : Set where<br>
field<br>
s : String<br>
yes : isTrue (p s)<br>
<br>
intLiteral : (s : String) → {p : isTrue (isIntLiteral s)} → Parsed<br>
isIntLiteral<br>
intLiteral s {yes} = record { s = s; yes = p }<br>
<br>
i0 = intLiteral "0" -- ok<br>
ix = intLiteral "x" -- marked yellow because the implicit arg could not<br>
be inferred<br>
-- I'd like to turn this case into a type error<br>
-----------------<br>
Here is another<br>
-----------------<br>
<br>
intLiteral' : (s : String) → if isIntLiteral s then Parsed isIntLiteral<br>
else ⊥<br>
intLiteral' s with isIntLiteral s<br>
... | true = record { s = s }<br>
... | false = ?<br>
<br>
-- at the ? agda knows that the expected type is ⊥, but clearly I cannot<br>
produce an element here<br>
-----------------<br>
<br>
.... and a few other variations.<br>
<br>
Any suggestions?<br>
-Peter<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></blockquote>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>