Expose the names of generated record constructors (reopen #6975) #7510
Conversation
6a1fabf to
428f660
Compare
428f660 to
8023232
Compare
…ecords Since ConstructorName can no longer take an empty set (commit ac2888a), we need to store the inductivity of a record in the new scopeRecords component.
|
@plt-amy Now that I am working with the code of this PR due to #7513, I wonder whether the new agda/src/full/Agda/Syntax/Scope/Base.hs Lines 108 to 110 in 756b4fb agda/src/full/Agda/Syntax/Scope/Base.hs Lines 58 to 64 in 756b4fb agda/src/full/Agda/Syntax/Scope/Base.hs Lines 67 to 69 in 756b4fb agda/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs Lines 1872 to 1875 in 756b4fb The respective setter and getter (that currently use scopeRecords) should be still definable.
|
|
|
||
| -- | Record (ha) that a given record has the specified constructor name. | ||
| setRecordConstructor :: A.QName -> A.QName -> ScopeM () | ||
| setRecordConstructor recr con = modifyScope_ $ over scopeRecords $ Map.insert recr con |
There was a problem hiding this comment.
Morally, recr should be an A.ModuleName, shouldn't it?
(Or at least it could, since each record type doubles as record module.)
* Record.constructor syntax: basic impl * Record.constructor syntax: add test cases * Record.constructor syntax: changelog & docs * Record.constructor syntax: updated tests * Record.constructor: Simplify errors and parsing
…opeRecords Since ConstructorName can no longer take an empty set (commit ac2888a), we need to store the inductivity of a record in the new scopeRecords component.
I quickly threw the implementation back together on top of master because it would be easier than rebasing or merging. Also: as discussed in the meeting on 09-25, the
Foo.constructorname is now always in scope (wheneverFoo) is, regardless of whether the constructor is named.