From e2c489431de2744b0e19106def273c31adea4186 Mon Sep 17 00:00:00 2001
From: 702fbtngus <702fbtngus@kaist.ac.kr>
Date: Wed, 25 Sep 2024 18:31:27 +0900
Subject: [PATCH] Validate CaseE with evalctx id

---
 spectec/src/al/valid.ml        | 17 ++++++++++++++++-
 spectec/src/il2al/translate.ml | 11 +++++------
 2 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/spectec/src/al/valid.ml b/spectec/src/al/valid.ml
index 445f3c9b2f..f147cc2a34 100644
--- a/spectec/src/al/valid.ml
+++ b/spectec/src/al/valid.ml
@@ -553,10 +553,25 @@ and valid_expr env (expr: expr) : unit =
     List.iter (valid_expr env) exprs;
     check_tuple source exprs expr.note;
   | CaseE (op, exprs) ->
+    let is_evalctx_id id =
+      let source = "" $ no_region in
+      let evalctx_ids = List.filter_map (fun (mixop, _, _) ->
+        let atom = mixop |> List.hd |> List.hd in
+        match atom.it with
+        | El.Atom.Atom s -> Some s
+        | _ -> None
+      ) (get_typcases source evalctxT) in
+      List.mem id evalctx_ids
+    in
+    (match 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
     check_case source exprs typ;
+)
   | CallE (id, args) ->
     List.iter (valid_arg env) args;
     check_call source id args expr.note;
@@ -632,7 +647,7 @@ let rec valid_instr (env: Env.t) (instr: instr) : Env.t =
   | EnterI (expr1, expr2, il) ->
     valid_expr env expr1;
     valid_expr env expr2;
-    check_context source expr1.note;
+    check_evalctx source expr1.note;
     check_instr source expr2.note;
     valid_instrs env il
   | AssertI expr ->
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index b2c0082e45..2a8ba3509f 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -471,26 +471,25 @@ and translate_context_instrs e' =
   | { it = Il.ListE [ctx]; _ } when is_context ctx ->
     (e'', translate_context_rhs ctx)
   | { it = Il.CatE (ve, ie); _ } ->
-    (catE (translate_exp ie, e'') ~note:ie.note, [pushI (translate_exp ve)])
+    (catE (translate_exp ie, e'') ~note:ie.note, [pushI (translate_exp ve |> subst_instr_typ)])
   | { it = Il.ListE [ve; ie]; _ } ->
-    (listE [translate_exp ie; e'] ~note:ie.note, [pushI (translate_exp ve)])
+    (listE [translate_exp ie; e'] ~note:ie.note, [pushI (translate_exp ve |> subst_instr_typ)])
   | instrs ->
     (catE (translate_exp instrs, e'') ~note:instrs.note, [])
 
 and translate_context_rhs exp =
   let at = exp.at in
-  let note = exp.note in
 
   let case = case_of_case exp in
   let atom = case |> List.hd |> List.hd in
   let args = args_of_case exp in
   let case', _ = Lib.List.split_last case in
   let args, instrs = Lib.List.split_last args in
-
   let args' = List.map translate_exp args in
-  let e' = caseE ([[atom]], []) ~at:instrs.at ~note:instrs.note in
+
+  let e' = caseE ([[atom]], []) ~at:instrs.at ~note:instrT in
   let instrs', al = translate_context_instrs e' instrs in
-  let ectx = caseE (case', args') ~at:at ~note:note in
+  let ectx = caseE (case', args') ~at:at ~note:evalctxT in
   [
     enterI (ectx, instrs', al) ~at:at;
   ]