Define behaviour for empty expressions

[YehorBoiar]

This PR is based on the Chris's and Oz's comment on Teams:

"
Chris:
I'd get existing PRs merged in first, but then it might be worth making a pass over empty constraints, I think (please check essence semantics , and I'm not sure which are implemented yet):

and([]) = true
or([]) = false
sum([]) = 0
product([]) = 1

it's worth getting these right because (from experience), while no-one is likely to write these, they often end up getting created as parts of more interesting expressions.

Oz:
min([]) and max([]) are a bit different, as min([])=x is always false, but this falseness will arise naturally from the fact they will end up turning into an 'and([])' and an 'or([])', and the or will be false, so there is no need to special-case empty min([]) and max([]) (hopefully!)

we can define an abstraction which has a zero vale and an append operator for these.
and is true, /
or is false, /
sum is 0, +
product is 1, *
regarding min and max, we already did a bunch of definedness work with Felix last semester (Soph and Yehor taking over this now)
"

[ozgurakgun]

we should also actually remove Nothing, shouldn't we?

[YehorBoiar]

Will do. The reason why we are not deleting it yet is that we want to ensure that all empty rules work before deleting Nothing.

[ozgurakgun]

I just noticed: why is this a separate rule instead of being handled by the full evaluator?

[ozgurakgun]

@niklasdewally @YehorBoiar @lixitrixi

[niklasdewally]

By the look of git blame, seems to just be because Nothing was added before the evaluator.

I agree that it should be an evaluation step.

[YehorBoiar]

So we don't need this rule at all. We should just define an empty expression behaviour in rules, is that correct?

[ozgurakgun]

don't know what you mean by "We should just define an empty expression behaviour in rules"

for context, full evaluator here:

conjure-oxide/crates/conjure_core/src/rules/constant.rs

Line 11 in dc7f98b

fn apply_eval_constant(expr: &Expr, _: &Model) -> ApplicationResult {

partial evaluator here:

conjure-oxide/crates/conjure_core/src/rules/partial_eval.rs

Line 10 in dc7f98b

fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult {

[ozgurakgun]

and if it all was working correctly this would already do it?

conjure-oxide/crates/conjure_core/src/rules/constant.rs

Line 42 in dc7f98b

Expr::Or(_, exprs) => {

I think there is a bug. how well tested is the full evaluator?

remove_empty_expression is at 8800, and full evaluator is at 9001, so that should take precedence even if this rule was buggy (which I think it is)