[Agda] Compile-time parsing

[Wojciech Jedynak]

Hello,
I attach another approach.

Greetings,
Wojtek

2011/12/15 Peter Thiemann <thiemann at informatik.uni-freiburg.de>:
> Hi Ben,
>
> thanks for your suggestion.
> Not quite. You approach elegantly sidesteps the production of a value at
> type ⊥.
> However, its result type still incorporates the choice (yes/no) between a
> correctly parsed
> string and an invalid string. In contrast, I want
> intLiteral "foo"
> to be rejected as a type error just like
> intLiteral true.
>
> -Peter
>
>
>> Hi Peter, will this sort of thing do what you want?
>> - Ben
>>
>> On 15 December 2011 13:01, Peter Thiemann
>> <thiemann at informatik.uni-freiburg.de>  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
>>
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
A non-text attachment was scrubbed...
Name: str.agda
Type: application/octet-stream
Size: 755 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111215/a49f830e/str.obj