Stream: Isabelle/ML

Topic: Embedded DSL: Parsing Identifiers Directly Into Strings

Andrew Chen (Aug 16 2025 at 01:58):

I want to embed (via mixfix operators and perhaps syntax and translation definitions ) a DSL with arbitrary identifiers, and ingest them as Isabelle strings. While my DSL can be parsed if I wrap all identifiers with quotations so they are auto-ingested as strings, that's ugly. Further, even if all identifiers in my DSL are disambiguated with a cleaner, special symbol, there still doesn't appear to be a straight path.

I think the following methods could work:

1. translation has access to outer syntax, so it's able to take in the special id, which doesn't seem to exist in the inner syntax level. With some additional ML code, could I directly convert an id to a string in a translation?
2. If identifiers are untouched when they come in, then perhaps they will be a Free/Bound variable, which can be intercepted with a proper Sign.parse_translation registration.

Is there an easier method? Would my proposed implementations work? Is there relevant code and docs I can be pointed to?

Thanks!
Andrew

Andrew Chen (Aug 16 2025 at 02:00):

To be perfectly clear, if my DSL fragment was:

Var a := 7;

I want a to be directly parsed into a string. I'm also cool if I must disambiguate with:

Var <a> := 7

or better yet, with a suffix symbol. Just not the quotations themselves:

Var ''a'' := 7 -- too much!

Last updated: Aug 20 2025 at 20:23 UTC