diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 1990461239..335a89a1da 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -279,7 +279,7 @@ let forms: list((string, t)) = [
   ("list_concat", mk_infix("@", Exp, P.plus)),
   ("cons_exp", mk_infix("::", Exp, P.cons)),
   ("cons_pat", mk_infix("::", Pat, P.cons)),
-  ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))),
+  ("typeann", mk(ss, [":"], mk_bin'(P.cast, Pat, Pat, [], Typ))),
   // UNARY PREFIX OPERATORS
   ("not", mk(ii, ["!"], mk_pre(P.not_, Exp, []))),
   ("typ_sum_single", mk(ss, ["+"], mk_pre(P.or_, Typ, []))),
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 7d72b66404..6f9f944255 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -2,60 +2,145 @@ 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;
 
+let associativity_map: ref(list((t, Direction.t))) = ref([]);
+let left_associative = (level: t) => {
+  associativity_map := [(level, Direction.Left), ...associativity_map^];
+  level;
+};
+let right_associative = (level: t) => {
+  associativity_map := [(level, Direction.Right), ...associativity_map^];
+  level;
+};
+
 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 semi = 16;
-let let_ = 17;
-let filter = 18;
-let rule_arr = 19;
-let rule_pre = 20;
-let rule_sep = 21;
-let case_ = 22;
-
-let comma = 15;
-
-let type_plus = 4;
-let type_arrow = 5;
-let type_prod = comma;
-
-let min = 26;
+// ========== TYPES ==========
+let type_sum_ap = 22;
+// _____ (Int)
+// + T1 + _____
+let type_plus = 25;
+// _____ -> Int
+let type_arrow = 28 |> right_associative;
+// Int -> _____
+// String , _____ , String
+let type_prod = 45;
+let type_binder = 38;
+// forall t -> _____
+// rec t -> _____
+
+// ======== PATTERNS =========
+// ======= EXPRESSIONS =======
+
+let unquote = 21;
+// $_____
+let ap = 22;
+// _____(x)
+// 5 : _____
+let cast = 23 |> left_associative;
+// _____ : T
+// - _____
+let neg = 24;
+// _____ ** 2
+let power = 25 |> right_associative;
+// 2 ** _____
+// 6 / _____
+let mult = 26 |> left_associative;
+let not_ = 26;
+// _____ / 6
+// 4 - _____
+let plus = 27 |> left_associative;
+// _____ - 4
+// _____ :: []
+let cons = 28 |> right_associative;
+// 1 :: _____
+// [1,2] @ _____
+let concat = 29 |> right_associative;
+// _____ @ [1,2]
+// x == _____
+let eqs = 30 |> left_associative;
+// _____ == x
+// _____ && true
+let and_ = 31;
+// true && _____
+// _____ || false
+let or_ = 32;
+// false || _____
+let if_ = 34;
+let fun_ = 35;
+// fun x -> _____
+let prod = 36;
+// a , _____ , x
+// _____ ; ()
+let semi = 37 |> right_associative;
+// () ; _____
+let let_ = 38;
+// let x = 3 in _____
+let rule_arr = 39;
+let rule_pre = 40;
+let rule_sep = 41;
+let case_ = 42;
+
+let comma = 45;
+
+let min = 46;
 
 let compare = (p1: t, p2: t): int =>
   (-1) * Int.compare((p1 :> int), (p2 :> int));
 // let min = (p1: t, p2: t): t => max(p1, p2);
 
 let associativity_map: IntMap.t(Direction.t) =
-  [
-    (mult, Direction.Left),
-    (plus, Left),
-    (power, Right),
-    (cons, Right),
-    (concat, Right),
-    (ann, Left),
-    (eqs, Left),
-    (type_arrow, Right),
-  ]
-  |> List.to_seq
-  |> IntMap.of_seq;
+  associativity_map^ |> List.to_seq |> IntMap.of_seq;
 
 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..2ebd9db88f
--- /dev/null
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -0,0 +1,1072 @@
+open Util;
+open PrettySegment;
+open Base;
+
+module Settings = {
+  type t = {
+    inline: bool,
+    fold_case_clauses: bool,
+    fold_fn_bodies: bool,
+    hide_fixpoints: bool,
+    fold_cast_types: bool,
+  };
+
+  let of_core = (~inline, settings: CoreSettings.t) => {
+    inline,
+    fold_case_clauses: !settings.evaluation.show_case_clauses,
+    fold_fn_bodies: !settings.evaluation.show_fn_bodies,
+    hide_fixpoints: !settings.evaluation.show_fixpoints,
+    fold_cast_types: !settings.evaluation.show_casts,
+  };
+};
+
+let should_add_space = (s1, s2) =>
+  switch () {
+  | _ when String.ends_with(s1, ~suffix="(") => false
+  | _ when String.ends_with(s1, ~suffix="[") => false
+  | _ when String.starts_with(s2, ~prefix=")") => false
+  | _ when String.starts_with(s2, ~prefix="]") => false
+  | _ when String.starts_with(s2, ~prefix=",") => false
+  | _ when String.starts_with(s2, ~prefix=";") => false
+  | _ when String.starts_with(s2, ~prefix=":") => false
+  | _ when String.ends_with(s1, ~suffix=" ") => false
+  | _ when String.starts_with(s2, ~prefix=" ") => false
+  | _ when String.ends_with(s1, ~suffix="⏎") => false
+  | _ when String.starts_with(s2, ~prefix="⏎") => false
+  | _ => true
+  };
+
+let text_to_pretty = (id, sort, str): pretty => {
+  p_just([
+    Tile({
+      id,
+      label: [str],
+      mold: Mold.mk_op(sort, []),
+      shards: [0],
+      children: [],
+    }),
+  ]);
+};
+
+let mk_form = (form_name: string, id, children): Piece.t => {
+  let form: Form.t = Form.get(form_name);
+  assert(List.length(children) == List.length(form.mold.in_));
+  // Add whitespaces
+  let children =
+    Aba.map_abas(
+      ((l, child, r)) => {
+        let lspace = should_add_space(l, child |> Segment.first_string);
+        let rspace = should_add_space(child |> Segment.last_string, r);
+        (lspace ? [Secondary(Secondary.mk_space(Id.mk()))] : [])
+        @ (
+          rspace ? child @ [Secondary(Secondary.mk_space(Id.mk()))] : child
+        );
+      },
+      Aba.mk(form.label, children),
+    )
+    |> Aba.get_bs;
+  Tile({
+    id,
+    label: form.label,
+    mold: form.mold,
+    shards: List.init(List.length(children) + 1, n => n),
+    children,
+  });
+};
+
+/* HACK[Matt]: Sometimes terms that should have multiple ids won't because
+   evaluation only ever gives them one */
+let pad_ids = (n: int, ids: list(Id.t)): list(Id.t) => {
+  let len = List.length(ids);
+  if (len < n) {
+    ids @ List.init(n - len, _ => Id.mk());
+  } else {
+    ListUtil.split_n(n, ids) |> fst;
+  };
+};
+
+let (@) = (seg1: Segment.t, seg2: Segment.t): Segment.t =>
+  switch (seg1, seg2) {
+  | ([], _) => seg2
+  | (_, []) => seg1
+  | _ =>
+    if (should_add_space(
+          Segment.last_string(seg1),
+          Segment.first_string(seg2),
+        )) {
+      seg1 @ [Secondary(Secondary.mk_space(Id.mk()))] @ seg2;
+    } else {
+      seg1 @ seg2;
+    }
+  };
+
+let fold_if = (condition, pieces) =>
+  if (condition) {
+    [
+      ProjectorPerform.Update.init(
+        Fold,
+        mk_form("parens_exp", Id.mk(), [pieces]),
+      ),
+    ];
+  } else {
+    pieces;
+  };
+
+/* 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 = (~settings: Settings.t, exp: Exp.t): pretty => {
+  let exp = Exp.substitute_closures(Environment.empty, exp);
+  let go = (~inline=settings.inline) =>
+    exp_to_pretty(~settings={...settings, inline});
+  switch (exp |> IdTagged.term_of) {
+  // Assume these have been removed by the parenthesizer
+  | DynamicErrorHole(_)
+  | Filter(_) => failwith("printing these not implemented yet")
+  // Forms which should be removed by substitute_closures
+  | Closure(_) => failwith("closure not removed before printing")
+  // Other cases
+  | 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})]);
+  | Undefined => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "undefined")
+  | 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 ++ "\"")
+  // TODO: Make sure types are correct
+  | Constructor(c, t) =>
+    let id = Id.mk();
+    let+ e = text_to_pretty(exp |> Exp.rep_id, Sort.Exp, c)
+    and+ t = typ_to_pretty(~settings: Settings.t, t);
+    e
+    @ [mk_form("typeasc", id, [])]
+    @ (t |> fold_if(settings.fold_cast_types));
+  | ListLit([]) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "[]")
+  | Deferral(_) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "deferral")
+  | ListLit([x, ...xs]) =>
+    // TODO: Add optional newlines
+    let* x = go(x)
+    and* xs = xs |> List.map(go) |> all;
+    let (id, ids) = (
+      exp.ids |> List.hd,
+      exp.ids |> List.tl |> pad_ids(List.length(xs)),
+    );
+    let form = (x, xs) =>
+      mk_form(
+        "list_lit_exp",
+        id,
+        [
+          x
+          @ List.flatten(
+              List.map2(
+                (id, x) => [mk_form("comma_exp", id, [])] @ x,
+                ids,
+                xs,
+              ),
+            ),
+        ],
+      );
+    p_just([form(x, xs)]);
+  | Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
+  | BinOp(op, l, r) =>
+    // TODO: Add optional newlines
+    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: [],
+      }),
+    ]
+    @ r;
+  | MultiHole(es) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~settings)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Fun(p, e, _, _) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~settings: Settings.t, p)
+    and+ e = go(e);
+    [mk_form("fun_", id, [p])] @ e |> fold_if(settings.fold_fn_bodies);
+  | TypFun(tp, e, _) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
+    and+ e = go(e);
+    [mk_form("typfun", id, [tp])] @ e |> fold_if(settings.fold_fn_bodies);
+  | Tuple([]) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "()")
+  | Tuple([_]) => failwith("Singleton Tuples are not allowed")
+  | Tuple([x, ...xs]) =>
+    // TODO: Add optional newlines
+    let+ x = go(x)
+    and+ xs = xs |> List.map(go) |> all;
+    let ids = exp.ids |> pad_ids(List.length(xs));
+    x
+    @ List.flatten(
+        List.map2((id, x) => [mk_form("comma_exp", id, [])] @ x, ids, xs),
+      );
+  | Let(p, e1, e2) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    // This step undoes the adding of fixpoints that happens in elaboration.
+    let e1 = settings.hide_fixpoints ? Exp.unfix(e1, p) : e1;
+    let+ p = pat_to_pretty(~settings: Settings.t, p)
+    and+ e1 = go(e1)
+    and+ e2 = go(e2);
+    let e2 =
+      settings.inline
+        ? e2 : [Secondary(Secondary.mk_newline(Id.mk()))] @ e2;
+    [mk_form("let_", id, [p, e1])] @ e2;
+  | FixF(p, e, _) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~settings: Settings.t, p)
+    and+ e = go(e);
+    [mk_form("fix", id, [p])] @ e;
+  | TyAlias(tp, t, e) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
+    and+ t = typ_to_pretty(~settings: Settings.t, t)
+    and+ e = go(e);
+    let e =
+      settings.inline ? e : [Secondary(Secondary.mk_newline(Id.mk()))] @ e;
+    [mk_form("type_alias", id, [tp, t])] @ e;
+  | Ap(Forward, e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("ap_exp", id, [e2])];
+  | Ap(Reverse, e1, e2) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2)
+    and+ op = text_to_pretty(id, Sort.Exp, "|>");
+    e2 @ op @ e1;
+  | TypAp(e, t) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e)
+    and+ tp = typ_to_pretty(~settings: Settings.t, t);
+    e @ [mk_form("ap_exp_typ", id, [tp])];
+  | DeferredAp(e, es) =>
+    // TODO: Add optional newlines
+    let+ e = go(e)
+    and+ es = es |> List.map(go) |> all;
+    let (id, ids) = (
+      exp.ids |> List.hd,
+      exp.ids |> List.tl |> pad_ids(List.length(es)),
+    );
+    e
+    @ [
+      mk_form(
+        "ap_exp",
+        id,
+        [
+          List.flatten(
+            List.map2(
+              (id, e) => [mk_form("comma_exp", id, [])] @ e,
+              ids,
+              es,
+            ),
+          ),
+        ],
+      ),
+    ];
+  | If(e1, e2, e3) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2)
+    and+ e3 = go(e3);
+    let e2 =
+      settings.inline
+        ? e2
+        : [Secondary(Secondary.mk_newline(Id.mk()))]
+          @ e2
+          @ [Secondary(Secondary.mk_newline(Id.mk()))];
+    let e3 =
+      settings.inline
+        ? e3 : [Secondary(Secondary.mk_newline(Id.mk()))] @ e3;
+    [mk_form("if_", id, [e1, e2])] @ e3;
+  | Seq(e1, e2) =>
+    // TODO: Make newline optional
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    let e2 =
+      settings.inline
+        ? e2 : [Secondary(Secondary.mk_newline(Id.mk()))] @ e2;
+    e1 @ [mk_form("cell-join", id, [])] @ e2;
+  | Test(e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("test", id, [e])];
+  | Parens(e) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("parens_exp", id, [e])];
+  | Cons(e1, e2) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("cons_exp", id, [])] @ e2;
+  | ListConcat(e1, e2) =>
+    // TODO: Add optional newlines
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("list_concat", id, [])] @ e2;
+  | UnOp(Meta(Unquote), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("unquote", id, [])] @ e;
+  | UnOp(Bool(Not), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("not", id, [])] @ e;
+  | UnOp(Int(Minus), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("unary_minus", id, [])] @ e;
+  /* TODO: this isn't actually correct because we could the builtin
+     could have been overriden in this scope; worth fixing when we fix
+     closures. */
+  | BuiltinFun(f) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, f)
+  | FailedCast(e, _, t)
+  | Cast(e, _, t) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e)
+    and+ t = typ_to_pretty(~settings: Settings.t, t);
+    e
+    @ [mk_form("typeasc", id, [])]
+    @ (t |> fold_if(settings.fold_cast_types));
+  | Match(e, rs) =>
+    // TODO: Add newlines
+    let+ e = go(e)
+    and+ rs: list((Segment.t, Segment.t)) = {
+      rs
+      |> List.map(((p, e)) =>
+           (pat_to_pretty(~settings: Settings.t, p), go(e))
+         )
+      |> List.map(((x, y)) => (x, y))
+      |> all;
+    };
+    let (id, ids) = (
+      exp.ids |> List.hd,
+      exp.ids |> List.tl |> pad_ids(List.length(rs)),
+    );
+    [
+      mk_form(
+        "case",
+        id,
+        [
+          e
+          @ (
+            List.map2(
+              (id, (p, e)) =>
+                settings.inline
+                  ? []
+                  : [Secondary(Secondary.mk_newline(Id.mk()))]
+                    @ [mk_form("rule", id, [p])]
+                    @ (e |> fold_if(settings.fold_case_clauses)),
+              ids,
+              rs,
+            )
+            |> List.flatten
+          )
+          @ (
+            settings.inline
+              ? [] : [Secondary(Secondary.mk_newline(Id.mk()))]
+          ),
+        ],
+      ),
+    ];
+  };
+}
+and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
+  let go = pat_to_pretty(~settings: Settings.t);
+  switch (pat |> Pat.term_of) {
+  | Invalid(t) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, t)
+  | EmptyHole =>
+    let id = pat |> Pat.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | Wild => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "_")
+  | Var(v) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, v)
+  | Int(n) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Int.to_string(n))
+  | Float(f) =>
+    text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Float.to_string(f))
+  | Bool(b) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Bool.to_string(b))
+  | String(s) =>
+    text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "\"" ++ s ++ "\"")
+  | Constructor(c, _) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, c)
+  | ListLit([]) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "[]")
+  | ListLit([x, ...xs]) =>
+    let* x = go(x)
+    and* xs = xs |> List.map(go) |> all;
+    let (id, ids) = (
+      pat.ids |> List.hd,
+      pat.ids |> List.tl |> pad_ids(List.length(xs)),
+    );
+    p_just([
+      mk_form(
+        "list_lit_pat",
+        id,
+        [
+          x
+          @ List.flatten(
+              List.map2(
+                (id, x) => [mk_form("comma_pat", id, [])] @ x,
+                ids,
+                xs,
+              ),
+            ),
+        ],
+      ),
+    ]);
+  | Cons(p1, p2) =>
+    let id = pat |> Pat.rep_id;
+    let+ p1 = go(p1)
+    and+ p2 = go(p2);
+    p1 @ [mk_form("cons_pat", id, [])] @ p2;
+  | Tuple([]) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "()")
+  | Tuple([_]) => failwith("Singleton Tuples are not allowed")
+  | Tuple([x, ...xs]) =>
+    let+ x = go(x)
+    and+ xs = xs |> List.map(go) |> all;
+    let ids = pat.ids |> pad_ids(List.length(xs));
+    x
+    @ List.flatten(
+        List.map2((id, x) => [mk_form("comma_pat", id, [])] @ x, ids, xs),
+      );
+  | Parens(p) =>
+    let id = pat |> Pat.rep_id;
+    let+ p = go(p);
+    [mk_form("parens_pat", id, [p])];
+  | MultiHole(es) =>
+    let id = pat |> Pat.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~settings: Settings.t)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Ap(p1, p2) =>
+    let id = pat |> Pat.rep_id;
+    let+ p1 = go(p1)
+    and+ p2 = go(p2);
+    p1 @ [mk_form("ap_pat", id, [p2])];
+  | Cast(p, t, _) =>
+    let id = pat |> Pat.rep_id;
+    let+ p = go(p)
+    and+ t = typ_to_pretty(~settings: Settings.t, t);
+    p @ [mk_form("typeann", id, [])] @ t;
+  };
+}
+and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
+  let go = typ_to_pretty(~settings: Settings.t);
+  let go_constructor: ConstructorMap.variant(Typ.t) => pretty =
+    fun
+    | Variant(c, ids, None) => text_to_pretty(List.hd(ids), Sort.Typ, c)
+    | Variant(c, ids, Some(x)) => {
+        let+ constructor =
+          text_to_pretty(List.hd(List.tl(ids)), Sort.Typ, c);
+        constructor @ [mk_form("ap_typ", List.hd(ids), [go(x)])];
+      }
+    | BadEntry(x) => go(x);
+  switch (typ |> Typ.term_of) {
+  | Unknown(Hole(Invalid(s))) =>
+    text_to_pretty(typ |> Typ.rep_id, Sort.Typ, s)
+  | Unknown(Internal)
+  | Unknown(SynSwitch)
+  | Unknown(Hole(EmptyHole)) =>
+    let id = typ |> Typ.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | Unknown(Hole(MultiHole(es))) =>
+    let id = typ |> Typ.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~settings: Settings.t)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Var(v) => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, v)
+  | Int => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Int")
+  | Float => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Float")
+  | Bool => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Bool")
+  | String => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "String")
+  | List(t) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go(t);
+    [mk_form("list_typ", id, [t])];
+  | Prod([]) => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "()")
+  | Prod([_]) => failwith("Singleton Prods are not allowed")
+  | Prod([t, ...ts]) =>
+    let+ t = go(t)
+    and+ ts = ts |> List.map(go) |> all;
+    t
+    @ List.flatten(
+        List.map2(
+          (id, t) => [mk_form("comma_typ", id, [])] @ t,
+          typ.ids |> pad_ids(ts |> List.length),
+          ts,
+        ),
+      );
+  | Parens(t) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go(t);
+    [mk_form("parens_typ", id, [t])];
+  | Ap(t1, t2) =>
+    let id = typ |> Typ.rep_id;
+    let+ t1 = go(t1)
+    and+ t2 = go(t2);
+    t1 @ [mk_form("ap_typ", id, [t2])];
+  | Rec(tp, t) =>
+    let id = typ |> Typ.rep_id;
+    let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
+    and+ t = go(t);
+    [mk_form("rec", id, [tp])] @ t;
+  | Forall(tp, t) =>
+    let id = typ |> Typ.rep_id;
+    let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
+    and+ t = go(t);
+    [mk_form("forall", id, [tp])] @ t;
+  | Arrow(t1, t2) =>
+    let id = typ |> Typ.rep_id;
+    let+ t1 = go(t1)
+    and+ t2 = go(t2);
+    t1 @ [mk_form("type-arrow", id, [])] @ t2;
+  | Sum([]) => failwith("Empty Sums are not allowed")
+  | Sum([t]) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go_constructor(t);
+    [mk_form("typ_sum_single", id, [])] @ t;
+  | Sum([t, ...ts]) =>
+    let ids = typ.ids |> pad_ids(List.length(ts) + 1);
+    let id = List.hd(ids);
+    let ids = List.tl(ids);
+    let+ t = go_constructor(t)
+    and+ ts = ts |> List.map(go_constructor) |> all;
+    [mk_form("typ_sum_single", id, [])]
+    @ t
+    @ List.flatten(
+        List.map2((id, t) => [mk_form("typ_plus", id, [])] @ t, ids, ts),
+      );
+  };
+}
+and tpat_to_pretty = (~settings: Settings.t, tpat: TPat.t): pretty => {
+  switch (tpat |> IdTagged.term_of) {
+  | Invalid(t) => text_to_pretty(tpat |> TPat.rep_id, Sort.Typ, t)
+  | EmptyHole =>
+    let id = tpat |> TPat.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | MultiHole(xs) =>
+    let id = tpat |> TPat.rep_id;
+    let+ xs = xs |> List.map(any_to_pretty(~settings: Settings.t)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), xs);
+  | Var(v) => text_to_pretty(tpat |> TPat.rep_id, Sort.Typ, v)
+  };
+}
+and any_to_pretty = (~settings: Settings.t, any: Any.t): pretty => {
+  switch (any) {
+  | Exp(e) => exp_to_pretty(~settings: Settings.t, e)
+  | Pat(p) => pat_to_pretty(~settings: Settings.t, p)
+  | Typ(t) => typ_to_pretty(~settings: Settings.t, t)
+  | TPat(tp) => tpat_to_pretty(~settings: Settings.t, tp)
+  | Any(_)
+  | Nul(_)
+  | Rul(_) =>
+    //TODO: print out invalid rules properly
+    let id = any |> Any.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  };
+};
+
+// Use Precedence.re to work out where your construct goes here.
+let rec external_precedence = (exp: Exp.t): Precedence.t => {
+  switch (IdTagged.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
+  | Deferral(_)
+  | BuiltinFun(_)
+  | Undefined => Precedence.max
+
+  // Same goes for forms which are already surrounded
+  | Parens(_)
+  | ListLit(_)
+  | Test(_)
+  | Match(_) => Precedence.max
+
+  // Other forms
+  | UnOp(Meta(Unquote), _) => Precedence.unquote
+  | Constructor(_) // Constructor is here because we currently always add a type annotation to constructors
+  | 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_
+
+  // Matt: 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.cast
+  | Tuple(_) => Precedence.prod
+
+  // Matt: I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
+  | MultiHole(_) => Precedence.min
+  };
+
+let external_precedence_typ = (tp: Typ.t) =>
+  switch (Typ.term_of(tp)) {
+  // Indivisible forms never need parentheses around them
+  | Unknown(Hole(Invalid(_)))
+  | Unknown(Internal)
+  | Unknown(SynSwitch)
+  | Unknown(Hole(EmptyHole))
+  | Var(_)
+  | Int
+  | Float
+  | Bool
+  | String => Precedence.max
+
+  // Same goes for forms which are already surrounded
+  | Parens(_)
+  | List(_) => Precedence.max
+
+  // Other forms
+  | Prod(_) => Precedence.type_prod
+  | Ap(_) => Precedence.type_sum_ap
+  | Arrow(_, _) => Precedence.type_arrow
+  | Sum(_) => Precedence.type_plus
+  | Rec(_, _) => Precedence.let_
+  | Forall(_, _) => Precedence.let_
+
+  // Matt: I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
+  | Unknown(Hole(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 paren_pat_assoc_at =
+    (internal_precedence: Precedence.t, pat: Pat.t): Pat.t =>
+  external_precedence_pat(pat) > internal_precedence
+    ? Pat.fresh(Parens(pat)) : pat;
+
+let paren_typ_at = (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
+  external_precedence_typ(typ) >= internal_precedence
+    ? Typ.fresh(Parens(typ)) : typ;
+
+let paren_typ_assoc_at =
+    (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
+  external_precedence_typ(typ) > internal_precedence
+    ? Typ.fresh(Parens(typ)) : typ;
+
+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(_) // Not indivisible because of the type annotation!
+  | Deferral(_)
+  | BuiltinFun(_)
+  | Undefined => exp
+
+  // Forms that currently need to stripped before outputting
+  | Closure(_, x)
+  | DynamicErrorHole(x, _)
+  | Tuple([x])
+  | Filter(_, x) => x |> parenthesize
+
+  // Other forms
+  | Constructor(c, t) =>
+    Constructor(c, paren_typ_at(Precedence.cast, t)) |> rewrap
+  | 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.prod)),
+    )
+    |> 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_assoc_at(Precedence.ap),
+      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),
+      parenthesize_typ(tp) |> paren_typ_at(Precedence.min),
+    )
+    |> 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
+  | Cast(e, t1, t2) =>
+    Cast(
+      parenthesize(e) |> paren_assoc_at(Precedence.cast),
+      parenthesize_typ(t1) |> paren_typ_at(Precedence.cast),
+      parenthesize_typ(t2) |> paren_typ_at(Precedence.cast),
+    )
+    |> rewrap
+  | FailedCast(e, t1, t2) =>
+    FailedCast(
+      parenthesize(e) |> paren_at(Precedence.cast),
+      parenthesize_typ(t1) |> paren_typ_at(Precedence.cast),
+      parenthesize_typ(t2) |> paren_typ_at(Precedence.cast),
+    )
+    |> 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(xs) => MultiHole(List.map(parenthesize_any, xs)) |> rewrap
+  };
+}
+and parenthesize_pat = (pat: Pat.t): Pat.t => {
+  let (term, rewrap) = Pat.unwrap(pat);
+  switch (term) {
+  // Indivisible forms dont' change
+  | Var(_)
+  | Invalid(_)
+  | Bool(_)
+  | Int(_)
+  | Float(_)
+  | String(_)
+  | EmptyHole
+  | Constructor(_) => pat
+
+  // Other forms
+  | Wild => pat
+  | Parens(p) =>
+    Parens(parenthesize_pat(p) |> paren_pat_at(Precedence.min)) |> rewrap
+  | Cons(p1, p2) =>
+    Cons(
+      parenthesize_pat(p1) |> paren_pat_at(Precedence.cons),
+      parenthesize_pat(p2) |> paren_pat_assoc_at(Precedence.cons),
+    )
+    |> rewrap
+  | Tuple(ps) =>
+    Tuple(
+      ps
+      |> List.map(parenthesize_pat)
+      |> List.map(paren_pat_at(Precedence.prod)),
+    )
+    |> rewrap
+  | ListLit(ps) =>
+    ListLit(
+      ps
+      |> List.map(parenthesize_pat)
+      |> List.map(paren_pat_at(Precedence.prod)),
+    )
+    |> rewrap
+  | Ap(p1, p2) =>
+    Ap(
+      parenthesize_pat(p1) |> paren_pat_assoc_at(Precedence.ap),
+      parenthesize_pat(p2) |> paren_pat_at(Precedence.min),
+    )
+    |> rewrap
+  | MultiHole(xs) => MultiHole(List.map(parenthesize_any, xs)) |> rewrap
+  | Cast(p, t1, t2) =>
+    Cast(
+      parenthesize_pat(p) |> paren_pat_assoc_at(Precedence.cast),
+      parenthesize_typ(t1) |> paren_typ_at(Precedence.max), // Hack[Matt]: always add parens to get the arrows right
+      parenthesize_typ(t2) |> paren_typ_at(Precedence.max),
+    )
+    |> rewrap
+  };
+}
+
+and parenthesize_typ = (typ: Typ.t): Typ.t => {
+  let (term, rewrap) = Typ.unwrap(typ);
+  switch (term) {
+  // Indivisible forms dont' change
+  | Var(_)
+  | Unknown(Hole(Invalid(_)))
+  | Unknown(Internal)
+  | Unknown(SynSwitch)
+  | Unknown(Hole(EmptyHole))
+  | Int
+  | Float
+  | Bool
+  | String => typ
+
+  // Other forms
+  | Parens(t) =>
+    Parens(parenthesize_typ(t) |> paren_typ_at(Precedence.min)) |> rewrap
+  | List(t) =>
+    List(parenthesize_typ(t) |> paren_typ_at(Precedence.min)) |> rewrap
+  | Prod(ts) =>
+    Prod(
+      ts
+      |> List.map(parenthesize_typ)
+      |> List.map(paren_typ_at(Precedence.type_prod)),
+    )
+    |> rewrap
+  | Ap(t1, t2) =>
+    Ap(
+      parenthesize_typ(t1) |> paren_typ_assoc_at(Precedence.type_sum_ap),
+      parenthesize_typ(t2) |> paren_typ_at(Precedence.min),
+    )
+    |> rewrap
+  | Rec(tp, t) =>
+    Rec(
+      tp,
+      parenthesize_typ(t) |> paren_typ_assoc_at(Precedence.type_binder),
+    )
+    |> rewrap
+  | Forall(tp, t) =>
+    Forall(
+      tp,
+      parenthesize_typ(t) |> paren_typ_assoc_at(Precedence.type_binder),
+    )
+    |> rewrap
+  | Arrow(t1, t2) =>
+    Arrow(
+      parenthesize_typ(t1) |> paren_typ_at(Precedence.type_arrow),
+      parenthesize_typ(t2) |> paren_typ_assoc_at(Precedence.type_arrow),
+    )
+    |> rewrap
+  | Sum(ts) =>
+    Sum(
+      ConstructorMap.map(
+        ts =>
+          ts
+          |> Option.map(parenthesize_typ)
+          |> Option.map(paren_typ_at(Precedence.type_plus)),
+        ts,
+      ),
+    )
+    |> rewrap
+  | Unknown(Hole(MultiHole(xs))) =>
+    Unknown(Hole(MultiHole(List.map(parenthesize_any, xs)))) |> rewrap
+  };
+}
+
+and parenthesize_tpat = (tpat: TPat.t): TPat.t => {
+  let (term, rewrap) = IdTagged.unwrap(tpat);
+  switch (term) {
+  // Indivisible forms dont' change
+  | Var(_)
+  | Invalid(_)
+  | EmptyHole => tpat
+
+  // Other forms
+  | MultiHole(xs) => TPat.MultiHole(List.map(parenthesize_any, xs)) |> rewrap
+  };
+}
+
+and parenthesize_rul = (rul: Rul.t): Rul.t => {
+  let (term, rewrap) = IdTagged.unwrap(rul);
+  switch (term) {
+  // Indivisible forms dont' change
+  | Invalid(_) => rul
+
+  // Other forms
+  | Rules(e, ps) =>
+    Rul.Rules(
+      parenthesize(e),
+      List.map(((p, e)) => (parenthesize_pat(p), parenthesize(e)), ps),
+    )
+    |> rewrap
+  | Hole(xs) => Rul.Hole(List.map(parenthesize_any, xs)) |> rewrap
+  };
+}
+
+and parenthesize_any = (any: Any.t): Any.t =>
+  switch (any) {
+  | Exp(e) => Exp(parenthesize(e))
+  | Pat(p) => Pat(parenthesize_pat(p))
+  | Typ(t) => Typ(parenthesize_typ(t))
+  | TPat(tp) => TPat(parenthesize_tpat(tp))
+  | Rul(r) => Rul(parenthesize_rul(r))
+  | Any(_) => any
+  | Nul(_) => any
+  };
+
+let exp_to_segment = (~settings, exp: Exp.t): Segment.t => {
+  let exp = exp |> Exp.substitute_closures(Builtins.env_init) |> parenthesize;
+  let p = exp_to_pretty(~settings, exp);
+  p |> PrettySegment.select;
+};
+
+let typ_to_segment = (~settings, typ: Typ.t): Segment.t => {
+  let typ = parenthesize_typ(typ);
+  let p = typ_to_pretty(~settings, typ);
+  p |> PrettySegment.select;
+};
diff --git a/src/haz3lcore/pretty/PrettySegment.re b/src/haz3lcore/pretty/PrettySegment.re
new file mode 100644
index 0000000000..ee8faa3f13
--- /dev/null
+++ b/src/haz3lcore/pretty/PrettySegment.re
@@ -0,0 +1,23 @@
+/* This file is a placeholder, ideally an algorithm would be implemented here that allows
+   efficient calculation of the best way to add linebreaks etc, but that hasn't been implemented yet, so
+   none of these functions do anything yet. (Matt) */
+
+type pretty = Segment.t;
+
+let p_concat = (pretty2, pretty1) => pretty1 @ pretty2;
+let p_or = (_pretty2, pretty1) => pretty1;
+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) => f(pretty);
+let (and+) = (pretty1, pretty2) => (pretty1, pretty2);
+
+let ( let* ) = (pretty, f) => f(pretty);
+let ( and* ) = (pretty1, pretty2) => (pretty1, pretty2);
+
+let all = x => x;
+
+let select: pretty => Segment.t = x => x;
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 0493150865..14db116c68 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -271,6 +271,26 @@ module Pat = {
     | Constructor(name, _) => Some(name)
     | _ => None
     };
+
+  let rec bound_vars = (dp: t): list(Var.t) =>
+    switch (dp |> term_of) {
+    | EmptyHole
+    | MultiHole(_)
+    | Wild
+    | Invalid(_)
+    | Int(_)
+    | Float(_)
+    | Bool(_)
+    | String(_)
+    | Constructor(_) => []
+    | Cast(y, _, _)
+    | Parens(y) => bound_vars(y)
+    | Var(y) => [y]
+    | Tuple(dps) => List.flatten(List.map(bound_vars, dps))
+    | Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
+    | ListLit(dps) => List.flatten(List.map(bound_vars, dps))
+    | Ap(_, dp1) => bound_vars(dp1)
+    };
 };
 
 module Exp = {
@@ -551,6 +571,176 @@ module Exp = {
       | Constructor(_) => None
       };
     };
+
+  let rec substitute_closures =
+          (
+            env: Environment.t,
+            old_bound_vars: list(string),
+            new_bound_vars: list(string),
+          ) =>
+    map_term(
+      ~f_exp=
+        (cont, e) => {
+          let (term, rewrap) = unwrap(e);
+          switch (term) {
+          // Variables: lookup if bound
+          | Var(x) =>
+            switch (Environment.lookup(env, x)) {
+            | Some(e) =>
+              e |> substitute_closures(env, old_bound_vars, new_bound_vars)
+            | None =>
+              Var(
+                List.mem(x, old_bound_vars)
+                  ? x : Var.free_name(x, new_bound_vars),
+              )
+              |> rewrap
+            }
+          // Forms with environments: look up in new environment
+          | Closure(env, e) =>
+            substitute_closures(
+              env |> ClosureEnvironment.map_of,
+              [],
+              new_bound_vars,
+              e,
+            )
+          | Fun(p, e, Some(env), n) =>
+            let pat_bound_vars = Pat.bound_vars(p);
+            Fun(
+              p,
+              substitute_closures(
+                env
+                |> ClosureEnvironment.map_of
+                |> Environment.without_keys(pat_bound_vars),
+                pat_bound_vars,
+                pat_bound_vars @ new_bound_vars,
+                e,
+              ),
+              None,
+              n,
+            )
+            |> rewrap;
+          | FixF(p, e, Some(env)) =>
+            let pat_bound_vars = Pat.bound_vars(p);
+            FixF(
+              p,
+              substitute_closures(
+                env
+                |> ClosureEnvironment.map_of
+                |> Environment.without_keys(pat_bound_vars),
+                pat_bound_vars,
+                pat_bound_vars @ new_bound_vars,
+                e,
+              ),
+              None,
+            )
+            |> rewrap;
+          // Cases with binders: remove binder from env
+          | Let(p, e1, e2) =>
+            let pat_bound_vars = Pat.bound_vars(p);
+            Let(
+              p,
+              substitute_closures(env, old_bound_vars, new_bound_vars, e1),
+              substitute_closures(
+                env |> Environment.without_keys(pat_bound_vars),
+                pat_bound_vars @ old_bound_vars,
+                pat_bound_vars @ new_bound_vars,
+                e2,
+              ),
+            )
+            |> rewrap;
+          | Match(e, cases) =>
+            Match(
+              substitute_closures(env, old_bound_vars, new_bound_vars, e),
+              cases
+              |> List.map(((p, e)) => {
+                   let pat_bound_vars = Pat.bound_vars(p);
+                   (
+                     p,
+                     substitute_closures(
+                       env |> Environment.without_keys(pat_bound_vars),
+                       pat_bound_vars @ old_bound_vars,
+                       pat_bound_vars @ new_bound_vars,
+                       e,
+                     ),
+                   );
+                 }),
+            )
+            |> rewrap
+          | Fun(p, e, None, n) =>
+            let pat_bound_vars = Pat.bound_vars(p);
+            Fun(
+              p,
+              substitute_closures(
+                env |> Environment.without_keys(pat_bound_vars),
+                pat_bound_vars @ old_bound_vars,
+                pat_bound_vars @ new_bound_vars,
+                e,
+              ),
+              None,
+              n,
+            )
+            |> rewrap;
+          | FixF(p, e, None) =>
+            let pat_bound_vars = Pat.bound_vars(p);
+            FixF(
+              p,
+              substitute_closures(
+                env |> Environment.without_keys(pat_bound_vars),
+                pat_bound_vars @ old_bound_vars,
+                pat_bound_vars @ new_bound_vars,
+                e,
+              ),
+              None,
+            )
+            |> rewrap;
+          // Other cases: recurse
+          | Invalid(_)
+          | EmptyHole
+          | MultiHole(_)
+          | DynamicErrorHole(_)
+          | FailedCast(_)
+          | Deferral(_)
+          | Bool(_)
+          | Int(_)
+          | Float(_)
+          | String(_)
+          | ListLit(_)
+          | Constructor(_)
+          | TypFun(_)
+          | Tuple(_)
+          | TyAlias(_)
+          | Ap(_)
+          | TypAp(_)
+          | DeferredAp(_)
+          | If(_)
+          | Seq(_)
+          | Test(_)
+          | Filter(_)
+          | Parens(_)
+          | Cons(_)
+          | ListConcat(_)
+          | UnOp(_)
+          | BinOp(_)
+          | BuiltinFun(_)
+          | Cast(_)
+          | Undefined => cont(e)
+          };
+        },
+      _,
+    );
+  let substitute_closures = substitute_closures(_, [], []);
+
+  let unfix = (e: t, p: Pat.t) => {
+    switch (e.term) {
+    | FixF(p1, e1, _) =>
+      if (Pat.fast_equal(p, p1)) {
+        e1;
+      } else {
+        e;
+      }
+    | _ => e
+    };
+  };
 };
 
 module Rul = {
diff --git a/src/haz3lcore/statics/Var.re b/src/haz3lcore/statics/Var.re
index 68c3d9d1b3..a840aa33e7 100644
--- a/src/haz3lcore/statics/Var.re
+++ b/src/haz3lcore/statics/Var.re
@@ -27,3 +27,10 @@ let split = (pos, name) => {
 
 /* Used for VarBstMap */
 let compare = (x: t, y: t) => compare(x, y);
+
+let rec free_name = (x: t, bound: list(t)) =>
+  if (List.mem(x, bound)) {
+    free_name(x ++ "'", bound);
+  } else {
+    x;
+  };
diff --git a/src/haz3lcore/tiles/Secondary.re b/src/haz3lcore/tiles/Secondary.re
index c973469254..7db7861256 100644
--- a/src/haz3lcore/tiles/Secondary.re
+++ b/src/haz3lcore/tiles/Secondary.re
@@ -24,6 +24,8 @@ let cls_of = (s: t): cls =>
 
 let mk_space = id => {content: Whitespace(Form.space), id};
 
+let mk_newline = id => {content: Whitespace(Form.linebreak), id};
+
 let construct_comment = content =>
   if (String.equal(content, "#")) {
     Comment("##");
diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re
index de8689f08a..b1ec3b1df0 100644
--- a/src/haz3lcore/tiles/Segment.re
+++ b/src/haz3lcore/tiles/Segment.re
@@ -674,3 +674,22 @@ and ids_of_piece = (p: Piece.t): list(Id.t) =>
   | Secondary(_)
   | Projector(_) => [Piece.id(p)]
   };
+
+let first_string =
+  fun
+  | [] => "EMPTY"
+  | [Piece.Secondary(w), ..._] => Secondary.get_string(w.content)
+  | [Piece.Projector(_), ..._] => "PROJECTOR"
+  | [Piece.Grout(_), ..._] => "?"
+  | [Piece.Tile(t), ..._] => t.label |> List.hd;
+
+let last_string =
+  fun
+  | [] => "EMPTY"
+  | xs =>
+    switch (ListUtil.last(xs)) {
+    | Piece.Secondary(w) => Secondary.get_string(w.content)
+    | Piece.Grout(_) => "?"
+    | Piece.Projector(_) => "PROJECTOR"
+    | Piece.Tile(t) => t.label |> ListUtil.last
+    };
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index 9c6bed90b0..350838a870 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -526,3 +526,54 @@ 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));
+
+let rec intersperse = (sep, xs) =>
+  switch (xs) {
+  | [] => []
+  | [x] => [x]
+  | [x, ...xs] => [x, sep, ...intersperse(sep, xs)]
+  };
+
+let rec flat_intersperse = (sep, xss) =>
+  switch (xss) {
+  | [] => []
+  | [xs] => xs
+  | [xs, ...xss] => xs @ [sep, ...flat_intersperse(sep, xss)]
+  };
+
+let rec map_last_only = (f, xs) =>
+  switch (xs) {
+  | [] => []
+  | [x] => [f(x)]
+  | [x, ...xs] => [x, ...map_last_only(f, xs)]
+  };
+
+let rec split_last = (xs: list('x)): (list('x), 'x) =>
+  switch (xs) {
+  | [] => failwith("ListUtil.split_last")
+  | [x] => ([], x)
+  | [x, ...xs] =>
+    let (prefix, last) = split_last(xs);
+    ([x, ...prefix], last);
+  };
+
+let minimum = (f: 'a => int, xs: list('a)): option('a) =>
+  switch (xs) {
+  | [] => None
+  | [x, ...xs] =>
+    let rec loop = (best: 'a, best_f: int, xs: list('a)): option('a) =>
+      switch (xs) {
+      | [] => Some(best)
+      | [x, ...xs] =>
+        let f_x = f(x);
+        if (f_x < best_f) {
+          loop(x, f_x, xs);
+        } else {
+          loop(best, best_f, xs);
+        };
+      };
+    loop(x, f(x), xs);
+  };