[spectec] Misc corrections for SpecTec IL semantics

spectec/doc/semantics/il/1-syntax.spectec

@@ -115,16 +115,16 @@ 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
   | 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
+  | 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
 
 

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