[Agda] Compile-time parsing

[gallais at ensl.org]

Hi Peter,

What about something like this?

Cheers,

--
gallais



On 15 December 2011 02: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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Parsing.agda
Type: application/octet-stream
Size: 2049 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111215/14b35ac6/Parsing.obj