[Agda] Compile-time parsing

[Daniel Peebles]

One other trick might be to have your parsing function return something
like:

data ParseError (s : String) : Set where
-- no constructor

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.

On Thu, Dec 15, 2011 at 7:02 PM, Peter Thiemann <
thiemann at informatik.uni-freiburg.de> wrote:

> Thanks to all who responded for your insightful suggestions!
> I'm settling for a variant of Alan's code because it's very simple and
> yields the most informative error message:
>
> record ParsedAs (E : Element) : Set where
>  field
>    s : String
>    ok : T (s parsesAs E)
>
> ⟪ : (E : Element) → (s : String) → (p : T (s parsesAs E)) → ParsedAs E
> ⟪ E s p = record { s = s ; ok = p }
> ⟫ = tt
>
> -- ok:bb42 = ⟪ Int "42" ⟫
> -- err:bbxx = ⟪ Int "xx" ⟫
>
> with the error message for err:bbxx being
> ⊤ !=< ⊥ of type Set
> when checking that the expression ⟫ has type T ("xx" parsesAs Int)
>
> -Peter
>
>
>
> On 12/16/11 3:32 AM, Alan Jeffrey wrote:
>
>> Hi Peter,
>>
>> 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.
>>
>> 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:
>>
>> intLiteral :
>>  (s : String) → (p : isTrue (isIntLiteral s)) → Parsed isIntLiteral
>> intLiteral s p = record { s = s; yes = p }
>>
>> then define some shorthands:
>>
>> ⟪ = intLiteral
>> ⟫ = tt
>>
>> so you can write:
>>
>> ok = ⟪"0"⟫
>> nok = ⟪"a"⟫
>>
>> Not exactly brilliant, but it does give a type error for nok.
>>
>> A.
>>
>> On 12/14/2011 08:01 PM, Peter Thiemann wrote:
>>
>>> Hi all,
>>>
>>> I want to statically ensure that a string constant has a certain format.
>>> That is, I want an ill-formatted constant to be a typing error.
>>>
>>> For example, suppose I wanted to ensure that certain string constants
>>> can be parsed as integers.
>>> Then there should be a function like this
>>>
>>> intLiteral : String ->  ParsedIntLiteral
>>>
>>> such that
>>>
>>> intLiteral "42"
>>>
>>> is accepted, but
>>>
>>> intLiteral "foo"
>>>
>>> is a type error.
>>>
>>> I made a few attempts, but did not find a satisfactory solution, yet.
>>> Here is one:
>>> ----------------
>>>
>>> isTrue : Bool → Set
>>> isTrue true = ⊤
>>> isTrue false = ⊥
>>>
>>> record Parsed (p : String → Bool) : Set where
>>>    field
>>>      s : String
>>>      yes : isTrue (p s)
>>>
>>> intLiteral : (s : String) → {p : isTrue (isIntLiteral s)} → Parsed
>>> isIntLiteral
>>> intLiteral s {yes} = record { s = s; yes = p }
>>>
>>> i0 = intLiteral "0" -- ok
>>> ix = intLiteral "x" -- marked yellow because the implicit arg could not
>>> be inferred
>>>                             -- I'd like to turn this case into a type
>>> error
>>> -----------------
>>> Here is another
>>> -----------------
>>>
>>> intLiteral' : (s : String) → if isIntLiteral s then Parsed isIntLiteral
>>> else ⊥
>>> intLiteral' s with isIntLiteral s
>>> ... | true = record { s = s }
>>> ... | false = ?
>>>
>>> -- at the ? agda knows that the expected type is ⊥, but clearly I cannot
>>> produce an element here
>>> -----------------
>>>
>>> .... and a few other variations.
>>>
>>> Any suggestions?
>>> -Peter
>>>
>>>
>>> ______________________________**_________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>>
>>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111215/2b8b352e/attachment.html