Questions tagged [abstract-syntax-tree]

Use this tag with abstract syntax trees.

Filter by
Sorted by
Tagged with
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 ...