Code for bottom up tree traversal and parser for terms str to AST about coqgym HOT 4 CLOSED

1. In the TermEncoder class, we calculate the node embeddings from bottom to top.
2. In the GallinaTermParser class, we use lark to parse the S-expressions of Coq terms into ASTs.

from coqgym.

1. In the TermEncoder class, we calculate the node embeddings from bottom to top.
2. In the GallinaTermParser class, we use lark to parse the S-expressions of Coq terms into ASTs.

Thanks! Also, do you embed individual symbols? (e.g. characters?) There are 128 chars so what is the point of embedding those? Asking after reading the paper, will attach relevant parts that are unclear to me:

from coqgym.

so do you embed symbols or use one hot vectors for them is basically my question.

from coqgym.

We use embeddings. See

where the embedding dimension is 256:

from coqgym.