SeLFiE: change the type signature of eval in Eval_Syntax.

[yutakang]

The type signature of eval should be "val eval: Proof.state -> term -> assert -> bool" so that I can use it in Eval_Syntax_Struct.

[yutakang]

I also have to change the type signature of eval in Eval_Modifier.

[yutakang]

I also have to change the type signature of pst_to_full_path_to_fpunode_table in Full_Path_To_FPUnode.

[yutakang]

The fundamental difference between Eval_Syntax and Eval_Semantics is the following:

• Eval_Syntax has to discuss chained facts and nth sub-goals, while
• Eval_Semantics has to discuss all or some equations for the Semantic construct.

[yutakang]

So, we should define Full_Path_To_FPUnode after we define Eval_Semantics.

[yutakang]

So, we should define Full_Path_To_FPUnode after we define Eval_Semantics.

Probably, the right order is

1. print
2. semantics
3. full_path (and update print)
4. mod

So, I have to

• [ ] introduce Eval_Path similarly to Eval_Full_Path"