[Agda] Compile-time parsing

[Alan Jeffrey]

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