Hi all,
I'm in the process of adding a fancy GUI on top of a proof assistant
that should show the binding structure of extracted code in a manner
reminiscent of DrRacket's arrows. This is especially important because
the code extraction process makes use of the results of
make-syntax-introducer to control shadowing.
What I would like to do is to use the macro expander to discover the
actual binding structure of the high-level syntax. However, I'm not
having a lot of luck in figuring out how to do this. I imagine that if I
were doing this for real source code, I'd need to traverse the expanded
syntax and find identifiers for which syntax-original? answers in the
affirmative, and then work backwards using their source locations.
However, only small parts of the syntax objects that I'm interested in
are produced by read-syntax. The interesting parts are generated
programmatically from proof trees. Is there a good place to start on
using the macro expander for this?
In the worst case, I can have code extractors produce an AST whose
binding structure is directly apparent, use this for display purposes,
and then interpret the AST as a syntax object when it comes time to run
my program. But this would significantly complicate the process of
implementing a logic, so I'd prefer to use what's already there.
Thanks in advance!
/David
--
You received this message because you are subscribed to the Google Groups "Racket
Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
