Improve how operator typing rules are specified and checked

[bpandreotti]

Currently, the type checking for all operator terms happens inside the Parser::make_op function, in a huge (and ever increasing) match statement. This means that to add a new operator, a maintainer needs to modify this function in the parser, and implement the type checking rules manually, which can be non-trivial, and has lead to bugs before. It would be better if this type checking logic were in a different module, and if there was some simpler way to specify the typing rules for an operator.

The ideal version of this would be if a maintainer could add a new operator without having to even touch rust code, by just editing a configuration file. Carcara could then read this file at compile-time, and enforce the type checking rules specified in it. One way this might look is a .toml file, like this:

[[operator]]
name = "str.replace_re"
return_type = "String"
arg_types = ["String", "RegLan", "String"]

Alternatively, we can use the syntax used by SMT-LIB theory declarations:

(str.replace_re String RegLan String String) 

It might be the case that not all operators can be succintly defined with this configuration language, especially considering the behaviour of some operators changes depending on parser config. In that case, I think it makes sense to have built-in operators, whose typing rules are still defined in rust, as well as the custom operators:

enum Operator {
    Add,
    Sub,
    // ...
    Custom(CustomOperator), // Read from config file
}

[caotic123]

I see a better potential if we allow the sort Function to allow variadic typing. Add and Sub could also be applied in these files. Additionally, Rare files contain numerous examples of this, which will be helpful in this module. I really recommend also mapping operators/functions to their type definition by using bidirectional typing, even though we do not allow partial applications. So we only need to know that (str.replace_str) is (-> String (-> String String)).

[HanielB]

@caotic123 Do you mean to rather than having Op as a constructor of Term to use Function instead? That has the big downside of making us lose the ability to easily pattern matching on operators, which we do all the time.

[caotic123]

No @HanielB, just mapping, for example, a function that maps (str.replace_str) to FunctionSort String (FunctionSort String String). We just need to add Variadic types, for example, or could be mapped to VariadicFunctionSort String. So now we test types, not their terms.

[HanielB]

I think I see what you mean. This ties in with some changes I'm doing to Carcara in a branch to improve the handling of parametric things. Once I have something more concrete we can discuss further. But I think that what Bruno is proposing here can be done independently and maybe later on adapted.