1 files changed, 85 insertions, 0 deletions
diff --git a/src/Inky/Term/Rename.idr b/src/Inky/Term/Rename.idr
new file mode 100644
index 0000000..7bbd524
--- /dev/null
+++ b/src/Inky/Term/Rename.idr
@@ -0,0 +1,85 @@
+module Inky.Term.Rename
+
+import Inky.Term
+import Flap.Data.List
+import Flap.Data.SnocList.Thinning
+
+public export
+data Thins : Mode -> Mode -> Type where
+  NoSugar : NoSugar `Thins` NoSugar
+  Sugar : qtCtx1 `Thins` qtCtx2 -> Sugar qtCtx1 `Thins` Sugar qtCtx2
+  Quote : ctx2 `Thins` ctx3 -> Quote ctx1 ctx2 `Thins` Quote ctx1 ctx3
+
+export
+rename :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  Term mode meta tyCtx tmCtx ->
+  Term mode' meta tyCtx tmCtx'
+renameList :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  List (Term mode meta tyCtx tmCtx) ->
+  List (Term mode' meta tyCtx tmCtx')
+renameAll :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  (ts : Context (Term mode meta tyCtx tmCtx)) ->
+  All (Assoc0 $ Term mode' meta tyCtx tmCtx') ts.names
+renameBranches :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  (ts : Context (x ** Term mode meta tyCtx (tmCtx :< x))) ->
+  All (Assoc0 (x ** Term mode' meta tyCtx (tmCtx' :< x))) ts.names
+renameTy' :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  Ty' mode meta tyCtx tmCtx ->
+  Ty' mode' meta tyCtx tmCtx'
+renameBoundTy' :
+  mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
+  BoundTy' mode meta tyCtx tmCtx ->
+  BoundTy' mode' meta tyCtx tmCtx'
+
+rename f g (Annot m e a) = Annot m (rename f g e) (renameTy' f g a)
+rename f g (Var m i) = Var m (index g i)
+rename f g (Let m e (x ** t)) = Let m (rename f g e) (x ** rename f (Keep g) t)
+rename f g (LetTy m a (x ** t)) =
+  case f of
+    NoSugar => LetTy m a (x ** rename f g t)
+    Sugar _ => LetTy m a (x ** rename f g t)
+rename f g (Abs m (bound ** t)) = Abs m (bound ** rename f (g <>< lengthOf bound) t)
+rename f g (App m e ts) = App m (rename f g e) (renameList f g ts)
+rename f g (Tup m (MkRow ts fresh)) = Tup m (fromAll (renameAll f g ts) fresh)
+rename f g (Prj m e l) = Prj m (rename f g e) l
+rename f g (Inj m l t) = Inj m l (rename f g t)
+rename f g (Case m e (MkRow ts fresh)) =
+  Case m (rename f g e) (fromAll (renameBranches f g ts) fresh)
+rename f g (Roll m t) = Roll m (rename f g t)
+rename f g (Unroll m e) = Unroll m (rename f g e)
+rename f g (Fold m e (x ** t)) = Fold m (rename f g e) (x ** rename f (Keep g) t)
+rename f g (Map m a b c) = Map m (renameBoundTy' f g a) (renameTy' f g b) (renameTy' f g c)
+rename (Sugar f) g (QuasiQuote m t) = QuasiQuote m (rename (Quote g) f t)
+rename (Quote f) g (Unquote m t) = Unquote m (rename (Sugar g) f t)
+rename (Sugar f) g (QAbs m (bound ** t)) =
+  QAbs m (bound ** rename (Sugar (f <>< lengthOf bound)) g t)
+rename (Sugar f) g (Lit m k) = Lit m k
+rename (Sugar f) g (Suc m t) = Suc m (rename (Sugar f) g t)
+rename (Sugar f) g (List m ts) = List m (renameList (Sugar f) g ts)
+rename (Sugar f) g (Cons m t u) = Cons m (rename (Sugar f) g t) (rename (Sugar f) g u)
+rename (Sugar f) g (Str m str) = Str m str
+rename (Sugar f) g (FoldCase m e (MkRow ts fresh)) =
+  FoldCase m (rename (Sugar f) g e) (fromAll (renameBranches (Sugar f) g ts) fresh)
+
+renameList f g [] = []
+renameList f g (t :: ts) = rename f g t :: renameList f g ts
+
+renameAll f g [<] = [<]
+renameAll f g (ts :< (x :- t)) = renameAll f g ts :< (x :- rename f g t)
+
+renameBranches f g [<] = [<]
+renameBranches f g (ts :< (l :- (x ** t))) =
+  renameBranches f g ts :< (l :- (x ** rename f (Keep g) t))
+
+renameTy' NoSugar g a = a
+renameTy' (Sugar f) g a = a
+renameTy' (Quote f) g t = rename (Sugar g) f t
+
+renameBoundTy' NoSugar g xa = xa
+renameBoundTy' (Sugar f) g xa = xa
+renameBoundTy' (Quote f) g t = rename (Sugar g) f t