Wasm-DSL · rossberg · Mar 6, 2024 · Mar 6, 2024
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
@@ -5,18 +5,18 @@ Instructions
 ------------
 
 :ref:`Instructions <syntax-instr>` are classified by :ref:`instruction types <syntax-instrtype>` that describe how they manipulate the :ref:`operand stack <stack>` and initialize :ref:`locals <syntax-local>`:
-A type ${instrtype: t_1* ->x* t_2*} describes the required input stack with argument values of types ${:t_1*}` that an instruction pops off
+A type ${instrtype: t_1* ->_(x*) t_2*} describes the required input stack with argument values of types ${:t_1*}` that an instruction pops off
 and the provided output stack with result values of types ${:t_2*} that it pushes back.
 Moreover, it enumerates the :ref:`indices <syntax-localidx>` ${:x*} of locals that have been set by the instruction.
 In most cases, this is empty.
 
 .. note::
    For example, the instruction ${:BINOP I32 ADD} has type ${: I32 I32 -> I32},
    consuming two ${:I32} values and producing one.
-   The instruction ${:LOCAL.SET x} has type ${instrtype: t ->x eps}, provided ${:t} is the type declared for the local ${:x}.
+   The instruction ${:LOCAL.SET x} has type ${instrtype: t ->_(x) eps}, provided ${:t} is the type declared for the local ${:x}.
 
 Typing extends to :ref:`instruction sequences <valid-instr-seq>` ${:instr*}.
-Such a sequence has an instruction type ${instrtype: t_1* ->x* t_2*} if the accumulative effect of executing the instructions is consuming values of types ${:t_1*} off the operand stack, pushing new values of types ${:t_2*}, and setting all locals ${:x*}.
+Such a sequence has an instruction type ${instrtype: t_1* ->_(x*) t_2*} if the accumulative effect of executing the instructions is consuming values of types ${:t_1*} off the operand stack, pushing new values of types ${:t_2*}, and setting all locals ${:x*}.
 
 .. _polymorphism:
 

diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -9,7 +9,10 @@ syntax localtype hint(desc "local type") =
   init valtype
 
 syntax instrtype hint(desc "instruction type") =
-  resulttype -> localidx* resulttype
+  resulttype ->_ localidx* resulttype  hint(show %0 `->_ %2 %3)
+
+syntax finstrtype =
+  resulttype -> resulttype  ;; TODO: HACK, shouldn't be needed
 
 
 syntax context hint(desc "context") =
@@ -98,7 +101,7 @@ rule Resulttype_ok:
   -- (Valtype_ok: C |- t : OK)*
 
 rule Instrtype_ok:
-  C |- t_1* -> x* t_2* : OK
+  C |- t_1* ->_(x*) t_2* : OK
   -- Resulttype_ok: C |- t_1* : OK
   -- Resulttype_ok: C |- t_2* : OK
   -- (if C.LOCAL[x] = lct)*
@@ -381,7 +384,7 @@ rule Resulttype_sub:
   -- (Valtype_sub: C |- t_1 <: t_2)*
 
 rule Instrtype_sub:
-  C |- t_11* ->(x_1*) t_12* <: t_21* ->(x_2*) t_22*
+  C |- t_11* ->_(x_1*) t_12* <: t_21* ->_(x_2*) t_22*
   -- Resulttype_sub: C |- t_21* <: t_11*
   -- Resulttype_sub: C |- t_12* <: t_22*
   -- if x* = $setminus(x_2*, x_1*)
@@ -502,8 +505,6 @@ rule Externtype_sub/mem:
 ;; Instructions
 ;;
 
-syntax finstrtype = resulttype -> resulttype  ;; TODO: HACK, shouldn't be needed
-
 relation Instr_ok: context |- instr : finstrtype    hint(show "T")
 relation Instrf_ok: context |- instr : instrtype    hint(show "T")
 relation Instrs_ok: context |- instr* : instrtype   hint(show "T-instr*")
@@ -514,33 +515,33 @@ relation Expr_ok: context |- expr : resulttype      hint(show "T-expr")
 
 rule Expr_ok:
   C |- instr* : t*
-  -- Instrs_ok: C |- instr* : eps ->(eps) t*
+  -- Instrs_ok: C |- instr* : eps ->_(eps) t*
 
 
 ;; Instruction sequences
 
 rule Instrf_ok/instr:
-  C |- instr : t_1* ->(eps) t_2*
+  C |- instr : t_1* ->_(eps) t_2*
   -- Instr_ok: C |- instr : t_1* -> t_2*
 
 rule Instrs_ok/empty:
-  C |- eps : eps ->(eps) eps
+  C |- eps : eps ->_(eps) eps
 
 rule Instrs_ok/seq:
-  C |- instr_1 instr_2* : t_1* ->(x_1* x_2*) t_3*
+  C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
   -- if (C.LOCAL[x_1] = init t)*
   -- if C' = $with_locals(C, x_1*, (SET t)*)
-  -- Instrf_ok: C |- instr_1 : t_1* ->(x_1*) t_2*
-  -- Instrs_ok: C' |- instr_2* : t_2* ->(x_2*) t_3*
+  -- Instrf_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
+  -- Instrs_ok: C' |- instr_2* : t_2* ->_(x_2*) t_3*
 
 rule Instrs_ok/sub:
   C |- instr* : it'
   -- Instrs_ok: C |- instr* : it
   -- Instrtype_sub: C |- it <: it'
 
 rule Instrs_ok/frame:
-  C |- instr* : t* t_1* ->(x*) (t* t_2*)
-  -- Instrs_ok: C |- instr* : t_1* ->(x*) t_2*
+  C |- instr* : t* t_1* ->_(x*) (t* t_2*)
+  -- Instrs_ok: C |- instr* : t_1* ->_(x*) t_2*
 
 
 ;; Polymorphic instructions
@@ -580,18 +581,18 @@ rule Blocktype_ok/typeidx:
 rule Instr_ok/block:
   C |- BLOCK bt instr* : t_1* -> t_2*
   -- Blocktype_ok: C |- bt : t_1* -> t_2*
-  -- Instrs_ok: C, LABEL (t_2*) |- instr* : t_1* ->(x*) t_2*
+  -- Instrs_ok: C, LABEL (t_2*) |- instr* : t_1* ->_(x*) t_2*
 
 rule Instr_ok/loop:
   C |- LOOP bt instr* : t_1* -> t_2*
   -- Blocktype_ok: C |- bt : t_1* -> t_2*
-  -- Instrs_ok: C, LABEL (t_1*) |- instr* : t_1* ->(x*) t_2*
+  -- Instrs_ok: C, LABEL (t_1*) |- instr* : t_1* ->_(x*) t_2*
 
 rule Instr_ok/if:
   C |- IF bt instr_1* ELSE instr_2* : t_1* I32 -> t_2*
   -- Blocktype_ok: C |- bt : t_1* -> t_2*
-  -- Instrs_ok: C, LABEL (t_2*) |- instr_1* : t_1* ->(x_1*) t_2*
-  -- Instrs_ok: C, LABEL (t_2*) |- instr_2* : t_1* ->(x_2*) t_2*
+  -- Instrs_ok: C, LABEL (t_2*) |- instr_1* : t_1* ->_(x_1*) t_2*
+  -- Instrs_ok: C, LABEL (t_2*) |- instr_2* : t_1* ->_(x_2*) t_2*
 
 
 ;; Branch instructions
@@ -923,11 +924,11 @@ rule Instr_ok/local.get:
   -- if C.LOCAL[x] = init t
 
 rule Instrf_ok/local.set:
-  C |- LOCAL.SET x : t ->(x) eps
+  C |- LOCAL.SET x : t ->_(x) eps
   -- if C.LOCAL[x] = init t
 
 rule Instrf_ok/local.tee:
-  C |- LOCAL.TEE x : t ->(x) t
+  C |- LOCAL.TEE x : t ->_(x) t
   -- if C.LOCAL[x] = init t
 
 

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -70,21 +70,27 @@ let env_hints name map id hints =
     map := Map.add id (hintexp::exps) !map
   ) hints
 
+let env_atom map atom id1 hints =
+  let id = El.Print.string_of_atom atom in
+  env_hints "show" map (typed_id id id1) hints
+
 let env_typfield env id1 = function
-  | Elem ({it = Atom id; _}, _, hints) ->
-    env_hints "show" env.show_field (typed_id id id1) hints
+  | Elem (atom, _, hints) -> env_atom env.show_field atom id1 hints
   | _ -> ()
 
 let env_typcase env id1 = function
-  | Elem ({it = Atom id; _}, _, hints) ->
-    env_hints "show" env.show_case (typed_id id id1) hints
+  | Elem (atom, _, hints) -> env_atom env.show_case atom id1 hints
   | _ -> ()
 
-let env_typcon env id1 = function
-  | (({it = SeqT ts; _}, _prems), hints) ->
+let env_typcon env id1 ((t, _prems), hints) =
+  match t.it with
+  | AtomT atom
+  | InfixT (_, atom, _)
+  | BrackT (atom, _, _) ->
+    env_atom env.show_case atom id1 hints
+  | SeqT ts ->
     (match List.find_opt is_atom_typ ts with
-    | Some {it = AtomT {it = Atom id; _}; _} ->
-      env_hints "show" env.show_case (typed_id id id1) hints
+    | Some {it = AtomT atom; _} -> env_atom env.show_case atom id1 hints
     | _ -> ()
     )
   | _ -> ()
@@ -194,6 +200,12 @@ let as_paren_exp e =
 let as_tup_exp e =
   match e.it with
   | TupE es -> es
+  | ParenE (e1, _) -> [e1]
+  | _ -> [e]
+
+let as_seq_exp e =
+  match e.it with
+  | SeqE es -> es
   | _ -> [e]
 
 let rec fuse_exp e deep =
@@ -284,7 +296,10 @@ and expand_exp args i e =
   | HoleE (`Num j) ->
     (match List.nth_opt args j with
     | None -> raise Arity_mismatch
-    | Some arg -> i := j + 1; CallE ("" $ e.at, [arg])
+    | Some arg -> i := j + 1;
+      match !(arg.it) with
+      | ExpA eJ -> eJ.it
+      | _ -> CallE ("" $ e.at, [arg])
     )
   | HoleE `Next -> (expand_exp args i (HoleE (`Num !i) $ e.at)).it
   | HoleE `Rest ->
@@ -323,6 +338,19 @@ and expand_arg args i a =
   ) $ a.at
 
 
+let ends_sub id = id <> "" && id.[String.length id - 1] = '_'
+let chop_sub id = String.sub id 0 (String.length id - 1)
+
+let ends_sub_atom atom = ends_sub (Il.Atom.string_of_atom atom)
+let chop_sub_atom atom =
+  (match atom.it with
+  | Il.Atom.Atom id -> Il.Atom.Atom (chop_sub id)
+  | Il.Atom.ArrowSub -> Il.Atom.Arrow
+  | Il.Atom.Arrow2Sub -> Il.Atom.Arrow2
+  | _ -> assert false
+  ) $$ atom.at % atom.note
+
+
 (* Attempt to show-expand the application `id(args)`, using the hints `show`,
  * and the function `render` for rendering the resulting expression.
  * If no hint can be found, fall back to the default of rendering `f`.
@@ -332,8 +360,7 @@ let render_expand render env (show : exp list Map.t ref) id args f =
   | None -> f ()
   | Some showexps ->
     let rec attempt = function
-      | [] ->
-      f ()
+      | [] -> f ()
       | showexp::showexps' ->
         try
           let e = expand_exp args (ref 1) showexp in
@@ -346,12 +373,9 @@ let render_expand render env (show : exp list Map.t ref) id args f =
            * e.g., using CONST for both instruction and relation. *)
     in attempt showexps
 
-let ends_sub id = id <> "" && id.[String.length id - 1] = '_'
-let chop_sub id = String.sub id 0 (String.length id - 1)
-
 (* Same as render_expand, but with rendered id funnelled as argument 0 *)
 let render_expand_id render_id render_exp env show id args f =
-  let atom = Atom (" " ^ render_id env id) $$ id.at % (ref "") in
+  let atom = Il.Atom.Atom (" " ^ render_id env id) $$ id.at % (ref "") in
   let arg0 = arg_of_exp (AtomE atom $ id.at) in
   render_expand render_exp env show id (arg0::args) f
 
@@ -386,9 +410,9 @@ let rec chop_tick id =
 let rec chop_sub_exp e =
   match e.it with
   | VarE (id, []) when ends_sub id.it -> Some (VarE (chop_sub id.it $ id.at, []) $ e.at)
-  | AtomE {it = Atom "_"; _} -> None
-  | AtomE {it = Atom id; at; note} when ends_sub id ->
-    Some (AtomE {it = Atom (chop_sub id); at; note} $ e.at)
+  | AtomE atom when atom.it = Il.Atom.Atom "_" -> None
+  | AtomE atom when ends_sub_atom atom ->
+    Some (AtomE (chop_sub_atom atom) $ e.at)
   | FuseE (e1, e2) ->
     (match chop_sub_exp e2 with
     | Some e2' -> Some (FuseE (e1, e2') $ e.at)
@@ -480,6 +504,7 @@ let render_atom env atom =
         ("cannot infer type of notation `" ^ El.Print.string_of_atom atom ^ "`")
   in
   let s =
+    let open Il.Atom in
     match atom.it with
     | Atom id when id.[0] = '_' && id <> "_" -> ""
     (* HACK: inject literal, already rendered stuff *)
@@ -494,8 +519,8 @@ let render_atom env atom =
     | Semicolon -> if macros then "\\semicolon" else ";"
     | Backslash -> "\\setminus"
     | In -> "\\in"
-    | Arrow -> "\\rightarrow"
-    | Arrow2 -> "\\Rightarrow"
+    | Arrow | ArrowSub -> "\\rightarrow"
+    | Arrow2 | Arrow2Sub -> "\\Rightarrow"
     | Colon -> if macros then "\\colon" else ":"
     | Sub -> "\\leq"
     | Sup -> "\\geq"
@@ -578,9 +603,9 @@ and render_typ env t =
   *)
   match t.it with
   | StrT tfs ->
-    "\\{\\; " ^
+    "\\{ " ^
     "\\begin{array}[t]{@{}l@{}l@{}}\n" ^
-    concat_map_nl ",\\; " "\\\\\n  " (render_typfield env) tfs ^ " \\;\\}" ^
+    concat_map_nl ",\\; " "\\\\\n  " (render_typfield env) tfs ^ " \\}" ^
     "\\end{array}"
   | CaseT (dots1, ts, tcases, dots2) ->
     altern_map_nl " ~|~ " " \\\\ &&|&\n" Fun.id
@@ -628,7 +653,8 @@ and render_exp env e =
   match e.it with
   | VarE (id, args) ->
     render_apply render_varid render_exp env env.show_typ id args
-  | BoolE b -> render_atom env (Atom (string_of_bool b) $$ e.at % ref "bool")
+  | BoolE b ->
+    render_atom env (Il.Atom.Atom (string_of_bool b) $$ e.at % ref "bool")
   | NatE (DecOp, n) -> Z.to_string n
   | NatE (HexOp, n) ->
     let fmt =
@@ -657,14 +683,14 @@ and render_exp env e =
       (El.Print.string_of_atom atom $ e.at) [arg_of_exp e]
       (fun () -> render_atom env atom)
   | SeqE es ->
-    (match List.find_opt (is_atom_exp_with_show env) es with
-    | Some {it = AtomE atom; _} ->
-      let args = List.map arg_of_exp es in
-      render_expand render_exp env env.show_case
-        (El.Print.string_of_atom atom $ atom.at) args
-        (fun () -> render_exp_seq env es)
-    | _ -> render_exp_seq env es
-    )
+    let id =
+      match List.find_opt (is_atom_exp_with_show env) es with
+      | Some {it = AtomE atom; _} -> El.Print.string_of_atom atom $ atom.at
+      | _ -> "" $ e.at
+    in
+    let args = List.map arg_of_exp es in
+    render_expand render_exp env env.show_case id args
+      (fun () -> render_exp_seq env es)
   | IdxE (e1, e2) -> render_exp env e1 ^ "{}[" ^ render_exp env e2 ^ "]"
   | SliceE (e1, e2, e3) ->
     render_exp env e1 ^
@@ -690,12 +716,24 @@ and render_exp env e =
     render_exp env e1
   | ParenE (e1, _) -> "(" ^ render_exp env e1 ^ ")"
   | TupE es -> "(" ^ render_exps ",\\, " env es ^ ")"
-  | InfixE ({it = SeqE []; _}, atom, e2) ->
-    "{" ^ space (render_atom env) atom ^ "}\\;" ^ render_exp env e2
   | InfixE (e1, atom, e2) ->
-    render_exp env e1 ^ space (render_atom env) atom ^ render_exp env e2
+    let id = El.Print.string_of_atom atom $ atom.at in
+    let e = AtomE atom $ atom.at in
+    let args = List.map arg_of_exp (as_seq_exp e1 @ [e] @ as_seq_exp e2) in
+    render_expand render_exp env env.show_case id args
+      (fun () ->
+        (match e1.it with
+        | SeqE [] -> "{" ^ space (render_atom env) atom ^ "}\\;"
+        | _ -> render_exp env e1 ^ space (render_atom env) atom
+        ) ^ render_exp env e2
+      )
   | BrackE (l, e1, r) ->
-    render_atom env l ^ render_exp env e1 ^ render_atom env r
+    let id = El.Print.string_of_atom l $ l.at in
+    let el = AtomE l $ l.at in
+    let er = AtomE r $ r.at in
+    let args = List.map arg_of_exp ([el] @ as_seq_exp e1 @ [er]) in
+    render_expand render_exp env env.show_case id args
+      (fun () -> render_atom env l ^ render_exp env e1 ^ render_atom env r)
   | CallE (id, [arg]) when id.it = "" -> (* expansion result only *)
     render_arg env arg
   | CallE (id, args) when id.it = "" ->  (* expansion result only *)

diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml
@@ -84,7 +84,7 @@ let vrule_group_to_prose ((_name, vrules): vrule_group) =
 
   (* name *)
   let winstr_name = match winstr.it with
-  | Ast.CaseE (({it = Ast.Atom winstr_name; _}::_)::_, _) -> winstr_name
+  | Ast.CaseE (({it = Il.Atom.Atom winstr_name; _}::_)::_, _) -> winstr_name
   | _ -> failwith "unreachable"
   in
   let name = kwd winstr_name winstr.note in

diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
@@ -47,16 +47,16 @@ let al_to_el_binop = function
    *)
 let al_to_el_infixop op =
   let elatom, typ = match op with
-  | "->" -> Some El.Ast.Arrow, ""
-  | "X" -> Some (El.Ast.Atom "X"), "shape"
+  | "->" -> Some Il.Atom.Arrow, ""
+  | "X" -> Some (Il.Atom.Atom "X"), "shape"
   | _ -> None, ""
   in
   Option.map
     (fun elatom -> elatom $$ no_region % ref typ)
     elatom
 
 let al_to_el_kwd (id, typ) = 
-  let elatom = El.Ast.Atom id in
+  let elatom = Il.Atom.Atom id in
   elatom $$ no_region % (ref typ)
 
 let rec al_to_el_iter iter = match iter with