SeLFiE: Boolean operators have to take `Literal bool` in `From_Parameter_With_Bool_To_Bound.ML`

data61 / PSL

Other

65 stars 9 forks source link

SeLFiE: Boolean operators have to take `Literal bool` in `From_Parameter_With_Bool_To_Bound.ML` #109

Closed yutakang closed 4 years ago

yutakang commented 4 years ago

The problem originates in From_Parameter_To_Parameter_With_Bool.ML.

For example, the interpreter cannot process Not (And [True, False]) in From_Parameter_With_Bool_To_Bound.ML.

Probably this is okay:

we can remove this restriction at Eval_Sugar.
this restriction at earlier stages only force the interpreter to use the strict evaluation.

yutakang commented 4 years ago

This forced strict evaluation might be problematic when we implement smart-induction later. But we can think about it later.

yutakang commented 4 years ago

Ah.... this was not a problem.

This line in From_Variable_To_Quantifier.ML already implements an eager evaluation for LiFtEr. So, when the modular interpreter reaches From_Parameter_To_Parameter_With_Bool.ML, all the arguments to those boolean connectives (Not, And, and so on) are already normalized to boolean literals.