Remove invalid pattern match

Update stringifier for vconst

spectec/src/al/print.ml

@@ -46,7 +46,8 @@ let rec string_of_record r =
   depth := !depth - 1;
   str
 
-and string_of_value = function
+and string_of_value =
+  function
   | LabelV (v1, v2) ->
     sprintf "Label_%s %s" (string_of_value v1) (string_of_value v2)
   (*| FrameV (None, v2) -> sprintf "(Frame %s)" (string_of_value v2)
@@ -57,7 +58,7 @@ and string_of_value = function
   | BoolV b -> string_of_bool b
   | TextV s -> s
   | TupV vl -> "(" ^ string_of_values ", " vl ^ ")"
-  | CaseV ("CONST", hd::tl) -> "(" ^ string_of_value hd ^ ".CONST " ^ string_of_values " " tl ^ ")"
+  | CaseV (("CONST" | "VCONST"), hd::tl) -> "(" ^ string_of_value hd ^ ".CONST " ^ string_of_values " " tl ^ ")"
   | CaseV (s, []) -> s
   | CaseV (s, vl) -> "(" ^ s ^ " " ^ string_of_values " " vl ^ ")"
   | StrV r -> string_of_record r
@@ -156,7 +157,7 @@ and string_of_expr expr =
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
   | InfixE (e1, infix, e2) -> "(" ^ string_of_expr e1 ^ " " ^ infix ^ " " ^ string_of_expr e2 ^ ")"
-  | CaseE (("CONST", _), hd::tl) -> "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
+  | CaseE ((("CONST"|"VCONST"), _), hd::tl) -> "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
   | CaseE ((s, _), []) -> s
   | CaseE ((s, _), el) -> "(" ^ s ^ " " ^ string_of_exprs " " el ^ ")"
   | OptE (Some e) -> "?(" ^ string_of_expr e ^ ")"

spectec/src/backend-interpreter/ds.ml

@@ -297,6 +297,11 @@ module WasmContext = struct
     let _, vs, _ = get_context () in
     vs
 
+  let pop_value_stack () =
+    let v, vs, ws = pop_context () in
+    push_context (v, [], ws);
+    vs
+
   let push_value v =
     let v_ctx, vs, vs_instr = pop_context () in
     if is_value v then

spectec/src/backend-interpreter/ds.mli

@@ -74,6 +74,7 @@ module WasmContext : sig
   val get_current_label : unit -> value
 
   val get_value_stack : unit -> value list
+  val pop_value_stack : unit -> value list
   val push_value : value -> unit
   val pop_value : unit -> value
 

spectec/src/backend-interpreter/interpreter.ml

@@ -471,39 +471,29 @@ and step_instr (ctx: AlContext.t) (env: value Env.t) (instr: instr) : AlContext.
     | v -> WasmContext.push_value v
     );
     ctx
-  | PopI ({ it = FrameE _; _ }) ->
-    WasmContext.pop_context () |> ignore;
-    ctx
-  | PopI ({ it = IterE ({ it = VarE name; _ }, [name'], ListN (e', None)); _ }) when name = name' ->
-    let i = eval_expr env e' |> al_to_int in
-    let v =
-      List.init i (fun _ -> WasmContext.pop_value ())
-      |> List.rev
-      |> listV_of_list
-    in
-    AlContext.update_env name v ctx
   | PopI e ->
-    (match e.it, WasmContext.pop_value () with
-    | CaseE (("CONST", _), [{ it = VarE nt; _ }; { it = VarE name; _ }]), CaseV ("CONST", [ ty; v ]) ->
+    (match e.it with
+    | FrameE _ ->
+      (match WasmContext.pop_context () with
+      | FrameV _, _, _ -> ()
+      | _ -> failwith "Invalid context");
       ctx
-      |> AlContext.update_env nt ty
-      |> AlContext.update_env name v
-    | CaseE (("CONST", _), [tyE; { it = VarE name; _ }]), CaseV ("CONST", [ ty; v ]) ->
-      assert (eval_expr env tyE = ty);
+    | IterE ({ it = VarE name; _ }, [name'], ListN (e', None)) when name = name' ->
+      let i = eval_expr env e' |> al_to_int in
+      let v =
+        List.init i (fun _ -> WasmContext.pop_value ())
+        |> List.rev
+        |> listV_of_list
+      in
       AlContext.update_env name v ctx
-    | VarE name, v -> AlContext.update_env name v ctx
-    | CaseE (("VCONST", _), [tyE; { it = VarE name; _ }]), CaseV ("VCONST", [ ty; v ]) ->
-      assert (eval_expr env tyE = ty);
-      AlContext.update_env name v ctx
-    | (_, h) ->
-      fail_on_instr
-        (sprintf "Invalid pop for value %s: " (structured_string_of_value h))
-        instr
-    )
-  | PopAllI ({ it = IterE ({ it = VarE name; _ }, [name'], List); _ }) when name = name' ->
-    let v = WasmContext.get_value_stack () |> List.rev |> listV_of_list in
-    AlContext.update_env name v ctx
-  | PopAllI _ -> fail_on_instr "Invalid pop" instr
+    | _ ->
+      let new_env = assign e (WasmContext.pop_value ()) env in
+      AlContext.set_env new_env ctx
+      )
+  | PopAllI e ->
+    let v = WasmContext.pop_value_stack () |> List.rev |> listV_of_list in
+    let new_env = assign e v env in
+    AlContext.set_env new_env ctx
   | LetI (e1, e2) ->
     let new_env = ctx |> AlContext.get_env |> assign e1 (eval_expr env e2) in
     AlContext.set_env new_env ctx

spectec/src/il2al/translate.ml

@@ -288,7 +288,31 @@ let insert_assert exp =
     -> assertI (topValueE (Some (translate_exp ty)) ~at:at) ~at:at
   | _ -> assertI (topValueE None) ~at:at
 
-let insert_pop e = [ insert_assert e; popI (translate_exp e) ~at:e.at ]
+let insert_pop e =
+  let consts = [ "CONST"; "VCONST" ] in
+
+  let e' =
+    let open Il in
+    match e.it with
+    | CaseE (Atom name, tup) when List.mem name consts ->
+      let tup' =
+        match tup.it with
+        | TupE (ty :: exps) ->
+          let ty' =
+            match ty.it with
+            | CallE _ ->
+              let var, typ = if name = "CONST" then "nt_0", "numtype" else "vt_0", "vectype" in
+              VarE (var $ no_region) $$ no_region % (VarT (typ $ no_region, []) $ no_region)
+            | _ -> ty
+          in
+          { tup with it = TupE (ty' :: exps) }
+        | _ -> tup
+      in
+      { e with it = CaseE (Atom name, tup') }
+    | _ -> e
+  in
+
+  [ insert_assert e; popI (translate_exp e') ~at:e'.at ]
 
 let insert_nop instrs = match instrs with [] -> [ nopI () ] | _ -> instrs