Allow attributes on record fields #2192
Conversation
| @@ -973,7 +973,7 @@ and p_aqual = function | |||
| in | |||
| str "#[" ^^ p_term false false t ^^ str "]" ^^ break1 | |||
| | Meta (Arg_qualifier_meta_attr t) -> | |||
| str "#[@" ^^ p_term false false t ^^ str "]" ^^ break1 | |||
| str "#[@@" ^^ p_term false false t ^^ str "]" ^^ break1 | |||
There was a problem hiding this comment.
I think the "#[@" syntax is deprecated? Is that correct?
There was a problem hiding this comment.
Agreed, good to fix this. thanks.
src/syntax/FStar.Syntax.Resugar.fs
Outdated
| let q = | ||
| // TODO: There's a 'FIXME' note on resugar_arg_qual that I don't fully understand. It doesn't seem applicable in this case as the | ||
| // syntax for records only support 'Arg_qualifier_meta_attr' and the only problematic case seems to be 'inaccessible implicit argument of a data constructor' | ||
| match resugar_arg_qual env qual with |
There was a problem hiding this comment.
@nikswamy This is my main question. The only supported qual for record field is an attribute, and looking at how 'resugar_arg_qual' works, it should always return 'Some'. Do you think this code is fine? Should I at least leave some comment here?
There was a problem hiding this comment.
Yes, I think this is fine.
The case where resugar_arg_qual returns None is relevant for patterns in which some arguments to a data constructor are marked as inaccessible, since they should always be computed via unification.
I don't think it is relevant here for resugaring the fields of a datacon.
|
@nikswamy I've extended the test and querying seems to work fine. I consider this one done and ready for review :) |
| #[@@ (description "This is a number") ] field1 : int; | ||
| #[@@ (description "This is a string") ] field2 : string; | ||
| } | ||
|
|
There was a problem hiding this comment.
Sadly, there's one aspect of it that I neglected to notice earlier. These attributes on binders are unfortunately coupled with implicit arguments (i.e., the preceding #) makes both these fields implicits arguments to the record constructor.
That means that the code below fails to typecheck
let test (x:int) (y:string) = { field1 = x; field2 = y }
And you instead have to write:
let test (x:int) (y:string) : r = Mkr #x #y
I think we should decouple attributes on binders with implicit arguments. i.e., you should be able to associate an attribute with a binder whether it is implicit or not. E.g.,
([@@ attr1] x : t) -> (#[@@attr2] y:t) -> ...
The first being an explicit and the second an implicit arg.
@aseemr @R1kM ... wdyt? This should be fine for Steel too, right?
There was a problem hiding this comment.
I think it should be fine for Steel indeed. So far, I don't think we needed the framing attribute on explicit arguments, but this would be good to have for the future
There was a problem hiding this comment.
Right, I completely missed this.
"I think we should decouple attributes on binders with implicit arguments."
@nikswamy Do I understand correctly that 'Meta' aqual cases are currently assumed to be implicit? And I should extend the aqual with some new case which could be used for an explicit argument? Plus change the rule so that when HASH is missing, we go with the new case?
Or maybe use "option attributes" instead with some extra flag to tell if it's implicit?
I guess this means I also need to touch the representation of TyconVariant / Product so that [@@ ] is supported there too, right?
mateuszbujalski
force-pushed
the
matbuj_record_field_attributes
branch
from
ca1a015 to
ce00c25
Compare
…ces new shift/reduce conflicts in the parser)
mateuszbujalski
changed the title
|
@nikswamy @aseemr I've updated the PR after the refactoring done by Aseem. I wrote some simple test for records and now it works both for implicit and explicit fields. I'll add some more tests for various cases where attributes are now possible. Unfortunately, I wasn't able to change the parser without increasing the number of shift/reduce conflicts around LBRACK_AT_AT (the total number went up from 6 to 11 - I've temporarily hacked the makefile to accept this to see if CI will be happy with the rest of the changes). What's currently pushed there seems to work but it's probably best if it's reverted and reworked. It would be great if you could take a look :) |
mateuszbujalski
changed the title
This change extends the record syntax to allow decorating fields with attributes.
I still need to write a test where I query the attribute from a tactic to make sure it works correctly.