diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index f6669cb550..9fe3c61928 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -248,8 +248,8 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
 let forms: list((string, t)) = [
   // INFIX OPERATORS
   ("typ_plus", mk_infix("+", Typ, P.or_)),
-  ("type-arrow", mk_infix("->", Typ, 6)),
-  ("cell-join", mk_infix(";", Exp, 10)),
+  ("type-arrow", mk_infix("->", Typ, P.plus)),
+  ("cell-join", mk_infix(";", Exp, P.semi)),
   ("plus", mk_infix("+", Exp, P.plus)),
   ("minus", mk_infix("-", Exp, P.plus)),
   ("times", mk_infix("*", Exp, P.mult)),
diff --git a/src/haz3lcore/lang/Operators.re b/src/haz3lcore/lang/Operators.re
index aa8842b72b..5ec740e2cc 100644
--- a/src/haz3lcore/lang/Operators.re
+++ b/src/haz3lcore/lang/Operators.re
@@ -175,3 +175,12 @@ let string_op_to_string = (op: op_bin_string): string => {
   | Equals => "$=="
   };
 };
+
+let bin_op_to_string = (op: op_bin): string => {
+  switch (op) {
+  | Int(op) => int_op_to_string(op)
+  | Float(op) => float_op_to_string(op)
+  | Bool(op) => bool_op_to_string(op)
+  | String(op) => string_op_to_string(op)
+  };
+};
diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re
index e809621df7..6fc0dcfe73 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -3,6 +3,12 @@ open Util;
 
 /**
  * higher precedence means lower int representation
+ *
+ * These precedences are interspersed with examples to help you
+ * work out the precedence. For each example, if a construct
+ * requires parentheses when placed in the '_____' space, then
+ * your new construct's precedence is below the comment with
+ * the example. (i.e. higher int)
  */
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = int;
@@ -10,31 +16,50 @@ type t = int;
 let max: t = 0;
 
 let unquote = 1;
-let ap = 2;
-let neg = 3;
-let power = 4;
-let mult = 5;
-
-let not_ = 5;
-let plus = 6;
-let cons = 7;
-let concat = 8;
-let eqs = 9;
-let and_ = 10;
-let or_ = 11;
-let ann = 12;
-let if_ = 13;
-let fun_ = 14;
-let prod = 15;
-let semi = 16;
-let let_ = 17;
-let filter = 18;
+let cast = 2;
+let ap = 3;
+// _____(x)
+let neg = 4;
+// _____ ** 2
+let power = 5;
+// 2 ** _____
+// 6 / _____
+let mult = 6;
+let not_ = 6;
+// _____ / 6
+// 4 - _____
+let plus = 7;
+// _____ - 4
+// _____ :: []
+let cons = 8;
+// 1 :: _____
+// [1,2] @ _____
+let concat = 9;
+// _____ @ [1,2]
+// x == _____
+let eqs = 10;
+// _____ == x
+// _____ && true
+let and_ = 11;
+// true && _____
+// _____ || false
+let or_ = 12;
+// false || _____
+let ann = 13;
+let if_ = 14;
+let fun_ = 15;
+// fun x -> _____
+let prod = 16;
+// a , _____ , x
+// _____ ; ()
+let semi = 17;
+// () ; _____
+let let_ = 18;
 let rule_arr = 19;
 let rule_pre = 20;
 let rule_sep = 21;
 let case_ = 22;
-
-let min = 23;
+let min = 24;
 
 let compare = (p1: t, p2: t): int =>
   (-1) * Int.compare((p1 :> int), (p2 :> int));
@@ -55,3 +80,44 @@ let associativity_map: IntMap.t(Direction.t) =
 
 let associativity = (p: t): option(Direction.t) =>
   IntMap.find_opt(p, associativity_map);
+
+let of_bin_op: Operators.op_bin => t =
+  fun
+  | Int(op) =>
+    switch (op) {
+    | Plus => plus
+    | Minus => plus
+    | Times => mult
+    | Power => power
+    | Divide => mult
+    | LessThan => eqs
+    | LessThanOrEqual => eqs
+    | GreaterThan => eqs
+    | GreaterThanOrEqual => eqs
+    | Equals => eqs
+    | NotEquals => eqs
+    }
+  | Float(op) =>
+    switch (op) {
+    | Plus => plus
+    | Minus => plus
+    | Times => mult
+    | Power => power
+    | Divide => mult
+    | LessThan => eqs
+    | LessThanOrEqual => eqs
+    | GreaterThan => eqs
+    | GreaterThanOrEqual => eqs
+    | Equals => eqs
+    | NotEquals => eqs
+    }
+  | Bool(op) =>
+    switch (op) {
+    | And => and_
+    | Or => or_
+    }
+  | String(op) =>
+    switch (op) {
+    | Concat => concat
+    | Equals => eqs
+    };
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
new file mode 100644
index 0000000000..377fde8043
--- /dev/null
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -0,0 +1,311 @@
+open PrettySegment;
+open Base;
+
+let text_to_pretty = (id, sort, str): pretty => {
+  p_just([
+    Tile({
+      id,
+      label: [str],
+      mold: Mold.mk_op(sort, []),
+      shards: [0],
+      children: [],
+    }),
+  ]);
+};
+
+// /* We assume that parentheses have already been added as necessary, and
+//       that the expression has no DynamicErrorHoles, Casts, or FailedCasts
+//    */
+// let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
+//   let go = exp_to_pretty(~inline);
+//   switch (exp |> Exp.term_of) {
+//   | Invalid(x) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, x)
+//   | EmptyHole =>
+//     let id = exp |> Exp.rep_id;
+//     p_just([Grout({id, shape: Convex})]);
+//   | Bool(b) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Bool.to_string(b))
+//   | Int(n) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Int.to_string(n))
+//   // TODO: do floats print right?
+//   | Float(f) =>
+//     text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Float.to_string(f))
+//   | String(s) =>
+//     text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "\"" ++ s ++ "\"")
+//   | Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
+//   // TODO: add multi-line binop support?
+//   | BinOp(op, l, r) =>
+//     let id = exp |> Exp.rep_id;
+//     let+ l = go(l)
+//     and+ r = go(r);
+//     l
+//     @ [
+//       Tile({
+//         id,
+//         label: [Operators.bin_op_to_string(op)],
+//         mold: Mold.mk_bin(Precedence.of_bin_op(op), Sort.Exp, []),
+//         shards: [0],
+//         children: [l, r],
+//       }),
+//     ]
+//     @ r;
+//   };
+// };
+
+// Use Precedence.re to work out where your construct goes here.
+let rec external_precedence = (exp: Exp.t): Precedence.t => {
+  switch (Exp.term_of(exp)) {
+  // Forms which we are about to strip, so we just look inside
+  | Closure(_, x)
+  | DynamicErrorHole(x, _) => external_precedence(x)
+
+  // Binary operations are handled in Precedence.re
+  | BinOp(op, _, _) => Precedence.of_bin_op(op)
+
+  // Indivisible forms never need parentheses around them
+  | Var(_)
+  | Invalid(_)
+  | Bool(_)
+  | Int(_)
+  | Float(_)
+  | String(_)
+  | EmptyHole
+  | Constructor(_)
+  | Deferral(_)
+  | BuiltinFun(_) => Precedence.max
+
+  // Same goes for forms which are already surrounded
+  | Parens(_)
+  | ListLit(_)
+  | Test(_)
+  | Match(_) => Precedence.max
+
+  // Other forms
+  | UnOp(Meta(Unquote), _) => Precedence.unquote
+  | Cast(_)
+  | FailedCast(_) => Precedence.cast
+  | Ap(Forward, _, _)
+  | DeferredAp(_)
+  | TypAp(_) => Precedence.ap
+  | UnOp(Bool(Not), _) => Precedence.not_
+  | UnOp(Int(Minus), _) => Precedence.neg
+  | Cons(_) => Precedence.cons
+  | Ap(Reverse, _, _) => Precedence.eqs
+  | ListConcat(_) => Precedence.concat
+  | If(_) => Precedence.if_
+  | TypFun(_)
+  | Fun(_)
+  | FixF(_) => Precedence.fun_
+  | Tuple(_) => Precedence.prod
+  | Seq(_) => Precedence.semi
+
+  // Top-level things
+  | Filter(_)
+  | TyAlias(_)
+  | Let(_) => Precedence.let_
+
+  // I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
+  | MultiHole(_) => Precedence.min
+  };
+};
+
+let external_precedence_pat = (dp: Pat.t) =>
+  switch (DHPat.term_of(dp)) {
+  // Indivisible forms never need parentheses around them
+  | EmptyHole
+  | Wild
+  | Invalid(_)
+  | Var(_)
+  | Int(_)
+  | Float(_)
+  | Bool(_)
+  | String(_)
+  | Constructor(_) => Precedence.max
+
+  // Same goes for forms which are already surrounded
+  | ListLit(_)
+  | Parens(_) => Precedence.max
+
+  // Other forms
+  | Cons(_) => Precedence.cons
+  | Ap(_) => Precedence.ap
+  | Cast(_) => Precedence.ann
+  | Tuple(_) => Precedence.prod
+
+  // I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
+  | MultiHole(_) => Precedence.min
+  };
+
+let paren_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
+  external_precedence(exp) >= internal_precedence
+    ? Exp.fresh(Parens(exp)) : exp;
+
+let paren_assoc_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
+  external_precedence(exp) > internal_precedence
+    ? Exp.fresh(Parens(exp)) : exp;
+
+let paren_pat_at = (internal_precedence: Precedence.t, pat: Pat.t): Pat.t =>
+  external_precedence_pat(pat) >= internal_precedence
+    ? Pat.fresh(Parens(pat)) : pat;
+
+let rec parenthesize = (exp: Exp.t): Exp.t => {
+  let (term, rewrap) = Exp.unwrap(exp);
+  switch (term) {
+  // Indivisible forms dont' change
+  | Var(_)
+  | Invalid(_)
+  | Bool(_)
+  | Int(_)
+  | Float(_)
+  | String(_)
+  | EmptyHole
+  | Constructor(_)
+  | Deferral(_)
+  | BuiltinFun(_) => exp
+
+  // Forms that currently need to stripped before oututting
+  | Closure(_, x) => x
+  | DynamicErrorHole(x, _) => x
+
+  // Other forms
+  | Fun(p, e, c, n) =>
+    Fun(
+      parenthesize_pat(p) |> paren_pat_at(Precedence.min),
+      parenthesize(e) |> paren_assoc_at(Precedence.fun_),
+      c, // TODO: Parenthesize through closure
+      n,
+    )
+    |> rewrap
+  | TypFun(tp, e, n) =>
+    TypFun(tp, parenthesize(e) |> paren_assoc_at(Precedence.fun_), n)
+    |> rewrap
+  | Tuple(es) =>
+    Tuple(
+      es |> List.map(parenthesize) |> List.map(paren_at(Precedence.prod)),
+    )
+    |> rewrap
+  | ListLit(es) =>
+    ListLit(
+      es |> List.map(parenthesize) |> List.map(paren_at(Precedence.concat)),
+    )
+    |> rewrap
+  | Let(p, e1, e2) =>
+    Let(
+      parenthesize_pat(p) |> paren_pat_at(Precedence.min),
+      parenthesize(e1) |> paren_at(Precedence.min),
+      parenthesize(e2) |> paren_assoc_at(Precedence.let_),
+    )
+    |> rewrap
+  | FixF(p, e, c) =>
+    FixF(
+      parenthesize_pat(p) |> paren_pat_at(Precedence.min),
+      parenthesize(e) |> paren_assoc_at(Precedence.fun_),
+      c // TODO: Parenthesize through closure
+    )
+    |> rewrap
+  | TyAlias(tp, t, e) =>
+    TyAlias(
+      tp,
+      t, // TODO: Types
+      parenthesize(e) |> paren_assoc_at(Precedence.let_),
+    )
+    |> rewrap
+  | Ap(Forward, e1, e2) =>
+    Ap(
+      Forward,
+      parenthesize(e1) |> paren_at(Precedence.min),
+      parenthesize(e2) |> paren_at(Precedence.min),
+    )
+    |> rewrap
+  | Ap(Reverse, e1, e2) =>
+    Ap(
+      Reverse,
+      parenthesize(e1) |> paren_assoc_at(Precedence.eqs),
+      parenthesize(e2) |> paren_at(Precedence.eqs),
+    )
+    |> rewrap
+  | TypAp(e, tp) =>
+    TypAp(
+      parenthesize(e) |> paren_assoc_at(Precedence.ap),
+      tp // TODO: Types
+    )
+    |> rewrap
+  | DeferredAp(e, es) =>
+    DeferredAp(
+      parenthesize(e) |> paren_assoc_at(Precedence.ap),
+      es |> List.map(parenthesize) |> List.map(paren_at(Precedence.prod)),
+    )
+    |> rewrap
+  | If(e1, e2, e3) =>
+    If(
+      parenthesize(e1) |> paren_at(Precedence.min),
+      parenthesize(e2) |> paren_at(Precedence.min),
+      parenthesize(e3) |> paren_assoc_at(Precedence.if_),
+    )
+    |> rewrap
+  | Seq(e1, e2) =>
+    Seq(
+      parenthesize(e1) |> paren_at(Precedence.semi), // tempting to make this one assoc too
+      parenthesize(e2) |> paren_assoc_at(Precedence.semi),
+    )
+    |> rewrap
+  | Test(e) => Test(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
+  | Filter(f, e) =>
+    Filter(
+      f, // TODO: Filters
+      parenthesize(e) |> paren_at(Precedence.min),
+    )
+    |> rewrap
+  | Parens(e) =>
+    Parens(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
+  | Cons(e1, e2) =>
+    Cons(
+      parenthesize(e1) |> paren_at(Precedence.cons),
+      parenthesize(e2) |> paren_assoc_at(Precedence.cons),
+    )
+    |> rewrap
+  | ListConcat(e1, e2) =>
+    ListConcat(
+      parenthesize(e1) |> paren_at(Precedence.concat),
+      parenthesize(e2) |> paren_assoc_at(Precedence.concat),
+    )
+    |> rewrap
+  | UnOp(Meta(Unquote), e) =>
+    UnOp(Meta(Unquote), parenthesize(e) |> paren_at(Precedence.unquote))
+    |> rewrap
+  | UnOp(Bool(Not), e) =>
+    UnOp(Bool(Not), parenthesize(e) |> paren_at(Precedence.not_)) |> rewrap
+  | UnOp(Int(Minus), e) =>
+    UnOp(Int(Minus), parenthesize(e) |> paren_at(Precedence.neg)) |> rewrap
+  | BinOp(op, e1, e2) =>
+    BinOp(
+      op,
+      parenthesize(e1) |> paren_assoc_at(Precedence.of_bin_op(op)),
+      parenthesize(e2) |> paren_at(Precedence.of_bin_op(op)),
+    )
+    |> rewrap
+  | Match(e, rs) =>
+    Match(
+      parenthesize(e) |> paren_at(Precedence.min),
+      rs
+      |> List.map(((p, e)) =>
+           (
+             parenthesize_pat(p) |> paren_pat_at(Precedence.min),
+             parenthesize(e) |> paren_assoc_at(Precedence.case_),
+           )
+         ),
+    )
+    |> rewrap
+  | MultiHole(_) => exp // TODO: Parenthesize through multiholes
+  | Cast(e, t1, t2) =>
+    // TODO: Types
+    Cast(parenthesize(e) |> paren_assoc_at(Precedence.cast), t1, t2)
+    |> rewrap
+  | FailedCast(e, t1, t2) =>
+    // TODO: Types
+    FailedCast(parenthesize(e) |> paren_assoc_at(Precedence.cast), t1, t2)
+    |> rewrap
+  };
+}
+and parenthesize_pat = (pat: Pat.t): Pat.t => {
+  // TODO: patterns
+  pat;
+};
diff --git a/src/haz3lcore/pretty/PrettySegment.re b/src/haz3lcore/pretty/PrettySegment.re
new file mode 100644
index 0000000000..67b5e089a2
--- /dev/null
+++ b/src/haz3lcore/pretty/PrettySegment.re
@@ -0,0 +1,20 @@
+open Util;
+
+// invariant: always has at least one option
+type pretty = list(Segment.t);
+
+let p_concat = (pretty2, pretty1) =>
+  List.map(piece1 => List.map(piece2 => piece1 @ piece2, pretty2), pretty1)
+  |> List.flatten;
+let p_or = (pretty2, pretty1) => pretty1 @ pretty2;
+let p_orif = (cond, pretty2, pretty1) => if (cond) {pretty1} else {pretty2};
+let p_just = segment => [segment];
+
+let p_concat = (pretties: list(pretty)) =>
+  List.fold_left(p_concat, [[]], pretties);
+
+let (let+) = (pretty, f) => List.map(f, pretty);
+let (and+) = (pretty1, pretty2) => ListUtil.cross(pretty1, pretty2);
+
+let ( let* ) = (pretty, f) => List.map(f, pretty) |> List.flatten;
+let ( and* ) = (pretty1, pretty2) => ListUtil.cross(pretty1, pretty2);
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 4331965a52..2457485150 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -295,6 +295,7 @@ module Exp = {
 
   let rep_id: t => Id.t = IdTagged.rep_id;
   let fresh: term => t = IdTagged.fresh;
+  let term_of: t => term = IdTagged.term_of;
   let unwrap: t => (term, term => t) = IdTagged.unwrap;
 
   let cls_of_term: term => cls =
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 0a630288c4..fa4242f8f8 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -3,92 +3,6 @@ open EvaluatorStep;
 open Transition;
 module Doc = Pretty.Doc;
 
-let precedence_bin_bool_op = (op: Operators.op_bin_bool) =>
-  switch (op) {
-  | And => DHDoc_common.precedence_And
-  | Or => DHDoc_common.precedence_Or
-  };
-
-let precedence_bin_int_op = (bio: Operators.op_bin_int) =>
-  switch (bio) {
-  | Times => DHDoc_common.precedence_Times
-  | Power => DHDoc_common.precedence_Power
-  | Divide => DHDoc_common.precedence_Divide
-  | Plus => DHDoc_common.precedence_Plus
-  | Minus => DHDoc_common.precedence_Minus
-  | Equals => DHDoc_common.precedence_Equals
-  | NotEquals => DHDoc_common.precedence_Equals
-  | LessThan => DHDoc_common.precedence_LessThan
-  | LessThanOrEqual => DHDoc_common.precedence_LessThan
-  | GreaterThan => DHDoc_common.precedence_GreaterThan
-  | GreaterThanOrEqual => DHDoc_common.precedence_GreaterThan
-  };
-let precedence_bin_float_op = (bfo: Operators.op_bin_float) =>
-  switch (bfo) {
-  | Times => DHDoc_common.precedence_Times
-  | Power => DHDoc_common.precedence_Power
-  | Divide => DHDoc_common.precedence_Divide
-  | Plus => DHDoc_common.precedence_Plus
-  | Minus => DHDoc_common.precedence_Minus
-  | Equals => DHDoc_common.precedence_Equals
-  | NotEquals => DHDoc_common.precedence_Equals
-  | LessThan => DHDoc_common.precedence_LessThan
-  | LessThanOrEqual => DHDoc_common.precedence_LessThan
-  | GreaterThan => DHDoc_common.precedence_GreaterThan
-  | GreaterThanOrEqual => DHDoc_common.precedence_GreaterThan
-  };
-let precedence_bin_string_op = (bso: Operators.op_bin_string) =>
-  switch (bso) {
-  | Concat => DHDoc_common.precedence_Plus
-  | Equals => DHDoc_common.precedence_Equals
-  };
-let rec precedence = (~show_casts: bool, d: DHExp.t) => {
-  let precedence' = precedence(~show_casts);
-  switch (DHExp.term_of(d)) {
-  | Var(_)
-  | Invalid(_)
-  | Bool(_)
-  | Int(_)
-  | Seq(_)
-  | Test(_)
-  | Float(_)
-  | String(_)
-  | ListLit(_)
-  | EmptyHole
-  | Constructor(_)
-  | FailedCast(_)
-  | DynamicErrorHole(_)
-  | If(_)
-  | Closure(_)
-  | BuiltinFun(_)
-  | Deferral(_)
-  | Filter(_) => DHDoc_common.precedence_const
-  | Cast(d1, _, _) =>
-    show_casts ? DHDoc_common.precedence_Ap : precedence'(d1)
-  | DeferredAp(_)
-  | Ap(_)
-  | TypAp(_) => DHDoc_common.precedence_Ap
-  | Cons(_) => DHDoc_common.precedence_Cons
-  | ListConcat(_) => DHDoc_common.precedence_Plus
-  | Tuple(_) => DHDoc_common.precedence_Comma
-  | TypFun(_)
-  | Fun(_) => DHDoc_common.precedence_max
-  | Let(_)
-  | TyAlias(_)
-  | FixF(_)
-  | Match(_) => DHDoc_common.precedence_max
-  | UnOp(Meta(Unquote), _) => DHDoc_common.precedence_Ap
-  | UnOp(Bool(Not), _) => DHDoc_common.precedence_Not
-  | UnOp(Int(Minus), _) => DHDoc_common.precedence_Minus
-  | BinOp(Bool(op), _, _) => precedence_bin_bool_op(op)
-  | BinOp(Int(op), _, _) => precedence_bin_int_op(op)
-  | BinOp(Float(op), _, _) => precedence_bin_float_op(op)
-  | BinOp(String(op), _, _) => precedence_bin_string_op(op)
-  | MultiHole(_) => DHDoc_common.precedence_max
-  | Parens(d) => precedence'(d)
-  };
-};
-
 let mk_bin_bool_op = (op: Operators.op_bin_bool): DHDoc.t =>
   Doc.text(Operators.bool_op_to_string(op));
 
@@ -126,7 +40,6 @@ let mk =
   // //     hidden_steps,
   // //   );
   // let _ = print_endline("============");
-  let precedence = precedence(~show_casts=settings.show_casts);
   let rec go =
           (
             d: DHExp.t,
@@ -189,16 +102,6 @@ let mk =
         ) => {
       go(d, env, enforce_inline, recent_subst);
     };
-    let parenthesize = (b, doc) =>
-      if (b) {
-        hcats([
-          DHDoc_common.Delim.open_Parenthesized,
-          doc |> DHDoc_common.pad_child(~enforce_inline),
-          DHDoc_common.Delim.close_Parenthesized,
-        ]);
-      } else {
-        doc(~enforce_inline);
-      };
     let go_case_rule = ((dp, dclause)): DHDoc.t => {
       let hidden_clause = annot(DHAnnot.Collapsed, text(Unicode.ellipsis));
       let clause_doc =
@@ -243,17 +146,11 @@ let mk =
         );
       };
     let go_formattable = (~enforce_inline) => go'(~enforce_inline);
-    let mk_left_associative_operands = (precedence_op, d1, d2) => (
-      go_formattable(d1) |> parenthesize(precedence(d1) > precedence_op),
-      go_formattable(d2) |> parenthesize(precedence(d2) >= precedence_op),
-    );
-    let mk_right_associative_operands = (precedence_op, d1, d2) => (
-      go_formattable(d1) |> parenthesize(precedence(d1) >= precedence_op),
-      go_formattable(d2) |> parenthesize(precedence(d2) > precedence_op),
-    );
+    let mk_left_associative_operands = (d1, d2) => (go'(d1), go'(d2));
+    let mk_right_associative_operands = (d1, d2) => (go'(d1), go'(d2));
     let doc = {
       switch (DHExp.term_of(d)) {
-      | Parens(d') => go'(d')
+      | Parens(d') => hseps([text("("), go'(d'), text(")")])
       | Closure(env', d') => go'(d', ~env=env')
       | Filter(flt, d') =>
         if (settings.show_stepper_filters) {
@@ -332,74 +229,41 @@ let mk =
         let ol = d_list |> List.map(d => go'(d));
         DHDoc_common.mk_ListLit(ol);
       | Ap(Forward, d1, d2) =>
-        let (doc1, doc2) = (
-          go_formattable(d1)
-          |> parenthesize(precedence(d1) > DHDoc_common.precedence_Ap),
-          go'(d2),
-        );
+        let (doc1, doc2) = (go'(d1), go'(d2));
         DHDoc_common.mk_Ap(doc1, doc2);
       | DeferredAp(d1, d2) =>
-        let (doc1, doc2) = (
-          go_formattable(d1)
-          |> parenthesize(precedence(d1) > DHDoc_common.precedence_Ap),
-          go'(Tuple(d2) |> DHExp.fresh),
-        );
+        let (doc1, doc2) = (go'(d1), go'(Tuple(d2) |> DHExp.fresh));
         DHDoc_common.mk_Ap(doc1, doc2);
       | TypAp(d1, ty) =>
         let doc1 = go'(d1);
         let doc2 = DHDoc_Typ.mk(~enforce_inline=true, ty);
         DHDoc_common.mk_TypAp(doc1, doc2);
       | Ap(Reverse, d1, d2) =>
-        let (doc1, doc2) = (
-          go_formattable(d1)
-          |> parenthesize(precedence(d1) > DHDoc_common.precedence_Ap),
-          go'(d2),
-        );
+        let (doc1, doc2) = (go'(d1), go'(d2));
         DHDoc_common.mk_rev_Ap(doc2, doc1);
-      | UnOp(Meta(Unquote), d) =>
-        DHDoc_common.mk_Ap(
-          text("$"),
-          go_formattable(d)
-          |> parenthesize(precedence(d) > DHDoc_common.precedence_Ap),
-        )
-      | UnOp(Bool(Not), d) =>
-        DHDoc_common.mk_Ap(
-          text("!"),
-          go_formattable(d)
-          |> parenthesize(precedence(d) > DHDoc_common.precedence_Not),
-        )
-      | UnOp(Int(Minus), d) =>
-        DHDoc_common.mk_Ap(
-          text("-"),
-          go_formattable(d)
-          |> parenthesize(precedence(d) > DHDoc_common.precedence_Minus),
-        )
+      | UnOp(Meta(Unquote), d) => DHDoc_common.mk_Ap(text("$"), go'(d))
+      | UnOp(Bool(Not), d) => DHDoc_common.mk_Ap(text("!"), go'(d))
+      | UnOp(Int(Minus), d) => DHDoc_common.mk_Ap(text("-"), go'(d))
       | BinOp(Int(op), d1, d2) =>
         // TODO assumes all bin int ops are left associative
-        let (doc1, doc2) =
-          mk_left_associative_operands(precedence_bin_int_op(op), d1, d2);
+        let (doc1, doc2) = mk_left_associative_operands(d1, d2);
         hseps([doc1, mk_bin_int_op(op), doc2]);
       | BinOp(Float(op), d1, d2) =>
         // TODO assumes all bin float ops are left associative
-        let (doc1, doc2) =
-          mk_left_associative_operands(precedence_bin_float_op(op), d1, d2);
+        let (doc1, doc2) = mk_left_associative_operands(d1, d2);
         hseps([doc1, mk_bin_float_op(op), doc2]);
       | BinOp(String(op), d1, d2) =>
         // TODO assumes all bin string ops are left associative
-        let (doc1, doc2) =
-          mk_left_associative_operands(precedence_bin_string_op(op), d1, d2);
+        let (doc1, doc2) = mk_left_associative_operands(d1, d2);
         hseps([doc1, mk_bin_string_op(op), doc2]);
       | Cons(d1, d2) =>
-        let (doc1, doc2) =
-          mk_right_associative_operands(DHDoc_common.precedence_Cons, d1, d2);
+        let (doc1, doc2) = mk_right_associative_operands(d1, d2);
         DHDoc_common.mk_Cons(doc1, doc2);
       | ListConcat(d1, d2) =>
-        let (doc1, doc2) =
-          mk_right_associative_operands(DHDoc_common.precedence_Plus, d1, d2);
+        let (doc1, doc2) = mk_right_associative_operands(d1, d2);
         DHDoc_common.mk_ListConcat(doc1, doc2);
       | BinOp(Bool(op), d1, d2) =>
-        let (doc1, doc2) =
-          mk_right_associative_operands(precedence_bin_bool_op(op), d1, d2);
+        let (doc1, doc2) = mk_right_associative_operands(d1, d2);
         hseps([doc1, mk_bin_bool_op(op), doc2]);
       | Tuple([]) => DHDoc_common.Delim.triv
       | Tuple(ds) => DHDoc_common.mk_Tuple(ds |> List.map(d => go'(d)))
@@ -407,9 +271,7 @@ let mk =
       | TyAlias(_, _, d) => go'(d)
       | Cast(d, t1, t2) when settings.show_casts =>
         // TODO[Matt]: Roll multiple casts into one cast
-        let doc =
-          go_formattable(d)
-          |> parenthesize(precedence(d) > DHDoc_common.precedence_Ap);
+        let doc = go'(d);
         Doc.(
           hcat(
             doc,
@@ -664,3 +526,5 @@ let mk =
   };
   go(d, env, enforce_inline, []);
 };
+
+let mk = exp => mk(exp |> ExpToSegment.parenthesize);
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
index ff55cfe7d5..8f3d5a2479 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
@@ -128,7 +128,7 @@ let mk_comma_seq = (ld, rd, l) => {
 
 let mk_ListLit = l => mk_comma_seq("[", "]", l);
 
-let mk_Tuple = elts => mk_comma_seq("(", ")", elts);
+let mk_Tuple = elts => mk_comma_seq("", "", elts);
 
 let mk_TypAp = (doc1, doc2) =>
   Doc.(hcats([doc1, text("@<"), doc2, text(">")]));
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index 52ffd1ac73..b06a5a3980 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -514,3 +514,6 @@ let rec unzip = (lst: list(('a, 'b))): (list('a), list('b)) => {
     ([a, ..._as], [b, ...bs]);
   };
 };
+
+let cross = (xs, ys) =>
+  List.concat(List.map(x => List.map(y => (x, y), ys), xs));