data61 / PSL

Other
65 stars 9 forks source link

SeLFiE: Should I have only one `EVAL_PATH` instead of `EVAL_INNER_PATH` and `EVAL_OUTER_PATH` #107

Closed yutakang closed 5 years ago

yutakang commented 5 years ago

signature TEST = sig type test_type; end; structure Test = struct datatype test_type = One | Two; end; Test.One; structure Test2 = Test:TEST; (Test2.One;)

functor mk_Test (T:TEST) = T; structure Test3 = mk_Test(Test); (Test3.One;)

yutakang commented 5 years ago

Probably I should have only one signature for Eval_Path and use it for both Eval_Inner_Path and Eval_Outer_Path.

The good news is that we do not have to expose the tables (path-to-(inner/outer)node-table and print-to-(inner/outer)-nodes-table).

So, we can have an ML functor from_Table_to_Eval_Path: PATH_TO_UNODE_TABLE -> EVAL_PATH.

yutakang commented 5 years ago

So, it is going to be something like

yutakang commented 5 years ago

This means I have to have constructs for outer-nodes even when I deal with inner-nodes. Use Utils.try'.

yutakang commented 5 years ago

Essentially, the only difference between Inner and Outer should be

I think we can produce Quantifier_Domain from a path-to-node-table. i.e.

which means we probably do not have to have these functors independently.

yutakang commented 5 years ago

Done.