quox/lib/Quox/Context.idr

369 lines
10 KiB
Idris
Raw Normal View History

2021-09-09 17:56:10 -04:00
module Quox.Context
import Quox.Syntax.Shift
import Quox.Pretty
2023-03-15 10:54:51 -04:00
import Quox.Name
2021-09-09 17:56:10 -04:00
import Data.DPair
import Data.Nat
2023-09-12 00:48:51 -04:00
import Data.Singleton
2021-09-09 17:56:10 -04:00
import Data.SnocList
import Data.SnocVect
import Data.Vect
2021-09-09 17:56:10 -04:00
import Control.Monad.Identity
%default total
||| a sequence of bindings under an existing context. each successive element
||| has one more bound variable, which correspond to all previous elements
2022-08-22 04:17:08 -04:00
||| as well as the surrounding context.
2021-09-09 17:56:10 -04:00
public export
data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
Lin : Telescope tm from from
(:<) : Telescope tm from to -> tm to -> Telescope tm from (S to)
%name Telescope tel
2021-09-25 14:11:29 -04:00
public export
Telescope' : (a : Type) -> (from, to : Nat) -> Type
2021-09-25 14:11:29 -04:00
Telescope' a = Telescope (\_ => a)
2022-08-22 04:17:08 -04:00
||| a top level context is actually just a telescope over no existing bindings
2021-09-09 17:56:10 -04:00
public export
Context : (tm : Nat -> Type) -> (len : Nat) -> Type
Context tm len = Telescope tm 0 len
2021-09-25 14:11:29 -04:00
public export
Context' : (a : Type) -> (len : Nat) -> Type
2021-09-25 14:11:29 -04:00
Context' a = Context (\_ => a)
2023-03-15 10:54:51 -04:00
public export
NContext : Nat -> Type
NContext = Context' BaseName
2023-05-01 21:06:25 -04:00
public export
BContext : Nat -> Type
BContext = Context' BindName
2023-03-15 10:54:51 -04:00
public export
unsnoc : Context tm (S n) -> (Context tm n, tm n)
unsnoc (tel :< x) = (tel, x)
2023-03-15 10:54:51 -04:00
public export
head : Context tm (S n) -> tm n
head = snd . unsnoc
2021-09-25 14:11:29 -04:00
2022-04-23 18:21:30 -04:00
public export
tail : Context tm (S n) -> Context tm n
tail = fst . unsnoc
2022-04-23 18:21:30 -04:00
2023-09-12 00:48:51 -04:00
parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a)
export
toSnocListWith : Telescope tm _ _ -> SnocList a
toSnocListWith [<] = [<]
toSnocListWith (tel :< t) = toSnocListWith tel :< f t
export
toListWith : Telescope tm _ _ -> List a
toListWith tel = toListAcc tel [] where
toListAcc : Telescope tm _ _ -> List a -> List a
toListAcc [<] acc = acc
toListAcc (tel :< t) acc = toListAcc tel (f t :: acc)
2021-09-09 17:56:10 -04:00
2023-04-15 09:13:01 -04:00
export
toSnocVectWith : Context tm n -> SnocVect n a
toSnocVectWith [<] = [<]
toSnocVectWith (tel :< t) = toSnocVectWith tel :< f t
2021-09-09 17:56:10 -04:00
export %inline
toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
toSnocList = toSnocListWith (Evidence _)
2021-09-25 14:11:29 -04:00
export %inline
2022-04-11 17:34:18 -04:00
toSnocList' : Telescope' a _ _ -> SnocList a
toSnocList' = toSnocListWith id
export %inline
toList : Telescope tm _ _ -> List (Exists tm)
toList = toListWith (Evidence _)
2021-09-25 14:11:29 -04:00
export %inline
2022-04-11 17:34:18 -04:00
toList' : Telescope' a _ _ -> List a
toList' = toListWith id
2023-04-15 09:13:01 -04:00
export %inline
toSnocVect : Context tm n -> SnocVect n (Exists tm)
toSnocVect = toSnocVectWith (Evidence _)
export %inline
toSnocVect' : Context' a n -> SnocVect n a
toSnocVect' = toSnocVectWith id
2021-09-09 17:56:10 -04:00
export
fromSnocVect : SnocVect n a -> Context' a n
fromSnocVect [<] = [<]
fromSnocVect (sx :< x) = fromSnocVect sx :< x
public export
tabulateLT : (n : Nat) -> ((i : Nat) -> (0 p : i `LT` n) => tm i) ->
Context tm n
tabulateLT 0 f = [<]
tabulateLT (S k) f =
tabulateLT k (\i => f i @{lteSuccRight %search}) :< f k @{reflexive}
public export
tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
tabulate f n = tabulateLT n (\i => f i)
-- [todo] fixup argument order lol
public export
replicate : (n : Nat) -> a -> Context' a n
replicate n x = tabulate (const x) n
2021-09-09 17:56:10 -04:00
public export
(.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
tel1 . [<] = tel1
tel1 . (tel2 :< s) = (tel1 . tel2) :< s
export
(<><) : Telescope' a from to -> Vect n a -> Telescope' a from (n + to)
(<><) tel [] = tel
(<><) tel (x :: xs) {n = S n} =
rewrite plusSuccRightSucc n to in
(tel :< x) <>< xs
export
(++) : Telescope' a from to -> SnocVect n a -> Telescope' a from (n + to)
tel ++ [<] = tel
tel ++ (sx :< x) = (tel ++ sx) :< x
2021-09-09 17:56:10 -04:00
2021-12-23 09:55:18 -05:00
public export
2022-02-26 19:22:02 -05:00
getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
Shift len out -> Context tm len -> Var len -> tm out
getShiftWith shft by (ctx :< t) VZ = t `shft` ssDown by
getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i
2022-02-26 19:22:02 -05:00
public export %inline
getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out
getShift = getShiftWith (//)
2021-09-09 17:56:10 -04:00
2021-12-23 09:55:18 -05:00
public export %inline
2022-02-26 19:22:02 -05:00
getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
Context tm len -> Var len -> tm len
getWith shft = getShiftWith shft SZ
2024-05-05 13:41:06 -04:00
export infixl 8 !!
2023-01-26 13:54:46 -05:00
public export %inline
2021-09-09 17:56:10 -04:00
(!!) : CanShift tm => Context tm len -> Var len -> tm len
2022-02-26 19:22:02 -05:00
(!!) = getWith (//)
2021-09-09 17:56:10 -04:00
2024-05-05 13:41:06 -04:00
export infixl 8 !!!
2021-12-23 09:56:01 -05:00
public export %inline
2022-02-26 19:22:02 -05:00
(!!!) : Context' tm len -> Var len -> tm
(!!!) = getWith const
2021-12-23 09:56:01 -05:00
2023-03-05 10:49:50 -05:00
public export
find : Alternative f =>
(forall n. tm n -> Bool) -> Context tm len -> f (Var len)
find p [<] = empty
find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx)
2021-09-09 17:56:10 -04:00
export
0 telescopeLTE : Telescope _ from to -> from `LTE` to
telescopeLTE [<] = reflexive
2021-09-09 17:56:10 -04:00
telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
export
2022-02-26 19:28:19 -05:00
(gt : from `GT` to) => Uninhabited (Telescope _ from to) where
uninhabited tel = void $ LTEImpliesNotGT (telescopeLTE tel) gt
2021-09-09 17:56:10 -04:00
export %hint
0 succGT : S n `GT` n
succGT = LTESucc reflexive
2021-09-09 17:56:10 -04:00
public export
drop : (m : Nat) -> Context term (m + n) -> Context term n
drop 0 ctx = ctx
drop (S m) (ctx :< _) = drop m ctx
2021-09-09 17:56:10 -04:00
parameters {auto _ : Applicative f}
export
traverse : (forall n. tm1 n -> f (tm2 n)) ->
Telescope tm1 from to -> f (Telescope tm2 from to)
traverse f [<] = pure [<]
traverse f (tel :< x) = [|traverse f tel :< f x|]
2023-05-01 21:06:25 -04:00
export %inline
traverse' : (a -> f b) -> Telescope' a from to -> f (Telescope' b from to)
traverse' f = traverse f
2024-05-05 13:41:06 -04:00
export infixl 3 `app`
2021-09-09 17:56:10 -04:00
||| like `(<*>)` but with effects
export
app : Telescope (\n => tm1 n -> f (tm2 n)) from to ->
Telescope tm1 from to -> f (Telescope tm2 from to)
app [<] [<] = pure [<]
app (ftel :< f) (xtel :< x) = [|app ftel xtel :< f x|]
2021-09-25 14:11:29 -04:00
app [<] (xtel :< _) = void $ uninhabited xtel
app (ftel :< _) [<] = void $ uninhabited ftel
2021-09-09 17:56:10 -04:00
export %inline
sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
sequence = traverse id
2023-05-01 21:06:25 -04:00
2022-02-26 19:28:19 -05:00
parameters {0 tm1, tm2 : Nat -> Type}
(f : forall n. tm1 n -> tm2 n)
export %inline
map : Telescope tm1 from to -> Telescope tm2 from to
map = runIdentity . traverse (pure . f)
2021-09-09 17:56:10 -04:00
2022-02-26 19:28:19 -05:00
export %inline
(<$>) : Telescope tm1 from to -> Telescope tm2 from to
(<$>) = map
2021-09-09 17:56:10 -04:00
2023-05-01 21:06:25 -04:00
2021-09-09 17:56:10 -04:00
export %inline
(<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
Telescope tm1 from to -> Telescope tm2 from to
ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
2022-02-26 19:28:36 -05:00
-- ...but can't write pure without `from,to` being ω, so no idiom brackets ☹
2023-01-26 13:54:46 -05:00
export %inline
(<$) : (forall n. tm1 n) -> Telescope tm2 from to -> Telescope tm1 from to
x <$ tel = const x <$> tel
2021-09-25 14:11:29 -04:00
2021-09-09 17:56:10 -04:00
export %inline
zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
Telescope tm1 from to -> Telescope tm2 from to ->
Telescope tm3 from to
zipWith f tel1 tel2 = f <$> tel1 <*> tel2
2021-09-25 14:11:29 -04:00
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
unzip : Telescope (\n => (tm1 n, tm2 n)) from to ->
(Telescope tm1 from to, Telescope tm2 from to)
unzip [<] = ([<], [<])
unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
2023-03-15 10:54:51 -04:00
export
unzip3 : Telescope (\n => (tm1 n, tm2 n, tm3 n)) from to ->
(Telescope tm1 from to, Telescope tm2 from to, Telescope tm3 from to)
unzip3 [<] = ([<], [<], [<])
unzip3 (tel :< (x, y, z)) =
let (xs, ys, zs) = unzip3 tel in (xs :< x, ys :< y, zs :< z)
2023-02-11 12:13:44 -05:00
2023-03-26 10:10:39 -04:00
public export
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
lengthPrf [<] = Element 0 Refl
2021-12-23 09:55:18 -05:00
lengthPrf (tel :< _) =
let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
2021-09-09 17:56:10 -04:00
2021-12-23 10:03:49 -05:00
export
lengthPrf0 : Context _ to -> Singleton to
2021-12-23 10:03:49 -05:00
lengthPrf0 ctx =
let Element len prf = lengthPrf ctx in
rewrite sym prf `trans` plusZeroRightNeutral len in
[|len|]
2021-12-23 10:03:49 -05:00
2021-09-09 17:56:10 -04:00
public export %inline
length : Telescope {} -> Nat
length = fst . lengthPrf
2023-03-26 10:10:39 -04:00
public export
null : Telescope _ from to -> Bool
null [<] = True
null _ = False
2021-09-09 17:56:10 -04:00
2021-12-23 09:55:18 -05:00
export
foldl : {0 acc : Nat -> Type} ->
(f : forall n. acc n -> tm (n + from) -> acc (S n)) ->
(z : acc 0) -> (tel : Telescope tm from to) -> acc (length tel)
foldl f z [<] = z
foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
2021-09-09 17:56:10 -04:00
export %inline
foldl_ : (acc -> tm -> acc) -> acc -> Telescope' tm from to -> acc
foldl_ f z tel = foldl f z tel
2021-12-23 09:55:18 -05:00
export %inline
foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
2021-09-09 17:56:10 -04:00
2021-12-23 09:55:18 -05:00
export %inline
fold : Monoid a => Telescope' a from to -> a
fold = foldMap id
2021-09-09 17:56:10 -04:00
2021-12-23 09:55:18 -05:00
||| like `fold` but calculate the elements only when actually appending
export %inline
foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
foldLazy = foldMap force
2021-09-09 17:56:10 -04:00
export %inline
all, any : (forall n. tm n -> Bool) -> Telescope tm from to -> Bool
all p = foldMap @{All} p
any p = foldMap @{Any} p
2021-09-25 14:11:29 -04:00
export %inline
2021-09-09 17:56:10 -04:00
(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
2023-03-08 16:33:52 -05:00
(==) = foldLazy @{All} .: zipWithLazy (==)
2021-09-09 17:56:10 -04:00
2021-09-25 14:11:29 -04:00
export %inline
2021-09-09 17:56:10 -04:00
(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
2021-09-25 14:11:29 -04:00
compare = foldLazy .: zipWithLazy compare
2021-09-09 17:56:10 -04:00
2023-03-13 13:25:07 -04:00
export %inline
(forall n. Show (tm n)) => Show (Telescope tm from to) where
showPrec d = showPrec d . toSnocList
where Show (Exists tm) where showPrec d t = showPrec d t.snd
2023-05-14 13:58:46 -04:00
parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
(nameHL : HL)
(pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))
private
prettyOne : BindName -> BContext to -> tm to -> Eff Pretty (Doc opts)
prettyOne x xs tm = hsep <$> sequence
[hl nameHL $ prettyBind' x, hl Delim $ text ":", pterm xs tm]
private
prettyEach : BContext to -> Telescope tm from to ->
Eff Pretty (Telescope' (Doc opts) from to)
prettyEach _ [<] = pure [<]
prettyEach (xs :< x) (ts :< t) = [|prettyEach xs ts :< prettyOne x xs t|]
export
prettyTel : BContext to -> Telescope tm from to -> Eff Pretty (Doc opts)
prettyTel names tel = do
docs <- prettyEach names tel
comma <- hl Delim $ text ","
pure $ separateTight comma $ toList' docs
2023-05-01 21:06:25 -04:00
namespace BContext
export
toNames : BContext n -> SnocList BaseName
2023-09-20 15:58:27 -04:00
toNames = foldl (\xs, x => xs :< x.val) [<]