Commit Graph

7 Commits

Author SHA1 Message Date
Edwin Brady
ea0de3d499 Initial implementation of 'case' blocks
It's not quite there yet, though, because the treatment of 'as' patterns
isn't quite right and the slightly hacky approach we're taking might not
be the best. Rethinking now...
2019-05-17 13:52:09 +01:00
Edwin Brady
83dc0b0e6d Add simple let bindings 2019-05-12 19:04:31 +01:00
Edwin Brady
14f717aa33 Add test for failed delayed elaborator 2019-05-12 16:03:04 +01:00
Edwin Brady
43d323f685 First go at ambiguous name resolution
Works by running all possible elaborators and checking that exactly one
succeeds. Still to do: pruning the list of elaborators by target type,
dealing with 'UniqueDefault', checking that delaying on failure works as
it should.
2019-05-11 20:50:51 +01:00
Edwin Brady
a2ce8d0b7d Add as patterns
When we encounter them, not that they're a binding as normal, but also
record the thing they expand to. Then bind as a PLet, and convert that
to a Let on the RHS so it has computational force. The case tree
compiler knows about as patterns, so they get compiled to use the
appropriate name on the rhs (rather than a let).
2019-05-09 16:48:09 +01:00
Edwin Brady
411b8ccc07 Support eta in unification
Also added (necessarily) a rule for lambdas
2019-05-07 15:06:00 +01:00
Edwin Brady
77bf4c7c44 Added test framework (copied from Blodwen) 2019-05-07 10:43:02 +01:00