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):
|
"_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
|
\<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.
It seems that for each of our three(/four?)
urust_callablegrammar 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
Note that each one corresponds to an entry in the
_urust_callablegrammar.For a function call without arguments (
_urust_funcall_no_args), we haveAutoCorrode/Shallow_Micro_Rust/Micro_Rust_Shallow_Embedding.thy
Lines 329 to 335 in 7bb1e28
with an entry for all
_urust_callablegrammare 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.