From 3578bdc27c63edf81096a922c20f5e38675654c3 Mon Sep 17 00:00:00 2001
From: jaehyun1ee <99jaehyunlee@kaist.ac.kr>
Date: Tue, 24 Mar 2026 20:16:10 +0900
Subject: [PATCH] add fail rule for str match; fix comments

---
 spectec/doc/semantics/il/1-syntax.spectec    | 8 ++++----
 spectec/doc/semantics/il/5-reduction.spectec | 3 +++
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec
index bb369461e0..66e16b7699 100644
--- a/spectec/doc/semantics/il/1-syntax.spectec
+++ b/spectec/doc/semantics/il/1-syntax.spectec
@@ -115,7 +115,7 @@ syntax exp =
   | LIST exp*               ;; [ exp* ]
   | LIFT exp                ;; exp : _? <: _*
   | STR expfield*           ;; { expfield* }
-  | SEL exp nat             ;; exp.i
+  | SEL exp nat             ;; exp.n
   | LEN exp                 ;; | exp |
   | MEM exp exp             ;; exp `<-` exp
   | CAT exp exp             ;; exp `++` exp
@@ -123,8 +123,8 @@ syntax exp =
   | 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
+  | ITER exp iter exppull*  ;; exp iter{ exppull* }
+  | CVT exp numtyp numtyp   ;; exp : numtyp1 <:> numtyp2
   | SUB exp typ typ         ;; exp : typ1 <: typ2
   | MATCH arg* WITH clause* ;; `match` arg* `with` clause*
 
@@ -149,7 +149,7 @@ syntax sym =
   | SEQ sym*           ;; sym*
   | ALT sym*           ;; sym `|` sym
   | RANGE sym sym      ;; sym `|` `...` `|` sym
-  | ITER sym iter exppull*   ;; sym iter{ expiter* }
+  | ITER sym iter exppull*   ;; sym iter{ exppull* }
   | ATTR exp sym       ;; exp `:` sym
 
 
diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec
index 91a55d66f8..0dffbf67cd 100644
--- a/spectec/doc/semantics/il/5-reduction.spectec
+++ b/spectec/doc/semantics/il/5-reduction.spectec
@@ -697,6 +697,9 @@ rule Step_expmatch_plain/STR:
   -- (if (l `= e') = ef')*
   -- (if (l `= e) <- ef*)*
 
+rule Step_expmatch_plain/STR-fail:
+  S |- STR ef* / STR ef'* ~> FAIL
+  -- otherwise
 
 rule Step_expmatch_plain/ITER-PLUS:
   S |- LIST e* / ITER e' PLUS (x `: t `<- e_p)* ~>