quox/lib/Quox/Scope.idr

95 lines
2.3 KiB
Idris
Raw Permalink Normal View History

2022-10-10 11:30:46 -04:00
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