[spectec] Clean up IL semantics and elaborator (WIP)

interpreter/binary/decode.ml

@@ -920,6 +920,7 @@ let rec instr s =
     | 0xebl -> f32x4_pmax
     | 0xecl -> f64x2_abs
     | 0xedl -> f64x2_neg
+    | 0xeel as n -> illegal s pos (I32.to_int_u n)
     | 0xefl -> f64x2_sqrt
     | 0xf0l -> f64x2_add
     | 0xf1l -> f64x2_sub

specification/wasm-3.0/6.1-text.values.spectec

@@ -153,7 +153,7 @@ syntax I = idctxt
 
 def $concat_idctxt(idctxt*) : idctxt  hint(show (++) %)
 def $concat_idctxt(eps) = {}
-def $concat_idctxt(I I') = I ++ $concat_idctxt(I'*)
+def $concat_idctxt(I I'*) = I ++ $concat_idctxt(I'*)
 
 
 relation Idctxt_ok: |- idctxt : OK

specification/wasm-3.0/6.3-text.modules.spectec → specification/wasm-3.0/6.4-text.modules.spectec

@@ -56,7 +56,7 @@ grammar Tlocal_(I)/plain : (local*, idctxt) =
   | ...
 
 grammar Tlocal_(I)/abbrev : (local*, idctxt) =
-  ... | "(" "local" t:Tvaltype_(I)* ")" == ("(" "local" t:Tvaltype_(I) ")")*
+  ... | "(" "local" Tvaltype_(I)* ")" == ("(" "local" Tvaltype_(I) ")")*
 
 
 ;; Data segments
@@ -97,8 +97,8 @@ grammar Telem_(I)/plain : (elem, idctxt) =
   | ...
 
 grammar Telem_(I)/abbrev : (elem, idctxt) = ...
-  | "(" "elem" e':Toffset_(I) Tlist(Tfuncidx_(I)) ")" ==
-    "(" "elem" e':Toffset_(I) "func" Tlist(Tfuncidx_(I)) ")"
+  | "(" "elem" Toffset_(I) Tlist(Tfuncidx_(I)) ")" ==
+    "(" "elem" Toffset_(I) "func" Tlist(Tfuncidx_(I)) ")"
 
 grammar Telemlist_(I)/plain : (reftype, expr*) =
   | rt:Treftype_(I) e*:Tlist(Texpr_(I)) => (rt, e*)

spectec/doc/Language.md

@@ -1547,7 +1547,7 @@ params ::= ("(" param*"," ")")?
 param ::=
   (varid ":") typ
   "syntax" synid
-  "grammar" gramid ":" typ
+  "grammar" gramid params ":" typ
   "def" "$" defid params ":" typ
 
 def ::=

spectec/src/al/al_util.ml

@@ -298,21 +298,13 @@ let atom_of_atom' atom' typ = atom' $$ no_region % (Atom.info typ)
 
 let frame_atom = atom_of_name "FRAME_" "evalctx"
 let frameE ?(at = no) ~note (arity, e) =
-  let frame_mixop = [[frame_atom]; [atom_of_atom' Atom.LBrace "evalctx"]; [atom_of_atom' Atom.RBrace "evalctx"]] in
+  let frame_mixop = Mixop.(Seq [Atom frame_atom; Brack (atom_of_atom' Atom.LBrace "evalctx", Arg (), atom_of_atom' Atom.RBrace "evalctx")]) in
   caseE (frame_mixop, [arity; e]) ~at:at ~note:note
 
-
-let get_atom op =
-  match List.find_opt (fun al -> al <> []) op with
-  | Some al -> Some (List.hd al)
-  | None -> None
-
-let name_of_mixop = Mixop.name
-
 (* Il Types *)
 
 (* name for tuple type *)
-let no_name = Il.Ast.VarE ("_" $ no_region) $$ no_region % (Il.Ast.TextT $ no_region)
+let no_name = "_" $ no_region
 let varT id args = Il.Ast.VarT (id $ no_region, args) $ no_region
 let iterT ty iter = Il.Ast.IterT (ty, iter) $ no_region
 let listT ty = iterT ty Il.Ast.List

spectec/src/al/ast.ml

@@ -4,7 +4,7 @@ open Xl
 (* Terminals *)
 
 type atom = Atom.atom
-type mixop = Mixop.mixop
+type mixop = unit Mixop.mixop
 
 (* Types *)
 

spectec/src/al/print.ml

@@ -152,11 +152,11 @@ and string_of_expr expr =
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, ie) -> string_of_expr e ^ string_of_iterexp ie
-  | CaseE ([{ it=Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
+  | CaseE (Mixop.(Seq (Atom { it=Atom.Atom ("CONST" | "VCONST"); _ }::_tl)), hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
-  | CaseE ([[ atom ]], []) -> string_of_atom atom
+  | CaseE (Mixop.Atom atom, []) -> string_of_atom atom
   | CaseE (op, el) ->
-    let op' = List.map (fun al -> String.concat "" (List.map string_of_atom al)) op in
+    let op' = List.map (fun al -> String.concat "" (List.map string_of_atom al)) (Mixop.flatten op) in
     (match op' with
     | [] -> "()"
     | _::tl when List.length tl != List.length el ->

spectec/src/al/valid.ml

@@ -68,7 +68,10 @@ let il_env: IlEnv.t ref = ref IlEnv.empty
 
 let varT s = VarT (s $ no_region, []) $ no_region
 
-let is_trivial_mixop = List.for_all (fun atoms -> List.length atoms = 0)
+let rec is_trivial_mixop = function
+  | Mixop.Arg () -> true
+  | Mixop.Seq mixops -> List.for_all is_trivial_mixop mixops
+  | _ -> false
 
 
 (* Subtyping *)
@@ -128,7 +131,7 @@ let rec unify_deftyp_opt (deftyp: deftyp) : typ option =
   | StructT _ -> None
   | VariantT typcases
   when List.for_all (fun (mixop', _, _) -> is_trivial_mixop mixop') typcases ->
-    typcases |> List.map (fun (_mixop, (_bs, typ, _ps), _hs) -> typ) |> unify_typs_opt
+    typcases |> List.map (fun (_mixop, (typ, _qs, _ps), _hs) -> typ) |> unify_typs_opt
   | _ -> None
 
 and unify_deftyps_opt : deftyp list -> typ option = function
@@ -226,7 +229,7 @@ let rec get_typfields_of_inst (inst: inst) : typfield list =
   match dt.it with
   | StructT typfields -> typfields
   | AliasT typ -> get_typfields typ
-  | VariantT [mixop, (_, typ, _), _] when is_trivial_mixop mixop ->
+  | VariantT [mixop, (typ, _, _), _] when is_trivial_mixop mixop ->
     get_typfields typ
   (* TODO: some variants of struct type *)
   | VariantT _ -> []
@@ -279,7 +282,7 @@ let check_evalctx source typ =
   | _ -> error_mismatch source typ (varT "evalctx")
 
 let check_field source source_typ expr_record typfield =
-  let atom, (_, typ, _), _ = typfield in
+  let atom, (typ, _, _), _ = typfield in
   (* TODO: Use record api *)
   let f e = e |> fst |> Atom.eq atom in
   match List.find_opt f expr_record with
@@ -402,7 +405,7 @@ let check_inv_call source id indices args result_typ =
     | _ ->
       let arg2typ arg = (
         match arg.it with
-        | ExpA exp -> (Il.Ast.VarE ("" $ no_region) $$ no_region % exp.note, exp.note)
+        | ExpA exp -> ("_" $ no_region, exp.note)
         | a -> error_valid (Printf.sprintf "wrong result argument")
           source (Print.string_of_arg (a $ no_region))
       ) in
@@ -443,7 +446,7 @@ let access (source: source) (typ: typ) (path: path) : typ =
   | DotP atom ->
     let typfields = get_typfields typ in
     match List.find_opt (fun (field, _, _) -> Atom.eq field atom) typfields with
-    | Some (_, (_, typ', _), _) -> typ'
+    | Some (_, (typ', _, _), _) -> typ'
     | None -> error_field source typ atom
 
 
@@ -555,20 +558,20 @@ and valid_expr env (expr: expr) : unit =
   | CaseE (op, exprs) ->
     let is_evalctx_id id =
       let evalctx_ids = List.filter_map (fun (mixop, _, _) ->
-        let atom = mixop |> List.hd |> List.hd in
+        let atom = Mixop.flatten mixop |> List.hd |> List.hd in
         match atom.it with
         | Atom.Atom s -> Some s
         | _ -> None
       ) (get_typcases source evalctxT) in
       List.mem id evalctx_ids
     in
-    (match op with
+    (match Mixop.flatten op with
     | [[{ it=Atom id; _ }]] when is_evalctx_id id ->
       check_case source exprs (TupT [] $ no_region)
     | _ -> 
       List.iter (valid_expr env) exprs;
       let tcs = get_typcases source expr.note in
-      let _binds, typ, _prems = find_case source tcs op in
+      let typ, _qs, _prems = find_case source tcs op in
       check_case source exprs typ;
     )
   | CallE (id, args) ->

spectec/src/backend-ast/print.ml

@@ -11,10 +11,7 @@ open Ast
 let bool b = Atom (Bool.to_string b)
 let text t = Atom ("\"" ^ String.escaped t ^ "\"")
 let id x = text x.it
-let mixop op =
-  String.concat "%" (List.map (
-    fun ats -> String.concat "" (List.map Atom.to_string ats)) op
-  ) |> text
+let mixop op = text (Mixop.to_string op)
 
 let num = function
   | `Nat n -> Node ("nat", [Atom (Z.to_string n)])
@@ -86,14 +83,14 @@ and deftyp dt =
   | StructT tfs -> Node ("struct", List.map typfield tfs)
   | VariantT tcs -> Node ("variant", List.map typcase tcs)
 
-and typbind (e, t) =
-  Node ("bind", [exp e; typ t])
+and typbind (x, t) =
+  Node ("bind", [id x; typ t])
 
-and typfield (at, (bs, t, prs), _hints) =
-  Node ("field", mixop [[at]] :: List.map bind bs @ typ t :: List.map prem prs)
+and typfield (at, (t, qs, prs), _hints) =
+  Node ("field", mixop (Mixop.Atom at) :: typ t :: List.map param qs @ List.map prem prs)
 
-and typcase (op, (bs, t, prs), _hints) =
-  Node ("case", mixop op :: List.map bind bs @ typ t :: List.map prem prs)
+and typcase (op, (t, qs, prs), _hints) =
+  Node ("case", mixop op :: typ t :: List.map param qs @ List.map prem prs)
 
 
 (* Expressions *)
@@ -112,7 +109,7 @@ and exp e =
   | UpdE (e1, p, e2) -> Node ("upd", [exp e1; path p; exp e2])
   | ExtE (e1, p, e2) -> Node ("ext", [exp e1; path p; exp e2])
   | StrE efs -> Node ("struct", List.map expfield efs)
-  | DotE (e1, at) -> Node ("dot", [exp e1; mixop [[at]]])
+  | DotE (e1, at) -> Node ("dot", [exp e1; mixop (Mixop.Atom at)])
   | CompE (e1, e2) -> Node ("comp", [exp e1; exp e2])
   | MemE (e1, e2) -> Node ("mem", [exp e1; exp e2])
   | LenE e1 -> Node ("len", [exp e1])
@@ -131,14 +128,14 @@ and exp e =
   | SubE (e1, t1, t2) -> Node ("sub", [typ t1; typ t2; exp e1])
 
 and expfield (at, e) =
-  Node ("field", [mixop [[at]]; exp e])
+  Node ("field", [mixop (Mixop.Atom at); exp e])
 
 and path p =
   match p.it with
   | RootP -> Atom "root"
   | IdxP (p1, e) -> Node ("idx", [path p1; exp e])
   | SliceP (p1, e1, e2) -> Node ("slice", [path p1; exp e1; exp e2])
-  | DotP (p1, at) -> Node ("dot", [path p1; mixop [[at]]])
+  | DotP (p1, at) -> Node ("dot", [path p1; mixop (Mixop.Atom at)])
 
 and iterexp (it, xes) =
   iter it :: List.map (fun (x, e) -> Node ("dom", [id x; exp e])) xes
@@ -179,39 +176,32 @@ and arg a =
   | DefA x -> Node ("def", [id x])
   | GramA g -> Node ("gram", [sym g])
 
-and bind bind =
-  match bind.it with
-  | ExpB (x, t) -> Node ("exp", [id x; typ t])
-  | TypB x -> Node ("typ", [id x])
-  | DefB (x, ps, t) -> Node ("def", [id x] @ List.map param ps @ [typ t])
-  | GramB (x, ps, t) -> Node ("gram", [id x] @ List.map param ps @ [typ t])
-
 and param p =
   match p.it with
   | ExpP (x, t) -> Node ("exp", [id x; typ t])
   | TypP x -> Node ("typ", [id x])
   | DefP (x, ps, t) -> Node ("def", [id x] @ List.map param ps @ [typ t])
-  | GramP (x, t) -> Node ("gram", [id x; typ t])
+  | GramP (x, ps, t) -> Node ("gram", [id x] @ List.map param ps @ [typ t])
 
 let inst inst =
   match inst.it with
-  | InstD (bs, as_, dt) ->
-    Node ("inst", List.map bind bs @ List.map arg as_ @ [deftyp dt])
+  | InstD (ps, as_, dt) ->
+    Node ("inst", List.map param ps @ List.map arg as_ @ [deftyp dt])
 
 let rule rule =
   match rule.it with
-  | RuleD (x, bs, op, e, prs) ->
-    Node ("rule", [id x] @ List.map bind bs @ [mixop op; exp e] @ List.map prem prs)
+  | RuleD (x, ps, op, e, prs) ->
+    Node ("rule", [id x] @ List.map param ps @ [mixop op; exp e] @ List.map prem prs)
 
 let clause clause =
   match clause.it with
-  | DefD (bs, as_, e, prs) ->
-    Node ("clause", List.map bind bs @ List.map arg as_ @ [exp e] @ List.map prem prs)
+  | DefD (ps, as_, e, prs) ->
+    Node ("clause", List.map param ps @ List.map arg as_ @ [exp e] @ List.map prem prs)
 
 let prod prod =
   match prod.it with
-  | ProdD (bs, g, e, prs) ->
-    Node ("prod", List.map bind bs @ [sym g; exp e] @ List.map prem prs)
+  | ProdD (ps, g, e, prs) ->
+    Node ("prod", List.map param ps @ [sym g; exp e] @ List.map prem prs)
 
 let rec def d =
   match d.it with

spectec/src/backend-interpreter/construct.ml

@@ -124,10 +124,7 @@ and al_to_resulttype: value -> resulttype = function
 and al_to_comptype: value -> comptype = function
   | CaseV ("STRUCT", [ ftl ]) -> StructT (al_to_list al_to_fieldtype ftl)
   | CaseV ("ARRAY", [ ft ]) -> ArrayT (al_to_fieldtype ft)
-  | CaseV ("FUNC", [ CaseV ("->", [ rt1; rt2 ]) ]) when !version <= 2 ->
-    FuncT (al_to_resulttype rt1, (al_to_resulttype rt2))
-  | CaseV ("FUNC", [ rt1; rt2 ]) ->
-    FuncT (al_to_resulttype rt1, (al_to_resulttype rt2))
+  | CaseV ("->", [ rt1; rt2 ]) -> FuncT (al_to_resulttype rt1, (al_to_resulttype rt2))
   | v -> error_value "comptype" v
 
 and al_to_subtype: value -> subtype = function
@@ -1139,11 +1136,7 @@ and al_of_resulttype rt = al_of_list al_of_valtype rt
 and al_of_comptype = function
   | StructT ftl -> CaseV ("STRUCT", [ al_of_list al_of_fieldtype ftl ])
   | ArrayT ft -> CaseV ("ARRAY", [ al_of_fieldtype ft ])
-  | FuncT (rt1, rt2) ->
-    if !version <= 2 then
-      CaseV ("FUNC", [ CaseV ("->", [ al_of_resulttype rt1; al_of_resulttype rt2 ])])
-    else
-      CaseV ("FUNC", [ al_of_resulttype rt1; al_of_resulttype rt2 ])
+  | FuncT (rt1, rt2) -> CaseV ("->", [ al_of_resulttype rt1; al_of_resulttype rt2 ])
 
 and al_of_subtype = function
   | SubT (fin, tul, st) ->
@@ -1900,7 +1893,7 @@ let al_of_type ty =
 
     match subtypes with
     | [ subtype ] ->
-      let rt = subtype |> arg_of_case "SUB" 2 |> arg_of_case "FUNC" 0 in
+      let rt = subtype |> arg_of_case "SUB" 2 in
       CaseV ("TYPE", [ rt ])
     | _ -> failwith ("Rectype is not supported in Wasm " ^ (string_of_int !version))
   else

spectec/src/backend-interpreter/host.ml

@@ -22,7 +22,7 @@ let spectest () =
     let code = nullary winstr_tag in
     let ptype = Array.map nullary type_tags in
     let arrow = CaseV ("->", [ listV ptype; listV [||] ]) in
-    let ftype = CaseV ("FUNC", [ listV ptype; listV [||] ]) in
+    let ftype = CaseV ("->", [ listV ptype; listV [||] ]) in
     let dtype =
       CaseV ("_DEF", [
         CaseV ("REC", [
@@ -41,9 +41,9 @@ let spectest () =
     "VALUE", v |> ref
   ] in
 
-  let create_tableinst t elems = StrV [
+  let create_tableinst t refs = StrV [
     "TYPE", t |> ref;
-    "REFS", elems |> ref
+    "REFS", refs |> ref
   ] in
 
   let create_meminst t bytes_ = StrV [

spectec/src/backend-interpreter/interpreter.ml

@@ -342,7 +342,7 @@ and eval_expr env expr =
       | [] -> eval_expr env e2 in
     eval_expr env e1 |> replace ps
   | CaseE (op, el) ->
-    (match (get_atom op) with
+    (match Mixop.head op with
     | Some a -> caseV (Print.string_of_atom a, List.map (eval_expr env) el)
     | None -> caseV ("", List.map (eval_expr env) el)
     )
@@ -370,6 +370,12 @@ and eval_expr env expr =
       raise Exception.OutOfMemory
     else
       Array.make i v |> listV
+  (* HARDCODE: The case where itered variable does not appear in xes.
+    --> Insert itered variable. This was instroduced due to the change of IrerE's ListN. *)
+  | IterE (e1, (ListN (e2, Some x), [])) ->
+    let dummy_expr = VarE "_" $$ no_region % (Il.Ast.VarT ("_" $ no_region, []) $ no_region) in
+    let expr' = {expr with it = IterE (e1, (ListN (e2, Some x), [(x, dummy_expr)]))} in
+    eval_expr env expr'
   | IterE (inner_e, (iter, xes)) ->
     let vs =
       env
@@ -480,7 +486,7 @@ and assign lhs rhs env =
     when List.length lhs_s = Array.length !rhs_s ->
     List.fold_right2 assign lhs_s (Array.to_list !rhs_s) env
   | CaseE (op, lhs_s), CaseV (rhs_tag, rhs_s) when List.length lhs_s = List.length rhs_s ->
-    (match get_atom op with
+    (match Mixop.head op with
     | Some lhs_tag when (Print.string_of_atom lhs_tag) = rhs_tag ->
       List.fold_right2 assign lhs_s rhs_s env
     | None when "" = rhs_tag ->
@@ -600,7 +606,7 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     )
   | PopI e ->
     (match e.it with
-    | CaseE ([{it = Atom.Atom "FRAME_"; _}] :: _, [_; inner_e]) ->
+    | CaseE (op, [_; inner_e]) when (Option.get (Mixop.head op)).it = Atom.Atom "FRAME_" ->
       (match WasmContext.pop_context () with
       | CaseV ("FRAME_", [_; inner_v]), _, _ ->
         let new_env = assign inner_e inner_v env in

spectec/src/backend-latex/render.ml

@@ -1676,7 +1676,7 @@ let render_param env p =
   match p.it with
   | ExpP (id, t) -> if id.it = "_" then render_typ env t else render_varid env id
   | TypP id -> render_typid env id
-  | GramP (id, _t) -> render_gramid env id
+  | GramP (id, _ps, _t) -> render_gramid env id
   | DefP (id, _ps, _t) -> render_defid env id
 
 let _render_params env = function