Add support for alternative pattern matching and totality checking

pwang347 commented 4 years ago

Description

This change presents an initial solution for #92, as well as various other features listed below.

Added a prefix-tree-like data structure
Added a pattern match function using the data structure
Added "equality" check for testing (ignores syntax properties)
Added bottom-up fold function
Added totality checker

Notes

There is already get-constructors in cic-saccharata.rkt, but it didn't seem to be pulling constructor info
Currently there is a bit of log spewing from get-typeof in stdlib\pattern-tree.rkt for certain files. This is because it doesn't know how to handle implicitly defined constructors, especially trickier cases like :: which supports infinite nesting (this is the main TODO that I'm aware of)
- The type-aliases kwarg currently is only used in the totality checker to make sure we match against the right set of constructors. Future work could possibly integrate this into the pattern tree builder.
- In fact, even this approach is somewhat naive; it isn't able to support both the implicit and the explicit versions together in the same definition. Potentially, a "better" (well, more convenient) approach could be implemented that associates the implicit types to the original type directly.
The pattern match function is a proof of concept that performs body substitution directly by building up an environment by traversing the tree, though another approach could be to generate native Cur syntax - the key idea is that temporaries must be resolved before they are used so that we don't run into unbound IDs but the matcher is otherwise just a small collection of helpers for matching and traversing

Tests performed:

See test files

pwang347 commented 4 years ago

Some notes/questions:

Current approach of using assign-type doesn't work for lists since (List A) needs to be evaluated in the context where A is defined. Is there a way to perform this expansion manually?
Generated temporaries for nested expressions still need to have type inference (and therefore validation) based on which constructors they were used in
The tests in #92 are actually addressed by pr#100 already, so I omitted them

pwang347 commented 4 years ago

Current state of affairs:

Type inference now working on generic types
Temporaries for match cases in define/rec/match now have source information copied over - cleaner error messages for totality check
Didn't implement Vector, seems to already exist in tests\stdlib\deppat.rkt as Vect

TODO (blocked?):

Matching should be done with free-identifier=?, but it may be better to do this in one sweep once we establish a mechanism to distinguish type constructors from identifiers
Recursively add patterns for generic types; e.g. List Nat -> generates a pattern for the inner element too

Test failure case:

(define/rec/match minus-bad : Nat Nat -> Nat
[z _ => z]
[n z => n]
[(s n-1) (s m-1) => (minus n-1 m-1)])

can be fixed with

(define/rec/match minus-bad : Nat Nat -> Nat
[z _ => z]
[(s n-1) z => (s n-1)]
[(s n-1) (s m-1) => (minus n-1 m-1)])

so this change (to allow pattern variables to represent more complicated forms) would also require the ability to distinguish between constructors literals and variables

pwang347 commented 4 years ago

Summary of latest change:

Re-wrote into several methods for improved maintainability
Added free-identifier=? check of head patterns for determining equality (and also checking that they have the same number of arguments)
Associated constructors to their types, as well as the types of the arguments; a caveat to this below
Added identification of constructors
Body now correctly rewritten to use wildcard temporary when merged

Outstanding items:

Implicit constructors are not handled properly (error in CI)
Wildcards are not properly handled yet for totality; I'm still debating whether it's better to propagate wildcard contents into the tree itself (commented out methods do this already, but there's a tricky interaction with nested variables and associating types to the temporaries), or rather to do this from totality check itself by traversing several branches at a time (given that some are marked as wildcards). The latter would require a new traversal method, as the current fold is bottom up and not top down.

Some notes:

The compiler should not care about proper syntax; we care only to rewrite them in an alternate form and therefore failures in syntax should be handled elsewhere (e.g. at the end of phase 1)

wilbowma commented 4 years ago

Finally working on this, in pr-103-totality-checking

When I merged, I got some odd totality failures in bool. My guess would be either automatic merge did the wrong thing, or something about the merged termination checker broke something.

pwang347 commented 4 years ago

Finally working on this, in pr-103-totality-checking

When I merged, I got some odd totality failures in bool. My guess would be either automatic merge did the wrong thing, or something about the merged termination checker broke something.

Weird, I'm guessing it may be a sugar.rkt thing. Will take a look later, thanks!

wilbowma commented 4 years ago

Might be my fault. Looks like one of these depends on 7.6 and I was using 7.5. Updating know and will keep this PR updated.

wilbowma commented 4 years ago

Wasn't due to 7.6. Must be because define/rec/match got wrapped, to support totality checking. This is a bit strange since bool is one of the few places that didn't use the additional syntax added by the termination checker.

pwang347 commented 4 years ago

Most likely this: https://github.com/wilbowma/cur/pull/100/files#diff-bc56fe40e5300f5b41ec73c652f230c5R228

I moved the totality check up to the main call and I'm running travis on it right now. Will let you know how it goes!

wilbowma commented 4 years ago

You're a champ!

I agree that change looks suspicious, although it looks like I reverted it when I merged.

pwang347 commented 4 years ago

I was so deeply bothered by that coding artifact that I still remembered about it lol Looks like it's working so far (~7mins in)

wilbowma commented 4 years ago

We all know where our hacks are buried.

wilbowma commented 4 years ago

I replicated your changes locally and they seem to work---cur-lib builds properly now.

I'm a little confused by this change: https://github.com/wilbowma/cur/commit/4122d0d04bcd52ae2c7eb77f9c874b2f77a1e022#diff-bc56fe40e5300f5b41ec73c652f230c5R274

Given that the input was ((pat ...) => body) in the define/rec/match macro, and we didn't do any munges (as far as I can tell), this looks like it shouldn't match.

pwang347 commented 4 years ago

If I recall correctly, it's because I needed to pass the pat-bodies as literals back into the syntax expression but I couldn't find a way to preserve it exactly as before; in this case I wanted a flattened form [p1 p2 => body] but the closest I got was [(p1 p2) => body].

--

Also, see some other minor fixes I added here: https://github.com/wilbowma/cur/compare/pr-103-totality-checking...pwang347:pr-103-totality-checking?expand=1

Accidentally triggered several travis requests without killing previous ones, so they all got queued up and it's still running.

wilbowma commented 4 years ago

Okay. I'll investigate. I might rewrite it to get rid of those local-expands and the repeated syntax-parsing.

I'll do a proper merge off your branch shortly.

Thanks again, and sorry it took me so long to get to merging this... last semester, 411 was all consuming.

pwang347 commented 4 years ago

Sounds good, do keep me updated if there are any other issues that arise. Also no worries at all, I do hope it was a successful reboot despite the abrupt ending to the term!

Hope you and your family are doing well!

wilbowma commented 4 years ago

Yeah it went great. Will be even better next time.

Thanks, you too. Stay safe.

wilbowma commented 4 years ago

Moved this to #105 so I can get github to run checks against my copy of the branch.

wilbowma commented 4 years ago

Closed by 9b3dc826660a21fdd14690a18cad0eaf5e301086

wilbowma / cur