Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make more use of List1 (List.NonEmpty) in concrete syntax #4547

Closed
andreasabel opened this issue Mar 28, 2020 · 3 comments
Closed

Make more use of List1 (List.NonEmpty) in concrete syntax #4547

andreasabel opened this issue Mar 28, 2020 · 3 comments
Assignees
@andreasabel
Labels
refactor Changes to the code base which do not affect users (not in changelog) type: task Concerning the development of Agda (not in changelog)
Milestone
2.6.2

Comments

@andreasabel
Copy link
Member

Several sequences in the concrete syntax cannot be empty, and we can express this via List1.
@andreasabel andreasabel added refactor Changes to the code base which do not affect users (not in changelog) type: task Concerning the development of Agda (not in changelog) labels Mar 28, 2020
@andreasabel andreasabel self-assigned this Mar 28, 2020
andreasabel added a commit that referenced this issue Mar 28, 2020
@andreasabel
[ refactor for #4547 ] more precise LamClause
d1d999b 
Remove fields that have a fixed value (e.g. lamWhere = NoWhere).

As a plus, this simplifies scope checking.
andreasabel added a commit that referenced this issue Mar 28, 2020
@andreasabel
[ refactor for #4547 ] more precise LamClause
304160b 
Remove fields that have a fixed value (e.g. lamWhere = NoWhere).

As a plus, this simplifies scope checking.
@andreasabel andreasabel added this to the 2.6.2 milestone Mar 28, 2020
andreasabel added a commit that referenced this issue Mar 28, 2020
@andreasabel
[ #4547 ] Use List1 (List.NonEmpty) in Parser and Concrete syntax
78795eb 
This eliminates a couple of __IMPOSSIBLE__s and documents non-emptiness
robustly.

I introduced some uses of List1.fromList that should be eliminated over
time.  More opportunities for List1 may be on the declaration level,
e.g. in Syntax.Concrete.Definitions.
andreasabel added a commit that referenced this issue Mar 28, 2020
@andreasabel
[ #4547 ] Use List1 (List.NonEmpty) in Parser and Concrete syntax
c87e3be 
This eliminates a couple of __IMPOSSIBLE__s and documents non-emptiness
robustly.

I introduced some uses of List1.fromList that should be eliminated over
time.  More opportunities for List1 may be on the declaration level,
e.g. in Syntax.Concrete.Definitions.
andreasabel added a commit that referenced this issue Mar 28, 2020
@andreasabel
[ #4547 ] Use List1 (List.NonEmpty) in Parser and Concrete syntax
4ae0ba2 
This eliminates a couple of __IMPOSSIBLE__s and documents non-emptiness
robustly.

I introduced some uses of List1.fromList that should be eliminated over
time.  More opportunities for List1 may be on the declaration level,
e.g. in Syntax.Concrete.Definitions.
@andreasabel
Copy link
Member Author

Spent my 17th day in quarantine with a day-long refactoring of the parser to use List1 where possible: 4ae0ba2

andreasabel added a commit that referenced this issue Mar 29, 2020
@andreasabel
[ #4547 ] refactor Concrete.Generic: use DefaultSignatures
ad2e763
andreasabel added a commit that referenced this issue Mar 29, 2020
@andreasabel
[ #4547 ] refactor Concrete.Generic: use DefaultSignatures
04420e0
@andreasabel
Copy link
Member Author

There is plenty of opportunities for List1 left in other parts of Agda, like Concrete.Definitions and further down the pipeline. I may reopen if I feel like doing more on this.

andreasabel added a commit that referenced this issue Apr 10, 2020
@andreasabel
[ #4547 ] List1 in TopLevelModuleName and qnameParts
d16cae9
andreasabel added a commit that referenced this issue Apr 13, 2020
@andreasabel
[ #4547 ] List1 in TopLevelModuleName and qnameParts
3ef9404
andreasabel added a commit that referenced this issue Apr 25, 2020
@andreasabel
[ #4547 ] Two (inessential) uses of List1 in Concrete.Definitions
35b0395
andreasabel added a commit that referenced this issue Apr 25, 2020
@andreasabel
[ #4547 ] Two (inessential) uses of List1 in Concrete.Definitions
723a65b
andreasabel added a commit that referenced this issue Jun 4, 2020
@andreasabel
[ #4547 refactor ] Use List2 in RawApp[P]
9f4b31a 
An application naturally is a list of at least 2 elements.

No more removeSingletonRawAppP!  Eliminated ~10 corner cases.

Concrete.Definitions:
Since EllipsisP is no longer wrapped in a RawAppP which stores its
range even after replacement, we need to set the range of the ellipsis
to the pattern we substitute for the ellipsis.
@andreasabel
Copy link
Member Author

I am now making RawApp[P] hold a List2, list of at least 2 elements. This removes many annoying corner cases of singleton RawApps.

andreasabel added a commit that referenced this issue Jun 4, 2020
@andreasabel
[ #4547 refactor ] Use List2 in RawApp[P]
0418338 
An application naturally is a list of at least 2 elements.

No more removeSingletonRawAppP!  Eliminated ~10 corner cases.

Change to Concrete.Definitions:

- Since EllipsisP is no longer wrapped in a RawAppP which stores its
range even after replacement, we need to set the range of the ellipsis
to the pattern we substitute for the ellipsis.

- As a side effect, the ellipsis ... maybe be highlighted as function now,
allowing jump-to-definition.  Can be considered a feature rather than a
bug.
andreasabel added a commit that referenced this issue Jun 6, 2020
@andreasabel
[ #4547 ] C.nameNameParts cannot be empty (use List1)
8937789 
Also: introduce smart constructors for C.Name:

- simpleName
- simpleHole
- simpleBinaryOperator
andreasabel added a commit that referenced this issue Jun 6, 2020
@andreasabel
[ #4547 ] C.nameNameParts cannot be empty (use List1)
55ec34c 
Also: introduce smart constructors for C.Name:

- simpleName
- simpleHole
- simpleBinaryOperator
andreasabel added a commit that referenced this issue Jun 6, 2020
@andreasabel
[ #4547 ] C.OpApp[P] has non-empty argument List1
495f1ec 
This refactoring does not remove any __IMPOSSIBLE__s.
It does not seem to matter whether we have "0-ary operators" or not.
andreasabel added a commit that referenced this issue Jun 18, 2020
@andreasabel
[ #4235 #4547 ] generalize pretty printers from List to Foldable
fe7e525 
This makes many calls to {NonEmpty,List1}.toList obsolete.

Also added some more functions to Agda.Utils.List1 to make even more
calls to toList obsolete.
andreasabel added a commit that referenced this issue Jun 18, 2020
@andreasabel
[ #4235 #4547 ] generalize pretty printers from List to Foldable
5954a1e 
This makes many calls to {NonEmpty,List1}.toList obsolete.

Also added some more functions to Agda.Utils.List1 to make even more
calls to toList obsolete.
andreasabel added a commit that referenced this issue Jun 18, 2020
@andreasabel
[ #4547 ] use List1 in {C|A}.{T}Let
f23b621 
Statically disallowing empty Let has some repercussions in the
translations between concrete and abstract syntax.
I had to introduce 'Maybe TypedBinding' in some places which wasn't
necessary before since Let could host an empty binding before.
andreasabel added a commit that referenced this issue Jun 21, 2020
@andreasabel
[ #4547 ] use List1 in {C|A}.{T}Let
31fbd2d 
Statically disallowing empty Let has some repercussions in the
translations between concrete and abstract syntax.
I had to introduce 'Maybe TypedBinding' in some places which wasn't
necessary before since Let could host an empty binding before.
andreasabel added a commit that referenced this issue May 19, 2021
@andreasabel
[ #4547 ] use List1/2 in Concrete.Definition.Errors.ShadowingInTelescope
245c95d
andreasabel added a commit that referenced this issue May 19, 2021
@andreasabel
[ #4547 ] use List1/2 in Concrete.Definition.Errors.ShadowingInTelescope
0911e84
andreasabel added a commit that referenced this issue May 19, 2021
@andreasabel
[ #4547 ] use List1/2 in Concrete.Definition.Errors.ShadowingInTelescope
7b385b4
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
refactor Changes to the code base which do not affect users (not in changelog) type: task Concerning the development of Agda (not in changelog)
Projects
None yet
Milestone
2.6.2
Development

No branches or pull requests
1 participant
@andreasabel