rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

remove old file i forgot about

Browse source
This commit is contained in:
rhiannon morris 2021-09-03 16:38:26 +02:00
parent 45150c2a3b
commit 06e5c09896
2 changed files with 0 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

98
src/Quox/Ctx.idr
View file

@ -1,98 +0,0 @@
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

1
src/Quox/Syntax/Term.idr
View file

@ -1,6 +1,5 @@
module Quox.Syntax.Term module Quox.Syntax.Term
import public Quox.Ctx
import public Quox.Syntax.Var import public Quox.Syntax.Var
import public Quox.Syntax.Shift import public Quox.Syntax.Shift
import public Quox.Syntax.Subst import public Quox.Syntax.Subst