Skip to content

Commit f9c743a

Browse files
rossbergrossberg
committed
[spectec] Minor tweak to syntax in IL semantics
1 parent 91f9d08 commit f9c743a

4 files changed

Lines changed: 28 additions & 28 deletions

File tree

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -184,9 +184,9 @@ syntax dec =
184184
| GRAM id param* `: typ `= prod*
185185
| REC dec*
186186

187-
syntax inst = INST `{quant*} arg* `= deftyp
187+
syntax inst = INST `{quant*} arg* `=> deftyp
188188
syntax rul = RULE `{quant*} exp `- prem*
189-
syntax clause = CLAUSE `{quant*} arg* `= exp `- prem*
189+
syntax clause = CLAUSE `{quant*} arg* `=> exp `- prem*
190190
syntax prod = PROD `{quant*} sym `=> exp `- prem*
191191

192192

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -250,15 +250,15 @@ def $subst_prem(s, ITER pr it ep*) = ITER $subst_prem(s ++ s' ++ s'', pr) $subst
250250

251251

252252
def $subst_inst(subst, inst) : inst
253-
def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `= $subst_deftyp(s ++ s', dt)
253+
def $subst_inst(s, INST `{q*} a* `=> dt) = INST `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_deftyp(s ++ s', dt)
254254
-- if (q'*, s') = $refresh_params(q*)
255255

256256
def $subst_rule(subst, rul) : rul
257257
def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q')*} $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
258258
-- if (q'*, s') = $refresh_params(q*)
259259

260260
def $subst_clause(subst, clause) : clause
261-
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)*
261+
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)*
262262
-- if (q'*, s') = $refresh_params(q*)
263263

264264
def $subst_prod(subst, prod) : prod

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

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ rule Expand_typ/plain:
1313

1414
rule Expand_typ/def:
1515
S |- t ~~ dt
16-
-- Reduce_typ: S |- t ~>* MATCH x WITH (INST `{} `= dt) inst*
16+
-- Reduce_typ: S |- t ~>* MATCH x WITH (INST `{} `=> dt) inst*
1717

1818

1919
rule Eq_typ:
@@ -51,17 +51,17 @@ rule Step_typ/MATCH-ctx2:
5151
-- Step_inst: S |- inst*[n] ~> inst'_n
5252

5353
rule Step_typ/MATCH-alias:
54-
S |- MATCH x eps WITH (INST `{} eps `= ALIAS t) inst* ~> t
54+
S |- MATCH x eps WITH (INST `{} eps `=> ALIAS t) inst* ~> t
5555

5656
rule Step_typ/MATCH-match:
57-
S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~>
57+
S |- MATCH x a* WITH (INST `{q*} a'* `=> dt) inst* ~>
5858
MATCH x a''* WITH
59-
(INST `{q'*} a'''* `= $subst_deftyp(s, dt))
60-
(INST `{} a''* `= ALIAS (MATCH x a* WITH inst*))
59+
(INST `{q'*} a'''* `=> $subst_deftyp(s, dt))
60+
(INST `{} a''* `=> ALIAS (MATCH x a* WITH inst*))
6161
-- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{q'*} (a'' / a''')*
6262

6363
rule Step_typ/MATCH-match-fail:
64-
S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~>
64+
S |- MATCH x a* WITH (INST `{q*} a'* `=> dt) inst* ~>
6565
MATCH x a* WITH inst*
6666
-- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{} FAIL
6767

@@ -420,15 +420,15 @@ rule Step_exp/SUB-LIST:
420420

421421
rule Step_exp/SUB-STR:
422422
S |- SUB (STR (at `= e)*) t_1 t_2 ~> STR (at' `= SUB e t'_1 t'_2)*
423-
-- if t_1 = MATCH x_1 WITH (INST `{} `= STRUCT tf_1*)
424-
-- if t_2 = MATCH x_2 WITH (INST `{} `= STRUCT tf_2*)
423+
-- if t_1 = MATCH x_1 WITH (INST `{} `=> STRUCT tf_1*)
424+
-- if t_2 = MATCH x_2 WITH (INST `{} `=> STRUCT tf_2*)
425425
-- (if (at' `: t'_1 `- `{q_1*} pr_1*) <- tf_1*)*
426426
-- (if (at' `: t'_2 `- `{q_2*} pr_2*) = tf_2)*
427427

428428
rule Step_exp/SUB-CASE:
429429
S |- SUB (INJ op e) t_1 t_2 ~> INJ op (SUB e t'_1 t'_2)
430-
-- if t_1 = MATCH x_1 WITH (INST `{} `= VARIANT tc_1*)
431-
-- if t_2 = MATCH x_2 WITH (INST `{} `= VARIANT tc_2*)
430+
-- if t_1 = MATCH x_1 WITH (INST `{} `=> VARIANT tc_1*)
431+
-- if t_2 = MATCH x_2 WITH (INST `{} `=> VARIANT tc_2*)
432432
-- if (op `: t'_1 `- `{q_1*} pr_1*) <- tc_1*
433433
-- if (op `: t'_2 `- `{q_2*} pr_2*) <- tc_2*
434434

@@ -442,28 +442,28 @@ rule Step_exp/MATCH-ctx2:
442442
-- Step_clause: S |- clause*[n] ~> clause'_n
443443

444444
rule Step_exp/MATCH-match:
445-
S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~>
445+
S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~>
446446
MATCH a''* WITH
447-
(CLAUSE `{q'*} a'''* `= $subst_exp(s, e) `- $subst_prem(s, pr)*)
448-
(CLAUSE `{} a''* `= (MATCH a* WITH clause*) `- eps)
447+
(CLAUSE `{q'*} a'''* `=> $subst_exp(s, e) `- $subst_prem(s, pr)*)
448+
(CLAUSE `{} a''* `=> (MATCH a* WITH clause*) `- eps)
449449
-- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{q'*} (a'' / a''')*
450450

451451
rule Step_exp/MATCH-match-fail:
452-
S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~>
452+
S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~>
453453
MATCH a''* WITH clause*
454454
-- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{} FAIL
455455

456456
rule Step_exp/MATCH-guess:
457-
S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~>
458-
MATCH a* WITH (CLAUSE `{} $subst_arg(s, a')* `= e `- pr*) clause*
457+
S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~>
458+
MATCH a* WITH (CLAUSE `{} $subst_arg(s, a')* `=> e `- pr*) clause*
459459
-- Ok_subst: $storeenv(S) |- s : q*
460460
;; Note: non-computational rule
461461

462462
rule Step_exp/MATCH-true:
463-
S |- MATCH eps WITH (CLAUSE `{} eps `= e `- eps) clause* ~> e
463+
S |- MATCH eps WITH (CLAUSE `{} eps `=> e `- eps) clause* ~> e
464464

465465
rule Step_exp/MATCH-false:
466-
S |- MATCH eps WITH (CLAUSE `{} eps `= e `- (IF (BOOL false)) pr*) clause* ~>
466+
S |- MATCH eps WITH (CLAUSE `{} eps `=> e `- (IF (BOOL false)) pr*) clause* ~>
467467
MATCH eps WITH clause*
468468

469469

@@ -730,20 +730,20 @@ relation Step_inst: S |- inst ~> inst
730730
relation Step_clause: S |- clause ~> clause
731731

732732
rule Step_inst/INST-ctx:
733-
S |- INST `{q*} a* `= t ~> INST `{q*} a*[[n] = a'_n] `= t
733+
S |- INST `{q*} a* `=> t ~> INST `{q*} a*[[n] = a'_n] `=> t
734734
-- Step_arg: S |- a*[n] ~> a'_n
735735

736736

737737
rule Step_clause/CLAUSE-ctx1:
738-
S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a*[[n] = a'_n] `= e `- pr*
738+
S |- CLAUSE `{q*} a* `=> e `- pr* ~> CLAUSE `{q*} a*[[n] = a'_n] `=> e `- pr*
739739
-- Step_arg: S |- a*[n] ~> a'_n
740740

741741
rule Step_clause/CLAUSE-ctx2:
742-
S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e' `- pr*
742+
S |- CLAUSE `{q*} a* `=> e `- pr* ~> CLAUSE `{q*} a* `=> e' `- pr*
743743
-- Step_exp: S |- e ~> e'
744744

745745
rule Step_clause/CLAUSE-ctx3:
746-
S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'*
746+
S |- CLAUSE `{q*} a* `=> e `- pr* ~> CLAUSE `{q*} a* `=> e `- pr'*
747747
-- Step_prems: S |- pr* ~> pr'*
748748

749749

‎spectec/doc/semantics/il/6-typing.spectec‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -633,7 +633,7 @@ rule Ok_decs/cons:
633633
relation Ok_inst: E |- inst : param* -> OK
634634

635635
rule Ok_inst:
636-
E |- INST `{q*} a* `= dt : p* -> OK
636+
E |- INST `{q*} a* `=> dt : p* -> OK
637637
-- Ok_params: E |- q* : OK
638638
-- Ok_args: E ++ $paramenv(q*) |- a* : p* => s
639639
-- Ok_deftyp: E ++ $paramenv(q*) |- dt : OK
@@ -649,7 +649,7 @@ rule Ok_rule:
649649
relation Ok_clause: E |- clause : param* -> typ
650650

651651
rule Ok_clause:
652-
E |- CLAUSE `{q*} a* `= e `- pr* : p* -> t
652+
E |- CLAUSE `{q*} a* `=> e `- pr* : p* -> t
653653
-- Ok_params: E |- q* : OK
654654
-- Ok_args: E ++ $paramenv(q*) |- a* : p* => s
655655
-- Ok_exp: E ++ $paramenv(q*) |- e : t

0 commit comments

Comments
 (0)