From ac72738d53a6f58e41069f5130520fc03fe77d3b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 27 Mar 2024 11:19:46 +0100 Subject: [PATCH] More todos --- spectec/spec/wasm-1.0/A-binary.watsup | 4 +- spectec/spec/wasm-2.0/A-binary.watsup | 6 +- spectec/spec/wasm-3.0/1-syntax.watsup | 8 +- spectec/spec/wasm-3.0/2-syntax-aux.watsup | 2 + spectec/spec/wasm-3.0/6-typing.watsup | 12 +- spectec/spec/wasm-3.0/8-reduction.watsup | 14 +- spectec/spec/wasm-3.0/A-binary.watsup | 13 +- spectec/src/backend-interpreter/construct.ml | 29 +- spectec/src/backend-interpreter/ds.ml | 5 +- spectec/src/frontend/elab.ml | 9 +- spectec/test-frontend/TEST.md | 174 ++-- spectec/test-latex/TEST.md | 35 +- spectec/test-middlend/TEST.md | 870 +++++++++---------- spectec/test-prose/TEST.md | 22 +- spectec/test-splice/TEST.md | 2 +- 15 files changed, 611 insertions(+), 594 deletions(-) diff --git a/spectec/spec/wasm-1.0/A-binary.watsup b/spectec/spec/wasm-1.0/A-binary.watsup index 2d9c4e1736..92559760d8 100644 --- a/spectec/spec/wasm-1.0/A-binary.watsup +++ b/spectec/spec/wasm-1.0/A-binary.watsup @@ -211,8 +211,8 @@ grammar Binstr/memory : instr = ... grammar Binstr/numeric-const : instr = ... | 0x41 n:Bu32 => CONST I32 n | 0x42 n:Bu64 => CONST I64 n -;; | 0x43 p:Bf32 => CONST F32 p ;; TODO -;; | 0x44 p:Bf64 => CONST F64 p ;; TODO + | 0x43 p:Bf32 => CONST F32 p + | 0x44 p:Bf64 => CONST F64 p | ... grammar Binstr/numeric-test-i32 : instr = ... diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup index 22f191fb6f..8f5c0a7a96 100644 --- a/spectec/spec/wasm-2.0/A-binary.watsup +++ b/spectec/spec/wasm-2.0/A-binary.watsup @@ -182,7 +182,7 @@ grammar Binstr/reference : instr = ... grammar Binstr/parametric : instr = ... | 0x1A => DROP | 0x1B => SELECT eps -;; | 0x1C t*:Bvec(Bvaltype) => SELECT (t*) TODO + | 0x1C ts:Bvec(Bvaltype) => SELECT ts | ... @@ -255,8 +255,8 @@ grammar Binstr/memory : instr = ... grammar Binstr/numeric-const : instr = ... | 0x41 n:Bu32 => CONST I32 n | 0x42 n:Bu64 => CONST I64 n -;; | 0x43 p:Bf32 => CONST F32 p ;; TODO -;; | 0x44 p:Bf64 => CONST F64 p ;; TODO + | 0x43 p:Bf32 => CONST F32 p + | 0x44 p:Bf64 => CONST F64 p | ... grammar Binstr/numeric-test-i32 : instr = ... diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup index 1451a066e1..551ebfb924 100644 --- a/spectec/spec/wasm-3.0/1-syntax.watsup +++ b/spectec/spec/wasm-3.0/1-syntax.watsup @@ -221,7 +221,7 @@ syntax elemtype hint(desc "element type") = syntax datatype hint(desc "data type") = OK syntax externtype hint(desc "external type") = - | FUNC deftype | GLOBAL globaltype | TABLE tabletype | MEM memtype + | FUNC typeuse | GLOBAL globaltype | TABLE tabletype | MEM memtype ;; Meta variables @@ -250,8 +250,6 @@ var xt : externtype var yt : fieldtype ;; TODO: better choice? var zt : storagetype -var tu : typeuse - ;; ;; Operators @@ -436,11 +434,11 @@ syntax instr/br hint(desc "branch instruction") = ... syntax instr/call hint(desc "function instruction") = ... | CALL funcidx | CALL_REF typeuse - | CALL_INDIRECT tableidx typeidx + | CALL_INDIRECT tableidx typeuse | RETURN | RETURN_CALL funcidx | RETURN_CALL_REF typeuse - | RETURN_CALL_INDIRECT tableidx typeidx + | RETURN_CALL_INDIRECT tableidx typeuse | ... syntax instr/num hint(desc "numeric instruction") = ... diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup index ecc8858e6b..1e9a8d23ff 100644 --- a/spectec/spec/wasm-3.0/2-syntax-aux.watsup +++ b/spectec/spec/wasm-3.0/2-syntax-aux.watsup @@ -129,6 +129,8 @@ def $diffrt((REF nul_1 ht_1), (REF eps ht_2)) = (REF nul_1 ht_1) syntax typevar = _IDX typeidx | REC nat var xx : typevar +var yy : typeuse hint(show y) +var tu : typeuse def $idx(typeidx) : typevar hint(show %) def $idx(x) = _IDX x diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup index 6f34d98ba5..99d53cd661 100644 --- a/spectec/spec/wasm-3.0/6-typing.watsup +++ b/spectec/spec/wasm-3.0/6-typing.watsup @@ -328,8 +328,8 @@ rule Heaptype_sub/typeidx-r: -- Heaptype_sub: C |- heaptype <: C.TYPES[typeidx] rule Heaptype_sub/rec: - C |- REC i <: tu - -- if C.REC[i] = SUB fin (tu_1* tu tu_2*) ct + C |- REC i <: yy + -- if C.REC[i] = SUB fin (yy_1* yy yy_2*) ct rule Heaptype_sub/none: C |- NONE <: heaptype @@ -440,8 +440,8 @@ rule Deftype_sub/refl: rule Deftype_sub/super: C |- deftype_1 <: deftype_2 - -- if $unrolldt(deftype_1) = SUB fin (tu_1* tu tu_2*) ct - -- Heaptype_sub: C |- tu <: deftype_2 + -- if $unrolldt(deftype_1) = SUB fin (yy_1* yy yy_2*) ct + -- Heaptype_sub: C |- yy <: deftype_2 ;; External types @@ -649,7 +649,7 @@ rule Instr_ok/call_ref: -- Expand: C.TYPES[x] ~~ FUNC (t_1* -> t_2*) rule Instr_ok/call_indirect: - C |- CALL_INDIRECT x y : t_1* I32 -> t_2* + C |- CALL_INDIRECT x $idx(y) : t_1* I32 -> t_2* -- if C.TABLES[x] = lim rt -- Reftype_sub: C |- rt <: (REF NULL FUNC) -- Expand: C.TYPES[y] ~~ FUNC (t_1* -> t_2*) @@ -677,7 +677,7 @@ rule Instr_ok/return_call_ref: ;; TODO: enable t_2* <: C.RETURN rule Instr_ok/return_call_indirect: - C |- RETURN_CALL_INDIRECT x y : t_3* t_1* I32 -> t_4* + C |- RETURN_CALL_INDIRECT x $idx(y) : t_3* t_1* I32 -> t_4* -- if C.TABLES[x] = lim rt -- Reftype_sub: C |- rt <: (REF NULL FUNC) diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup index 49b128932a..5ace0e5924 100644 --- a/spectec/spec/wasm-3.0/8-reduction.watsup +++ b/spectec/spec/wasm-3.0/8-reduction.watsup @@ -161,10 +161,10 @@ rule Step_read/call: -- if $funcaddr(z)[x] = a rule Step_read/call_ref-null: - z; (REF.NULL ht) (CALL_REF tu) ~> TRAP + z; (REF.NULL ht) (CALL_REF yy) ~> TRAP rule Step_read/call_ref-func: - z; val^n (REF.FUNC_ADDR a) (CALL_REF tu) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) + z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) -- if $funcinst(z)[a] = fi -- Expand: fi.TYPE ~~ FUNC (t_1^n -> t_2^m) @@ -178,21 +178,21 @@ rule Step_read/return_call: rule Step_read/return_call_ref-label: - z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF tu) instr*) ~> val* (RETURN_CALL_REF tu) + z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF yy) instr*) ~> val* (RETURN_CALL_REF yy) rule Step_read/return_call_ref-frame-null: - z; (FRAME_ k `{f} val* (REF.NULL ht) (RETURN_CALL_REF tu) instr*) ~> TRAP + z; (FRAME_ k `{f} val* (REF.NULL ht) (RETURN_CALL_REF yy) instr*) ~> TRAP rule Step_read/return_call_ref-frame-addr: - z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF tu) instr*) ~> val^n (REF.FUNC_ADDR a) (CALL_REF tu) + z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF yy) instr*) ~> val^n (REF.FUNC_ADDR a) (CALL_REF yy) -- Expand: $funcinst(z)[a].TYPE ~~ FUNC (t_1^n -> t_2^m) rule Step_pure/call_indirect: - (CALL_INDIRECT x y) ~> (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (CALL_REF $idx(y)) + (CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (CALL_REF yy) rule Step_pure/return_call_indirect: - (RETURN_CALL_INDIRECT x y) ~> (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (RETURN_CALL_REF $idx(y)) + (RETURN_CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (RETURN_CALL_REF yy) rule Step_pure/frame-vals: diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup index 6dd83ad5fa..06edd8337d 100644 --- a/spectec/spec/wasm-3.0/A-binary.watsup +++ b/spectec/spec/wasm-3.0/A-binary.watsup @@ -171,7 +171,7 @@ grammar Bmemtype : memtype = grammar Bexterntype : externtype = - | 0x00 ct:Bcomptype => FUNC (DEF (REC (SUB FINAL eps ct)) 0) ;; TODO: typeidx + | 0x00 x:Btypeidx => FUNC $idx(x) | 0x01 tt:Btabletype => TABLE tt | 0x02 mt:Bmemtype => MEM mt | 0x03 gt:Bglobaltype => GLOBAL gt @@ -203,7 +203,9 @@ grammar Binstr/control : instr = | 0x0E l*:Bvec(Blabelidx) l_N:Blabelidx => BR_TABLE l* l_N | 0x0F => RETURN | 0x10 x:Bfuncidx => CALL x - | 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x y + | 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x $idx(y) + | 0x12 x:Bfuncidx => RETURN_CALL x + | 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x $idx(y) | ... @@ -234,7 +236,6 @@ grammar Binstr/reference : instr = ... | ... - ;; Heap instructions grammar Binstr/struct : instr = ... @@ -271,7 +272,7 @@ grammar Binstr/struct : instr = ... grammar Binstr/parametric : instr = ... | 0x1A => DROP | 0x1B => SELECT -;; | 0x1C t*:Bvec(Bvaltype) => SELECT (t*) TODO + | 0x1C ts:Bvec(Bvaltype) => SELECT ts ;; TODO: t* | ... @@ -347,8 +348,8 @@ grammar Binstr/memory : instr = ... grammar Binstr/numeric-const : instr = ... | 0x41 n:Bu32 => CONST I32 n | 0x42 n:Bu64 => CONST I64 n -;; | 0x43 p:Bf32 => CONST F32 p ;; TODO -;; | 0x44 p:Bf64 => CONST F64 p ;; TODO + | 0x43 p:Bf32 => CONST F32 p + | 0x44 p:Bf64 => CONST F64 p | ... grammar Binstr/numeric-test-i32 : instr = ... diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml index 72ef69df70..933c7b1836 100644 --- a/spectec/src/backend-interpreter/construct.ml +++ b/spectec/src/backend-interpreter/construct.ml @@ -138,6 +138,13 @@ and al_to_def_type: value -> def_type = function | CaseV ("DEF", [ rt; i32 ]) -> DefT (al_to_rec_type rt, al_to_int32 i32) | v -> error_value "def type" v +and al_to_typeuse: value -> idx = function + | v when !version <= 2 -> al_to_idx v + | CaseV ("_IDX", [ i32 ]) -> al_to_idx i32 + | CaseV ("REC", _) -> 0l @@ no_region (* dummy *) + | CaseV ("DEF", _) -> 0l @@ no_region (* dummy *) + | v -> error_value "type use" v + and al_to_heap_type: value -> heap_type = function | CaseV ("_IDX", [ i32 ]) -> VarHT (StatX (al_to_int32 i32)) | CaseV ("REC", [ i32 ]) -> VarHT (RecX (al_to_int32 i32)) @@ -820,13 +827,13 @@ and al_to_instr': value -> Ast.instr' = function BrOnCastFail (al_to_idx idx, al_to_ref_type rt1, al_to_ref_type rt2) | CaseV ("RETURN", []) -> Return | CaseV ("CALL", [ idx ]) -> Call (al_to_idx idx) - | CaseV ("CALL_REF", [ OptV (Some idx) ]) -> CallRef (al_to_idx idx) - | CaseV ("CALL_INDIRECT", [ idx1; idx2 ]) -> - CallIndirect (al_to_idx idx1, al_to_idx idx2) + | CaseV ("CALL_REF", [ typeuse ]) -> CallRef (al_to_typeuse typeuse) + | CaseV ("CALL_INDIRECT", [ idx1; typeuse2 ]) -> + CallIndirect (al_to_idx idx1, al_to_typeuse typeuse2) | CaseV ("RETURN_CALL", [ idx ]) -> ReturnCall (al_to_idx idx) - | CaseV ("RETURN_CALL_REF", [ OptV (Some idx) ]) -> ReturnCallRef (al_to_idx idx) - | CaseV ("RETURN_CALL_INDIRECT", [ idx1; idx2 ]) -> - ReturnCallIndirect (al_to_idx idx1, al_to_idx idx2) + | CaseV ("RETURN_CALL_REF", [ typeuse ]) -> ReturnCallRef (al_to_typeuse typeuse) + | CaseV ("RETURN_CALL_INDIRECT", [ idx1; typeuse2 ]) -> + ReturnCallIndirect (al_to_idx idx1, al_to_typeuse typeuse2) | CaseV ("LOAD", loadop) -> let idx, op = al_to_loadop loadop in Load (idx, op) | CaseV ("STORE", storeop) -> let idx, op = al_to_storeop storeop in Store (idx, op) | CaseV ("VLOAD", vloadop) -> let idx , op = al_to_vloadop vloadop in VecLoad (idx, op) @@ -1107,6 +1114,10 @@ and al_of_rec_type = function and al_of_def_type = function | DefT (rt, i) -> CaseV ("DEF", [al_of_rec_type rt; al_of_int32 i]) +and al_of_typeuse = function + | idx when !version <= 2 -> al_of_idx idx + | idx -> CaseV ("_IDX", [ al_of_idx idx ]) + and al_of_heap_type = function | VarHT (StatX i) -> CaseV ("_IDX", [ al_of_int32 i ]) | VarHT (RecX i) -> CaseV ("REC", [ al_of_int32 i ]) @@ -1793,12 +1804,12 @@ let rec al_of_instr instr = | Call idx -> CaseV ("CALL", [ al_of_idx idx ]) | CallRef idx -> CaseV ("CALL_REF", [ optV (Some (al_of_idx idx)) ]) | CallIndirect (idx1, idx2) -> - let args = al_with_version [ 2; 3 ] al_of_idx idx1 @ [ al_of_idx idx2 ] in + let args = al_with_version [ 2; 3 ] al_of_idx idx1 @ [ al_of_typeuse idx2 ] in CaseV ("CALL_INDIRECT", args) | ReturnCall idx -> CaseV ("RETURN_CALL", [ al_of_idx idx ]) - | ReturnCallRef idx -> CaseV ("RETURN_CALL_REF", [ optV (Some (al_of_idx idx)) ]) + | ReturnCallRef idx -> CaseV ("RETURN_CALL_REF", [ optV (Some (al_of_typeuse idx)) ]) | ReturnCallIndirect (idx1, idx2) -> - CaseV ("RETURN_CALL_INDIRECT", [ al_of_idx idx1; al_of_idx idx2 ]) + CaseV ("RETURN_CALL_INDIRECT", [ al_of_idx idx1; al_of_typeuse idx2 ]) | Load (idx, loadop) -> CaseV ("LOAD", al_of_loadop idx loadop) | Store (idx, storeop) -> CaseV ("STORE", al_of_storeop idx storeop) | VecLoad (idx, vloadop) -> CaseV ("VLOAD", al_of_vloadop idx vloadop) diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml index 442f0d7e35..a0c4124af6 100644 --- a/spectec/src/backend-interpreter/ds.ml +++ b/spectec/src/backend-interpreter/ds.ml @@ -82,9 +82,8 @@ let string_of_env env = let lookup_env key env = try Env.find key env with Not_found -> - Printf.sprintf "The key '%s' is not in the map: %s." - key (string_of_env env) - |> prerr_endline; + Printf.eprintf "The key '%s' is not in the map: %s.\n%!" + key (string_of_env env); raise Not_found diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index 03cd6990d2..38721e62db 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -1593,10 +1593,11 @@ and elab_sym_list env = function and elab_prod env prod t = let (g, e, prems) = prod.it in - let _e' = elab_exp env e t in - let _prems' = concat_map_filter_nl_list (elab_prem env) prems in - ignore (elab_sym env g); - let free = Free.(diff (free_prod prod) (union (det_prod prod) (bound_env env))) in + let env' = local_env env in + let _prems' = concat_map_filter_nl_list (elab_prem env') prems in + let _g, env'' = elab_sym env' g in + let _e' = elab_exp env'' e t in + let free = Free.(diff (free_prod prod) (union (det_prod prod) (bound_env env''))) in if free <> Free.empty then error prod.at ("grammar rule contains indeterminate variable(s) `" ^ String.concat "`, `" (Free.Set.elements free.varid) ^ "`") diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index df1f786c45..c66e320281 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -458,7 +458,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -848,7 +848,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -866,11 +866,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -1166,14 +1166,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -1196,78 +1196,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -1289,7 +1289,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -1310,11 +1310,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -1357,13 +1357,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -1371,13 +1371,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -1385,13 +1385,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -1399,13 +1399,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -2341,11 +2341,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -2941,10 +2941,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -3006,9 +3006,9 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -3236,7 +3236,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -3313,7 +3313,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -3452,7 +3452,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -3481,7 +3481,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -4157,7 +4157,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) ;; 6-typing.watsup @@ -4358,12 +4358,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -4672,12 +4672,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if ($funcinst(z)[a] = fi) -- Expand: `%~~%`(fi.TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) -- if (fi.CODE_funcinst = FUNC_func(y, LOCAL_local(t)*{t : valtype}, instr*{instr : instr})) @@ -4689,16 +4689,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- Expand: `%~~%`($funcinst(z)[a].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) ;; 8-reduction.watsup diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index d277275ca5..94ed5df028 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -284,7 +284,7 @@ $$ \mbox{(memory type)} & {\mathit{memtype}} &::=& {\mathit{limits}}~\mathsf{i{\scriptstyle8}} \\ \mbox{(element type)} & {\mathit{elemtype}} &::=& {\mathit{reftype}} \\ \mbox{(data type)} & {\mathit{datatype}} &::=& \mathsf{ok} \\ -\mbox{(external type)} & {\mathit{externtype}} &::=& \mathsf{func}~{\mathit{deftype}} ~|~ \mathsf{global}~{\mathit{globaltype}} ~|~ \mathsf{table}~{\mathit{tabletype}} ~|~ \mathsf{mem}~{\mathit{memtype}} \\ +\mbox{(external type)} & {\mathit{externtype}} &::=& \mathsf{func}~{\mathit{typeuse}} ~|~ \mathsf{global}~{\mathit{globaltype}} ~|~ \mathsf{table}~{\mathit{tabletype}} ~|~ \mathsf{mem}~{\mathit{memtype}} \\ \end{array} $$ @@ -494,11 +494,11 @@ $$ \mathsf{br\_on\_cast\_fail}~{\mathit{labelidx}}~{\mathit{reftype}}~{\mathit{reftype}} \\ &&|& \mathsf{call}~{\mathit{funcidx}} \\ &&|& \mathsf{call\_ref}~{\mathit{typeuse}} \\ &&|& -\mathsf{call\_indirect}~{\mathit{tableidx}}~{\mathit{typeidx}} \\ &&|& +\mathsf{call\_indirect}~{\mathit{tableidx}}~{\mathit{typeuse}} \\ &&|& \mathsf{return} \\ &&|& \mathsf{return\_call}~{\mathit{funcidx}} \\ &&|& \mathsf{return\_call\_ref}~{\mathit{typeuse}} \\ &&|& -\mathsf{return\_call\_indirect}~{\mathit{tableidx}}~{\mathit{typeidx}} \\ &&|& +\mathsf{return\_call\_indirect}~{\mathit{tableidx}}~{\mathit{typeuse}} \\ &&|& {\mathit{numtype}}.\mathsf{const}~{{\mathit{num}}}_{{\mathit{numtype}}} \\ &&|& {\mathit{numtype}} . {{\mathit{unop}}}_{{\mathit{numtype}}} \\ &&|& {\mathit{numtype}} . {{\mathit{binop}}}_{{\mathit{numtype}}} \\ &&|& @@ -2702,9 +2702,9 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -{\mathit{C}}.\mathsf{rec}{}[{\mathit{i}}] = \mathsf{sub}~{\mathit{fin}}~({{\mathit{tu}}_{{1}}^\ast}~{\mathit{tu}}~{{\mathit{tu}}_{{2}}^\ast})~{\mathit{ct}} +{\mathit{C}}.\mathsf{rec}{}[{\mathit{i}}] = \mathsf{sub}~{\mathit{fin}}~({{{\mathit{y}}}_{{1}}^\ast}~{{\mathit{y}}}~{{{\mathit{y}}}_{{2}}^\ast})~{\mathit{ct}} }{ -{\mathit{C}} \vdash \mathsf{rec}~{\mathit{i}} \leq {\mathit{tu}} +{\mathit{C}} \vdash \mathsf{rec}~{\mathit{i}} \leq {{\mathit{y}}} } \, {[\textsc{\scriptsize S{-}heap{-}rec}]} \qquad \end{array} @@ -2977,9 +2977,9 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -{\mathrm{unroll}}({\mathit{deftype}}_{{1}}) = \mathsf{sub}~{\mathit{fin}}~({{\mathit{tu}}_{{1}}^\ast}~{\mathit{tu}}~{{\mathit{tu}}_{{2}}^\ast})~{\mathit{ct}} +{\mathrm{unroll}}({\mathit{deftype}}_{{1}}) = \mathsf{sub}~{\mathit{fin}}~({{{\mathit{y}}}_{{1}}^\ast}~{{\mathit{y}}}~{{{\mathit{y}}}_{{2}}^\ast})~{\mathit{ct}} \qquad -{\mathit{C}} \vdash {\mathit{tu}} \leq {\mathit{deftype}}_{{2}} +{\mathit{C}} \vdash {{\mathit{y}}} \leq {\mathit{deftype}}_{{2}} }{ {\mathit{C}} \vdash {\mathit{deftype}}_{{1}} \leq {\mathit{deftype}}_{{2}} } \, {[\textsc{\scriptsize S{-}def{-}super}]} @@ -5355,8 +5355,8 @@ $$ \begin{array}{@{}l@{}rcl@{}l@{}} {[\textsc{\scriptsize E{-}call}]} \quad & {\mathit{z}} ; (\mathsf{call}~{\mathit{x}}) &\hookrightarrow& (\mathsf{ref.func}~{\mathit{a}})~(\mathsf{call\_ref}~{\mathit{z}}.\mathsf{funcs}{}[{\mathit{a}}].\mathsf{type}) &\quad \mbox{if}~{\mathit{z}}.\mathsf{module}.\mathsf{func}{}[{\mathit{x}}] = {\mathit{a}} \\ -{[\textsc{\scriptsize E{-}call\_ref{-}null}]} \quad & {\mathit{z}} ; (\mathsf{ref.null}~{\mathit{ht}})~(\mathsf{call\_ref}~{\mathit{tu}}) &\hookrightarrow& \mathsf{trap} \\ -{[\textsc{\scriptsize E{-}call\_ref{-}func}]} \quad & {\mathit{z}} ; {{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{call\_ref}~{\mathit{tu}}) &\hookrightarrow& \multicolumn{2}{l@{}}{ ({{\mathsf{frame}}_{{\mathit{m}}}}{\{{\mathit{f}}\}}~({{\mathsf{label}}_{{\mathit{m}}}}{\{\epsilon\}}~{{\mathit{instr}}^\ast})) } \\ +{[\textsc{\scriptsize E{-}call\_ref{-}null}]} \quad & {\mathit{z}} ; (\mathsf{ref.null}~{\mathit{ht}})~(\mathsf{call\_ref}~{{\mathit{y}}}) &\hookrightarrow& \mathsf{trap} \\ +{[\textsc{\scriptsize E{-}call\_ref{-}func}]} \quad & {\mathit{z}} ; {{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{call\_ref}~{{\mathit{y}}}) &\hookrightarrow& \multicolumn{2}{l@{}}{ ({{\mathsf{frame}}_{{\mathit{m}}}}{\{{\mathit{f}}\}}~({{\mathsf{label}}_{{\mathit{m}}}}{\{\epsilon\}}~{{\mathit{instr}}^\ast})) } \\ &&& \multicolumn{2}{l@{}}{\quad \mbox{if}~{\mathit{z}}.\mathsf{funcs}{}[{\mathit{a}}] = {\mathit{fi}}} \\ &&& \multicolumn{2}{l@{}}{\quad {\land}~{\mathit{fi}}.\mathsf{type} \approx \mathsf{func}~({{\mathit{t}}_{{1}}^{{\mathit{n}}}} \rightarrow {{\mathit{t}}_{{2}}^{{\mathit{m}}}})} \\ &&& \multicolumn{2}{l@{}}{\quad {\land}~{\mathit{fi}}.\mathsf{code} = \mathsf{func}~{\mathit{y}}~{(\mathsf{local}~{\mathit{t}})^\ast}~({{\mathit{instr}}^\ast})} \\ @@ -5378,9 +5378,9 @@ $$ $$ \begin{array}{@{}l@{}rcl@{}l@{}} -{[\textsc{\scriptsize E{-}return\_call\_ref{-}label}]} \quad & {\mathit{z}} ; ({{\mathsf{label}}_{{\mathit{k}}}}{\{{{\mathit{instr}'}^\ast}\}}~{{\mathit{val}}^\ast}~(\mathsf{return\_call\_ref}~{\mathit{tu}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& {{\mathit{val}}^\ast}~(\mathsf{return\_call\_ref}~{\mathit{tu}}) \\ -{[\textsc{\scriptsize E{-}return\_call\_ref{-}frame{-}null}]} \quad & {\mathit{z}} ; ({{\mathsf{frame}}_{{\mathit{k}}}}{\{{\mathit{f}}\}}~{{\mathit{val}}^\ast}~(\mathsf{ref.null}~{\mathit{ht}})~(\mathsf{return\_call\_ref}~{\mathit{tu}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& \mathsf{trap} \\ -{[\textsc{\scriptsize E{-}return\_call\_ref{-}frame{-}addr}]} \quad & {\mathit{z}} ; ({{\mathsf{frame}}_{{\mathit{k}}}}{\{{\mathit{f}}\}}~{{\mathit{val}'}^\ast}~{{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{return\_call\_ref}~{\mathit{tu}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& {{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{call\_ref}~{\mathit{tu}}) +{[\textsc{\scriptsize E{-}return\_call\_ref{-}label}]} \quad & {\mathit{z}} ; ({{\mathsf{label}}_{{\mathit{k}}}}{\{{{\mathit{instr}'}^\ast}\}}~{{\mathit{val}}^\ast}~(\mathsf{return\_call\_ref}~{{\mathit{y}}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& {{\mathit{val}}^\ast}~(\mathsf{return\_call\_ref}~{{\mathit{y}}}) \\ +{[\textsc{\scriptsize E{-}return\_call\_ref{-}frame{-}null}]} \quad & {\mathit{z}} ; ({{\mathsf{frame}}_{{\mathit{k}}}}{\{{\mathit{f}}\}}~{{\mathit{val}}^\ast}~(\mathsf{ref.null}~{\mathit{ht}})~(\mathsf{return\_call\_ref}~{{\mathit{y}}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& \mathsf{trap} \\ +{[\textsc{\scriptsize E{-}return\_call\_ref{-}frame{-}addr}]} \quad & {\mathit{z}} ; ({{\mathsf{frame}}_{{\mathit{k}}}}{\{{\mathit{f}}\}}~{{\mathit{val}'}^\ast}~{{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{return\_call\_ref}~{{\mathit{y}}})~{{\mathit{instr}}^\ast}) &\hookrightarrow& {{\mathit{val}}^{{\mathit{n}}}}~(\mathsf{ref.func}~{\mathit{a}})~(\mathsf{call\_ref}~{{\mathit{y}}}) &\quad \mbox{if}~{\mathit{z}}.\mathsf{funcs}{}[{\mathit{a}}].\mathsf{type} \approx \mathsf{func}~({{\mathit{t}}_{{1}}^{{\mathit{n}}}} \rightarrow {{\mathit{t}}_{{2}}^{{\mathit{m}}}}) \\ \end{array} $$ @@ -5389,8 +5389,8 @@ $$ $$ \begin{array}{@{}l@{}rcl@{}l@{}} -{[\textsc{\scriptsize E{-}call\_indirect}]} \quad & (\mathsf{call\_indirect}~{\mathit{x}}~{\mathit{y}}) &\hookrightarrow& (\mathsf{table.get}~{\mathit{x}})~(\mathsf{ref.cast}~(\mathsf{ref}~\mathsf{null}~{\mathit{y}}))~(\mathsf{call\_ref}~{\mathit{y}}) \\ -{[\textsc{\scriptsize E{-}return\_call\_indirect}]} \quad & (\mathsf{return\_call\_indirect}~{\mathit{x}}~{\mathit{y}}) &\hookrightarrow& (\mathsf{table.get}~{\mathit{x}})~(\mathsf{ref.cast}~(\mathsf{ref}~\mathsf{null}~{\mathit{y}}))~(\mathsf{return\_call\_ref}~{\mathit{y}}) \\ +{[\textsc{\scriptsize E{-}call\_indirect}]} \quad & (\mathsf{call\_indirect}~{\mathit{x}}~{{\mathit{y}}}) &\hookrightarrow& (\mathsf{table.get}~{\mathit{x}})~(\mathsf{ref.cast}~(\mathsf{ref}~\mathsf{null}~{{\mathit{y}}}))~(\mathsf{call\_ref}~{{\mathit{y}}}) \\ +{[\textsc{\scriptsize E{-}return\_call\_indirect}]} \quad & (\mathsf{return\_call\_indirect}~{\mathit{x}}~{{\mathit{y}}}) &\hookrightarrow& (\mathsf{table.get}~{\mathit{x}})~(\mathsf{ref.cast}~(\mathsf{ref}~\mathsf{null}~{{\mathit{y}}}))~(\mathsf{return\_call\_ref}~{{\mathit{y}}}) \\ \end{array} $$ @@ -6628,7 +6628,7 @@ $$ $$ \begin{array}{@{}l@{}rrlll@{}l@{}} -& {\mathtt{externtype}} &::=& \mathtt{0x00}~{\mathit{ct}}{:}{\mathtt{comptype}} &\Rightarrow& \mathsf{func}~((\mathsf{rec}~(\mathsf{sub}~\mathsf{final}~\epsilon~{\mathit{ct}})) . 0) \\ &&|& +& {\mathtt{externtype}} &::=& \mathtt{0x00}~{\mathit{x}}{:}{\mathtt{typeidx}} &\Rightarrow& \mathsf{func}~{\mathit{x}} \\ &&|& \mathtt{0x01}~{\mathit{tt}}{:}{\mathtt{tabletype}} &\Rightarrow& \mathsf{table}~{\mathit{tt}} \\ &&|& \mathtt{0x02}~{\mathit{mt}}{:}{\mathtt{memtype}} &\Rightarrow& \mathsf{mem}~{\mathit{mt}} \\ &&|& \mathtt{0x03}~{\mathit{gt}}{:}{\mathtt{globaltype}} &\Rightarrow& \mathsf{global}~{\mathit{gt}} \\ @@ -6664,6 +6664,8 @@ $$ \mathtt{0x0F} &\Rightarrow& \mathsf{return} \\ &&|& \mathtt{0x10}~{\mathit{x}}{:}{\mathtt{funcidx}} &\Rightarrow& \mathsf{call}~{\mathit{x}} \\ &&|& \mathtt{0x11}~{\mathit{y}}{:}{\mathtt{typeidx}}~{\mathit{x}}{:}{\mathtt{tableidx}} &\Rightarrow& \mathsf{call\_indirect}~{\mathit{x}}~{\mathit{y}} \\ &&|& +\mathtt{0x12}~{\mathit{x}}{:}{\mathtt{funcidx}} &\Rightarrow& \mathsf{return\_call}~{\mathit{x}} \\ &&|& +\mathtt{0x13}~{\mathit{y}}{:}{\mathtt{typeidx}}~{\mathit{x}}{:}{\mathtt{tableidx}} &\Rightarrow& \mathsf{return\_call\_indirect}~{\mathit{x}}~{\mathit{y}} \\ &&|& \dots \\ \end{array} $$ @@ -6741,6 +6743,7 @@ $$ & {\mathtt{instr}} &::=& \dots \\ &&|& \mathtt{0x1A} &\Rightarrow& \mathsf{drop} \\ &&|& \mathtt{0x1B} &\Rightarrow& \mathsf{select} \\ &&|& +\mathtt{0x1C}~{\mathit{ts}}{:}{\mathtt{vec}}({\mathtt{valtype}}) &\Rightarrow& \mathsf{select}~{\mathit{ts}} \\ &&|& \dots \\ \end{array} $$ @@ -6833,6 +6836,8 @@ $$ & {\mathtt{instr}} &::=& \dots \\ &&|& \mathtt{0x41}~{\mathit{n}}{:}{\mathtt{u{\scriptstyle32}}} &\Rightarrow& \mathsf{i{\scriptstyle32}}.\mathsf{const}~{\mathit{n}} \\ &&|& \mathtt{0x42}~{\mathit{n}}{:}{\mathtt{u{\scriptstyle64}}} &\Rightarrow& \mathsf{i{\scriptstyle64}}.\mathsf{const}~{\mathit{n}} \\ &&|& +\mathtt{0x43}~{\mathit{p}}{:}{\mathtt{f{\scriptstyle32}}} &\Rightarrow& \mathsf{f{\scriptstyle32}}.\mathsf{const}~{\mathit{p}} \\ &&|& +\mathtt{0x44}~{\mathit{p}}{:}{\mathtt{f{\scriptstyle64}}} &\Rightarrow& \mathsf{f{\scriptstyle64}}.\mathsf{const}~{\mathit{p}} \\ &&|& \mathtt{0x45} &\Rightarrow& \mathsf{i{\scriptstyle32}} . \mathsf{eqz} \\ &&|& \mathtt{0x46} &\Rightarrow& \mathsf{i{\scriptstyle32}} . \mathsf{eq} \\ &&|& \mathtt{0x47} &\Rightarrow& \mathsf{i{\scriptstyle32}} . \mathsf{ne} \\ &&|& diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 6ac67d7f77..4824a2d6d6 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -448,7 +448,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -838,7 +838,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -856,11 +856,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -1156,14 +1156,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -1186,78 +1186,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -1279,7 +1279,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -1300,11 +1300,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -1347,13 +1347,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -1361,13 +1361,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -1375,13 +1375,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -1389,13 +1389,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -2331,11 +2331,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -2931,10 +2931,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -2996,9 +2996,9 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -3226,7 +3226,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -3303,7 +3303,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -3442,7 +3442,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -3471,7 +3471,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -4147,7 +4147,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) ;; 6-typing.watsup @@ -4348,12 +4348,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -4662,12 +4662,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if ($funcinst(z)[a] = fi) -- Expand: `%~~%`(fi.TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) -- if (fi.CODE_funcinst = FUNC_func(y, LOCAL_local(t)*{t : valtype}, instr*{instr : instr})) @@ -4679,16 +4679,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- Expand: `%~~%`($funcinst(z)[a].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) ;; 8-reduction.watsup @@ -5994,7 +5994,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -6384,7 +6384,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -6402,11 +6402,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -6705,14 +6705,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -6735,78 +6735,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -6828,7 +6828,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -6849,11 +6849,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -6896,13 +6896,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -6910,13 +6910,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -6924,13 +6924,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -6938,13 +6938,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -7880,11 +7880,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -8482,10 +8482,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -8547,9 +8547,9 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -8777,7 +8777,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -8854,7 +8854,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -8993,7 +8993,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -9022,7 +9022,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -9698,7 +9698,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) ;; 6-typing.watsup @@ -9899,12 +9899,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -10213,12 +10213,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if ($funcinst(z)[a] = fi) -- Expand: `%~~%`(fi.TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) -- if (fi.CODE_funcinst = FUNC_func(y, LOCAL_local(t)*{t : valtype}, instr*{instr : instr})) @@ -10230,16 +10230,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- Expand: `%~~%`($funcinst(z)[a].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) ;; 8-reduction.watsup @@ -11545,7 +11545,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -11935,7 +11935,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -11953,11 +11953,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -12256,14 +12256,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -12286,78 +12286,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -12379,7 +12379,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -12400,11 +12400,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -12447,13 +12447,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -12461,13 +12461,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -12475,13 +12475,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -12489,13 +12489,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -13431,11 +13431,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -14033,10 +14033,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -14098,9 +14098,9 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -14328,7 +14328,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -14405,7 +14405,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -14544,7 +14544,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -14573,7 +14573,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(`NULL%?`_nul(?(())), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})))) @@ -15249,7 +15249,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) ;; 6-typing.watsup @@ -15450,12 +15450,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -15764,12 +15764,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if ($funcinst(z)[a] = fi) -- Expand: `%~~%`(fi.TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) -- if (fi.CODE_funcinst = FUNC_func(y, LOCAL_local(t)*{t : valtype}, instr*{instr : instr})) @@ -15781,16 +15781,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- Expand: `%~~%`($funcinst(z)[a].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) ;; 8-reduction.watsup @@ -17096,7 +17096,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -17486,7 +17486,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -17504,11 +17504,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -17807,14 +17807,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -17837,78 +17837,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -17930,7 +17930,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -17951,11 +17951,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -17998,13 +17998,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -18012,13 +18012,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -18026,13 +18026,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -18040,13 +18040,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -18982,11 +18982,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -19588,10 +19588,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -19655,10 +19655,10 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) -- if (i < |C.REC_context|) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -19892,7 +19892,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -19972,7 +19972,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -20122,7 +20122,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (y!`%`_idx.0 < |C.TYPES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) @@ -20155,7 +20155,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (y!`%`_idx.0 < |C.TYPES_context|) -- if (C.TABLES_context[x!`%`_idx.0] = `%%`_tabletype(lim, rt)) @@ -20901,7 +20901,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (x!`%`_idx.0 < |C.FUNCS_context|) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) @@ -21115,12 +21115,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -21437,12 +21437,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if (a < |$funcinst(z)|) -- if ($funcinst(z)[a] = fi) -- Expand: `%~~%`(fi.TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) @@ -21457,16 +21457,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if ($funcaddr(z)[x!`%`_idx.0] = a) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- if (a < |$funcinst(z)|) -- Expand: `%~~%`($funcinst(z)[a].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype})))) @@ -22806,7 +22806,7 @@ syntax datatype = ;; 1-syntax.watsup syntax externtype = - | FUNC{deftype : deftype}(deftype : deftype) + | FUNC{typeuse : typeuse}(typeuse : typeuse) | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | TABLE{tabletype : tabletype}(tabletype : tabletype) | MEM{memtype : memtype}(memtype : memtype) @@ -23196,7 +23196,7 @@ syntax zero = ;; 1-syntax.watsup rec { -;; 1-syntax.watsup:582.1-583.22 +;; 1-syntax.watsup:580.1-581.22 syntax instr = | NOP | UNREACHABLE @@ -23214,11 +23214,11 @@ syntax instr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -23517,14 +23517,14 @@ def $idx(typeidx : typeidx) : typevar ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:139.1-139.91 +;; 2-syntax-aux.watsup:141.1-141.91 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:165.1-165.38 + ;; 2-syntax-aux.watsup:167.1-167.38 def $subst_typevar{xx : typevar}(xx, [], []) = (xx : typevar <: typeuse) - ;; 2-syntax-aux.watsup:166.1-166.95 + ;; 2-syntax-aux.watsup:168.1-168.95 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = tu_1 -- if (xx = xx_1) - ;; 2-syntax-aux.watsup:167.1-167.92 + ;; 2-syntax-aux.watsup:169.1-169.92 def $subst_typevar{xx : typevar, xx_1 : typevar, xx'* : typevar*, tu_1 : typeuse, tu'* : typeuse*}(xx, [xx_1] :: xx'*{xx' : typevar}, [tu_1] :: tu'*{tu' : typeuse}) = $subst_typevar(xx, xx'*{xx' : typevar}, tu'*{tu' : typeuse}) -- otherwise } @@ -23547,78 +23547,78 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:140.1-140.91 +;; 2-syntax-aux.watsup:142.1-142.91 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; 2-syntax-aux.watsup:169.1-169.66 + ;; 2-syntax-aux.watsup:171.1-171.66 def $subst_typeuse{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = $subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) - ;; 2-syntax-aux.watsup:170.1-170.64 + ;; 2-syntax-aux.watsup:172.1-172.64 def $subst_typeuse{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: typeuse), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse) -;; 2-syntax-aux.watsup:144.1-144.91 +;; 2-syntax-aux.watsup:146.1-146.91 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; 2-syntax-aux.watsup:175.1-175.67 + ;; 2-syntax-aux.watsup:177.1-177.67 def $subst_heaptype{xx' : typevar, xx* : typevar*, tu* : typeuse*}((xx' : typevar <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_typevar(xx', xx*{xx : typevar}, tu*{tu : typeuse}) : typeuse <: heaptype) - ;; 2-syntax-aux.watsup:176.1-176.65 + ;; 2-syntax-aux.watsup:178.1-178.65 def $subst_heaptype{dt : deftype, xx* : typevar*, tu* : typeuse*}((dt : deftype <: heaptype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: heaptype) - ;; 2-syntax-aux.watsup:177.1-177.53 + ;; 2-syntax-aux.watsup:179.1-179.53 def $subst_heaptype{ht : heaptype, xx* : typevar*, tu* : typeuse*}(ht, xx*{xx : typevar}, tu*{tu : typeuse}) = ht -- otherwise -;; 2-syntax-aux.watsup:145.1-145.91 +;; 2-syntax-aux.watsup:147.1-147.91 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; 2-syntax-aux.watsup:179.1-179.83 + ;; 2-syntax-aux.watsup:181.1-181.83 def $subst_reftype{nul : nul, ht : heaptype, xx* : typevar*, tu* : typeuse*}(REF_reftype(nul, ht), xx*{xx : typevar}, tu*{tu : typeuse}) = REF_reftype(nul, $subst_heaptype(ht, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:146.1-146.91 +;; 2-syntax-aux.watsup:148.1-148.91 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; 2-syntax-aux.watsup:181.1-181.64 + ;; 2-syntax-aux.watsup:183.1-183.64 def $subst_valtype{nt : numtype, xx* : typevar*, tu* : typeuse*}((nt : numtype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_numtype(nt, xx*{xx : typevar}, tu*{tu : typeuse}) : numtype <: valtype) - ;; 2-syntax-aux.watsup:182.1-182.64 + ;; 2-syntax-aux.watsup:184.1-184.64 def $subst_valtype{vt : vectype, xx* : typevar*, tu* : typeuse*}((vt : vectype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_vectype(vt, xx*{xx : typevar}, tu*{tu : typeuse}) : vectype <: valtype) - ;; 2-syntax-aux.watsup:183.1-183.64 + ;; 2-syntax-aux.watsup:185.1-185.64 def $subst_valtype{rt : reftype, xx* : typevar*, tu* : typeuse*}((rt : reftype <: valtype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_reftype(rt, xx*{xx : typevar}, tu*{tu : typeuse}) : reftype <: valtype) - ;; 2-syntax-aux.watsup:184.1-184.40 + ;; 2-syntax-aux.watsup:186.1-186.40 def $subst_valtype{xx* : typevar*, tu* : typeuse*}(BOT_valtype, xx*{xx : typevar}, tu*{tu : typeuse}) = BOT_valtype -;; 2-syntax-aux.watsup:149.1-149.91 +;; 2-syntax-aux.watsup:151.1-151.91 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; 2-syntax-aux.watsup:188.1-188.66 + ;; 2-syntax-aux.watsup:190.1-190.66 def $subst_storagetype{t : valtype, xx* : typevar*, tu* : typeuse*}((t : valtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_valtype(t, xx*{xx : typevar}, tu*{tu : typeuse}) : valtype <: storagetype) - ;; 2-syntax-aux.watsup:189.1-189.69 + ;; 2-syntax-aux.watsup:191.1-191.69 def $subst_storagetype{pt : packtype, xx* : typevar*, tu* : typeuse*}((pt : packtype <: storagetype), xx*{xx : typevar}, tu*{tu : typeuse}) = ($subst_packtype(pt, xx*{xx : typevar}, tu*{tu : typeuse}) : packtype <: storagetype) -;; 2-syntax-aux.watsup:150.1-150.91 +;; 2-syntax-aux.watsup:152.1-152.91 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; 2-syntax-aux.watsup:191.1-191.80 + ;; 2-syntax-aux.watsup:193.1-193.80 def $subst_fieldtype{mut : mut, zt : storagetype, xx* : typevar*, tu* : typeuse*}(`%%`_fieldtype(mut, zt), xx*{xx : typevar}, tu*{tu : typeuse}) = `%%`_fieldtype(mut, $subst_storagetype(zt, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:152.1-152.91 +;; 2-syntax-aux.watsup:154.1-154.91 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; 2-syntax-aux.watsup:193.1-193.85 + ;; 2-syntax-aux.watsup:195.1-195.85 def $subst_comptype{yt* : fieldtype*, xx* : typevar*, tu* : typeuse*}(STRUCT_comptype(`%`_structtype(yt*{yt : fieldtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = STRUCT_comptype(`%`_structtype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})*{yt : fieldtype})) - ;; 2-syntax-aux.watsup:194.1-194.81 + ;; 2-syntax-aux.watsup:196.1-196.81 def $subst_comptype{yt : fieldtype, xx* : typevar*, tu* : typeuse*}(ARRAY_comptype(yt), xx*{xx : typevar}, tu*{tu : typeuse}) = ARRAY_comptype($subst_fieldtype(yt, xx*{xx : typevar}, tu*{tu : typeuse})) - ;; 2-syntax-aux.watsup:195.1-195.78 + ;; 2-syntax-aux.watsup:197.1-197.78 def $subst_comptype{ft : functype, xx* : typevar*, tu* : typeuse*}(FUNC_comptype(ft), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_comptype($subst_functype(ft, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:153.1-153.91 +;; 2-syntax-aux.watsup:155.1-155.91 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; 2-syntax-aux.watsup:197.1-198.71 + ;; 2-syntax-aux.watsup:199.1-200.71 def $subst_subtype{fin : fin, tu'* : typeuse*, ct : comptype, xx* : typevar*, tu* : typeuse*}(SUB_subtype(fin, tu'*{tu' : typeuse}, ct), xx*{xx : typevar}, tu*{tu : typeuse}) = SUB_subtype(fin, $subst_typeuse(tu', xx*{xx : typevar}, tu*{tu : typeuse})*{tu' : typeuse}, $subst_comptype(ct, xx*{xx : typevar}, tu*{tu : typeuse})) -;; 2-syntax-aux.watsup:154.1-154.91 +;; 2-syntax-aux.watsup:156.1-156.91 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; 2-syntax-aux.watsup:200.1-200.76 + ;; 2-syntax-aux.watsup:202.1-202.76 def $subst_rectype{st* : subtype*, xx* : typevar*, tu* : typeuse*}(REC_rectype(`%`_list(st*{st : subtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = REC_rectype(`%`_list($subst_subtype(st, xx*{xx : typevar}, tu*{tu : typeuse})*{st : subtype})) -;; 2-syntax-aux.watsup:155.1-155.91 +;; 2-syntax-aux.watsup:157.1-157.91 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; 2-syntax-aux.watsup:202.1-202.78 + ;; 2-syntax-aux.watsup:204.1-204.78 def $subst_deftype{qt : rectype, i : nat, xx* : typevar*, tu* : typeuse*}(DEF_deftype(qt, i), xx*{xx : typevar}, tu*{tu : typeuse}) = DEF_deftype($subst_rectype(qt, xx*{xx : typevar}, tu*{tu : typeuse}), i) -;; 2-syntax-aux.watsup:158.1-158.91 +;; 2-syntax-aux.watsup:160.1-160.91 def $subst_functype(functype : functype, typevar*, typeuse*) : functype - ;; 2-syntax-aux.watsup:205.1-205.113 + ;; 2-syntax-aux.watsup:207.1-207.113 def $subst_functype{t_1* : valtype*, t_2* : valtype*, xx* : typevar*, tu* : typeuse*}(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype})), xx*{xx : typevar}, tu*{tu : typeuse}) = `%->%`_functype(`%`_resulttype($subst_valtype(t_1, xx*{xx : typevar}, tu*{tu : typeuse})*{t_1 : valtype}), `%`_resulttype($subst_valtype(t_2, xx*{xx : typevar}, tu*{tu : typeuse})*{t_2 : valtype})) } @@ -23640,7 +23640,7 @@ def $subst_memtype(memtype : memtype, typevar*, typeuse*) : memtype ;; 2-syntax-aux.watsup def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; 2-syntax-aux.watsup - def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype(dt), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse})) + def $subst_externtype{dt : deftype, xx* : typevar*, tu* : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), xx*{xx : typevar}, tu*{tu : typeuse}) = FUNC_externtype(($subst_deftype(dt, xx*{xx : typevar}, tu*{tu : typeuse}) : deftype <: typeuse)) ;; 2-syntax-aux.watsup def $subst_externtype{gt : globaltype, xx* : typevar*, tu* : typeuse*}(GLOBAL_externtype(gt), xx*{xx : typevar}, tu*{tu : typeuse}) = GLOBAL_externtype($subst_globaltype(gt, xx*{xx : typevar}, tu*{tu : typeuse})) ;; 2-syntax-aux.watsup @@ -23661,11 +23661,11 @@ def $subst_all_deftype(deftype : deftype, heaptype*) : deftype ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:221.1-221.77 +;; 2-syntax-aux.watsup:223.1-223.77 def $subst_all_deftypes(deftype*, heaptype*) : deftype* - ;; 2-syntax-aux.watsup:223.1-223.40 + ;; 2-syntax-aux.watsup:225.1-225.40 def $subst_all_deftypes{tu* : typeuse*}([], (tu : typeuse <: heaptype)*{tu : typeuse}) = [] - ;; 2-syntax-aux.watsup:224.1-224.101 + ;; 2-syntax-aux.watsup:226.1-226.101 def $subst_all_deftypes{dt_1 : deftype, dt* : deftype*, tu* : typeuse*}([dt_1] :: dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) = [$subst_all_deftype(dt_1, (tu : typeuse <: heaptype)*{tu : typeuse})] :: $subst_all_deftypes(dt*{dt : deftype}, (tu : typeuse <: heaptype)*{tu : typeuse}) } @@ -23708,13 +23708,13 @@ relation Expand: `%~~%`(deftype, comptype) ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:254.1-254.64 +;; 2-syntax-aux.watsup:256.1-256.64 def $funcsxt(externtype*) : deftype* - ;; 2-syntax-aux.watsup:259.1-259.24 + ;; 2-syntax-aux.watsup:261.1-261.24 def $funcsxt([]) = [] - ;; 2-syntax-aux.watsup:260.1-260.47 - def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype(dt)] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:261.1-261.59 + ;; 2-syntax-aux.watsup:262.1-262.47 + def $funcsxt{dt : deftype, xt* : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] :: xt*{xt : externtype}) = [dt] :: $funcsxt(xt*{xt : externtype}) + ;; 2-syntax-aux.watsup:263.1-263.59 def $funcsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $funcsxt(xt*{xt : externtype}) -- otherwise } @@ -23722,13 +23722,13 @@ def $funcsxt(externtype*) : deftype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:255.1-255.66 +;; 2-syntax-aux.watsup:257.1-257.66 def $globalsxt(externtype*) : globaltype* - ;; 2-syntax-aux.watsup:263.1-263.26 + ;; 2-syntax-aux.watsup:265.1-265.26 def $globalsxt([]) = [] - ;; 2-syntax-aux.watsup:264.1-264.53 + ;; 2-syntax-aux.watsup:266.1-266.53 def $globalsxt{gt : globaltype, xt* : externtype*}([GLOBAL_externtype(gt)] :: xt*{xt : externtype}) = [gt] :: $globalsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:265.1-265.63 + ;; 2-syntax-aux.watsup:267.1-267.63 def $globalsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $globalsxt(xt*{xt : externtype}) -- otherwise } @@ -23736,13 +23736,13 @@ def $globalsxt(externtype*) : globaltype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:256.1-256.65 +;; 2-syntax-aux.watsup:258.1-258.65 def $tablesxt(externtype*) : tabletype* - ;; 2-syntax-aux.watsup:267.1-267.25 + ;; 2-syntax-aux.watsup:269.1-269.25 def $tablesxt([]) = [] - ;; 2-syntax-aux.watsup:268.1-268.50 + ;; 2-syntax-aux.watsup:270.1-270.50 def $tablesxt{tt : tabletype, xt* : externtype*}([TABLE_externtype(tt)] :: xt*{xt : externtype}) = [tt] :: $tablesxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:269.1-269.61 + ;; 2-syntax-aux.watsup:271.1-271.61 def $tablesxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $tablesxt(xt*{xt : externtype}) -- otherwise } @@ -23750,13 +23750,13 @@ def $tablesxt(externtype*) : tabletype* ;; 2-syntax-aux.watsup rec { -;; 2-syntax-aux.watsup:257.1-257.63 +;; 2-syntax-aux.watsup:259.1-259.63 def $memsxt(externtype*) : memtype* - ;; 2-syntax-aux.watsup:271.1-271.23 + ;; 2-syntax-aux.watsup:273.1-273.23 def $memsxt([]) = [] - ;; 2-syntax-aux.watsup:272.1-272.44 + ;; 2-syntax-aux.watsup:274.1-274.44 def $memsxt{mt : memtype, xt* : externtype*}([MEM_externtype(mt)] :: xt*{xt : externtype}) = [mt] :: $memsxt(xt*{xt : externtype}) - ;; 2-syntax-aux.watsup:273.1-273.57 + ;; 2-syntax-aux.watsup:275.1-275.57 def $memsxt{externtype : externtype, xt* : externtype*}([externtype] :: xt*{xt : externtype}) = $memsxt(xt*{xt : externtype}) -- otherwise } @@ -24693,11 +24693,11 @@ syntax admininstr = | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | RETURN | RETURN_CALL{funcidx : funcidx}(funcidx : funcidx) | RETURN_CALL_REF{typeuse : typeuse}(typeuse : typeuse) - | RETURN_CALL_INDIRECT{tableidx : tableidx, typeidx : typeidx}(tableidx : tableidx, typeidx : typeidx) + | RETURN_CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) | CONST{numtype : numtype, num_ : num_(numtype)}(numtype : numtype, num_ : num_(numtype)) | UNOP{numtype : numtype, unop_ : unop_(numtype)}(numtype : numtype, unop_ : unop_(numtype)) | BINOP{numtype : numtype, binop_ : binop_(numtype)}(numtype : numtype, binop_ : binop_(numtype)) @@ -25299,10 +25299,10 @@ relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) -- if ($clostype(C, deftype_1) = $clostype(C, deftype_2)) ;; 6-typing.watsup:441.1-444.40 - rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, tu_1* : typeuse*, tu : typeuse, tu_2* : typeuse*, ct : comptype}: + rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, fin : fin, yy_1* : typeuse*, yy : typeuse, yy_2* : typeuse*, ct : comptype}: `%|-%<:%`(C, deftype_1, deftype_2) - -- if ($unrolldt(deftype_1) = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) - -- Heaptype_sub: `%|-%<:%`(C, (tu : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- if ($unrolldt(deftype_1) = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) + -- Heaptype_sub: `%|-%<:%`(C, (yy : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) ;; 6-typing.watsup:274.1-274.79 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -25366,10 +25366,10 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) ;; 6-typing.watsup:330.1-332.47 - rule rec{C : context, i : nat, tu : typeuse, fin : fin, tu_1* : typeuse*, tu_2* : typeuse*, ct : comptype}: - `%|-%<:%`(C, REC_heaptype(i), (tu : typeuse <: heaptype)) + rule rec{C : context, i : nat, yy : typeuse, fin : fin, yy_1* : typeuse*, yy_2* : typeuse*, ct : comptype}: + `%|-%<:%`(C, REC_heaptype(i), (yy : typeuse <: heaptype)) -- if (i < |C.REC_context|) - -- if (C.REC_context[i] = SUB_subtype(fin, tu_1*{tu_1 : typeuse} :: [tu] :: tu_2*{tu_2 : typeuse}, ct)) + -- if (C.REC_context[i] = SUB_subtype(fin, yy_1*{yy_1 : typeuse} :: [yy] :: yy_2*{yy_2 : typeuse}, ct)) ;; 6-typing.watsup:334.1-336.40 rule none{C : context, heaptype : heaptype}: @@ -25604,7 +25604,7 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) relation Externtype_ok: `%|-%:OK`(context, externtype) ;; 6-typing.watsup rule func{C : context, deftype : deftype, functype : functype}: - `%|-%:OK`(C, FUNC_externtype(deftype)) + `%|-%:OK`(C, FUNC_externtype((deftype : deftype <: typeuse))) -- Deftype_ok: `%|-%:OK`(C, deftype) -- Expand: `%~~%`(deftype, FUNC_comptype(functype)) @@ -25684,7 +25684,7 @@ relation Memtype_sub: `%|-%<:%`(context, memtype, memtype) relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) ;; 6-typing.watsup rule func{C : context, dt_1 : deftype, dt_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype(dt_1), FUNC_externtype(dt_2)) + `%|-%<:%`(C, FUNC_externtype((dt_1 : deftype <: typeuse)), FUNC_externtype((dt_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, dt_1, dt_2) ;; 6-typing.watsup @@ -25841,7 +25841,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:651.1-655.47 rule call_indirect{C : context, x : idx, y : idx, t_1* : valtype*, t_2* : valtype*, lim : limits, rt : reftype}: - `%|-%:%`(C, CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) + `%|-%:%`(C, CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_2*{t_2 : valtype}))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (y!`%`_idx.0 < |C.TYPES_context|) -- where `%%`_tabletype(lim, rt) = C.TABLES_context[x!`%`_idx.0] @@ -25874,7 +25874,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 6-typing.watsup:679.1-687.42 rule return_call_indirect{C : context, x : idx, y : idx, t_3* : valtype*, t_1* : valtype*, t_4* : valtype*, lim : limits, rt : reftype, t_2* : valtype*, t'_2* : valtype*}: - `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) + `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, ($idx(y) : typevar <: typeuse)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype} :: t_1*{t_1 : valtype} :: [I32_valtype]), [], `%`_resulttype(t_4*{t_4 : valtype}))) -- if (x!`%`_idx.0 < |C.TABLES_context|) -- if (y!`%`_idx.0 < |C.TYPES_context|) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 : valtype}), [], `%`_resulttype(t_4*{t_4 : valtype}))) @@ -26657,7 +26657,7 @@ relation Import_ok: `%|-%:%`(context, import, externtype) relation Externidx_ok: `%|-%:%`(context, externidx, externtype) ;; 6-typing.watsup rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(dt)) + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) -- if (x!`%`_idx.0 < |C.FUNCS_context|) -- where dt = C.FUNCS_context[x!`%`_idx.0] @@ -26871,12 +26871,12 @@ relation Step_pure: `%~>%`(admininstr*, admininstr*) -- otherwise ;; 8-reduction.watsup - rule call_indirect{x : idx, y : idx}: - `%~>%`([CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule call_indirect{x : idx, yy : typeuse}: + `%~>%`([CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_indirect{x : idx, y : idx}: - `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, y)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), ($idx(y) : typevar <: heaptype))) RETURN_CALL_REF_admininstr(($idx(y) : typevar <: typeuse))]) + rule return_call_indirect{x : idx, yy : typeuse}: + `%~>%`([RETURN_CALL_INDIRECT_admininstr(x, yy)], [TABLE.GET_admininstr(x) REF.CAST_admininstr(REF_reftype(`NULL%?`_nul(?(())), (yy : typeuse <: heaptype))) RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup rule frame-vals{n : n, f : frame, val^n : val^n}: @@ -27194,12 +27194,12 @@ relation Step_read: `%~>%`(config, admininstr*) -- if (a < |$funcinst(z)|) ;; 8-reduction.watsup - rule call_ref-null{z : state, ht : heaptype, tu : typeuse}: - `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(tu)]), [TRAP_admininstr]) + rule call_ref-null{z : state, ht : heaptype, yy : typeuse}: + `%~>%`(`%;%`_config(z, [REF.NULL_admininstr(ht) CALL_REF_admininstr(yy)]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, tu : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: - `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) + rule call_ref-func{z : state, val^n : val^n, n : n, a : addr, yy : typeuse, m : m, f : frame, instr* : instr*, fi : funcinst, t_1^n : valtype^n, t_2^m : valtype^m, y : idx, t* : valtype*}: + `%~>%`(`%;%`_config(z, (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]), [`FRAME_%{%}%`_admininstr(m, f, [`LABEL_%{%}%`_admininstr(m, [], (instr : instr <: admininstr)*{instr : instr})])]) -- if (a < |$funcinst(z)|) -- where fi = $funcinst(z)[a] -- where FUNC_func(y, LOCAL_local(t)*{t : valtype}, instr*{instr : instr}) = fi.CODE_funcinst @@ -27214,16 +27214,16 @@ relation Step_read: `%~>%`(config, admininstr*) -- if (a < |$funcinst(z)|) ;; 8-reduction.watsup - rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(tu)]) + rule return_call_ref-label{z : state, k : nat, instr'* : instr*, val* : val*, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_admininstr(k, instr'*{instr' : instr}, (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)*{val : val} :: [RETURN_CALL_REF_admininstr(yy)]) ;; 8-reduction.watsup - rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, tu : typeuse, instr* : instr*}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) + rule return_call_ref-frame-null{z : state, k : nat, f : frame, val* : val*, ht : heaptype, yy : typeuse, instr* : instr*}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val : val <: admininstr)*{val : val} :: [REF.NULL_admininstr(ht)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), [TRAP_admininstr]) ;; 8-reduction.watsup - rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, tu : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: - `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(tu)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(tu)]) + rule return_call_ref-frame-addr{z : state, k : nat, f : frame, val'* : val*, val^n : val^n, n : n, a : addr, yy : typeuse, instr* : instr*, t_1^n : valtype^n, t_2^m : valtype^m, m : m}: + `%~>%`(`%;%`_config(z, [`FRAME_%{%}%`_admininstr(k, f, (val' : val <: admininstr)*{val' : val} :: (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a)] :: [RETURN_CALL_REF_admininstr(yy)] :: (instr : instr <: admininstr)*{instr : instr})]), (val : val <: admininstr)^n{val : val} :: [REF.FUNC_ADDR_admininstr(a) CALL_REF_admininstr(yy)]) -- if (a < |$funcinst(z)|) -- where FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1^n{t_1 : valtype}), `%`_resulttype(t_2^m{t_2 : valtype}))) = $expanddt($funcinst(z)[a].TYPE_funcinst) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index e8210ada41..850bbca98a 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -3762,7 +3762,7 @@ validation_of_CALL_REF $idx(x) - Let (FUNC (t_1* -> t_2*)) be $expanddt(C.TYPES[x]). - The instruction is valid with type (t_1* ++ [(REF (NULL ?(())) $idx(x))] ->_ [] ++ t_2*). -validation_of_CALL_INDIRECT x y +validation_of_CALL_INDIRECT x $idx(y) - |C.TABLES| must be greater than x. - |C.TYPES| must be greater than y. - Let (lim, rt) be C.TABLES[x]. @@ -3791,7 +3791,7 @@ validation_of_RETURN_CALL_REF $idx(x) - C.RETURN must be equal to ?(t'_2*). - The instruction is valid with type (t_3* ++ t_1* ++ [(REF (NULL ?(())) $idx(x))] ->_ [] ++ t_4*). -validation_of_RETURN_CALL_INDIRECT x y +validation_of_RETURN_CALL_INDIRECT x $idx(y) - |C.TABLES| must be greater than x. - |C.TYPES| must be greater than y. - Under the context C, (t_3* ->_ [] ++ t_4*) must be valid. @@ -5903,15 +5903,15 @@ execution_of_BR_ON_NON_NULL l a. Push the value val to the stack. b. Execute the instruction (BR l). -execution_of_CALL_INDIRECT x y +execution_of_CALL_INDIRECT x yy 1. Execute the instruction (TABLE.GET x). -2. Execute the instruction (REF.CAST (REF (NULL ?(())) $idx(y))). -3. Execute the instruction (CALL_REF $idx(y)). +2. Execute the instruction (REF.CAST (REF (NULL ?(())) yy)). +3. Execute the instruction (CALL_REF yy). -execution_of_RETURN_CALL_INDIRECT x y +execution_of_RETURN_CALL_INDIRECT x yy 1. Execute the instruction (TABLE.GET x). -2. Execute the instruction (REF.CAST (REF (NULL ?(())) $idx(y))). -3. Execute the instruction (RETURN_CALL_REF $idx(y)). +2. Execute the instruction (REF.CAST (REF (NULL ?(())) yy)). +3. Execute the instruction (RETURN_CALL_REF yy). execution_of_FRAME_ 1. Let f be the current frame. @@ -6291,12 +6291,12 @@ execution_of_RETURN_CALL x 4. Push the value (REF.FUNC_ADDR a) to the stack. 5. Execute the instruction (RETURN_CALL_REF $funcinst()[a].TYPE). -execution_of_RETURN_CALL_REF tu +execution_of_RETURN_CALL_REF yy 1. If the current context is LABEL_, then: a. Pop all values val* from the stack. b. Exit current context. c. Push the values val* to the stack. - d. Execute the instruction (RETURN_CALL_REF tu). + d. Execute the instruction (RETURN_CALL_REF yy). 2. Else if the current context is FRAME_, then: a. Pop the value admin_u0 from the stack. b. Pop all values admin_u1* from the stack. @@ -6311,7 +6311,7 @@ execution_of_RETURN_CALL_REF tu 1. Let val'* ++ val^n be admin_u1*. 2. Push the values val^n to the stack. 3. Push the value (REF.FUNC_ADDR a) to the stack. - 4. Execute the instruction (CALL_REF tu). + 4. Execute the instruction (CALL_REF yy). e. If admin_u0 is of the case REF.NULL, then: 1) Trap. diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 05db82b05f..d3fb161118 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -69,7 +69,7 @@ $$ \mbox{(table type)} & {\mathit{tabletype}} &::=& {\mathit{limits}}~{\mathit{reftype}} \\ \mbox{(memory type)} & {\mathit{memtype}} &::=& {\mathit{limits}}~\mathsf{i{\scriptstyle8}} \\[0.8ex] {} \\[-2ex] -\mbox{(external type)} & {\mathit{externtype}} &::=& \mathsf{func}~{\mathit{deftype}} ~|~ \mathsf{global}~{\mathit{globaltype}} ~|~ \mathsf{table}~{\mathit{tabletype}} ~|~ \mathsf{mem}~{\mathit{memtype}} \\ +\mbox{(external type)} & {\mathit{externtype}} &::=& \mathsf{func}~{\mathit{typeuse}} ~|~ \mathsf{global}~{\mathit{globaltype}} ~|~ \mathsf{table}~{\mathit{tabletype}} ~|~ \mathsf{mem}~{\mathit{memtype}} \\ \end{array} $$