Wasm-DSL · rossberg · Sep 4, 2024 · Aug 2, 2024 · Aug 2, 2024 · Aug 2, 2024
diff --git a/spectec/spec/wasm-1.0/6-typing.watsup b/spectec/spec/wasm-1.0/6-typing.watsup
@@ -136,7 +136,7 @@ rule Instrs_ok/empty:
 rule Instrs_ok/seq:
   C |- instr_1 instr_2* : t_1* -> t_3*
   -- Instr_ok: C |- instr_1 : t_1* -> t_2*
-  -- Instrs_ok: C |- instr_2 : t_2* -> t_3*
+  -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/frame:
   C |- instr* : t* t_1* -> t* t_2*

diff --git a/spectec/spec/wasm-1.0/8-reduction.watsup b/spectec/spec/wasm-1.0/8-reduction.watsup
@@ -21,7 +21,7 @@ rule Steps/refl:
 rule Steps/trans:
   z; admininstr*  ~>*  z''; admininstr''*
   -- Step: z; admininstr*  ~>  z'; admininstr'*
-  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+  -- Steps: z'; admininstr'*  ~>*  z''; admininstr''*
 
 
 ;; Expressions

diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup
@@ -153,7 +153,7 @@ rule Instrs_ok/empty:
 rule Instrs_ok/seq:
   C |- instr_1 instr_2* : t_1* -> t_3*
   -- Instr_ok: C |- instr_1 : t_1* -> t_2*
-  -- Instrs_ok: C |- instr_2 : t_2* -> t_3*
+  -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/sub:
   C |- instr* : t'_1* -> t'_2*

diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -21,7 +21,7 @@ rule Steps/refl:
 rule Steps/trans:
   z; admininstr*  ~>*  z''; admininstr''*
   -- Step: z; admininstr*  ~>  z'; admininstr'*
-  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+  -- Steps: z'; admininstr'*  ~>*  z''; admininstr''*
 
 
 ;; Expressions

diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -1402,5 +1402,5 @@ rule Globals_ok/empty:
 
 rule Globals_ok/cons:
   C |- global_1 global* : gt_1 gt*
-  -- Global_ok: C |- global : gt_1
+  -- Global_ok: C |- global_1 : gt_1
   -- Globals_ok: C ++ {GLOBALS gt_1} |- global* : gt*
diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup
@@ -21,7 +21,7 @@ rule Steps/refl:
 rule Steps/trans:
   z; instr*  ~>*  z''; instr''*
   -- Step: z; instr*  ~>  z'; instr'*
-  -- Steps: z'; instr'  ~>*  z''; instr''*
+  -- Steps: z'; instr'*  ~>*  z''; instr''*
 
 
 ;; Expressions

diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml
@@ -58,7 +58,7 @@ let tupE ?(at = no) ~note el = TupE el |> mk_expr at note
 let caseE ?(at = no) ~note (op, el) = CaseE (op, el) |> mk_expr at note
 let callE ?(at = no) ~note (id, el) = CallE (id, el) |> mk_expr at note
 let invCallE ?(at = no) ~note (id, il, el) = InvCallE (id, il, el) |> mk_expr at note
-let iterE ?(at = no) ~note (e, idl, it) = IterE (e, idl, it) |> mk_expr at note
+let iterE ?(at = no) ~note (e, ite) = IterE (e, ite) |> mk_expr at note
 let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
 let listE ?(at = no) ~note el = ListE el |> mk_expr at note
 let arityE ?(at = no) ~note e = ArityE e |> mk_expr at note
@@ -105,6 +105,10 @@ let zero = numV Z.zero
 let one = numV Z.one
 let empty_list = listV [||]
 let singleton v = listV [|v|]
+let iter_var ?(at = no) x iter t =
+  let xs = x ^ (match iter with Opt -> "?" | _ -> "*") in
+  let il_iter = match iter with Opt -> Il.Ast.Opt | _ -> Il.Ast.List in
+  iterE (varE x ~at:at ~note:t, (iter, [x, varE xs ~at:at ~note:(Il.Ast.IterT (t, il_iter) $ t.at)])) ~at:at ~note:t
 
 
 let some x = caseV (x, [optV (Some (tupV []))])
@@ -191,6 +195,10 @@ let unwrap_listv: value -> value growable_array = function
 let unwrap_listv_to_array (v: value): value array = !(unwrap_listv v)
 let unwrap_listv_to_list (v: value): value list = unwrap_listv_to_array v |> Array.to_list
 
+let unwrap_seqv_to_list: value -> value list = function
+  | OptV opt -> Option.to_list opt
+  | ListV arr -> Array.to_list !arr
+  | v -> fail_value "unwrap_seqv_to_list" v
 let unwrap_seq_to_array: value -> value array = function
   | OptV opt -> opt |> Option.to_list |> Array.of_list
   | v -> unwrap_listv_to_array v

diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
@@ -97,7 +97,7 @@ and expr' =
   | CaseE of mixop * expr list                    (* mixop `(` expr* `)` -- CaseE *)
   | CallE of id * arg list                        (* id `(` expr* `)` *)
   | InvCallE of id * int option list * arg list   (* id`_`int*`^-1(` expr* `)` *)
-  | IterE of expr * id list * iter                (* expr (`{` id* `}`)* *)
+  | IterE of expr * iterexp                       (* expr (`{` id* `}`)* *)
   | OptE of expr option                           (* expr?  *)
   | ListE of expr list                            (* `[` expr* `]` *)
   | ArityE of expr                                (* "the arity of expr" *)
@@ -137,6 +137,8 @@ and arg' =
   | TypA of typ
   | DefA of id
 
+and iterexp = iter * (id * expr) list
+
 (* Instructions *)
 
 type instr = (instr', int) note_phrase

diff --git a/spectec/src/al/eq.ml b/spectec/src/al/eq.ml
@@ -4,10 +4,14 @@ open Source
 
 let eq_list eq l1 l2 =
   List.length l1 = List.length l2 && List.for_all2 eq l1 l2
+let eq_pair eqx eqy (x1, y1) (x2, y2) =
+  eqx x1 x2 && eqy y1 y2
+
+let eq_id = (=)
 
 let rec eq_expr e1 e2 =
   match e1.it, e2.it with
-  | VarE id1, VarE id2 -> id1 = id2
+  | VarE id1, VarE id2 -> eq_id id1 id2
   | NumE n1, NumE n2 -> n1 = n2
   | BoolE b1, BoolE b2 -> b1 = b2
   | UnE (unop1, e1), UnE (unop2, e2) -> unop1 = unop2 && eq_expr e1 e2
@@ -28,8 +32,8 @@ let rec eq_expr e1 e2 =
   | CallE (i1, al1), CallE (i2, al2) -> i1 = i2 && eq_args al1 al2
   | InvCallE (i1, nl1, al1), InvCallE (i2, nl2, al2) ->
     i1 = i2 && List.for_all2 (=) nl1 nl2 && eq_args al1 al2
-  | IterE (e1, il1, it1), IterE (e2, il2, it2) ->
-    eq_expr e1 e2 && il1 = il2 && it1 = it2
+  | IterE (e1, ie1), IterE (e2, ie2) ->
+    eq_expr e1 e2 && eq_iterexp ie1 ie2
   | OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
   | ListE el1, ListE el2 -> eq_exprs el1 el2
   | ArityE e1, ArityE e2 -> eq_expr e1 e2
@@ -73,6 +77,15 @@ and eq_expr_record r1 r2 =
 and eq_exprs el1 el2 = eq_list eq_expr el1 el2
 
 
+and eq_iter i1 i2 =
+  match i1, i2 with
+  | Opt, Opt -> true
+  | List, List -> true
+  | List1, List1 -> true
+  | ListN (e1, id_opt1), ListN (e2, id_opt2) -> eq_expr e1 e2 && Option.equal eq_id id_opt1 id_opt2
+  | _ -> false
+
+
 and eq_path p1 p2 =
   match p1.it, p2.it with
   | IdxP e1, IdxP e2 -> eq_expr e1 e2
@@ -92,6 +105,11 @@ and eq_arg a1 a2 =
 
 and eq_args al1 al2 = eq_list eq_arg al1 al2
 
+
+and eq_iterexp (iter1, xes1) (iter2, xes2) =
+  eq_iter iter1 iter2 && eq_list (eq_pair eq_id eq_expr) xes1 xes2
+
+
 let rec eq_instr i1 i2 =
   match i1.it, i2.it with
   | IfI (e1, il11, il12), IfI (e2, il21, il22) ->
@@ -111,7 +129,7 @@ let rec eq_instr i1 i2 =
   | ReturnI e_opt1, ReturnI e_opt2 -> eq_expr_opt e_opt1 e_opt2
   | ExecuteI e1, ExecuteI e2
   | ExecuteSeqI e1, ExecuteSeqI e2 -> eq_expr e1 e2
-  | PerformI (id1, al1), PerformI (id2, al2) -> id1 = id2 && eq_args al1 al2
+  | PerformI (id1, al1), PerformI (id2, al2) -> eq_id id1 id2 && eq_args al1 al2
   | ExitI a1, ExitI a2 -> El.Atom.eq a1 a2
   | ReplaceI (e11, p1, e12), ReplaceI (e21, p2, e22) ->
     eq_expr e11 e21 && eq_path p1 p2 && eq_expr e12 e22

diff --git a/spectec/src/al/free.ml b/spectec/src/al/free.ml
@@ -2,15 +2,18 @@ open Ast
 open Util
 open Source
 
-(* TODO: Change list to set *)
 module IdSet = Set.Make (String)
 
 (* Expressions *)
 
 let (@) = IdSet.union
+let (-) = IdSet.diff
 let free_opt free_x xo = Option.(value (map free_x xo) ~default:IdSet.empty)
 let free_list free_x xs = List.(fold_left IdSet.union IdSet.empty (map free_x xs))
 
+
+let free_id = IdSet.singleton
+
 let rec free_expr expr =
   match expr.it with
   | NumE _
@@ -22,7 +25,7 @@ let rec free_expr expr =
   | ContextKindE _
   | YetE _ -> IdSet.empty
   | VarE id
-  | SubE (id, _) -> IdSet.singleton id
+  | SubE (id, _) -> free_id id
   | UnE (_, e)
   | LenE e
   | ArityE e
@@ -44,7 +47,12 @@ let rec free_expr expr =
   | ExtE (e1, ps, e2, _)
   | UpdE (e1, ps, e2) -> free_expr e1 @ free_list free_path ps @ free_expr e2
   | OptE e_opt -> free_opt free_expr e_opt
-  | IterE (e, _, i) -> free_expr e @ free_iter i
+  | IterE (e, ie) ->
+    (* We look for semantic free variables, not the syntactic free variables. *)
+    (* Therefore, in the expression `x*{x <- xs}`, xs is free, but x is not. *)
+    let free1 = free_expr e in
+    let bound, free2 = free_iterexp ie in
+    (free1 - bound) @ free2
   | MatchE (e1, e2) -> free_expr e1 @ free_expr e2
   | TopLabelE
   | TopFrameE
@@ -76,13 +84,23 @@ and free_path path =
 
 
 (* Args *)
+
 and free_arg arg =
   match arg.it with
   | ExpA e -> free_expr e
   | TypA _
   | DefA _ -> IdSet.empty
 
 
+(* Iter exps *)
+
+and free_iterexp (iter, xes) =
+  let xs, es = List.split xes in
+  let bound = free_list free_id xs in
+  let free = free_iter iter @ free_list free_expr es in
+  bound, free
+
+
 (* Instructions *)
 
 let rec free_instr instr =

diff --git a/spectec/src/al/free.mli b/spectec/src/al/free.mli
@@ -1,6 +1,6 @@
 open Ast
 
-module IdSet : Set.S with type elt = string
+module IdSet : Set.S with type elt = string with type t = Set.Make(String).t
 
 val free_list : ('a -> IdSet.t) -> 'a list -> IdSet.t
 val free_expr : expr -> IdSet.t

diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml
@@ -177,7 +177,7 @@ and string_of_expr expr =
     sprintf "label(%s, %s)" (string_of_expr e1) (string_of_expr e2)
   | VarE id -> id
   | SubE (id, _) -> id
-  | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
+  | IterE (e, ie) -> string_of_expr e ^ string_of_iterexp ie
   | CaseE ([{ it=Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
   | CaseE ([[ atom ]], []) -> string_of_atom atom
@@ -241,6 +241,14 @@ and string_of_arg arg =
 and string_of_args sep = string_of_list string_of_arg sep
 
 
+
+(* Iter exps *)
+
+and string_of_iterexp (iter, xes) =
+  string_of_iter iter ^ "{" ^ String.concat ", "
+    (List.map (fun (id, e) -> id ^ " <- " ^ string_of_expr e) xes) ^ "}"
+
+
 (* Instructions *)
 
 let _index = ref 0
@@ -382,11 +390,6 @@ let string_of_algorithm algo =
 
 (* Wasm type *)
 
-(* Names *)
-
-let structured_string_of_ids ids =
-  "[" ^ String.concat ", " ids ^ "]"
-
 
 (* Values *)
 
@@ -510,14 +513,14 @@ and structured_string_of_expr expr =
     ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
   | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
-  | IterE (e, ids, iter) ->
+  | IterE (e, (iter, xes)) ->
     "IterE ("
     ^ structured_string_of_expr e
-    ^ ", "
-    ^ structured_string_of_ids ids
-    ^ ", "
-    ^ string_of_iter iter
-    ^ ")"
+    ^ ", ("
+    ^ structured_string_of_iter iter
+    ^ ", {"
+    ^ string_of_list (fun (x, e) -> x ^ structured_string_of_expr e) ", " xes
+    ^ "}))"
   | CaseE (op, el) ->
     "CaseE (" ^ string_of_mixop op
     ^ ", [" ^ structured_string_of_exprs el ^ "])"

diff --git a/spectec/src/al/valid.ml b/spectec/src/al/valid.ml
@@ -159,9 +159,7 @@ and unify_typs_opt : typ list -> typ option = function
 and ground_typ_of (typ: typ) : typ =
   match typ.it with
   | VarT (id, _) when Env.mem_var !env id ->
-    let typ', iters = Env.find_var !env id in
-    (* TODO: local var type contains iter *)
-    assert (iters = []);
+    let typ' = Env.find_var !env id in
     if Il.Eq.eq_typ typ typ' then typ else ground_typ_of typ'
   (* NOTE: Consider `fN` as a `NumT` to prevent diverging ground type *)
   | VarT (id, _) when id.it = "fN" -> NumT RealT $ typ.at
@@ -299,7 +297,7 @@ let check_call source id args result_typ =
       match arg.it, param.it with
       | ExpA expr, ExpP (_, typ') -> check_match source expr.note typ'
       (* Add local variable typ *)
-      | TypA typ1, TypP id -> env := Env.bind_var !env id (typ1, [])
+      | TypA typ1, TypP id -> env := Env.bind_var !env id typ1
       | DefA aid, DefP (_, pparams, ptyp) ->
         (match Env.find_opt_def !env (aid $ no_region) with
         | Some (aparams, atyp, _) -> 
@@ -490,7 +488,7 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
     check_case source exprs typ
   | CallE (id, args) -> check_call source id args expr.note
   | InvCallE (id, indices, args) -> check_inv_call source id indices args expr.note;
-  | IterE (expr1, _, iter) ->
+  | IterE (expr1, (iter, _xes)) -> (* TODO *)
     if not (expr1.note.it = BoolT && expr.note.it = BoolT) then
       (match iter with
       | Opt ->

diff --git a/spectec/src/al/walk.ml b/spectec/src/al/walk.ml
@@ -57,7 +57,10 @@ let walk_expr (walker: unit_walker) (expr: expr) : unit =
     walker.walk_expr walker e1; List.iter (walk_path walker) ps;
     walker.walk_expr walker e2
   | OptE e_opt -> Option.iter (walker.walk_expr walker) e_opt
-  | IterE (e, _, i) -> walker.walk_expr walker e; walk_iter walker i
+  | IterE (e, (iter, xes)) ->
+    walker.walk_expr walker e;
+    walker.walk_iter walker iter;
+    List.iter (fun (_, e) -> walker.walk_expr walker e) xes
 
 let walk_instr (walker: unit_walker) (instr: instr) : unit =
   match instr.it with
@@ -155,7 +158,7 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | LabelE (e1, e2) -> LabelE (walk_expr e1, walk_expr e2)
     | ContE e' -> ContE (walk_expr e')
     | ChooseE e' -> ChooseE (walk_expr e')
-    | IterE (e, ids, iter) -> IterE (walk_expr e, ids, walk_iter iter)
+    | IterE (e, (iter, xes)) -> IterE (walk_expr e, (walk_iter iter, List.map (fun (x, e) -> (x, walk_expr e)) xes))
     | IsCaseOfE (e, a) -> IsCaseOfE (walk_expr e, a)
     | IsDefinedE e -> IsDefinedE (walk_expr e)
     | HasTypeE (e, t) -> HasTypeE(walk_expr e, t)
@@ -277,7 +280,7 @@ let rec walk_expr f e =
       | ChooseE e' -> ChooseE (new_ e')
       | VarE id -> VarE id
       | SubE (id, t) -> SubE (id, t)
-      | IterE (e, ids, iter) -> IterE (new_ e, ids, iter)
+      | IterE (e, (iter, xes)) -> IterE (new_ e, (iter, List.map (fun (x, e) -> (x, new_ e)) xes))
       | ContextKindE _ -> e.it
       | IsCaseOfE (e, a) -> IsCaseOfE (new_ e, a)
       | IsDefinedE e -> IsDefinedE (new_ e)