Removing tokens in gallina.py

[tlringer]

Hello,

I'm currently working off of a codebase that uses gallina.py from CoqGym to parse ASTs. I noticed that compute_height_remove_toekn removes a lot of information, like names, dirpaths, modpaths, particular debruijn indices, and particular inductive types. It seems from the name that this is deliberate, but I'm a little confused as to why. Is this purposeful behavior? Is there a benefit to doing this?

As an example, in case it's not deliberate, when I parse:

(Prod (Name (Id n)) (Ind (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq)))) (DirPath ()) (Id nat)) 0) (Instance ()))) (Prod (Name (Id a)) (Ind (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq)))) (DirPath ()) (Id nat)) 0) (Instance ()))) (Prod (Name (Id x)) (Ind (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq)))) (DirPath ()) (Id nat)) 0) (Instance ()))) (Prod Anonymous (App (Const ((Constant (MPfile (DirPath ((Id List) (Id Lists) (Id Coq)))) (DirPath ()) (Id In)) (Instance ()))) ((Ind (((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq)))) (DirPath ()) (Id nat)) 0) (Instance ()))) (Rel 1) (App (Const ((Constant (MPfile (DirPath ((Id List) (Id Lists) (Id Coq)))) (DirPath ()) (Id seq)) (Instance ()))) ((Rel 2) (Rel 3))))) (App (Ind (((Mutind (MPfile (DirPath ((Id Logic) (Id Init) (Id Coq)))) (DirPath ()) (Id and)) 0) (Instance ()))) ((App (Ind (((Mutind (MPfile (DirPath ((Id Peano) (Id Init) (Id Coq)))) (DirPath ()) (Id le)) 0) (Instance ()))) ((Rel 3) (Rel 2))) (App (Const ((Constant (MPfile (DirPath ((Id Peano) (Id Init) (Id Coq)))) (DirPath ()) (Id lt)) (Instance ()))) ((Rel 2) (App (Const ((Constant (MPfile (DirPath ((Id Nat) (Id Init) (Id Coq)))) (DirPath ()) (Id add)) (Instance ()))) ((Rel 3) (Rel 4)))))))))))

before that function call, I get this, which looks good to me:

Tree(constructor_prod, [Tree(constructor_name, [Token(__ANON_1, 'n')]), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Datatypes'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'nat')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_name, [Token(__ANON_1, 'a')]), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Datatypes'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'nat')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_name, [Token(__ANON_1, 'x')]), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Datatypes'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'nat')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_anonymous, []), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'List'), Token(__ANON_1, 'Lists'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'In')])]), Tree(constructor_instance, [])]), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Datatypes'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'nat')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '1')])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'List'), Token(__ANON_1, 'Lists'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'seq')])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '2')])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '3')])])])]), Tree(constructor_app, [Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Logic'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'and')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_app, [Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Peano'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'le')])]), Tree(int, [Token(SIGNED_INT, '0')])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '3')])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '2')])])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Peano'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'lt')])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '2')])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [Token(__ANON_1, 'Nat'), Token(__ANON_1, 'Init'), Token(__ANON_1, 'Coq')])]), Tree(constructor_dirpath, []), Tree(names__label__t, [Token(__ANON_1, 'add')])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '3')])]), Tree(constructor_rel, [Tree(int, [Token(SIGNED_INT, '4')])])])])])])])])])

but after that function call, I get this, which is missing a lot of useful information:

Tree(constructor_prod, [Tree(constructor_name, []), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_name, []), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_name, []), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_prod, [Tree(constructor_anonymous, []), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(constructor_instance, [])]), Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [])]), Tree(constructor_rel, [Tree(int, [])])])]), Tree(constructor_app, [Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_app, [Tree(constructor_ind, [Tree(names__inductive, [Tree(constructor_mutind, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(int, [])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [])]), Tree(constructor_rel, [Tree(int, [])])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [])]), Tree(constructor_app, [Tree(constructor_const, [Tree(constructor_constant, [Tree(constructor_mpfile, [Tree(constructor_dirpath, [])]), Tree(constructor_dirpath, []), Tree(names__label__t, [])]), Tree(constructor_instance, [])]), Tree(constructor_rel, [Tree(int, [])]), Tree(constructor_rel, [Tree(int, [])])])])])])])])])

Is this deliberate erasure or a bug? And if it's deliberate, what does it help with?

[yangky11]

Hi,

Thanks for your interest in our work!
Yes, it is deliberate. We use only type information in the term AST. This was mainly for technical convenience. After the preprocessing, the nonterminal symbols in the ASTs are from a closed vocabulary, making it easier to apply machine learning models.

[yangky11]

No problem! Looking forward to it!

[tlringer]

Hi again, thanks so much for the prompt help last time!

I made a quick change to include some of the removed tokens in the AST, and I'm curious if there's an easy way to get a sense of which parts of the code I need to touch now that I've made this change. For example, in addition to changing gallina.py, I also added a new nonterminal to term_encoder.py. But I still get __ANON_1 in the token during caching, so I assume there are more places I need to make changes for this change to propagate all the way to the embedding.

If there's a good way to get an idea of the code architecture, and everything that needs to change as I continue to enrich the AST, please let me know! I'd also be happy to meet and talk through it for 30 minutes or so if that's easier.

[yangky11]

Hi,

I'm happy to talk through it later this week or next week. Could you email [email protected] so that we can find a time?

[tlringer]

Hi Kaiyu, thank you so much for the really helpful conversation today! The post-processing trick really helped and we're immediately on a good path. Strongly appreciated.

[yangky11]

No problem. Great talking to you today!

I did some search after our meeting and I'm 99% sure __ANON_ denotes anonymous terminals in Lark. They are due to some intricacies in how Lark handles terminal symbols. The post-processing trick should work fine in the current scenario. But you can take a look at the grammar specification in Lark's documentation and the output of print_grammar if it becomes a problem later.