|
|
|---|
|
|
|
|---|
Check if a non-strict binary expression is statically well-formed.
(check-nonstrict-binary-expression op arg1 arg2 expr ctxt) → result
For a conjunction, we first check that the left conjunct is boolean. Then we check that the right conjunct is boolean, in the context augmented by the left conjucnt. That is, in the second conjunct we can assume that the first conjunct holds: otherwise, the conjunction is already false (non-strictness).
A disjunction is treated similarly to a conjunction, except that the context for the second disjunct is augmented with the negation of the first disjunct. That is, in the second disjunct we can assume that the first disjunct does not hold: otherwise, the conjunction is already true (non-strictness).
A forward implication is treated the same as a conjunction: in the consequent we can assume that the antecedent holds, otherwise the implication is already true (non-strictness).
A backward implication is treated the same as a forward implication, with the roles of the operands swapped.