Questions tagged [abstract-syntax-tree]
Use this tag with abstract syntax trees.
4
questions
0
votes
1
answer
95
views
How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?
Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages".
On PDF page 28 you'll see an OCaml ...
1
vote
1
answer
167
views
How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?
Question:
Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms.
I'm wondering whether Lean4 (or a typical well-known PA) just ...
5
votes
0
answers
136
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...
8
votes
1
answer
165
views
How to deal with the proliferation of encodings of ASTs?
When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...