-
Notifications
You must be signed in to change notification settings - Fork 12
Description
It seems that for each of our three(/four?) urust_callable grammar entries and each of the ways to call them, we have a separate syntax translation.
For example, these are the syntax translations for a regular function call with arguments (_urust_funcall_with_args):
AutoCorrode/Shallow_Micro_Rust/Micro_Rust_Shallow_Embedding.thy
Lines 299 to 306 in 7bb1e28
| "_shallow (_urust_funcall_with_args (_urust_callable_id id) args)" | |
| \<rightharpoonup> "_urust_shallow_fun_with_args (_shallow_identifier_as_function id) (_shallow args)" | |
| "_shallow (_urust_funcall_with_args (_urust_antiquotation emb) args)" | |
| \<rightharpoonup> "_urust_shallow_fun_with_args emb (_shallow args)" | |
| "_shallow (_urust_funcall_with_args (_urust_callable_fun_literal f) args)" | |
| \<rightharpoonup> "_urust_shallow_fun_with_args (_shallow f) (_shallow args)" | |
| "_shallow (_urust_funcall_with_args (_urust_callable_struct f id) args)" | |
| \<rightharpoonup> "_urust_shallow_fun_with_args (_shallow_identifier_as_function id) (_shallow (_urust_args_app f args))" |
Note that each one corresponds to an entry in the _urust_callable grammar.
For a function call without arguments (_urust_funcall_no_args), we have
AutoCorrode/Shallow_Micro_Rust/Micro_Rust_Shallow_Embedding.thy
Lines 329 to 335 in 7bb1e28
| \<comment>\<open>Turbofish no args\<close> | |
| "_shallow (_urust_funcall_no_args (_urust_callable_with_params (_urust_callable_id id) params))" | |
| \<rightharpoonup> "_urust_shallow_fun_no_args (_shallow_apply_params (_shallow_identifier_as_function id) params)" | |
| "_shallow (_urust_funcall_no_args (_urust_callable_with_params (_urust_callable_fun_literal f) params))" | |
| \<rightharpoonup> "_urust_shallow_fun_no_args (_shallow_apply_params (_shallow f) params)" | |
| "_shallow (_urust_funcall_no_args (_urust_callable_with_params (_urust_callable_struct f id) params))" | |
| \<rightharpoonup> "_urust_shallow_fun_with_args (_shallow_apply_params (_shallow_identifier_as_function id) params) (_shallow (_urust_args_single f))" |
with an entry for all _urust_callable grammare entries (except _urust_embed_antiquotation, which I think never appears without arguments).
It seems to me that these could/should be unified, into a single rule for each of the ways to call a function, and a single rule for each of the ways to shallowly embed the called function. This should improve readability and extensibility.