-
Notifications
You must be signed in to change notification settings - Fork 122
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update the parser to deal more robustly with type applications.
We now reject situations where the user writes a type application on a term that is not an identifier, and we correctly unwind and reapply tuple and field selectors. Fixes #962 Fixes #1045 Fixes #1050
- Loading branch information
1 parent
668c135
commit 2a2ec6e
Showing
8 changed files
with
102 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,9 @@ | ||
`{1} | ||
(((True`{}, zero`{Integer})`{}).1)`{} | ||
number`{3}`{}`{}`{}`{}`{Integer} | ||
|
||
:l issue962a.cry | ||
:t i | ||
:t j | ||
|
||
:l issue962b.cry |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
Loading module Cryptol | ||
|
||
[error] at issue962.icry:1:2--1:5: | ||
Unexpected bare type application. | ||
Perhaps you meant `( ... ) instead. | ||
|
||
Parse error at issue962.icry:2:3--2:28 | ||
Explicit type applications can only be applied to named values. | ||
Unexpected: (True`{}, zero`{Integer}) | ||
|
||
Parse error at issue962.icry:3:1--3:11 | ||
Explicit type applications can only be applied to named values. | ||
Unexpected: number`{3} | ||
Loading module Cryptol | ||
Loading module Main | ||
i : {a} (fin a) => [a] -> [a] | ||
j : {a} (fin a) => [a]{fld : Integer} -> [a]Integer | ||
Loading module Cryptol | ||
Loading module Main | ||
|
||
[error] at issue962b.cry:32:16--32:25: | ||
Unexpected bare type application. | ||
Perhaps you meant `( ... ) instead. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,10 +1,13 @@ | ||
f : {a} (fin a) => [a] -> (Bit, [a]) | ||
f : {a, b} (fin a) => [a]b -> (Bit, [a]b) | ||
f x = (True, x) | ||
|
||
g : {a} (fin a) => [a] -> [a] | ||
g : {a,b} (fin a) => [a]b -> [a]b | ||
g x = (f`{a=a} x).1 | ||
|
||
h = f.1 | ||
|
||
i : {a} (fin a) => [a] -> [a] | ||
i = f`{a=a}.1 | ||
|
||
j : {a} (fin a) => [a]{ fld : Integer } -> [a]Integer | ||
j = f`{a=a,b={fld : Integer}}.1.fld |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters