Wasm-DSL · DCupello1 · Sep 30, 2025 · Oct 1, 2025 · Oct 3, 2025 · Oct 3, 2025
diff --git a/specification/wasm-2.0/1-syntax.spectec b/specification/wasm-2.0/1-syntax.spectec
@@ -150,7 +150,7 @@ syntax resulttype hint(desc "result type") =
 syntax packtype hint(desc "packed type") = I8 | I16
 syntax lanetype hint(desc "lane type") = numtype | packtype
 
-syntax Pnn hint(show I#n) = I8 | I16
+syntax Pnn hint(show I#n) = packtype
 syntax Jnn hint(show I#n) = Inn | Pnn
 syntax Lnn hint(show I#n) = Inn | Fnn | Pnn
 

diff --git a/specification/wasm-3.0/1.2-syntax.types.spectec b/specification/wasm-3.0/1.2-syntax.types.spectec
@@ -52,7 +52,7 @@ syntax valtype/sem =
   | ... | BOT
 
 
-syntax Inn hint(show I#N) hint(macro "nt%") = I32 | I64
+syntax Inn hint(show I#N) hint(macro "nt%") = addrtype
 syntax Fnn hint(show F#N) hint(macro "nt%") = F32 | F64
 syntax Vnn hint(show V#N) hint(macro "nt%") = V128
 syntax Cnn hint(show t) = Inn | Fnn | Vnn

diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
@@ -179,7 +179,7 @@ and check_type ty v expr =
     boolV (ty = "val")
   (* numtype *)
   | CaseV (nt, []) when List.mem nt inn_types ->
-    boolV (ty = "Inn" || ty = "Jnn" || ty = "numtype" || ty = "valtype" || ty = "consttype")
+    boolV (ty = "Inn" || ty = "Jnn" || ty = "numtype" || ty = "valtype" || ty = "consttype" || ty = "addrtype")
   | CaseV (nt, []) when List.mem nt fnn_types ->
     boolV (ty = "Fnn" || ty = "numtype" || ty = "valtype" || ty = "consttype")
   | CaseV (vt, []) when List.mem vt vnn_types ->

diff --git a/spectec/src/exe-spectec/main.ml b/spectec/src/exe-spectec/main.ml
@@ -19,6 +19,7 @@ type pass =
   | Totalize
   | Unthe
   | Sideconditions
+  | TypeFamilyRemoval
 
 (* This list declares the intended order of passes.
 
@@ -27,7 +28,7 @@ passers (--all-passes, some targets), we do _not_ want to use the order of
 flags on the command line.
 *)
 let _skip_passes = [ Sub; Unthe ]  (* Not clear how to extend them to indexed types *)
-let all_passes = [ Totalize; Sideconditions ]
+let all_passes = [ TypeFamilyRemoval; Totalize; Sideconditions; ]
 
 type file_kind =
   | Spec
@@ -73,18 +74,21 @@ let pass_flag = function
   | Totalize -> "totalize"
   | Unthe -> "the-elimination"
   | Sideconditions -> "sideconditions"
+  | TypeFamilyRemoval -> "typefamily-removal"
 
 let pass_desc = function
   | Sub -> "Synthesize explicit subtype coercions"
   | Totalize -> "Run function totalization"
   | Unthe -> "Eliminate the ! operator in relations"
   | Sideconditions -> "Infer side conditions"
+  | TypeFamilyRemoval -> "Transform Type families into sum types"
 
 let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | Sub -> Middlend.Sub.transform
   | Totalize -> Middlend.Totalize.transform
   | Unthe -> Middlend.Unthe.transform
   | Sideconditions -> Middlend.Sideconditions.transform
+  | TypeFamilyRemoval -> Middlend.Typefamilyremoval.transform
 
 
 (* Argument parsing *)

diff --git a/spectec/src/middlend/dune b/spectec/src/middlend/dune
@@ -6,5 +6,6 @@
     totalize
     unthe
     sideconditions
+    typefamilyremoval
   )
 )
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
@@ -214,7 +214,7 @@ let rec t_def' env = function
         | ExpP (_, typI) ->
           let x = ("x" ^ string_of_int i) $ no_region in
           [ExpB (x, typI) $ x.at], ExpA (VarE x $$ no_region % typI) $ no_region
-        | TypP id -> [], TypA (VarT (id, []) $ no_region) $ no_region
+        | TypP id -> [TypB id $ no_region], TypA (VarT (id, []) $ no_region) $ no_region
         | DefP (id, _, _) -> [], DefA id $ no_region
         | GramP (id, _) -> [], GramA (VarG (id, []) $ no_region) $ no_region
         ) params' |> List.split in