From 3ee8583fcdc8a052a3c75cdab488e2a38a790dec Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 18 Nov 2025 12:37:19 +0100
Subject: [PATCH 1/4] [spectec] Track closed normal forms for performance

---
 spectec/doc/example/output/NanoWasm.pdf | Bin 245571 -> 245572 bytes
 spectec/src/backend-latex/render.ml     |   2 +-
 spectec/src/il/ast.ml                   |   6 +-
 spectec/src/il/eval.ml                  | 129 ++++++++++++++----------
 spectec/src/il/subst.ml                 |   3 +
 spectec/src/il2al/preprocess.ml         |   2 +-
 spectec/src/util/lib.ml                 |  13 +++
 spectec/src/util/lib.mli                |   6 ++
 spectec/src/util/source.ml              |  16 +--
 spectec/src/util/source.mli             |   4 +-
 10 files changed, 117 insertions(+), 64 deletions(-)

diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 3401b402bf0e00a21ab9bde6998f8a7301d274b4..e1a6afd34bf4e407e8fad4ada8e3289451e54cba 100644
GIT binary patch
delta 880
zcmX^7kMGDoz71wVjK-4>Fl$au5IQZ?bm^>&M5NmDS8s3U)G<mc`u=OS5pK5;W&~oU
z?KZ;9B8#*QEewr}jf@Sn4Gh%{4AeEb^nLSFToOxC6*OF|j0}uS4Gm#RwpVXuE@X2y
zGI2IGGcYiBGjuaGb8<CvaxpeBb#*j!v~)9ev2=B|Q?MbVWV-$yX2*IyYo(4&9XjFP
zLRrjRLc$`a9_5`Xo1FP(P0!q^8#f!Ol&RH;UOaN_RMca80pV!jXkCwzdDowvw0=LQ
z_}Lum^RmX9_veLWNp3!J$LibEXU5N5k9+VLCA6+<o6;b&!K-}A6z)$4q+(4q<wY7w
zcWDJFYA{KcOkI*xz>sq(bb{A``hy}9oy%KJ2L-rI_b#7t+Ihhoz5c!_FW8J1b@(}N
z(eUq1vI_IuqF5%SS`ro4{%}g5+i^ajzXDrJzLwmIl3lSpd&%W@(hk$swfY^m;*)x5
z^`hjH+6ABM-pl7NVcpVXw*5)&FRf3<f<*TD1bzzDUwU}0&FU-X?&LmurCZYIxBYPa
z=Uum%{Tkv5guXP^6>!aAOFs}<z{k_@IYA(X!TEvG4i>%UzzcKj-p-w8#^ZLQo3W;|
z`hl3a+JPC-Pt|$l*e^fmioR-GIys?h=cOFJGdn{6U%VT+fn(jSt0F6RANwTzfG>hI
zJ3;nN>ItUTCr?TzoLu{F`m;FpTeosI@I<I4M%8DW5Zm!`n(p<be4Cl_Hfwxp_d8kU
z+?T(5>z>2{m3e#W7PQ0!KDcJS(mSpwhbe?}W^X~`T*bzVW=nK8wWYjeyPC)RIEvNU
zx$IHO2~QuME8HvF3mOv@4+m)7YFP4;B{pyRr!8`MF8#MZ)W$0L7W|2Lw&KrR=3*uw
ze5B?u-=Tg!kU)YDSXua3LGaQM4vEs)cdi}|_Ld9P=-q8AA2h3=`nQ+n*QdAVTv~Gb
z--1h1st=1V&HO&mb*bd{t?gc$-}!$%-f8)LuG7-h@8+i_#T5VFxzyzS%s2BcHKot{
zGk^DsnR}0WdCxmj7ryJ=Nx%J-pB5S%)qlr-a~?mJgYF9EUv4H1Iu?9idNY{LI?Qhm
qyTEp<(T;!aygmQt>iz%N`j`2a_OvV0rS>x`au{)`s=E5SaRC5)-Glo8

delta 858
zcmX@|kMHn5z71wVj7F0WFl$au5IQZ$^fQgGM`v>J*KfII`=wNTzc<?ox7!Lc0x{Ee
zTVZCAMH~i3h6W~vrsmTlw=zq^dE0BYG8eKr8@L&onK?NbSejaz85mf)n!6f0x*D1o
zI~$u@SUQ>;+9}u&QZn6O53^%^-vL&afEa;Dz2EB|^=WKc-=wo>#Tp@RVQuT=)a6TC
zIXkDa#xFj0<k+!!FYFtR+`5squ=CvKTQ-%?=N6xvQ~Z2qa@x1+XT5Zjr_G4IoxfCC
z^7A5L6?VxDKH;8T2kbUDmCu>N{^_7rEbB^!l!H=t4TBUlm|mB-dmc@&zp=pDNvocb
zJ?MztuER0Ynv8bY>?+dZZ*ngAS+c~%e1@QFiPR$3$|#Y`8@(3sZoI6q@bV`sp5;A8
zR%H`jw69pSdg0}3s~mY_ZReK7a~GBPmRN<!u2`PE`0`0<2j#n(R)1A|7f5c|p?dq}
z>J#!_fj^8~PloTEVz%Aca%tGJJfraZh0I%a*H1nFB2V0c)35RJ0_i!7=?5(f<YE}a
z52{{Z)@zO{V2xp|eIO;lGWX@>d#^M9CN%7oI52$&dtPBO3(rp3ziSR2PGIWUC0o5L
zkEh2td{!*`<UG;+CFNXa8Z)<_aw;{}+0XZ`L39JxwF9wjXEx27vxoE9-K@HdcT5+q
z<u$7w(BiDW?Bx8e*>(FJ$Jkc}ryrPgE7iZ4l4Jhl$Fk_l(roUJPQGUMIw2al{as+}
zr%B1o3%pL`v~a)S;q2L_m^;x_C0l((!ETc!p&N`-)cxA#9692!cS041xP+Jy&(cM#
z9<$0WJiIo2`PTyFU3Y$&mv)*Q{FvOi_)|IG8BQSVbZxM!Z?r>&2e~<9xIl18C!@g&
zvu|Pi{<@VV5t%pMR<6I)ar>M0(ks*NYA!Y0Zg1=L_}x}(FX4C0o4qE#Tg^Xp*`4`y
zfxF)An;JT+?Eb_~!^i(>onN-47wz`iJg@Ro{ku8o-{iE<RvT?yzU9Hmu<ezf3}-*m
zziWOoj$zXRt`O#0<t#_OD~z?uQVz-&o-dT#(h#=byz_2#`MPDN>#Gv~GaS4;ZT)oV
Q{mhCShFq$uuKsRZ0Q9$YZ2$lO

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
index 4434e93cbd..55ce577d4b 100644
--- a/spectec/src/backend-latex/render.ml
+++ b/spectec/src/backend-latex/render.ml
@@ -1276,7 +1276,7 @@ and render_exp env e =
       "%X"
     in "\\mathrm{U{+}" ^ Z.format fmt n ^ "}"
   | NumE (`AtomOp, `Nat n) ->
-    let atom = {it = Atom.Atom (Z.to_string n); at = e.at; note = Atom.info "nat"} in
+    let atom = Atom.Atom (Z.to_string n) $$ e.at % Atom.info "nat" in
     render_atom (without_macros true env) atom
   | NumE _ -> assert false
   | TextE t -> render_text t
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 9132687342..428b8537a8 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -25,7 +25,7 @@ type iter =
 and numtyp = Num.typ
 and optyp = [Bool.typ | Num.typ]
 
-and typ = typ' phrase
+and typ = typ' phrase  (* mark denotes closed normal forms up to struct/variant type names *)
 and typ' =
   | VarT of id * arg list        (* typid( arg* ) *)
   | BoolT                        (* `bool` *)
@@ -50,7 +50,7 @@ and unop = [Bool.unop | Num.unop]
 and binop = [Bool.binop | Num.binop]
 and cmpop = [Bool.cmpop | Num.cmpop]
 
-and exp = (exp', typ) note_phrase
+and exp = (exp', typ) note_phrase  (* mark denotes closed normal forms *)
 and exp' =
   | VarE of id                   (* varid *)
   | BoolE of bool                (* bool *)
@@ -111,7 +111,7 @@ and sym' =
 
 (* Definitions *)
 
-and arg = arg' phrase
+and arg = arg' phrase  (* mark denotes closed normal forms *)
 and arg' =
   | ExpA of exp                                       (* exp *)
   | TypA of typ                                       (* `syntax` typ *)
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index be9321624c..f70ce909cf 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -31,6 +31,17 @@ let snd3 (_, x, _) = x
 let unordered s1 s2 = not Set.(subset s1 s2 || subset s2 s1)
 
 
+let cnf x = x.mark <- true; x
+
+let cnf_if b e = if b then cnf e else e
+
+let cnf_if_prim e =
+  if e.mark then e else
+  match e.it with
+  | BoolE _ | NumE _ | TextE _ -> cnf e
+  | _ -> e
+
+
 let of_bool_exp = function
   | BoolE b -> Some b
   | _ -> None
@@ -80,12 +91,13 @@ let rec reduce_typ env t : typ =
     (fun _ -> fmt "%s" (il_typ t))
     (fun r -> fmt "%s" (il_typ r))
   ) @@ fun _ ->
+  if t.mark then t else
   match t.it with
   | VarT (id, args) ->
     let args' = List.map (reduce_arg env) args in
     (match reduce_typ_app' env id args' t.at (Env.find_opt_typ env id) with
     | Some {it = AliasT t'; _} -> reduce_typ env t'
-    | _ -> VarT (id, args') $ t.at
+    | _ -> VarT (id, args') $ t.at |> cnf_if (List.for_all Source.mark args')
     )
   | _ -> t
 
@@ -128,6 +140,7 @@ and reduce_typ_app' env id args at = function
 (* Expression Reduction *)
 
 and is_head_normal_exp e =
+  e.mark ||
   match e.it with
   | BoolE _ | NumE _ | TextE _
   | OptE _ | ListE _ | TupE _ | CaseE _ | StrE _ -> true
@@ -135,6 +148,7 @@ and is_head_normal_exp e =
   | _ -> false
 
 and is_normal_exp e =
+  e.mark ||
   match e.it with
   | BoolE _ | NumE _ | TextE _ -> true
   | ListE es | TupE es -> List.for_all is_normal_exp es
@@ -148,17 +162,19 @@ and reduce_exp env e : exp =
     (fun _ -> fmt "%s" (il_exp e))
     (fun e' -> fmt "%s" (il_exp e'))
   ) @@ fun _ ->
+  if e.mark then e else
   match e.it with
-  | VarE _ | BoolE _ | NumE _ | TextE _ -> e
+  | VarE _ -> e
+  | BoolE _ | NumE _ | TextE _ -> cnf e
   | UnE (op, ot, e1) ->
     let e1' = reduce_exp env e1 in
     (match op, e1'.it with
-    | #Bool.unop as op', BoolE b1 -> BoolE (Bool.un op' b1) $> e
+    | #Bool.unop as op', BoolE b1 -> BoolE (Bool.un op' b1) $> e |> cnf
     | #Num.unop as op', NumE n1 ->
       (match Num.un op' n1 with
-      | Some n -> NumE n
-      | None -> UnE (op, ot, e1')
-      ) $> e
+      | Some n -> NumE n $> e |> cnf
+      | None -> UnE (op, ot, e1') $> e
+      )
     | `NotOp, UnE (`NotOp, _, e11') -> e11'
     | `MinusOp, UnE (`MinusOp, _, e11') -> e11'
     | _ -> UnE (op, ot, e1') $> e
@@ -169,30 +185,30 @@ and reduce_exp env e : exp =
     (match op with
     | #Bool.binop as op' ->
       (match Bool.bin_partial op' e1'.it e2'.it of_bool_exp to_bool_exp with
-      | None -> BinE (op, ot, e1', e2')
-      | Some e' -> e'
+      | None -> BinE (op, ot, e1', e2') $> e
+      | Some e' -> e' $> e |> cnf_if_prim
       )
     | #Num.binop as op' ->
       (match Num.bin_partial op' e1'.it e2'.it of_num_exp to_num_exp with
-      | None -> BinE (op, ot, e1', e2')
-      | Some e' -> e'
+      | None -> BinE (op, ot, e1', e2') $> e
+      | Some e' -> e' $> e |> cnf_if_prim
       )
-    ) $> e
+    )
   | CmpE (op, ot, e1, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match op, e1'.it, e2'.it with
-    | `EqOp, _, _ when Eq.eq_exp e1' e2' -> BoolE true
-    | `NeOp, _, _ when Eq.eq_exp e1' e2' -> BoolE false
-    | `EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
-    | `NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true
+    | `EqOp, _, _ when Eq.eq_exp e1' e2' -> BoolE true $> e |> cnf
+    | `NeOp, _, _ when Eq.eq_exp e1' e2' -> BoolE false $> e |> cnf
+    | `EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false $> e |> cnf
+    | `NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true $> e |> cnf
     | #Num.cmpop as op', NumE n1, NumE n2 ->
       (match Num.cmp op' n1 n2 with
-      | Some b -> BoolE b
-      | None -> CmpE (op, ot, e1', e2')
+      | Some b -> BoolE b $> e |> cnf
+      | None -> CmpE (op, ot, e1', e2') $> e
       )
-    | _ -> CmpE (op, ot, e1', e2')
-    ) $> e
+    | _ -> CmpE (op, ot, e1', e2') $> e
+    )
   | IdxE (e1, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
@@ -206,9 +222,9 @@ and reduce_exp env e : exp =
     let e3' = reduce_exp env e3 in
     (match e1'.it, e2'.it, e3'.it with
     | ListE es, NumE (`Nat i), NumE (`Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
-      ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es))
-    | _ -> SliceE (e1', e2', e3')
-    ) $> e
+      ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es)) $> e |> cnf_if e1'.mark
+    | _ -> SliceE (e1', e2', e3') $> e
+    )
   | UpdE (e1, p, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
@@ -220,10 +236,12 @@ and reduce_exp env e : exp =
     reduce_path env e1' p
       (fun e' p' ->
         if p'.it = RootP
-        then reduce_exp env (CatE (e', e2') $> e')
+        then reduce_exp env (CatE (e', e2') $> e' |> cnf_if (e'.mark && e2'.mark))
         else ExtE (e', p', e2') $> e'
       )
-  | StrE efs -> StrE (List.map (reduce_expfield env) efs) $> e
+  | StrE efs ->
+    let efs' = List.map (reduce_expfield env) efs in
+    StrE efs' $> e |> cnf_if (List.for_all (fun (_, e') -> e'.mark) efs')
   | DotE (e1, atom) ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
@@ -235,16 +253,16 @@ and reduce_exp env e : exp =
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match e1'.it, e2'.it with
-    | ListE es1, ListE es2 -> ListE (es1 @ es2)
-    | OptE None, OptE _ -> e2'.it
-    | OptE _, OptE None -> e1'.it
+    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if (e1'.mark && e2'.mark)
+    | OptE None, OptE _ -> e2'
+    | OptE _, OptE None -> e1'
     | StrE efs1, StrE efs2 ->
       let merge (atom1, e1) (atom2, e2) =
         assert (Atom.eq atom1 atom2);
         (atom1, reduce_exp env (CompE (e1, e2) $> e1))
-      in StrE (List.map2 merge efs1 efs2)
-    | _ -> CompE (e1', e2')
-    ) $> e
+      in StrE (List.map2 merge efs1 efs2) $> e |> cnf_if (e1'.mark && e2'.mark)
+    | _ -> CompE (e1', e2') $> e
+    )
   | MemE (e1, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
@@ -256,14 +274,16 @@ and reduce_exp env e : exp =
     | ListE es2' when List.exists (Eq.eq_exp e1') es2' -> BoolE true
     | ListE es2' when is_normal_exp e1' && List.for_all is_normal_exp es2' -> BoolE false
     | _ -> MemE (e1', e2')
-    ) $> e
+    ) $> e |> cnf_if_prim
   | LenE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
-    | ListE es -> NumE (`Nat (Z.of_int (List.length es)))
-    | _ -> LenE e1'
-    ) $> e
-  | TupE es -> TupE (List.map (reduce_exp env) es) $> e
+    | ListE es -> NumE (`Nat (Z.of_int (List.length es))) $> e |> cnf
+    | _ -> LenE e1' $> e
+    )
+  | TupE es ->
+    let es' = List.map (reduce_exp env) es in
+    TupE es' $> e |> cnf_if (List.for_all Source.mark es')
   | CallE (id, args) ->
     let args' = List.map (reduce_arg env) args in
     let _ps, _t, clauses = Env.find_def env id in
@@ -284,7 +304,7 @@ and reduce_exp env e : exp =
       | Opt ->
         let eos' = List.map as_opt_exp es' in
         if List.for_all Option.is_none eos' then
-          OptE None $> e
+          OptE None $> e |> cnf
         else if List.for_all Option.is_some eos' then
           let es1' = List.map Option.get eos' in
           let s = List.fold_left2 Subst.add_varid Subst.empty ids es1' in
@@ -330,37 +350,43 @@ and reduce_exp env e : exp =
     | CaseE (_, e11') -> e11'
     | _ -> UncaseE (e1', mixop) $> e
     )
-  | OptE eo -> OptE (Option.map (reduce_exp env) eo) $> e
+  | OptE eo ->
+    let eo' = Option.map (reduce_exp env) eo in
+    OptE eo' $> e |> cnf_if (Lib.Option.for_all Source.mark eo')
   | TheE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
     | OptE (Some e11) -> e11
     | _ -> TheE e1' $> e
     )
-  | ListE es -> ListE (List.map (reduce_exp env) es) $> e
+  | ListE es -> 
+    let es' = List.map (reduce_exp env) es in
+    ListE es' $> e |> cnf_if (List.for_all Source.mark es')
   | LiftE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
-    | OptE None -> ListE []
-    | OptE (Some e11') -> ListE [e11']
-    | _ -> LiftE e1'
-    ) $> e
+    | OptE None -> ListE [] $> e |> cnf
+    | OptE (Some e11') -> ListE [e11'] $> e |> cnf_if e11'.mark
+    | _ -> LiftE e1' $> e
+    )
   | CatE (e1, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match e1'.it, e2'.it with
-    | ListE es1, ListE es2 -> ListE (es1 @ es2)
-    | OptE None, OptE _ -> e2'.it
-    | OptE _, OptE None -> e1'.it
-    | _ -> CatE (e1', e2')
-    ) $> e
-  | CaseE (op, e1) -> CaseE (op, reduce_exp env e1) $> e
+    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if (e1'.mark && e2'.mark)
+    | OptE None, OptE _ -> e2'
+    | OptE _, OptE None -> e1'
+    | _ -> CatE (e1', e2') $> e
+    )
+  | CaseE (op, e1) ->
+    let e1' = reduce_exp env e1 in
+    CaseE (op, e1') $> e |> cnf_if e1'.mark
   | CvtE (e1, _nt1, nt2) ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
     | NumE n ->
       (match Num.cvt nt2 n with
-      | Some n' -> NumE n' $> e
+      | Some n' -> NumE n' $> e |> cnf
       | None -> e1'
       )
     | _ -> e1'
@@ -389,7 +415,7 @@ and reduce_exp env e : exp =
             Some (s1', s2', eI'::res')
           ) (Some (Subst.empty, Subst.empty, [])) es' (List.combine ets1 ets2)
         with
-        | Some (_, _, res') -> TupE (List.rev res') $> e
+        | Some (_, _, res') -> TupE (List.rev res') $> e |> cnf_if (List.for_all Source.mark res')
         | None -> SubE (e1', t1', t2') $> e
         )
       | _ -> SubE (e1', t1', t2') $> e
@@ -451,8 +477,9 @@ and reduce_arg env a : arg =
     (fun _ -> fmt "%s" (il_arg a))
     (fun a' -> fmt "%s" (il_arg a'))
   ) @@ fun _ ->
+  if a.mark then a else
   match a.it with
-  | ExpA e -> ExpA (reduce_exp env e) $ a.at
+  | ExpA e -> let e' = reduce_exp env e in ExpA e' $ a.at |> cnf_if e'.mark
   | TypA _t -> a  (* types are reduced on demand *)
   | DefA _id -> a
   | GramA _g -> a
diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml
index 7e1bde0280..d4bff66b1c 100644
--- a/spectec/src/il/subst.ml
+++ b/spectec/src/il/subst.ml
@@ -95,6 +95,7 @@ let rec subst_iter s iter =
 (* Types *)
 
 and subst_typ s t =
+  if t.mark then t else
   (match t.it with
   | VarT (id, as_) ->
     (match Map.find_opt id.it s.typid with
@@ -130,6 +131,7 @@ and subst_typcase s (op, (bs, t, prems), hints) =
 (* Expressions *)
 
 and subst_exp s e =
+  if e.mark then e else
   (match e.it with
   | VarE id ->
     (match Map.find_opt id.it s.varid with
@@ -223,6 +225,7 @@ and subst_prem s prem =
 (* Definitions *)
 
 and subst_arg s a =
+  if a.mark then a else
   (match a.it with
   | ExpA e -> ExpA (subst_exp s e)
   | TypA t -> TypA (subst_typ s t)
diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml
index 98f7e3030e..f2fa33731a 100644
--- a/spectec/src/il2al/preprocess.ml
+++ b/spectec/src/il2al/preprocess.ml
@@ -12,7 +12,7 @@ let rec transform_rulepr_prem prem =
     prem
     |> transform_rulepr_prem
     |> (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
-  | IfPr ({ it = CmpE (`EqOp, _, { it = CallE (id, args); note; at }, rhs); _ })
+  | IfPr ({ it = CmpE (`EqOp, _, { it = CallE (id, args); note; at; _ }, rhs); _ })
   when List.mem id.it !typing_functions ->
     IfPr (CallE (id, args @ [ExpA rhs $ rhs.at]) $$ at % note) $ prem.at
   | _ -> prem
diff --git a/spectec/src/util/lib.ml b/spectec/src/util/lib.ml
index 351ed0a24c..87e1b36e63 100644
--- a/spectec/src/util/lib.ml
+++ b/spectec/src/util/lib.ml
@@ -1,3 +1,16 @@
+module Option =
+struct
+  include Option
+
+  let exists f = function
+    | None -> false
+    | Some e -> f e
+
+  let for_all f = function
+    | None -> true
+    | Some e -> f e
+end
+
 module List =
 struct
   include List
diff --git a/spectec/src/util/lib.mli b/spectec/src/util/lib.mli
index 56e29ffc52..fe1d834a74 100644
--- a/spectec/src/util/lib.mli
+++ b/spectec/src/util/lib.mli
@@ -1,5 +1,11 @@
 (* Things that should be in the OCaml library... *)
 
+module Option :
+sig
+  val exists : ('a -> bool) -> 'a option -> bool
+  val for_all : ('a -> bool) -> 'a option -> bool
+end
+
 module List :
 sig
   val take : int -> 'a list -> 'a list (* raises Failure *)
diff --git a/spectec/src/util/source.ml b/spectec/src/util/source.ml
index 58e72eec3f..ac88ed1de5 100644
--- a/spectec/src/util/source.ml
+++ b/spectec/src/util/source.ml
@@ -38,18 +38,20 @@ let string_of_region r =
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b}
+type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mutable mark : bool}
 type 'a phrase = ('a, unit) note_phrase
 
-let ($) it at = {it; at; note = ()}
-let ($$) it (at, note) = {it; at; note}
+let ($) it at = {it; at; note = (); mark = false}
+let ($$) it (at, note) = {it; at; note; mark = false}
 let (%) at note = (at, note)
 
-let it {it; _} = it
-let at {at; _} = at
-let note {note; _} = note
+let it phrase = phrase.it
+let at phrase = phrase.at
+let note phrase = phrase.note
+let mark phrase = phrase.mark
+let set_mark phrase b = phrase.mark <- b
 
 
 (* Utilities *)
 
-let map f {it; at; note} = {it = f it; at; note}
+let map f {it; at; note; mark} = {it = f it; at; note; mark}
diff --git a/spectec/src/util/source.mli b/spectec/src/util/source.mli
index dd3fb44334..2dc5d53514 100644
--- a/spectec/src/util/source.mli
+++ b/spectec/src/util/source.mli
@@ -18,7 +18,7 @@ val string_of_region : region -> string
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b}
+type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mutable mark : bool}
 type 'a phrase = ('a, unit) note_phrase
 
 val ($) : 'a -> region -> 'a phrase
@@ -28,6 +28,8 @@ val (%) : region -> 'b -> region * 'b
 val it : ('a, 'b) note_phrase -> 'a
 val at : ('a, 'b) note_phrase -> region
 val note : ('a, 'b) note_phrase -> 'b
+val mark : ('a, 'b) note_phrase -> bool
+val set_mark : ('a, 'b) note_phrase -> bool -> unit
 
 
 (* Utilities *)

From fa71348f30c2a6b0983c89cc7d95768c1a5995de Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 18 Nov 2025 12:45:51 +0100
Subject: [PATCH 2/4] Immutable marks

---
 spectec/src/il/eval.ml      | 2 +-
 spectec/src/util/source.ml  | 3 +--
 spectec/src/util/source.mli | 3 +--
 3 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index f70ce909cf..e073e9ef2f 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -31,7 +31,7 @@ let snd3 (_, x, _) = x
 let unordered s1 s2 = not Set.(subset s1 s2 || subset s2 s1)
 
 
-let cnf x = x.mark <- true; x
+let cnf x = {x with mark = true}
 
 let cnf_if b e = if b then cnf e else e
 
diff --git a/spectec/src/util/source.ml b/spectec/src/util/source.ml
index ac88ed1de5..3181c72dd7 100644
--- a/spectec/src/util/source.ml
+++ b/spectec/src/util/source.ml
@@ -38,7 +38,7 @@ let string_of_region r =
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mutable mark : bool}
+type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mark : bool}
 type 'a phrase = ('a, unit) note_phrase
 
 let ($) it at = {it; at; note = (); mark = false}
@@ -49,7 +49,6 @@ let it phrase = phrase.it
 let at phrase = phrase.at
 let note phrase = phrase.note
 let mark phrase = phrase.mark
-let set_mark phrase b = phrase.mark <- b
 
 
 (* Utilities *)
diff --git a/spectec/src/util/source.mli b/spectec/src/util/source.mli
index 2dc5d53514..b317c6b3c7 100644
--- a/spectec/src/util/source.mli
+++ b/spectec/src/util/source.mli
@@ -18,7 +18,7 @@ val string_of_region : region -> string
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mutable mark : bool}
+type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b; mark : bool}
 type 'a phrase = ('a, unit) note_phrase
 
 val ($) : 'a -> region -> 'a phrase
@@ -29,7 +29,6 @@ val it : ('a, 'b) note_phrase -> 'a
 val at : ('a, 'b) note_phrase -> region
 val note : ('a, 'b) note_phrase -> 'b
 val mark : ('a, 'b) note_phrase -> bool
-val set_mark : ('a, 'b) note_phrase -> bool -> unit
 
 
 (* Utilities *)

From 1d300cc80d3808e25913dfdd5437b42704bb4973 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 18 Nov 2025 12:58:11 +0100
Subject: [PATCH 3/4] Simplify mark propagation

---
 spectec/src/il/eval.ml   | 42 +++++++++++++++++++++-------------------
 spectec/src/util/lib.ml  | 13 -------------
 spectec/src/util/lib.mli |  6 ------
 3 files changed, 22 insertions(+), 39 deletions(-)

diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index e073e9ef2f..0eeff2c58e 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -31,9 +31,11 @@ let snd3 (_, x, _) = x
 let unordered s1 s2 = not Set.(subset s1 s2 || subset s2 s1)
 
 
+let is_cnf x = x.mark
+
 let cnf x = {x with mark = true}
 
-let cnf_if b e = if b then cnf e else e
+let cnf_if xs x = if List.for_all is_cnf xs then cnf x else x
 
 let cnf_if_prim e =
   if e.mark then e else
@@ -91,13 +93,13 @@ let rec reduce_typ env t : typ =
     (fun _ -> fmt "%s" (il_typ t))
     (fun r -> fmt "%s" (il_typ r))
   ) @@ fun _ ->
-  if t.mark then t else
+  if is_cnf t then t else
   match t.it with
   | VarT (id, args) ->
     let args' = List.map (reduce_arg env) args in
     (match reduce_typ_app' env id args' t.at (Env.find_opt_typ env id) with
     | Some {it = AliasT t'; _} -> reduce_typ env t'
-    | _ -> VarT (id, args') $ t.at |> cnf_if (List.for_all Source.mark args')
+    | _ -> VarT (id, args') $ t.at |> cnf_if args'
     )
   | _ -> t
 
@@ -140,7 +142,7 @@ and reduce_typ_app' env id args at = function
 (* Expression Reduction *)
 
 and is_head_normal_exp e =
-  e.mark ||
+  is_cnf e ||
   match e.it with
   | BoolE _ | NumE _ | TextE _
   | OptE _ | ListE _ | TupE _ | CaseE _ | StrE _ -> true
@@ -148,7 +150,7 @@ and is_head_normal_exp e =
   | _ -> false
 
 and is_normal_exp e =
-  e.mark ||
+  is_cnf e ||
   match e.it with
   | BoolE _ | NumE _ | TextE _ -> true
   | ListE es | TupE es -> List.for_all is_normal_exp es
@@ -162,7 +164,7 @@ and reduce_exp env e : exp =
     (fun _ -> fmt "%s" (il_exp e))
     (fun e' -> fmt "%s" (il_exp e'))
   ) @@ fun _ ->
-  if e.mark then e else
+  if is_cnf e then e else
   match e.it with
   | VarE _ -> e
   | BoolE _ | NumE _ | TextE _ -> cnf e
@@ -222,7 +224,7 @@ and reduce_exp env e : exp =
     let e3' = reduce_exp env e3 in
     (match e1'.it, e2'.it, e3'.it with
     | ListE es, NumE (`Nat i), NumE (`Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
-      ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es)) $> e |> cnf_if e1'.mark
+      ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es)) $> e |> cnf_if [e1']
     | _ -> SliceE (e1', e2', e3') $> e
     )
   | UpdE (e1, p, e2) ->
@@ -236,12 +238,12 @@ and reduce_exp env e : exp =
     reduce_path env e1' p
       (fun e' p' ->
         if p'.it = RootP
-        then reduce_exp env (CatE (e', e2') $> e' |> cnf_if (e'.mark && e2'.mark))
+        then reduce_exp env (CatE (e', e2') $> e' |> cnf_if [e'; e2'])
         else ExtE (e', p', e2') $> e'
       )
   | StrE efs ->
     let efs' = List.map (reduce_expfield env) efs in
-    StrE efs' $> e |> cnf_if (List.for_all (fun (_, e') -> e'.mark) efs')
+    StrE efs' $> e |> cnf_if (List.map snd efs')
   | DotE (e1, atom) ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
@@ -253,14 +255,14 @@ and reduce_exp env e : exp =
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match e1'.it, e2'.it with
-    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if (e1'.mark && e2'.mark)
+    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if [e1'; e2']
     | OptE None, OptE _ -> e2'
     | OptE _, OptE None -> e1'
     | StrE efs1, StrE efs2 ->
       let merge (atom1, e1) (atom2, e2) =
         assert (Atom.eq atom1 atom2);
         (atom1, reduce_exp env (CompE (e1, e2) $> e1))
-      in StrE (List.map2 merge efs1 efs2) $> e |> cnf_if (e1'.mark && e2'.mark)
+      in StrE (List.map2 merge efs1 efs2) $> e |> cnf_if [e1'; e2']
     | _ -> CompE (e1', e2') $> e
     )
   | MemE (e1, e2) ->
@@ -283,7 +285,7 @@ and reduce_exp env e : exp =
     )
   | TupE es ->
     let es' = List.map (reduce_exp env) es in
-    TupE es' $> e |> cnf_if (List.for_all Source.mark es')
+    TupE es' $> e |> cnf_if es'
   | CallE (id, args) ->
     let args' = List.map (reduce_arg env) args in
     let _ps, _t, clauses = Env.find_def env id in
@@ -352,7 +354,7 @@ and reduce_exp env e : exp =
     )
   | OptE eo ->
     let eo' = Option.map (reduce_exp env) eo in
-    OptE eo' $> e |> cnf_if (Lib.Option.for_all Source.mark eo')
+    OptE eo' $> e |> cnf_if (Option.to_list eo')
   | TheE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
@@ -361,26 +363,26 @@ and reduce_exp env e : exp =
     )
   | ListE es -> 
     let es' = List.map (reduce_exp env) es in
-    ListE es' $> e |> cnf_if (List.for_all Source.mark es')
+    ListE es' $> e |> cnf_if es'
   | LiftE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
     | OptE None -> ListE [] $> e |> cnf
-    | OptE (Some e11') -> ListE [e11'] $> e |> cnf_if e11'.mark
+    | OptE (Some e11') -> ListE [e11'] $> e |> cnf_if [e11']
     | _ -> LiftE e1' $> e
     )
   | CatE (e1, e2) ->
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match e1'.it, e2'.it with
-    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if (e1'.mark && e2'.mark)
+    | ListE es1, ListE es2 -> ListE (es1 @ es2) $> e |> cnf_if [e1'; e2']
     | OptE None, OptE _ -> e2'
     | OptE _, OptE None -> e1'
     | _ -> CatE (e1', e2') $> e
     )
   | CaseE (op, e1) ->
     let e1' = reduce_exp env e1 in
-    CaseE (op, e1') $> e |> cnf_if e1'.mark
+    CaseE (op, e1') $> e |> cnf_if [e1']
   | CvtE (e1, _nt1, nt2) ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
@@ -415,7 +417,7 @@ and reduce_exp env e : exp =
             Some (s1', s2', eI'::res')
           ) (Some (Subst.empty, Subst.empty, [])) es' (List.combine ets1 ets2)
         with
-        | Some (_, _, res') -> TupE (List.rev res') $> e |> cnf_if (List.for_all Source.mark res')
+        | Some (_, _, res') -> TupE (List.rev res') $> e |> cnf_if res'
         | None -> SubE (e1', t1', t2') $> e
         )
       | _ -> SubE (e1', t1', t2') $> e
@@ -477,9 +479,9 @@ and reduce_arg env a : arg =
     (fun _ -> fmt "%s" (il_arg a))
     (fun a' -> fmt "%s" (il_arg a'))
   ) @@ fun _ ->
-  if a.mark then a else
+  if is_cnf a then a else
   match a.it with
-  | ExpA e -> let e' = reduce_exp env e in ExpA e' $ a.at |> cnf_if e'.mark
+  | ExpA e -> let e' = reduce_exp env e in ExpA e' $ a.at |> cnf_if [e']
   | TypA _t -> a  (* types are reduced on demand *)
   | DefA _id -> a
   | GramA _g -> a
diff --git a/spectec/src/util/lib.ml b/spectec/src/util/lib.ml
index 87e1b36e63..351ed0a24c 100644
--- a/spectec/src/util/lib.ml
+++ b/spectec/src/util/lib.ml
@@ -1,16 +1,3 @@
-module Option =
-struct
-  include Option
-
-  let exists f = function
-    | None -> false
-    | Some e -> f e
-
-  let for_all f = function
-    | None -> true
-    | Some e -> f e
-end
-
 module List =
 struct
   include List
diff --git a/spectec/src/util/lib.mli b/spectec/src/util/lib.mli
index fe1d834a74..56e29ffc52 100644
--- a/spectec/src/util/lib.mli
+++ b/spectec/src/util/lib.mli
@@ -1,11 +1,5 @@
 (* Things that should be in the OCaml library... *)
 
-module Option :
-sig
-  val exists : ('a -> bool) -> 'a option -> bool
-  val for_all : ('a -> bool) -> 'a option -> bool
-end
-
 module List :
 sig
   val take : int -> 'a list -> 'a list (* raises Failure *)

From 9c7ef4aa564648122767c62fee6824b4eb7fc8ce Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 18 Nov 2025 14:36:27 +0100
Subject: [PATCH 4/4] Update

---
 spectec/doc/example/output/NanoWasm.pdf | Bin 245572 -> 245572 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index e1a6afd34bf4e407e8fad4ada8e3289451e54cba..07a992ef5040b0e2ba045fe362d98480664ff442 100644
GIT binary patch
delta 112
zcmX@|kMGDozJ?aY7N#xCAzN9E4U7ydr$=sOmV+?2*KB1jWOFt!aJF=EHgGaAb8|Jd
iFg3MsGcYi*v~Y8AH8Hj{c6GB;upy*myTKl25oQ2oz#dWn

delta 112
zcmX@|kMGDozJ?aY7N#xCAzN9EjE#&9rbljNmV+?2*KB1jWOFt$aW*zHFfeyBbTc(`
iay4^uF*Y%Ebu@IebTf9bbal2<upy*myTKl25oQ2m&>m_4