Open
Description
Noticed by @virgil-serbanuta: #if ... #then ... #else
currently has inconsistent semantics.
In the following example, during function evaluation#if B #then Bottom #else g(x)
will be evaluated to Bottom
(because a symbol with a Bottom
argument is Bottom
) while when unifying this term, say unify(stuff, #if B #then Bottom #else g(x) #fi)
this will result in ((B == true) and (stuff == Bottom)) or ((B == false) and (stuff == g(x)))
therefore the result will be defined (so not Bottom
).
@virgil-serbanuta suggests we change this result to ((B == true) and (stuff == f(x)) and (ceil(#if ... #fi))) or ((B == false) and (stuff == g(x)) and (ceil(#if ... #fi)))
and investigate any resulting failures.