[spectec] Handle shadowing in IL semantics

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)

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*)

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