Remove CaseE in AL

spectec/src/al/al_util.ml

@@ -52,7 +52,6 @@ let catE ?(at = no) ~note (e1, e2) = CatE (e1, e2) |> mk_expr at note
 let memE ?(at = no) ~note (e1, e2) = MemE (e1, e2) |> mk_expr at note
 let lenE ?(at = no) ~note e = LenE e |> mk_expr at note
 let tupE ?(at = no) ~note el = TupE el |> mk_expr at note
-let caseE ?(at = no) ~note (a, el) = CaseE (a, el) |> mk_expr at note
 let caseE2 ?(at = no) ~note (op, el) = CaseE2 (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

spectec/src/al/ast.ml

@@ -92,7 +92,6 @@ and expr' =
   | MemE of expr * expr                           (* expr `<-` expr *)
   | LenE of expr                                  (* `|` expr `|` *)
   | TupE of expr list                             (* `(` (expr `,`)* `)` *)
-  | CaseE of atom * expr list                     (* atom `(` expr* `)` -- MixE/CaseE *)
   | CaseE2 of mixop * expr list                   (* mixop `(` expr* `)` -- CaseE *) (* TODO: Migrate CaseE to CaseE2*)
   | CallE of id * arg list                        (* id `(` expr* `)` *)
   | InvCallE of id * int option list * arg list   (* id`_`int*`^-1(` expr* `)` *)

spectec/src/al/eq.ml

@@ -23,7 +23,6 @@ let rec eq_expr e1 e2 =
   | MemE (e11, e12), MemE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | LenE e1, LenE e2 -> eq_expr e1 e2
   | TupE el1, TupE el2 -> eq_exprs el1 el2
-  | CaseE (a1, el1), CaseE (a2, el2) -> El.Atom.eq a1 a2 && eq_exprs el1 el2
   | CaseE2 (op1, el1), CaseE2 (op2, el2) -> Il.Mixop.eq op1 op2 && eq_exprs el1 el2
   | CallE (i1, al1), CallE (i2, al2) -> i1 = i2 && eq_args al1 al2
   | InvCallE (i1, nl1, al1), InvCallE (i2, nl2, al2) ->

spectec/src/al/free.ml

@@ -36,7 +36,6 @@ let rec free_expr expr =
   | InvCallE (_, _, al) ->  free_list free_arg al
   | TupE el
   | ListE el
-  | CaseE (_, el) -> free_list free_expr el
   | CaseE2 (_, el) -> free_list free_expr el
   | StrE r -> free_list (fun (_, e) -> free_expr !e) r
   | AccE (e, p) -> free_expr e @ free_path p

spectec/src/al/print.ml

@@ -175,10 +175,6 @@ and string_of_expr expr =
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
-  | CaseE ({ it=Atom.Atom ("CONST" | "VCONST"); _ }, hd::tl) ->
-    "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
-  | CaseE (a, []) -> string_of_atom a
-  | CaseE (a, el) -> "(" ^ string_of_atom a ^ " " ^ string_of_exprs " " el ^ ")"
   | CaseE2 ([{ it=Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
   | CaseE2 ([[ atom ]], []) -> string_of_atom atom
@@ -507,9 +503,6 @@ and structured_string_of_expr expr =
     ^ ", "
     ^ string_of_iter iter
     ^ ")"
-  | CaseE (a, el) ->
-    "CaseE (" ^ string_of_atom a
-    ^ ", [" ^ structured_string_of_exprs el ^ "])"
   | CaseE2 (op, el) ->
     "CaseE2 (" ^ string_of_mixop op
     ^ ", [" ^ structured_string_of_exprs el ^ "])"

spectec/src/al/valid.ml

@@ -376,7 +376,7 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
   | LenE expr' ->
     check_list source expr'.note; check_num source expr.note
   | TupE exprs -> check_tuple source exprs expr.note
-  | CaseE _ | CaseE2 _ -> () (* TODO *)
+  | CaseE2 _ -> () (* TODO *)
   | 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) ->

spectec/src/al/walk.ml

@@ -48,7 +48,7 @@ let walk_expr (walker: unit_walker) (expr: expr) : unit =
     Option.iter (walker.walk_expr walker) e_opt; walker.walk_expr walker e
   | CallE (_, al) | InvCallE (_, _, al) ->
     List.iter (walker.walk_arg walker) al
-  | TupE el | ListE el | CaseE (_, el) | CaseE2 (_, el) ->
+  | TupE el | ListE el | CaseE2 (_, el) ->
     List.iter (walker.walk_expr walker) el
   | StrE r -> List.iter (fun (_, e) -> walker.walk_expr walker !e) r
   | AccE (e, p) -> walker.walk_expr walker e; walk_path walker p
@@ -144,7 +144,6 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | ExtE (e1, ps, e2, dir) ->
       ExtE (walk_expr e1, List.map walk_path ps, walk_expr e2, dir)
     | UpdE (e1, ps, e2) -> UpdE (walk_expr e1, List.map walk_path ps, walk_expr e2)
-    | CaseE (a, el) -> CaseE (a, List.map walk_expr el)
     | CaseE2 (a, el) -> CaseE2 (a, List.map walk_expr el)
     | OptE e -> OptE (Option.map walk_expr e)
     | TupE el -> TupE (List.map walk_expr el)
@@ -263,7 +262,6 @@ let rec walk_expr f e =
       | AccE (e, p) -> AccE (new_ e, walk_path f p)
       | ExtE (e1, ps, e2, dir) -> ExtE (new_ e1, List.map (walk_path f) ps, new_ e2, dir)
       | UpdE (e1, ps, e2) -> UpdE (new_ e1, List.map (walk_path f) ps, new_ e2)
-      | CaseE (a, el) -> CaseE (a, List.map new_ el)
       | CaseE2 (a, el) -> CaseE2 (a, List.map new_ el)
       | OptE e -> OptE (Option.map new_ e)
       | TupE el -> TupE (List.map new_ el)

spectec/src/backend-interpreter/interpreter.ml

@@ -276,7 +276,6 @@ and eval_expr env expr =
       | path :: rest -> access_path env base path |> replace rest |> replace_path env base path
       | [] -> eval_expr env e2 in
     eval_expr env e1 |> replace ps
-  | CaseE (tag, el) -> caseV (Print.string_of_atom tag, List.map (eval_expr env) el)
   | CaseE2 (op, el) ->
     (match (get_atom op) with
     | Some a -> caseV (Print.string_of_atom a, List.map (eval_expr env) el)
@@ -461,9 +460,6 @@ and assign lhs rhs env =
   | ListE lhs_s, ListV rhs_s
     when List.length lhs_s = Array.length !rhs_s ->
     List.fold_right2 assign lhs_s (Array.to_list !rhs_s) env
-  | CaseE (lhs_tag, lhs_s), CaseV (rhs_tag, rhs_s)
-    when (Print.string_of_atom lhs_tag) = rhs_tag && List.length lhs_s = List.length rhs_s ->
-    List.fold_right2 assign lhs_s rhs_s env
   | CaseE2 (op, lhs_s), CaseV (rhs_tag, rhs_s) when List.length lhs_s = List.length rhs_s ->
     (match get_atom op with
     | Some lhs_tag when (Print.string_of_atom lhs_tag) = rhs_tag ->

spectec/src/backend-prose/print.ml

@@ -150,10 +150,6 @@ and string_of_expr expr =
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
-  | CaseE ({ it=El.Atom.Atom ("CONST" | "VCONST"); _ }, hd::tl) ->
-    "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
-  | CaseE (a, []) -> string_of_atom a
-  | CaseE (a, el) -> "(" ^ string_of_atom a ^ " " ^ string_of_exprs " " el ^ ")"
   | CaseE2 ([{ it=El.Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
   | CaseE2 ([[ atom ]], []) -> string_of_atom atom

spectec/src/backend-prose/render.ml

@@ -230,12 +230,6 @@ and al_to_el_expr expr =
         | _ -> ele
       in
       Some (El.Ast.IterE (ele, eliter))
-    | Al.Ast.CaseE (a, el) ->
-      let ela = (El.Ast.AtomE a) $ no_region in
-      let* elel = al_to_el_exprs el in
-      let ele = El.Ast.SeqE ([ ela ] @ elel) in
-      if List.length elel = 0 then Some ele
-      else Some (El.Ast.ParenE (ele $ no_region, `Insig))
     | Al.Ast.CaseE2 (op, el) ->
       let elal = mixop_to_el_exprs op in
       let* elel = al_to_el_exprs el in

spectec/src/il2al/translate.ml

@@ -752,21 +752,7 @@ and handle_special_lhs lhs rhs free_ids =
       [ letI (VarE s $$ lhs.at % lhs.note, rhs) ~at:at ],
       []
     )]
-  (* Normal cases TODO *)
-  | CaseE (tag, es) ->
-    let bindings, es' = extract_non_names es in
-    let rec inject_isCaseOf expr =
-      match expr.it with
-      | IterE (inner_expr, ids, iter) ->
-        IterE (inject_isCaseOf inner_expr, ids, iter) $$ expr.at % boolT
-      | _ -> IsCaseOfE (expr, tag) $$ rhs.at % boolT
-    in
-    [ ifI (
-      inject_isCaseOf rhs,
-      letI (caseE (tag, es') ~at:lhs.at ~note:lhs.note, rhs) ~at:at
-        :: translate_bindings free_ids bindings,
-      []
-    )]
+  (* Normal cases *)
   | CaseE2 (op, es) ->
     let tag = get_atom op |> Option.get in
     let bindings, es' = extract_non_names es in