From 9487d422076cbe3ad018c5bed9945d25591f05f7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 10 Mar 2026 14:34:23 +0100 Subject: [PATCH 01/13] [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 02/13] [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 03/13] 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 04/13] 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 05/13] 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 06/13] 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 78443568300431e53809d3aaaecae89cb428d20d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 11 Mar 2026 14:37:43 +0100 Subject: [PATCH 07/13] [spectec] Binding semantics for IL LET --- spectec/doc/semantics/il/1-syntax.spectec | 5 +- spectec/doc/semantics/il/4-subst.spectec | 8 +- spectec/doc/semantics/il/5-reduction.spectec | 82 +++++++++++++------- spectec/doc/semantics/il/6-typing.spectec | 54 +++++++------ 4 files changed, 94 insertions(+), 55 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index db4633ab72..13e0b30785 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -139,6 +139,7 @@ syntax exp = syntax expfield = atom `= exp syntax exppull = id `: typ `<- exp +syntax exppush = exp `-> id `: typ syntax path = | ROOT ;; @@ -183,8 +184,8 @@ syntax prem = | IF exp | ELSE | NOT prem - | LET exp `= exp ;; TODO: variables/quantifiers? - | ITER prem iter exppull* + | LET `{quant*} exp `= exp + | ITER prem iter exppull* exppush* syntax dec = | TYP id param* `= inst* diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec index 2b7f4f4176..ac134e2aa9 100644 --- a/spectec/doc/semantics/il/4-subst.spectec +++ b/spectec/doc/semantics/il/4-subst.spectec @@ -151,8 +151,12 @@ def $subst_prem(subst, prem) : prem 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 -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_prem(s, LET `{q*} e_1 `= e_2) = LET `{$subst_param(s, q)*} $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture +def $subst_prem(s, ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)*) = ;; TODO: avoid capture + ITER $subst_prem(s, pr) $subst_iter(s, it) (x_1 `: $subst_typ(s, t_1) `<- $subst_exp(s, e_1))* ($subst_exp(s, e_2) `-> x_2 `: $subst_typ(s, t_2))* + +def $subst_exppush(subst, exppush) : exppush +def $subst_exppush(s, e `-> x `: t) = $subst_exp(s, e) `-> x `: $subst_typ(s, t) 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 3c434594b4..cc4eb68c80 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -80,6 +80,7 @@ rule Step_typ/ITER-ctx: relation Step_iter: S |- iter ~> iter relation Step_exppull: S |- exppull ~> exppull +relation Step_exppush: S |- exppush ~> exppush rule Step_iter/SUP-ctx: S |- SUP x e ~> SUP x e' @@ -94,6 +95,14 @@ rule Step_exppull/ctx2: S |- x `: t `<- e ~> x `: t `<- e' -- Step_exp: S |- e ~> e' +rule Step_exppush/ctx1: + S |- e `-> x `: t ~> e' `-> x `: t + -- Step_exp: S |- e ~> e' + +rule Step_exppush/ctx2: + S |- e `-> x `: t ~> e `-> x `: t' + -- Step_typ: S |- t ~> t' + ;; Expressions @@ -747,7 +756,7 @@ rule Step_clause/CLAUSE-ctx2: rule Step_clause/CLAUSE-ctx3: S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'* - -- Step_prems: S |- pr* ~> pr'* + -- Step_prems: S |- pr* ~>_s pr'* ;; Arguments @@ -785,7 +794,7 @@ rule Step_arg/TYP-ctx: ;; Premises relation Reduce_prems: S |- prem* ~>* prem* -relation Step_prems: S |- prem* ~> prem* +relation Step_prems: S |- prem* ~>_subst prem* relation Eq_prems: S |- prem* == prem* @@ -801,74 +810,91 @@ rule Reduce_prems/refl: rule Reduce_prems/step: S |- pr* ~>* pr''* - -- Step_prems: S |- pr* ~> pr'* + -- Step_prems: S |- pr* ~>_s pr'* -- Reduce_prems: S |- pr'* ~>* pr''* -rule Step_prems/ctx: - S |- pr* ~> pr*[0 : n] pr'_n* pr*[n : |pr*| - n] - -- Step_prems: S |- pr*[n] ~> pr'_n* +rule Step_prems/seq: + S |- pr_1* pr pr_2* ~>_s pr_1* pr'* $subst_prem(s, pr_2)* + -- Step_prems: S |- pr ~>_s pr'* rule Step_prems/REL: - S |- REL 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* ;; Note: non-computational rule rule Step_prems/IF-ctx: - S |- IF e ~> IF e' + S |- IF e ~>_{} IF e' -- Step_exp: S |- e ~> e' rule Step_prems/IF-true: - S |- IF (BOOL true) ~> eps + S |- IF (BOOL true) ~>_{} eps rule Step_prems/ELSE: - S |- ELSE ~> IF (BOOL true) + S |- ELSE ~>_{} IF (BOOL true) rule Step_prems/LET-ctx: - S |- LET e_1 `= e_2 ~> LET e_1 `= e'_2 + S |- LET `{q*} e_1 `= e_2 ~>_{} LET `{q*} e_1 `= e'_2 -- Step_exp: S |- e_2 ~> e'_2 rule Step_prems/LET: - S |- LET e `= e ~> eps + S |- LET `{(EXP x `: t)*} e_1 `= e_2 ~>_{EXP (x, e)*} eps + -- (if e = MATCH (EXP e_2) WITH (CLAUSE `{(EXP x `: t)*} (EXP e_1) `= (VAR x) `- eps))* rule Step_prems/NOT-ctx: - S |- NOT pr ~> NOT pr' - -- Step_prems: S |- pr ~> pr' + S |- NOT pr ~>_{} NOT pr' + -- Step_prems: S |- pr ~>_s pr' rule Step_prems/NOT-true: - S |- NOT (IF (BOOL true)) ~> IF (BOOL false) + S |- NOT (IF (BOOL true)) ~>_{} IF (BOOL false) rule Step_prems/NOT-false: - S |- NOT (IF (BOOL false)) ~> IF (BOOL true) + S |- NOT (IF (BOOL false)) ~>_{} IF (BOOL true) + +var ep : exppull +var eq : exppush rule Step_prems/ITER-ctx1: - S |- ITER pr it ep* ~> ITER pr' it ep* - -- Step_prems: S |- pr ~> pr' + S |- ITER pr it ep* eq* ~>_{} ITER pr' it ep* $subst_exppush(s, eq)* + -- Step_prems: S |- pr ~>_s pr' rule Step_prems/ITER-ctx2: - S |- ITER pr it ep* ~> ITER pr it' ep* + S |- ITER pr it ep* eq* ~>_{} ITER pr it' ep* eq* -- Step_iter: S |- it ~> it' rule Step_prems/ITER-ctx3: - S |- ITER pr it ep* ~> ITER pr it ep*[[n] = ep'_n] + S |- ITER pr it ep* eq* ~>_{} ITER pr it ep*[[n] = ep'_n] eq* -- Step_exppull: S |- ep*[n] ~> ep'_n +rule Step_prems/ITER-ctx4: + S |- ITER pr it ep* eq* ~>_{} ITER pr it ep* eq*[[n] = eq'_n] + -- Step_exppush: S |- eq*[n] ~> eq'_n + rule Step_prems/ITER-QUEST: - S |- ITER pr QUEST (x `: t `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)? - -- if e'*? = $transpose_(exp, e?*) + S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_{EXP (x_2, OPT e''_2?)*} + $subst_prem({EXP (x_1, e'_1)*}, pr)? + -- if e'_1*? = $transpose_(exp, e_1?*) + -- if e'_2*? = $transpose_(exp, e''_2?*) + -- (if |e_1?| = |e''_2?|)* + -- (if e'_2 = e_2)*? rule Step_prems/ITER-PLUS: - S |- ITER pr PLUS (x `: t `<- LIST e*)* ~> ITER pr STAR (x `: t `<- LIST e*)* - -- if |e**[0]| >= 1 + S |- ITER pr PLUS (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{} + ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* + -- if |e_1**[0]| >= 1 rule Step_prems/ITER-STAR: - S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)* - -- if |e**[0]| = n + S |- ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{} + ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* + -- if |e_1**[0]| = n ;; 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')* (y, NAT i)}, pr)^(i_{EXP (x_2, LIST e''_2^n)*} + $subst_prem({EXP (x_1, e'_1)* (y, NAT i)}, pr)^(i t `= rul*)) <- E.REL -- Ok_args: E |- a* : p* => s -- Ok_exp: E |- e : $subst_typ(s, t) rule Ok_prem/IF: - E |- IF e : OK + E |- IF e : OK -| {} -- Ok_exp: E |- e : BOOL rule Ok_prem/ELSE: - E |- ELSE : OK + E |- ELSE : OK -| {} rule Ok_prem/NOT: - E |- NOT pr : OK - -- Ok_prem: E |- pr : OK + 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 + E |- LET `{q*} e_1 `= e_2 : OK -| $paramenv(q*) + -- Ok_exp: E ++ $paramenv(q*) |- e_1 : t -- Ok_exp: E |- e_2 : t rule Ok_prem/ITER: - E |- ITER pr it (x `: t `<- e)* : OK + E |- ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)* : OK -| {EXP (x_2, t_2)*} -- Ok_iter: E |- it : it' -| E' - -- (Ok_typ: E |- t : OK)* - -- (Ok_exp: E |- e : ITER t it')* - -- Ok_prem: E ++ {EXP (x, t)*} ++ E' |- pr : OK - - -rule Ok_prems: - E |- prem* : OK - -- (Ok_prem: E |- prem : OK)* + -- (Ok_typ: E |- t_1 : OK)* + -- (Ok_exp: E |- e_1 : ITER t_1 it')* + -- Ok_prem: E ++ {EXP (x_1, t_1)*} ++ E' |- pr : OK -| E' + -- (Ok_typ: E |- t_2 : OK)* + -- (Eq_typ: E |- t_2 == ITER t'_2 it')* + -- (Ok_exp: E ++ E' |- e_2 : t'_2)* ;; Parameters and Arguments @@ -644,7 +652,7 @@ rule Ok_rule: E |- RULE `{q*} e `- pr* : t -- Ok_params: E |- q* : OK -- Ok_exp: E ++ $paramenv(q*) |- e : t - -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK + -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E' relation Ok_clause: E |- clause : param* -> typ @@ -653,7 +661,7 @@ rule Ok_clause: -- Ok_params: E |- q* : OK -- Ok_args: E ++ $paramenv(q*) |- a* : p* => s -- Ok_exp: E ++ $paramenv(q*) |- e : t - -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK + -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E' relation Ok_prod: E |- prod : typ @@ -662,7 +670,7 @@ rule Ok_prod: -- Ok_params: E |- q* : OK -- Ok_sym: E ++ $paramenv(q*) |- g : t' -- Ok_exp: E ++ $paramenv(q*) |- e : t - -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK + -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E' ;; Scripts From 3797f61664fe3661d3c58fd97533c25427eb68c3 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 11 Mar 2026 15:06:27 +0100 Subject: [PATCH 08/13] Scope let premises over clause/rule r.h.s.'s --- spectec/doc/semantics/il/5-reduction.spectec | 2 +- spectec/doc/semantics/il/6-typing.spectec | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index cc4eb68c80..0b5be00233 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -755,7 +755,7 @@ rule Step_clause/CLAUSE-ctx2: -- Step_exp: S |- e ~> e' rule Step_clause/CLAUSE-ctx3: - S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'* + S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= $subst_exp(s, e) `- pr'* -- Step_prems: S |- pr* ~>_s pr'* diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec index 65c156ccb0..dc682c34ec 100644 --- a/spectec/doc/semantics/il/6-typing.spectec +++ b/spectec/doc/semantics/il/6-typing.spectec @@ -660,8 +660,8 @@ rule Ok_clause: E |- CLAUSE `{q*} a* `= e `- pr* : p* -> t -- Ok_params: E |- q* : OK -- Ok_args: E ++ $paramenv(q*) |- a* : p* => s - -- Ok_exp: E ++ $paramenv(q*) |- e : t -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E' + -- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t relation Ok_prod: E |- prod : typ @@ -669,8 +669,8 @@ rule Ok_prod: E |- PROD `{q*} g `=> e `- pr* : t -- Ok_params: E |- q* : OK -- Ok_sym: E ++ $paramenv(q*) |- g : t' - -- Ok_exp: E ++ $paramenv(q*) |- e : t -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E' + -- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t ;; Scripts From 36ee1ccab23926879b54a60bf84a831ab1c11579 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 12 Mar 2026 09:08:30 +0100 Subject: [PATCH 09/13] 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 10/13] 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: From 9c77173b2f9678c7011f57fefff2e64c4acdacb4 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 24 Mar 2026 15:37:02 +0100 Subject: [PATCH 11/13] TODO --- spectec/doc/semantics/il/5-reduction.spectec | 1 + 1 file changed, 1 insertion(+) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 59785abad7..43b1b34e73 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -847,6 +847,7 @@ rule Step_prems/LET-ctx: rule Step_prems/LET: S |- LET `{(EXP x `: t)*} e_1 `= e_2 ~>_{EXP (x, e)*} eps -- (if e = MATCH (EXP e_2) WITH (CLAUSE `{(EXP x `: t)*} (EXP e_1) `= (VAR x) `- eps))* + ;; TODO: Propagate false in case of match failure rule Step_prems/NOT-ctx: S |- NOT pr ~>_{} NOT pr' From 74180d3ce826cbe6dff8d96407fc354ed8ab325e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 25 Mar 2026 10:51:20 +0100 Subject: [PATCH 12/13] Refactor freshness --- spectec/doc/semantics/il/1-syntax.spectec | 12 +-- spectec/doc/semantics/il/4-subst.spectec | 92 +++++++++++--------- spectec/doc/semantics/il/5-reduction.spectec | 23 ++--- 3 files changed, 72 insertions(+), 55 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index 59618e8224..468a8e6368 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -31,8 +31,9 @@ syntax deftyp = | VARIANT typcase* syntax typbind = id `: typ -syntax typfield = atom `: typ `- `{quant*} prem* -syntax typcase = mixop `: typ `- `{quant*} prem* +syntax typfield = atom `: typprems +syntax typcase = mixop `: typprems +syntax typprems = typ `- `{quant*} prem* ;; Iterators @@ -131,6 +132,7 @@ syntax exp = syntax expfield = atom `= exp syntax exppull = id `: typ `<- exp syntax exppush = exp `-> id `: typ +syntax expprems = exp `- prem* syntax path = | ROOT ;; @@ -186,9 +188,9 @@ syntax dec = | REC dec* syntax inst = INST `{quant*} arg* `= deftyp -syntax rul = RULE `{quant*} exp `- prem* -syntax clause = CLAUSE `{quant*} arg* `= exp `- prem* -syntax prod = PROD `{quant*} sym `=> exp `- prem* +syntax rul = RULE `{quant*} expprems +syntax clause = CLAUSE `{quant*} arg* `= expprems +syntax prod = PROD `{quant*} sym `=> expprems ;; Scripts diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec index 32b8185cb5..f3ca395c33 100644 --- a/spectec/doc/semantics/il/4-subst.spectec +++ b/spectec/doc/semantics/il/4-subst.spectec @@ -80,9 +80,16 @@ def $refresh_params(p*) = $refresh_list(param, $refresh_param, $subst_param, p*) +def $refresh_typ(typ) : (typ, subst) def $refresh_typbind(typbind) : (typbind, subst) def $refresh_typbinds(typbind*) : (typbind*, subst) +def $refresh_typ(VAR x a*) = (VAR x a*, {}) +def $refresh_typ(optyp) = (optyp, {}) +def $refresh_typ(TUP tb*) = (TUP tb'*, s') -- if (tb'*, s') = $refresh_typbinds(tb*) +def $refresh_typ(ITER t it) = (ITER t it, {}) +def $refresh_typ(MATCH x a* WITH inst*) = (MATCH x a* WITH inst*, {}) + def $refresh_typbind(x `: t) = (x' `: t, s) -- if (x', s) = $refresh_expid(x) @@ -115,7 +122,23 @@ def $refresh_iter(iter) : (iter, subst) def $refresh_iter(QUEST) = (QUEST, {}) def $refresh_iter(STAR) = (STAR, {}) def $refresh_iter(PLUS) = (PLUS, {}) -def $refresh_iter(SUP x e) = (SUP x' e, s) -- if (x', s) = $refresh_expid(x) +def $refresh_iter(SUP x e) = (SUP x' e, s) + -- if (x', s) = $refresh_expid(x) + + +def $refresh_prem(prem) : (prem, subst) +def $refresh_prems(prem*) : (prem*, subst) + +def $refresh_prem(REL x a* `: e) = (REL x a* `: e, {}) +def $refresh_prem(IF e) = (IF e, {}) +def $refresh_prem(ELSE) = (ELSE, {}) +def $refresh_prem(LET `{q*} e_1 `= e_2) = (LET `{q'*} $subst_exp(s, e_1) `= e_2, s) + -- if (q'*, s) = $refresh_params(q*) +def $refresh_prem(ITER pr it ep* eq*) = (ITER pr it ep* eq'*, s) + -- if (eq'*, s) = $refresh_exppushs(eq*) + +def $refresh_prems(pr*) = + $refresh_list(prem, $refresh_prem, $subst_prem, pr*) ;; Lists @@ -135,26 +158,18 @@ def $subst_fun(s, x) = x -- otherwise ;; Types def $subst_typ(subst, typ) : typ -def $subst_typ(s, t) = t' -- if (t', s') = $subst_refresh_typ(s, t) - -def $subst_refresh_typ(subst, typ) : (typ, subst) -def $subst_refresh_typ(s, VAR x a*) = (t, {}) -- if (x,t) <- s.TYP /\ a* = eps -def $subst_refresh_typ(s, VAR x a*) = (VAR x $subst_arg(s, a)*, {}) -- otherwise -def $subst_refresh_typ(s, optyp) = (optyp, {}) -def $subst_refresh_typ(s, TUP tb*) = (TUP $subst_typbind(s, tb')*, s') - -- if (tb'*, s') = $refresh_typbinds(tb*) -def $subst_refresh_typ(s, ITER t it) = (ITER $subst_typ(s ++ s', t) $subst_iter(s, it'), {}) +def $subst_typ(s, VAR x a*) = t -- if (x,t) <- s.TYP /\ a* = eps +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 tb*) = TUP $subst_typbind(s, tb)* +def $subst_typ(s, ITER t it) = ITER $subst_typ(s ++ s', t) $subst_iter(s, it') -- if (it', s') = $refresh_iter(it) -def $subst_refresh_typ(s, MATCH x a* WITH inst*) = (MATCH x $subst_arg(s, a)* WITH $subst_inst(s, inst)*, {}) +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) -def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: t' `- `{$subst_param(s ++ s', q')*} $subst_prems(s ++ s' ++ s'', pr*))* - -- if (t', s') = $subst_refresh_typ(s, t) - -- if (q'*, s'') = $refresh_params(q*) -def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: t' `- `{$subst_param(s ++ s', q')*} $subst_prems(s ++ s' ++ s'', pr*))* - -- if (t', s') = $subst_refresh_typ(s, t) - -- if (q'*, s'') = $refresh_params(q*) +def $subst_deftyp(s, STRUCT (a `: tpr)*) = STRUCT (a `: $subst_typprems(s, tpr))* +def $subst_deftyp(s, VARIANT (m `: tpr)*) = VARIANT (m `: $subst_typprems(s, tpr))* def $subst_typbind(subst, typbind) : typbind def $subst_typbind(s, x `: t) = x' `: $subst_typ(s, t) @@ -252,26 +267,28 @@ def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p')* `-> $su ;; Premises -def $subst_refresh_prem(subst, prem) : (prem, subst) -def $subst_refresh_prem(s, REL x a* `: e) = (REL x $subst_arg(s, a)* `: $subst_exp(s, e), {}) -def $subst_refresh_prem(s, IF e) = (IF $subst_exp(s, e), {}) -def $subst_refresh_prem(s, ELSE) = (ELSE, {}) -def $subst_refresh_prem(s, LET `{q*} e_1 `= e_2) = (LET `{$subst_param(s, q')*} $subst_exp(s ++ s', e_1) `= $subst_exp(s, e_2), s') - -- if (q'*, s') = $refresh_params(q*) -def $subst_refresh_prem(s, ITER pr it ep* eq*) = (ITER pr' $subst_iter(s, it') $subst_exppull(s, ep')* $subst_exppush(s ++ s''' , eq')*, s'''') +def $subst_prem(subst, prem) : prem +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 `{q*} e_1 `= e_2) = LET `{$subst_param(s, q)*} $subst_exp(s, e_1) `= $subst_exp(s, e_2) + ;; Assume: q* fresh (from caller $subst_typprems, $subst_expprems) +def $subst_prem(s, ITER pr it ep* eq*) = ITER $subst_prem(s ++ s' ++ s'', pr') $subst_iter(s, it') $subst_exppull(s, ep')* $subst_exppush(s ++ s''', eq')* + ;; Assume: eq* fresh (from caller $subst_typprems, $subst_expprems) -- if (it', s') = $refresh_iter(it) -- if (ep'*, s'') = $refresh_exppulls(ep*) - -- if (pr', s''') = $subst_refresh_prem(s ++ s' ++ s'', pr) - -- if (eq'*, s'''') = $refresh_exppushs(eq*) + -- if (pr', s''') = $refresh_prem(pr) -def $subst_refresh_prems(subst, prem*) : (prem*, subst) -def $subst_refresh_prems(s, eps) = (eps, {}) -def $subst_refresh_prems(s, pr_1 pr*) = (pr'_1 pr'*, s_1 ++ s') - -- if (pr'_1, s_1) = $subst_refresh_prem(s, pr_1) - -- if (pr'*, s') = $subst_refresh_prems(s ++ s_1, pr*) -def $subst_prems(subst, prem*) : prem* -def $subst_prems(s, pr*) = pr'* -- if (pr'*, s') = $subst_refresh_prems(s, pr*) +def $subst_typprems(subst, typprems) : typprems +def $subst_typprems(s, t `- `{q*} pr*) = $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr')* + -- if (t', s') = $refresh_typ(t) + -- if (q'*, s'') = $refresh_params(q*) + -- if (pr'*, s''') = $refresh_prems(pr*) + +def $subst_expprems(subst, expprems) : expprems +def $subst_expprems(s, e `- pr*) = $subst_exp(s ++ s', e) `- $subst_prem(s, pr)* + -- if (pr'*, s') = $refresh_prems(pr*) ;; Definitions @@ -281,19 +298,16 @@ def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q')*} $subst_ar -- if (q'*, s') = $refresh_params(q*) def $subst_rule(subst, rul) : rul -def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q')*} $subst_exp(s ++ s', e) `- pr'* +def $subst_rule(s, RULE `{q*} epr) = RULE `{$subst_param(s, q')*} $subst_expprems(s ++ s', epr) -- if (q'*, s') = $refresh_params(q*) - -- if (pr'*, s'') = $subst_refresh_prems(s ++ s', pr*) def $subst_clause(subst, clause) : clause -def $subst_clause(s, CLAUSE `{q*} a* `= e `- pr*) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `= $subst_exp(s ++ s', e) `- pr'* +def $subst_clause(s, CLAUSE `{q*} a* `= epr) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `= $subst_expprems(s ++ s', epr) -- if (q'*, s') = $refresh_params(q*) - -- if (pr'*, s'') = $subst_refresh_prems(s ++ s', pr*) def $subst_prod(subst, prod) : prod -def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_exp(s ++ s', e) `- pr'* +def $subst_prod(s, PROD `{q*} g `=> epr) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_expprems(s ++ s', epr) -- if (q'*, s') = $refresh_params(q*) - -- if (pr'*, s'') = $subst_refresh_prems(s ++ s', pr*) ;; Constructing substitutions for parameters diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 7a2590eb7a..cd11f35c2d 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -451,12 +451,11 @@ rule Step_exp/MATCH-ctx2: -- Step_clause: S |- clause*[n] ~> clause'_n rule Step_exp/MATCH-match: - S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> + S |- MATCH a* WITH (CLAUSE `{q*} a'* `= epr) clause* ~> MATCH a''* WITH - (CLAUSE `{q'*} a'''* `= $subst_exp(s ++ s', e) `- pr'*) + (CLAUSE `{q'*} a'''* `= $subst_expprems(s, epr)) (CLAUSE `{} a''* `= (MATCH a* WITH clause*) `- eps) -- Step_argmatch: S |- `{q*} (a / a')* ~>_s `{q'*} (a'' / a''')* - -- if (pr'*, s') = $subst_refresh_prems(s, pr*) rule Step_exp/MATCH-match-fail: S |- MATCH a* WITH (CLAUSE `{q*} a'* `= e `- pr*) clause* ~> @@ -820,17 +819,17 @@ rule Reduce_prems/step: rule Step_prems/seq: - S |- pr_1* pr pr_2* ~>_(s ++ s') pr_1* pr'* pr'_2 + S |- pr_1* pr pr_2* ~>_(s ++ s') pr_1* pr'* $subst_prem(s, pr'_2)* -- Step_prems: S |- pr ~>_s pr'* - -- if (pr'_2, s') = $subst_refresh_prems(s, pr_2*) + -- if (pr'_2*, s') = $refresh_prems(pr_2*) rule Step_prems/REL: S |- REL x a* `: e ~>_{} pr'* (IF (CMP EQ $subst_exp(s ++ s', e') e)) -- if (x, p* `-> t `= rul*) <- S.REL - -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)* + -- if (RULE `{q*} (e' `- pr*)) <- $subst_rule($args_for_params(a*, p*), rul)* -- Ok_subst: $storeenv(S) |- s : q* - -- if (pr'*, s') = $subst_refresh_prems(s, pr*) + -- if (pr'*, s') = $refresh_prems(pr*) ;; Note: non-computational rule rule Step_prems/IF-ctx: @@ -882,12 +881,13 @@ rule Step_prems/ITER-ctx4: -- Step_exppush: S |- eq*[n] ~> eq'_n rule Step_prems/ITER-QUEST: - S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_{EXP (x_2, OPT $subst_exp(s, e''_2)?)*} pr'? + S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_({EXP (x_2, OPT $subst_exp(s', e''_2)?)*} ++ s') + $subst_prem({EXP (x_1, e'_1)*}, pr')? -- if e'_1*? = $transpose_(exp, e_1?*) -- if e'_2*? = $transpose_(exp, e''_2?*) -- (if |e_1?| = |e''_2?|)* -- (if e'_2 = e_2)*? - -- (if (pr', s) = $subst_refresh_prems({EXP (x_1, e'_1)*}, pr))? + -- if (pr', s') = $refresh_prem(pr) rule Step_prems/ITER-PLUS: S |- ITER pr PLUS (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{} @@ -901,8 +901,9 @@ rule Step_prems/ITER-STAR: -- Fresh_id: y FRESH rule Step_prems/ITER-SUP: - S |- ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1^n)* ~>_{EXP (x_2, LIST e''_2^n)*} pr' + S |- ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1^n)* ~>_({EXP (x_2, LIST $subst_exp(s', e''_2)^n)*} ++ s') + $subst_prem({EXP (x_1, e'_1)* (y, NAT i)}, pr')^(i Date: Tue, 21 Apr 2026 13:56:29 +0200 Subject: [PATCH 13/13] [spectec] Implement let premise quantifiers (WIP) --- spectec/src/backend-ast/print.ml | 2 +- spectec/src/backend-prose/gen.ml | 2 +- spectec/src/frontend/det.ml | 2 +- spectec/src/frontend/dim.ml | 8 +++-- spectec/src/il/ast.ml | 2 +- spectec/src/il/eq.ml | 4 +-- spectec/src/il/eval.ml | 6 ++-- spectec/src/il/free.ml | 9 ++++-- spectec/src/il/free.mli | 1 + spectec/src/il/iter.ml | 10 +++--- spectec/src/il/print.ml | 7 ++-- spectec/src/il/subst.ml | 13 +++++--- spectec/src/il/subst.mli | 1 + spectec/src/il/valid.ml | 45 +++++++++++++++----------- spectec/src/il2al/animate.ml | 42 ++++++++++++++++++------ spectec/src/il2al/encode.ml | 11 ++++--- spectec/src/il2al/free.ml | 2 +- spectec/src/il2al/il2al_util.ml | 16 ++++++--- spectec/src/il2al/il_walk.ml | 2 +- spectec/src/il2al/translate.ml | 5 +-- spectec/src/il2al/unify.ml | 22 ++++++++++--- spectec/src/middlend/sideconditions.ml | 2 +- spectec/src/middlend/sub.ml | 2 +- spectec/src/middlend/totalize.ml | 2 +- spectec/src/middlend/unthe.ml | 2 +- 25 files changed, 141 insertions(+), 79 deletions(-) diff --git a/spectec/src/backend-ast/print.ml b/spectec/src/backend-ast/print.ml index 1372e94ea3..47696cfd02 100644 --- a/spectec/src/backend-ast/print.ml +++ b/spectec/src/backend-ast/print.ml @@ -162,7 +162,7 @@ and prem pr = match pr.it with | RulePr (x, as1, op, e) -> Node ("rule", id x :: List.map arg as1 @ [mixop op; exp e]) | IfPr e -> Node ("if", [exp e]) - | LetPr (e1, e2, _xs) -> Node ("let", [exp e1; exp e2]) + | LetPr (_qs, e1, e2) -> Node ("let", [exp e1; exp e2]) | ElsePr -> Atom "else" | IterPr (pr1, it) -> Node ("iter", [prem pr1] @ iterexp it) diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 29e8389a7c..f84db74fd7 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -276,7 +276,7 @@ let inject_ctx frees c stmts = let rec prem_to_instrs prem = match prem.it with - | Ast.LetPr (e1, e2, _) -> + | Ast.LetPr (_, e1, e2) -> [ LetS (exp_to_expr e1, exp_to_expr e2) ] | Ast.IfPr e -> if_expr_to_instrs e diff --git a/spectec/src/frontend/det.ml b/spectec/src/frontend/det.ml index 840479ea31..f5ae1da69a 100644 --- a/spectec/src/frontend/det.ml +++ b/spectec/src/frontend/det.ml @@ -188,7 +188,7 @@ and det_prem pr = match pr.it with | RulePr (_x, _as, _mixop, e) -> det_exp e | IfPr e -> det_cond_exp e - | LetPr (e1, _e2, _xs) -> det_exp e1 + | LetPr (_qs, e1, _e2) -> det_exp e1 | ElsePr -> empty | IterPr (pr1, ite) -> det_iterexp (det_prem pr1) ite diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml index 6e733fdb7e..f100989949 100644 --- a/spectec/src/frontend/dim.ml +++ b/spectec/src/frontend/dim.ml @@ -260,7 +260,8 @@ and check_prem dims ctx prem = check_exp dims ctx e | IfPr e -> check_exp dims ctx e | ElsePr -> () - | LetPr (e1, e2, _xs) -> + | LetPr (qs, e1, e2) -> + List.iter (check_param dims) qs; check_exp dims ctx e1; check_exp dims ctx e2 | IterPr (prem1, ite) -> @@ -678,10 +679,11 @@ and annot_prem dims prem : prem * occur = | IfPr e -> let e', occur = annot_exp `Rhs dims e in IfPr e', occur - | LetPr (e1, e2, ids) -> + | LetPr (qs, e1, e2) -> + let qs', occurs = List.split (List.map (annot_param dims) qs) in let e1', occur1 = annot_exp `Lhs dims e1 in let e2', occur2 = annot_exp `Rhs dims e2 in - LetPr (e1', e2', ids), union occur1 occur2 + LetPr (qs', e1', e2'), List.fold_left union (union occur1 occur2) occurs | ElsePr -> ElsePr, Map.empty | IterPr (prem1, iter) -> diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index 7cb5709e5c..c1f545019f 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -156,7 +156,7 @@ and prem = prem' phrase and prem' = | RulePr of id * arg list * mixop * exp (* premise *) | IfPr of exp (* side condition *) - | LetPr of exp * exp * string list (* binding *) + | LetPr of quant list * exp * exp (* binding *) | ElsePr (* otherwise *) | IterPr of prem * iterexp (* iteration *) diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml index a814f50efa..804fb9d7ba 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml @@ -147,8 +147,8 @@ and eq_prem prem1 prem2 = | IfPr e1, IfPr e2 -> eq_exp e1 e2 | IterPr (prem1, e1), IterPr (prem2, e2) -> eq_prem prem1 prem2 && eq_iterexp e1 e2 - | LetPr (e1, e1', xs1), LetPr (e2, e2', xs2) -> - eq_exp e1 e2 && eq_exp e1' e2' && xs1 = xs2 + | LetPr (qs1, e11, e12), LetPr (qs2, e21, e22) -> + eq_list eq_param qs1 qs2 && eq_exp e11 e21 && eq_exp e12 e22 | _, _ -> prem1.it = prem2.it diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index 8c9679a5bb..d7bbb6ccd7 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -498,7 +498,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = | _ -> `None ) | ElsePr -> `True Subst.empty - | LetPr (e1, e2, _ids) -> + | LetPr (_qs, e1, e2) -> (match match_exp env Subst.empty e2 e1 with | Some s -> `True s | None -> `None @@ -510,7 +510,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = * and others, which are assumed to flow inwards. *) let rec is_let_bound prem (x, _) = match prem.it with - | LetPr (_, _, xs) -> List.mem x.it xs + | LetPr (qs, _, _) -> Free.(Set.mem x.it (bound_quants qs).varid) | IterPr (premI, iterexpI) -> let _iter1', xes1' = reduce_iterexp env iterexpI in let xes1_out, _ = List.partition (is_let_bound premI) xes1' in @@ -961,7 +961,7 @@ and equiv_prem env pr1 pr2 = | RulePr (id1, mixop1, e1), RulePr (id2, mixop2, e2) -> id1.it = id2.it && Eq.eq_mixop mixop1 mixop2 && equiv_exp env e1 e2 | IfPr e1, IfPr e2 -> equiv_exp env e1 e2 - | LetPr (e11, e12, _ids1), LetPr (e21, e22, _id2) -> + | LetPr (_qs1, e11, e12), LetPr (_qs2, e21, e22) -> equiv_exp env e11 e21 && equiv_exp env e12 e22 | IterPr (pr11, iter1), IterPr (pr21, iter2) -> equiv_prem env pr11 pr21 && equiv_iter env (fst iter1) (fst iter2) diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index 728810da51..71c54bb204 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -110,11 +110,16 @@ and free_prem prem = match prem.it with | RulePr (x, as_, _op, e) -> free_relid x ++ free_args as_ ++ free_exp e | IfPr e -> free_exp e - | LetPr (e1, e2, _) -> free_exp e1 ++ free_exp e2 + | LetPr (qs, e1, e2) -> (free_exp e1 -- bound_quants qs) ++ free_exp e2 | ElsePr -> empty | IterPr (prem1, ite) -> (free_prem prem1 -- bound_iterexp ite) ++ free_iterexp ite -and free_prems prems = free_list free_prem prems +and bound_prem prem = + match prem.it with + | LetPr (qs, _e1, _e2) -> bound_quants qs + | _ -> empty + +and free_prems prems = free_list_dep free_prem bound_prem prems (* Definitions *) diff --git a/spectec/src/il/free.mli b/spectec/src/il/free.mli index 1b962475c4..2744ccf838 100644 --- a/spectec/src/il/free.mli +++ b/spectec/src/il/free.mli @@ -24,6 +24,7 @@ val free_params : param list -> sets val bound_iter : iter -> sets val bound_iterexp : iterexp -> sets +val bound_prem : prem -> sets val bound_quant : quant -> sets val bound_param : param -> sets val bound_def : def -> sets diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml index 3688a48458..7b194b3d63 100644 --- a/spectec/src/il/iter.ml +++ b/spectec/src/il/iter.ml @@ -210,7 +210,7 @@ and prem pr = | IfPr e -> exp e | ElsePr -> () | IterPr (pr1, it) -> iterexp prem pr1 it - | LetPr (e1, e2, _) -> exp e1; exp e2 + | LetPr (qs, e1, e2) -> params qs; exp e1; exp e2 and prems prs = list prem prs @@ -244,19 +244,19 @@ let hintdef d = let inst i = match i.it with - | InstD (ps, as_, dt) -> params ps; args as_; deftyp dt + | InstD (qs, as_, dt) -> params qs; args as_; deftyp dt let rule r = match r.it with - | RuleD (x, ps, op, e, prs) -> ruleid x; params ps; mixop op; exp e; prems prs + | RuleD (x, qs, op, e, prs) -> ruleid x; params qs; mixop op; exp e; prems prs let clause c = match c.it with - | DefD (ps, as_, e, prs) -> params ps; args as_; exp e; prems prs + | DefD (qs, as_, e, prs) -> params qs; args as_; exp e; prems prs let prod p = match p.it with - | ProdD (ps, g, e, prs) -> params ps; sym g; exp e; prems prs + | ProdD (qs, g, e, prs) -> params qs; sym g; exp e; prems prs let rec def d = visit_def d; diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index 05aea3ef35..110322ced9 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -218,10 +218,9 @@ and string_of_prem prem = string_of_id x ^ string_of_args as1 ^ ": " ^ string_of_mixop mixop ^ string_of_exp_args e | IfPr e -> "if " ^ string_of_exp e - | LetPr (e1, e2, xs) -> - let xs' = List.map (fun x -> x $ no_region) xs in - "where " ^ string_of_exp e1 ^ " = " ^ string_of_exp e2 ^ - " {" ^ (String.concat ", " (List.map string_of_id xs')) ^ "}" + | LetPr (qs, e1, e2) -> + "let" ^ string_of_quants qs ^ " " ^ + string_of_exp e1 ^ " = " ^ string_of_exp e2 | ElsePr -> "otherwise" | IterPr ({it = IterPr _; _} as prem', iter) -> string_of_prem prem' ^ string_of_iterexp iter diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml index 885ed05e40..d73b4ecd3a 100644 --- a/spectec/src/il/subst.ml +++ b/spectec/src/il/subst.ml @@ -141,12 +141,12 @@ and subst_deftyp s dt = and subst_typfield s (atom, (t, qs, prems), hints) = let t', s' = subst_typ' s t in let qs', s'' = subst_quants s' qs in - (atom, (t', qs', subst_list subst_prem s'' prems), hints) + (atom, (t', qs', subst_prems s'' prems), hints) and subst_typcase s (op, (t, qs, prems), hints) = let t', s' = subst_typ' s t in let qs', s'' = subst_quants s' qs in - (op, (t', qs', subst_list subst_prem s'' prems), hints) + (op, (t', qs', subst_prems s'' prems), hints) (* Expressions *) @@ -237,9 +237,14 @@ and subst_prem s prem = | IterPr (prem1, iterexp) -> let prem1', it' = subst_iterexp s subst_prem prem1 iterexp in IterPr (prem1', it') - | LetPr (e1, e2, xs) -> LetPr (subst_exp s e1, subst_exp s e2, xs) + | LetPr (qs, e1, e2) -> + let s' = remove_varids s (Free.bound_quants qs).Free.varid in + LetPr (qs, subst_exp s' e1, subst_exp s e2) ) $ prem.at +and subst_prems s prems = + fst (subst_list_dep subst_prem Free.bound_prem s prems) + (* Definitions *) @@ -274,4 +279,4 @@ let subst_typ s t = if s = empty then t else subst_typ s t let subst_deftyp s dt = if s = empty then dt else subst_deftyp s dt let subst_exp s e = if s = empty then e else subst_exp s e let subst_sym s g = if s = empty then g else subst_sym s g -let subst_prem s pr = if s = empty then pr else subst_prem s pr +let subst_prems s prs = if s = empty then prs else subst_prems s prs diff --git a/spectec/src/il/subst.mli b/spectec/src/il/subst.mli index c8fd8fc5d8..5d28899999 100644 --- a/spectec/src/il/subst.mli +++ b/spectec/src/il/subst.mli @@ -39,6 +39,7 @@ val subst_deftyp : subst -> deftyp -> deftyp val subst_typcase : subst -> typcase -> typcase val subst_typfield : subst -> typfield -> typfield +val subst_prems : subst -> prem list -> prem list val subst_args : subst -> arg list -> arg list val subst_params : subst -> param list -> param list * subst diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml index 7a0fe7eb65..526858689d 100644 --- a/spectec/src/il/valid.ml +++ b/spectec/src/il/valid.ml @@ -249,7 +249,7 @@ and valid_typfield env (atom, (t, qs, prems), _hints) = valid_atom env atom; let env' = valid_typ_bind env t in let env'' = valid_quants env' qs in - List.iter (valid_prem env'') prems + ignore (valid_prems env'' prems) and valid_typcase env (mixop, (t, qs, prems), _hints) = Debug.(log_at "il.valid_typcase" t.at @@ -267,7 +267,7 @@ and valid_typcase env (mixop, (t, qs, prems), _hints) = valid_mixop env mixop; let env' = valid_typ_bind env t in let env'' = valid_quants env' qs in - List.iter (valid_prem env'') prems + ignore (valid_prems env'' prems) (* Expressions *) @@ -592,26 +592,33 @@ and valid_prem env prem = let ps, mixop', t, _rules = Env.find_rel env x in assert (Mixop.eq mixop mixop'); let s = valid_args env as_ ps Subst.empty prem.at in - valid_expmix env mixop e (mixop, Subst.subst_typ s t) e.at + valid_expmix env mixop e (mixop, Subst.subst_typ s t) e.at; + env | IfPr e -> - valid_exp env e (BoolT $ e.at) - | LetPr (e1, e2, xs) -> + valid_exp env e (BoolT $ e.at); + env + | LetPr (qs, e1, e2) -> + let env' = valid_quants env qs in let t = infer_exp env e2 in - valid_exp ~side:`Lhs env e1 t; + valid_exp ~side:`Lhs env' e1 t; valid_exp env e2 t; - let target_ids = Free.{empty with varid = Set.of_list xs} in - let free_ids = Free.(free_exp e1) in - if not (Free.subset target_ids free_ids) then - error prem.at ("target identifier(s) " ^ - ( Free.Set.elements (Free.diff target_ids free_ids).varid |> + let bound = Free.(bound_quants qs) in + let free = Free.(free_exp e1) in + if not (Free.subset bound free) then + error prem.at ("quantified identifier(s) " ^ + ( Free.Set.elements (Free.diff bound free).varid |> List.map (fun x -> "`" ^ x ^ "`") |> String.concat ", " ) ^ - " do not occur in left-hand side expression") + " do not occur in left-hand side expression"); + env' | ElsePr -> - () + env | IterPr (prem', ite) -> let _it, env' = valid_iterexp env ite prem.at in - valid_prem env' prem' + let _env'' = valid_prem env' prem' in + env (* TODO: out it *) + +and valid_prems env prems = List.fold_left valid_prem env prems (* Definitions *) @@ -695,7 +702,7 @@ let valid_rule env mixop t rule = | RuleD (_x, qs, mixop', e, prems) -> let env' = valid_quants env qs in valid_expmix ~side:`Lhs env' mixop' e (mixop, t) e.at; - List.iter (valid_prem env') prems + ignore (valid_prems env' prems) let valid_clause env x ps t clause = Debug.(log_in "il.valid_clause" line); @@ -706,8 +713,8 @@ let valid_clause env x ps t clause = | DefD (qs, as_, e, prems) -> let env' = valid_quants env qs in let s = valid_args env' as_ ps Subst.empty clause.at in - valid_exp env' e (Subst.subst_typ s t); - List.iter (valid_prem env') prems + let env'' = valid_prems env' prems in + valid_exp env'' e (Subst.subst_typ s t) let valid_prod env ps t prod = Debug.(log_in "il.valid_prod" line); @@ -718,8 +725,8 @@ let valid_prod env ps t prod = | ProdD (qs, g, e, prems) -> let env' = valid_quants env qs in let _t' = valid_sym env' g in - valid_exp env' e t; - List.iter (valid_prem env') prems + let env'' = valid_prems env' prems in + valid_exp env'' e t let infer_def env d : Env.t = match d.it with diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml index 5308fefc99..a37c25b92d 100644 --- a/spectec/src/il2al/animate.ml +++ b/spectec/src/il2al/animate.ml @@ -48,6 +48,19 @@ let is_assign env (tag, prem, _) = | Assign frees -> subset (diff (free_prem false prem) {empty with varid = (Set.of_list frees)}) env | _ -> false +(* conversion between quantifiers and id lists *) +let ids_of_quants qs = + List.filter_map (fun q -> + match q.it with + | ExpP (id, _) -> Some id.it + | _ -> None + ) qs + +let quants_of_ids ids = + List.map (fun id -> + ExpP (id $ no_region, VarT ("?" $ no_region, []) $ no_region) $ no_region + ) ids + (* Rewrite iterexp of IterPr *) let rewrite (iter, xes) e = let rewrite' e' = @@ -67,6 +80,10 @@ let rewrite_id (_, xes) id = | _ -> None ) xes |> get_or_else id +let rewrite_quant iterexp q = + match q.it with + | ExpP (id, t) -> ExpP (rewrite_id iterexp id.it $ id.at, t) $ q.at + | _ -> q let rec rewrite_iterexp' iterexp pr = let transformer = { Il_walk.base_transformer with transform_exp = rewrite iterexp } in @@ -74,9 +91,9 @@ let rec rewrite_iterexp' iterexp pr = match pr with | RulePr (id, args, mixop, e) -> RulePr (id, args, mixop, new_ e) | IfPr e -> IfPr (new_ e) - | LetPr (e1, e2, ids) -> - let new_ids = List.map (rewrite_id iterexp) ids in - LetPr (new_ e1, new_ e2, new_ids) + | LetPr (qs, e1, e2) -> + let new_qs = List.map (rewrite_quant iterexp) qs in + LetPr (new_qs, new_ e1, new_ e2) | ElsePr -> ElsePr | IterPr (pr, (iter, xes)) -> IterPr (rewrite_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e)))) and rewrite_iterexp iterexp pr = Source.map (rewrite_iterexp' iterexp) pr @@ -97,6 +114,10 @@ let recover_id (_, xes) id = | _ -> None ) xes |> get_or_else id +let recover_quant iterexp q = + match q.it with + | ExpP (id, t) -> ExpP (recover_id iterexp id.it $ id.at, t) $ q.at + | _ -> q let rec recover_iterexp' iterexp pr = let transformer = { Il_walk.base_transformer with transform_exp = recover iterexp } in @@ -104,9 +125,9 @@ let rec recover_iterexp' iterexp pr = match pr with | RulePr (id, args, mixop, e) -> RulePr (id, args, mixop, new_ e) | IfPr e -> IfPr (new_ e) - | LetPr (e1, e2, ids) -> - let new_ids = List.map (recover_id iterexp) ids in - LetPr (new_ e1, new_ e2, new_ids) + | LetPr (qs, e1, e2) -> + let new_qs = List.map (recover_quant iterexp) qs in + LetPr (new_qs, new_ e1, new_ e2) | ElsePr -> ElsePr | IterPr (pr, (iter, xes)) -> IterPr (recover_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e)))) and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr @@ -114,14 +135,14 @@ and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr (* is this assign premise a if-let? *) let is_cond_assign prem = match prem.it with - | LetPr ({it = CaseE (_, _); _}, _, _) -> true + | LetPr (_, {it = CaseE (_, _); _}, _) -> true | _ -> false (* is this assign premise encoded premise for popping one value? *) let is_pop env row = is_assign env row && match (unwrap row).it with - | LetPr (_, {it = CallE (_, {it = ExpA n; _} :: _); note; _}, _) when Il.Print.string_of_typ note = "stackT" -> + | LetPr (_, _, {it = CallE (_, {it = ExpA n; _} :: _); note; _}) when Il.Print.string_of_typ note = "stackT" -> (match n.it with | NumE (`Nat i) -> Z.equal i (Z.one) | _ -> false) @@ -272,7 +293,7 @@ let rows_of_eq vars len i l r at = |> List.filter_map (fun frees -> let covering_vars = List.filter_map (index_of len vars) frees in if List.length frees = List.length covering_vars then ( - Some (Assign frees, LetPr (l, r, frees) $ at, [i] @ covering_vars) ) + Some (Assign frees, LetPr (quants_of_ids frees, l, r) $ at, [i] @ covering_vars) ) else None ) @@ -290,7 +311,8 @@ let rec rows_of_prem vars len i p = @ rows_of_eq vars len i l { r with it = TheE r } p.at | _ -> [ Condition, p, [i] ] ) - | LetPr (_, _, targets) -> + | LetPr (qs, _, _) -> + let targets = ids_of_quants qs in let covering_vars = List.filter_map (index_of len vars) targets in [ Assign targets, p, [i] @ covering_vars ] | RulePr (_, _, _, { it = TupE args; _ }) -> diff --git a/spectec/src/il2al/encode.ml b/spectec/src/il2al/encode.ml index 149f1ae9b6..63c9d9da2e 100644 --- a/spectec/src/il2al/encode.ml +++ b/spectec/src/il2al/encode.ml @@ -61,6 +61,7 @@ let free_ids e = (free_exp false e) .varid |> Set.elements + |> List.map (fun id -> ExpP (id $ no_region, mk_varT "?") $ no_region) let dim e = let t = (NumT `NatT $ no_region) in @@ -91,7 +92,7 @@ let encode_inner_stack context_opt stack = [] else let unused = TupE dropped $$ no_region % (mk_varT "unusedT") in - [LetPr (unused, mk_varE "unused" "unusedT", free_ids unused) $ no_region] + [LetPr (free_ids unused, unused, mk_varE "unused" "unusedT") $ no_region] in match es with @@ -101,13 +102,13 @@ let encode_inner_stack context_opt stack = match context_opt with | None -> assert false | Some e -> - Some (LetPr (e, mk_varE "input" "inputT", free_ids e) $ e.at), unused_prems + Some (LetPr (free_ids e, e, mk_varE "input" "inputT") $ e.at), unused_prems ) | _ -> (* ASSUMPTION: The top of the stack should be now the target instruction *) let winstr, operands = Lib.List.split_hd es in - let prem = LetPr (winstr, mk_varE "input" "inputT", free_ids winstr) $ winstr.at in + let prem = LetPr (free_ids winstr, winstr, mk_varE "input" "inputT") $ winstr.at in let prems = List.mapi (fun i e -> let s0 = ("stack" ^ string_of_int i) in let s1 = ("stack" ^ string_of_int (i+1)) in @@ -138,7 +139,7 @@ let encode_stack stack = let e1 = { e with it = CaseE (mixop', TupE args' $$ no_region % (mk_varT "")) } in let e2 = (mk_varE "ctxt" "contextT") in - let pr = LetPr (e1, e2, free_ids e1) $ e2.at in + let pr = LetPr (free_ids e1, e1, e2) $ e2.at in let pr_opt, prs = encode_inner_stack (Some e) inner_stack in ( @@ -153,7 +154,7 @@ let encode_stack stack = let encode_lhs lhs = match lhs.it with | CaseE (Xl.Mixop.(Infix (Arg (), {it = Semicolon; _}, Arg ())), {it = TupE [z; stack]; _}) -> - let prem = LetPr (z, mk_varE "state" "stateT", free_ids z) $ z.at in + let prem = LetPr (free_ids z, z, mk_varE "state" "stateT") $ z.at in prem :: encode_stack stack | _ -> let stack = lhs in diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml index af0f4029f7..047306712f 100644 --- a/spectec/src/il2al/free.ml +++ b/spectec/src/il2al/free.ml @@ -83,7 +83,7 @@ let rec free_prem ignore_listN prem = match prem.it with | RulePr (_id, args, _op, e) -> free_list fa args ++ f e | IfPr e -> f e - | LetPr (e1, e2, _ids) -> f e1 ++ f e2 + | LetPr (_qs, e1, e2) -> f e1 ++ f e2 | ElsePr -> empty | IterPr (prem', iter) -> let free1 = fp prem' in diff --git a/spectec/src/il2al/il2al_util.ml b/spectec/src/il2al/il2al_util.ml index 72e1826c4b..18e5893857 100644 --- a/spectec/src/il2al/il2al_util.ml +++ b/spectec/src/il2al/il2al_util.ml @@ -34,20 +34,26 @@ let prems_of_rule rule = let lhs_of_prem pr = match pr.it with - | LetPr (lhs, _, _) -> lhs + | LetPr (_, lhs, _) -> lhs | _ -> error pr.at "expected a LetPr" let rhs_of_prem pr = match pr.it with - | LetPr (_, rhs, _) -> rhs + | LetPr (_, _, rhs) -> rhs | _ -> error pr.at "expected a LetPr" let replace_lhs lhs pr = let open Il.Free in match pr.it with - | LetPr (lhs', rhs, _) -> + | LetPr (qs, lhs', rhs) -> if Il.Eq.eq_exp lhs lhs' then pr else - { pr with it = LetPr (lhs, rhs, (free_exp lhs).varid |> Set.elements) } + let free = free_exp lhs in + let qs' = List.filter (fun q -> + match q.it with + | ExpP (id, _) -> Set.mem id.it free.varid + | _ -> true + ) qs in + { pr with it = LetPr (qs', lhs, rhs) } | _ -> error pr.at "expected a LetPr" let case_of_case e = @@ -87,7 +93,7 @@ let split_last_case mixop = Option.get (split_last_case' mixop) let is_let_prem_with_rhs_type t prem = match prem.it with - | LetPr (_, e, _) -> + | LetPr (_, _, e) -> (match e.note.it with | VarT (id, []) -> id.it = t | _ -> false diff --git a/spectec/src/il2al/il_walk.ml b/spectec/src/il2al/il_walk.ml index 90d5c842ef..0b42810697 100644 --- a/spectec/src/il2al/il_walk.ml +++ b/spectec/src/il2al/il_walk.ml @@ -72,7 +72,7 @@ and transform_prem t p = let it = match p.it with | RulePr (id, as1, op, e) -> RulePr (id, List.map (transform_arg t) as1, op, transform_exp t e) | IfPr e -> IfPr (transform_exp t e) - | LetPr (e1, e2, ss) -> LetPr (transform_exp t e1, transform_exp t e2, ss) + | LetPr (qs, e1, e2) -> LetPr (qs, transform_exp t e1, transform_exp t e2) | ElsePr -> ElsePr | IterPr (p, ie) -> IterPr (transform_prem t p, transform_iterexp t ie) in diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 4d56bea331..a1b1966df1 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -142,7 +142,7 @@ let is_winstr_prem = is_let_prem_with_rhs_type "inputT" let lhs_of_prem pr = match pr.it with - | Il.LetPr (lhs, _, _) -> lhs + | Il.LetPr (_, lhs, _) -> lhs | _ -> Error.error pr.at "prose translation" "expected a LetPr" let rec is_wasm_value e = @@ -979,7 +979,8 @@ and translate_prem prem = match prem.it with | Il.IfPr exp -> [ ifI (translate_exp exp, [], []) ~at ] | Il.ElsePr -> [ otherwiseI [] ~at ] - | Il.LetPr (exp1, exp2, ids) -> + | Il.LetPr (qs, exp1, exp2) -> + let ids = List.filter_map (fun q -> match q.it with (Il.ExpP (id, _)) -> Some id.it | _ -> None) qs in init_lhs_id (); translate_letpr exp1 exp2 ids | Il.RulePr (id, args, _, exp) -> diff --git a/spectec/src/il2al/unify.ml b/spectec/src/il2al/unify.ml index 4db51215a3..170aa34b94 100644 --- a/spectec/src/il2al/unify.ml +++ b/spectec/src/il2al/unify.ml @@ -40,6 +40,13 @@ let imap : idxs ref = ref Map.empty let init_env frees = { idxs = !imap; frees } +let ids_of_quants qs = + List.filter_map (fun q -> + match q.it with + | ExpP (id, _) -> Some id.it + | _ -> None + ) qs + let gen_new_unified ?prefix env ty = let var = match prefix with @@ -58,6 +65,11 @@ let rename_string _env s = let rename_id env id = { id with it = rename_string env id.it } +let rename_quant env q = + match q.it with + | ExpP (id, t) -> ExpP (rename_id env id, t) $ q.at + | _ -> q + let rename_iterexp env (iter, ides) = (iter, List.map (fun (id, e) -> (rename_id env id, e)) ides) let rename_exp env exp = @@ -68,7 +80,7 @@ let rename_exp env exp = let rename_prem env p = {p with it = match p.it with - | LetPr (e1, e2, ss) -> LetPr (e1, e2, List.map (rename_string env) ss) + | LetPr (qs, e1, e2) -> LetPr (List.map (rename_quant env) qs, e1, e2) | p' -> p' } let rename_rule_def (env, rd) = @@ -319,14 +331,14 @@ let unify_enc env premss encs = let is_encoded_ctxt pr = match pr.it with - | LetPr (_, e, _) -> + | LetPr (_, _, e) -> (match e.note.it with | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"; "contextT"] | _ -> false) | _ -> false let is_encoded_pop_or_winstr pr = match pr.it with - | LetPr (_, e, _) -> + | LetPr (_, _, e) -> (match e.note.it with | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"] | _ -> false) @@ -433,7 +445,7 @@ let unify_rule_def (env: env) (rule: rule_def) : rule_def = List.concat_map (fun p -> match p.it with - | LetPr (_, _, ids) -> ids + | LetPr (qs, _, _) -> ids_of_quants qs | _ -> assert false ) pops @@ -461,7 +473,7 @@ let reorder_unified_args args prems = (* Helpers *) let has_uarg_on_rhs p = match p.it with - | LetPr (_, {it = VarE id; _}, _) -> is_unified_id id.it + | LetPr (_, _, {it = VarE id; _}) -> is_unified_id id.it | _ -> false in let on_rhs p a = diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml index 5000d56768..6872b78e11 100644 --- a/spectec/src/middlend/sideconditions.ml +++ b/spectec/src/middlend/sideconditions.ml @@ -131,7 +131,7 @@ let rec t_prem env prem = (match prem.it with | RulePr (_, args, _, exp) -> List.concat_map (t_arg env) args @ t_exp env exp | IfPr e -> t_exp env e - | LetPr (e1, e2, _) -> t_exp env e1 @ t_exp env e2 + | LetPr (_qs, e1, e2) -> t_exp env e1 @ t_exp env e2 | ElsePr -> [] | IterPr (prem, iterexp) -> iter_side_conditions env iterexp @ diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index 1aa0fe5d91..38dcc24ca2 100644 --- a/spectec/src/middlend/sub.ml +++ b/spectec/src/middlend/sub.ml @@ -216,7 +216,7 @@ and t_params env = List.map (t_param env) and t_prem' env = function | RulePr (id, args, mixop, exp) -> RulePr (id, t_args env args, mixop, t_exp env exp) | IfPr e -> IfPr (t_exp env e) - | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids) + | LetPr (qs, e1, e2) -> LetPr (t_params env qs, t_exp env e1, t_exp env e2) | ElsePr -> ElsePr | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp) diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml index ade0ec336c..feb8e5ee98 100644 --- a/spectec/src/middlend/totalize.ml +++ b/spectec/src/middlend/totalize.ml @@ -154,7 +154,7 @@ and t_params env = List.map (t_param env) and t_prem' env = function | RulePr (id, args, mixop, exp) -> RulePr (id, t_args env args, mixop, t_exp env exp) | IfPr e -> IfPr (t_exp env e) - | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids) + | LetPr (qs, e1, e2) -> LetPr (t_params env qs, t_exp env e1, t_exp env e2) | ElsePr -> ElsePr | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp) diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml index fb2155f825..015d1bc15c 100644 --- a/spectec/src/middlend/unthe.ml +++ b/spectec/src/middlend/unthe.ml @@ -198,7 +198,7 @@ and t_prem' n prem : eqns * prem' = match prem with | RulePr (a, args, b, exp) -> binary (fun n x -> t_list t_arg n x Fun.id) t_exp n (args, exp) (fun (args', exp') -> RulePr (a, args', b, exp')) | IfPr e -> unary t_exp n e (fun e' -> IfPr e') - | LetPr (e1, e2, ids) -> binary t_exp t_exp n (e1, e2) (fun (e1', e2') -> LetPr (e1', e2', ids)) + | LetPr (qs, e1, e2) -> binary t_exp t_exp n (e1, e2) (fun (e1', e2') -> LetPr (qs, e1', e2')) | ElsePr -> [], prem | IterPr (prem, iterexp) -> let eqns1, prem' = t_prem n prem in