From aa8718c16d7a9485e14f859ace80924a961bf72c Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 4 Jun 2026 13:28:10 +0200 Subject: [PATCH] [spectec] Handle shadowing in IL semantics --- spectec/doc/semantics/il/2-env.spectec | 21 ++++++++++++++++++++ spectec/doc/semantics/il/5-reduction.spectec | 6 +++--- spectec/doc/semantics/il/6-typing.spectec | 16 +++++++-------- 3 files changed, 32 insertions(+), 11 deletions(-) diff --git a/spectec/doc/semantics/il/2-env.spectec b/spectec/doc/semantics/il/2-env.spectec index f198b3b432..0fff887d40 100644 --- a/spectec/doc/semantics/il/2-env.spectec +++ b/spectec/doc/semantics/il/2-env.spectec @@ -35,3 +35,24 @@ def $paramenv(TYP x) = {TYP (x, eps `-> OK `= eps)} def $paramenv(FUN x `: p* `-> t) = {FUN (x, p* `-> t `= eps)} def $paramenv(GRAM x `: p* `-> t) = {GRAM (x, p* `-> t `= eps)} def $paramenv(param*) = $composeenvs($paramenv(param)*) -- otherwise + + +;; Lookup + + +def $lookup_typ(S, id) : typdef? hint(show %.TYP#(%)) +def $lookup_fun(S, id) : fundef? hint(show %.FUN#(%)) +def $lookup_rel(S, id) : reldef? hint(show %.REL#(%)) +def $lookup_gram(S, id) : gramdef? hint(show %.GRAM#(%)) +def $lookup_exp(S, id) : typ? hint(show %.EXP#(%)) + +def $lookup_(syntax Y, (id, Y)*, id) : Y? +def $lookup_(syntax Y, eps, x') = eps +def $lookup_(syntax Y, (x, y)* (x', y'), x') = y' +def $lookup_(syntax Y, (x, y)* (x'', y'), x') = $lookup_(Y, (x, y)*, x') -- if x'' =/= x' + +def $lookup_typ(S, x) = $lookup_(typdef, S.TYP, x) +def $lookup_fun(S, x) = $lookup_(fundef, S.FUN, x) +def $lookup_rel(S, x) = $lookup_(reldef, S.REL, x) +def $lookup_gram(S, x) = $lookup_(gramdef, S.GRAM, x) +def $lookup_exp(E, x) = $lookup_(typ, E.EXP, x) diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index ebe9a64a88..272c8e9210 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -35,7 +35,7 @@ rule Reduce_typ/step: rule Step_typ/VAR-apply: S |- VAR x a* ~> MATCH x a* WITH inst* - -- if (x, p* `-> OK `= inst*) <- S.TYP + -- if $lookup_typ(S, x) = (p* `-> OK `= inst*) rule Step_typ/MATCH-alias: S |- MATCH x eps WITH (INST `{} eps `=> ALIAS t) inst* ~> t @@ -455,7 +455,7 @@ rule Step_exp/ITER-SUP-bad: rule Step_exp/CALL-apply: S |- CALL x a* ~> MATCH a* WITH clause* - -- if (x, p* `-> t `= clause*) <- S.FUN + -- if $lookup_fun(S, x) = (p* `-> t `= clause*) rule Step_exp/CVT-NUM-good: @@ -1419,7 +1419,7 @@ rule Step_prems/ctx-fail: 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 $lookup_rel(S, x) = (p* `-> t `= rul*) -- if (RULE `{q*} (e' `- pr*)) <- $subst_rule($args_for_params(a*, p*), rul)* -- Ok_subst: $storeenv(S) |- s : q* -- if (pr'*, s') = $refresh_prems(pr*) diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec index 7cde9d69c8..44b4af9716 100644 --- a/spectec/doc/semantics/il/6-typing.spectec +++ b/spectec/doc/semantics/il/6-typing.spectec @@ -108,7 +108,7 @@ rule Ok_typ/optyp: rule Ok_typ/VAR: E |- VAR x a* : OK - -- if (x, p* `-> OK `= inst*) <- E.TYP + -- if $lookup_typ(E, x) = (p* `-> OK `= inst*) -- Ok_args: E |- a* : p* => s rule Ok_typ/TUP-empty: @@ -126,7 +126,7 @@ rule Ok_typ/ITER: rule Ok_typ/MATCH: E |- MATCH x a* WITH inst* : OK - -- if (x, p* `-> OK `= inst'*) <- E.TYP + -- if $lookup_typ(E, x) = (p* `-> OK `= inst'*) -- Ok_args: E |- a* : p* => s -- (Ok_inst: E |- inst : p* -> OK)* @@ -243,7 +243,7 @@ rule Ok_exp/TEXT: rule Ok_exp/VAR: E |- VAR x : t - -- if (x, t) <- E.EXP + -- if $lookup_exp(E, x) = t rule Ok_exp/UN-BOOL: @@ -361,7 +361,7 @@ rule Ok_exp/EXT: rule Ok_exp/CALL: E |- CALL x a* : $subst_typ(s, t) - -- if (x, (p* `-> t `= cl*)) <- E.FUN + -- if $lookup_fun(E, x) = (p* `-> t `= cl*) -- Ok_args: E |- a* : p* => s @@ -445,7 +445,7 @@ relation Ok_sym: E |- sym : typ rule Ok_sym/VAR: E |- VAR x a* : $subst_typ(s, t) - -- if (x, (p* `-> t `= prod*)) <- E.GRAM + -- if $lookup_gram(E, x) = (p* `-> t `= prod*) -- Ok_args: E |- a* : p* => s rule Ok_sym/NUM: @@ -511,7 +511,7 @@ rule Ok_prems/cons: rule Ok_prem/REL: E |- REL x a* `: e : OK -| {} - -- if (x, (p* `-> t `= rul*)) <- E.REL + -- if $lookup_rel(E, x) = (p* `-> t `= rul*) -- Ok_args: E |- a* : p* => s -- Ok_exp: E |- e : $subst_typ(s, t) @@ -586,7 +586,7 @@ rule Ok_arg/EXP: rule Ok_arg/FUN: E |- FUN y : FUN x `: p* `-> t => {FUN (x, y)} - -- if (y, (p'* `-> t' `= clause*)) <- E.FUN + -- if $lookup_fun(E, y) = (p'* `-> t' `= clause*) -- Sub_params: E |- p* <: p'* => s -- Sub_typ: E |- $subst_typ(s, t') <: t @@ -596,7 +596,7 @@ rule Ok_arg/GRAM-ground: rule Ok_arg/GRAM-higher: E |- GRAM (VAR y) : GRAM x `: p* `-> t => {GRAM (x, VAR y)} - -- if (y, (p'* `-> t' `= prod*)) <- E.GRAM + -- if $lookup_gram(E, y) = (p'* `-> t' `= prod*) -- Sub_params: E |- p* <: p'* => s -- Sub_typ: E |- $subst_typ(s, t') <: t