Concrete ident for coq #1073
Concrete ident for coq #1073
Conversation
cmester0
force-pushed
the
coq-generic-printer
branch
from
abdcd67 to
9e36cb0
Compare
|
For Coq I cannot name tuple fields, 0,1,2,.., furthermore fields need to be unique, so we should use the path in the name of the fields. This naming also has to be consistent when used elsewhere, so I changing this in concrete ident. |
cmester0
force-pushed
the
coq-generic-printer-concrete-ident
branch
from
96e7a0e to
3305abc
Compare
cmester0
force-pushed
the
coq-generic-printer
branch
from
390a82a to
1abd124
Compare
cmester0
force-pushed
the
coq-generic-printer-concrete-ident
branch
from
73ae346 to
f0517ad
Compare
| Arguments t_Foo:clear implicits. | ||
| Arguments t_Foo. | ||
|
|
||
| Record t_Bar : Type := | ||
| { | ||
| 0 : t_Foo; | ||
| t_Bar_0 : t_Foo; |
There was a problem hiding this comment.
This is a solution to tuple structs.
There was a problem hiding this comment.
I think enum_constructor_name_transform will do the job as well.
Such a choice need to be backend specific
| @@ -47,13 +47,13 @@ Export Hax_lib (t_int). | |||
|
|
|||
| Record t_Foo : Type := | |||
| { | |||
| f_field : t_u8; | |||
| t_Foo_f_field : t_u8; | |||
There was a problem hiding this comment.
This is a solution to overlapping field names in structs.
There was a problem hiding this comment.
Oh, I see!
Then you need to improve the name policies API: the binding enum_constructor_name_transform is what you want, but you need to add an extra argument "struct_name" or something, just as I did for enum_constructor_name_transform.
Do you see what I mean?
There was a problem hiding this comment.
Ahh, yes. Makes sense.
There was a problem hiding this comment.
😃
Let's chat if something looks odd or whatever, I'm available, just ping me if needed :)
There was a problem hiding this comment.
This will also fix the issue I had, with overwriting keywords (e.g. end).
cmester0
force-pushed
the
coq-generic-printer-concrete-ident
branch
from
f0517ad to
1587ec2
Compare
cmester0
force-pushed
the
coq-generic-printer-concrete-ident
branch
from
1587ec2 to
14904e9
Compare
|
Closed in favor of #1108, which has more features |
Move concrete ident modifications for Coq backend (#987) to separate PR.