[Agda] Compile-time parsing

[Peter Thiemann]

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