From 6833e0f82f2be586c4313d68089b8cf8846abc07 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 13:58:14 -0500
Subject: [PATCH 01/11] Rename PATH_ABS to ABS and PATH_APP to DIM_APP.

---
 src/redprl/machine.fun       | 32 ++++++++++++++++----------------
 src/redprl/operator.sml      | 10 +++++-----
 src/redprl/pretty.sml        |  8 ++++----
 src/redprl/redprl.grm        |  4 ++--
 src/redprl/refiner.fun       | 14 +++++++-------
 src/redprl/refiner_types.fun | 34 +++++++++++++++++-----------------
 src/redprl/syntax.sml        | 10 +++++-----
 7 files changed, 56 insertions(+), 56 deletions(-)

diff --git a/src/redprl/machine.fun b/src/redprl/machine.fun
index 378a0139c..53fb5277a 100644
--- a/src/redprl/machine.fun
+++ b/src/redprl/machine.fun
@@ -29,7 +29,7 @@ struct
    | WIF of (variable * abt) * hole * abt * abt
    | S1_REC of (variable * abt) * hole * abt * (variable * abt)
    | IF of hole * abt * abt
-   | PATH_APP of hole * abt
+   | DIM_APP of hole * abt
    | NAT_REC of hole * abt * (variable * variable * abt)
    | INT_REC of hole * abt * (variable * variable * abt) * abt * (variable * variable * abt)
    | PROJ of string * hole
@@ -53,7 +53,7 @@ struct
        | IF (HOLE, t, f) => Syn.into @@ Syn.IF (m, (t, f))
        | WIF ((x, tyx), HOLE, t, f) => Syn.into @@ Syn.WIF ((x, tyx), m, (t, f))
        | S1_REC ((x, tyx), HOLE, base, (u, loop)) => Syn.into @@ Syn.S1_REC ((x, tyx), m, (base, (u, loop)))
-       | PATH_APP (HOLE, r) => Syn.into @@ Syn.PATH_APP (m, r)
+       | DIM_APP (HOLE, r) => Syn.into @@ Syn.DIM_APP (m, r)
        | NAT_REC (HOLE, zer, (x, y, succ)) => Syn.into @@ Syn.NAT_REC (m, (zer, (x, y, succ)))
        | INT_REC (HOLE, zer, (x,y,succ), negone, (x',y',negss)) => Syn.into @@ Syn.INT_REC (m, (zer, (x,y,succ), negone, (x',y',negss)))
        | PROJ (lbl, HOLE) => Syn.into @@ Syn.PROJ (lbl, m)
@@ -545,16 +545,16 @@ struct
          CRITICAL @@ lambda || (SymSet.remove syms u, stk)
        end
 
-     | O.PATH_ABS $ _ || (_, []) => raise Final
+     | O.ABS $ _ || (_, []) => raise Final
      | O.PATH_TY $ _ || (_, []) => raise Final
      | O.LINE_TY $ _ || (_, []) => raise Final
 
-     | O.PATH_APP $ [_ \ m, _ \ r] || (syms, stk) => COMPAT @@ m || (syms, PATH_APP (HOLE, r) :: stk)
-     | O.PATH_ABS $ [[x] \ m] || (syms, PATH_APP (HOLE, r) :: stk) => CRITICAL @@ substVar (r, x) m || (syms, stk)
+     | O.DIM_APP $ [_ \ m, _ \ r] || (syms, stk) => COMPAT @@ m || (syms, DIM_APP (HOLE, r) :: stk)
+     | O.ABS $ [[x] \ m] || (syms, DIM_APP (HOLE, r) :: stk) => CRITICAL @@ substVar (r, x) m || (syms, stk)
 
      | O.PATH_TY $ [[u] \ tyu, _ \ m0, _ \ m1] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
        let
-         fun apu m = Syn.into @@ Syn.PATH_APP (m, check (`u, O.DIM))
+         fun apu m = Syn.into @@ Syn.DIM_APP (m, check (`u, O.DIM))
          val v = Sym.named "_"
          val hcomu =
            Syn.intoHcom
@@ -562,7 +562,7 @@ struct
               ty = tyu,
               cap = apu cap,
               tubes = ((VarKit.toDim u, Syn.into Syn.DIM0), (v, m0)) :: ((VarKit.toDim u, Syn.into Syn.DIM1), (v, m1)) :: mapTubes_ apu tubes}
-         val abs = Syn.into @@ Syn.PATH_ABS (u, hcomu)
+         val abs = Syn.into @@ Syn.ABS (u, hcomu)
        in
          CRITICAL @@ abs || (syms, stk)
        end
@@ -572,9 +572,9 @@ struct
            Syn.into @@ Syn.COM
              {dir = dir,
               ty = (v, tyuv),
-              cap = Syn.into @@ Syn.PATH_APP (coercee, check (`u, O.DIM)),
+              cap = Syn.into @@ Syn.DIM_APP (coercee, check (`u, O.DIM)),
               tubes = [((VarKit.toDim u, Syn.into Syn.DIM0), (v, m0v)), ((VarKit.toDim u, Syn.into Syn.DIM1), (v, m1v))]}
-         val abs = Syn.into @@ Syn.PATH_ABS (u, comu)
+         val abs = Syn.into @@ Syn.ABS (u, comu)
        in
          CRITICAL @@ abs || (SymSet.remove syms v, stk)
        end
@@ -582,14 +582,14 @@ struct
      | O.LINE_TY $ [[u] \ tyu] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
        let
          val utm = VarKit.toDim u
-         fun apu n = Syn.into @@ Syn.PATH_APP (n, utm)
+         fun apu n = Syn.into @@ Syn.DIM_APP (n, utm)
          val hcomu = 
            Syn.intoHcom
              {dir = dir,
               ty = tyu,
               cap = apu cap,
               tubes = mapTubes_ apu tubes}
-         val abs = Syn.into @@ Syn.PATH_ABS (u, hcomu)
+         val abs = Syn.into @@ Syn.ABS (u, hcomu)
        in
          CRITICAL @@ abs || (syms, stk)
        end
@@ -600,8 +600,8 @@ struct
            Syn.intoCoe
              {dir = dir,
               ty = (v, tyuv),
-              coercee = Syn.into @@ Syn.PATH_APP (coercee, VarKit.toDim u)}
-         val abs = Syn.into @@ Syn.PATH_ABS (u,coe)
+              coercee = Syn.into @@ Syn.DIM_APP (coercee, VarKit.toDim u)}
+         val abs = Syn.into @@ Syn.ABS (u,coe)
        in
          CRITICAL @@ abs || (SymSet.remove syms u, stk)
        end
@@ -830,7 +830,7 @@ struct
                                 ty = substVar (s, v) b,
                                 cap = projFromOne s,
                                 tubes =
-                                  [ ((s, Syn.intoDim 0), (w, Syn.into @@ Syn.PATH_APP (Syn.intoSnd (fiberFromOne s), VarKit.toDim w)))
+                                  [ ((s, Syn.intoDim 0), (w, Syn.into @@ Syn.DIM_APP (Syn.intoSnd (fiberFromOne s), VarKit.toDim w)))
                                   , ((s, Syn.intoDim 1), (w, projFromOne s)) ]}
                            end
                        in
@@ -860,7 +860,7 @@ struct
                                   in
                                     Syn.intoAnonTuple
                                       [ m
-                                      , Syn.into @@ Syn.PATH_ABS (z,
+                                      , Syn.into @@ Syn.ABS (z,
                                           Syn.intoCom
                                             {dir = (Syn.intoDim 0, VarKit.toDim y),
                                              ty = (y, substVar (Syn.intoDim 0, v) b),
@@ -895,7 +895,7 @@ struct
                                          , ((#1 dir, #2 dir),
                                             (w, Syn.into @@ Syn.VPROJ (#2 dir, coercee, Syn.intoFst @@ substVar (#2 dir, v) e)))
                                          , ((#2 dir, Syn.intoDim 0),
-                                            (w, Syn.into @@ Syn.PATH_APP (Syn.intoSnd frontFiber, VarKit.toDim w))) ]}
+                                            (w, Syn.into @@ Syn.DIM_APP (Syn.intoSnd frontFiber, VarKit.toDim w))) ]}
                                   end
                               in
                                 Syn.into @@ Syn.VIN (#2 dir, Syn.intoFst frontFiber, n)
diff --git a/src/redprl/operator.sml b/src/redprl/operator.sml
index ff1f45ad6..32f47ef91 100644
--- a/src/redprl/operator.sml
+++ b/src/redprl/operator.sml
@@ -176,7 +176,7 @@ struct
    (* record and tuple *)
    | RECORD of string list | TUPLE of string list | PROJ of string | TUPLE_UPDATE of string
    (* path: path abstraction and application *)
-   | PATH_TY | PATH_ABS | PATH_APP
+   | PATH_TY | ABS | DIM_APP
    (* lines: paths without fixed endpoints *)
    | LINE_TY
    (* equality *)
@@ -322,8 +322,8 @@ struct
 
      | PATH_TY => [[DIM] |: EXP, [] |: EXP, [] |: EXP] ->> EXP
      | LINE_TY => [[DIM] |: EXP] ->> EXP
-     | PATH_ABS => [[DIM] |: EXP] ->> EXP
-     | PATH_APP => [[] |: EXP, [] |: DIM] ->> EXP
+     | ABS => [[DIM] |: EXP] ->> EXP
+     | DIM_APP => [[] |: EXP, [] |: DIM] ->> EXP
 
      | FCOM => [[] |: DIM, [] |: DIM, [] |: EXP, [] |: VEC TUBE] ->> EXP
      | BOX => [[] |: DIM, [] |: DIM, [] |: EXP, [] |: VEC BDRY] ->> EXP
@@ -468,8 +468,8 @@ struct
 
      | PATH_TY => "path"
      | LINE_TY => "line"
-     | PATH_ABS => "abs"
-     | PATH_APP => "path-app"
+     | ABS => "abs"
+     | DIM_APP => "path-app"
 
      | UNIVERSE => "U"
      | V => "V"
diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index d79924fc3..ccbb24c7e 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -125,13 +125,13 @@ struct
 
   fun multiPathAbs (us : variable list) m =
     case Abt.out m of
-       O.PATH_ABS $ [[u] \ mu] =>
+       O.ABS $ [[u] \ mu] =>
          multiPathAbs (u :: us) mu
      | _ => (List.rev us, m)
 
   fun multiPathApp m (rs : abt list) =
     case Abt.out m of
-       O.PATH_APP $ [_ \ m, _ \ r] =>
+       O.DIM_APP $ [_ \ m, _ \ r] =>
          multiPathApp m (r :: rs)
      | _ => (m, rs)
 
@@ -222,9 +222,9 @@ struct
          end
      | O.PROJ lbl $ [m] =>
          Atomic.parens @@ expr @@ hvsep [char #"!", ppLabel lbl, ppBinder m]
-     | O.PATH_ABS $ _ =>
+     | O.ABS $ _ =>
          printPathAbs @@ multiPathAbs [] m
-     | O.PATH_APP $ _ =>
+     | O.DIM_APP $ _ =>
          printPathApp @@ multiPathApp m []
      | O.EQUALITY $ args =>
          Atomic.parens @@ expr @@ hvsep @@
diff --git a/src/redprl/redprl.grm b/src/redprl/redprl.grm
index 0ad47fb12..4137429a9 100644
--- a/src/redprl/redprl.grm
+++ b/src/redprl/redprl.grm
@@ -84,10 +84,10 @@ struct
     List.foldl (fn (n, app) => O.APP $$ [[] \ app, [] \ n]) m ns
 
   fun makePathAbs [] m = m
-    | makePathAbs (u::us) m = O.PATH_ABS $$ [[Option.getOpt (u, "_")] \ makePathAbs us m]
+    | makePathAbs (u::us) m = O.ABS $$ [[Option.getOpt (u, "_")] \ makePathAbs us m]
 
   fun makePathApp m ns =
-    List.foldl (fn (r, app) => O.PATH_APP $$ [[] \ app, [] \ r]) m ns
+    List.foldl (fn (r, app) => O.DIM_APP $$ [[] \ app, [] \ r]) m ns
 
   fun makeNum i =
     case IntInf.compare (i, 0) of
diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index ab533432d..08b4e28fb 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -482,7 +482,7 @@ struct
        | Syn.S1_REC _ => true
        | Syn.APP (f, _) => autoSynthesizableNeu sign f
        | Syn.PROJ (_, t) => autoSynthesizableNeu sign t
-       | Syn.PATH_APP (l, _) => autoSynthesizableNeu sign l
+       | Syn.DIM_APP (l, _) => autoSynthesizableNeu sign l
        | Syn.CUST => true (* XXX should check the signature *)
        | _ => false
   in
@@ -538,7 +538,7 @@ struct
          | (Syn.APP (f, _), Syn.APP _) => if autoSynthesizableNeu sign f then Lcf.rule o Fun.EqTypeApp
                                           else fail @@ E.NOT_APPLICABLE (Fpp.text "StepEq", Fpp.text "unresolved synth")
          | (Syn.PROJ _, Syn.PROJ _) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "EqType with `!`"
-         | (Syn.PATH_APP (_, _), Syn.PATH_APP (_, _)) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "EqType with `@`" (* pattern used to have a var for the dimension; needed? *)
+         | (Syn.DIM_APP (_, _), Syn.DIM_APP (_, _)) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "EqType with `@`" (* pattern used to have a var for the dimension; needed? *)
          | (Syn.CUST, Syn.CUST) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "EqType with custom operators"
          | _ => fail @@ E.NOT_APPLICABLE (Fpp.text "StepEqTypeNeuByStruct", Fpp.hvsep [TermPrinter.ppTerm m, Fpp.text "and", TermPrinter.ppTerm n])
 
@@ -631,7 +631,7 @@ struct
          | (Syn.APP (f, _), Syn.APP _) => if autoSynthesizableNeu sign f then Lcf.rule o Fun.EqApp
                                           else fail @@ E.NOT_APPLICABLE (Fpp.text "StepEq", Fpp.text "unresolved synth")
          | (Syn.PROJ _, Syn.PROJ _) => Lcf.rule o Record.EqProj (* XXX should consult autoSynthesizableNeu *)
-         | (Syn.PATH_APP (_, r1), Syn.PATH_APP (_, r2)) =>
+         | (Syn.DIM_APP (_, r1), Syn.DIM_APP (_, r2)) =>
            (case (Abt.out r1, Abt.out r2) of 
                (`_, `_) => Lcf.rule o Path.EqApp orelse_ Lcf.rule o Line.EqApp
              | _ =>  fail @@ E.NOT_APPLICABLE (Fpp.text "StepEqNeuByStruct", Fpp.hvsep [TermPrinter.ppTerm m, Fpp.text "and", TermPrinter.ppTerm n]))
@@ -723,11 +723,11 @@ struct
            (_, Machine.REDEX, _, _) => Lcf.rule o Computation.SequentReduce sign [O.IN_CONCL]
          | (_, _, _, Machine.REDEX) => Lcf.rule o Computation.SequentReduce sign [O.IN_CONCL]
          | (_, Machine.CANONICAL, _, Machine.CANONICAL) => StepEqVal sign (m, n) ty
-         | (Syn.PATH_APP (_, r), _, _, _) => 
+         | (Syn.DIM_APP (_, r), _, _, _) =>
            (case Abt.out r of 
               `_ => kont ((m, n), ty)
              | _ => Lcf.rule o Path.EqAppConst)
-         | (_, _, Syn.PATH_APP (_, r), _) =>
+         | (_, _, Syn.DIM_APP (_, r), _) =>
            (case Abt.out r of 
               `_ => kont ((m, n), ty)
              | _ => CatJdgSymmetry then_ Lcf.rule o Path.EqAppConst)
@@ -760,7 +760,7 @@ struct
          | Syn.S1_REC _ => Lcf.rule o S1.SynthElim
          | Syn.APP _ => Lcf.rule o Fun.SynthApp
          | Syn.PROJ _ => Lcf.rule o Record.SynthProj
-         | Syn.PATH_APP _ => Lcf.rule o Path.SynthApp par Lcf.rule o Line.SynthApp
+         | Syn.DIM_APP _ => Lcf.rule o Path.SynthApp par Lcf.rule o Line.SynthApp
          | Syn.CUST => Lcf.rule o Custom.Synth sign
          | _ => fail @@ E.GENERIC [Fpp.text "Could not find suitable type synthesis rule for", TermPrinter.ppTerm m]
 
@@ -773,7 +773,7 @@ struct
         case (Syn.out u, canonicity sign u) of
            (_, Machine.REDEX) => Lcf.rule o Computation.SequentReduce sign [O.IN_CONCL]
          | (_, Machine.CANONICAL) => Lcf.rule o Universe.SubUniverse
-         | (Syn.PATH_APP (_, r), _) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "SubUniverse with (@ p r)"
+         | (Syn.DIM_APP (_, r), _) => fail @@ E.UNIMPLEMENTED @@ Fpp.text "SubUniverse with (@ p r)"
          | (_, Machine.NEUTRAL blocker) => StepSubUniverseNeuExpand sign u blocker
          | _ => fail @@ E.NOT_APPLICABLE (Fpp.text "StepSubUniverse", TermPrinter.ppTerm u)
 
diff --git a/src/redprl/refiner_types.fun b/src/redprl/refiner_types.fun
index a31db8ea9..63a5d8d81 100644
--- a/src/redprl/refiner_types.fun
+++ b/src/redprl/refiner_types.fun
@@ -1231,8 +1231,8 @@ struct
         val H >> AJ.EQ ((abs0, abs1), (ty, l, k)) = jdg
         val Syn.LINE_TY (u, au) = Syn.out ty
         val ka = kindConstraintOnBase k
-        val Syn.PATH_ABS (v, m0v) = Syn.out abs0
-        val Syn.PATH_ABS (w, m1w) = Syn.out abs1
+        val Syn.ABS (v, m0v) = Syn.out abs0
+        val Syn.ABS (w, m1w) = Syn.out abs1
 
         val z = alpha 0
         val az = substVar (VarKit.toDim z, u) au
@@ -1256,7 +1256,7 @@ struct
         val av = substVar (VarKit.toDim v, u) au
         val (mainGoal, mhole) = makeTrue (H @> (v, AJ.TERM O.DIM)) (av, l, ka)
 
-        val abstr = Syn.into @@ Syn.PATH_ABS (v, mhole)
+        val abstr = Syn.into @@ Syn.ABS (v, mhole)
       in
         |>: mainGoal #> (H, abstr)
       end
@@ -1267,7 +1267,7 @@ struct
         val H >> AJ.EQ ((m, n), (pathTy, l, k)) = jdg
         val Syn.LINE_TY (u, _) = Syn.out pathTy
 
-        val m' = Syn.into @@ Syn.PATH_ABS (u, Syn.into @@ Syn.PATH_APP (m, VarKit.toDim u))
+        val m' = Syn.into @@ Syn.ABS (u, Syn.into @@ Syn.DIM_APP (m, VarKit.toDim u))
         val goal1 = makeMem H (m, (pathTy, l, k))
         val goal2 = makeEqIfDifferent H ((m', n), (pathTy, NONE, K.top)) (* m' will-typed *)
       in
@@ -1289,7 +1289,7 @@ struct
         val ar = substVar (dimHole, u) a
 
         val w = Sym.named "w"
-        val pathApp = substVar (dimHole, w) @@ Syn.into @@ Syn.PATH_APP (VarKit.toExp z, VarKit.toDim w)
+        val pathApp = substVar (dimHole, w) @@ Syn.into @@ Syn.DIM_APP (VarKit.toExp z, VarKit.toDim w)
 
         val H' = Hyps.interposeAfter
           (z, |@> (x, AJ.TRUE (ar, l', K.top))
@@ -1306,8 +1306,8 @@ struct
       let
         val _ = RedPrlLog.trace "Line.EqApp"
         val H >> AJ.EQ ((ap0, ap1), (ty, l, k)) = jdg
-        val Syn.PATH_APP (m0, r0) = Syn.out ap0
-        val Syn.PATH_APP (m1, r1) = Syn.out ap1
+        val Syn.DIM_APP (m0, r0) = Syn.out ap0
+        val Syn.DIM_APP (m1, r1) = Syn.out ap1
         val () = Assert.alphaEq (r0, r1)
 
         val (goalSynth, holeSynth) = makeSynth H (m0, NONE, K.top)
@@ -1322,7 +1322,7 @@ struct
       let
         val _ = RedPrlLog.trace "Line.SynthApp"
         val H >> AJ.SYNTH (tm, l, k) = jdg
-        val Syn.PATH_APP (m, r) = Syn.out tm
+        val Syn.DIM_APP (m, r) = Syn.out tm
         val (goalPathTy, holePathTy) = makeSynth H (m, NONE, K.top)
         val (goalLine, holeLine) = makeMatch (O.LINE_TY, 0, holePathTy, [r])
         val goalKind = makeTypeUnlessSubUniv H (holeLine, l, k) (NONE, K.top)
@@ -1368,8 +1368,8 @@ struct
         val H >> AJ.EQ ((abs0, abs1), (ty, l, k)) = jdg
         val Syn.PATH_TY ((u, au), p0, p1) = Syn.out ty
         val ka = kindConstraintOnBase k
-        val Syn.PATH_ABS (v, m0v) = Syn.out abs0
-        val Syn.PATH_ABS (w, m1w) = Syn.out abs1
+        val Syn.ABS (v, m0v) = Syn.out abs0
+        val Syn.ABS (w, m1w) = Syn.out abs1
 
         val z = alpha 0
         val az = substVar (VarKit.toDim z, u) au
@@ -1407,7 +1407,7 @@ struct
         val goalCoh0 = makeEqIfDifferent H ((m0, p0), (a0, NONE, K.top))
         val goalCoh1 = makeEqIfDifferent H ((m1, p1), (a1, NONE, K.top))
 
-        val abstr = Syn.into @@ Syn.PATH_ABS (v, mhole)
+        val abstr = Syn.into @@ Syn.ABS (v, mhole)
       in
         |>: mainGoal >:? goalCoh0 >:? goalCoh1 #> (H, abstr)
       end
@@ -1418,7 +1418,7 @@ struct
         val H >> AJ.EQ ((m, n), (pathTy, l, k)) = jdg
         val Syn.PATH_TY ((u, _), _, _) = Syn.out pathTy
 
-        val m' = Syn.into @@ Syn.PATH_ABS (u, Syn.into @@ Syn.PATH_APP (m, VarKit.toDim u))
+        val m' = Syn.into @@ Syn.ABS (u, Syn.into @@ Syn.DIM_APP (m, VarKit.toDim u))
         val goal1 = makeMem H (m, (pathTy, l, k))
         val goal2 = makeEqIfDifferent H ((m', n), (pathTy, NONE, K.top)) (* m' will-typed *)
       in
@@ -1441,7 +1441,7 @@ struct
 
 
         val w = Sym.named "w"
-        val pathApp = substVar (dimHole, w) @@ Syn.into @@ Syn.PATH_APP (VarKit.toExp z, VarKit.toDim w)
+        val pathApp = substVar (dimHole, w) @@ Syn.into @@ Syn.DIM_APP (VarKit.toExp z, VarKit.toDim w)
 
         val H' = Hyps.interposeAfter
           (z, |@> (x, AJ.TRUE (ar, l', K.top))
@@ -1458,8 +1458,8 @@ struct
       let
         val _ = RedPrlLog.trace "Path.EqApp"
         val H >> AJ.EQ ((ap0, ap1), (ty, l, k)) = jdg
-        val Syn.PATH_APP (m0, r0) = Syn.out ap0
-        val Syn.PATH_APP (m1, r1) = Syn.out ap1
+        val Syn.DIM_APP (m0, r0) = Syn.out ap0
+        val Syn.DIM_APP (m1, r1) = Syn.out ap1
         val () = Assert.alphaEq (r0, r1)
 
         val (goalSynth, holeSynth) = makeSynth H (m0, NONE, K.top)
@@ -1474,7 +1474,7 @@ struct
       let
         val _ = RedPrlLog.trace "Path.SynthApp"
         val H >> AJ.SYNTH (tm, l, k) = jdg
-        val Syn.PATH_APP (m, r) = Syn.out tm
+        val Syn.DIM_APP (m, r) = Syn.out tm
         val (goalPathTy, holePathTy) = makeSynth H (m, NONE, K.top)
         val (goalLine, holeLine) = makeMatch (O.PATH_TY, 0, holePathTy, [r])
         val goalKind = makeTypeUnlessSubUniv H (holeLine, l, k) (NONE, K.top)
@@ -1486,7 +1486,7 @@ struct
       let
         val _ = RedPrlLog.trace "Path.EqAppConst"
         val H >> AJ.EQ ((ap, p), (a, l, k)) = jdg
-        val Syn.PATH_APP (m, r) = Syn.out ap
+        val Syn.DIM_APP (m, r) = Syn.out ap
 
         val dimAddr = case Syn.out r of Syn.DIM0 => 1 | Syn.DIM1 => 2
 
diff --git a/src/redprl/syntax.sml b/src/redprl/syntax.sml
index 8b29124f0..a8d143228 100644
--- a/src/redprl/syntax.sml
+++ b/src/redprl/syntax.sml
@@ -57,7 +57,7 @@ struct
    | RECORD of ((string * variable) * 'a) list
    | TUPLE of (label * 'a) list | PROJ of string * 'a | TUPLE_UPDATE of (string * 'a) * 'a
    (* path: path abstraction and path application *)
-   | PATH_TY of (variable * 'a) * 'a * 'a | PATH_ABS of variable * 'a | PATH_APP of 'a * 'a
+   | PATH_TY of (variable * 'a) * 'a * 'a | ABS of variable * 'a | DIM_APP of 'a * 'a
    | LINE_TY of variable * 'a
    (* equality *)
    | EQUALITY of 'a * 'a * 'a
@@ -334,8 +334,8 @@ struct
 
        | PATH_TY ((u, a), m, n) => O.PATH_TY $$ [[u] \ a, [] \ m, [] \ n]
        | LINE_TY (u, a) => O.LINE_TY $$ [[u] \ a]
-       | PATH_ABS (u, m) => O.PATH_ABS $$ [[u] \ m]
-       | PATH_APP (m, r) => O.PATH_APP $$ [[] \ m, [] \ r]
+       | ABS (u, m) => O.ABS $$ [[u] \ m]
+       | DIM_APP (m, r) => O.DIM_APP $$ [[] \ m, [] \ r]
 
        | EQUALITY (a, m, n) => O.EQUALITY $$ [[] \ a, [] \ m, [] \ n]
 
@@ -438,8 +438,8 @@ struct
 
        | O.PATH_TY $ [[u] \ a, _ \ m, _ \ n] => PATH_TY ((u, a), m, n)
        | O.LINE_TY $ [[u] \ a] => LINE_TY (u, a)
-       | O.PATH_ABS $ [[u] \ m] => PATH_ABS (u, m)
-       | O.PATH_APP $ [_ \ m, _ \ r] => PATH_APP (m, r)
+       | O.ABS $ [[u] \ m] => ABS (u, m)
+       | O.DIM_APP $ [_ \ m, _ \ r] => DIM_APP (m, r)
 
        | O.EQUALITY $ [_ \ a, _ \ m, _ \ n] => EQUALITY (a, m, n)
 

From 2e0e13b231df5c38f4019799c7f87d0827d0537a Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 15:13:45 -0500
Subject: [PATCH 02/11] Implement the Immortal notation. Needs testing.

---
 src/redprl/redprl.grm | 59 ++++++++++++++++++++++++++++++-------------
 1 file changed, 42 insertions(+), 17 deletions(-)

diff --git a/src/redprl/redprl.grm b/src/redprl/redprl.grm
index 4137429a9..12fc5fc09 100644
--- a/src/redprl/redprl.grm
+++ b/src/redprl/redprl.grm
@@ -95,14 +95,23 @@ struct
     | EQUAL => O.ZERO $$ []
     | LESS => O.NEGSUCC $$ [[] \ makeNum ((~ i) - 1)]
 
-  fun flatten xsys =
-    List.concat (List.map (fn (xs, y) => List.map (fn x => (x, y)) xs) xsys)
+  datatype ('a, 'b) binder = DIM of 'a | TERM of ('a * 'b)
 
-  fun makeQuant opr [] cod = cod
-    | makeQuant opr ((x, a) :: doms) cod =
-       opr $$ [[] \ a, [Option.getOpt (x, "_")] \ makeQuant opr doms cod]
+  fun flatten (quant : ('a list,'b) binder list) : ('a,'b) binder list =
+    let
+      fun expand (DIM vars) = List.map DIM vars
+        | expand (TERM (vars, term)) = List.map (fn var => TERM (var, term)) vars
+    in
+      List.concat (List.map expand quant)
+    end
+
+  fun makeFunOrLineAux [] cod = cod
+    | makeFunOrLineAux (TERM (x, a) :: doms) cod =
+       O.FUN $$ [[] \ a, [Option.getOpt (x, "_")] \ makeFunOrLineAux doms cod]
+    | makeFunOrLineAux (DIM x :: doms) cod =
+       O.LINE_TY $$ [[Option.getOpt (x, "_")] \ makeFunOrLineAux doms cod]
 
-  val makeFun = makeQuant O.FUN o flatten
+  val makeFunOrLine = makeFunOrLineAux o flatten
 
   structure LabelSet = SplaySet (structure Elem = StringOrdered)
 
@@ -121,7 +130,11 @@ struct
 
   fun makeRecordAux pos tbs =
     let
-      val fields = ListUtil.mapWithIndex (fn (_, (SOME x, ty)) => (x, ty) | (i, (NONE, ty)) => (O.indexToLabel i, ty)) (flatten tbs)
+      val fields = ListUtil.mapWithIndex
+        (fn (_, TERM (SOME x, ty)) => (x, ty)
+          | (i, TERM (NONE, ty)) => (O.indexToLabel i, ty)
+          | (_, DIM _) => E.raiseAnnotatedError (pos, E.GENERIC [Fpp.text "No dimension binders in record types."]))
+        (flatten tbs)
       val init = {labels = [], args = []}
       val {labels, args} =
         List.foldl
@@ -139,7 +152,7 @@ struct
 
   fun makeProd pos (tbs, ty) =
     let
-      val (_, args) = makeRecordAux pos (tbs @ [([NONE], ty)])
+      val (_, args) = makeRecordAux pos (tbs @ [TERM ([NONE], ty)])
       val lbls = ListUtil.mapWithIndex (O.indexToLabel o #1) args
     in
       O.RECORD lbls $$ args
@@ -385,9 +398,11 @@ end
  | customOpTerm of string * ast abs list
 
 
- | typedBinder of string option list * ast
- | typedBinders of (string option list * ast) list
- | quantifierData of (string option list * ast) list * ast
+ | typedBinder of (string option list, ast) Multi.binder
+ | typedBinders of (string option list, ast) Multi.binder list
+ | dimBinder of (string option list, ast) Multi.binder
+ | arrowQuantifierData of (string option list, ast) Multi.binder list * ast
+ | timesQuantifierData of (string option list, ast) Multi.binder list * ast
  | field of string * ast
  | fields of (string * ast) list
 
@@ -554,15 +569,25 @@ metavar
   : HASH ident (ident)
 
 typedBinder
-  : LSQUARE boundVars COLON term RSQUARE ((boundVars, term))
+  : LSQUARE boundVars COLON term RSQUARE (Multi.TERM (boundVars, term))
 
 typedBinders
   : typedBinder ([typedBinder])
   | typedBinder typedBinders (typedBinder :: typedBinders)
 
-quantifierData
-  : typedBinder quantifierData ((typedBinder :: #1 quantifierData), #2 quantifierData)
-  | term quantifierData ((([NONE], term) :: #1 quantifierData), #2 quantifierData)
+dimBinder
+  : LSQUARE boundVars COLON DIM RSQUARE (Multi.DIM boundVars)
+
+arrowQuantifierData
+  : typedBinder arrowQuantifierData ((typedBinder :: #1 arrowQuantifierData), #2 arrowQuantifierData)
+  | dimBinder arrowQuantifierData ((dimBinder :: #1 arrowQuantifierData), #2 arrowQuantifierData)
+  | term arrowQuantifierData ((Multi.TERM ([NONE], term) :: #1 arrowQuantifierData), #2 arrowQuantifierData)
+  | DIM arrowQuantifierData ((Multi.DIM [NONE] :: #1 arrowQuantifierData), #2 arrowQuantifierData)
+  | term ([], term)
+
+timesQuantifierData
+  : typedBinder timesQuantifierData ((typedBinder :: #1 timesQuantifierData), #2 timesQuantifierData)
+  | term timesQuantifierData ((Multi.TERM ([NONE], term) :: #1 timesQuantifierData), #2 timesQuantifierData)
   | term ([], term)
 
 field
@@ -690,12 +715,12 @@ rawTermAndTac
   | NUMERAL (Multi.makeNum NUMERAL)
 
   (* function types *)
-  | LPAREN RIGHT_ARROW quantifierData RPAREN (Multi.makeFun (#1 quantifierData) (#2 quantifierData))
+  | LPAREN RIGHT_ARROW arrowQuantifierData RPAREN (Multi.makeFunOrLine (#1 arrowQuantifierData) (#2 arrowQuantifierData))
   | LPAREN LAMBDA LSQUARE boundVars RSQUARE term RPAREN (Multi.makeLam boundVars term)
   | LPAREN DOLLAR_SIGN term terms RPAREN (Multi.makeApp term terms)
 
   (* pair types *)
-  | LPAREN TIMES quantifierData RPAREN (Multi.makeProd (Pos.pos (LPAREN1left fileName) (RPAREN1right fileName)) quantifierData)
+  | LPAREN TIMES timesQuantifierData RPAREN (Multi.makeProd (Pos.pos (LPAREN1left fileName) (RPAREN1right fileName)) timesQuantifierData)
 
   (* dependent record types *)
   | RECORD (Multi.makeRecord (Pos.pos (RECORD1left fileName) (RECORD1right fileName)) [])

From 4d46372626fc0eef507a7850652db17b3f4aaa0d Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 18:11:37 -0500
Subject: [PATCH 03/11] Printing of line and function types.

---
 src/redprl/pretty.sml | 49 ++++++++++++++++++++++++++-----------------
 1 file changed, 30 insertions(+), 19 deletions(-)

diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index ccbb24c7e..3245d8b6e 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -97,18 +97,27 @@ struct
 
   (* This is still quite rudimentary; we can learn to more interesting things like alignment, etc. *)
 
-  fun multiFun (doms : (variable list option * abt) list) m =
+  datatype ('a, 'b) binder = DIM of 'a | TERM of ('a * 'b)
+
+  fun multiFunOrLine (doms : (variable list option, abt) binder list) m =
     case Abt.out m of
        O.FUN $ [_ \ a, [x] \ bx] =>
          if Abt.Var.Ctx.member (Abt.varctx bx) x then
            case doms of
-              (SOME xs, a') :: doms' =>
+              TERM (SOME xs, a') :: doms' =>
                 if Abt.eq (a, a') then
-                  multiFun ((SOME (xs @ [x]), a) :: doms') bx
+                  multiFunOrLine (TERM (SOME (xs @ [x]), a) :: doms') bx
                 else
-                  multiFun ((SOME [x], a) :: doms) bx
-            | _ => multiFun ((SOME [x], a) :: doms) bx
-         else multiFun ((NONE, a) :: doms) bx
+                  multiFunOrLine (TERM (SOME [x], a) :: doms) bx
+            | _ => multiFunOrLine (TERM (SOME [x], a) :: doms) bx
+         else multiFunOrLine (TERM (NONE, a) :: doms) bx
+     | O.LINE_TY $ [[x] \ ax] =>
+         if Abt.Var.Ctx.member (Abt.varctx ax) x then
+           case doms of
+              DIM (SOME xs) :: doms' =>
+                multiFunOrLine (DIM (SOME (xs @ [x])) :: doms') ax
+            | _ => multiFunOrLine (DIM (SOME [x]) :: doms) ax
+         else multiFunOrLine (DIM NONE :: doms) ax
      | _ => (List.rev doms, m)
 
   fun multiLam (xs : variable list) m =
@@ -123,24 +132,26 @@ struct
          multiApp m (n :: ns)
      | _ => (m, ns)
 
-  fun multiPathAbs (us : variable list) m =
+  fun multiAbs (us : variable list) m =
     case Abt.out m of
        O.ABS $ [[u] \ mu] =>
-         multiPathAbs (u :: us) mu
+         multiAbs (u :: us) mu
      | _ => (List.rev us, m)
 
-  fun multiPathApp m (rs : abt list) =
+  fun multiDimApp m (rs : abt list) =
     case Abt.out m of
        O.DIM_APP $ [_ \ m, _ \ r] =>
-         multiPathApp m (r :: rs)
+         multiDimApp m (r :: rs)
      | _ => (m, rs)
 
-  fun printQuant opr (doms, cod) =
+  fun printFunOrLine (doms, cod) =
     Atomic.parens @@ expr @@ hvsep @@
-      (text opr)
+      (text "->")
         :: List.map
-            (fn (SOME xs, a) => Atomic.squares @@ hsep @@ List.map ppVar xs @ [char #":", ppTerm a]
-              | (NONE, a) => ppTerm a)
+            (fn TERM (SOME xs, a) => Atomic.squares @@ hsep @@ List.map ppVar xs @ [char #":", ppTerm a]
+              | TERM (NONE, a) => ppTerm a
+              | DIM (SOME xs) => Atomic.squares @@ hsep @@ List.map ppVar xs @ [char #":", text "dim"]
+              | DIM NONE => text "dim")
             doms
           @ [ppTerm cod]
 
@@ -152,11 +163,11 @@ struct
     Atomic.parens @@ expr @@ hvsep
       (char #"$" :: ppTerm m :: List.map ppTerm ns)
 
-  and printPathAbs (us, m) =
+  and printAbs (us, m) =
     Atomic.parens @@ expr @@ hvsep @@
       [hvsep [text "abs", symBinding us], align @@ ppTerm m]
 
-  and printPathApp (m, rs) =
+  and printDimApp (m, rs) =
     Atomic.parens @@ expr @@ hvsep
       (char #"@" :: ppTerm m :: List.map ppTerm rs)
 
@@ -187,7 +198,7 @@ struct
      | O.LOOP $ [_ \ r] =>
          Atomic.parens @@ expr @@ hvsep @@ [text "loop", ppTerm r]
      | O.FUN $ _ =>
-         printQuant "->" @@ multiFun [] m
+         printFunOrLine @@ multiFunOrLine [] m
      | O.LAM $ _ =>
          printLam @@ multiLam [] m
      | O.APP $ _ =>
@@ -223,9 +234,9 @@ struct
      | O.PROJ lbl $ [m] =>
          Atomic.parens @@ expr @@ hvsep [char #"!", ppLabel lbl, ppBinder m]
      | O.ABS $ _ =>
-         printPathAbs @@ multiPathAbs [] m
+         printAbs @@ multiAbs [] m
      | O.DIM_APP $ _ =>
-         printPathApp @@ multiPathApp m []
+         printDimApp @@ multiDimApp m []
      | O.EQUALITY $ args =>
          Atomic.parens @@ expr @@ hvsep @@
            char #"=" :: List.map ppBinder args

From 578d12af6bb72325bd5b7554b6e6748e2719c859 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 18:21:32 -0500
Subject: [PATCH 04/11] Fix the printing of fcom, hcom, coe, com, box and cap.

---
 src/redprl/pretty.sml | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index 3245d8b6e..d33127761 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -171,28 +171,28 @@ struct
     Atomic.parens @@ expr @@ hvsep
       (char #"@" :: ppTerm m :: List.map ppTerm rs)
 
-  and ppComHead name (r, r') =
-    seq [text name, Atomic.braces @@ seq [ppTerm r, text "~>", ppTerm r']]
+  and ppDir (r, r') = seq [ppTerm r, text "~>", ppTerm r']
 
-  and ppComHeadBackward name (r, r') =
-    seq [text name, Atomic.braces @@ seq [ppTerm r, text "<~", ppTerm r']]
+  and ppBackwardDir (r, r') = seq [ppTerm r, text "<~", ppTerm r']
 
   and ppTerm m =
     case Abt.out m of
        `x => ppVar x
      | O.FCOM $ [_ \ r1, _ \ r2, _ \ cap, _ \ system] =>
          Atomic.parens @@ expr @@ hvsep @@
-           hvsep [ppComHead "fcom" (r1, r2), ppTerm cap]
+           hvsep [text "fcom", ppDir (r1, r2), ppTerm cap]
              :: [ppVector system]
 
      | O.HCOM $ [_ \ r1, _ \ r2, _ \ ty, _ \ cap, _ \ system] =>
          Atomic.parens @@ expr @@ hvsep @@
-           hvsep [ppComHead "hcom" (r1, r2), ppTerm ty, ppTerm cap]
+           hvsep [text "hcom", ppDir (r1, r2), ppTerm ty, ppTerm cap]
              :: [ppVector system]
-
+     | O.COE $ [_ \ r1, _ \ r2, ty, _ \ coercee] =>
+         Atomic.parens @@ expr @@ hvsep @@
+           [text "coe", ppDir (r1, r2), ppBinder ty, ppTerm coercee]
      | O.COM $ [_ \ r1, _ \ r2, ty, _ \ cap, _ \ system] =>
          Atomic.parens @@ expr @@ hvsep @@
-           hvsep [ppComHead "com" (r1, r2), ppBinder ty, ppTerm cap]
+           hvsep [text "com", ppDir (r1, r2), ppBinder ty, ppTerm cap]
              :: [ppVector system]
 
      | O.LOOP $ [_ \ r] =>
@@ -242,8 +242,12 @@ struct
            char #"=" :: List.map ppBinder args
      | O.BOX $ [_ \ r1, _ \ r2, cap, _ \ boundaries] =>
          Atomic.parens @@ expr @@ hvsep @@
-           hvsep [ppComHead "box" (r1, r2), ppBinder cap]
+           hvsep [text "box", ppDir (r1, r2), ppBinder cap]
              :: [ppVector boundaries]
+     | O.CAP $ [_ \ r1, _ \ r2, coercee, _ \ tubes] =>
+         Atomic.parens @@ expr @@ hvsep @@
+           hvsep [text "cap", ppBackwardDir (r1, r2), ppBinder coercee]
+             :: [ppVector tubes]
      | O.V $ args =>
          Atomic.parens @@ expr @@ hvsep @@ text "V" :: List.map ppBinder args
      | O.VIN $ args =>
@@ -253,6 +257,8 @@ struct
      | O.UNIVERSE $ [_ \ l, _ \ k] =>
          Atomic.parens @@ expr @@ hvsep @@ [text "U", ppTerm l, ppTerm k]
 
+     | O.DIM0 $ _ => char #"0"
+     | O.DIM1 $ _ => char #"1"
      | O.MK_TUBE $ [_ \ r1, _ \ r2, [u] \ mu]  => 
        Atomic.squares @@ hsep
          [seq [ppTerm r1, Atomic.equals, ppTerm r2],

From fce66dbcd2879771531de0e55b4ce51d4923697a Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 18:23:42 -0500
Subject: [PATCH 05/11] Add the printing of ghcom and gcom.

---
 src/redprl/pretty.sml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index d33127761..3edd49fb9 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -187,6 +187,10 @@ struct
          Atomic.parens @@ expr @@ hvsep @@
            hvsep [text "hcom", ppDir (r1, r2), ppTerm ty, ppTerm cap]
              :: [ppVector system]
+     | O.GHCOM $ [_ \ r1, _ \ r2, _ \ ty, _ \ cap, _ \ system] =>
+         Atomic.parens @@ expr @@ hvsep @@
+           hvsep [text "ghcom", ppDir (r1, r2), ppTerm ty, ppTerm cap]
+             :: [ppVector system]
      | O.COE $ [_ \ r1, _ \ r2, ty, _ \ coercee] =>
          Atomic.parens @@ expr @@ hvsep @@
            [text "coe", ppDir (r1, r2), ppBinder ty, ppTerm coercee]
@@ -194,6 +198,10 @@ struct
          Atomic.parens @@ expr @@ hvsep @@
            hvsep [text "com", ppDir (r1, r2), ppBinder ty, ppTerm cap]
              :: [ppVector system]
+     | O.GCOM $ [_ \ r1, _ \ r2, ty, _ \ cap, _ \ system] =>
+         Atomic.parens @@ expr @@ hvsep @@
+           hvsep [text "gcom", ppDir (r1, r2), ppBinder ty, ppTerm cap]
+             :: [ppVector system]
 
      | O.LOOP $ [_ \ r] =>
          Atomic.parens @@ expr @@ hvsep @@ [text "loop", ppTerm r]

From 63c0e986e8d515694a206401dd21df43f0a2fe74 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 18:29:02 -0500
Subject: [PATCH 06/11] No more braces for dim binders.

---
 src/redprl/pretty.sml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index 3edd49fb9..b61a839f7 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -165,7 +165,7 @@ struct
 
   and printAbs (us, m) =
     Atomic.parens @@ expr @@ hvsep @@
-      [hvsep [text "abs", symBinding us], align @@ ppTerm m]
+      [hvsep [text "abs", varBinding us], align @@ ppTerm m]
 
   and printDimApp (m, rs) =
     Atomic.parens @@ expr @@ hvsep
@@ -267,10 +267,10 @@ struct
 
      | O.DIM0 $ _ => char #"0"
      | O.DIM1 $ _ => char #"1"
-     | O.MK_TUBE $ [_ \ r1, _ \ r2, [u] \ mu]  => 
+     | O.MK_TUBE $ [_ \ r1, _ \ r2, tube]  =>
        Atomic.squares @@ hsep
          [seq [ppTerm r1, Atomic.equals, ppTerm r2],
-          nest 1 @@ hvsep [Atomic.braces @@ ppVar u, ppTerm mu]]
+          nest 1 @@ ppBinder tube]
      | O.MK_BDRY $ [_ \ r1, _ \ r2, _ \ m] =>
        Atomic.squares @@ hsep
          [seq [ppTerm r1, Atomic.equals, ppTerm r2],
@@ -301,11 +301,6 @@ struct
         [] => atLevel 10 @@ ppTerm m
       | _ => grouped @@ hvsep [varBinding xs, align @@ ppTerm m]
 
-  and symBinding us =
-    unlessEmpty us @@
-      Atomic.braces @@
-        hsep @@ List.map ppVar us
-
   and varBinding xs =
     unlessEmpty xs @@
       Atomic.squares @@

From 8b20e9806a903c106653aef91e7a4a6cbb1190eb Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 22:32:24 -0500
Subject: [PATCH 07/11] Add missing rules of line types.

---
 src/redprl/refiner.fun | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index 08b4e28fb..3be9b91bc 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -519,6 +519,7 @@ struct
          | (Syn.FUN _, Syn.FUN _) => Lcf.rule o Fun.EqType
          | (Syn.RECORD _, Syn.RECORD _) => Lcf.rule o Record.EqType
          | (Syn.PATH_TY _, Syn.PATH_TY _) => Lcf.rule o Path.EqType
+         | (Syn.LINE_TY _, Syn.LINE_TY _) => Lcf.rule o Line.EqType
          | (Syn.EQUALITY _, Syn.EQUALITY _) => Lcf.rule o InternalizedEquality.EqType
          | (Syn.FCOM _, Syn.FCOM _) => Lcf.rule o FormalComposition.EqType
          | (Syn.V _, Syn.V _) => Lcf.rule o V.EqType
@@ -608,6 +609,7 @@ struct
          | (_, _, Syn.FUN _) => Lcf.rule o Fun.Eq
          | (_, _, Syn.RECORD _) => Lcf.rule o Record.Eq
          | (_, _, Syn.PATH_TY _) => Lcf.rule o Path.Eq
+         | (_, _, Syn.LINE_TY _) => Lcf.rule o Line.Eq
          | (_, _, Syn.EQUALITY _) => Lcf.rule o InternalizedEquality.Eq
          | (_, _, Syn.FCOM _) => Lcf.rule o FormalComposition.Eq
          | (_, _, Syn.V _) => Lcf.rule o V.Eq

From 95845b6be3b1716187afc0d6c61927b73cdaf682 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 22:48:21 -0500
Subject: [PATCH 08/11] Goodbye, TY.

---
 src/redprl/machine.fun           | 12 +++++-----
 src/redprl/operator.sml          | 12 +++++-----
 src/redprl/pretty.sml            |  2 +-
 src/redprl/redprl.grm            |  6 ++---
 src/redprl/refiner.fun           | 16 ++++++-------
 src/redprl/refiner_types.fun     | 40 ++++++++++++++++----------------
 src/redprl/syntax.sml            | 12 +++++-----
 src/redprl/tactic_elaborator.fun |  4 ++--
 8 files changed, 52 insertions(+), 52 deletions(-)

diff --git a/src/redprl/machine.fun b/src/redprl/machine.fun
index 53fb5277a..c608f4493 100644
--- a/src/redprl/machine.fun
+++ b/src/redprl/machine.fun
@@ -546,13 +546,13 @@ struct
        end
 
      | O.ABS $ _ || (_, []) => raise Final
-     | O.PATH_TY $ _ || (_, []) => raise Final
-     | O.LINE_TY $ _ || (_, []) => raise Final
+     | O.PATH $ _ || (_, []) => raise Final
+     | O.LINE $ _ || (_, []) => raise Final
 
      | O.DIM_APP $ [_ \ m, _ \ r] || (syms, stk) => COMPAT @@ m || (syms, DIM_APP (HOLE, r) :: stk)
      | O.ABS $ [[x] \ m] || (syms, DIM_APP (HOLE, r) :: stk) => CRITICAL @@ substVar (r, x) m || (syms, stk)
 
-     | O.PATH_TY $ [[u] \ tyu, _ \ m0, _ \ m1] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
+     | O.PATH $ [[u] \ tyu, _ \ m0, _ \ m1] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
        let
          fun apu m = Syn.into @@ Syn.DIM_APP (m, check (`u, O.DIM))
          val v = Sym.named "_"
@@ -566,7 +566,7 @@ struct
        in
          CRITICAL @@ abs || (syms, stk)
        end
-     | O.PATH_TY $ [[u] \ tyuv, _ \ m0v, _ \ m1v] || (syms, COE (dir, (v, HOLE), coercee) :: stk) =>
+     | O.PATH $ [[u] \ tyuv, _ \ m0v, _ \ m1v] || (syms, COE (dir, (v, HOLE), coercee) :: stk) =>
        let
          val comu =
            Syn.into @@ Syn.COM
@@ -579,7 +579,7 @@ struct
          CRITICAL @@ abs || (SymSet.remove syms v, stk)
        end
 
-     | O.LINE_TY $ [[u] \ tyu] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
+     | O.LINE $ [[u] \ tyu] || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) =>
        let
          val utm = VarKit.toDim u
          fun apu n = Syn.into @@ Syn.DIM_APP (n, utm)
@@ -594,7 +594,7 @@ struct
          CRITICAL @@ abs || (syms, stk)
        end
 
-     | O.LINE_TY $ [[u] \ tyuv] || (syms, COE (dir, (v, HOLE), coercee) :: stk) =>
+     | O.LINE $ [[u] \ tyuv] || (syms, COE (dir, (v, HOLE), coercee) :: stk) =>
        let
          val coe = 
            Syn.intoCoe
diff --git a/src/redprl/operator.sml b/src/redprl/operator.sml
index 32f47ef91..5fa7cde3a 100644
--- a/src/redprl/operator.sml
+++ b/src/redprl/operator.sml
@@ -176,9 +176,9 @@ struct
    (* record and tuple *)
    | RECORD of string list | TUPLE of string list | PROJ of string | TUPLE_UPDATE of string
    (* path: path abstraction and application *)
-   | PATH_TY | ABS | DIM_APP
+   | PATH | ABS | DIM_APP
    (* lines: paths without fixed endpoints *)
-   | LINE_TY
+   | LINE
    (* equality *)
    | EQUALITY
    (* universe *)
@@ -320,8 +320,8 @@ struct
      | PROJ lbl => [[] |: EXP] ->> EXP
      | TUPLE_UPDATE lbl => [[] |: EXP, [] |: EXP] ->> EXP
 
-     | PATH_TY => [[DIM] |: EXP, [] |: EXP, [] |: EXP] ->> EXP
-     | LINE_TY => [[DIM] |: EXP] ->> EXP
+     | PATH => [[DIM] |: EXP, [] |: EXP, [] |: EXP] ->> EXP
+     | LINE => [[DIM] |: EXP] ->> EXP
      | ABS => [[DIM] |: EXP] ->> EXP
      | DIM_APP => [[] |: EXP, [] |: DIM] ->> EXP
 
@@ -466,8 +466,8 @@ struct
      | PROJ lbl => "proj{" ^ lbl ^ "}"
      | TUPLE_UPDATE lbl => "update{" ^ lbl ^ "}"
 
-     | PATH_TY => "path"
-     | LINE_TY => "line"
+     | PATH => "path"
+     | LINE => "line"
      | ABS => "abs"
      | DIM_APP => "path-app"
 
diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index b61a839f7..27d01fd29 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -111,7 +111,7 @@ struct
                   multiFunOrLine (TERM (SOME [x], a) :: doms) bx
             | _ => multiFunOrLine (TERM (SOME [x], a) :: doms) bx
          else multiFunOrLine (TERM (NONE, a) :: doms) bx
-     | O.LINE_TY $ [[x] \ ax] =>
+     | O.LINE $ [[x] \ ax] =>
          if Abt.Var.Ctx.member (Abt.varctx ax) x then
            case doms of
               DIM (SOME xs) :: doms' =>
diff --git a/src/redprl/redprl.grm b/src/redprl/redprl.grm
index 12fc5fc09..b6cb20266 100644
--- a/src/redprl/redprl.grm
+++ b/src/redprl/redprl.grm
@@ -109,7 +109,7 @@ struct
     | makeFunOrLineAux (TERM (x, a) :: doms) cod =
        O.FUN $$ [[] \ a, [Option.getOpt (x, "_")] \ makeFunOrLineAux doms cod]
     | makeFunOrLineAux (DIM x :: doms) cod =
-       O.LINE_TY $$ [[Option.getOpt (x, "_")] \ makeFunOrLineAux doms cod]
+       O.LINE $$ [[Option.getOpt (x, "_")] \ makeFunOrLineAux doms cod]
 
   val makeFunOrLine = makeFunOrLineAux o flatten
 
@@ -649,9 +649,9 @@ regularMultinaryOperator
   (* S1 *)
   | S1_REC (O.S1_REC)
   (* paths *)
-  | PATH (O.PATH_TY)
+  | PATH (O.PATH)
   (* lines *)
-  | LINE (O.LINE_TY)
+  | LINE (O.LINE)
   (* equality *)
   | EQUALS (O.EQUALITY)
 
diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index 3be9b91bc..23151c9c2 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -518,8 +518,8 @@ struct
          | (Syn.S1, Syn.S1) => Lcf.rule o S1.EqType
          | (Syn.FUN _, Syn.FUN _) => Lcf.rule o Fun.EqType
          | (Syn.RECORD _, Syn.RECORD _) => Lcf.rule o Record.EqType
-         | (Syn.PATH_TY _, Syn.PATH_TY _) => Lcf.rule o Path.EqType
-         | (Syn.LINE_TY _, Syn.LINE_TY _) => Lcf.rule o Line.EqType
+         | (Syn.PATH _, Syn.PATH _) => Lcf.rule o Path.EqType
+         | (Syn.LINE _, Syn.LINE _) => Lcf.rule o Line.EqType
          | (Syn.EQUALITY _, Syn.EQUALITY _) => Lcf.rule o InternalizedEquality.EqType
          | (Syn.FCOM _, Syn.FCOM _) => Lcf.rule o FormalComposition.EqType
          | (Syn.V _, Syn.V _) => Lcf.rule o V.EqType
@@ -608,8 +608,8 @@ struct
          | (Syn.FCOM _, Syn.FCOM _, Syn.S1) => Lcf.rule o S1.EqFCom
          | (_, _, Syn.FUN _) => Lcf.rule o Fun.Eq
          | (_, _, Syn.RECORD _) => Lcf.rule o Record.Eq
-         | (_, _, Syn.PATH_TY _) => Lcf.rule o Path.Eq
-         | (_, _, Syn.LINE_TY _) => Lcf.rule o Line.Eq
+         | (_, _, Syn.PATH _) => Lcf.rule o Path.Eq
+         | (_, _, Syn.LINE _) => Lcf.rule o Line.Eq
          | (_, _, Syn.EQUALITY _) => Lcf.rule o InternalizedEquality.Eq
          | (_, _, Syn.FCOM _) => Lcf.rule o FormalComposition.Eq
          | (_, _, Syn.V _) => Lcf.rule o V.Eq
@@ -668,8 +668,8 @@ struct
         (case (blocker, Syn.out ty) of
            (_, Syn.FUN _) => Lcf.rule o Fun.Eta
          | (_, Syn.RECORD _) => Lcf.rule o Record.Eta
-         | (_, Syn.PATH_TY _) => Lcf.rule o Path.Eta
-         | (_, Syn.LINE_TY _) => Lcf.rule o Line.Eta
+         | (_, Syn.PATH _) => Lcf.rule o Path.Eta
+         | (_, Syn.LINE _) => Lcf.rule o Line.Eta
          | (_, Syn.EQUALITY _) => Lcf.rule o InternalizedEquality.Eta
          | (Machine.VAR z, _) => AutoElim sign z
          | (Machine.OPERATOR theta, _) => Lcf.rule o Custom.Unfold sign [theta] [O.IN_CONCL])
@@ -843,8 +843,8 @@ struct
          | Syn.S1 => Lcf.rule o S1.Elim z
          | Syn.FUN _ => Lcf.rule o Fun.Elim z
          | Syn.RECORD _ => Lcf.rule o Record.Elim z
-         | Syn.PATH_TY _ => Lcf.rule o Path.Elim z
-         | Syn.LINE_TY _ => Lcf.rule o Line.Elim z
+         | Syn.PATH _ => Lcf.rule o Path.Elim z
+         | Syn.LINE _ => Lcf.rule o Line.Elim z
          | Syn.EQUALITY _ => Lcf.rule o InternalizedEquality.Elim z
          | Syn.UNIVERSE _ => Universe.Elim z
          | _ => fail @@ E.GENERIC [Fpp.text "elim tactic", TermPrinter.ppTerm ty]
diff --git a/src/redprl/refiner_types.fun b/src/redprl/refiner_types.fun
index 63a5d8d81..292092b07 100644
--- a/src/redprl/refiner_types.fun
+++ b/src/redprl/refiner_types.fun
@@ -1213,8 +1213,8 @@ struct
       let
         val _ = RedPrlLog.trace "Line.EqType"
         val H >> AJ.EQ_TYPE ((ty0, ty1), l, k) = jdg
-        val Syn.LINE_TY (u, a0u) = Syn.out ty0
-        val Syn.LINE_TY (v, a1v) = Syn.out ty1
+        val Syn.LINE (u, a0u) = Syn.out ty0
+        val Syn.LINE (v, a1v) = Syn.out ty1
         val ka = kindConstraintOnBase k
 
         val w = alpha 0
@@ -1229,7 +1229,7 @@ struct
       let
         val _ = RedPrlLog.trace "Line.Eq"
         val H >> AJ.EQ ((abs0, abs1), (ty, l, k)) = jdg
-        val Syn.LINE_TY (u, au) = Syn.out ty
+        val Syn.LINE (u, au) = Syn.out ty
         val ka = kindConstraintOnBase k
         val Syn.ABS (v, m0v) = Syn.out abs0
         val Syn.ABS (w, m1w) = Syn.out abs1
@@ -1247,7 +1247,7 @@ struct
       let
         val _ = RedPrlLog.trace "Line.True"
         val H >> AJ.TRUE (ty, l, k) = jdg
-        val Syn.LINE_TY (u, au) = Syn.out ty
+        val Syn.LINE (u, au) = Syn.out ty
         val ka = kindConstraintOnBase k
         val a0 = substVar (Syn.into Syn.DIM0, u) au
         val a1 = substVar (Syn.into Syn.DIM1, u) au
@@ -1265,7 +1265,7 @@ struct
       let
         val _ = RedPrlLog.trace "Line.Eta"
         val H >> AJ.EQ ((m, n), (pathTy, l, k)) = jdg
-        val Syn.LINE_TY (u, _) = Syn.out pathTy
+        val Syn.LINE (u, _) = Syn.out pathTy
 
         val m' = Syn.into @@ Syn.ABS (u, Syn.into @@ Syn.DIM_APP (m, VarKit.toDim u))
         val goal1 = makeMem H (m, (pathTy, l, k))
@@ -1280,7 +1280,7 @@ struct
         val H >> catjdg = jdg
         (* for now we ignore the kind in the context *)
         val AJ.TRUE (ty, l', _) = Hyps.lookup H z
-        val Syn.LINE_TY (u, a) = Syn.out ty
+        val Syn.LINE (u, a) = Syn.out ty
 
         val x = alpha 0
         val y = alpha 1
@@ -1312,7 +1312,7 @@ struct
 
         val (goalSynth, holeSynth) = makeSynth H (m0, NONE, K.top)
         val goalMem = makeEqIfDifferent H ((m0, m1), (holeSynth, NONE, K.top)) (* m0 well-typed *)
-        val (goalLine, holeLine) = makeMatch (O.LINE_TY, 0, holeSynth, [r0])
+        val (goalLine, holeLine) = makeMatch (O.LINE, 0, holeSynth, [r0])
         val goalTy = makeSubType H (holeLine, NONE, K.top) (ty, l, k) (* holeLine type *)
       in
         |>: goalSynth >:? goalMem >: goalLine >:? goalTy #> (H, trivial)
@@ -1324,7 +1324,7 @@ struct
         val H >> AJ.SYNTH (tm, l, k) = jdg
         val Syn.DIM_APP (m, r) = Syn.out tm
         val (goalPathTy, holePathTy) = makeSynth H (m, NONE, K.top)
-        val (goalLine, holeLine) = makeMatch (O.LINE_TY, 0, holePathTy, [r])
+        val (goalLine, holeLine) = makeMatch (O.LINE, 0, holePathTy, [r])
         val goalKind = makeTypeUnlessSubUniv H (holeLine, l, k) (NONE, K.top)
       in
         |>: goalPathTy >: goalLine >:? goalKind #> (H, holeLine)
@@ -1345,8 +1345,8 @@ struct
       let
         val _ = RedPrlLog.trace "Path.EqType"
         val H >> AJ.EQ_TYPE ((ty0, ty1), l, k) = jdg
-        val Syn.PATH_TY ((u, a0u), m0, n0) = Syn.out ty0
-        val Syn.PATH_TY ((v, a1v), m1, n1) = Syn.out ty1
+        val Syn.PATH ((u, a0u), m0, n0) = Syn.out ty0
+        val Syn.PATH ((v, a1v), m1, n1) = Syn.out ty1
         val ka = kindConstraintOnBase k
 
         val w = alpha 0
@@ -1366,7 +1366,7 @@ struct
       let
         val _ = RedPrlLog.trace "Path.Eq"
         val H >> AJ.EQ ((abs0, abs1), (ty, l, k)) = jdg
-        val Syn.PATH_TY ((u, au), p0, p1) = Syn.out ty
+        val Syn.PATH ((u, au), p0, p1) = Syn.out ty
         val ka = kindConstraintOnBase k
         val Syn.ABS (v, m0v) = Syn.out abs0
         val Syn.ABS (w, m1w) = Syn.out abs1
@@ -1392,7 +1392,7 @@ struct
       let
         val _ = RedPrlLog.trace "Path.True"
         val H >> AJ.TRUE (ty, l, k) = jdg
-        val Syn.PATH_TY ((u, au), p0, p1) = Syn.out ty
+        val Syn.PATH ((u, au), p0, p1) = Syn.out ty
         val ka = kindConstraintOnBase k
         val a0 = substVar (Syn.into Syn.DIM0, u) au
         val a1 = substVar (Syn.into Syn.DIM1, u) au
@@ -1416,7 +1416,7 @@ struct
       let
         val _ = RedPrlLog.trace "Path.Eta"
         val H >> AJ.EQ ((m, n), (pathTy, l, k)) = jdg
-        val Syn.PATH_TY ((u, _), _, _) = Syn.out pathTy
+        val Syn.PATH ((u, _), _, _) = Syn.out pathTy
 
         val m' = Syn.into @@ Syn.ABS (u, Syn.into @@ Syn.DIM_APP (m, VarKit.toDim u))
         val goal1 = makeMem H (m, (pathTy, l, k))
@@ -1431,7 +1431,7 @@ struct
         val H >> catjdg = jdg
         (* for now we ignore the kind in the context *)
         val AJ.TRUE (ty, l', _) = Hyps.lookup H z
-        val Syn.PATH_TY ((u, a), _, _) = Syn.out ty
+        val Syn.PATH ((u, a), _, _) = Syn.out ty
 
         val x = alpha 0
         val y = alpha 1
@@ -1464,7 +1464,7 @@ struct
 
         val (goalSynth, holeSynth) = makeSynth H (m0, NONE, K.top)
         val goalMem = makeEqIfDifferent H ((m0, m1), (holeSynth, NONE, K.top)) (* m0 well-typed *)
-        val (goalLine, holeLine) = makeMatch (O.PATH_TY, 0, holeSynth, [r0])
+        val (goalLine, holeLine) = makeMatch (O.PATH, 0, holeSynth, [r0])
         val goalTy = makeSubType H (holeLine, NONE, K.top) (ty, l, k) (* holeLine type *)
       in
         |>: goalSynth >:? goalMem >: goalLine >:? goalTy #> (H, trivial)
@@ -1476,7 +1476,7 @@ struct
         val H >> AJ.SYNTH (tm, l, k) = jdg
         val Syn.DIM_APP (m, r) = Syn.out tm
         val (goalPathTy, holePathTy) = makeSynth H (m, NONE, K.top)
-        val (goalLine, holeLine) = makeMatch (O.PATH_TY, 0, holePathTy, [r])
+        val (goalLine, holeLine) = makeMatch (O.PATH, 0, holePathTy, [r])
         val goalKind = makeTypeUnlessSubUniv H (holeLine, l, k) (NONE, K.top)
       in
         |>: goalPathTy >: goalLine >:? goalKind #> (H, holeLine)
@@ -1492,8 +1492,8 @@ struct
 
         val (goalSynth, holeSynth) = makeSynth H (m, NONE, K.top)
 
-        val (goalLine, holeLine) = makeMatch (O.PATH_TY, 0, holeSynth, [r])
-        val (goalEndpoint, holeEndpoint) = makeMatch (O.PATH_TY, dimAddr, holeSynth, [])
+        val (goalLine, holeLine) = makeMatch (O.PATH, 0, holeSynth, [r])
+        val (goalEndpoint, holeEndpoint) = makeMatch (O.PATH, dimAddr, holeSynth, [])
         val goalTy = makeSubType H (holeLine, NONE, K.top) (a, NONE, K.top) (* holeLine should be well-typed *)
         val goalEq = makeEq H ((holeEndpoint, p), (a, l, k))
       in
@@ -1896,7 +1896,7 @@ struct
         val dummy = Sym.named "_"
       in
         Syn.into @@ Syn.FUN (C, c',
-          Syn.into @@ Syn.PATH_TY ((dummy, C), VarKit.toExp c', c))
+          Syn.into @@ Syn.PATH ((dummy, C), VarKit.toExp c', c))
       end
 
     fun intoIsContr C =
@@ -1912,7 +1912,7 @@ struct
         val dummy = Sym.named "_"
       in
         Syn.intoProd [(a, A)] @@
-          Syn.into @@ Syn.PATH_TY
+          Syn.into @@ Syn.PATH
             ((dummy, B), Syn.intoApp (f, VarKit.toExp a), b)
       end
 
diff --git a/src/redprl/syntax.sml b/src/redprl/syntax.sml
index a8d143228..989f8170b 100644
--- a/src/redprl/syntax.sml
+++ b/src/redprl/syntax.sml
@@ -57,8 +57,8 @@ struct
    | RECORD of ((string * variable) * 'a) list
    | TUPLE of (label * 'a) list | PROJ of string * 'a | TUPLE_UPDATE of (string * 'a) * 'a
    (* path: path abstraction and path application *)
-   | PATH_TY of (variable * 'a) * 'a * 'a | ABS of variable * 'a | DIM_APP of 'a * 'a
-   | LINE_TY of variable * 'a
+   | PATH of (variable * 'a) * 'a * 'a | ABS of variable * 'a | DIM_APP of 'a * 'a
+   | LINE of variable * 'a
    (* equality *)
    | EQUALITY of 'a * 'a * 'a
    (* fcom types *)
@@ -332,8 +332,8 @@ struct
        | PROJ (lbl, a) => O.PROJ lbl $$ [[] \ a]
        | TUPLE_UPDATE ((lbl, n), m) => O.TUPLE_UPDATE lbl $$ [[] \ n, [] \ m]
 
-       | PATH_TY ((u, a), m, n) => O.PATH_TY $$ [[u] \ a, [] \ m, [] \ n]
-       | LINE_TY (u, a) => O.LINE_TY $$ [[u] \ a]
+       | PATH ((u, a), m, n) => O.PATH $$ [[u] \ a, [] \ m, [] \ n]
+       | LINE (u, a) => O.LINE $$ [[u] \ a]
        | ABS (u, m) => O.ABS $$ [[u] \ m]
        | DIM_APP (m, r) => O.DIM_APP $$ [[] \ m, [] \ r]
 
@@ -436,8 +436,8 @@ struct
        | O.PROJ lbl $ [_ \ m] => PROJ (lbl, m)
        | O.TUPLE_UPDATE lbl $ [_ \ n, _ \ m] => TUPLE_UPDATE ((lbl, n), m)
 
-       | O.PATH_TY $ [[u] \ a, _ \ m, _ \ n] => PATH_TY ((u, a), m, n)
-       | O.LINE_TY $ [[u] \ a] => LINE_TY (u, a)
+       | O.PATH $ [[u] \ a, _ \ m, _ \ n] => PATH ((u, a), m, n)
+       | O.LINE $ [[u] \ a] => LINE (u, a)
        | O.ABS $ [[u] \ m] => ABS (u, m)
        | O.DIM_APP $ [_ \ m, _ \ r] => DIM_APP (m, r)
 
diff --git a/src/redprl/tactic_elaborator.fun b/src/redprl/tactic_elaborator.fun
index bfe3ceb2d..7f0e7969d 100644
--- a/src/redprl/tactic_elaborator.fun
+++ b/src/redprl/tactic_elaborator.fun
@@ -145,8 +145,8 @@ struct
     in
       case Syn.out ty of 
          Syn.FUN _ => (Lcf.rule o RT.Fun.Elim z thenl' (names, [appTac, contTac])) alpha jdg
-       | Syn.PATH_TY _ => (Lcf.rule o RT.Path.Elim z thenl' (names, [appTac, contTac])) alpha jdg
-       | Syn.LINE_TY _ => (Lcf.rule o RT.Line.Elim z thenl' (names, [appTac, contTac])) alpha jdg
+       | Syn.PATH _ => (Lcf.rule o RT.Path.Elim z thenl' (names, [appTac, contTac])) alpha jdg
+       | Syn.LINE _ => (Lcf.rule o RT.Line.Elim z thenl' (names, [appTac, contTac])) alpha jdg
        | _ => raise RedPrlError.error [Fpp.text "'apply' tactical does not apply"]
     end
 

From 3eff92fddab9609caaa7b97fb796f6c85ad0c917 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 23:00:19 -0500
Subject: [PATCH 09/11] Name the low-level rules in Coe.

---
 src/redprl/refiner.fun | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index 23151c9c2..8da2acd7f 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -411,6 +411,8 @@ struct
      | "hcom/eq" => Lcf.rule o HCom.Eq
      | "hcom/eq/cap" => Lcf.rule o HCom.EqCapL
      | "hcom/eq/tube" => Lcf.rule o HCom.EqTubeL
+     | "coe/eq" => Lcf.rule o Coe.Eq
+     | "coe/eq/cap" => Lcf.rule o Coe.EqCapL
 
      | r => raise E.error [Fpp.text "No rule registered with name", Fpp.text r]
 

From 653355abf55ebc2b0909942336b9b2ae4dec2a5e Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 23:02:07 -0500
Subject: [PATCH 10/11] Very basic testing of line types.

---
 test/success/lines.prl | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test/success/lines.prl

diff --git a/test/success/lines.prl b/test/success/lines.prl
new file mode 100644
index 000000000..434e96d1b
--- /dev/null
+++ b/test/success/lines.prl
@@ -0,0 +1,8 @@
+Thm Line/Test0 : [
+  (->
+   [a : (U 0 kan)]
+   [l : (-> dim a)]
+   (= a (coe 0~>1 [_] a (@ l 0)) (@ (coe 0~>1 [_] (-> dim a) l) 0)))
+] by [
+  lam a, l. exact ax; refine eq/eq/ax; reduce; refine coe/eq; [refine line/eq/app; auto]; auto
+].

From 2ffe12b8aeb5a31f7028a134638bbc9f7e9a475e Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 10 Nov 2017 23:19:42 -0500
Subject: [PATCH 11/11] Enable the Immortal printing for line types.

---
 src/redprl/pretty.sml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/redprl/pretty.sml b/src/redprl/pretty.sml
index 27d01fd29..43663ef71 100644
--- a/src/redprl/pretty.sml
+++ b/src/redprl/pretty.sml
@@ -241,6 +241,8 @@ struct
          end
      | O.PROJ lbl $ [m] =>
          Atomic.parens @@ expr @@ hvsep [char #"!", ppLabel lbl, ppBinder m]
+     | O.LINE $ _ =>
+         printFunOrLine @@ multiFunOrLine [] m
      | O.ABS $ _ =>
          printAbs @@ multiAbs [] m
      | O.DIM_APP $ _ =>