99 lines
2.2 KiB
Idris
99 lines
2.2 KiB
Idris
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
|