This adds a facility to impose a side condition expressed as a python lambda to a rule otherwise written in KS. (So: not useful for rules parsed from a .ks file; but useful for KS rules embedded within a .py).
I keep oscillating about this, as almost every side condition can be done in some other (probably better) way; for example, many times one wants a side condition, it's something about free variables that could be figured automatically by All Binders Unique or more complex equivalents. The canonical example (for now) might be the side condition for:
(rule "lift_let_from_if_true" ..args..
(if p (let (x e) body) f)
(let (x e) (if p body f))
)
where (in order to preserve program semantics) the side-condition says that e must not possibly throw an exception if evaluated when not p.
But, I probably shouldn't oscillate. The overhead in code is tiny, small enough that even if we never use it in anger, we probably won't regret it. So here it is.
This adds a facility to impose a side condition expressed as a python lambda to a rule otherwise written in KS. (So: not useful for rules parsed from a .ks file; but useful for KS rules embedded within a .py).
I keep oscillating about this, as almost every side condition can be done in some other (probably better) way; for example, many times one wants a side condition, it's something about free variables that could be figured automatically by All Binders Unique or more complex equivalents. The canonical example (for now) might be the side condition for:
where (in order to preserve program semantics) the side-condition says that
emust not possibly throw an exception if evaluated whennot p.But, I probably shouldn't oscillate. The overhead in code is tiny, small enough that even if we never use it in anger, we probably won't regret it. So here it is.