Skip to content

Commit 89edfee

Browse files
committed
Add sugar for declaration punning
This is analogous to record (or definition or binding) punning where one can write e.g. x = 1; y = 2; xy = {x; y}; ;; same as {x = x; y = y} Now that notation also exists for declarations. This is motivated by the upcoming intersection like signature combination operator `&`. Consider a `MAP` signature: type MAP = { type t _; Key: ORD; ;; ... }; With the declaration punning notation and intersection like combination, one could write Map (Key: ORD) :> MAP & {Key} = ;; ... to refine the `MAP` signature.
1 parent 7c69219 commit 89edfee

3 files changed

Lines changed: 7 additions & 0 deletions

File tree

README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,7 @@ D ::= ...
172172
X A1 ... An = E ~> X : A1 -> ... -> An -> (= E)
173173
type X A1 ... An ~> X : A1 => ... => An => type
174174
type X A1 ... An = T ~> X : A1 => ... => An => (= type T)
175+
X ~> X : (= X)
175176
176177
(expressions)
177178
E ::= ...

parser.mly

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,8 @@ atdec :
183183
| head typparamlist EQUAL exp
184184
{ VarD($1, funT($2, EqT($4)@@ati 4, Pure@@ati 3)@@span[ati 2; ati 4])
185185
@@at() }
186+
| name
187+
{ VarD($1, funT([], EqT(VarE($1)@@ati 1)@@ati 1, Pure@@ati 1)@@ati 1)@@at() }
186188
| TYPE head typparamlist EQUAL typ
187189
{ VarD($2, funT($3, EqT(TypE($5)@@ati 5)@@ati 5, Pure@@ati 4)@@at())
188190
@@at() }

regression.1ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@ record_inference x = x.works_a_little;
22

33
;;
44

5+
type DEC_PUNNING = {int; list};
6+
7+
;;
8+
59
Equivalence: {
610
type t a b;
711

0 commit comments

Comments
 (0)