jonsterling / tt

secret project
17 stars 1 forks source link

source language #3

Open jonsterling opened 6 years ago

jonsterling commented 6 years ago

I'd like to have a very simple source language that's easy to parse, print and then elaborate to the term language. It'd be sweet if there was a way to hold onto source locations without things getting too gnarly.

jonsterling commented 6 years ago

(sexprs may be a good choice)

ghost commented 6 years ago

I don't know if you have seen it already or not but there is support for deriving serialization to and from s-expressions via ppx_deriving and ppx_sexp_conv.

For a more serious implementation using Menhir for parsing and Format for printing would be a better choice though. Menhir should support parsing with source locations. It is also possible to interleave Menhir parsing actions with an arbitrary monad.

jonsterling commented 6 years ago

Huh, sounds interesting... I do think that something like sexprs are the best choice, but I think I'd prefer to handroll it so that the notation doesn't have to coincide exactly with however we choose to represent things.

Also, I have this style of sexpr that I like which has a standardized notion of binding (like we use in redprl).