SeLFiE: Don't call `pst_n_trm_to_path_to_unode_table` so many times.

[yutakang]

We don't have to construct these tables so many times. The current implementation is not efficient. But at the same time, we want to get this interpreter work before making it efficient.

[yutakang]

pst_n_trm_to_path_to_unode_table is called by eval in Eval_Path.ML, which, in return, is called by eval in Eval_Parameter.ML.

eval' in Eval_Parameter.ML has many case distinctions over assert, which is the first parameter of eval'.

The second parameter is a list of literals, which distinguishes outer paths and inner paths.

So, can we path outer_term_table and inner_term_table to eval in Eval_Parameter.ML?

[yutakang]

The important thing is that we only have to send exactly one of either inner_term_table or outer_term_table to eval in Eval_Parameter.ML, which is called by eval in Eval_Parameter_With_Bool.ML.

So, the type of this parameter would be

• datatype term_table = Inner_Table of Inner_Path_To_Unode.path_to_unode_table | Outer_Table of Outer_Path_To_Unode.table

The problem of current implementation is that make_Each_Eval_Path is parametrised over structures of the signature PATH_TO_UNODE: These structures, Inner_Path_To_Unode and Outer_Path_To_Unode, contain functions to create term tables from a proof state and term but not term tables themselves.

That is why the SeLFiE interpreter has to build the table many times.

[yutakang]

On the other hand, I cannot parametrise make_Each_Eval_Path over structures that contain term tables themselves because we need a term and proof state to decide the structure of a term table and they are passed to the eval function as arguments.

So, instead of passing a term and proof state to eval in make_Each_Eval_Path, we should pass a term table.

[yutakang]

Accordingly, we should also parametrise Eval_Parameter and Eval_Parameter not over a term and proof state but over a term table.

For eval' in Eval_Unary.ML, this function has to carry around a term table in stead of a term. And for that reason we have to modify outer_literal_to_definitions and inner_literal_to_definitions accordingly.

[yutakang]

Done in 1bd4990c6737ac1d5726d6e501585bb33afe55cd.