More todos

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 = ...

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 = ...

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") = ...

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

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)
 

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:

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 = ...

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)

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
 
 

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) ^ "`")