more context stuff
This commit is contained in:
parent
f87950915d
commit
36b3479c8d
1 changed files with 76 additions and 15 deletions
|
|
@ -21,24 +21,41 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
|
|||
(:<) : Telescope tm from to -> tm to -> Telescope tm from (S to)
|
||||
%name Telescope tel
|
||||
|
||||
public export
|
||||
Telescope' : Type -> (from, to : Nat) -> Type
|
||||
Telescope' a = Telescope (\_ => a)
|
||||
|
||||
||| a global context is actually just a telescope over no existing bindings
|
||||
public export
|
||||
Context : (tm : Nat -> Type) -> (len : Nat) -> Type
|
||||
Context tm len = Telescope tm 0 len
|
||||
|
||||
public export
|
||||
Context' : Type -> (len : Nat) -> Type
|
||||
Context' a = Context (\_ => a)
|
||||
|
||||
|
||||
export
|
||||
toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
|
||||
toSnocList [<] = [<]
|
||||
toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
|
||||
|
||||
private
|
||||
toList' : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
|
||||
toList' [<] acc = acc
|
||||
toList' (tel :< t) acc = toList' tel (Evidence _ t :: acc)
|
||||
toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
|
||||
toListAcc [<] acc = acc
|
||||
toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
|
||||
|
||||
export %inline
|
||||
toList : Telescope tm _ _ -> List (Exists tm)
|
||||
toList tel = toList' tel []
|
||||
toList tel = toListAcc tel []
|
||||
|
||||
export %inline
|
||||
toSnocList' : Telescope' a _ _ -> SnocList a
|
||||
toSnocList' = map snd . toSnocList
|
||||
|
||||
export %inline
|
||||
toList' : Telescope' a _ _ -> List a
|
||||
toList' = map snd . toList
|
||||
|
||||
|
||||
infixl 9 .
|
||||
|
|
@ -65,6 +82,9 @@ public export
|
|||
Triangle : (tm : Nat -> Type) -> (len : Nat) -> Type
|
||||
Triangle = Context . Context
|
||||
|
||||
public export
|
||||
Triangle' : Type -> (len : Nat) -> Type
|
||||
Triangle' a = Context $ Context (\_ => a)
|
||||
|
||||
export
|
||||
0 telescopeLTE : Telescope _ from to -> from `LTE` to
|
||||
|
|
@ -79,10 +99,6 @@ export %hint
|
|||
0 succGT : S n `GT` n
|
||||
succGT = LTESucc $ reflexive {rel=LTE}
|
||||
|
||||
export %inline
|
||||
absurd0 : (0 _ : Uninhabited a) => (0 _ : a) -> x
|
||||
absurd0 x = void $ absurd x
|
||||
|
||||
|
||||
parameters {auto _ : Applicative f}
|
||||
export
|
||||
|
|
@ -98,8 +114,8 @@ parameters {auto _ : Applicative f}
|
|||
Telescope tm1 from to -> f (Telescope tm2 from to)
|
||||
app [<] [<] = pure [<]
|
||||
app (ftel :< f) (xtel :< x) = [|app ftel xtel :< f x|]
|
||||
app [<] (xtel :< _) = absurd0 xtel
|
||||
app (ftel :< _) [<] = absurd0 ftel
|
||||
app [<] (xtel :< _) = void $ uninhabited xtel
|
||||
app (ftel :< _) [<] = void $ uninhabited ftel
|
||||
|
||||
export %inline
|
||||
sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
|
||||
|
|
@ -124,6 +140,7 @@ ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
|
|||
-- ...but can't write pure without `from,to` being relevant,
|
||||
-- so no idiom brackets ☹
|
||||
|
||||
|
||||
export %inline
|
||||
zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
|
||||
Telescope tm1 from to -> Telescope tm2 from to ->
|
||||
|
|
@ -138,6 +155,22 @@ zipWith3 : (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
|
|||
Telescope tm4 from to
|
||||
zipWith3 f tel1 tel2 tel3 = f <$> tel1 <*> tel2 <*> tel3
|
||||
|
||||
export %inline
|
||||
zipWithLazy : forall tm1, tm2, tm3.
|
||||
(forall n. tm1 n -> tm2 n -> tm3 n) ->
|
||||
Telescope tm1 from to -> Telescope tm2 from to ->
|
||||
Telescope (\n => Lazy (tm3 n)) from to
|
||||
zipWithLazy f = zipWith $ delay .: f
|
||||
|
||||
export %inline
|
||||
zipWith3Lazy : forall tm1, tm2, tm3, tm4.
|
||||
(forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
|
||||
Telescope tm1 from to ->
|
||||
Telescope tm2 from to ->
|
||||
Telescope tm3 from to ->
|
||||
Telescope (\n => Lazy (tm4 n)) from to
|
||||
zipWith3Lazy f = zipWith3 (\x, y, z => delay $ f x y z)
|
||||
|
||||
|
||||
export
|
||||
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
|
||||
|
|
@ -172,14 +205,42 @@ parameters {auto _ : Monoid a}
|
|||
foldLazy = foldMap force
|
||||
|
||||
|
||||
export
|
||||
export %inline
|
||||
and : Telescope' (Lazy Bool) from to -> Bool
|
||||
and = force . fold @{All}
|
||||
|
||||
export %inline
|
||||
all : (forall n. f n -> Bool) -> Telescope f from to -> Bool
|
||||
all p = and . map (delay . p)
|
||||
|
||||
export %inline
|
||||
all2 : (forall n. f n -> g n -> Bool) ->
|
||||
Telescope f from to -> Telescope g from to -> Bool
|
||||
all2 p = and .: zipWithLazy p
|
||||
|
||||
|
||||
export %inline
|
||||
or : Telescope' (Lazy Bool) from to -> Bool
|
||||
or = force . fold @{Any}
|
||||
|
||||
export %inline
|
||||
any : (forall n. f n -> Bool) -> Telescope f from to -> Bool
|
||||
any p = or . map (delay . p)
|
||||
|
||||
export %inline
|
||||
any2 : (forall n. f n -> g n -> Bool) ->
|
||||
Telescope f from to -> Telescope g from to -> Bool
|
||||
any2 p = or .: zipWithLazy p
|
||||
|
||||
|
||||
export %inline
|
||||
(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
|
||||
(==) = fold @{All} .: zipWith (==)
|
||||
(==) = all2 (==)
|
||||
|
||||
export
|
||||
export %inline
|
||||
(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
|
||||
compare = foldLazy .: zipWith (delay .: compare)
|
||||
compare = foldLazy .: zipWithLazy compare
|
||||
|
||||
export
|
||||
export %inline
|
||||
(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
|
||||
prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
|
||||
|
|
|
|||
Loading…
Reference in a new issue