Deep Abduction, PGT SeLFiE: we now have better utility functions in SeLFiE to implement PGT.

data61 / PSL

Other

65 stars 9 forks source link

Closed yutakang closed 3 years ago

yutakang commented 3 years ago

For example

typ_to_arg_numb in PGT.ML and count_numb_of_args_of_fun_typ in PSL/Utils.ML can be handled by Term.binder_types.
Probably we can use Unique_Node to implement replace_with in PGT.ML.

yutakang commented 3 years ago

Can I use SeLFiE or an improved version of SeLFiE for conjecturing?

yutakang commented 3 years ago

I removed typ_to_arg_numb and improved count_numb_of_args_of_fun_typ in c3f59ff6bd059ec7d11af57a0c2dde076519b69f.

yutakang commented 3 years ago

Can I use SeLFiE or an improved version of SeLFiE for conjecturing?

The answer is probably yes. But I have to change the SeLFiE interpreter for this.