From 9487d422076cbe3ad018c5bed9945d25591f05f7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 10 Mar 2026 14:34:23 +0100 Subject: [PATCH 1/8] [spectec] Formalise IL pattern matching --- spectec/doc/semantics/il/0-aux.spectec | 9 + spectec/doc/semantics/il/1-syntax.spectec | 55 +-- spectec/doc/semantics/il/3-primitives.spectec | 6 + spectec/doc/semantics/il/4-subst.spectec | 42 +- spectec/doc/semantics/il/5-reduction.spectec | 427 +++++++++++++++--- spectec/doc/semantics/il/6-typing.spectec | 56 ++- 6 files changed, 484 insertions(+), 111 deletions(-) diff --git a/spectec/doc/semantics/il/0-aux.spectec b/spectec/doc/semantics/il/0-aux.spectec index 7f322499c6..e3a72d38dc 100644 --- a/spectec/doc/semantics/il/0-aux.spectec +++ b/spectec/doc/semantics/il/0-aux.spectec @@ -10,6 +10,15 @@ def $equiv_(syntax X, x_1*, x_2*) = true -- (if x_1 <- x_2*)* -- (if x_2 <- x_ def $equiv_(syntax X, x_1*, x_2*) = false -- otherwise +def $concat_(syntax X, X**) : X* hint(show (++)%2) +def $concat_(syntax X, eps) = eps +def $concat_(syntax X, x_1* x**) = x_1* $concat_(X, x**) + + def $transpose_(syntax X, X**) : X** def $transpose_(syntax X, eps^n) = eps def $transpose_(syntax X, (x_1 x*)*) = x_1* $transpose_(X, x**) + +def $transposeq_(syntax X, X*?) : X?* +def $transposeq_(syntax X, (eps)) = eps +def $transposeq_(syntax X, (x_1 x*)?) = x_1? $transposeq_(X, x*?) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index 5278bf572b..fbe814ed9c 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -32,6 +32,7 @@ syntax plaintyp = syntax typ = | plaintyp | VAR id arg* ;; typid(arg*) + | MATCH id arg* WITH inst* ;; `match` typid(arg*) `with` inst* syntax deftyp = | ALIAS typ @@ -49,7 +50,7 @@ syntax iter = | QUEST ;; `?` | STAR ;; `*` | PLUS ;; `+` - | SUP id? exp ;; `^` (id `<`)? exp + | SUP id exp ;; `^` id `<` exp ;; Expressions @@ -110,33 +111,34 @@ syntax valfield = atom `= val ;; atom `=` val syntax exp = - | num ;; num - | VAR id ;; varid - | BOOL bool ;; bool - | TEXT text ;; text - | UN unop exp ;; unop exp - | BIN binop exp exp ;; exp binop exp - | CMP cmpop exp exp ;; exp cmpop exp - | TUP exp* ;; ( exp* ) - | INJ mixop exp ;; mixop exp - | OPT exp? ;; exp? - | LIST exp* ;; [ exp* ] - | LIFT exp ;; exp : _? <: _* - | STR expfield* ;; { expfield* } - | SEL exp nat ;; exp.i - | LEN exp ;; | exp | - | MEM exp exp ;; exp `<-` exp - | CAT exp exp ;; exp `++` exp - | ACC exp path ;; exp[ path ] - | UPD exp path exp ;; exp[ path = exp ] - | EXT exp path exp ;; exp[ path =.. exp ] - | CALL id arg* ;; defid( arg* ) + | num ;; num + | VAR id ;; varid + | BOOL bool ;; bool + | TEXT text ;; text + | UN unop exp ;; unop exp + | BIN binop exp exp ;; exp binop exp + | CMP cmpop exp exp ;; exp cmpop exp + | TUP exp* ;; ( exp* ) + | INJ mixop exp ;; mixop exp + | OPT exp? ;; exp? + | LIST exp* ;; [ exp* ] + | LIFT exp ;; exp : _? <: _* + | STR expfield* ;; { expfield* } + | SEL exp nat ;; exp.i + | LEN exp ;; | exp | + | MEM exp exp ;; exp `<-` exp + | CAT exp exp ;; exp `++` exp + | ACC exp path ;; exp[ path ] + | UPD exp path exp ;; exp[ path = exp ] + | EXT exp path exp ;; exp[ path =.. exp ] + | CALL id arg* ;; defid( arg* ) | ITER exp iter exppull* ;; exp iter{ expiter* } | CVT exp numtyp numtyp ;; exp : typ1 <:> typ2 | SUB exp typ typ ;; exp : typ1 <: typ2 + | MATCH arg* WITH clause* ;; `match` arg* `with` clause* -syntax expfield = atom `= exp ;; atom `=` exp -syntax exppull = id `<- exp ;; id `<-` exp +syntax expfield = atom `= exp +syntax exppull = id `<- exp syntax path = | ROOT ;; @@ -163,14 +165,14 @@ syntax sym = ;; Definitions syntax arg = - | EXP exp | TYP typ + | EXP exp | FUN id | GRAM sym syntax param = - | EXP id `: typ | TYP id + | EXP id `: typ | FUN id `: param* `-> typ | GRAM id `: param* `-> typ @@ -180,6 +182,7 @@ syntax prem = | RULE id arg* `: exp | IF exp | ELSE + | NOT prem | LET exp `= exp ;; TODO: variables/quantifiers? | ITER prem iter exppull* diff --git a/spectec/doc/semantics/il/3-primitives.spectec b/spectec/doc/semantics/il/3-primitives.spectec index 49ce49c6a8..caa5064665 100644 --- a/spectec/doc/semantics/il/3-primitives.spectec +++ b/spectec/doc/semantics/il/3-primitives.spectec @@ -17,6 +17,7 @@ def $boolbin(EQUIV, b_1, b_2) = b_1 <=> b_2 def $iszero(num) : bool def $isone(num) : bool +def $isneg(num) : bool def $iszero(NAT n) = (n = 0) def $iszero(INT i) = (i = 0) @@ -28,6 +29,11 @@ def $isone(INT i) = (i = 1) def $isone(RAT q) = (q = 1) def $isone(REAL r) = (r = 1) +def $isneg(NAT n) = false +def $isneg(INT i) = (i < 0) +def $isneg(RAT q) = (q < 0) +def $isneg(REAL r) = (r < 0) + def $numcvt(numtyp, num) : num hint(partial) diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec index f2a9998b5b..d218069793 100644 --- a/spectec/doc/semantics/il/4-subst.spectec +++ b/spectec/doc/semantics/il/4-subst.spectec @@ -10,6 +10,11 @@ syntax subst = } +def $composesubsts(subst*) : subst hint(show (++)%) +def $composesubsts(eps) = {} +def $composesubsts(s_1 s*) = s_1 ++ $composesubsts(s*) + + ;; Domain syntax dom = @@ -54,6 +59,7 @@ def $subst_typ(s, VAR x a*) = VAR x $subst_arg(s, a)* -- otherwise def $subst_typ(s, optyp) = optyp def $subst_typ(s, TUP (x `: t)*) = TUP (x `: $subst_typ(s, t))* ;; TODO: avoid capture def $subst_typ(s, ITER t it) = ITER $subst_typ(s, t) $subst_iter(s, it) +def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)* WITH $subst_inst(s, inst)* def $subst_deftyp(subst, deftyp) : deftyp def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t) @@ -67,7 +73,7 @@ def $subst_iter(subst, iter) : iter def $subst_iter(s, QUEST) = QUEST def $subst_iter(s, STAR) = STAR def $subst_iter(s, PLUS) = PLUS -def $subst_iter(s, SUP x? e) = SUP x? $subst_exp(s, e) ;; TODO: avoid capture +def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e) ;; TODO: avoid capture ;; Expressions @@ -98,6 +104,7 @@ def $subst_exp(s, CALL x a*) = CALL $subst_fun(s, x) $subst_arg(s, a)* 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 def $subst_exp(s, CVT e nt_1 nt_2) = CVT $subst_exp(s, e) nt_1 nt_2 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) +def $subst_exp(s, MATCH a* WITH clause*) = MATCH $subst_arg(s, a)* WITH $subst_clause(s, clause)* def $subst_path(subst, path) : path def $subst_path(s, ROOT) = ROOT @@ -126,14 +133,14 @@ def $subst_sym(s, ITER g it (x `<- e)*) = ITER $subst_sym(s, g) $subst_iter(s, i ;; Definitions def $subst_arg(subst, arg) : arg -def $subst_arg(s, EXP e) = EXP $subst_exp(s, e) def $subst_arg(s, TYP t) = TYP $subst_typ(s, t) +def $subst_arg(s, EXP e) = EXP $subst_exp(s, e) def $subst_arg(s, FUN x) = FUN $subst_fun(s, x) def $subst_arg(s, GRAM g) = GRAM $subst_sym(s, g) def $subst_param(subst, param) : param -def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t) def $subst_param(s, TYP x) = TYP x +def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t) def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture @@ -148,11 +155,38 @@ def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2 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 +def $subst_inst(subst, inst) : inst +def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q)*} $subst_arg(s, a)* `= $subst_deftyp(s, dt) ;; TODO: avoid capture + +def $subst_rule(subst, rul) : rul +def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q)*} $subst_exp(s, e) `- $subst_prem(s, pr)* ;; TODO: avoid capture + +def $subst_clause(subst, clause) : clause +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 + +def $subst_prod(subst, prod) : prod +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 + + +;; Constructing substitutions for parameters + +def $arg_for_param(arg, param) : subst +def $arg_for_param(TYP t, TYP x) = {TYP (x, t)} +def $arg_for_param(EXP e, EXP x `: t) = {EXP (x, e)} +def $arg_for_param(FUN y, FUN x `: p* `-> t) = {FUN (x, y)} +def $arg_for_param(GRAM g, GRAM x `: p* `-> t) = {GRAM (x, g)} + +def $args_for_params(arg*, param*) : subst +def $args_for_params(eps, eps) = {} +def $args_for_params(a_1 a*, p_1 p*) = s ++ $args_for_params(a*, $subst_param(s, p)*) + -- if s = $arg_for_param(a_1, p_1) + + ;; Well-formedness def $paramarg(param) : arg -def $paramarg(EXP x `: t) = EXP (VAR x) def $paramarg(TYP x) = TYP (VAR x) +def $paramarg(EXP x `: t) = EXP (VAR x) def $paramarg(FUN x `: p* `-> t) = FUN x def $paramarg(GRAM x `: p* `-> t) = GRAM (VAR x) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 2b3c2563ac..9992efc574 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -1,25 +1,19 @@ ;; Types -relation Expand_typ: S |- typ => deftyp relation Reduce_typ: S |- typ ~>* typ relation Step_typ: S |- typ ~> typ relation Eq_typ: S |- typ == typ +relation Expand_typ: S |- typ ~~ deftyp rule Expand_typ/plain: - S |- t => ALIAS t + S |- t ~~ ALIAS t' + -- Reduce_typ: S |- t ~>* t' -- if t = plaintyp -rule Expand_typ/alias: - S |- VAR x a* => dt - -- Expand_typ: S |- VAR x a* => ALIAS t - -- Expand_typ: S |- t => dt - -rule Expand_typ/step: - S |- VAR x a* => $subst_deftyp(s, dt) - -- if (x, p* `-> OK `= inst*) <- S.TYP - -- if (INST `{q*} a'* `= dt) <- inst* - -- Match_args: S |- a* `/ `{q*} a'* => s +rule Expand_typ/def: + S |- t ~~ dt + -- Reduce_typ: S |- t ~>* MATCH x eps WITH (INST `{} eps `= dt) inst* rule Eq_typ: @@ -27,9 +21,10 @@ rule Eq_typ: -- Reduce_typ: S |- t_1 ~>* t'_1 -- Reduce_typ: S |- t_2 ~>* t'_2 -- if t'_1 = t'_2 + ;; Note: defined types are nominal -rule Reduce_typ/normal: +rule Reduce_typ/refl: S |- t ~>* t rule Reduce_typ/step: @@ -43,8 +38,32 @@ rule Step_typ/VAR-ctx: -- Step_arg: S |- a*[n] ~> a'_n rule Step_typ/VAR-apply: - S |- VAR x a* ~> t - -- Expand_typ: S |- VAR x a* => ALIAS t + S |- VAR x a* ~> MATCH x a* WITH inst* + -- if (x, p* `-> OK `= inst*) <- E.TYP + + +rule Step_typ/MATCH-ctx: + S |- MATCH x a* WITH inst* ~> MATCH x a*[[n] = a'_n] WITH inst* + -- Step_arg: S |- a*[n] ~> a'_n + +rule Step_typ/MATCH-ctx2: + S |- MATCH x a* WITH inst* ~> MATCH x a* WITH inst*[[n] = inst'_n] + -- Step_inst: S |- inst*[n] ~> inst'_n + +rule Step_typ/MATCH-alias: + S |- MATCH x eps WITH (INST `{} eps `= ALIAS t) inst* ~> t + +rule Step_typ/MATCH-match: + S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~> + MATCH x a''* WITH + (INST `{q'*} a'''* `= $subst_deftyp(s, dt)) + (INST `{} a''* `= ALIAS (MATCH x a* WITH inst*)) + -- Step_argsmatch: S |- (a* / `{q*} a'*) ~>_s (a''* / `{q'*} a'''*) + +rule Step_typ/MATCH-match-fail: + S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~> + MATCH x a''* WITH inst* + -- Step_argsmatch: S |- (a* / `{q*} a'*) ~>_s FAIL rule Step_typ/TUP-ctx: @@ -57,13 +76,27 @@ rule Step_typ/ITER-ctx: -- Step_typ: S |- t ~> t' +;; Iterators + +relation Step_iter: S |- iter ~> iter +relation Step_exppull: S |- exppull ~> exppull + +rule Step_iter/SUP-ctx: + S |- SUP x e ~> SUP x e' + -- Step_exp: S |- e ~> e' + + +rule Step_exppull/ctx: + S |- x `<- e ~> x `<- e' + -- Step_exp: S |- e ~> e' + + ;; Expressions relation Reduce_exp: S |- exp ~>* exp relation Step_exp: S |- exp ~> exp +relation Step_expfield: S |- expfield ~> expfield relation Step_path: S |- path ~> path -relation Step_iter: S |- iter ~> iter -relation Step_exppull: S |- exppull ~> exppull relation Eq_exp: S |- exp == exp @@ -74,7 +107,7 @@ rule Eq_exp: -- if e'_1 = e'_2 -rule Reduce_exp/normal: +rule Reduce_exp/refl: S |- e ~>* e rule Reduce_exp/step: @@ -150,8 +183,8 @@ rule Step_exp/TUP-ctx: -- Step_exp: S |- e*[n] ~> e'_n rule Step_exp/STR-ctx: - S |- STR (a `= e)* ~> STR (a `= e)*[[n] = (a*[n] `= e'_n)] - -- Step_exp: S |- e*[n] ~> e'_n + S |- STR ef* ~> STR ef*[[n] = ef'_n] + -- Step_expfield: S |- ef*[n] ~> ef'_n rule Step_exp/INJ-ctx: S |- INJ mixop e ~> INJ mixop e' @@ -326,15 +359,12 @@ rule Step_exp/ITER-PLUS: -- if |e'**[0]| >= 1 rule Step_exp/ITER-STAR: - S |- ITER e STAR (x `<- LIST e'*)* ~> ITER e (SUP (NAT n)) (x `<- LIST e'*)* + S |- ITER e STAR (x `<- LIST e'*)* ~> ITER e (SUP y (NAT n)) (x `<- LIST e'*)* -- if |e'**[0]| = n - -rule Step_exp/ITER-SUP-eps: - S |- ITER e (SUP eps e_n) (x `<- LIST e'*)* ~> ITER e (SUP y e_n) (x `<- LIST e'*)* ;; TODO: y fresh rule Step_exp/ITER-SUP: - S |- ITER e (SUP x_i (NAT n)) (x `<- LIST e'^n)* ~> LIST $subst_exp({EXP (x, e'')* (x_i, NAT i)}, e)^(i LIST $subst_exp({EXP (x, e'')* (y, NAT i)}, e)^(i a'_n rule Step_exp/CALL-apply: - S |- CALL x a* ~> $subst_exp(s, e) - -- if (x, p* `-> t `= clause*) <- S.FUN - -- if (CLAUSE `{q*} a'* `= e `- pr*) <- clause* - -- Match_args: S |- a* `/ `{q*} a'* => s - -- Reduce_prems: S |- $subst_prem(s, pr)* ~>* eps - ;; TODO: need to try in order for ELSE to behave correctly + S |- CALL x a* ~> MATCH a* WITH clause* + -- if (x, p* `-> t `= clause*) <- E.FUN rule Step_exp/CVT-ctx: @@ -371,6 +397,9 @@ rule Step_exp/SUB-ctx3: S |- SUB e t_1 t_2 ~> SUB e t_1 t'_2 -- Step_typ: S |- t_2 ~> t'_2 +rule Step_exp/SUB-refl: + S |- SUB e t t ~> e + rule Step_exp/SUB-SUB: S |- SUB (SUB e' t'_1 t'_2) t_1 t_2 ~> SUB e' t'_1 t_2 @@ -386,19 +415,289 @@ rule Step_exp/SUB-LIST: S |- SUB (LIST e*) (ITER t_1 STAR) (ITER t_2 STAR) ~> LIST (SUB e t_1 t_2)* rule Step_exp/SUB-STR: - S |- SUB (STR ef*) (VAR x_1 a_1*) (VAR x_2 a_2*) ~> STR (at `= SUB e t_1 t_2)* - -- Expand_typ: S |- VAR x_1 a_1* => STRUCT tf_1* - -- Expand_typ: S |- VAR x_2 a_2* => STRUCT tf_2* - -- (if (at `: t_2 `- `{q_2*} pr_2*) = tf_2)* - -- (if (at `: t_1 `- `{q_1*} pr_1*) <- tf_1*)* - -- (if (at `= e) <- ef*)* + S |- SUB (STR (at `= e)*) t_1 t_2 ~> STR (at' `= SUB e t'_1 t'_2)* + -- if t_1 = MATCH x_1 eps WITH (INST `{} eps `= STRUCT tf_1*) + -- if t_2 = MATCH x_2 eps WITH (INST `{} eps `= STRUCT tf_2*) + -- (if (at' `: t'_1 `- `{q_1*} pr_1*) <- tf_1*)* + -- (if (at' `: t'_2 `- `{q_2*} pr_2*) = tf_2)* rule Step_exp/SUB-CASE: - S |- SUB (INJ op e) (VAR x_1 a_1*) (VAR x_2 a_2*) ~> INJ op (SUB e t_1 t_2) - -- Expand_typ: S |- VAR x_1 a_1* => VARIANT tc_1* - -- Expand_typ: S |- VAR x_2 a_2* => VARIANT tc_2* - -- if (op `: t_1 `- `{q_1*} pr_1*) <- tc_1* - -- if (op `: t_2 `- `{q_2*} pr_2*) <- tc_2* + S |- SUB (INJ op e) t_1 t_2 ~> INJ op (SUB e t'_1 t'_2) + -- if t_1 = MATCH x_1 eps WITH (INST `{} eps `= VARIANT tc_1*) + -- if t_2 = MATCH x_2 eps WITH (INST `{} eps `= VARIANT tc_2*) + -- if (op `: t'_1 `- `{q_1*} pr_1*) <- tc_1* + -- if (op `: t'_2 `- `{q_2*} pr_2*) <- tc_2* + + +rule Step_exp/MATCH-ctx1: + S |- MATCH a* WITH clause* ~> MATCH a*[[n] = a'_n] WITH clause* + -- Step_arg: S |- a*[n] ~> a'_n + +rule Step_exp/MATCH-ctx2: + S |- MATCH a* WITH clause* ~> MATCH a* WITH clause*[[n] = clause'_n] + -- Step_clause: S |- clause*[n] ~> clause'_n + +rule Step_exp/MATCH-match: + S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> + MATCH a''* WITH + (CLAUSE `{q'*} a'''* `= $subst_exp(s, e) `- $subst_prem(s, pr)*) + (CLAUSE `{} a''* `= (MATCH a* WITH clause*) `- eps) + -- Step_argsmatch: S |- a* / `{q*} a'* ~>_s a''* / `{q'*} a'''* + +rule Step_exp/MATCH-match-fail: + S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> + MATCH a''* WITH clause* + -- Step_argsmatch: S |- a* / `{q*} a'* ~>_s FAIL + +rule Step_exp/MATCH-guess: + S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> + MATCH a* WITH (CLAUSE `{} $subst_arg(s, a')* `= e `- pr*) clause* + -- Ok_subst: $storeenv(S) |- s : q* + ;; Note: non-computational rule + +rule Step_exp/MATCH-true: + S |- MATCH eps WITH (CLAUSE `{} eps `= e `- eps) clause* ~> e + +rule Step_exp/MATCH-false: + S |- MATCH eps WITH (CLAUSE `{} eps `= e `- (IF (BOOL false)) pr*) clause* ~> + MATCH eps WITH clause* + + +rule Step_expfield/ctx: + S |- a `= e ~> a `= e' + -- Step_exp: S |- e ~> e' + + +;; Paths + +rule Step_path/THE-ctx: + S |- THE p ~> THE p' + -- Step_path: S |- p ~> p' + +rule Step_path/IDX-ctx1: + S |- IDX p e ~> IDX p' e + -- Step_path: S |- p ~> p' + +rule Step_path/IDX-ctx2: + S |- IDX p e ~> IDX p e' + -- Step_exp: S |- e ~> e' + +rule Step_path/SLICE-ctx1: + S |- SLICE p e_1 e_2 ~> SLICE p' e_1 e_2 + -- Step_path: S |- p ~> p' + +rule Step_path/SLICE-ctx2: + S |- SLICE p e_1 e_2 ~> SLICE p e'_1 e_2 + -- Step_exp: S |- e_1 ~> e'_1 + +rule Step_path/SLICE-ctx3: + S |- SLICE p e_1 e_2 ~> SLICE p e_1 e'_2 + -- Step_exp: S |- e_2 ~> e'_2 + +rule Step_path/DOT-ctx: + S |- DOT p a ~> DOT p' a + -- Step_path: S |- p ~> p' + +rule Step_path/PROJ-ctx: + S |- PROJ p m ~> PROJ p' m + -- Step_path: S |- p ~> p' + + +;; Matches + +syntax argsmatch = arg* / `{quant*} arg* | FAIL +syntax expmatch = exp / exp | FAIL + +relation Step_argsmatch: S |- argsmatch ~>_subst argsmatch +relation Step_expmatch: S |- expmatch ~> expmatch* + + +rule Step_argsmatch/ctx1: + S |- a* / `{q*} a'* ~>_{} a*[[n] = a'_n] / `{q*} a'* + -- Step_arg: S |- a*[n] ~> a'_n + +rule Step_argsmatch/ctx2: + S |- a* / `{q*} a'* ~>_{} a* / `{q*} a'*[[n] = a''_n] + -- Step_arg: S |- a'*[n] ~> a''_n + +rule Step_argsmatch/cons: + S |- a_1 a* / `{q_1* q*} a'_1 a'* ~>_s a''_1* a* / `{q'_1* q*} a'''_1* $subst_arg(s, a')* + -- Step_argsmatch: S |- a_1 / `{q_1*} a'_1 ~>_s a''_1* / `{q'_1*} a'''_1* + +rule Step_argsmatch/eq: + S |- a / `{} a ~>_{} eps / `{} eps + +;; TODO: disjoint +;;rule Step_argsmatch/neq: +;; S |- (a / `{} a') ~>_{} FAIL +;; -- Disj_arg: S |- a =/= a' + +rule Step_argsmatch/TYP: + S |- TYP t / `{(TYP x)} TYP (VAR x) ~>_{TYP (x, t)} eps / `{} eps + +rule Step_argsmatch/EXP: + S |- EXP e / `{(EXP x `: t)} EXP (VAR x) ~>_{EXP (x, e)} eps / `{} eps + +rule Step_argsmatch/EXP-ctx: + S |- EXP e / `{q*} EXP e' ~>_{} (EXP e'')* / `{q*} (EXP e''')* + -- Step_expmatch: S |- e / e' ~> (e'' / e''')* + +rule Step_argsmatch/EXP-fail: + S |- EXP e / `{q*} EXP e' ~>_{} FAIL + -- Step_expmatch: S |- e / e' ~> FAIL + +rule Step_argsmatch/FUN: + S |- FUN y / `{(FUN x `: p* `-> t)} FUN x ~>_{FUN (x, y)} eps / `{} eps + +rule Step_argsmatch/GRAM: + S |- GRAM g / `{(GRAM x `: p* `-> t)} GRAM (VAR x) ~>_{GRAM (x, g)} eps / `{} eps + + +rule Step_expmatch/UN-PLUS: + S |- num / UN PLUS e ~> num / e + -- if ~ $isneg(num) + +rule Step_expmatch/UN-PLUS-fail: + S |- num / UN PLUS e ~> FAIL + -- otherwise + +rule Step_expmatch/UN-MINUS: + S |- num / UN MINUS e ~> $numun(MINUS, num) / e + -- if $isneg(num) + +rule Step_expmatch/UN-MINUS-fail: + S |- num / UN MINUS e ~> FAIL + -- otherwise + +rule Step_expmatch/CVT: + S |- num / CVT e nt_1 nt_2 ~> num' / e + -- if num' = $numcvt(nt_1, num) + +rule Step_expmatch/CVT-fail: + S |- num / CVT e nt_1 nt_2 ~> FAIL + -- otherwise + +rule Step_expmatch/TUP: + S |- TUP e* / TUP e'* ~> (e / e')* + +rule Step_expmatch/INJ: + S |- INJ op e / INJ op' e' ~> e / e' + -- if op = op' + +rule Step_expmatch/INJ-fail: + S |- INJ op e / INJ op' e' ~> FAIL + -- otherwise + +rule Step_expmatch/OPT: + S |- OPT e? / OPT e'? ~> (e / e')? + -- if |e?| = |e'?| + +rule Step_expmatch/OPT-fail: + S |- OPT e? / OPT e'? ~> FAIL + -- otherwise + +rule Step_expmatch/LIST: + S |- LIST e* / LIST e'* ~> (e / e')* + -- if |e*| = |e'*| + +rule Step_expmatch/LIST-fail: + S |- LIST e* / LIST e'* ~> FAIL + -- otherwise + +rule Step_expmatch/LIFT: + S |- LIST e? / LIFT e' ~> OPT e? / e' + +rule Step_expmatch/LIFT-fail: + S |- LIST e* / LIFT e' ~> FAIL + -- if |e*| > 1 + +rule Step_expmatch/CAT-left: + S |- LIST e_1* e_2* / CAT (LIST e'_1*) e'_2 ~> (LIST e_1* / LIST e'_1*) (LIST e_2* / e'_2) + -- if |e_1*| = |e'_1*| + +rule Step_expmatch/CAT-left-fail: + S |- LIST e_1* e_2* / CAT (LIST e'_1*) e'_2 ~> FAIL + -- otherwise + +rule Step_expmatch/CAT-right: + S |- LIST e_1* e_2* / CAT e'_1 (LIST e'_2*) ~> (LIST e_1* / e'_1) (LIST e_2* / LIST e'_2*) + -- if |e_2*| = |e'_2*| + +rule Step_expmatch/CAT-right-fail: + S |- LIST e_1* e_2* / CAT e'_1 (LIST e'_2*) ~> FAIL + -- otherwise + +rule Step_expmatch/STR: + S |- STR ef* / STR ef'* ~> (e / e')* + -- (if (l `= e') = ef')* + -- (if (l `= e) <- ef*)* + + +rule Step_expmatch/ITER-QUEST: + S |- OPT e? / ITER e' QUEST (x `<- e_x')* ~> + (e / $subst_exp({EXP (x, VAR x')*}, e'))? (OPT (VAR x'')? / e_x')* + -- if x''?* = $transposeq_(id, x'*?) + ;; TODO: x'*? fresh + ;; Note: inner match can only instantiate iteration variables + +rule Step_expmatch/ITER-PLUS: + S |- LIST e* / ITER e' PLUS (x `<- e_x')* ~> + LIST e* / ITER e' STAR (x `<- e_x')* + -- if |e*| >= 1 + +rule Step_expmatch/ITER-PLUS-fail: + S |- LIST eps / ITER e' PLUS (x `<- e_x')* ~> FAIL + +rule Step_expmatch/ITER-STAR: + S |- LIST e* / ITER e' STAR (x `<- e_x')* ~> + LIST e* / ITER e' (SUP y (NAT n)) (x `<- e_x')* + -- if |e*| = n + ;; TODO: y fresh + +rule Step_expmatch/ITER-SUP: + S |- LIST e^n / ITER e' (SUP y e_n') (x `<- e_x')* ~> + (NAT n / e_n') + (e / $subst_exp({EXP (y, NAT i) (x, VAR x')*}, e'))^(i + SUB e t_1 t'_1 / e' + -- Sub_typ: $storeenv(S) |- t_1 <: t'_1 + +;; TODO: disjointness + +rule Step_expmatch/SUB-TUP: + S |- TUP e^n / SUB e' (TUP (x_1 `: t'_1)^n) (TUP (x_2 `: t'_2)^n) ~> + TUP (SUB e' $subst_typ(s_1, t'_1) $subst_typ(s_2, t'_2))^n / e' + -- if s_1 = {EXP (x_1, SEL e i)^(i inst +relation Step_clause: S |- clause ~> clause + +rule Step_inst/INST-ctx: + S |- INST `{q*} a* `= t ~> INST `{q*} a*[[n] = a'_n] `= t + -- Step_arg: S |- a*[n] ~> a'_n + + +rule Step_clause/CLAUSE-ctx1: + S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a*[[n] = a'_n] `= e `- pr* + -- Step_arg: S |- a*[n] ~> a'_n + +rule Step_clause/CLAUSE-ctx2: + S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e' `- pr* + -- Step_exp: S |- e ~> e' + +rule Step_clause/CLAUSE-ctx3: + S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'* + -- Step_prems: S |- pr* ~> pr'* ;; Arguments @@ -406,13 +705,6 @@ rule Step_exp/SUB-CASE: relation Reduce_arg: S |- arg ~>* arg relation Step_arg: S |- arg ~> arg relation Eq_arg: S |- arg == arg -relation Match_args: S |- arg* `/ `{quant*} arg* => subst - - -rule Match_args: - S |- a* `/ `{q*} a' => s - -- Ok_subst: $storeenv(S) |- s : q* - -- if a* = $subst_arg(s, a')* rule Eq_arg: @@ -422,7 +714,7 @@ rule Eq_arg: -- if a'_1 = a'_2 -rule Reduce_arg/normal: +rule Reduce_arg/refl: S |- a ~>* a rule Reduce_arg/step: @@ -454,7 +746,7 @@ rule Eq_prems: -- if pr'_1* = pr'_2* -rule Reduce_prems/normal: +rule Reduce_prems/refl: S |- pr* ~>* pr* rule Reduce_prems/step: @@ -464,10 +756,17 @@ rule Reduce_prems/step: rule Step_prems/ctx: - S |- pr_1 pr* ~> pr_1'* pr* - -- Step_prems: S |- pr_1 ~> pr_1'* + S |- pr* ~> pr*[0 : n] pr'_n* pr*[n : |pr*| - n] + -- Step_prems: S |- pr*[n] ~> pr'_n* +rule Step_prems/RULE: + S |- RULE x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e)) + -- if (x, p* `-> t `= rul*) <- S.REL + -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)* + -- Ok_subst: $storeenv(S) |- s : q* + ;; Note: non-computational rule + rule Step_prems/IF-ctx: S |- IF e ~> IF e' -- Step_exp: S |- e ~> e' @@ -476,15 +775,24 @@ rule Step_prems/IF-true: S |- IF (BOOL true) ~> eps rule Step_prems/ELSE: - S |- ELSE ~> eps + S |- ELSE ~> IF (BOOL true) rule Step_prems/LET-ctx: S |- LET e_1 `= e_2 ~> LET e_1 `= e'_2 -- Step_exp: S |- e_2 ~> e'_2 rule Step_prems/LET: - S |- LET e_1 `= e_2 ~> eps - -- Eq_exp: S |- e_1 == e_2 + S |- LET e `= e ~> eps + +rule Step_prems/NOT-ctx: + S |- NOT pr ~> NOT pr' + -- Step_prems: S |- pr ~> pr' + +rule Step_prems/NOT-true: + S |- NOT (IF (BOOL true)) ~> IF (BOOL false) + +rule Step_prems/NOT-false: + S |- NOT (IF (BOOL false)) ~> IF (BOOL true) rule Step_prems/ITER-ctx1: S |- ITER pr it ep* ~> ITER pr' it ep* @@ -507,13 +815,10 @@ rule Step_prems/ITER-PLUS: -- if |e**[0]| >= 1 rule Step_prems/ITER-STAR: - S |- ITER pr STAR (x `<- LIST e*)* ~> ITER pr (SUP (NAT n)) (x `<- LIST e*)* + S |- ITER pr STAR (x `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `<- LIST e*)* -- if |e**[0]| = n - -rule Step_prems/ITER-SUP-eps: - S |- ITER pr (SUP eps e_n) (x `<- LIST e*)* ~> ITER pr (SUP y e_n) (x `<- LIST e*)* ;; TODO: y fresh rule Step_prems/ITER-SUP: - S |- ITER pr (SUP x_i (NAT n)) (x `<- LIST e^n)* ~> $subst_prem({EXP (x, e')* (x_i, NAT i)}, pr)^(i $subst_prem({EXP (x, e_x)* (y, NAT i)}, pr)^(i ALIAS (ITER t' it) + -- Expand_typ: E |- t ~~ ALIAS (ITER t' it) rule Catable_typ/STRUCT: E |- t CATABLE - -- Expand_typ: E |- t => STRUCT (atom `: t' `- `{q*} pr*)* + -- Expand_typ: E |- t ~~ STRUCT (atom `: t' `- `{q*} pr*)* -- (Catable_typ: E |- t' CATABLE)* @@ -43,18 +43,18 @@ rule Sub_typ/tup: rule Sub_typ/struct: E |- t_1 <: t_2 - -- Expand_typ: E |- t_1 => STRUCT tf_1* - -- Expand_typ: E |- t_2 => STRUCT tf_2* + -- Expand_typ: E |- t_1 ~~ STRUCT tf_1* + -- Expand_typ: E |- t_2 ~~ STRUCT tf_2* -- (if (a `: t_2a `- `{q*} pr*) = tf_2)* -- (if (a `: t_1a `- `{q*} pr*) <- tf_1*)* -- (Sub_typ: E |- t_1a <: t_2a)* rule Sub_typ/variant: E |- t_1 <: t_2 - -- Expand_typ: E |- t_1 => VARIANT tc_1* - -- Expand_typ: E |- t_2 => VARIANT tc_2* - -- (if (m `: t_1a `- `{q*} pr*) = tc_1)* - -- (if (m `: t_2a `- `{q*} pr*) <- tc_2*)* + -- Expand_typ: E |- t_1 ~~ VARIANT tc_1* + -- Expand_typ: E |- t_2 ~~ VARIANT tc_2* + -- (if (a `: t_1a `- `{q*} pr*) = tc_1)* + -- (if (a `: t_2a `- `{q*} pr*) <- tc_2*)* -- (Sub_typ: E |- t_1a <: t_2a)* rule Sub_typ/iter: @@ -124,6 +124,12 @@ rule Ok_typ/ITER: -- Ok_typ: E |- t : OK -- if it <- [QUEST STAR] +rule Ok_typ/MATCH: + E |- MATCH x a* WITH inst* : OK + -- if (x, p* `-> OK `= inst'*) <- E.TYP + -- Ok_args: E |- a* : p* => s + -- (Ok_inst: E |- inst : p* -> OK)* + relation Ok_deftyp: E |- deftyp : OK relation Ok_typfield: E |- typfield : OK @@ -174,7 +180,7 @@ rule Ok_iter/PLUS: E |- PLUS : STAR -| {} rule Ok_iter/SUP: - E |- SUP x? e : STAR -| {EXP (x, NAT)?} + E |- SUP x e : STAR -| {EXP (x, NAT)} -- Ok_exp: E |- e : NAT @@ -297,14 +303,14 @@ rule Ok_exp/LIFT: rule Ok_exp/INJ: E |- INJ op e : VAR x a* - -- Expand_typ: E |- VAR x a* => VARIANT tc* + -- Expand_typ: E |- VAR x a* ~~ VARIANT tc* -- if (op `: t `- `{q*} pr*) <- tc* -- Ok_exp: E |- e : t ;; Note: premises need not hold! rule Ok_exp/STR: E |- STR ef* : VAR x a* - -- Expand_typ: E |- VAR x a* => STRUCT tf* + -- Expand_typ: E |- VAR x a* ~~ STRUCT tf* -- if (at `: t `- `{q*} pr*)* = tf* -- if (at `= e)* = ef* -- (Ok_exp: E |- e : t)* @@ -374,6 +380,12 @@ rule Ok_exp/SUB: -- Ok_exp: E |- e : t_1 -- Sub_typ: E |- t_1 <: t_2 +rule Ok_exp/MATCH: + E |- MATCH a* WITH clause* : t + -- Ok_args: E |- a* : p* => s + -- Ok_params: E |- p* : OK + -- (Ok_clause: E ++ $paramenv(p*) |- clause : p* -> t)* + rule Ok_exp/conv: E |- e : t @@ -407,14 +419,14 @@ rule Ok_path/SLICE: rule Ok_path/DOT: E |- DOT p atom : t -> t' -- Ok_path: E |- p : t -> VAR x a* - -- Expand_typ: E |- VAR x a* => STRUCT tf* + -- Expand_typ: E |- VAR x a* ~~ STRUCT tf* -- if (atom `: t' `- `{q*} pr*) <- tf* ;; Note: premises cannot be used rule Ok_path/PROJ: E |- PROJ p mixop : t -> t' -- Ok_path: E |- p : t -> VAR x a* - -- Expand_typ: E |- VAR x a* => VARIANT tc* + -- Expand_typ: E |- VAR x a* ~~ VARIANT tc* -- if (mixop `: t' `- `{q*} pr*) <- tc* ;; Note: premises cannot be used @@ -489,6 +501,10 @@ rule Ok_prem/IF: rule Ok_prem/ELSE: E |- ELSE : OK +rule Ok_prem/NOT: + E |- NOT pr : OK + -- Ok_prem: E |- pr : OK + rule Ok_prem/LET: E |- LET e_1 `= e_2 : OK -- Ok_exp: E |- e_1 : t @@ -511,13 +527,13 @@ rule Ok_prems: relation Ok_param: E |- param : OK relation Ok_params: E |- param* : OK +rule Ok_param/TYP: + E |- TYP x : OK + rule Ok_param/EXP: E |- EXP x `: t : OK -- Ok_typ: E |- t : OK -rule Ok_param/TYP: - E |- TYP x : OK - rule Ok_param/FUN: E |- FUN x `: p* `-> t : OK -- Ok_params: E |- p* : OK @@ -540,14 +556,14 @@ rule Ok_params/cons: relation Ok_arg: E |- arg : param => subst relation Ok_args: E |- arg* : param* => subst -rule Ok_arg/EXP: - E |- EXP e : EXP x `: t => {EXP (x, e)} - -- Ok_exp: E |- e : t - rule Ok_arg/TYP: E |- TYP t : TYP x => {TYP (x, t)} -- Ok_typ: E |- t : OK +rule Ok_arg/EXP: + E |- EXP e : EXP x `: t => {EXP (x, e)} + -- Ok_exp: E |- e : t + rule Ok_arg/FUN: E |- FUN y : FUN x `: p* `-> t => {FUN (x, y)} -- if (y, (p'* `-> t' `= clause*)) <- E.FUN From 62cb2b8e03cc4aa7d1eda4aeeac937c5890730a5 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 10 Mar 2026 12:34:25 +0100 Subject: [PATCH 2/8] [spectec] Complete IL matching semantics --- spectec/doc/semantics/il/1-syntax.spectec | 2 +- spectec/doc/semantics/il/4-subst.spectec | 6 +- spectec/doc/semantics/il/5-reduction.spectec | 222 +++++++++++-------- spectec/doc/semantics/il/6-typing.spectec | 13 +- 4 files changed, 146 insertions(+), 97 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index fbe814ed9c..5eb525c8a1 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -138,7 +138,7 @@ syntax exp = | MATCH arg* WITH clause* ;; `match` arg* `with` clause* syntax expfield = atom `= exp -syntax exppull = id `<- exp +syntax exppull = id `: typ `<- exp syntax path = | ROOT ;; diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec index d218069793..07b2bd014c 100644 --- a/spectec/doc/semantics/il/4-subst.spectec +++ b/spectec/doc/semantics/il/4-subst.spectec @@ -101,7 +101,7 @@ def $subst_exp(s, ACC e_1 p) = ACC $subst_exp(s, e_1) $subst_path(s, p) 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) 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) def $subst_exp(s, CALL x a*) = CALL $subst_fun(s, x) $subst_arg(s, a)* -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 +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 def $subst_exp(s, CVT e nt_1 nt_2) = CVT $subst_exp(s, e) nt_1 nt_2 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) def $subst_exp(s, MATCH a* WITH clause*) = MATCH $subst_arg(s, a)* WITH $subst_clause(s, clause)* @@ -127,7 +127,7 @@ def $subst_sym(s, SEQ g*) = SEQ $subst_sym(s, g)* def $subst_sym(s, ALT g*) = ALT $subst_sym(s, g)* def $subst_sym(s, RANGE g_1 g_2) = RANGE $subst_sym(s, g_1) $subst_sym(s, g_2) def $subst_sym(s, ATTR e g) = ATTR $subst_exp(s, e) $subst_sym(s, g) -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 +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 ;; Definitions @@ -152,7 +152,7 @@ def $subst_prem(s, RULE x a* `: e) = RULE x $subst_arg(s, a)* `: $subst_exp(s, e def $subst_prem(s, IF e) = IF $subst_exp(s, e) def $subst_prem(s, ELSE) = ELSE def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture -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 +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 def $subst_inst(subst, inst) : inst diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 9992efc574..a58f17b4e8 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -58,12 +58,12 @@ rule Step_typ/MATCH-match: MATCH x a''* WITH (INST `{q'*} a'''* `= $subst_deftyp(s, dt)) (INST `{} a''* `= ALIAS (MATCH x a* WITH inst*)) - -- Step_argsmatch: S |- (a* / `{q*} a'*) ~>_s (a''* / `{q'*} a'''*) + -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{q'*} (a'' / a''')* rule Step_typ/MATCH-match-fail: S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~> MATCH x a''* WITH inst* - -- Step_argsmatch: S |- (a* / `{q*} a'*) ~>_s FAIL + -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{} FAIL rule Step_typ/TUP-ctx: @@ -87,7 +87,7 @@ rule Step_iter/SUP-ctx: rule Step_exppull/ctx: - S |- x `<- e ~> x `<- e' + S |- x `: t `<- e ~> x `: t `<- e' -- Step_exp: S |- e ~> e' @@ -351,20 +351,20 @@ rule Step_exp/ITER-ctx3: -- Step_exppull: S |- ep*[n] ~> ep'_n rule Step_exp/ITER-QUEST: - S |- ITER e QUEST (x `<- OPT e'?)* ~> OPT $subst_exp({EXP (x, e'')*}, e)? + S |- ITER e QUEST (x `: t `<- OPT e'?)* ~> OPT $subst_exp({EXP (x, e'')*}, e)? -- if e''*? = $transpose_(exp, e'?*) rule Step_exp/ITER-PLUS: - S |- ITER e PLUS (x `<- LIST e'*)* ~> ITER e STAR (x `<- LIST e'*)* + S |- ITER e PLUS (x `: t `<- LIST e'*)* ~> ITER e STAR (x `: t `<- LIST e'*)* -- if |e'**[0]| >= 1 rule Step_exp/ITER-STAR: - S |- ITER e STAR (x `<- LIST e'*)* ~> ITER e (SUP y (NAT n)) (x `<- LIST e'*)* + S |- ITER e STAR (x `: t `<- LIST e'*)* ~> ITER e (SUP y (NAT n)) (x `: t `<- LIST e'*)* -- if |e'**[0]| = n ;; TODO: y fresh rule Step_exp/ITER-SUP: - S |- ITER e (SUP y (NAT n)) (x `<- LIST e'^n)* ~> LIST $subst_exp({EXP (x, e'')* (y, NAT i)}, e)^(i LIST $subst_exp({EXP (x, e'')* (y, NAT i)}, e)^(i_s a''* / `{q'*} a'''* + -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{q'*} (a'' / a''')* rule Step_exp/MATCH-match-fail: S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> MATCH a''* WITH clause* - -- Step_argsmatch: S |- a* / `{q*} a'* ~>_s FAIL + -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{} FAIL rule Step_exp/MATCH-guess: S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> @@ -505,172 +505,218 @@ rule Step_path/PROJ-ctx: ;; Matches -syntax argsmatch = arg* / `{quant*} arg* | FAIL +syntax argmatch = arg / arg | FAIL syntax expmatch = exp / exp | FAIL -relation Step_argsmatch: S |- argsmatch ~>_subst argsmatch -relation Step_expmatch: S |- expmatch ~> expmatch* +relation Step_argmatch: S |- `{quant*} argmatch* ~>_subst `{quant*} argmatch* +relation Step_expmatch: S |- `{quant*} expmatch* ~>_subst `{quant*} expmatch* +relation Step_argmatch_plain: S |- argmatch* ~> argmatch* +relation Step_expmatch_plain: S |- expmatch* ~> expmatch* +def $subst_argmatch(subst, argmatch) : argmatch +def $subst_expmatch(subst, expmatch) : expmatch -rule Step_argsmatch/ctx1: - S |- a* / `{q*} a'* ~>_{} a*[[n] = a'_n] / `{q*} a'* - -- Step_arg: S |- a*[n] ~> a'_n +def $subst_argmatch(s, a / a') = $subst_arg(s, a) / $subst_arg(s, a') +def $subst_expmatch(s, e / e') = $subst_exp(s, e) / $subst_exp(s, e') + + +rule Step_argmatch/plain: + S |- `{q*} (a / a')* ~>_{} `{q*} (a'' / a''')* + -- Step_argmatch_plain: S |- (a / a')* ~> (a'' / a''')* + +rule Step_argmatch/seq: + S |- `{q_1* q* q_2*} am_1* am am_2* ~>_s + `{q_1* q'* $subst_quant(s, q_2)*} am_1* am'* $subst_argmatch(s, am_2)* + -- Step_argmatch: S |- `{q*} am ~>_s `{q'*} am'* + +rule Step_argmatch/seq-fail: + S |- `{q_1* q* q_2*} am_1* am am_2* ~>_s `{} FAIL + -- Step_argmatch: S |- `{q*} am ~>_s `{} FAIL + +rule Step_argmatch/TYP: + S |- `{TYP x} (TYP t / TYP (VAR x)) ~>_{TYP (x, t)} `{} eps + +rule Step_argmatch/EXP: + S |- `{EXP x `: t} (EXP e / EXP (VAR x)) ~>_{EXP (x, e)} `{} eps + +rule Step_argmatch/FUN: + S |- `{FUN x `: p* `-> t} (FUN y / FUN x) ~>_{FUN (x, y)} `{} eps -rule Step_argsmatch/ctx2: - S |- a* / `{q*} a'* ~>_{} a* / `{q*} a'*[[n] = a''_n] - -- Step_arg: S |- a'*[n] ~> a''_n +rule Step_argmatch/GRAM: + S |- `{GRAM x `: p* `-> t} (GRAM g / GRAM (VAR x)) ~>_{GRAM (x, g)} `{} eps -rule Step_argsmatch/cons: - S |- a_1 a* / `{q_1* q*} a'_1 a'* ~>_s a''_1* a* / `{q'_1* q*} a'''_1* $subst_arg(s, a')* - -- Step_argsmatch: S |- a_1 / `{q_1*} a'_1 ~>_s a''_1* / `{q'_1*} a'''_1* +rule Step_argmatch/EXP-exp: + S |- `{q*} (EXP e / EXP e') ~>_s `{q'*} (EXP e'' / EXP e''')* + -- Step_expmatch: S |- `{q*} (e / e') ~>_s `{q'*} (e'' / e''')* -rule Step_argsmatch/eq: - S |- a / `{} a ~>_{} eps / `{} eps +rule Step_argmatch/EXP-fail: + S |- `{q*} (EXP e / EXP e') ~>_s `{} FAIL + -- Step_expmatch: S |- `{q*} (e / e') ~>_s `{} FAIL + + +rule Step_argmatch_plain/ctx1: + S |- a / a' ~> a'' / a' + -- Step_arg: S |- a ~> a'' + +rule Step_argmatch_plain/ctx2: + S |- a / a' ~> a / a'' + -- Step_arg: S |- a' ~> a'' + +rule Step_argmatch_plain/eq: + S |- a / a ~> eps ;; TODO: disjoint -;;rule Step_argsmatch/neq: -;; S |- (a / `{} a') ~>_{} FAIL +;;rule Step_argmatch_plain/neq: +;; S |- a / a' ~> FAIL ;; -- Disj_arg: S |- a =/= a' -rule Step_argsmatch/TYP: - S |- TYP t / `{(TYP x)} TYP (VAR x) ~>_{TYP (x, t)} eps / `{} eps -rule Step_argsmatch/EXP: - S |- EXP e / `{(EXP x `: t)} EXP (VAR x) ~>_{EXP (x, e)} eps / `{} eps +rule Step_expmatch/plain: + S |- `{q*} (e / e')* ~>_{} `{q*} (e'' / e''')* + -- Step_expmatch_plain: S |- (e / e')* ~> (e'' / e''')* + +rule Step_expmatch/seq: + S |- `{q_1* q* q_2*} em_1* em em_2* ~>_s + `{q_1* q'* $subst_quant(s, q_2)*} em_1* em'* $subst_expmatch(s, em_2)* + -- Step_expmatch: S |- `{q*} em ~>_s `{q'*} em'* + +rule Step_expmatch/seq-fail: + S |- `{q_1* q* q_2*} em_1* em em_2* ~>_s `{} FAIL + -- Step_expmatch: S |- `{q*} em ~>_s `{} FAIL + +rule Step_expmatch/ITER-QUEST: + S |- `{q*} (OPT e? / ITER e' QUEST (x `: t `<- e_p)*) ~>_{} + `{$concat_(quant, (EXP x' `: t)*?) q*} + (e / $subst_exp({EXP (x, VAR x')*}, e'))? + (OPT (VAR x'')? / e_p)* + -- if x''?* = $transposeq_(id, x'*?) + ;; TODO: x'*? fresh + ;; Note: inner match can only instantiate iteration variables -rule Step_argsmatch/EXP-ctx: - S |- EXP e / `{q*} EXP e' ~>_{} (EXP e'')* / `{q*} (EXP e''')* - -- Step_expmatch: S |- e / e' ~> (e'' / e''')* +rule Step_expmatch/ITER-SUP: + S |- `{q*} (LIST e^n / ITER e' (SUP y e_n) (x `: t `<- e_p)*) ~>_{} + `{$concat_(quant, (EXP x' `: t)*^n) q*} + (e / $subst_exp({EXP (y, NAT i) (x, VAR x')*}, e'))^(i_{} FAIL - -- Step_expmatch: S |- e / e' ~> FAIL -rule Step_argsmatch/FUN: - S |- FUN y / `{(FUN x `: p* `-> t)} FUN x ~>_{FUN (x, y)} eps / `{} eps +rule Step_expmatch_plain/ctx1: + S |- e / e' ~> e'' / e' + -- Step_exp: S |- e ~> e'' -rule Step_argsmatch/GRAM: - S |- GRAM g / `{(GRAM x `: p* `-> t)} GRAM (VAR x) ~>_{GRAM (x, g)} eps / `{} eps +rule Step_expmatch_plain/ctx2: + S |- e / e' ~> e' / e'' + -- Step_exp: S |- e' ~> e'' +rule Step_expmatch_plain/eq: + S |- e / e ~> eps -rule Step_expmatch/UN-PLUS: +rule Step_expmatch_plain/UN-PLUS: S |- num / UN PLUS e ~> num / e -- if ~ $isneg(num) -rule Step_expmatch/UN-PLUS-fail: +rule Step_expmatch_plain/UN-PLUS-fail: S |- num / UN PLUS e ~> FAIL -- otherwise -rule Step_expmatch/UN-MINUS: +rule Step_expmatch_plain/UN-MINUS: S |- num / UN MINUS e ~> $numun(MINUS, num) / e -- if $isneg(num) -rule Step_expmatch/UN-MINUS-fail: +rule Step_expmatch_plain/UN-MINUS-fail: S |- num / UN MINUS e ~> FAIL -- otherwise -rule Step_expmatch/CVT: +rule Step_expmatch_plain/CVT: S |- num / CVT e nt_1 nt_2 ~> num' / e -- if num' = $numcvt(nt_1, num) -rule Step_expmatch/CVT-fail: +rule Step_expmatch_plain/CVT-fail: S |- num / CVT e nt_1 nt_2 ~> FAIL -- otherwise -rule Step_expmatch/TUP: +rule Step_expmatch_plain/TUP: S |- TUP e* / TUP e'* ~> (e / e')* -rule Step_expmatch/INJ: +rule Step_expmatch_plain/INJ: S |- INJ op e / INJ op' e' ~> e / e' -- if op = op' -rule Step_expmatch/INJ-fail: +rule Step_expmatch_plain/INJ-fail: S |- INJ op e / INJ op' e' ~> FAIL -- otherwise -rule Step_expmatch/OPT: +rule Step_expmatch_plain/OPT: S |- OPT e? / OPT e'? ~> (e / e')? -- if |e?| = |e'?| -rule Step_expmatch/OPT-fail: +rule Step_expmatch_plain/OPT-fail: S |- OPT e? / OPT e'? ~> FAIL -- otherwise -rule Step_expmatch/LIST: +rule Step_expmatch_plain/LIST: S |- LIST e* / LIST e'* ~> (e / e')* -- if |e*| = |e'*| -rule Step_expmatch/LIST-fail: +rule Step_expmatch_plain/LIST-fail: S |- LIST e* / LIST e'* ~> FAIL -- otherwise -rule Step_expmatch/LIFT: +rule Step_expmatch_plain/LIFT: S |- LIST e? / LIFT e' ~> OPT e? / e' -rule Step_expmatch/LIFT-fail: +rule Step_expmatch_plain/LIFT-fail: S |- LIST e* / LIFT e' ~> FAIL -- if |e*| > 1 -rule Step_expmatch/CAT-left: +rule Step_expmatch_plain/CAT-left: S |- LIST e_1* e_2* / CAT (LIST e'_1*) e'_2 ~> (LIST e_1* / LIST e'_1*) (LIST e_2* / e'_2) -- if |e_1*| = |e'_1*| -rule Step_expmatch/CAT-left-fail: +rule Step_expmatch_plain/CAT-left-fail: S |- LIST e_1* e_2* / CAT (LIST e'_1*) e'_2 ~> FAIL -- otherwise -rule Step_expmatch/CAT-right: +rule Step_expmatch_plain/CAT-right: S |- LIST e_1* e_2* / CAT e'_1 (LIST e'_2*) ~> (LIST e_1* / e'_1) (LIST e_2* / LIST e'_2*) -- if |e_2*| = |e'_2*| -rule Step_expmatch/CAT-right-fail: +rule Step_expmatch_plain/CAT-right-fail: S |- LIST e_1* e_2* / CAT e'_1 (LIST e'_2*) ~> FAIL -- otherwise -rule Step_expmatch/STR: +rule Step_expmatch_plain/STR: S |- STR ef* / STR ef'* ~> (e / e')* -- (if (l `= e') = ef')* -- (if (l `= e) <- ef*)* -rule Step_expmatch/ITER-QUEST: - S |- OPT e? / ITER e' QUEST (x `<- e_x')* ~> - (e / $subst_exp({EXP (x, VAR x')*}, e'))? (OPT (VAR x'')? / e_x')* - -- if x''?* = $transposeq_(id, x'*?) - ;; TODO: x'*? fresh - ;; Note: inner match can only instantiate iteration variables - -rule Step_expmatch/ITER-PLUS: - S |- LIST e* / ITER e' PLUS (x `<- e_x')* ~> - LIST e* / ITER e' STAR (x `<- e_x')* +rule Step_expmatch_plain/ITER-PLUS: + S |- LIST e* / ITER e' PLUS (x `: t `<- e_p)* ~> + LIST e* / ITER e' STAR (x `: t `<- e_p)* -- if |e*| >= 1 -rule Step_expmatch/ITER-PLUS-fail: - S |- LIST eps / ITER e' PLUS (x `<- e_x')* ~> FAIL +rule Step_expmatch_plain/ITER-PLUS-fail: + S |- LIST eps / ITER e' PLUS (x `: t `<- e_p)* ~> FAIL -rule Step_expmatch/ITER-STAR: - S |- LIST e* / ITER e' STAR (x `<- e_x')* ~> - LIST e* / ITER e' (SUP y (NAT n)) (x `<- e_x')* +rule Step_expmatch_plain/ITER-STAR: + S |- LIST e* / ITER e' STAR (x `: t `<- e_p)* ~> + LIST e* / ITER e' (SUP y (NAT n)) (x `: t `<- e_p)* -- if |e*| = n ;; TODO: y fresh -rule Step_expmatch/ITER-SUP: - S |- LIST e^n / ITER e' (SUP y e_n') (x `<- e_x')* ~> - (NAT n / e_n') - (e / $subst_exp({EXP (y, NAT i) (x, VAR x')*}, e'))^(i SUB e t_1 t'_1 / e' -- Sub_typ: $storeenv(S) |- t_1 <: t'_1 ;; TODO: disjointness -rule Step_expmatch/SUB-TUP: +rule Step_expmatch_plain/SUB-TUP: S |- TUP e^n / SUB e' (TUP (x_1 `: t'_1)^n) (TUP (x_2 `: t'_2)^n) ~> TUP (SUB e' $subst_typ(s_1, t'_1) $subst_typ(s_2, t'_2))^n / e' -- if s_1 = {EXP (x_1, SEL e i)^(i ep'_n rule Step_prems/ITER-QUEST: - S |- ITER pr QUEST (x `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)? + S |- ITER pr QUEST (x `: t `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)? -- if e'*? = $transpose_(exp, e?*) rule Step_prems/ITER-PLUS: - S |- ITER pr PLUS (x `<- LIST e*)* ~> ITER pr STAR (x `<- LIST e*)* + S |- ITER pr PLUS (x `: t `<- LIST e*)* ~> ITER pr STAR (x `: t `<- LIST e*)* -- if |e**[0]| >= 1 rule Step_prems/ITER-STAR: - S |- ITER pr STAR (x `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `<- LIST e*)* + S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)* -- if |e**[0]| = n ;; TODO: y fresh rule Step_prems/ITER-SUP: - S |- ITER pr (SUP y (NAT n)) (x `<- LIST e^n)* ~> $subst_prem({EXP (x, e_x)* (y, NAT i)}, pr)^(i $subst_prem({EXP (x, e_x)* (y, NAT i)}, pr)^(i Date: Wed, 11 Mar 2026 07:51:36 +0100 Subject: [PATCH 3/8] Tweak --- spectec/doc/semantics/il/5-reduction.spectec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index a58f17b4e8..cdc76a377d 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -13,7 +13,7 @@ rule Expand_typ/plain: rule Expand_typ/def: S |- t ~~ dt - -- Reduce_typ: S |- t ~>* MATCH x eps WITH (INST `{} eps `= dt) inst* + -- Reduce_typ: S |- t ~>* MATCH x WITH (INST `{} `= dt) inst* rule Eq_typ: @@ -42,7 +42,7 @@ rule Step_typ/VAR-apply: -- if (x, p* `-> OK `= inst*) <- E.TYP -rule Step_typ/MATCH-ctx: +rule Step_typ/MATCH-ctx1: S |- MATCH x a* WITH inst* ~> MATCH x a*[[n] = a'_n] WITH inst* -- Step_arg: S |- a*[n] ~> a'_n @@ -416,15 +416,15 @@ rule Step_exp/SUB-LIST: rule Step_exp/SUB-STR: S |- SUB (STR (at `= e)*) t_1 t_2 ~> STR (at' `= SUB e t'_1 t'_2)* - -- if t_1 = MATCH x_1 eps WITH (INST `{} eps `= STRUCT tf_1*) - -- if t_2 = MATCH x_2 eps WITH (INST `{} eps `= STRUCT tf_2*) + -- if t_1 = MATCH x_1 WITH (INST `{} `= STRUCT tf_1*) + -- if t_2 = MATCH x_2 WITH (INST `{} `= STRUCT tf_2*) -- (if (at' `: t'_1 `- `{q_1*} pr_1*) <- tf_1*)* -- (if (at' `: t'_2 `- `{q_2*} pr_2*) = tf_2)* rule Step_exp/SUB-CASE: S |- SUB (INJ op e) t_1 t_2 ~> INJ op (SUB e t'_1 t'_2) - -- if t_1 = MATCH x_1 eps WITH (INST `{} eps `= VARIANT tc_1*) - -- if t_2 = MATCH x_2 eps WITH (INST `{} eps `= VARIANT tc_2*) + -- if t_1 = MATCH x_1 WITH (INST `{} `= VARIANT tc_1*) + -- if t_2 = MATCH x_2 WITH (INST `{} `= VARIANT tc_2*) -- if (op `: t'_1 `- `{q_1*} pr_1*) <- tc_1* -- if (op `: t'_2 `- `{q_2*} pr_2*) <- tc_2* From f25ed8ac44425251bbd6cf516361c7cc07a11504 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 11 Mar 2026 07:58:13 +0100 Subject: [PATCH 4/8] Fix exppull typing; rename RULE prem to REL prem --- spectec/doc/semantics/il/1-syntax.spectec | 2 +- spectec/doc/semantics/il/4-subst.spectec | 2 +- spectec/doc/semantics/il/5-reduction.spectec | 2 +- spectec/doc/semantics/il/6-typing.spectec | 10 +++++----- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index 5eb525c8a1..db4633ab72 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -179,7 +179,7 @@ syntax param = syntax quant = param syntax prem = - | RULE id arg* `: exp + | REL id arg* `: exp | IF exp | ELSE | NOT prem diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec index 07b2bd014c..2b7f4f4176 100644 --- a/spectec/doc/semantics/il/4-subst.spectec +++ b/spectec/doc/semantics/il/4-subst.spectec @@ -148,7 +148,7 @@ def $subst_quant(subst, quant) : quant def $subst_quant(s, q) = $subst_param(s, q) def $subst_prem(subst, prem) : prem -def $subst_prem(s, RULE x a* `: e) = RULE x $subst_arg(s, a)* `: $subst_exp(s, e) +def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e) def $subst_prem(s, IF e) = IF $subst_exp(s, e) def $subst_prem(s, ELSE) = ELSE def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index cdc76a377d..ac1e578857 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -807,7 +807,7 @@ rule Step_prems/ctx: rule Step_prems/RULE: - S |- RULE x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e)) + S |- REL x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e)) -- if (x, p* `-> t `= rul*) <- S.REL -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)* -- Ok_subst: $storeenv(S) |- s : q* diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec index 90647f7c66..15ad528904 100644 --- a/spectec/doc/semantics/il/6-typing.spectec +++ b/spectec/doc/semantics/il/6-typing.spectec @@ -366,7 +366,7 @@ rule Ok_exp/CALL: rule Ok_exp/ITER: E |- ITER e it (x `: t' `<- e')* : ITER t it' -- Ok_iter: E |- it : it' -| E' - -- Ok_typ: E |- t' : OK + -- (Ok_typ: E |- t' : OK)* -- (Ok_exp: E |- e' : ITER t' it')* -- Ok_exp: E ++ {EXP (x, t')*} ++ E' |- e : t -- Ok_typ: E |- t : OK @@ -468,7 +468,7 @@ rule Ok_sym/RANGE: rule Ok_sym/ITER: E |- ITER g it (x `: t' `<- e)* : ITER t it' -- Ok_iter: E |- it : it' -| E' - -- Ok_typ: E |- t' : OK + -- (Ok_typ: E |- t' : OK)* -- (Ok_exp: E |- e : ITER t' it')* -- Ok_sym: E ++ {EXP (x, t')*} ++ E' |- g : t -- Ok_typ: E |- t : OK @@ -490,8 +490,8 @@ rule Ok_sym/conv: relation Ok_prem: E |- prem : OK relation Ok_prems: E |- prem* : OK -rule Ok_prem/RULE: - E |- RULE x a* `: e : OK +rule Ok_prem/REL: + E |- REL x a* `: e : OK -- if (x, (p* `-> t `= rul*)) <- E.REL -- Ok_args: E |- a* : p* => s -- Ok_exp: E |- e : $subst_typ(s, t) @@ -515,7 +515,7 @@ rule Ok_prem/LET: rule Ok_prem/ITER: E |- ITER pr it (x `: t `<- e)* : OK -- Ok_iter: E |- it : it' -| E' - -- Ok_typ: E |- t : OK + -- (Ok_typ: E |- t : OK)* -- (Ok_exp: E |- e : ITER t it')* -- Ok_prem: E ++ {EXP (x, t)*} ++ E' |- pr : OK From f56f1e20665e49d3be03c6fb409c280dbb865f99 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 11 Mar 2026 08:59:26 +0100 Subject: [PATCH 5/8] Typos --- spectec/doc/semantics/il/5-reduction.spectec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index ac1e578857..8dd5672be6 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -806,7 +806,7 @@ rule Step_prems/ctx: -- Step_prems: S |- pr*[n] ~> pr'_n* -rule Step_prems/RULE: +rule Step_prems/REL: S |- REL x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e)) -- if (x, p* `-> t `= rul*) <- S.REL -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)* @@ -866,5 +866,5 @@ rule Step_prems/ITER-STAR: ;; TODO: y fresh rule Step_prems/ITER-SUP: - S |- ITER pr (SUP y (NAT n)) (x `: t `<- LIST e^n)* ~> $subst_prem({EXP (x, e_x)* (y, NAT i)}, pr)^(i $subst_prem({EXP (x, e')* (y, NAT i)}, pr)^(i Date: Wed, 11 Mar 2026 14:38:24 +0100 Subject: [PATCH 6/8] Missing context rule for exppull --- spectec/doc/semantics/il/5-reduction.spectec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 8dd5672be6..3c434594b4 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -86,7 +86,11 @@ rule Step_iter/SUP-ctx: -- Step_exp: S |- e ~> e' -rule Step_exppull/ctx: +rule Step_exppull/ctx1: + S |- x `: t `<- e ~> x `: t' `<- e + -- Step_typ: S |- t ~> t' + +rule Step_exppull/ctx2: S |- x `: t `<- e ~> x `: t `<- e' -- Step_exp: S |- e ~> e' From 36ee1ccab23926879b54a60bf84a831ab1c11579 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 12 Mar 2026 09:08:30 +0100 Subject: [PATCH 7/8] Fix typo --- spectec/doc/semantics/il/5-reduction.spectec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 3c434594b4..29b9c788c5 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -62,7 +62,7 @@ rule Step_typ/MATCH-match: rule Step_typ/MATCH-match-fail: S |- MATCH x a* WITH (INST `{q*} a'* `= dt) inst* ~> - MATCH x a''* WITH inst* + MATCH x a* WITH inst* -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{} FAIL From eeb47af6a67257776edb7d2852f71dac715d2e5a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 12 Mar 2026 11:21:23 +0100 Subject: [PATCH 8/8] Typos --- spectec/doc/semantics/il/5-reduction.spectec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 29b9c788c5..6925f481a4 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -39,7 +39,7 @@ rule Step_typ/VAR-ctx: rule Step_typ/VAR-apply: S |- VAR x a* ~> MATCH x a* WITH inst* - -- if (x, p* `-> OK `= inst*) <- E.TYP + -- if (x, p* `-> OK `= inst*) <- S.TYP rule Step_typ/MATCH-ctx1: @@ -378,7 +378,7 @@ rule Step_exp/CALL-ctx: rule Step_exp/CALL-apply: S |- CALL x a* ~> MATCH a* WITH clause* - -- if (x, p* `-> t `= clause*) <- E.FUN + -- if (x, p* `-> t `= clause*) <- S.FUN rule Step_exp/CVT-ctx: