Phase-1 matcher

[gebner]

(This is still a bit off from merging. Posting here to describe some of the ideas and design decisions.)

This PR reimplements the matcher using a similar phase-1/phase-2 distinction we already internally use for type checking, utilizing uvars instead of substitions to represent the unifier. In the first phase we just run the unifier, and in only in the second phase do the actual type-checking and SMT queries happen. The API allows user code to skip the second phase entirely (it is returned as a continuation elaborator), so this new matcher can be used for the impure specs feature as well.

The new matcher is a lot stricter on mkeys; this is also with a future pulse_pattern feature in mind.

• If no arguments are marked with [@@@mkey] then effectively all arguments become mkeys. If the slprop is marked as [@@no_mkeys], then no arguments are mkeys. (I believe this is the current semantics, but not 100% sure.)
• If two resources are matched, then their head symbol is guaranteed to be equal.
• If two resources are matched, then all their mkeys are guaranteed to be unifiable.

For example, if you have a resource x |-> 1 and you need to solve for y |-> ?u, then this will reliably fail, even if you have pure (x == y) in the context. This is necessary because in the future we want to backtrack on this failure, and maybe insert a ghost lemma that turns x |-> 1 into y |-> 1 ** trade (y |-> 1) (x |-> 1).

Current state:

• The library builds.
• The F* unifier often produces beta-redexes like (fun a b c -> a) x y z (where the arguments are all local variables). I'm not sure why this happens, but it means we need to sprinkle a few more normalizer calls all over the place.

Fixes #32.
Fixes #107.
Fixes #110.

[mtzguido]

The new matcher is a lot stricter on mkeys; this is also with a future pulse_pattern feature in mind.

• If no arguments are marked with [@@@mkey] then effectively all arguments become mkeys. If the slprop is marked as [@@no_mkeys], then no arguments are mkeys. (I believe this is the current semantics, but not 100% sure.)
• If two resources are matched, then their head symbol is guaranteed to be equal.
• If two resources are matched, then all their mkeys are guaranteed to be unifiable.

For example, if you have a resource x |-> 1 and you need to solve for y |-> ?u, then this will reliably fail, even if you have pure (x == y) in the context. This is necessary because in the future we want to backtrack on this failure, and maybe insert a ghost lemma that turns x |-> 1 into y |-> 1 ** trade (y |-> 1) (x |-> 1).

Can you expand on this? This sounds like the current behavior (after #344) but maybe I am missing something.

[gebner]

Mmh, you're right. That seems to be the current behavior as well.