Fix module typing rules for 1.0 and 2.0

spectec/spec/wasm-1.0/2-syntax-aux.watsup

@@ -14,6 +14,32 @@ def $size(F32) = 32
 def $size(F64) = 64
 
 
+;; Projections
+
+;; TODO: use built-in notation
+def $funcsxt(externtype*) : functype*      hint(show $funcs(%))
+def $globalsxt(externtype*) : globaltype*  hint(show $globals(%))
+def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))
+def $memsxt(externtype*) : memtype*        hint(show $mems(%))
+
+def $funcsxt(eps) = eps
+def $funcsxt((FUNC ft) xt*) = ft $funcsxt(xt*)
+def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
+
+def $globalsxt(eps) = eps
+def $globalsxt((GLOBAL gt) xt*) = gt $globalsxt(xt*)
+def $globalsxt(externtype xt*) = $globalsxt(xt*)  -- otherwise
+
+def $tablesxt(eps) = eps
+def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*)
+def $tablesxt(externtype xt*) = $tablesxt(xt*)  -- otherwise
+
+def $memsxt(eps) = eps
+def $memsxt((MEM mt) xt*) = mt $memsxt(xt*)
+def $memsxt(externtype xt*) = $memsxt(xt*)  -- otherwise
+
+
+
 ;;
 ;; Auxiliary definitions on Instructions
 ;;

spectec/spec/wasm-1.0/6-typing.watsup

@@ -410,19 +410,28 @@ relation Module_ok: |- module : OK      hint(show "T-module")
 
 rule Module_ok:
   |- MODULE type* import* func* global* table* mem* elem* data* start? export* : OK
-  ;; TODO: incremental contexts for globals
-  -- if C = {TYPE ft'*, FUNC ft*, GLOBAL gt*, TABLE tt*, MEM mt*}
-
   -- (Type_ok: |- type : ft')*
+  -- (Import_ok: {TYPE ft'*} |- import : ixt)*
+
+  -- (Global_ok: C' |- global : gt)*
   -- (Func_ok: C |- func : ft)*
-  -- (Global_ok: C |- global : gt)*
   -- (Table_ok: C |- table : tt)*
   -- (Mem_ok: C |- mem : mt)*
 
   -- (Elem_ok: C |- elem : OK)*
   -- (Data_ok: C |- data : OK)*
   -- (Start_ok: C |- start : OK)?
+  -- (Export_ok: C |- export : xt)*
 
   -- if |tt*| <= 1
   -- if |mt*| <= 1
   ;; -- TODO: disjoint export names
+
+  -- if C = {TYPE ft'*, FUNC ift* ft*, GLOBAL igt* gt*, TABLE itt* tt*, MEM imt* mt*}
+
+  -- if C' = {TYPE ft'*, FUNC ift* ft*, GLOBAL igt*}
+
+  -- if ift* = $funcsxt(ixt*)
+  -- if igt* = $globalsxt(ixt*)
+  -- if itt* = $tablesxt(ixt*)
+  -- if imt* = $memsxt(ixt*)

spectec/spec/wasm-2.0/2-syntax-aux.watsup

@@ -55,6 +55,32 @@ def $dim(lnn X N) = N
 def $shsize(lnn X N) = $($lsize(lnn) * N)
 
 
+;; Projections
+
+;; TODO: use built-in notation
+def $funcsxt(externtype*) : functype*      hint(show $funcs(%))
+def $globalsxt(externtype*) : globaltype*  hint(show $globals(%))
+def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))
+def $memsxt(externtype*) : memtype*        hint(show $mems(%))
+
+def $funcsxt(eps) = eps
+def $funcsxt((FUNC ft) xt*) = ft $funcsxt(xt*)
+def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
+
+def $globalsxt(eps) = eps
+def $globalsxt((GLOBAL gt) xt*) = gt $globalsxt(xt*)
+def $globalsxt(externtype xt*) = $globalsxt(xt*)  -- otherwise
+
+def $tablesxt(eps) = eps
+def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*)
+def $tablesxt(externtype xt*) = $tablesxt(xt*)  -- otherwise
+
+def $memsxt(eps) = eps
+def $memsxt((MEM mt) xt*) = mt $memsxt(xt*)
+def $memsxt(externtype xt*) = $memsxt(xt*)  -- otherwise
+
+
+
 ;;
 ;; Auxiliary definitions on Indices
 ;;

spectec/spec/wasm-2.0/6-typing.watsup

@@ -650,20 +650,31 @@ rule Externidx_ok/mem:
 
 relation Module_ok: |- module : OK      hint(show "T-module")
 
+;; TODO: refs
 rule Module_ok:
   |- MODULE type* import* func* global* table* mem* elem* data^n start? export* : OK
-  ;; TODO: incremental contexts for globals
-  -- if C = {TYPE ft'*, FUNC ft*, GLOBAL gt*, TABLE tt*, MEM mt*, ELEM rt*, DATA OK^n}
-
   -- (Type_ok: |- type : ft')*
-  -- (Func_ok: C |- func : ft)*
-  -- (Global_ok: C |- global : gt)*
-  -- (Table_ok: C |- table : tt)*
-  -- (Mem_ok: C |- mem : mt)*
+  -- (Import_ok: {TYPE ft'*} |- import : ixt)*
+
+  -- (Global_ok: C' |- global : gt)*
+  -- (Table_ok: C' |- table : tt)*
+  -- (Mem_ok: C' |- mem : mt)*
+
+  -- (Elem_ok: C' |- elem : rt)*
+  -- (Data_ok: C' |- data : OK)^n
 
-  -- (Elem_ok: C |- elem : rt)*
-  -- (Data_ok: C |- data : OK)^n
+  -- (Func_ok: C |- func : ft)*
   -- (Start_ok: C |- start : OK)?
+  -- (Export_ok: C |- export : xt)*
 
   -- if |mt*| <= 1
   ;; -- TODO: disjoint export names
+
+  -- if C = {TYPE ft'*, FUNC ift* ft*, GLOBAL igt* gt*, TABLE itt* tt*, MEM imt* mt*, ELEM rt*, DATA OK^n}
+
+  -- if C' = {TYPE ft'*, FUNC ift* ft*, GLOBAL igt*, TABLE itt* tt*, MEM imt* mt*}
+
+  -- if ift* = $funcsxt(ixt*)
+  -- if igt* = $globalsxt(ixt*)
+  -- if itt* = $tablesxt(ixt*)
+  -- if imt* = $memsxt(ixt*)

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -227,7 +227,6 @@ var t : valtype
 ;; var bt : blocktype  ;; defined below
 var ct : comptype
 var dt : deftype
-var et : externtype
 var ft : functype
 var gt : globaltype
 var ht : heaptype

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -255,20 +255,21 @@ def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))
 def $memsxt(externtype*) : memtype*        hint(show $mems(%))
 
 def $funcsxt(eps) = eps
-def $funcsxt((FUNC dt) et*) = dt $funcsxt(et*)
-def $funcsxt(externtype et*) = $funcsxt(et*)  -- otherwise
+def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*)
+def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
 
 def $globalsxt(eps) = eps
-def $globalsxt((GLOBAL gt) et*) = gt $globalsxt(et*)
-def $globalsxt(externtype et*) = $globalsxt(et*)  -- otherwise
+def $globalsxt((GLOBAL gt) xt*) = gt $globalsxt(xt*)
+def $globalsxt(externtype xt*) = $globalsxt(xt*)  -- otherwise
 
 def $tablesxt(eps) = eps
-def $tablesxt((TABLE tt) et*) = tt $tablesxt(et*)
-def $tablesxt(externtype et*) = $tablesxt(et*)  -- otherwise
+def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*)
+def $tablesxt(externtype xt*) = $tablesxt(xt*)  -- otherwise
 
 def $memsxt(eps) = eps
-def $memsxt((MEM mt) et*) = mt $memsxt(et*)
-def $memsxt(externtype et*) = $memsxt(et*)  -- otherwise
+def $memsxt((MEM mt) xt*) = mt $memsxt(xt*)
+def $memsxt(externtype xt*) = $memsxt(xt*)  -- otherwise
+
 
 
 ;;

spectec/spec/wasm-3.0/6-typing.watsup

@@ -1228,12 +1228,6 @@ relation Module_ok: |- module : OK                    hint(show "T-module")
 relation Types_ok: context |- type* : deftype*        hint(show "T-types")
 relation Globals_ok: context |- global* : globaltype* hint(show "T-globals")
 
-var ixt : externtype
-var idt : deftype
-var igt : globaltype
-var itt : tabletype
-var imt : memtype
-
 ;; TODO: refs
 rule Module_ok:
   |- MODULE type* import* func* global* table* mem* elem* data^n start? export* : OK
@@ -1248,7 +1242,7 @@ rule Module_ok:
   -- (Elem_ok: C |- elem : rt)*
   -- (Data_ok: C |- data : OK)^n
   -- (Start_ok: C |- start : OK)?
-  -- (Export_ok: C |- export : et)*
+  -- (Export_ok: C |- export : xt)*
   ;; -- TODO: disjoint export names
 
   -- if C = {TYPE dt'*, FUNC idt* dt*, GLOBAL igt* gt*, TABLE itt* tt*, MEM imt* mt*, ELEM rt*, DATA OK^n}

spectec/src/il/print.ml

@@ -224,7 +224,7 @@ and string_of_path p =
     string_of_path p1 ^ "." ^ string_of_mixop [[atom]] ^ "_" ^ string_of_typ p1.note
 
 and string_of_iterexp (iter, bs) =
-  string_of_iter iter ^ "{" ^ String.concat " "
+  string_of_iter iter ^ "{" ^ String.concat ", "
     (List.map (fun (id, t) -> id.it ^ " : " ^ string_of_typ t) bs) ^ "}"