Skip to content

Commit ba0b447

Browse files
rossbergrossberg
committed
[spectec] Avoid variable capture in IL semantics
1 parent 594c534 commit ba0b447

2 files changed

Lines changed: 127 additions & 32 deletions

File tree

‎spectec/doc/semantics/il/4-subst.spectec‎

Lines changed: 119 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
;; TODO: avoid capture
2-
31
;; Substitution
42

53
syntax subst =
@@ -44,6 +42,79 @@ def $bound_param(FUN x `: p* `-> t) = {FUN x}
4442
def $bound_param(GRAM x `: p* `-> t) = {GRAM x}
4543

4644

45+
;; Freshness
46+
47+
relation Fresh_id: id FRESH hint(builtin)
48+
49+
def $refresh_expid(id) : (id, subst) hint(total)
50+
def $refresh_typid(id) : (id, subst) hint(total)
51+
def $refresh_funid(id) : (id, subst) hint(total)
52+
def $refresh_gramid(id) : (id, subst) hint(total)
53+
54+
def $refresh_expid(x) = (x', {EXP (x, VAR x')}) -- Fresh_id: x' FRESH
55+
def $refresh_typid(x) = (x', {TYP (x, VAR x')}) -- Fresh_id: x' FRESH
56+
def $refresh_funid(x) = (x', {FUN (x, x')}) -- Fresh_id: x' FRESH
57+
def $refresh_gramid(x) = (x', {GRAM (x, VAR x')}) -- Fresh_id: x' FRESH
58+
59+
60+
def $refresh_list(syntax X, def $refresh(X) : (X, subst), def $subst(subst, X) : X, X*) : (X*, subst)
61+
def $refresh_list(syntax X, $refresh, $subst, eps) = (eps, {})
62+
def $refresh_list(syntax X, $refresh, $subst, x_1 x*) = (x'_1 x'*, s_1 ++ s)
63+
-- if (x'_1, s_1) = $refresh(x_1)
64+
-- if (x'*, s) = $refresh_list(X, $refresh, $subst, $subst(s_1, x)*)
65+
66+
67+
def $refresh_param(param) : (param, subst)
68+
def $refresh_params(param*) : (param*, subst)
69+
70+
def $refresh_param(EXP x `: t) = (EXP x' `: t, s)
71+
-- if (x', s) = $refresh_expid(x)
72+
def $refresh_param(TYP x) = (TYP x', s)
73+
-- if (x', s) = $refresh_typid(x)
74+
def $refresh_param(FUN x `: p* `-> t) = (FUN x' `: p* `-> t, s)
75+
-- if (x', s) = $refresh_funid(x)
76+
def $refresh_param(GRAM x `: p* `-> t) = (GRAM x' `: p* `-> t, s)
77+
-- if (x', s) = $refresh_gramid(x)
78+
79+
def $refresh_params(p*) =
80+
$refresh_list(param, $refresh_param, $subst_param, p*)
81+
82+
83+
def $refresh_typbind(typbind) : (typbind, subst)
84+
def $refresh_typbinds(typbind*) : (typbind*, subst)
85+
86+
def $refresh_typbind(x `: t) = (x' `: t, s)
87+
-- if (x', s) = $refresh_expid(x)
88+
89+
def $refresh_typbinds(tb*) =
90+
$refresh_list(typbind, $refresh_typbind, $subst_typbind, tb*)
91+
92+
93+
def $refresh_exppull(exppull) : (exppull, subst)
94+
def $refresh_exppulls(exppull*) : (exppull*, subst)
95+
96+
def $refresh_exppull(x `: t `<- e) = (x' `: t `<- e, s)
97+
-- if (x', s) = $refresh_expid(x)
98+
99+
def $refresh_exppulls(tb*) =
100+
$refresh_list(exppull, $refresh_exppull, $subst_exppull, tb*)
101+
102+
103+
def $refresh_iter(iter) : (iter, subst)
104+
105+
def $refresh_iter(QUEST) = (QUEST, {})
106+
def $refresh_iter(STAR) = (STAR, {})
107+
def $refresh_iter(PLUS) = (PLUS, {})
108+
def $refresh_iter(SUP x e) = (SUP x' e, s) -- if (x', s) = $refresh_expid(x)
109+
110+
111+
;; Lists
112+
113+
def $subst_binds(syntax X, def $subst_X(subst, X) : X, subst, X*) : X*
114+
def $subst_binds(syntax X, def $subst_X, s, eps) = eps
115+
def $subst_binds(syntax X, def $subst_X, s, x_1 x*) = eps
116+
117+
47118
;; Identifiers
48119

49120
def $subst_fun(subst, id) : id
@@ -54,17 +125,29 @@ def $subst_fun(s, x) = x -- otherwise
54125
;; Types
55126

56127
def $subst_typ(subst, typ) : typ
57-
def $subst_typ(s, VAR x a*) = t -- if (x,t) <- s.TYP /\ a* = eps
58-
def $subst_typ(s, VAR x a*) = VAR x $subst_arg(s, a)* -- otherwise
59-
def $subst_typ(s, optyp) = optyp
60-
def $subst_typ(s, TUP (x `: t)*) = TUP (x `: $subst_typ(s, t))* ;; TODO: avoid capture
61-
def $subst_typ(s, ITER t it) = ITER $subst_typ(s, t) $subst_iter(s, it)
62-
def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)* WITH $subst_inst(s, inst)*
128+
def $subst_typ(s, t) = t' -- if (t', s') = $subst_refresh_typ(s, t)
129+
130+
def $subst_refresh_typ(subst, typ) : (typ, subst)
131+
def $subst_refresh_typ(s, VAR x a*) = (t, {}) -- if (x,t) <- s.TYP /\ a* = eps
132+
def $subst_refresh_typ(s, VAR x a*) = (VAR x $subst_arg(s, a)*, {}) -- otherwise
133+
def $subst_refresh_typ(s, optyp) = (optyp, {})
134+
def $subst_refresh_typ(s, TUP tb*) = (TUP $subst_typbind(s, tb')*, s')
135+
-- if (tb'*, s') = $refresh_typbinds(tb*)
136+
def $subst_refresh_typ(s, ITER t it) = (ITER $subst_typ(s ++ s', t) $subst_iter(s, it'), {})
137+
-- if (it', s') = $refresh_iter(it)
138+
def $subst_refresh_typ(s, MATCH x a* WITH inst*) = (MATCH x $subst_arg(s, a)* WITH $subst_inst(s, inst)*, {})
63139

64140
def $subst_deftyp(subst, deftyp) : deftyp
65141
def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t)
66-
def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: $subst_typ(s, t) `- `{$subst_quant(s, q)*} $subst_prem(s, pr)*)* ;; TODO: avoid capture
67-
def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: $subst_typ(s, t) `- `{$subst_quant(s, q)*} $subst_prem(s, pr)*)* ;; TODO: avoid capture
142+
def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: t' `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
143+
-- if (t', s') = $subst_refresh_typ(s, t)
144+
-- if (q'*, s'') = $refresh_params(q*)
145+
def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: t' `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
146+
-- if (t', s') = $subst_refresh_typ(s, t)
147+
-- if (q'*, s'') = $refresh_params(q*)
148+
149+
def $subst_typbind(subst, typbind) : typbind
150+
def $subst_typbind(s, x `: t) = x' `: $subst_typ(s, t)
68151

69152

70153
;; Iterators
@@ -73,7 +156,10 @@ def $subst_iter(subst, iter) : iter
73156
def $subst_iter(s, QUEST) = QUEST
74157
def $subst_iter(s, STAR) = STAR
75158
def $subst_iter(s, PLUS) = PLUS
76-
def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e) ;; TODO: avoid capture
159+
def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e)
160+
161+
def $subst_exppull(subst, exppull) : exppull
162+
def $subst_exppull(s, x `: t `<- e') = x `: $subst_typ(s, t) `<- $subst_exp(s, e')
77163

78164

79165
;; Expressions
@@ -101,7 +187,9 @@ def $subst_exp(s, ACC e_1 p) = ACC $subst_exp(s, e_1) $subst_path(s, p)
101187
def $subst_exp(s, UPD e_1 p e_2) = UPD $subst_exp(s, e_1) $subst_path(s, p) $subst_exp(s, e_2)
102188
def $subst_exp(s, EXT e_1 p e_2) = EXT $subst_exp(s, e_1) $subst_path(s, p) $subst_exp(s, e_2)
103189
def $subst_exp(s, CALL x a*) = CALL $subst_fun(s, x) $subst_arg(s, a)*
104-
def $subst_exp(s, ITER e it (x `: t `<- e')*) = ITER $subst_exp(s, e) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e'))* ;; TODO: avoid capture
190+
def $subst_exp(s, ITER e it ep*) = ITER $subst_exp(s ++ s' ++ s'', e) $subst_iter(s, it') $subst_exppull(s, ep')*
191+
-- if (it', s') = $refresh_iter(it)
192+
-- if (ep'*, s'') = $refresh_exppulls(ep*)
105193
def $subst_exp(s, CVT e nt_1 nt_2) = CVT $subst_exp(s, e) nt_1 nt_2
106194
def $subst_exp(s, SUB e t_1 t_2) = SUB $subst_exp(s, e) $subst_typ(s, t_1) $subst_typ(s, t_2)
107195
def $subst_exp(s, MATCH a* WITH clause*) = MATCH $subst_arg(s, a)* WITH $subst_clause(s, clause)*
@@ -127,7 +215,9 @@ def $subst_sym(s, SEQ g*) = SEQ $subst_sym(s, g)*
127215
def $subst_sym(s, ALT g*) = ALT $subst_sym(s, g)*
128216
def $subst_sym(s, RANGE g_1 g_2) = RANGE $subst_sym(s, g_1) $subst_sym(s, g_2)
129217
def $subst_sym(s, ATTR e g) = ATTR $subst_exp(s, e) $subst_sym(s, g)
130-
def $subst_sym(s, ITER g it (x `: t `<- e)*) = ITER $subst_sym(s, g) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e))* ;; TODO: avoid capture
218+
def $subst_sym(s, ITER g it ep*) = ITER $subst_sym(s ++ s' ++ s'', g) $subst_iter(s, it') $subst_exppull(s, ep')*
219+
-- if (it', s') = $refresh_iter(it)
220+
-- if (ep'*, s'') = $refresh_exppulls(ep*)
131221

132222

133223
;; Definitions
@@ -141,31 +231,36 @@ def $subst_arg(s, GRAM g) = GRAM $subst_sym(s, g)
141231
def $subst_param(subst, param) : param
142232
def $subst_param(s, TYP x) = TYP x
143233
def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t)
144-
def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture
145-
def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture
146-
147-
def $subst_quant(subst, quant) : quant
148-
def $subst_quant(s, q) = $subst_param(s, q)
234+
def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p')* `-> $subst_typ(s ++ s', t)
235+
-- if (p'*, s') = $refresh_params(p*)
236+
def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p')* `-> $subst_typ(s ++ s', t)
237+
-- if (p'*, s') = $refresh_params(p*)
149238

150239
def $subst_prem(subst, prem) : prem
151240
def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e)
152241
def $subst_prem(s, IF e) = IF $subst_exp(s, e)
153242
def $subst_prem(s, ELSE) = ELSE
154-
def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture
155-
def $subst_prem(s, ITER pr it (x `: t `<- e)*) = ITER $subst_prem(s, pr) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e))* ;; TODO: avoid capture
243+
def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2)
244+
def $subst_prem(s, ITER pr it ep*) = ITER $subst_prem(s ++ s' ++ s'', pr) $subst_iter(s, it') $subst_exppull(s, ep')*
245+
-- if (it', s') = $refresh_iter(it)
246+
-- if (ep'*, s'') = $refresh_exppulls(ep*)
156247

157248

158249
def $subst_inst(subst, inst) : inst
159-
def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q)*} $subst_arg(s, a)* `= $subst_deftyp(s, dt) ;; TODO: avoid capture
250+
def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `= $subst_deftyp(s ++ s', dt)
251+
-- if (q'*, s') = $refresh_params(q*)
160252

161253
def $subst_rule(subst, rul) : rul
162-
def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q)*} $subst_exp(s, e) `- $subst_prem(s, pr)* ;; TODO: avoid capture
254+
def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q')*} $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
255+
-- if (q'*, s') = $refresh_params(q*)
163256

164257
def $subst_clause(subst, clause) : clause
165-
def $subst_clause(s, CLAUSE `{q*} a* `= e `- pr*) = CLAUSE `{$subst_param(s, q)*} $subst_arg(s, a)* `= $subst_exp(s, e) `- $subst_prem(s, pr)* ;; TODO: avoid capture
258+
def $subst_clause(s, CLAUSE `{q*} a* `= e `- pr*) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `= $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
259+
-- if (q'*, s') = $refresh_params(q*)
166260

167261
def $subst_prod(subst, prod) : prod
168-
def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q)*} $subst_sym(s, g) `=> $subst_exp(s, e) `- $subst_prem(s, pr)* ;; TODO: avoid capture
262+
def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
263+
-- if (q'*, s') = $refresh_params(q*)
169264

170265

171266
;; Constructing substitutions for parameters

‎spectec/doc/semantics/il/5-reduction.spectec‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -365,7 +365,7 @@ rule Step_exp/ITER-PLUS:
365365
rule Step_exp/ITER-STAR:
366366
S |- ITER e STAR (x `: t `<- LIST e'*)* ~> ITER e (SUP y (NAT n)) (x `: t `<- LIST e'*)*
367367
-- if |e'**[0]| = n
368-
;; TODO: y fresh
368+
-- Fresh_id: y FRESH
369369

370370
rule Step_exp/ITER-SUP:
371371
S |- ITER e (SUP y (NAT n)) (x `: t `<- LIST e'^n)* ~> LIST $subst_exp({EXP (x, e'')* (y, NAT i)}, e)^(i<n)
@@ -530,7 +530,7 @@ rule Step_argmatch/plain:
530530

531531
rule Step_argmatch/seq:
532532
S |- `{q_1* q* q_2*} am_1* am am_2* ~>_s
533-
`{q_1* q'* $subst_quant(s, q_2)*} am_1* am'* $subst_argmatch(s, am_2)*
533+
`{q_1* q'* $subst_param(s, q_2)*} am_1* am'* $subst_argmatch(s, am_2)*
534534
-- Step_argmatch: S |- `{q*} am ~>_s `{q'*} am'*
535535

536536
rule Step_argmatch/seq-fail:
@@ -569,7 +569,7 @@ rule Step_argmatch_plain/ctx2:
569569
rule Step_argmatch_plain/eq:
570570
S |- a / a ~> eps
571571

572-
;; TODO: disjoint
572+
;; TODO: disjointness
573573
;;rule Step_argmatch_plain/neq:
574574
;; S |- a / a' ~> FAIL
575575
;; -- Disj_arg: S |- a =/= a'
@@ -581,7 +581,7 @@ rule Step_expmatch/plain:
581581

582582
rule Step_expmatch/seq:
583583
S |- `{q_1* q* q_2*} em_1* em em_2* ~>_s
584-
`{q_1* q'* $subst_quant(s, q_2)*} em_1* em'* $subst_expmatch(s, em_2)*
584+
`{q_1* q'* $subst_param(s, q_2)*} em_1* em'* $subst_expmatch(s, em_2)*
585585
-- Step_expmatch: S |- `{q*} em ~>_s `{q'*} em'*
586586

587587
rule Step_expmatch/seq-fail:
@@ -594,7 +594,7 @@ rule Step_expmatch/ITER-QUEST:
594594
(e / $subst_exp({EXP (x, VAR x')*}, e'))?
595595
(OPT (VAR x'')? / e_p)*
596596
-- if x''?* = $transposeq_(id, x'*?)
597-
;; TODO: x'*? fresh
597+
-- (Fresh_id: x' FRESH)*?
598598
;; Note: inner match can only instantiate iteration variables
599599

600600
rule Step_expmatch/ITER-SUP:
@@ -603,7 +603,7 @@ rule Step_expmatch/ITER-SUP:
603603
(e / $subst_exp({EXP (y, NAT i) (x, VAR x')*}, e'))^(i<n)
604604
(NAT n / e_n) (LIST (VAR x'')^n / e_p)*
605605
-- if x''^n* = $transpose_(id, x'*^n)
606-
;; TODO: x'*^n fresh
606+
-- (Fresh_id: x' FRESH)*^n
607607
;; Note: inner match can only instantiate iteration variables
608608

609609

@@ -713,7 +713,7 @@ rule Step_expmatch_plain/ITER-STAR:
713713
S |- LIST e* / ITER e' STAR (x `: t `<- e_p)* ~>
714714
LIST e* / ITER e' (SUP y (NAT n)) (x `: t `<- e_p)*
715715
-- if |e*| = n
716-
;; TODO: y fresh
716+
-- Fresh_id: y FRESH
717717

718718

719719
rule Step_expmatch_plain/SUB-SUB:
@@ -870,7 +870,7 @@ rule Step_prems/ITER-PLUS:
870870
rule Step_prems/ITER-STAR:
871871
S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)*
872872
-- if |e**[0]| = n
873-
;; TODO: y fresh
873+
-- Fresh_id: y FRESH
874874

875875
rule Step_prems/ITER-SUP:
876876
S |- ITER pr (SUP y (NAT n)) (x `: t `<- LIST e^n)* ~> $subst_prem({EXP (x, e')* (y, NAT i)}, pr)^(i<n)

0 commit comments

Comments
 (0)