{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wunused-imports -Wunused-top-binds -Worphans #-}

module Mikan.Syntax.Internal.Telescope
  (
  -- * Telescopes
    Tele(EmptyTel, ExtendTel)
  , type Telescope
  , mapAbsNames, mapAbsNamesM
  , telToArgs

  , type ListTel, type ListTel'
  , listTel, telToList, telFromList, foldTeleIndices

  , Teletype(..)
  , unpackTeletype
  ) where

import Control.DeepSeq

import GHC.Generics (Generic)

import Data.List qualified as List

import Mikan.Syntax.Concrete.Glyph qualified as P
import Mikan.Syntax.Internal.Term
import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Internal.Dom
import Mikan.Syntax.Position
import Mikan.Syntax.Common

import Mikan.Utils.Impossible
import Mikan.Utils.ExpandCase
import Mikan.Utils.List
import Mikan.Utils.Size
import Mikan.Utils.Null
import Mikan.Utils.Lens

---------------------------------------------------------------------------
-- * Telescopes and teletypes
---------------------------------------------------------------------------

-- | Sequence of types. An argument of the first type is bound in later types
--   and so on.
data Tele a
  = EmptyTel
  | ExtendTel# a !Int {-# UNPACK #-} !(Abs (Tele a))
  -- ^ The 'Abs' must never be 'NoAbs'.
  deriving (Int -> Tele a -> ShowS
[Tele a] -> ShowS
Tele a -> String
(Int -> Tele a -> ShowS)
-> (Tele a -> String) -> ([Tele a] -> ShowS) -> Show (Tele a)
forall a. Show a => Int -> Tele a -> ShowS
forall a. Show a => [Tele a] -> ShowS
forall a. Show a => Tele a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Tele a -> ShowS
showsPrec :: Int -> Tele a -> ShowS
$cshow :: forall a. Show a => Tele a -> String
show :: Tele a -> String
$cshowList :: forall a. Show a => [Tele a] -> ShowS
showList :: [Tele a] -> ShowS
Show, (forall a b. (a -> b) -> Tele a -> Tele b)
-> (forall a b. a -> Tele b -> Tele a) -> Functor Tele
forall a b. a -> Tele b -> Tele a
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Tele a -> Tele b
fmap :: forall a b. (a -> b) -> Tele a -> Tele b
$c<$ :: forall a b. a -> Tele b -> Tele a
<$ :: forall a b. a -> Tele b -> Tele a
Functor, Functor Tele
Foldable Tele
(Functor Tele, Foldable Tele) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Tele a -> f (Tele b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Tele (f a) -> f (Tele a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Tele a -> m (Tele b))
-> (forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a))
-> Traversable Tele
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
$csequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
sequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
Traversable, (forall x. Tele a -> Rep (Tele a) x)
-> (forall x. Rep (Tele a) x -> Tele a) -> Generic (Tele a)
forall x. Rep (Tele a) x -> Tele a
forall x. Tele a -> Rep (Tele a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Tele a) x -> Tele a
forall a x. Tele a -> Rep (Tele a) x
$cfrom :: forall a x. Tele a -> Rep (Tele a) x
from :: forall x. Tele a -> Rep (Tele a) x
$cto :: forall a x. Rep (Tele a) x -> Tele a
to :: forall x. Rep (Tele a) x -> Tele a
Generic)

pattern ExtendTel :: a -> Abs (Tele a) -> Tele a
pattern $bExtendTel :: forall a. a -> Abs (Tele a) -> Tele a
$mExtendTel :: forall {r} {a}.
Tele a -> (a -> Abs (Tele a) -> r) -> ((# #) -> r) -> r
ExtendTel a b <- ExtendTel# a _ b where
  ExtendTel a
a Abs (Tele a)
b = case Abs (Tele a)
b of
    Abs !ArgName
_ !Tele a
t -> a -> Int -> Abs (Tele a) -> Tele a
forall a. a -> Int -> Abs (Tele a) -> Tele a
ExtendTel# a
a (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Tele a -> Int
forall a. Sized a => a -> Int
size Tele a
t) Abs (Tele a)
b
    NoAbs{}   -> Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# INLINE ExtendTel #-}
{-# COMPLETE EmptyTel, ExtendTel #-}

instance NFData a => NFData (Tele a)

instance Eq a => Eq (Tele a) where
  Tele a
EmptyTel == :: Tele a -> Tele a -> Bool
== Tele a
EmptyTel = Bool
True
  Tele a
EmptyTel == Tele a
_        = Bool
False

  ExtendTel# a
_ Int
_ Abs (Tele a)
_ == Tele a
EmptyTel = Bool
False
  ExtendTel# a
a Int
n Abs (Tele a)
b == ExtendTel# a
a' Int
n' Abs (Tele a)
b' = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' Bool -> Bool -> Bool
&& a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a' Bool -> Bool -> Bool
&& case (Abs (Tele a)
b, Abs (Tele a)
b') of
    (Abs ArgName
_ Tele a
b, Abs ArgName
_ Tele a
b') -> Tele a
b Tele a -> Tele a -> Bool
forall a. Eq a => a -> a -> Bool
== Tele a
b'
    (Abs (Tele a), Abs (Tele a))
_                   -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Ord a => Ord (Tele a) where
  compare :: Tele a -> Tele a -> Ordering
compare Tele a
x Tele a
y = case Tele a
x of
    Tele a
EmptyTel -> case Tele a
y of
      Tele a
EmptyTel     -> Ordering
EQ
      ExtendTel#{} -> Ordering
LT

    ExtendTel# a
a Int
n Abs (Tele a)
b -> case Tele a
y of
      Tele a
EmptyTel            -> Ordering
GT
      ExtendTel# a
a' Int
n' Abs (Tele a)
b' -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
n' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> case (Abs (Tele a)
b, Abs (Tele a)
b') of
        (Abs ArgName
_ Tele a
b, Abs ArgName
_ Tele a
b') -> Tele a -> Tele a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Tele a
b Tele a
b'
        (Abs (Tele a), Abs (Tele a))
_                   -> Ordering
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Null (Tele a) where
  empty :: Tele a
empty = Tele a
forall a. Tele a
EmptyTel

  null :: Tele a -> Bool
null Tele a
EmptyTel    = Bool
True
  null ExtendTel{} = Bool
False

deriving via DontExpand (Tele a) instance ExpandCase LiftedRep (Tele a)

instance Foldable Tele where
  foldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
foldr a -> b -> b
f b
z = \case
    Tele a
EmptyTel      -> b
z
    ExtendTel a
a Abs (Tele a)
b -> a
a a -> b -> b
`f` (a -> b -> b) -> b -> Tele a -> b
forall a b. (a -> b -> b) -> b -> Tele a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
z (Abs (Tele a) -> Tele a
forall a. Abs a -> a
unAbs Abs (Tele a)
b)

  length :: forall a. Tele a -> Int
length = Tele a -> Int
forall a. Sized a => a -> Int
size

-- | The size of a telescope is its length (as a list).
instance Sized (Tele a) where
  size :: Tele a -> Int
size Tele a
EmptyTel           = Int
0
  size (ExtendTel# a
_ Int
s Abs (Tele a)
_) = Int
s

  natSize :: Tele a -> Peano
natSize Tele a
EmptyTel          = Peano
Zero
  natSize (ExtendTel a
_ Abs (Tele a)
tel) = Peano -> Peano
Succ (Peano -> Peano) -> Peano -> Peano
forall a b. (a -> b) -> a -> b
$ Abs (Tele a) -> Peano
forall a. Sized a => a -> Peano
natSize Abs (Tele a)
tel

instance KillRange a => KillRange (Tele a) where
  killRange :: KillRangeT (Tele a)
killRange = (a -> a) -> KillRangeT (Tele a)
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. KillRange a => KillRangeT a
killRange

instance (t ~ Dom a, Pretty a) => Pretty (Tele t) where
  pretty :: Tele t -> Doc
pretty Tele t
tel = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep
    [ Dom a -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
pDom Dom a
a (ArgName -> Doc
forall a. Pretty a => a -> Doc
pretty ArgName
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty (Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
a))
    | dom :: Dom (ArgName, a)
dom@(Dom' DomInfo Term
i (ArgName
x, a
a')) <- Tele (Dom a) -> [Dom (ArgName, a)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele t
Tele (Dom a)
tel
    , let a :: Dom a
a = DomInfo Term -> a -> Dom a
forall t e. DomInfo t -> e -> Dom' t e
Dom' DomInfo Term
i a
a'
    ]

-- | A traversal for the names in a telescope.
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM :: forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
_ Tele a
EmptyTel                  = Tele a -> m (Tele a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele a
forall a. Tele a
EmptyTel
mapAbsNamesM ArgName -> m ArgName
f (ExtendTel a
a (  Abs ArgName
x Tele a
b)) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (  ArgName -> Tele a -> Abs (Tele a)
forall a. ArgName -> a -> Abs a
Abs (ArgName -> Tele a -> Abs (Tele a))
-> m ArgName -> m (Tele a -> Abs (Tele a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m ArgName
f ArgName
x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ArgName -> m ArgName) -> Tele a -> m (Tele a)
forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
f Tele a
b)
mapAbsNamesM ArgName -> m ArgName
f (ExtendTel a
a (NoAbs ArgName
x Tele a
b)) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> Tele a -> Abs (Tele a)
forall a. ArgName -> a -> Abs a
NoAbs (ArgName -> Tele a -> Abs (Tele a))
-> m ArgName -> m (Tele a -> Abs (Tele a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m ArgName
f ArgName
x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ArgName -> m ArgName) -> Tele a -> m (Tele a)
forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
f Tele a
b)
  -- Ulf, 2013-11-06: Last case is really impossible but I'd rather find out we
  --                  violated that invariant somewhere other than here.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames :: forall a. (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames ArgName -> ArgName
f = Identity (Tele a) -> Tele a
forall a. Identity a -> a
runIdentity (Identity (Tele a) -> Tele a)
-> (Tele a -> Identity (Tele a)) -> Tele a -> Tele a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName -> Identity ArgName) -> Tele a -> Identity (Tele a)
forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM (ArgName -> Identity ArgName
forall a. a -> Identity a
Identity (ArgName -> Identity ArgName)
-> (ArgName -> ArgName) -> ArgName -> Identity ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ArgName
f)

-- | Telescope as list.
type ListTel' a = [Dom (a, Type)]
type ListTel = ListTel' ArgName

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
telFromList' :: forall a. (a -> ArgName) -> ListTel' a -> Telescope
telFromList' a -> ArgName
f = (Dom (a, Type) -> Telescope -> Telescope)
-> Telescope -> [Dom (a, Type)] -> Telescope
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr Dom (a, Type) -> Telescope -> Telescope
extTel Telescope
forall a. Tele a
EmptyTel
  where
    extTel :: Dom (a, Type) -> Telescope -> Telescope
extTel dom :: Dom (a, Type)
dom@Dom'{unDom :: forall t e. Dom' t e -> e
unDom = (a
x, Type
a)} = Dom' Term Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Dom (a, Type)
dom{unDom = a}) (Abs Telescope -> Telescope)
-> (Telescope -> Abs Telescope) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs (a -> ArgName
f a
x)

-- | Convert a list telescope to a telescope.
telFromList :: ListTel -> Telescope
telFromList :: ListTel -> Telescope
telFromList = (ArgName -> ArgName) -> ListTel -> Telescope
forall a. (a -> ArgName) -> ListTel' a -> Telescope
telFromList' ArgName -> ArgName
forall a. a -> a
id

-- | Convert a telescope to its list form.
--
-- This function returns '__IMPOSSIBLE__' if it encounters a 'NoAbs'.
telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
telToList :: forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
EmptyTel                    = []
telToList (ExtendTel Dom t
arg (Abs ArgName
x Tele (Dom t)
tel)) = ((t -> (ArgName, t)) -> Dom t -> Dom (ArgName, t)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName
x,) Dom t
arg Dom (ArgName, t) -> [Dom (ArgName, t)] -> [Dom (ArgName, t)]
forall a. a -> [a] -> [a]
:) ([Dom (ArgName, t)] -> [Dom (ArgName, t)])
-> [Dom (ArgName, t)] -> [Dom (ArgName, t)]
forall a b. (a -> b) -> a -> b
$! Tele (Dom t) -> [Dom (ArgName, t)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
tel
telToList (ExtendTel Dom t
_    NoAbs{}   ) = [Dom (ArgName, t)]
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# INLINE foldTeleIndices #-}
-- | Fold over the de Bruijn indices of a telescope.
--
-- This function returns '__IMPOSSIBLE__' if it encounters a 'NoAbs'.
--
-- == __Examples__
--
-- >>> foldTeleIndices (:) (ExtendTel () $ Abs "x" $ ExtendTel () $ Abs "y" $ ExtendTel () $ Abs "z" EmptyTel)
-- [2, 1, 0]
foldTeleIndices :: (Int -> b -> b) -> b -> Tele a -> b
foldTeleIndices :: forall b a. (Int -> b -> b) -> b -> Tele a -> b
foldTeleIndices Int -> b -> b
f = Int -> b -> Tele a -> b
loop Int
0 where
  {-# INLINABLE loop #-}
  loop :: Int -> b -> Tele a -> b
loop !Int
i !b
acc Tele a
EmptyTel = b
acc
  loop Int
i b
acc (ExtendTel a
arg (Abs ArgName
_ Tele a
tel)) = Int -> b -> Tele a -> b
loop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> b -> b
f Int
i b
acc) Tele a
tel
  loop Int
i b
acc (ExtendTel a
arg (NoAbs ArgName
_ Tele a
tel)) = b
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Lens to edit a 'Telescope' as a list.
listTel :: Lens' Telescope ListTel
listTel :: Lens' Telescope ListTel
listTel ListTel -> f ListTel
f = (ListTel -> Telescope) -> f ListTel -> f Telescope
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ListTel -> Telescope
telFromList (f ListTel -> f Telescope)
-> (Telescope -> f ListTel) -> Telescope -> f Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListTel -> f ListTel
f (ListTel -> f ListTel)
-> (Telescope -> ListTel) -> Telescope -> f ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

-- | Drop the types from a telescope.
class TelToArgs a where
  telToArgs :: a -> [Arg ArgName]

instance TelToArgs ListTel where
  telToArgs :: ListTel -> [Arg ArgName]
telToArgs = (Dom (ArgName, Type) -> Arg ArgName) -> ListTel -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' \Dom (ArgName, Type)
dom -> ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg (Dom (ArgName, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (ArgName, Type)
dom) ((ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName) -> (ArgName, Type) -> ArgName
forall a b. (a -> b) -> a -> b
$ Dom (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom Dom (ArgName, Type)
dom)

instance TelToArgs Telescope where
  telToArgs :: Telescope -> [Arg ArgName]
telToArgs = ListTel -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs (ListTel -> [Arg ArgName])
-> (Telescope -> ListTel) -> Telescope -> [Arg ArgName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

type Telescope = Tele (Dom Type)

-- | A 'Teletype' represents a 'Type' with some "pending"
-- quantification.
--
-- Teletypes are used to avoid the quadratic accumulation of 'PiSort's
-- when quantifying a type over a telescope, particularly in
-- metavariables.
--
-- Teletypes are otherwise identical to 'Type's (by making quantifiers
-- into 'Pi's); teletypes can be operated on transparently by the
-- functions in "Mikan.TypeChecking.Telescope".
data Teletype
  -- | A 'Type' with no quantification.
  = EmptyTt  Type
  -- | A 'Teletype' with an extra domain.
  | ExtendTt !(Dom Type) {-# UNPACK #-} !(Abs Teletype)
    -- ^ 'Abs' is never 'NoAbs'.
  deriving (Int -> Teletype -> ShowS
[Teletype] -> ShowS
Teletype -> String
(Int -> Teletype -> ShowS)
-> (Teletype -> String) -> ([Teletype] -> ShowS) -> Show Teletype
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Teletype -> ShowS
showsPrec :: Int -> Teletype -> ShowS
$cshow :: Teletype -> String
show :: Teletype -> String
$cshowList :: [Teletype] -> ShowS
showList :: [Teletype] -> ShowS
Show, (forall x. Teletype -> Rep Teletype x)
-> (forall x. Rep Teletype x -> Teletype) -> Generic Teletype
forall x. Rep Teletype x -> Teletype
forall x. Teletype -> Rep Teletype x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Teletype -> Rep Teletype x
from :: forall x. Teletype -> Rep Teletype x
$cto :: forall x. Rep Teletype x -> Teletype
to :: forall x. Rep Teletype x -> Teletype
Generic)

-- | Unpack a 'Teletype' into a pair of a 'Telescope' and a 'Type'.
--
-- The 'Type' lives under the returned 'Telescope'. Only the quantifiers
-- that belong explicitly to the 'Teletype' are returned in the
-- 'Telescope': even if the 'Type' has some manifest quantification, it
-- will not be moved into the 'Telescope'.
unpackTeletype :: Teletype -> (Telescope, Type)
unpackTeletype :: Teletype -> (Telescope, Type)
unpackTeletype (EmptyTt Type
t)      = (Telescope
forall a. Tele a
EmptyTel, Type
t)
unpackTeletype (ExtendTt Dom' Term Type
dom Abs Teletype
a) = case Abs Teletype
a of
  NoAbs{}       -> (Telescope, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
  Abs !ArgName
nm !Teletype
body -> case Teletype -> (Telescope, Type)
unpackTeletype (Abs Teletype -> Teletype
forall a. Abs a -> a
unAbs Abs Teletype
a) of
    (!Telescope
tel, !Type
ty) -> (Dom' Term Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
dom (ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs ArgName
nm Telescope
tel), Type
ty)

instance Pretty Teletype where
  prettyPrec :: Int -> Teletype -> Doc
prettyPrec Int
p Teletype
tty = do
    let (Telescope
quant, Type
ty) = Teletype -> (Telescope, Type)
unpackTeletype Teletype
tty
    Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
      Doc -> Doc
hlPrimitive Doc
"Π" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
quant Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
P.arrow Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
ty

instance NFData Teletype