[Agda] Compile-time parsing

[Peter Thiemann]

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