Why is there a need for a Gallina parser if the term encoder is able to create embeddings for using sexp?

[brando90]

I was able to generate an embedding using sexp and the ASTactic term encoder.
So I am wondering what is the need for a GallinaTermParser (using lark)? I see it does a bunch of other things but I am unable to appreciate their use. Can it be clarified why sexp alone is not enough?

Sample code:

...
 #build tree with S-expression
    root = traverse_sexprs(s_expression)
    maintain_height(root)
    print('\n\n-------------------------------postorder traversal---------------------------')
    print_postorder(root)
    opts = parse_args()
    term_encoder = TermEncoder(opts)
    asts = []
    asts.append(root)
    all_embeddings = term_encoder(asts)
    print('\n\n---------------------------------embeddings-----------------------------------')
    print(all_embeddings)

[yangky11]

It is used to parse an S-expression into the AST of a term. Sure, the S-expression is already a tree and you could parse it trivially using a general-purpose parser for S-expressions, such as sexpdata.

However, you will not get Coq-specific type information from the S-expression alone. For example, if the S-expression is (Dash 0), from Coq's implementation we know that it's actually a proof_bullet defined in:

CoqGym/coq/proofs/proof_bullet.ml

Lines 13 to 16 in 4c205a7

	type t =
	| Dash of int
	| Star of int
	| Plus of int

Parsing the S-expression with sexpdata will not get that information. But we coded the information in gallina.py and vernac_types.py.

CoqGym/vernac_types.py

Lines 1968 to 1980 in 4c205a7

	class Vernacexpr__bullet(Variant):
	'''
	type bullet =
	| Dash of int
	| Star of int
	| Plus of int
	'''
	def __init__(self):
	self.constructors = OrderedDict({
	'Dash': Int(),
	'Star': Int(),
	'Plus': Int(),
	})

So using GallinaTermParser to parse (Dash 0) will produce a node labeled vernacexpr__bullet

[yangky11]

Yes, exactly!

[brando90]

@yangky11 I am curious Kaiyu (will number questions to easy responding):

1. why do you need the Gallina parser? what extra information is it providing that sexpdata doesn't already give us?
2. why can't you use the format that SerAPI already gives us?

I am also asking because that seems like a non-trivial amount of code and processing and trying to understand what is essential.

Thanks again for your openness to chat about your work.

[yangky11]

I think they are essentially the same question. We don't use the output of SerAPI directly because the Gallina parser can extract extra information. For example, without the Gallina parser, you won't know (Dash 0) and (Star 0) both belong to the same type (bullet ).

[brando90]

@yangky11 let me see if I understand this (sorry took me some time to really figure out what I wanted to ask). So just using a sexpdata doesn't provide the information your Gallina parser provides to the model, right? I am curious of why is that? If you get the individual tokens from sexpdata isn't that enough?

Thanks for responses!

[yangky11]

Yes, S-expressions alone do not provide all information about the object being serialized. Here explains the mechanism used by SerAPI to serialize internal Coq structures (which are OCaml objects). The complete information of an OCaml object can be captured by the definition of the object + its S-expression, not by the S-expression alone.