[spectec] Fix typos in IL semantics (#2091)

Author: sukyoung

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

@@ -57,8 +57,8 @@ def $subst_typ(s, ITER t it) = ITER $subst_typ(s, t) $subst_iter(s, it)
 
 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 `: $subst_typ(s, t) `- `{$subst_quant(s, b)*} $subst_prem(s, pr)*)*  ;; TODO: avoid capture
-def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: $subst_typ(s, t) `- `{$subst_quant(s, b)*} $subst_prem(s, pr)*)*  ;; TODO: avoid capture
+def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: $subst_typ(s, t) `- `{$subst_quant(s, q)*} $subst_prem(s, pr)*)*  ;; TODO: avoid capture
+def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: $subst_typ(s, t) `- `{$subst_quant(s, q)*} $subst_prem(s, pr)*)*  ;; TODO: avoid capture
 
 
 ;; Iterators
@@ -149,20 +149,6 @@ 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
 
 
-;; Constructing substitutions for parameters
-
-def $arg_for_param(arg, param) : subst
-def $arg_for_param(EXP e, EXP x `: t) = {EXP (x, e)}
-def $arg_for_param(TYP t, TYP x) = {TYP (x, t)}
-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

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

@@ -17,7 +17,7 @@ rule Expand_typ/alias:
 
 rule Expand_typ/step:
   S |- VAR x a* => $subst_deftyp(s, dt)
-  -- if (x, p* `-> OK `= inst*) <- E.TYP
+  -- if (x, p* `-> OK `= inst*) <- S.TYP
   -- if (INST `{q*} a* `= dt) <- inst*
   -- Match_args: S |- a* `/ `{q*} a'* => s
 
@@ -123,11 +123,11 @@ rule Step_exp/CMP-EQ-true:
 
 rule Step_exp/CMP-EQ-false:
   S |- CMP EQ val_1 val_2 ~> BOOL false
-  -- if val_1 =/= val_2
+  -- if val_1 = val_2
 
 rule Step_exp/CMP-NE-false:
   S |- CMP NE e_1 e_2 ~> BOOL false
-  -- if e_1 = e_2
+  -- if e_1 =/= e_2
 
 rule Step_exp/CMP-NE-true:
   S |- CMP NE val_1 val_2 ~> BOOL true
@@ -338,7 +338,7 @@ rule Step_exp/ITER-STAR:
   -- if |e'**[0]| = n
 
 rule Step_exp/ITER-SUP-eps:
-  S |- ITER e (SUP eps e_n) (x `<- LIST e'*)* ~> ITER e (SUP y n) (x `<- LIST e'*)*
+  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:
@@ -352,7 +352,7 @@ rule Step_exp/CALL-ctx:
 
 rule Step_exp/CALL-apply:
   S |- CALL x a* ~> $subst_exp(s, e)
-  -- if (x, p* `-> t `= clause*) <- E.FUN
+  -- 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
@@ -519,7 +519,7 @@ rule Step_prems/ITER-STAR:
   -- if |e**[0]| = n
 
 rule Step_prems/ITER-SUP-eps:
-  S |- ITER pr (SUP eps e_n) (x `<- LIST e*)* ~> ITER pr (SUP y n) (x `<- LIST e*)*
+  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: