Skip to content

Commit 8a4f0d0

Browse files
rossbergrossberg
authored
[spectec] Define IL semantics for pattern matching (#2106)
1 parent 2907f45 commit 8a4f0d0

6 files changed

Lines changed: 553 additions & 127 deletions

File tree

‎spectec/doc/semantics/il/0-aux.spectec‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,15 @@ def $equiv_(syntax X, x_1*, x_2*) = true -- (if x_1 <- x_2*)* -- (if x_2 <- x_
1010
def $equiv_(syntax X, x_1*, x_2*) = false -- otherwise
1111

1212

13+
def $concat_(syntax X, X**) : X* hint(show (++)%2)
14+
def $concat_(syntax X, eps) = eps
15+
def $concat_(syntax X, x_1* x**) = x_1* $concat_(X, x**)
16+
17+
1318
def $transpose_(syntax X, X**) : X**
1419
def $transpose_(syntax X, eps^n) = eps
1520
def $transpose_(syntax X, (x_1 x*)*) = x_1* $transpose_(X, x**)
21+
22+
def $transposeq_(syntax X, X*?) : X?*
23+
def $transposeq_(syntax X, (eps)) = eps
24+
def $transposeq_(syntax X, (x_1 x*)?) = x_1? $transposeq_(X, x*?)

‎spectec/doc/semantics/il/1-syntax.spectec‎

Lines changed: 30 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ syntax typ =
2323
| TUP typbind* ;; (id : typ , ... , id : typ)
2424
| ITER typ iter ;; typ iter
2525
| VAR id arg* ;; typid(arg*)
26+
| MATCH id arg* WITH inst* ;; `match` typid(arg*) `with` inst*
2627

2728
syntax deftyp =
2829
| ALIAS typ
@@ -40,7 +41,7 @@ syntax iter =
4041
| QUEST ;; `?`
4142
| STAR ;; `*`
4243
| PLUS ;; `+`
43-
| SUP id? exp ;; `^` (id `<`)? exp
44+
| SUP id exp ;; `^` id `<` exp
4445

4546

4647
;; Expressions
@@ -101,33 +102,34 @@ syntax valfield = atom `= val ;; atom `=` val
101102

102103

103104
syntax exp =
104-
| num ;; num
105-
| VAR id ;; varid
106-
| BOOL bool ;; bool
107-
| TEXT text ;; text
108-
| UN unop exp ;; unop exp
109-
| BIN binop exp exp ;; exp binop exp
110-
| CMP cmpop exp exp ;; exp cmpop exp
111-
| TUP exp* ;; ( exp* )
112-
| INJ mixop exp ;; mixop exp
113-
| OPT exp? ;; exp?
114-
| LIST exp* ;; [ exp* ]
115-
| LIFT exp ;; exp : _? <: _*
116-
| STR expfield* ;; { expfield* }
117-
| SEL exp nat ;; exp.i
118-
| LEN exp ;; | exp |
119-
| MEM exp exp ;; exp `<-` exp
120-
| CAT exp exp ;; exp `++` exp
121-
| ACC exp path ;; exp[ path ]
122-
| UPD exp path exp ;; exp[ path = exp ]
123-
| EXT exp path exp ;; exp[ path =.. exp ]
124-
| CALL id arg* ;; defid( arg* )
105+
| num ;; num
106+
| VAR id ;; varid
107+
| BOOL bool ;; bool
108+
| TEXT text ;; text
109+
| UN unop exp ;; unop exp
110+
| BIN binop exp exp ;; exp binop exp
111+
| CMP cmpop exp exp ;; exp cmpop exp
112+
| TUP exp* ;; ( exp* )
113+
| INJ mixop exp ;; mixop exp
114+
| OPT exp? ;; exp?
115+
| LIST exp* ;; [ exp* ]
116+
| LIFT exp ;; exp : _? <: _*
117+
| STR expfield* ;; { expfield* }
118+
| SEL exp nat ;; exp.i
119+
| LEN exp ;; | exp |
120+
| MEM exp exp ;; exp `<-` exp
121+
| CAT exp exp ;; exp `++` exp
122+
| ACC exp path ;; exp[ path ]
123+
| UPD exp path exp ;; exp[ path = exp ]
124+
| EXT exp path exp ;; exp[ path =.. exp ]
125+
| CALL id arg* ;; defid( arg* )
125126
| ITER exp iter exppull* ;; exp iter{ expiter* }
126127
| CVT exp numtyp numtyp ;; exp : typ1 <:> typ2
127128
| SUB exp typ typ ;; exp : typ1 <: typ2
129+
| MATCH arg* WITH clause* ;; `match` arg* `with` clause*
128130

129-
syntax expfield = atom `= exp ;; atom `=` exp
130-
syntax exppull = id `<- exp ;; id `<-` exp
131+
syntax expfield = atom `= exp
132+
syntax exppull = id `: typ `<- exp
131133

132134
syntax path =
133135
| ROOT ;;
@@ -154,23 +156,24 @@ syntax sym =
154156
;; Definitions
155157

156158
syntax arg =
157-
| EXP exp
158159
| TYP typ
160+
| EXP exp
159161
| FUN id
160162
| GRAM sym
161163

162164
syntax param =
163-
| EXP id `: typ
164165
| TYP id
166+
| EXP id `: typ
165167
| FUN id `: param* `-> typ
166168
| GRAM id `: param* `-> typ
167169

168170
syntax quant = param
169171

170172
syntax prem =
171-
| RULE id arg* `: exp
173+
| REL id arg* `: exp
172174
| IF exp
173175
| ELSE
176+
| NOT prem
174177
| LET exp `= exp ;; TODO: variables/quantifiers?
175178
| ITER prem iter exppull*
176179

‎spectec/doc/semantics/il/3-primitives.spectec‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ def $boolbin(EQUIV, b_1, b_2) = b_1 <=> b_2
1717

1818
def $iszero(num) : bool
1919
def $isone(num) : bool
20+
def $isneg(num) : bool
2021

2122
def $iszero(NAT n) = (n = 0)
2223
def $iszero(INT i) = (i = 0)
@@ -28,6 +29,11 @@ def $isone(INT i) = (i = 1)
2829
def $isone(RAT q) = (q = 1)
2930
def $isone(REAL r) = (r = 1)
3031

32+
def $isneg(NAT n) = false
33+
def $isneg(INT i) = (i < 0)
34+
def $isneg(RAT q) = (q < 0)
35+
def $isneg(REAL r) = (r < 0)
36+
3137

3238
def $numcvt(numtyp, num) : num hint(partial)
3339

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

Lines changed: 42 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,11 @@ syntax subst =
1010
}
1111

1212

13+
def $composesubsts(subst*) : subst hint(show (++)%)
14+
def $composesubsts(eps) = {}
15+
def $composesubsts(s_1 s*) = s_1 ++ $composesubsts(s*)
16+
17+
1318
;; Domain
1419

1520
syntax dom =
@@ -54,6 +59,7 @@ def $subst_typ(s, VAR x a*) = VAR x $subst_arg(s, a)* -- otherwise
5459
def $subst_typ(s, optyp) = optyp
5560
def $subst_typ(s, TUP (x `: t)*) = TUP (x `: $subst_typ(s, t))* ;; TODO: avoid capture
5661
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)*
5763

5864
def $subst_deftyp(subst, deftyp) : deftyp
5965
def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t)
@@ -67,7 +73,7 @@ def $subst_iter(subst, iter) : iter
6773
def $subst_iter(s, QUEST) = QUEST
6874
def $subst_iter(s, STAR) = STAR
6975
def $subst_iter(s, PLUS) = PLUS
70-
def $subst_iter(s, SUP x? e) = SUP x? $subst_exp(s, e) ;; TODO: avoid capture
76+
def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e) ;; TODO: avoid capture
7177

7278

7379
;; Expressions
@@ -95,9 +101,10 @@ def $subst_exp(s, ACC e_1 p) = ACC $subst_exp(s, e_1) $subst_path(s, p)
95101
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)
96102
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)
97103
def $subst_exp(s, CALL x a*) = CALL $subst_fun(s, x) $subst_arg(s, a)*
98-
def $subst_exp(s, ITER e it (x `<- e')*) = ITER $subst_exp(s, e) $subst_iter(s, it) (x `<- $subst_exp(s, e'))* ;; TODO: avoid capture
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
99105
def $subst_exp(s, CVT e nt_1 nt_2) = CVT $subst_exp(s, e) nt_1 nt_2
100106
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)
107+
def $subst_exp(s, MATCH a* WITH clause*) = MATCH $subst_arg(s, a)* WITH $subst_clause(s, clause)*
101108

102109
def $subst_path(subst, path) : path
103110
def $subst_path(s, ROOT) = ROOT
@@ -120,39 +127,66 @@ def $subst_sym(s, SEQ g*) = SEQ $subst_sym(s, g)*
120127
def $subst_sym(s, ALT g*) = ALT $subst_sym(s, g)*
121128
def $subst_sym(s, RANGE g_1 g_2) = RANGE $subst_sym(s, g_1) $subst_sym(s, g_2)
122129
def $subst_sym(s, ATTR e g) = ATTR $subst_exp(s, e) $subst_sym(s, g)
123-
def $subst_sym(s, ITER g it (x `<- e)*) = ITER $subst_sym(s, g) $subst_iter(s, it) (x `<- $subst_exp(s, e))* ;; TODO: avoid capture
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
124131

125132

126133
;; Definitions
127134

128135
def $subst_arg(subst, arg) : arg
129-
def $subst_arg(s, EXP e) = EXP $subst_exp(s, e)
130136
def $subst_arg(s, TYP t) = TYP $subst_typ(s, t)
137+
def $subst_arg(s, EXP e) = EXP $subst_exp(s, e)
131138
def $subst_arg(s, FUN x) = FUN $subst_fun(s, x)
132139
def $subst_arg(s, GRAM g) = GRAM $subst_sym(s, g)
133140

134141
def $subst_param(subst, param) : param
135-
def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t)
136142
def $subst_param(s, TYP x) = TYP x
143+
def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t)
137144
def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture
138145
def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture
139146

140147
def $subst_quant(subst, quant) : quant
141148
def $subst_quant(s, q) = $subst_param(s, q)
142149

143150
def $subst_prem(subst, prem) : prem
144-
def $subst_prem(s, RULE x a* `: e) = RULE x $subst_arg(s, a)* `: $subst_exp(s, e)
151+
def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e)
145152
def $subst_prem(s, IF e) = IF $subst_exp(s, e)
146153
def $subst_prem(s, ELSE) = ELSE
147154
def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture
148-
def $subst_prem(s, ITER pr it (x `<- e)*) = ITER $subst_prem(s, pr) $subst_iter(s, it) (x `<- $subst_exp(s, e))* ;; 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
156+
157+
158+
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
160+
161+
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
163+
164+
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
166+
167+
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
169+
170+
171+
;; Constructing substitutions for parameters
172+
173+
def $arg_for_param(arg, param) : subst
174+
def $arg_for_param(TYP t, TYP x) = {TYP (x, t)}
175+
def $arg_for_param(EXP e, EXP x `: t) = {EXP (x, e)}
176+
def $arg_for_param(FUN y, FUN x `: p* `-> t) = {FUN (x, y)}
177+
def $arg_for_param(GRAM g, GRAM x `: p* `-> t) = {GRAM (x, g)}
178+
179+
def $args_for_params(arg*, param*) : subst
180+
def $args_for_params(eps, eps) = {}
181+
def $args_for_params(a_1 a*, p_1 p*) = s ++ $args_for_params(a*, $subst_param(s, p)*)
182+
-- if s = $arg_for_param(a_1, p_1)
149183

150184

151185
;; Well-formedness
152186

153187
def $paramarg(param) : arg
154-
def $paramarg(EXP x `: t) = EXP (VAR x)
155188
def $paramarg(TYP x) = TYP (VAR x)
189+
def $paramarg(EXP x `: t) = EXP (VAR x)
156190
def $paramarg(FUN x `: p* `-> t) = FUN x
157191
def $paramarg(GRAM x `: p* `-> t) = GRAM (VAR x)
158192

0 commit comments

Comments
 (0)