add support for lnot on ints and uints

[enjhnsn2]

fixes #571

[nilehmann]

@enjhnsn2 looks good, but some errors need to be fixed.

We also need to add the signatures here. We have a different set of signatures depending on whether overflow checking is enabled. Overflow is not relevant for ! but we still need to duplicate the signature.

Also, can you add a test here?

[nilehmann]

This needs to be

Suggested change

	(mir::UnOp::Not, s!(fn(a: Int) -> Int[E::tt()]))
	(mir::UnOp::Not, s!(fn(a: Int) -> Int{ v: E::tt() }))

Int[E::tt()] would mean the integer is indexed by a bool which is not well-formed.

[nilehmann]

Same here

[enjhnsn2]

sgtm, I'll add the duplicate signature and test. I'll take a look at the other int -> int functions to try and find a well-formed replacement for E::tt()

[enjhnsn2]

wait, the shift functions use E::tt() and those are int -> int functions. Why is it right there and wrong here? (note, I don't really understand what E::tt() does lol)

(Shl, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })),

[enjhnsn2]

it was my impression (from context) that E::tt() told Flux to treat the operorator as an uninterpreted function, as in the other bitwise operations:

// BIT
(BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})),
(BitOr,  s!(fn(a: Int, b: Int) -> Int{v: E::tt()})),

[nilehmann]

E::tt() means the true formula so you can read Int{v: E::tt()} as Int{v: true}

The problem is not E::tt() but using brackets instead of braces. Using brackets as in Int[E::tt()] would mean Int[true] which is not well-formed because (rust) integers have to be refined by (logical) integers. Instead, Int{v: E::tt()} is an existential type, i.e., the index is existentially quantified and the formula E::tt() is a constraint on the index (a trivial restriction in this case).

[nilehmann]

Looks good to me. I'm going to mer it.