diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index efbfc97cb0..2b34924655 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -7,6 +7,7 @@ type mixop = Il.Ast.mixop
 
 (* Types *)
 
+(* TODO: define AL type *)
 type typ = Il.Ast.typ
 
 (* Identifiers *)
diff --git a/spectec/src/al/dune b/spectec/src/al/dune
index 24cd65854b..ae8d1b614f 100644
--- a/spectec/src/al/dune
+++ b/spectec/src/al/dune
@@ -1,5 +1,5 @@
 (library
   (name al)
   (libraries util zarith il)
-  (modules ast al_util print walk free eq valid)
+  (modules ast al_util print walk free eq valid eval lang)
 )
diff --git a/spectec/src/al/eval.ml b/spectec/src/al/eval.ml
new file mode 100644
index 0000000000..af24ef3bce
--- /dev/null
+++ b/spectec/src/al/eval.ml
@@ -0,0 +1,381 @@
+open Ast
+open Print
+open Walk
+open Util
+open Source
+
+module Subst = struct
+  include Map.Make(String)
+
+  let subst_exp s e =
+    let subst_exp' walker e =
+      match e.it with
+      | VarE id when mem id s -> find id s
+      | _ -> base_walker.walk_expr walker e
+    in
+    let walker = {base_walker with walk_expr = subst_exp'} in
+    walker.walk_expr walker e
+end
+
+let rec get_subst lhs rhs s =
+  match lhs.it, rhs.it with
+  | VarE id, _ -> Subst.add id rhs s
+  | UnE (op1, e1), UnE (op2, e2) when op1 = op2 -> get_subst e1 e2 s
+  | OptE (Some e1), OptE (Some e2) | FrameE (None, e1), FrameE (None, e2) ->
+    get_subst e1 e2 s
+  | BinE (op1, e11, e12), BinE (op2, e21, e22) when op1 = op2 ->
+    s |> get_subst e11 e21 |> get_subst e12 e22
+  | CompE (e11, e12), CompE (e21, e22) | CatE (e11, e12), CatE (e21, e22)
+  | LabelE (e11, e12), LabelE (e21, e22) | FrameE (Some e11, e12), FrameE (Some e21, e22) ->
+    s |> get_subst e11 e21 |> get_subst e12 e22
+  | TupE el1, TupE el2 | ListE el1, ListE el2 ->
+    List.fold_right2 get_subst el1 el2 s
+  | CaseE (name1, el1), CaseE (name2, el2) when name1 = name2 ->
+    List.fold_right2 get_subst el1 el2 s
+  | StrE r1, StrE r2 ->
+    List.fold_left (fun acc (k, e) -> get_subst !e (Record.find k r2) acc) s r1
+  | IterE _, _ -> (* TODO *) s
+  | _, _ when Eq.eq_expr lhs rhs -> s
+  | _ -> assert (false)
+
+let get_subst_arg param arg s =
+  match param.it, arg.it with
+  | ExpA e1, ExpA e2 -> get_subst e1 e2 s
+  | _ -> s
+
+let ($>) it e = {e with it}
+
+let as_opt_exp e =
+  match e.it with
+  | OptE eo -> eo
+  | _ -> failwith "as_opt_exp"
+
+let as_list_exp e =
+    match e.it with
+    | ListE es -> es
+    | _ -> failwith "as_list_exp"
+    
+let is_head_normal_exp e =
+  match e.it with
+  | BoolE _ | NumE _ | UnE (MinusOp, {it = NumE _; _}) | SubE _
+  | OptE _ | ListE _ | TupE _ | CaseE _ | StrE _-> true
+  | _ -> false
+    
+let rec is_normal_exp e =
+  match e.it with
+  | BoolE _ | NumE _ | UnE (MinusOp, {it = NumE _; _}) | SubE _ -> true
+  | ListE es | TupE es | CaseE (_, es) -> List.for_all is_normal_exp es
+  | OptE None -> true
+  | OptE (Some e) -> is_normal_exp e
+  | StrE efs -> List.for_all (fun (_, e) -> is_normal_exp !e) efs
+  | _ -> false
+
+let rec reduce_exp s e : expr =
+  Debug_log.(log "al.reduce_exp"
+    (fun _ -> fmt "%s" (string_of_expr e))
+    (fun e' -> fmt "%s" (string_of_expr e'))
+  ) @@ fun _ ->
+  match e.it with
+  | VarE _ | BoolE _ | NumE _ -> e
+  | UnE (op, e1) ->
+    let e1' = reduce_exp s e1 in
+    (match op, e1'.it with
+    | NotOp, BoolE b -> BoolE (not b) $> e
+    | NotOp, UnE (NotOp, e11) -> e11
+    | MinusOp, UnE (MinusOp, e11) -> e11
+    | _ -> UnE (op, e1') $> e
+    )
+  | BinE (op, e1, e2) ->
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    (match op, e1'.it, e2'.it with
+    | AndOp, BoolE true, _ -> e2'
+    | AndOp, BoolE false, _ -> e1'
+    | AndOp, _, BoolE true -> e1'
+    | AndOp, _, BoolE false -> e2'
+    | OrOp, BoolE true, _ -> e1'
+    | OrOp, BoolE false, _ -> e2'
+    | OrOp, _, BoolE true -> e2'
+    | OrOp, _, BoolE false -> e1'
+    | ImplOp, BoolE b1, BoolE b2 -> BoolE (not b1 || b2) $> e
+    | ImplOp, BoolE true, _ -> e2'
+    | ImplOp, BoolE false, _ -> BoolE true $> e
+    | ImplOp, _, BoolE true -> e2'
+    | ImplOp, _, BoolE false -> UnE (NotOp, e1') $> e
+    | EquivOp, BoolE b1, BoolE b2 -> BoolE (b1 = b2) $> e
+    | EquivOp, BoolE true, _ -> e2'
+    | EquivOp, BoolE false, _ -> UnE (NotOp, e2') $> e
+    | EquivOp, _, BoolE true -> e1'
+    | EquivOp, _, BoolE false -> UnE (NotOp, e1') $> e
+    | AddOp, NumE n1, NumE n2 -> NumE Z.(n1 + n2) $> e
+    | AddOp, NumE z0, _ when z0 = Z.zero -> e2'
+    | AddOp, _, NumE z0 when z0 = Z.zero -> e1'
+    | SubOp, NumE n1, NumE n2 when n1 >= n2 -> NumE Z.(n1 - n2) $> e
+    | SubOp, NumE z0, _ when z0 = Z.zero -> UnE (MinusOp, e2') $> e
+    | SubOp, _, NumE z0 when z0 = Z.zero -> e1'
+    | MulOp, NumE n1, NumE n2 -> NumE Z.(n1 * n2) $> e
+    | MulOp, NumE z1, _ when z1 = Z.one -> e2'
+    | MulOp, _, NumE z1 when z1 = Z.one -> e1'
+    | DivOp, NumE n1, NumE n2 when Z.(n2 <> zero && rem n1 n2 = zero) -> NumE Z.(n1 / n2) $> e
+    | DivOp, NumE z0, _ when z0 = Z.zero -> e1'
+    | DivOp, _, NumE z1 when z1 = Z.one -> e1'
+    | ModOp, NumE n1, NumE n2 -> NumE Z.(rem n1 n2) $> e
+    | ModOp, NumE z0, _ when z0 = Z.zero -> e1'
+    | ModOp, _, NumE z1 when z1 = Z.one -> NumE Z.zero $> e
+    | ExpOp, NumE n1, NumE n2 when n2 >= Z.zero -> NumE Z.(n1 ** to_int n2) $> e
+    | ExpOp, NumE z01, _ when z01 = Z.zero || z01 = Z.one -> e1'
+    | ExpOp, _, NumE z0 when z0 = Z.zero -> NumE Z.one $> e
+    | ExpOp, _, NumE z1 when z1 = Z.one -> e1'
+    | EqOp, _, _ when Eq.eq_expr e1' e2' -> BoolE true $> e
+    | EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false $> e
+    | NeOp, _, _ when Eq.eq_expr e1' e2' -> BoolE false $> e
+    | NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true $> e
+    | LtOp, NumE n1, NumE n2 -> BoolE (n1 < n2) $> e
+    | LtOp, UnE (MinusOp, {it = NumE n1; _}), UnE (MinusOp, {it = NumE n2; _}) -> BoolE (n2 < n1) $> e
+    | LtOp, UnE (MinusOp, {it = NumE _; _}), NumE _ -> BoolE true $> e
+    | LtOp, NumE _, UnE (MinusOp, {it = NumE _; _}) -> BoolE false $> e
+    | GtOp, NumE n1, NumE n2 -> BoolE (n1 > n2) $> e
+    | GtOp, UnE (MinusOp, {it = NumE n1; _}), UnE (MinusOp, {it = NumE n2; _}) -> BoolE (n2 > n1) $> e
+    | GtOp, UnE (MinusOp, {it = NumE _; _}), NumE _ -> BoolE false $> e
+    | GtOp, NumE _, UnE (MinusOp, {it = NumE _; _}) -> BoolE true $> e
+    | LeOp, NumE n1, NumE n2 -> BoolE (n1 <= n2) $> e
+    | LeOp, UnE (MinusOp, {it = NumE n1; _}), UnE (MinusOp, {it = NumE n2; _}) -> BoolE (n2 <= n1) $> e
+    | LeOp, UnE (MinusOp, {it = NumE _; _}), NumE _ -> BoolE true $> e
+    | LeOp, NumE _, UnE (MinusOp, {it = NumE _; _}) -> BoolE false $> e
+    | GeOp, NumE n1, NumE n2 -> BoolE (n1 >= n2) $> e
+    | GeOp, UnE (MinusOp, {it = NumE n1; _}), UnE (MinusOp, {it = NumE n2; _}) -> BoolE (n2 >= n1) $> e
+    | GeOp, UnE (MinusOp, {it = NumE _; _}), NumE _ -> BoolE false $> e
+    | GeOp, NumE _, UnE (MinusOp, {it = NumE _; _}) -> BoolE true $> e
+    | _ -> BinE (op, e1', e2') $> e
+    )
+  | AccE (e1, p) ->
+    (match p.it with
+    | IdxP e2 ->
+      let e1' = reduce_exp s e1 in
+      let e2' = reduce_exp s e2 in
+      (match e1'.it, e2'.it with
+      | ListE es, NumE i when i < Z.of_int (List.length es) -> List.nth es (Z.to_int i)
+      | _ -> AccE (e1', IdxP e2' $ p.at) $> e
+      )
+    | SliceP (e2, e3) ->
+      let e1' = reduce_exp s e1 in
+      let e2' = reduce_exp s e2 in
+      let e3' = reduce_exp s e3 in
+      (match e1'.it, e2'.it, e3'.it with
+      | ListE es, NumE i, NumE n when Z.(i + n) < Z.of_int (List.length es) ->
+        ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es))
+      | _ -> AccE (e1', SliceP (e2', e3') $ p.at)
+      ) $> e
+    | DotP atom ->
+      let e1' = reduce_exp s e1 in
+      (match e1'.it with
+      | StrE efs -> !(snd (List.find (fun (atomN, _) -> El.Atom.eq atomN atom) efs))
+      | _ -> AccE (e1', DotP atom $ p.at) $> e
+      )
+    )
+  | UpdE (e1, p, e2) ->
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    reduce_path s e1' p
+      (fun e' ps -> if ps = [] then e2' else UpdE (e', ps, e2') $> e')
+  | ExtE (_e1, _p, _e2, _dir) -> e
+    (* TODO
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    reduce_path s e1' p
+      (fun e' p' ->
+        if p'.it = RootP
+        then reduce_exp s (CatE (e', e2') $> e')
+        else ExtE (e', p', e2') $> e'
+      )
+      *)
+  | StrE efs -> StrE (List.map (reduce_expfield s) efs) $> e
+  | CompE (e1, e2) ->
+    (* TODO(4, rossberg): avoid overlap with CatE? *)
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    (match e1'.it, e2'.it with
+    | ListE es1, ListE es2 -> ListE (es1 @ es2)
+    | OptE None, OptE _ -> e2'.it
+    | OptE _, OptE None -> e1'.it
+    | StrE efs1, StrE efs2 ->
+      let merge (atom1, e1) (atom2, e2) =
+        assert (El.Atom.eq atom1 atom2);
+        (atom1, ref (reduce_exp s (CompE (!e1, !e2) $> !e1)))
+      in StrE (List.map2 merge efs1 efs2)
+    | _ -> CompE (e1', e2')
+    ) $> e
+  | MemE (e1, e2) ->
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    (match e2'.it with
+    | OptE None -> BoolE false
+    | OptE (Some e2') when Eq.eq_expr e1' e2' -> BoolE true
+    | OptE (Some e2') when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
+    | ListE [] -> BoolE false
+    | ListE es2' when List.exists (Eq.eq_expr e1') es2' -> BoolE true
+    | ListE es2' when is_normal_exp e1' && List.for_all is_normal_exp es2' -> BoolE false
+    | _ -> MemE (e1', e2')
+    ) $> e
+  | LenE e1 ->
+    let e1' = reduce_exp s e1 in
+    (match e1'.it with
+    | ListE es -> NumE (Z.of_int (List.length es))
+    | _ -> LenE e1'
+    ) $> e
+  | TupE es -> TupE (List.map (reduce_exp s) es) $> e
+  | CallE (id, args) ->
+    let args' = List.map (reduce_arg s) args in
+    (match reduce_call id args' with
+    | None -> CallE (id, args') $> e
+    | Some e -> e
+    )
+  | IterE (e1, iterexp) ->
+    let e1' = reduce_exp s e1 in
+    let (iter', xes') as iterexp' = reduce_iterexp s iterexp in
+    let ids, es' = List.split xes' in
+    if not (List.for_all is_head_normal_exp es') || iter' <= List1 && es' = [] then
+      IterE (e1', iterexp') $> e
+    else
+      (match iter' with
+      | Opt ->
+        let eos' = List.map as_opt_exp es' in
+        if List.for_all Option.is_none eos' then
+          OptE None $> e
+        else if List.for_all Option.is_some eos' then
+          let es1' = List.map Option.get eos' in
+          let s = List.fold_right2 Subst.add ids es1' Subst.empty in
+          reduce_exp s (Subst.subst_exp s e1')
+        else
+          IterE (e1', iterexp') $> e
+      | List | List1 ->
+        let n = List.length (as_list_exp (List.hd es')) in
+        if iter' = List || n >= 1 then
+          let en = NumE (Z.of_int n) $$ e.at % (Il.Ast.NumT NatT $ e.at) in
+          reduce_exp s (IterE (e1', (ListN (en, None), xes')) $> e)
+        else
+          IterE (e1', iterexp') $> e
+      | ListN ({it = NumE n'; _}, ido) ->
+        let ess' = List.map as_list_exp es' in
+        let ns = List.map List.length ess' in
+        let n = Z.to_int n' in
+        if List.for_all ((=) n) ns then
+          (TupE (List.init n (fun i ->
+            let esI' = List.map (fun es -> List.nth es i) ess' in
+            let s = List.fold_right2 Subst.add ids esI' Subst.empty in
+            let s' =
+              Option.fold ido ~none:s ~some:(fun id ->
+                let en = NumE (Z.of_int i) $$ no_region % (Il.Ast.NumT NatT $ no_region) in
+                Subst.add id en s
+              )
+            in Subst.subst_exp s' e1'
+          )) $> e) |> reduce_exp s
+        else
+          IterE (e1', iterexp') $> e
+      | ListN _ ->
+        IterE (e1', iterexp') $> e
+      )
+  | OptE eo -> OptE (Option.map (reduce_exp s) eo) $> e
+  | ListE es -> ListE (List.map (reduce_exp s) es) $> e
+  | CatE (e1, e2) ->
+    let e1' = reduce_exp s e1 in
+    let e2' = reduce_exp s e2 in
+    (match e1'.it, e2'.it with
+    | ListE es1, ListE es2 -> ListE (es1 @ es2)
+    | OptE None, OptE _ -> e2'.it
+    | OptE _, OptE None -> e1'.it
+    | _ -> CatE (e1', e2')
+    ) $> e
+  | CaseE (op, es) -> CaseE (op, List.map (reduce_exp s) es) $> e
+  | SubE _ -> e
+  | _ -> e
+
+and reduce_iter s = function
+  | ListN (e, ido) -> ListN (reduce_exp s e, ido)
+  | iter -> iter
+
+and reduce_iterexp s (iter, xes) =
+  (reduce_iter s iter, List.map (fun (id, e) -> id, reduce_exp s e) xes)
+
+and reduce_expfield s (atom, e) : (atom * expr ref) = (atom, ref (reduce_exp s !e))
+
+and reduce_path s e p f =
+  match Lib.List.split_last_opt p with
+  | None -> f e []
+  | Some (ps, p') -> match p'.it with
+    | IdxP e1 ->
+      let e1' = reduce_exp s e1 in
+      let f' e' p1' =
+        match e'.it, e1'.it with
+        | ListE es, NumE i when i < Z.of_int (List.length es) ->
+          ListE (List.mapi (fun j eJ -> if Z.of_int j = i then f eJ p1' else eJ) es) $> e'
+        | _ ->
+          f e' (ps @ [IdxP (e1') $> p'])
+      in
+      reduce_path s e ps f'
+    | SliceP (e1, e2) ->
+      let e1' = reduce_exp s e1 in
+      let e2' = reduce_exp s e2 in
+      let f' e' p1' =
+        match e'.it, e1'.it, e2'.it with
+        | ListE es, NumE i, NumE n when Z.(i + n) < Z.of_int (List.length es) ->
+          let e1' = ListE Lib.List.(take (Z.to_int i) es) $> e' in
+          let e2' = ListE Lib.List.(take (Z.to_int n) (drop (Z.to_int i) es)) $> e' in
+          let e3' = ListE Lib.List.(drop Z.(to_int (i + n)) es) $> e' in
+          reduce_exp s (CatE (e1', CatE (f e2' p1', e3') $> e') $> e')
+        | _ ->
+          f e' (ps @ [SliceP (e1', e2') $> p'])
+      in
+      reduce_path s e ps f'
+    | DotP atom ->
+      let f' e' p1' =
+        match e'.it with
+        | StrE efs ->
+          StrE (List.map (fun (atomI, eI) ->
+            if El.Atom.eq atomI atom then (atomI, ref (f !eI p1')) else (atomI, eI)) efs) $> e'
+        | _ ->
+          f e' (ps @ [DotP (atom) $> p'])
+      in
+      reduce_path s e ps f'
+
+and reduce_arg s a : arg =
+  Debug_log.(log "al.reduce_arg"
+    (fun _ -> fmt "%s" (string_of_arg a))
+    (fun a' -> fmt "%s" (string_of_arg a'))
+  ) @@ fun _ ->
+  match a.it with
+  | ExpA e -> ExpA (reduce_exp s e) $ a.at
+  | TypA _t -> a  (* types are reduced on demand *)
+  | DefA _id -> a
+  (* | GramA _g -> a *)
+
+and reduce_call id args : expr option =
+  let func_finder = fun al -> match al.it with | FuncA (fname, _, _) -> fname = id | RuleA _ -> false in
+  match (List.find func_finder !Lang.al).it with
+  | FuncA (_, params, il) ->
+    let s = List.fold_right2 get_subst_arg params args Subst.empty in
+    reduce_instrs s il
+  | _ -> assert (false)
+
+and reduce_instrs s : instr list -> expr option = function
+  | [] -> None
+  | instr :: t ->
+    match instr.it with
+    | ReturnI expr_opt -> Option.map (reduce_exp s) expr_opt
+    | LetI (expr1, expr2) ->
+      let new_s = get_subst expr1 expr2 s in
+      reduce_instrs new_s t
+    | IfI (expr, il1, il2) ->
+      (* TODO: consider iter *)
+      (match (reduce_exp s expr).it with
+      | BoolE true -> reduce_instrs s (il1@t)
+      | BoolE false -> reduce_instrs s (il2@t)
+      | _ -> None
+      )
+    (* Can have side effect *)
+    | EitherI _ | PerformI _ | ReplaceI _ | AppendI _ | FieldWiseAppendI _ -> None
+    (* Invalid instruction in FuncA *)
+    | EnterI _  | PushI _ | PopI _ | PopAllI _ | TrapI | ThrowI _
+    | ExecuteI _ | ExecuteSeqI _ | ExitI _ | OtherwiseI _ | YetI _ -> assert (false)
+    (* Nop *)
+    | (AssertI _ | NopI) -> reduce_instrs s t
diff --git a/spectec/src/al/lang.ml b/spectec/src/al/lang.ml
new file mode 100644
index 0000000000..37c4133d52
--- /dev/null
+++ b/spectec/src/al/lang.ml
@@ -0,0 +1,3 @@
+open Ast
+
+let al: script ref = ref []
diff --git a/spectec/src/al/valid.ml b/spectec/src/al/valid.ml
index d85bf4a92a..7be5fde498 100644
--- a/spectec/src/al/valid.ml
+++ b/spectec/src/al/valid.ml
@@ -5,10 +5,11 @@ open Ast
 open Al_util
 open Print
 open Walk
+open Free
 
 
 module Atom = El.Atom
-module Eval = Il.Eval
+module IlEval = Il.Eval
 
 (* Error *)
 
@@ -37,20 +38,30 @@ let error_case source typ =
 
 let (let*) = Option.bind
 
-
-(* Bound Set *)
-
-module Set = Free.IdSet
-
-let bound_set: Set.t ref = ref Set.empty
-let add_bound_var id = bound_set := Set.add id !bound_set
-let add_bound_vars expr = bound_set := Set.union (Free.free_expr expr) !bound_set
-let add_bound_param arg = match arg.it with ExpA e -> add_bound_vars e | TypA _ | DefA _ -> ()
+module Env = struct
+  include Map.Make(String)
+
+  type t = expr option Map.Make(String).t
+
+  (* TODO: pass env *)
+  let env: t ref = ref empty
+  let add_bound_var id = env := add id None !env
+  let add_bound_vars expr = IdSet.iter add_bound_var (free_expr expr)
+  let add_bound_param arg =
+    match arg.it with ExpA e -> add_bound_vars e | TypA _ | DefA _ -> ()
+  let add_subst lhs rhs =
+    let open Eval in
+    env :=
+      get_subst lhs rhs Subst.empty
+      |> Subst.map Option.some
+      |> merge (fun _ _ _ -> (* TODO *) assert (false)) !env
+  let add id expr = env := add id (Some expr) !env
+end
 
 (* Type Env *)
 
-module Env = Il.Env
-let env: Env.t ref = ref Env.empty
+module IlEnv = Il.Env
+let il_env: IlEnv.t ref = ref IlEnv.empty
 
 
 let varT s = VarT (s $ no_region, []) $ no_region
@@ -61,10 +72,10 @@ let is_trivial_mixop = List.for_all (fun atoms -> List.length atoms = 0)
 (* Subtyping *)
 
 let get_deftyps (id: Il.Ast.id) (args: Il.Ast.arg list): deftyp list =
-  match Env.find_opt_typ !env id with
+  match IlEnv.find_opt_typ !il_env id with
   | Some (_, insts) ->
     let typ_of_arg arg =
-      match (Eval.reduce_arg !env arg).it with
+      match (IlEval.reduce_arg !il_env arg).it with
       | ExpA { it=SubE (_, typ, _); _ } -> typ
       | ExpA { note; _ } -> note
       | TypA typ -> typ
@@ -94,7 +105,7 @@ let get_deftyps (id: Il.Ast.id) (args: Il.Ast.arg list): deftyp list =
     let get_deftyp inst =
       let InstD (_, inst_args, deftyp) = inst.it in
       let valid_arg arg inst_arg = 
-        Eval.sub_typ !env (typ_of_arg arg) (typ_of_arg inst_arg)
+        IlEval.sub_typ !il_env (typ_of_arg arg) (typ_of_arg inst_arg)
       in
       if List.for_all2 valid_arg args inst_args then
         Some deftyp
@@ -158,8 +169,8 @@ and unify_typs_opt : typ list -> typ option = function
 
 and ground_typ_of (typ: typ) : typ =
   match typ.it with
-  | VarT (id, _) when Env.mem_var !env id ->
-    let typ' = Env.find_var !env id in
+  | VarT (id, _) when IlEnv.mem_var !il_env id ->
+    let typ' = IlEnv.find_var !il_env id in
     if Il.Eq.eq_typ typ typ' then typ else ground_typ_of typ'
   (* NOTE: Consider `fN` as a `NumT` to prevent diverging ground type *)
   | VarT (id, _) when id.it = "fN" -> NumT RealT $ typ.at
@@ -182,7 +193,7 @@ let rec sub_typ typ1 typ2 =
   match typ1'.it, typ2'.it with
   | IterT (typ1'', _), IterT (typ2'', _) -> sub_typ typ1'' typ2''
   | NumT _, NumT _ -> true
-  | _, _ -> Eval.sub_typ !env typ1' typ2'
+  | _, _ -> IlEval.sub_typ !il_env typ1' typ2'
 
 let rec matches typ1 typ2 =
   match (ground_typ_of typ1).it, (ground_typ_of typ2).it with
@@ -216,8 +227,8 @@ let rec get_typfields_of_inst (inst: inst) : typfield list =
 
 and get_typfields (typ: typ) : typfield list =
   match typ.it with
-  | VarT (id, _) when Env.mem_typ !env id ->
-    let _, insts = Env.find_typ !env id in
+  | VarT (id, _) when IlEnv.mem_typ !il_env id ->
+    let _, insts = IlEnv.find_typ !il_env id in
     List.concat_map get_typfields_of_inst insts
   | _ -> []
 
@@ -287,21 +298,21 @@ let check_tuple source exprs typ =
   | _ -> error_tuple source typ
 
 let check_call source id args result_typ =
-  match Env.find_opt_def !env (id $ no_region) with
+  match IlEnv.find_opt_def !il_env (id $ no_region) with
   | Some (params, typ, _) ->
-    (* TODO: Use local environment *)
-    (* Store global enviroment *)
-    let global_env = !env in
+    (* TODO: Use local il_environment *)
+    (* Store global il_enviroment *)
+    let global_il_env = !il_env in
 
     let check_arg arg param =
       match arg.it, param.it with
       | ExpA expr, ExpP (_, typ') -> check_match source expr.note typ'
       (* Add local variable typ *)
-      | TypA typ1, TypP id -> env := Env.bind_var !env id typ1
+      | TypA typ1, TypP id -> il_env := IlEnv.bind_var !il_env id typ1
       | DefA aid, DefP (_, pparams, ptyp) ->
-        (match Env.find_opt_def !env (aid $ no_region) with
+        (match IlEnv.find_opt_def !il_env (aid $ no_region) with
         | Some (aparams, atyp, _) -> 
-          if not (Eval.sub_typ !env atyp ptyp) then
+          if not (IlEval.sub_typ !il_env atyp ptyp) then
             error_valid
               "argument's return type is not a subtype of parameter's return type"
               source
@@ -321,7 +332,7 @@ let check_call source id args result_typ =
             let aptyp = typ_of_param aparam in
             let pptyp = typ_of_param pparam in
 
-            if not (Eval.sub_typ !env pptyp aptyp) then
+            if not (IlEval.sub_typ !il_env pptyp aptyp) then
               error_valid
                 "parameter's parameter type is not a subtype of argument's return type"
                 source
@@ -342,8 +353,8 @@ let check_call source id args result_typ =
     List.iter2 check_arg args params;
     check_match source result_typ typ;
 
-    (* Reset global enviroment *)
-    env := global_env
+    (* Reset global il_enviroment *)
+    il_env := global_il_env
   | None -> error_valid "no function definition" source ""
 
 let check_inv_call source id indices args result_typ =
@@ -443,7 +454,7 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
   let source = string_of_expr expr $ expr.at in
   (match expr.it with
   | VarE id ->
-    if not (Set.mem id !bound_set) then error expr.at ("free identifier " ^ id)
+    if not (Env.mem id !Env.env) then error expr.at ("free identifier " ^ id)
   | NumE _ -> check_num source expr.note;
   | UnE (NotOp, expr') ->
     check_bool source expr.note; check_bool source expr'.note
@@ -488,18 +499,20 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
     check_case source exprs typ
   | 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, _xes)) -> (* TODO *)
+  | IterE (expr1, (iter, xes)) -> (* TODO *)
+    let global_env = !Env.env in
     if not (expr1.note.it = BoolT && expr.note.it = BoolT) then
+      List.iter (fun (id, e) -> Env.add id e) xes;
       (match iter with
       | Opt ->
         check_match source expr.note (iterT expr1.note Opt);
-      | ListN (expr2, id_opt) ->
-        Option.iter add_bound_var id_opt;
+      | ListN (expr2, _) ->
         check_match source expr.note (iterT expr1.note List);
         check_num source expr2.note
       | _ ->
         check_match source expr.note (iterT expr1.note List);
-      )
+      );
+    Env.env := global_env
   | OptE expr_opt ->
     check_opt source expr.note;
     Option.iter
@@ -540,7 +553,7 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
     check_bool source expr.note; check_num source expr1.note
   | SubE _ | YetE _ -> error_valid "invalid expression" source ""
   );
-  (Option.get walker.super).walk_expr walker expr
+  base_unit_walker.walk_expr walker expr
 
 
 (* Instr validation *)
@@ -557,15 +570,15 @@ let valid_instr (walker: unit_walker) (instr: instr) : unit =
       not (sub_typ (get_base_typ expr.note) (varT "callframe"))
     then
       error_mismatch source (get_base_typ expr.note) (varT "val")
-  | PopI expr | PopAllI expr -> add_bound_vars expr;
+  | PopI expr | PopAllI expr -> Env.add_bound_vars expr;
     if
       not (sub_typ (get_base_typ expr.note) (varT "val")) &&
       not (sub_typ (get_base_typ expr.note) (varT "callframe"))
     then
       error_mismatch source (get_base_typ expr.note) (varT "val")
   | LetI (expr1, expr2) ->
-    add_bound_vars expr1; check_match source expr1.note expr2.note
-    | ExecuteI expr | ExecuteSeqI expr -> check_instr source expr.note
+    Env.add_subst expr1 expr2; check_match source expr1.note expr2.note
+  | ExecuteI expr | ExecuteSeqI expr -> check_instr source expr.note
   | PerformI (id, args) -> check_call source id args (TupT [] $ no_region)
   | ReplaceI (expr1, path, expr2) ->
     access source expr1.note path |> check_match source expr2.note
@@ -574,35 +587,34 @@ let valid_instr (walker: unit_walker) (instr: instr) : unit =
   | OtherwiseI _ | YetI _ -> error_valid "invalid instruction" source ""
   | _ -> ()
   );
-  (Option.get walker.super).walk_instr walker instr
+  base_unit_walker.walk_instr walker instr
 
 let init algo =
   let params = Al_util.params_of_algo algo in
 
-  bound_set := Set.singleton "s";
-  List.iter add_bound_param params
+  Env.add_bound_var "s";
+  List.iter Env.add_bound_param params
 
 
 let valid_algo (algo: algorithm) =
 
-  print_string (Al_util.name_of_algo algo ^ "(");
-
   algo
   |> Al_util.params_of_algo
   |> List.map string_of_arg
   |> String.concat ", "
-  |> print_string;
-  print_endline ")";
+  |> Printf.sprintf "%s(%s)" (Al_util.name_of_algo algo)
+  |> print_endline;
+
 
-  (* TODO: Use local environment *)
-  (* Store global enviroment *)
-  let global_env = !env in
+  (* TODO: Use local il_environment *)
+  (* Store global il_enviroment *)
+  let global_il_env = !il_env in
 
-  (* Add function argument to environment *)
-  (match Env.find_opt_def !env (Al_util.name_of_algo algo $ no_region) with
+  (* Add function argument to il_environment *)
+  (match IlEnv.find_opt_def !il_env (Al_util.name_of_algo algo $ no_region) with
   | Some (params, _, _) -> List.iter (fun param ->
       (match param.it with
-      | DefP (id, params', typ') -> env := Env.bind_def !env id (params', typ', [])
+      | DefP (id, params', typ') -> il_env := IlEnv.bind_def !il_env id (params', typ', [])
       | _ -> ()
       )
     ) params;
@@ -612,15 +624,15 @@ let valid_algo (algo: algorithm) =
   init algo;
   let walker =
     { base_unit_walker with
-      super = Some base_unit_walker;
       walk_expr = valid_expr;
       walk_instr = valid_instr
     }
   in
   walker.walk_algo walker algo;
 
-  (* Reset global enviroment *)
-  env := global_env
+  (* Reset global il_enviroment *)
+  il_env := global_il_env
 
 let valid (script: script) =
+  Lang.al := script;
   List.iter valid_algo script
diff --git a/spectec/src/al/walk.ml b/spectec/src/al/walk.ml
index a06cdb000d..e4acfaed95 100644
--- a/spectec/src/al/walk.ml
+++ b/spectec/src/al/walk.ml
@@ -6,7 +6,6 @@ open Source
 (* Unit walker *)
 
 type unit_walker = {
-  super: unit_walker option;
   walk_algo: unit_walker -> algorithm -> unit;
   walk_instr: unit_walker -> instr -> unit;
   walk_expr: unit_walker -> expr -> unit;
@@ -89,13 +88,12 @@ let walk_algo (walker: unit_walker) (algo: algorithm) : unit =
   | FuncA (_, args, instrs) ->
     List.iter (walker.walk_arg walker) args; List.iter (walker.walk_instr walker) instrs
 
-let base_unit_walker = { super=None; walk_algo; walk_instr; walk_expr; walk_path; walk_iter; walk_arg }
+let base_unit_walker = { walk_algo; walk_instr; walk_expr; walk_path; walk_iter; walk_arg }
 
 
 (* Transform walker *)
 
 type walker = {
-  super: walker option;
   walk_algo: walker -> algorithm -> algorithm;
   walk_instr: walker -> instr -> instr;
   walk_expr: walker -> expr -> expr;
@@ -215,7 +213,7 @@ let walk_algo (walker: walker) (algo: algorithm) : algorithm =
   in
   { algo with it }
 
-let base_walker = { super=None; walk_algo; walk_instr; walk_expr; walk_path; walk_iter; walk_arg }
+let base_walker = { walk_algo; walk_instr; walk_expr; walk_path; walk_iter; walk_arg }
 
 
 (* TODO: remove walker below *)
diff --git a/spectec/src/al/walk.mli b/spectec/src/al/walk.mli
index 6872cc9794..4e0467de3b 100644
--- a/spectec/src/al/walk.mli
+++ b/spectec/src/al/walk.mli
@@ -1,7 +1,6 @@
 open Ast
 
 type unit_walker = {
-  super: unit_walker option;
   walk_algo: unit_walker -> algorithm -> unit;
   walk_instr: unit_walker -> instr -> unit;
   walk_expr: unit_walker -> expr -> unit;
@@ -10,7 +9,6 @@ type unit_walker = {
   walk_arg: unit_walker -> arg -> unit;
 }
 type walker = {
-  super: walker option;
   walk_algo: walker -> algorithm -> algorithm;
   walk_instr: walker -> instr -> instr;
   walk_expr: walker -> expr -> expr;
diff --git a/spectec/src/il2al/manual.ml b/spectec/src/il2al/manual.ml
index 6069c9ff6d..448b53abe1 100644
--- a/spectec/src/il2al/manual.ml
+++ b/spectec/src/il2al/manual.ml
@@ -19,8 +19,8 @@ let eval_expr =
 
   (* Add function definition to AL environment *)
   let param = Il.Ast.ExpP ("_" $ no_region, ty_instrs) $ no_region in
-  Al.Valid.env :=
-    Il.Env.bind_def !Al.Valid.env ("eval_expr" $ no_region) ([param], ty_vals, []);
+  Al.Valid.il_env :=
+    Il.Env.bind_def !Al.Valid.il_env ("eval_expr" $ no_region) ([param], ty_vals, []);
 
   FuncA (
     "eval_expr",
diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml
index e5de3b8c88..711860e127 100644
--- a/spectec/src/il2al/preprocess.ml
+++ b/spectec/src/il2al/preprocess.ml
@@ -112,9 +112,9 @@ let rec preprocess_prem prem =
       in
 
       (* Add function definition to AL environment *)
-      if not (Env.mem_def !Al.Valid.env id) then (
+      if not (Env.mem_def !Al.Valid.il_env id) then (
         let param = ExpP ("_" $ no_region, dt.note) $ dt.at in
-        Al.Valid.env := Env.bind_def !Al.Valid.env id ([param], ct.note, [])
+        Al.Valid.il_env := Env.bind_def !Al.Valid.il_env id ([param], ct.note, [])
       );
 
       [ new_prem $ prem.at ]
@@ -137,9 +137,9 @@ let rec preprocess_prem prem =
       in
 
       (* Add function definition to AL environment *)
-      if not (Env.mem_def !Al.Valid.env id) then (
+      if not (Env.mem_def !Al.Valid.il_env id) then (
         let param = ExpP ("_" $ no_region, lhs.note) $ lhs.at in
-        Al.Valid.env := Env.bind_def !Al.Valid.env id ([param], rhs.note, [])
+        Al.Valid.il_env := Env.bind_def !Al.Valid.il_env id ([param], rhs.note, [])
       );
 
       [ new_prem $ prem.at ]
@@ -167,15 +167,15 @@ let preprocess_def (def: def) : def =
 
   match def'.it with
   | TypD (id, ps, insts) ->
-    Al.Valid.env := Env.bind_typ !Al.Valid.env id (ps, insts); def'
+    Al.Valid.il_env := Env.bind_typ !Al.Valid.il_env id (ps, insts); def'
   | RelD (id, mixop, t, rules) ->
-    Al.Valid.env := Env.bind_rel !Al.Valid.env id (mixop, t, rules);
+    Al.Valid.il_env := Env.bind_rel !Al.Valid.il_env id (mixop, t, rules);
     RelD (id, mixop, t, List.map preprocess_rule rules) $ def.at
   | DecD (id, ps, t, clauses) ->
-    Al.Valid.env := Env.bind_def !Al.Valid.env id (ps, t, clauses);
+    Al.Valid.il_env := Env.bind_def !Al.Valid.il_env id (ps, t, clauses);
     DecD (id, ps, t, List.map preprocess_clause clauses) $ def.at
   | GramD (id, ps, t, prods) ->
-    Al.Valid.env := Env.bind_gram !Al.Valid.env id (ps, t, prods); def'
+    Al.Valid.il_env := Env.bind_gram !Al.Valid.il_env id (ps, t, prods); def'
   | RecD _ -> assert (false);
   | HintD _ -> def'
 
diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml
index c911d4cc8b..ce1d00c9a1 100644
--- a/spectec/src/il2al/transpile.ml
+++ b/spectec/src/il2al/transpile.ml
@@ -606,12 +606,12 @@ let hide_state_expr expr =
 
 let hide_state instr =
   let at = instr.at in
-  let env = Al.Valid.env in
+  let il_env = Al.Valid.il_env in
   let set_unit_type fname =
     let id = (fname $ no_region) in
     let unit_type = Il.Ast.TupT [] $ no_region in
-    match Il.Env.find_def !Al.Valid.env id with
-    | (params, _, clauses) -> env := Al.Valid.Env.bind_def !env id (params, unit_type, clauses)
+    match Il.Env.find_def !Al.Valid.il_env id with
+    | (params, _, clauses) -> il_env := Al.Valid.IlEnv.bind_def !il_env id (params, unit_type, clauses)
   in
   match instr.it with
   (* Perform *)
@@ -690,7 +690,7 @@ let remove_state algo =
 let get_state_arg_opt f =
   let arg = ref (TypA (Il.Ast.BoolT $ no_region)) in
   let id = f $ no_region in
-  match Il.Env.find_opt_def !Al.Valid.env id with
+  match Il.Env.find_opt_def !Al.Valid.il_env id with
   | Some (params, _, _) ->
     let param_state = List.find_opt (
       fun param ->