95 lines
2.3 KiB
Idris
95 lines
2.3 KiB
Idris
|
module Quox.Scope
|
||
|
|
|
||
|
|
import public Quox.OPE
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Sub {a : Type} (t : Scoped a) (xs : Scope a) where
|
||
|
|
constructor Su
|
||
|
|
{0 support : Scope a}
|
||
|
|
term : t support
|
||
|
|
thin : support `LTE` xs
|
||
|
|
|
||
|
|
public export
|
||
|
|
CoverS : Sub s xs -> Sub t xs -> Type
|
||
|
|
CoverS ss tt = Cover ss.thin tt.thin
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
inj : Length xs => t xs -> Sub t xs
|
||
|
|
inj x = Su x id
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
flat : Sub (Sub t) xs -> Sub t xs
|
||
|
|
flat (Su (Su x q) p) = Su x (p . q)
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
thinSub : xs `LTE` ys -> Sub t xs -> Sub t ys
|
||
|
|
thinSub p x = flat $ Su x p
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
map : (forall x. s x -> t x) -> Sub s x -> Sub t x
|
||
|
|
map f = {term $= f}
|
||
|
|
|
||
|
|
public export
|
||
|
|
data Unit : Scoped a where
|
||
|
|
Nil : Unit [<]
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
unit : Length xs => Sub Unit xs
|
||
|
|
unit = Su [] zero
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Coprod {a : Type} {xs, ys, zs : Scope a}
|
||
|
|
(p : xs `LTE` zs) (q : ys `LTE` zs) where
|
||
|
|
constructor Cop
|
||
|
|
{0 scope : Scope a}
|
||
|
|
{thin : scope `LTE` zs}
|
||
|
|
{thinP : xs `LTE` scope}
|
||
|
|
{thinQ : ys `LTE` scope}
|
||
|
|
compP : Comp thin thinP p
|
||
|
|
compQ : Comp thin thinQ q
|
||
|
|
0 cover : Cover thinP thinQ
|
||
|
|
|
||
|
|
export
|
||
|
|
coprod : (p : xs `LTE` zs) -> (q : ys `LTE` zs) -> Coprod p q
|
||
|
|
coprod End End = %search
|
||
|
|
coprod (Keep p) (Keep q) = let Cop {} = coprod p q in %search
|
||
|
|
coprod (Keep p) (Drop q) = let Cop {} = coprod p q in %search
|
||
|
|
coprod (Drop p) (Keep q) = let Cop {} = coprod p q in %search
|
||
|
|
coprod (Drop p) (Drop q) =
|
||
|
|
-- idk why this one is harder to solve
|
||
|
|
let Cop compP compQ cover = coprod p q in
|
||
|
|
Cop (CD0 compP) (CD0 compQ) cover
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Pair {a : Type} (s, t : Scoped a) (zs : Scope a) where
|
||
|
|
constructor MkPair
|
||
|
|
fst : Sub s zs
|
||
|
|
snd : Sub t zs
|
||
|
|
0 cover : CoverS fst snd
|
||
|
|
|
||
|
|
export
|
||
|
|
pair : Sub s xs -> Sub t xs -> Sub (Pair s t) xs
|
||
|
|
pair (Su x p) (Su y q) =
|
||
|
|
let c = coprod p q in
|
||
|
|
Su (MkPair (Su x c.thinP) (Su y c.thinQ) c.cover) c.thin
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
data Var : a -> Scope a -> Type where
|
||
|
|
Only : Var x [< x]
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
var : (0 x : a) -> [< x] `LTE` xs => Sub (Var x) xs
|
||
|
|
var x @{p} = Su Only p
|
||
|
|
|
||
|
|
|
||
|
|
infix 0 \\\, \\
|
||
|
|
public export
|
||
|
|
data Bind : (t : Scoped a) -> (new, old : Scope a) -> Type where
|
||
|
|
(\\\) : new' `LTE` new -> t (old ++ new') -> Bind t new old
|
||
|
|
|
||
|
|
(\\) : (new : Scope a) -> Sub t (old ++ new) -> Sub (Bind t new) old
|
||
|
|
vs \\ Su term p with (split vs p)
|
||
|
|
vs \\ Su term (l ++ r) | MkSplit l r Refl Refl = Su (r \\\ term) l
|