Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.

1 files changed, 161 insertions, 243 deletions

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index cf5bb61..a756728 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -1,6 +1,7 @@
 module Obs.NormalForm
 
-import Data.Fin
+import Data.List.Elem
+import Data.So
 
 import Obs.Sort
 import Obs.Substitution
@@ -12,328 +13,245 @@ import Text.PrettyPrint.Prettyprinter
 
 -- Definition ------------------------------------------------------------------
 
-data Constructor : Nat -> Type
-data Neutral     : Nat -> Type
-data NormalForm  : Nat -> Type
+data NormalForm  : Sorted.Family Bool
 
 public export
-data Constructor : Nat -> Type where
-  Sort   : Sort -> Constructor n
-  Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Lambda : String -> NormalForm (S n) -> Constructor n
-  Sigma  : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Pair   : NormalForm n -> NormalForm n -> Constructor n
-  Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
-  Left   : NormalForm n -> Constructor n
-  Right  : NormalForm n -> Constructor n
-  Container : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
-  MkContainer : NormalForm n -> NormalForm n -> NormalForm n -> Constructor n
-  Top    : Constructor n
-  Bottom : Constructor n
+data Constructor : Unsorted.Family Bool where
+  Sort : (s : Sort) -> Constructor ctx
+  Pi : (s, s' : Sort)
+    -> (var : String)
+    -> (a : NormalForm True ctx)
+    -> (b : NormalForm True (isSet s :: ctx))
+    -> Constructor ctx
+  Lambda : (s : Sort)
+    -> (var : String)
+    -> NormalForm True (isSet s :: ctx)
+    -> Constructor ctx
+  Sigma : (s, s' : Sort)
+    -> (var : String)
+    -> (a : NormalForm True ctx)
+    -> (b : NormalForm True (isSet s :: ctx))
+    -> Constructor ctx
+  Pair : (s, s' : Sort)
+    -> (prf : So (isSet (max s s')))
+    -> NormalForm (isSet s) ctx
+    -> NormalForm (isSet s') ctx
+    -> Constructor ctx
+  Bool : Constructor ctx
+  True : Constructor ctx
+  False : Constructor ctx
+  Top : Constructor ctx
+  Bottom : Constructor ctx
 
 public export
-data Neutral : Nat -> Type where
-  Var    : String -> Fin n -> Neutral n
-  App    : Neutral n -> NormalForm n -> Neutral n
-  Fst    : Neutral n -> Neutral n
-  Snd    : Neutral n -> Neutral n
-  Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  Tag    : Neutral n -> Neutral n
-  Position : Neutral n -> Neutral n
-  Next   : Neutral n -> Neutral n
-  Absurd : Neutral n
-  Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
-  EqualR : Nat -> Constructor n -> Neutral n -> Neutral n
-  EqualU : Nat -> Constructor n -> Constructor n -> Neutral n
-  CastL  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  CastR  : Constructor n -> Neutral n -> NormalForm n -> Neutral n
-  CastU  : Constructor n -> Constructor n -> NormalForm n -> Neutral n
+data Neutral : Unsorted.Family Bool where
+  Var : (var : String)
+    -> (sort : Sort)
+    -> (prf : So (isSet sort))
+    -> (i : Elem True ctx)
+    -> Neutral ctx
+  App : (b : Bool) -> Neutral ctx -> NormalForm b ctx -> Neutral ctx
+  Fst : (b : Bool) -> Neutral ctx -> Neutral ctx
+  Snd : (b : Bool) -> Neutral ctx -> Neutral ctx
+  If : Neutral ctx -> (f, g : NormalForm True ctx) -> Neutral ctx
+  Absurd : Neutral ctx
+  Equal : Neutral ctx -> NormalForm True ctx -> NormalForm True ctx -> Neutral ctx
+  EqualL : (a : Neutral ctx) -> (b : NormalForm True ctx) -> Neutral ctx
+  EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
+  EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
+  CastL : (a : Neutral ctx) ->
+    (b : NormalForm True ctx) ->
+    NormalForm True ctx ->
+    Neutral ctx
+  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm True ctx -> Neutral ctx
+  CastStuck : (a, b : Constructor ctx) -> NormalForm True ctx -> Neutral ctx
 
 public export
-data NormalForm : Nat -> Type where
-  Ntrl  : Neutral n -> NormalForm n
-  Cnstr : Constructor n -> NormalForm n
-  Irrel : NormalForm n
+data NormalForm : Sorted.Family Bool where
+  Ntrl : Neutral ~|> NormalForm True
+  Cnstr : Constructor ~|> NormalForm True
+  Irrel : NormalForm False ctx
+
+%name Constructor t, u, v
+%name Neutral t, u, v
+%name NormalForm t, u, v
 
 public export
-record Definition (n : Nat) where
+record Definition (ctx : List Bool) where
   constructor MkDefinition
-  name   : WithBounds String
-  sort   : Sort
-  ty     : NormalForm n
-  tm     : NormalForm n
+  name : WithBounds String
+  sort : Sort
+  ty   : NormalForm True ctx
+  tm   : NormalForm (isSet sort) ctx
 
 public export
-data Context : Nat -> Type where
-  Nil  : Context 0
-  (:<) : Context n -> Definition n -> Context (S n)
-
--- Interfaces ------------------------------------------------------------------
-
--- Naive equality tests
-eqCnstr : Constructor n -> Constructor n -> Bool
-eqNtrl  : Neutral n -> Neutral n -> Bool
-eqWhnf  : NormalForm n -> NormalForm n -> Bool
-
-eqCnstr (Sort s) (Sort s') = s == s'
-eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
-eqCnstr (Sigma s s' _ a b) (Sigma l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
-eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Left t) (Left t') = eqWhnf t t'
-eqCnstr (Right t) (Right t') = eqWhnf t t'
-eqCnstr (Container s a s' s'') (Container l a' l' l'') = s == l && eqWhnf a a' && s' == l' && s'' == l''
-eqCnstr (MkContainer t p f) (MkContainer t' p' f') = eqWhnf t t' && eqWhnf p p' && eqWhnf f f'
-eqCnstr Top Top = True
-eqCnstr Bottom Bottom = True
-eqCnstr _ _ = False
-
-eqNtrl (Var _ i) (Var _ j) = i == j
-eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
-eqNtrl (Fst t) (Fst t') = eqNtrl t t'
-eqNtrl (Snd t) (Snd t') = eqNtrl t t'
-eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
-eqNtrl (Tag t) (Tag t') = eqNtrl t t'
-eqNtrl (Position t) (Position t') = eqNtrl t t'
-eqNtrl (Next t) (Next t') = eqNtrl t t'
-eqNtrl Absurd Absurd = True
-eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
-eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
-eqNtrl (EqualR i t u) (EqualR j t' u') = i == j && eqCnstr t t' && eqNtrl u u'
-eqNtrl (EqualU i t u) (EqualU j t' u') = i == j && eqCnstr t t' && eqCnstr u u'
-eqNtrl (CastL a b t) (CastL a' b' t') = eqNtrl a a' && eqWhnf b b' && eqWhnf t t'
-eqNtrl (CastR a b t) (CastR a' b' t') = eqCnstr a a' && eqNtrl b b' && eqWhnf t t'
-eqNtrl (CastU a b t) (CastU a' b' t') = eqCnstr a a' && eqCnstr b b' && eqWhnf t t'
-eqNtrl _ _ = False
-
-eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
-eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
-eqWhnf Irrel     Irrel     = True
-eqWhnf _ _ = False
-
-export
-Eq (Constructor n) where
-  t == u = eqCnstr t u
+data Context : List Bool -> Type where
+  Nil  : Context []
+  (:<) : Context ctx -> (def : Definition ctx) -> Context (isSet def.sort :: ctx)
 
-export
-Eq (Neutral n) where
-  t == u = eqNtrl t u
+%name Context ctx, ctx', ctx''
 
-export
-Eq (NormalForm n) where
-  t == u = eqWhnf t u
+-- Convenience Casts -----------------------------------------------------------
 
-export
-Cast Sort (Constructor n) where
-  cast = Sort
+public export
+Cast Sort (Constructor ctx) where
+  cast s = Sort s
 
-export
-Cast Sort (NormalForm n) where
-  cast = Cnstr . cast
+public export
+Cast Sort (NormalForm True ctx) where
+  cast s = Cnstr $ cast s
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyPrecCnstr : Prec -> Constructor n -> Doc ann
-prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
-prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
+prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
+prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
 prettyPrecCnstr d (Sort s) = prettyPrec d s
-prettyPrecCnstr d (Pi _ _ var a b) =
+prettyPrecCnstr d (Pi s s' var a b) =
+  let lhs = case var of
+              "" => align (prettyPrec App a)
+              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
+  in
   parenthesise (d > Open) $
   group $
-  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
-  pretty "->" <+> softline <+>
-  prettyPrecWhnf Open b
-prettyPrecCnstr d (Lambda var t) =
+  lhs <++> pretty "->" <+> line <+> align (prettyPrec Open b)
+prettyPrecCnstr d (Lambda _ var t) =
   parenthesise (d > Open) $
   group $
   backslash <+> pretty var <++>
-  pretty "=>" <+> softline <+>
-  prettyPrecWhnf Open t
-prettyPrecCnstr d (Sigma _ _ var a b) =
+  pretty "=>" <+> line <+>
+  align (prettyPrec Open t)
+prettyPrecCnstr d (Sigma s s' var a b) =
+  let lhs = case var of
+              "" => align (prettyPrec App a)
+              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
+  in
   parenthesise (d > Open) $
   group $
-  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
-  pretty "**" <+> softline <+>
-  prettyPrecWhnf Open b
-prettyPrecCnstr d (Pair t u) =
+  lhs <++> pretty "**" <+> line <+> align (prettyPrec Open b)
+prettyPrecCnstr d (Pair s s' prf t u) =
   angles $
   group $
-  neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
-prettyPrecCnstr d (Sum _ _ a b) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Either", prettyPrecWhnf App a, prettyPrecWhnf App b]
-prettyPrecCnstr d (Left t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Left", prettyPrecWhnf App t]
-prettyPrecCnstr d (Right t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Right", prettyPrecWhnf App t]
-prettyPrecCnstr d (Container s a s' s'') =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Container", prettyPrecWhnf App a, prettyPrec App s', prettyPrec App s'']
-prettyPrecCnstr d (MkContainer t p f) =
-  parenthesise (d >= User 0) $
-  group $
-  fillSep
-    [ prettyPrecWhnf (User 0) t <++> pretty "<|"
-    , prettyPrecWhnf (User 0) p <++> pretty "/"
-    , prettyPrecWhnf (User 0) f
-    ]
+  neutral <++> prettyPrec Open t <+> comma <+> line <+> prettyPrec Open u <++> neutral
+prettyPrecCnstr d Bool = pretty "Bool"
+prettyPrecCnstr d True = pretty "True"
+prettyPrecCnstr d False = pretty "False"
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
-prettyPrecNtrl d (Var var i) = pretty "\{show var}@\{show i}"
-prettyPrecNtrl d (App t u) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
-prettyPrecNtrl d (Fst t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "fst", prettyPrecNtrl App t]
-prettyPrecNtrl d (Snd t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "snd", prettyPrecNtrl App t]
-prettyPrecNtrl d (Case t f g) =
+prettyPrecNtrl : Prec -> Neutral ctx -> Doc ann
+prettyPrecNtrl d (Var var sort prf i) = pretty "\{var}@\{show $ elemToNat i}"
+prettyPrecNtrl d (App _ t u) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
-prettyPrecNtrl d (Tag t) =
+  vsep [prettyPrecNtrl Open t, prettyPrec App u]
+prettyPrecNtrl d (Fst _ t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "tag", prettyPrecNtrl App t]
-prettyPrecNtrl d (Position t) =
+  vsep [pretty "fst", prettyPrecNtrl App t]
+prettyPrecNtrl d (Snd _ t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "position", prettyPrecNtrl App t]
-prettyPrecNtrl d (Next t) =
+  vsep [pretty "snd", prettyPrecNtrl App t]
+prettyPrecNtrl d (If t f g) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "next", prettyPrecNtrl App t]
+  vsep [pretty "if", prettyPrecNtrl App t, prettyPrec App f, prettyPrec App g]
 prettyPrecNtrl d Absurd = pretty "absurd"
-prettyPrecNtrl d (Equal _ t u) =
+prettyPrecNtrl d (Equal a t u) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecWhnf Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
-prettyPrecNtrl d (EqualL _ t u) =
+  prettyPrec Equal t <++> pretty "~" <+> line <+> prettyPrec Equal u
+prettyPrecNtrl d (EqualL a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecNtrl Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
-prettyPrecNtrl d (EqualR _ t u) =
+  prettyPrecNtrl Equal a <++> pretty "~" <+> line <+> prettyPrec Equal b
+prettyPrecNtrl d (EqualR a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecNtrl Equal u
-prettyPrecNtrl d (EqualU _ t u) =
+  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecNtrl Equal b
+prettyPrecNtrl d (EqualStuck a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecCnstr Equal u
+  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecCnstr Equal b
 prettyPrecNtrl d (CastL a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecNtrl App a, prettyPrecWhnf App b, prettyPrecWhnf App t]
+  vsep [pretty "cast", prettyPrecNtrl App a, prettyPrec App b, prettyPrec App t]
 prettyPrecNtrl d (CastR a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrecWhnf App t]
-prettyPrecNtrl d (CastU a b t) =
+  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrec App t]
+prettyPrecNtrl d (CastStuck a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrecWhnf App t]
+  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrec App t]
 
-prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
-prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
-prettyPrecWhnf d Irrel     = pretty "_"
+prettyPrec d (Ntrl t) = prettyPrecNtrl d t
+prettyPrec d (Cnstr t) = prettyPrecCnstr d t
+prettyPrec d Irrel = pretty "_"
 
 export
-Pretty (Constructor n) where
+Pretty (Constructor ctx) where
   prettyPrec = prettyPrecCnstr
 
 export
-Pretty (Neutral n) where
+Pretty (Neutral ctx) where
   prettyPrec = prettyPrecNtrl
 
 export
-Pretty (NormalForm n) where
-  prettyPrec = prettyPrecWhnf
+Pretty (NormalForm b ctx) where
+  prettyPrec = NormalForm.prettyPrec
 
-export
-Pretty (Definition n) where
-  pretty def = group $
-    pretty def.name.val <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
-    pretty def.name.val <++> equals <+> softline <+> pretty def.tm
-
-export
-Pretty (Context n) where
-  pretty []           = neutral
-  pretty ([] :< def)  = pretty def
-  pretty (ctx :< def) = pretty ctx <+> hardline <+> hardline <+> pretty def
-
--- Operations ------------------------------------------------------------------
+-- Renaming --------------------------------------------------------------------
 
--- Renaming
-
-renameCnstr : Constructor n -> (Fin n -> Fin m) -> Constructor m
-renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
-renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
+rename : NormalForm ~|> Hom Elem NormalForm
 
+renameCnstr : Constructor ~|> Hom Elem Constructor
 renameCnstr (Sort s) f = Sort s
-renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
-renameCnstr (Sigma s s' var a b) f = Sigma s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
-renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
-renameCnstr (Left t) f = Left (renameWhnf t f)
-renameCnstr (Right t) f = Right (renameWhnf t f)
-renameCnstr (Container s a s' s'') f = Container s (renameWhnf a f) s' s''
-renameCnstr (MkContainer t p u) f = MkContainer (renameWhnf t f) (renameWhnf p f) (renameWhnf u f)
+renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
+renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
+renameCnstr (Sigma s s' var a b) f =
+  Sigma s s' var (rename a f) (rename b (lift [(_ ** ())] f))
+renameCnstr (Pair s s' prf t u) f = Pair s s' prf (rename t f) (rename u f)
+renameCnstr Bool f = Bool
+renameCnstr True f = True
+renameCnstr False f = False
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
-renameNtrl (Var var i) f = Var var (f i)
-renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
-renameNtrl (Fst t) f = Fst (renameNtrl t f)
-renameNtrl (Snd t) f = Snd (renameNtrl t f)
-renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f)
-renameNtrl (Tag t) f = Tag (renameNtrl t f)
-renameNtrl (Position t) f = Position (renameNtrl t f)
-renameNtrl (Next t) f = Next (renameNtrl t f)
+renameNtrl : Neutral ~|> Hom Elem Neutral
+renameNtrl (Var var sort prf i) f = Var var sort prf (f i)
+renameNtrl (App b t u) f = App b (renameNtrl t f) (rename u f)
+renameNtrl (Fst b t) f = Fst b (renameNtrl t f)
+renameNtrl (Snd b t) f = Snd b (renameNtrl t f)
+renameNtrl (If t u v) f = If (renameNtrl t f) (rename u f) (rename v f)
 renameNtrl Absurd f = Absurd
-renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
-renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
-renameNtrl (EqualR i t u) f = EqualR i (renameCnstr t f) (renameNtrl u f)
-renameNtrl (EqualU i t u) f = EqualU i (renameCnstr t f) (renameCnstr u f)
-renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (renameWhnf b f) (renameWhnf t f)
-renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (renameWhnf t f)
-renameNtrl (CastU a b t) f = CastU (renameCnstr a f) (renameCnstr b f) (renameWhnf t f)
-
-renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
-renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
-renameWhnf Irrel     f = Irrel
+renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (rename t f) (rename u f)
+renameNtrl (EqualL a b) f = EqualL (renameNtrl a f) (rename b f)
+renameNtrl (EqualR a b) f = EqualR (renameCnstr a f) (renameNtrl b f)
+renameNtrl (EqualStuck a b) f = EqualStuck (renameCnstr a f) (renameCnstr b f)
+renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (rename b f) (rename t f)
+renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (rename t f)
+renameNtrl (CastStuck a b t) f = CastStuck (renameCnstr a f) (renameCnstr b f) (rename t f)
+
+rename (Ntrl t) f = Ntrl $ renameNtrl t f
+rename (Cnstr t) f = Cnstr $ renameCnstr t f
+rename Irrel f = Irrel
 
 export
-Rename Constructor where
+Unsorted.Rename Bool Constructor where
   rename = renameCnstr
 
 export
-Rename Neutral where
+Unsorted.Rename Bool Neutral where
   rename = renameNtrl
-
-export
-Rename NormalForm where
-  rename = renameWhnf
-
+  
 export
-PointedRename Neutral where
-  point = Var ""
+Sorted.Rename Bool NormalForm where
+  rename = NormalForm.rename
 
 export
-PointedRename NormalForm where
-  point = Ntrl . point
+PointedRename Bool (\b => (String, (s : Sort ** isSet s = b))) NormalForm where
+  point {s = False} _ _ = Irrel
+  point {s = True} (var, (s ** prf)) i = Ntrl (Var var s (eqToSo prf) i)