edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-02 22:43:14 +03:00
Code Issues Projects Releases Wiki Activity
854e39936e
Idris2-boot/tests/ttimp/dot001/expected

16 lines
767 B
Plaintext
Raw Normal View History

Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Processing as TTImp
Written TTC
Yaffle> Bye for now!
Processing as TTImp
Check names are visible/public
2019-06-24 02:12:58 +03:00
Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
Better approach to erasure in pattern matching It's a big patch, but the summary is that it's okay to use a pattern in an erased position if either: - the pattern can also be solved by unification (this is the same as 'dot patterns' for matching on non-constructor forms) - the argument position is detaggable w.r.t. non-erased arguments, which means we can tell which pattern it is without pattern matching The second case, in particular, means we can still pattern match on proof terms which turn out to be irrelevant, especially Refl. Fixes #178
2020-01-21 21:47:43 +03:00
Dot2.yaff:15:28--15:30:Pattern variable {P:n:94} unifies with ?{P:m:94}_[]
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Processing as TTImp
Check names are visible/public
2019-06-24 02:12:58 +03:00
Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
Better approach to erasure in pattern matching It's a big patch, but the summary is that it's okay to use a pattern in an erased position if either: - the pattern can also be solved by unification (this is the same as 'dot patterns' for matching on non-constructor forms) - the argument position is detaggable w.r.t. non-erased arguments, which means we can tell which pattern it is without pattern matching The second case, in particular, means we can still pattern match on proof terms which turn out to be irrelevant, especially Refl. Fixes #178
2020-01-21 21:47:43 +03:00
Dot3.yaff:18:10--18:15:Can't match on ($resolved86 ?{P:x:99}_[] ?{P:x:99}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved86 ?Main.{_:13}_[] ?Main.{_:14}_[])
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Processing as TTImp
Better approach to erasure in pattern matching It's a big patch, but the summary is that it's okay to use a pattern in an erased position if either: - the pattern can also be solved by unification (this is the same as 'dot patterns' for matching on non-constructor forms) - the argument position is detaggable w.r.t. non-erased arguments, which means we can tell which pattern it is without pattern matching The second case, in particular, means we can still pattern match on proof terms which turn out to be irrelevant, especially Refl. Fixes #178
2020-01-21 21:47:43 +03:00
Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:101}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Reference in New Issue Copy Permalink