diff --git a/lib/concrete_domains.ml b/lib/concrete_domains.ml
index 7c5ed56..5a254dc 100644
--- a/lib/concrete_domains.ml
+++ b/lib/concrete_domains.ml
@@ -19,7 +19,7 @@ module M : Domains.S = struct
       | Int of int
       | String of string
       | Addr of addr
-      | View_spec of view_spec list
+      | View_specs of view_spec list
       | Clos of clos
       | Set_clos of set_clos
       | Comp_clos of comp_clos
@@ -50,6 +50,76 @@ module M : Domains.S = struct
 
     type entry = { part_view : part_view; children : tree Snoc_list.t }
     [@@deriving sexp_of]
+
+    (* constructors *)
+    let unit () = Unit
+    let bool b = Bool b
+    let int i = Int i
+    let string s = String s
+    let addr a = Addr a
+    let view_specs vss = View_specs vss
+    let clos c = Clos c
+    let set_clos sc = Set_clos sc
+    let comp_clos cc = Comp_clos cc
+    let comp_spec cs = Comp_spec cs
+
+    (* coercions *)
+    let to_unit = function Unit -> Some () | _ -> None
+    let to_bool = function Bool b -> Some b | _ -> None
+    let to_int = function Int i -> Some i | _ -> None
+    let to_string = function String s -> Some s | _ -> None
+    let to_addr = function Addr l -> Some l | _ -> None
+
+    let to_view_spec = function
+      | Unit -> Some Vs_null
+      | Int i -> Some (Vs_int i)
+      | Comp_spec t -> Some (Vs_comp t)
+      | _ -> None
+
+    let to_view_specs = function View_specs vss -> Some vss | _ -> None
+    let to_clos = function Clos c -> Some c | _ -> None
+    let to_comp_clos = function Comp_clos c -> Some c | _ -> None
+    let to_set_clos = function Set_clos c -> Some c | _ -> None
+
+    (* comparison *)
+    (* TODO: may not be comparable, so should be bool option *)
+    let equal v1 v2 =
+      match (v1, v2) with
+      | Unit, Unit -> true
+      | Bool b1, Bool b2 -> Bool.(b1 = b2)
+      | Int i1, Int i2 -> i1 = i2
+      | Addr l1, Addr l2 -> Addr.(l1 = l2)
+      | _, _ -> false
+
+    let ( = ) = equal
+    let ( <> ) v1 v2 = not (v1 = v2)
+
+    (* primitive operations *)
+    let uop op v =
+      match (op, v) with
+      | Expr.Not, Bool b -> Some (Bool (not b))
+      | Uplus, Int i -> Some (Int i)
+      | Uminus, Int i -> Some (Int ~-i)
+      | _, _ -> None
+
+    let bop op v1 v2 =
+      match (op, v1, v2) with
+      | Expr.Eq, Unit, Unit -> Some (Bool true)
+      | Eq, Bool b1, Bool b2 -> Some (Bool Bool.(b1 = b2))
+      | Eq, Int i1, Int i2 -> Some (Bool Int.(i1 = i2))
+      | Lt, Int i1, Int i2 -> Some (Bool Int.(i1 < i2))
+      | Gt, Int i1, Int i2 -> Some (Bool Int.(i1 > i2))
+      | Le, Int i1, Int i2 -> Some (Bool Int.(i1 <= i2))
+      | Ge, Int i1, Int i2 -> Some (Bool Int.(i1 >= i2))
+      | Ne, Unit, Unit -> Some (Bool false)
+      | Ne, Bool b1, Bool b2 -> Some (Bool Bool.(b1 <> b2))
+      | Ne, Int i1, Int i2 -> Some (Bool Int.(i1 <> i2))
+      | And, Bool b1, Bool b2 -> Some (Bool (b1 && b2))
+      | Or, Bool b1, Bool b2 -> Some (Bool (b1 || b2))
+      | Plus, Int i1, Int i2 -> Some (Int (i1 + i2))
+      | Minus, Int i1, Int i2 -> Some (Int (i1 - i2))
+      | Times, Int i1, Int i2 -> Some (Int (i1 * i2))
+      | _, _, _ -> None
   end
 
   and Path : (Domains.Path with type t = T.path) = Int
@@ -70,7 +140,10 @@ module M : Domains.S = struct
     type t = value Id.Map.t [@@deriving sexp_of]
 
     let empty = Id.Map.empty
-    let lookup obj ~field = Map.find obj field |> Option.value ~default:T.Unit
+
+    let lookup obj ~field =
+      Map.find obj field |> Option.value ~default:(T.unit ())
+
     let update obj ~field ~value = Map.set obj ~key:field ~data:value
   end
 
@@ -173,38 +246,6 @@ module M : Domains.S = struct
 
   include T
 
-  module Value = struct
-    type nonrec view_spec = view_spec
-    type nonrec clos = clos
-    type nonrec addr = addr
-    type t = value
-
-    let to_bool = function Bool b -> Some b | _ -> None
-    let to_int = function Int i -> Some i | _ -> None
-    let to_string = function String s -> Some s | _ -> None
-    let to_addr = function Addr l -> Some l | _ -> None
-
-    let to_vs = function
-      | Unit -> Some Vs_null
-      | Int i -> Some (Vs_int i)
-      | Comp_spec t -> Some (Vs_comp t)
-      | _ -> None
-
-    let to_vss = function View_spec vss -> Some vss | _ -> None
-    let to_clos = function Clos c -> Some c | _ -> None
-
-    let equal v1 v2 =
-      match (v1, v2) with
-      | Unit, Unit -> true
-      | Bool b1, Bool b2 -> Bool.(b1 = b2)
-      | Int i1, Int i2 -> i1 = i2
-      | Addr l1, Addr l2 -> Addr.(l1 = l2)
-      | _, _ -> false
-
-    let ( = ) = equal
-    let ( <> ) v1 v2 = not (v1 = v2)
-  end
-
   module Phase = struct
     type t = phase = P_init | P_update | P_retry | P_effect [@@deriving equal]
 
diff --git a/lib/domains.ml b/lib/domains.ml
index f48d9c1..bfd70d9 100644
--- a/lib/domains.ml
+++ b/lib/domains.ml
@@ -11,22 +11,9 @@ module type T = sig
   type clos = { param : Id.t; body : Expr.hook_free_t; env : env }
   type set_clos = { label : Label.t; path : path }
   type comp_clos = { comp : Prog.comp; env : env }
-
-  type value =
-    | Unit
-    | Bool of bool
-    | Int of int
-    | String of string
-    | Addr of addr
-    | View_spec of view_spec list
-    | Clos of clos
-    | Set_clos of set_clos
-    | Comp_clos of comp_clos
-    | Comp_spec of comp_spec
-
-  and comp_spec = { comp : Prog.comp; env : env; arg : value }
-  and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec
-
+  type value
+  type comp_spec = { comp : Prog.comp; env : env; arg : value }
+  type view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec
   type phase = P_init | P_update | P_retry | P_effect
   type decision = Idle | Retry | Update
 
@@ -42,6 +29,41 @@ module type T = sig
   type tree = Leaf_null | Leaf_int of int | Path of path
   type entry = { part_view : part_view; children : tree Snoc_list.t }
 
+  (* constructors *)
+  val unit : unit -> value
+  val bool : bool -> value
+  val int : int -> value
+  val string : string -> value
+  val addr : addr -> value
+  val view_specs : view_spec list -> value
+  val clos : clos -> value
+  val set_clos : set_clos -> value
+  val comp_clos : comp_clos -> value
+  val comp_spec : comp_spec -> value
+
+  (* coercions *)
+  val to_unit : value -> unit option
+  val to_bool : value -> bool option
+  val to_int : value -> int option
+  val to_string : value -> string option
+  val to_addr : value -> addr option
+  val to_view_spec : value -> view_spec option
+  val to_view_specs : value -> view_spec list option
+  val to_clos : value -> clos option
+  val to_comp_clos : value -> comp_clos option
+  val to_set_clos : value -> set_clos option
+
+  (* comparison *)
+  (* TODO: may not be comparable, so should be bool option *)
+  val equal : value -> value -> bool
+  val ( = ) : value -> value -> bool
+  val ( <> ) : value -> value -> bool
+
+  (* primitive operations *)
+  val uop : Expr.uop -> value -> value option
+  val bop : Expr.bop -> value -> value -> value option
+
+  (* sexp_of *)
   val sexp_of_clos : clos -> Sexp.t
   val sexp_of_set_clos : set_clos -> Sexp.t
   val sexp_of_comp_clos : comp_clos -> Sexp.t
@@ -146,24 +168,6 @@ module type Tree_mem = sig
   val sexp_of_t : t -> Sexp.t
 end
 
-module type Value = sig
-  type view_spec
-  type clos
-  type addr
-  type t
-
-  val to_bool : t -> bool option
-  val to_int : t -> int option
-  val to_string : t -> string option
-  val to_addr : t -> addr option
-  val to_vs : t -> view_spec option
-  val to_vss : t -> view_spec list option
-  val to_clos : t -> clos option
-  val equal : t -> t -> bool
-  val ( = ) : t -> t -> bool
-  val ( <> ) : t -> t -> bool
-end
-
 module type Phase = sig
   type t
 
@@ -206,13 +210,6 @@ module type S = sig
        and type clos = clos
        and type entry = entry
 
-  module Value :
-    Value
-      with type view_spec = view_spec
-       and type clos = clos
-       and type t = value
-       and type addr = addr
-
   module Phase : Phase with type t = phase
   module Decision : Decision with type t = decision
 end
diff --git a/lib/interp.ml b/lib/interp.ml
index cb6dc8c..3cde072 100644
--- a/lib/interp.ml
+++ b/lib/interp.ml
@@ -190,13 +190,13 @@ let treemem_h =
 let value_exn exn v =
   Option.value_exn v ~error:(Error.of_exn exn ~backtrace:`Get)
 
-let int_of_value_exn v = v |> Value.to_int |> value_exn Type_error
-let bool_of_value_exn v = v |> Value.to_bool |> value_exn Type_error
-let string_of_value_exn v = v |> Value.to_string |> value_exn Type_error
-let addr_of_value_exn v = v |> Value.to_addr |> value_exn Type_error
-let vs_of_value_exn v = v |> Value.to_vs |> value_exn Type_error
-let vss_of_value_exn v = v |> Value.to_vss |> value_exn Type_error
-let clos_of_value_exn v = v |> Value.to_clos |> value_exn Type_error
+let int_of_value_exn v = v |> to_int |> value_exn Type_error
+let bool_of_value_exn v = v |> to_bool |> value_exn Type_error
+let string_of_value_exn v = v |> to_string |> value_exn Type_error
+let addr_of_value_exn v = v |> to_addr |> value_exn Type_error
+let vs_of_value_exn v = v |> to_view_spec |> value_exn Type_error
+let vss_of_value_exn v = v |> to_view_specs |> value_exn Type_error
+let clos_of_value_exn v = v |> to_clos |> value_exn Type_error
 
 module Env = struct
   include Env
@@ -292,44 +292,30 @@ let rec eval : type a. a Expr.t -> value =
  fun expr ->
   Logger.eval expr;
   match expr with
-  | Const Unit -> Unit
-  | Const (Bool b) -> Bool b
-  | Const (Int i) -> Int i
-  | Const (String s) -> String s
+  | Const Unit -> unit ()
+  | Const (Bool b) -> bool b
+  | Const (Int i) -> int i
+  | Const (String s) -> string s
   | Var id ->
       let env = perform Rd_env in
       Env.lookup_exn env ~id
-  | View es -> View_spec (List.map es ~f:(fun e -> eval e |> vs_of_value_exn))
+  | View es -> view_specs (List.map es ~f:(fun e -> eval e |> vs_of_value_exn))
   | Cond { pred; con; alt } ->
       let p = eval pred |> bool_of_value_exn in
       if p then eval con else eval alt
-  | Fn { param; body } -> Clos { param; body; env = perform Rd_env }
+  | Fn { param; body } -> clos { param; body; env = perform Rd_env }
   | App { fn; arg } -> (
-      match eval fn with
-      | Clos { param; body; env } ->
-          let env = Env.extend env ~id:param ~value:(eval arg) in
-          perform (In_env env) eval body
-      | Comp_clos { comp; env } -> Comp_spec { comp; env; arg = eval arg }
-      | Set_clos { label; path } ->
-          (* Argument to the setter should be a setting thunk *)
-          let clos = eval arg |> clos_of_value_exn in
-
-          let self_pt = perform Rd_pt in
-          let phase = perform Rd_ph in
-
-          let dec =
-            if Path.(path = self_pt) && Phase.(phase <> P_effect) then Retry
-            else Update
-          in
-          perform (Set_dec (path, dec));
-
-          (*if Int.(path = self_pt) && Phase.(phase <> P_effect) then*)
-          (*  perform (Set_dec (path, Retry));*)
-          let v, q = perform (Lookup_st (path, label)) in
-          perform (Update_st (path, label, (v, Job_q.enqueue q clos)));
-
-          Unit
-      | _ -> raise Type_error)
+      let fn = eval fn in
+      let arg = eval arg in
+      match to_clos fn with
+      | Some c -> eval_app_clos c arg
+      | None -> (
+          match to_comp_clos fn with
+          | Some c -> eval_app_comp_clos c arg
+          | None -> (
+              match to_set_clos fn with
+              | Some c -> eval_app_set_clos c arg
+              | None -> raise Type_error)))
   | Let { id; bound; body } ->
       let value = eval bound in
       let env = Env.extend (perform Rd_env) ~id ~value in
@@ -337,32 +323,8 @@ let rec eval : type a. a Expr.t -> value =
   | Stt { label; stt; set; init; body } -> (
       let path = perform Rd_pt in
       match perform Rd_ph with
-      | P_init ->
-          let v = eval init in
-          let env =
-            perform Rd_env
-            |> Env.extend ~id:stt ~value:v
-            |> Env.extend ~id:set ~value:(Set_clos { label; path })
-          in
-          perform (Update_st (path, label, (v, Job_q.empty)));
-          perform (In_env env) eval body
-      | P_update | P_retry ->
-          let v_old, q = perform (Lookup_st (path, label)) in
-          (* Run the setting thunks in the set queue *)
-          let v =
-            Job_q.fold q ~init:v_old ~f:(fun value { param; body; env } ->
-                let env = Env.extend env ~id:param ~value in
-                perform (In_env env) eval body)
-          in
-
-          let env =
-            perform Rd_env
-            |> Env.extend ~id:stt ~value:v
-            |> Env.extend ~id:set ~value:(Set_clos { label; path })
-          in
-          if Value.(v_old <> v) then perform (Set_dec (path, Update));
-          perform (Update_st (path, label, (v, Job_q.empty)));
-          perform (In_env env) eval body
+      | P_init -> eval_stt_init ~label ~stt ~set ~init ~body ~path
+      | P_update | P_retry -> eval_stt_update_retry ~label ~stt ~set ~body ~path
       | P_effect -> raise Invalid_phase)
   | Eff e ->
       let path = perform Rd_pt
@@ -370,40 +332,20 @@ let rec eval : type a. a Expr.t -> value =
       and env = perform Rd_env in
       (match phase with P_effect -> raise Invalid_phase | _ -> ());
       perform (Enq_eff (path, { param = Id.unit; body = e; env }));
-      Unit
+      unit ()
   | Seq (e1, e2) ->
       eval e1 |> ignore;
       eval e2
   | Uop { op; arg } -> (
       let v = eval arg in
-      match (op, v) with
-      | Not, Bool b -> Bool (not b)
-      | Uplus, Int i -> Int i
-      | Uminus, Int i -> Int ~-i
-      | _, _ -> raise Type_error)
+      match uop op v with Some v -> v | None -> raise Type_error)
   | Bop { op; left; right } -> (
       let v1 = eval left in
       let v2 = eval right in
-      match (op, v1, v2) with
-      | Eq, Unit, Unit -> Bool true
-      | Eq, Bool b1, Bool b2 -> Bool Bool.(b1 = b2)
-      | Eq, Int i1, Int i2 -> Bool (i1 = i2)
-      | Lt, Int i1, Int i2 -> Bool (i1 < i2)
-      | Gt, Int i1, Int i2 -> Bool (i1 > i2)
-      | Le, Int i1, Int i2 -> Bool (i1 <= i2)
-      | Ge, Int i1, Int i2 -> Bool (i1 >= i2)
-      | Ne, Unit, Unit -> Bool false
-      | Ne, Bool b1, Bool b2 -> Bool Bool.(b1 <> b2)
-      | Ne, Int i1, Int i2 -> Bool (i1 <> i2)
-      | And, Bool b1, Bool b2 -> Bool (b1 && b2)
-      | Or, Bool b1, Bool b2 -> Bool (b1 || b2)
-      | Plus, Int i1, Int i2 -> Int (i1 + i2)
-      | Minus, Int i1, Int i2 -> Int (i1 - i2)
-      | Times, Int i1, Int i2 -> Int (i1 * i2)
-      | _, _, _ -> raise Type_error)
+      match bop op v1 v2 with Some v -> v | None -> raise Type_error)
   | Alloc ->
-      let addr = perform (Alloc_addr Obj.empty) in
-      Addr addr
+      let a = perform (Alloc_addr Obj.empty) in
+      addr a
   | Get { obj; idx } ->
       let addr = eval obj |> addr_of_value_exn in
       let i = eval idx |> string_of_value_exn in
@@ -416,7 +358,60 @@ let rec eval : type a. a Expr.t -> value =
       let value = eval value in
       let new_obj = Obj.update old_obj ~field:i ~value in
       perform (Update_addr (addr, new_obj));
-      Unit
+      unit ()
+
+and eval_app_clos { param; body; env } arg =
+  let env = Env.extend env ~id:param ~value:arg in
+  perform (In_env env) eval body
+
+and eval_app_comp_clos { comp; env } arg = comp_spec { comp; env; arg }
+
+and eval_app_set_clos { label; path } arg =
+  (* Argument to the setter should be a setting thunk *)
+  let clos = clos_of_value_exn arg in
+
+  let self_pt = perform Rd_pt in
+  let phase = perform Rd_ph in
+
+  let dec =
+    if Path.(path = self_pt) && Phase.(phase <> P_effect) then Retry else Update
+  in
+  perform (Set_dec (path, dec));
+
+  (*if Int.(path = self_pt) && Phase.(phase <> P_effect) then*)
+  (*  perform (Set_dec (path, Retry));*)
+  let v, q = perform (Lookup_st (path, label)) in
+  perform (Update_st (path, label, (v, Job_q.enqueue q clos)));
+
+  unit ()
+
+and eval_stt_init ~label ~stt ~set ~init ~body ~path =
+  let v = eval init in
+  let env =
+    perform Rd_env
+    |> Env.extend ~id:stt ~value:v
+    |> Env.extend ~id:set ~value:(set_clos { label; path })
+  in
+  perform (Update_st (path, label, (v, Job_q.empty)));
+  perform (In_env env) eval body
+
+and eval_stt_update_retry ~label ~stt ~set ~body ~path =
+  let v_old, q = perform (Lookup_st (path, label)) in
+  (* Run the setting thunks in the set queue *)
+  let v =
+    Job_q.fold q ~init:v_old ~f:(fun value { param; body; env } ->
+        let env = Env.extend env ~id:param ~value in
+        perform (In_env env) eval body)
+  in
+
+  let env =
+    perform Rd_env
+    |> Env.extend ~id:stt ~value:v
+    |> Env.extend ~id:set ~value:(set_clos { label; path })
+  in
+  if v_old <> v then perform (Set_dec (path, Update));
+  perform (Update_st (path, label, (v, Job_q.empty)));
+  perform (In_env env) eval body
 
 let rec eval_mult : type a. ?re_render:int -> a Expr.t -> value =
  fun ?(re_render = 1) expr ->
@@ -533,14 +528,14 @@ and reconcile1 (old_tree : tree option) (vs : view_spec) : bool * tree =
   Logger.reconcile1 old_tree vs;
   match (old_tree, vs) with
   | Some (Leaf_null as t), Vs_null -> (false, t)
-  | Some (Leaf_int i as t), Vs_int j when i = j -> (false, t)
+  | Some (Leaf_int i as t), Vs_int j when Int.(i = j) -> (false, t)
   | Some (Path pt as t), (Vs_comp { comp = { name; _ }; arg; _ } as vs) -> (
       let { part_view; _ } = perform (Lookup_ent pt) in
       match part_view with
       | Root -> assert false
       | Node { comp_spec = { comp = { name = name'; _ }; arg = arg'; _ }; _ } ->
           if Id.(name = name') then
-            (update1 t (if Value.(arg = arg') then None else Some arg), t)
+            (update1 t (if arg = arg' then None else Some arg), t)
           else (true, render1 vs))
   | _, vs -> (true, render1 vs)
 
@@ -578,7 +573,7 @@ let rec eval_top (prog : Prog.t) : view_spec list =
   | Expr e -> eval e |> vss_of_value_exn
   | Comp (comp, p) ->
       let env = perform Rd_env in
-      let env = Env.extend env ~id:comp.name ~value:(Comp_clos { comp; env }) in
+      let env = Env.extend env ~id:comp.name ~value:(comp_clos { comp; env }) in
       perform (In_env env) eval_top p
 
 let step_prog (prog : Prog.t) : Path.t =