Type check theory and operator during expression constructor

[filipeom]

Type check the theory and operator during expression construction to disallow expressions that are forbidden, for example:

let _ = unop Ty_bool Sqrt (value True) (* should not compile *)

[redianthus]

Hi @filipeom, this looks really interesting. I'd be interested in doing a full review but I won't be able to do it before the 22nd of may, could you wait before merging?

[filipeom]

Hi @filipeom, this looks really interesting. I'd be interested in doing a full review but I won't be able to do it before the 22nd of may, could you wait before merging?

Of course! But I should warn you, this PR might actually take a while to merge. I've only done it for unary operators so far, but I think it's working ok (at least it's doing what I wanted 😅).

Also, this breaks the SMT-LIB parser, because I was doing stuff like this:

| "-", [ a; b ] -> Expr.raw_binop Ty_none Sub a b
| "*", [ a; b ] -> Expr.raw_binop Ty_none Mul a b
| "/", [ a; b ] -> Expr.raw_binop Ty_none Div a b

In cases where the theory could be inferred directly from the operator, I was assigning it the Ty_none theory, and then inferring the correct theory in the rewriting module based on the arguments theories. But now this no longer typechecks 😅 So I still need to figure out the best way to build expressions from dolmen terms.