Work on inference, unification and subject-reduction

[fblanqui]

fix type inference, unification, handling of implicit arguments in rules, subject-reduction
fix issues #303 #330 #334

[fblanqui]

There is a bug I need to fix. I am working on it.

[fblanqui]

I have a question: do we assume somewhere in the code that a meta of arity n has a type of the form \forall x1:A1,..,\forall xn:An,B?

[rlepigre]

I have a question: do we assume somewhere in he code that a meta of arity n has a type of the form \forall x1:A1,..,\forall xn:An,B?

I'm not sure, but most probably.

[rlepigre]

There are still changes in there that I think are a mistake, but I guess I can live with them.

[rlepigre]

So can I merge @fblanqui? (I want to do it myself because I want to fix the commit message.)

[fblanqui]

I have a question: do you keep the LHS unchanged after scoping?

[rlepigre]

I have a question: do you keep the LHS unchanged after scoping?

For now yes, but it will have to change once I implement the optimisation.

[fblanqui]

Ok. The optimisation does not change the matching behavior. It is important to not change this indeed. Only the RHS metavariables should be instantiated by something.

[fblanqui]

Thanks to merge @rlepigre . And thanks for your improvements on this PR!

[rlepigre]

Ok. The optimisation does not change the matching behavior. It is important to not change this indeed. Only the RHS metavariables should be instantiated by something.

Yeah, the only thing that the optimisation will do is just not record the term matching a pattern variable in the case where it is not useful in the RHS (and does not appear non-linearly). This means that we will have wildcards again (i.e., terms of the form Patt(None,...,...)) when reducing. For now these do not appear anymore I think. This wastes space since we allocate arrays that are bigger than they need to be.