module Quox.Ctx

import Data.Nat
import Data.Fin
import Data.SnocList
import Data.DPair


%default total

public export
data Ctx : Nat -> (Nat -> Type) -> Type where
  Lin  : Ctx 0 f
  (:<) : Ctx n f -> f n -> Ctx (S n) f

%name Ctx ctx


public export
0 Ctx' : Nat -> Type -> Type
Ctx' n a = Ctx n (\_ => a)


public export
toSList : Ctx n f -> SnocList (Exists f)
toSList [<]        = [<]
toSList (ctx :< x) = toSList ctx :< Evidence _ x

public export
toSList' : Ctx' n a -> SnocList a
toSList' ctx = map (.snd) $ toSList ctx

public export
fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
fromSList' [<]       = [<]
fromSList' (sx :< x) = fromSList' sx :< x


public export
0 Weaken : (Nat -> Type) -> Type
Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)

public export
interface Weak f where weakN : Weaken f

public export
weak : Weak f => (1 x : f n) -> f (S n)
weak = weakN 1


public export
lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
lookBy w = go 0 where
  go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
  go by (ctx :< x) (FZ {k})   =
    rewrite sym $ plusSuccRightSucc by k in w (S by) x
  go by (ctx :< x) (FS {k} i) =
    rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i

public export
look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
look = lookBy weakN

infixl 9 !!
public export
(!!) : Ctx' n a -> (1 _ : Fin n) -> a
(!!) = lookBy (\_, x => x)


public export
map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
map f [<]        = [<]
map f (ctx :< x) = map f ctx :< f x


public export
(forall n. Eq (f n)) => Eq (Ctx n f) where
  [<]         == [<]         = True
  (ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y

public export
(forall n. Ord (f n)) => Ord (Ctx n f) where
  compare [<]         [<]         = EQ
  compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y


||| like `Exists` but only shows the second part
private
data ShowWrapper : (Nat -> Type) -> Type where
  SW : f n -> ShowWrapper f

private
(forall n. Show (f n)) => Show (ShowWrapper f) where
  showPrec d (SW x) = showPrec d x

export
(forall n. Show (f n)) => Show (Ctx n f) where
  show = show . map (\x => SW {f} x.snd) . toSList