Example dependent zipper

DepZip.idr

%default total

data Expr : Type -> Type where
  Var : a -> Expr a
  App : Expr a -> Expr b -> Expr a

GoLeft : Expr a -> Maybe Type 
GoLeft (Var x) = Nothing
GoLeft (App {a} x y) = Just a

GoRight : Expr a -> Maybe Type
GoRight (Var x) = Nothing
GoRight (App {b} x y) = Just b

data Ctx : Maybe Type -> Type where
  Root : Ctx (Just a)
  L : (x : Expr a) -> Ctx (Just a) -> Ctx (GoLeft x)
  R : (x : Expr a) -> Ctx (Just a) -> Ctx (GoRight x)

data Zipper : Type -> Type where
  Zip : Expr a -> Ctx (Just a) -> Zipper a

-- wraps a 'Zipper a' into a 'Sigma a : Type, Zipper a'.
wrap : Zipper a -> (a : Type ** Zipper a)
wrap x = (_ ** x)

subst : (x : (a : Type ** Zipper a)) -> Expr (fst x) -> (a : Type ** Zipper a)
subst (x ** pf) e =
  case pf of
    Zip e' c => (_ ** Zip e c)

left : (a : Type ** Zipper a) -> (b : Type ** Zipper b)
left (t ** pf) =
  case pf of
    Zip (Var x) c => (t ** pf)
    Zip (App x y) c => (_ ** Zip x (L (App x y) c))

up : (a : Type ** Zipper a) -> (b : Type ** Zipper b)
up (t ** pf) =
  case pf of
    (Zip e Root) => (t ** pf)
    (Zip e (L (Var x) c)) impossible
    (Zip e (L (App x y) c)) => (_ ** Zip (App e y) c)
    (Zip e (R (Var x) c)) impossible
    (Zip e (R (App x y) c)) => (_ ** Zip (App x e) c)

set : a -> Expr a
set x = Var x

ex1 : Expr Nat
ex1 = App (Var 2) (Var 3)

-- [App (Var 2) (Var 3)]
ex2 : Zipper Nat
ex2 = Zip ex1 Root

ex3 : (a : Type ** Zipper a)
ex3 = wrap ex2

-- (App [Var 2] (Var 3))
ex4 : (a : Type ** Zipper a)
ex4 = left ex3

-- (App [Var 4] (Var 3))
ex5 : (a : Type ** Zipper a)
ex5 = subst ex4 (set 4)

-- [App (Var 4) (Var 3)]
ex6 : (a : Type ** Zipper a)
ex6 = up ex5