@@ -700,6 +700,8 @@ substV x tm = dropV 0 (instantiate x tm) where
700 dropV i (Proj x idx) = Proj (dropV i x) idx
700 dropV i (Proj x idx) = Proj (dropV i x) idx
701 dropV i t = t
701 dropV i t = t
703+-- | Replace all non-free de Bruijn references in the given term with references
704+-- to the name of their binding.
703explicitNames :: TT n -> TT n
705explicitNames :: TT n -> TT n
704explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
706explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
705 Bind x b'
707 Bind x b'
@@ -709,6 +711,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
709explicitNames (Proj x idx) = Proj (explicitNames x) idx
711explicitNames (Proj x idx) = Proj (explicitNames x) idx
710explicitNames t = t
712explicitNames t = t
714+-- | Replace references to the given `Name`-like id with references to
715+-- de Bruijn index 0.
712pToV :: Eq n => n -> TT n -> TT n
716pToV :: Eq n => n -> TT n -> TT n
713pToV n = pToV' n 0
717pToV n = pToV' n 0
714pToV' n i (P _ x _) | n == x = V i
718pToV' n i (P _ x _) | n == x = V i
@@ -738,6 +742,9 @@ pToVs ns tm = pToVs' ns tm 0 where
738 pToVs' [] tm i = tm
742 pToVs' [] tm i = tm
739 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
743 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
745+-- | Replace de Bruijn indices in the given term with explicit references to
746+-- the names of the bindings they refer to. It is an error if the given term
747+-- contains free de Bruijn indices.
741vToP :: TT n -> TT n
748vToP :: TT n -> TT n
742vToP = vToP' [] where
749vToP = vToP' [] where
743 vToP' env (V i) = let (n, b) = (env !! i) in
750 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -747,12 +754,19 @@ vToP = vToP' [] where
747 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
754 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
748 vToP' env t = t
755 vToP' env t = t
757+-- | Replace every non-free reference to the name of a binding in
758+-- the given term with a de Bruijn index.
750finalise :: Eq n => TT n -> TT n
759finalise :: Eq n => TT n -> TT n
751finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
760finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
752finalise (App f a) = App (finalise f) (finalise a)
761finalise (App f a) = App (finalise f) (finalise a)
753finalise t = t
762finalise t = t
764+-- | As `instantiate`, but in addition to replacing `V 0`,
765+-- replace references to the given `Name`-like id.
755−subst :: Eq n => n -> TT n -> TT n -> TT n
766+subst :: Eq n => n {-^ The id to replace -} ->
767+ TT n {-^ The replacement term -} ->
768+ TT n {-^ The term to replace in -} ->
756subst n v tm = instantiate v (pToV n tm)
770subst n v tm = instantiate v (pToV n tm)
758substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
772substNames :: Eq n => [(n, TT n)] -> TT n -> TT n