Questions tagged [abstract-syntax-tree]
Use this tag with abstract syntax trees.
6
questions
1
vote
2
answers
183
views
How to parse Lean 3(?) theorem statements to JSON AST
I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
- 1,062
0
votes
1
answer
20
views
Induction error on mutually defined types in Coq
I want to define two types that depend on each other
...
- 131
0
votes
1
answer
104
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 ...
- 269
1
vote
1
answer
342
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 ...
- 269
6
votes
0
answers
170
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 ...
- 199
8
votes
1
answer
173
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 ...
- 2,768