{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wunused-imports -Wunused-top-binds -Worphans #-}

module Mikan.Syntax.Internal.Term
  (
  -- * Terms
    Term(Var, Lam, Lit, Def, Con, Pi, Sort, Level, MetaV, DontCare, Dummy)
  , dontCare, stripDontCare

  -- ** Variable sharing
  , var, unsharedVar, varTable, varTableSize

  -- ** Constructors
  , ConHead(..)
  , type ConInfo
  , LensConName(..)

  -- ** Dummies
  , DummyTermKind(..)
  , __DUMMY_TERM_WITH__
  , __DUMMY_TERM__
  , impossibleTerm

  -- * Arguments and eliminations
  , module Mikan.Syntax.Internal.Elim
  , type Args, type Elims, type Elim, type NamedArgs
  , type Args1, type NamedArgs1

  -- ** Spined forms
  , SpineHead(..), SpineHead'(..)
  , unSpine
  , hasElims

  -- * Types
  , Type''(..), type Type', type Type
  , __DUMMY_TYPE__

  -- ** Domains
  , type Dom
  , __DUMMY_DOM__

  -- ** Sorts
  , module Mikan.Syntax.Internal.Univ
  , Sort'(.., Prop, SSet, Type), type Sort
  , UnivSize(..)
  , varSort, mkType, mkProp, mkSSet, tmSort, tmSSort
  , isProp, isStrictDataSort, propToType
  , isSort, sortUniv
  , LensSort(..)
  , __DUMMY_SORT__

  -- *** Universe levels
  , Level'(.., ClosedLevel), type Level
  , PlusLevel'(..), type PlusLevel
  , type LevelAtom
  , levelSuc
  , levelPlus
  , atomicLevel
  , __DUMMY_LEVEL__

  -- * Substitutions
  , Substitution'(..)
  , type Substitution, type Renaming
  , NoSubst(..)
  , BraveTerm(..)

  -- * Blocked terms
  , module Mikan.Syntax.Internal.Blockers
  , type Blocked
  , type NotBlocked
  , type Blocked_

  -- * Basic traversals
  , TermSize(..)
  , TypeOf

  -- * Reexports
  , module Mikan.Syntax.Abstract.Name
  , MetaId(..), ProblemId(..)
  ) where

import Prelude hiding (null)

import Control.DeepSeq
import GHC.Exts

import Data.List qualified as List
import Data.Semigroup ( Sum(..) )

import GHC.Generics (Generic)

import Mikan.Syntax.Concrete.Glyph qualified as P
import Mikan.Syntax.Position
import Mikan.Syntax.Common
import Mikan.Syntax.Literal
import Mikan.Syntax.Abstract.Name
import Mikan.Syntax.Common.Pretty

import Mikan.Syntax.Internal.Blockers
import Mikan.Syntax.Internal.Elim
import Mikan.Syntax.Internal.Univ
import Mikan.Syntax.Internal.Dom

import Mikan.Utils.CallStack
    ( CallStack
    , HasCallStack
    , prettyCallSite
    , headCallSite
    , withCallerCallStack
    )

import Mikan.Utils.MinimalArray.Lifted qualified as AL
import Mikan.Utils.CompactRegion qualified as Compact
import Mikan.Utils.Function
import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.List1 (List1)
import Mikan.Utils.Null

import Mikan.Utils.Impossible

-- | Type of argument lists.
--
type Args       = [Arg Term]
type NamedArgs  = [NamedArg Term]
type Args1      = List1 (Arg Term)
type NamedArgs1 = List1 (NamedArg Term)
type Elim       = Elim' Term
type Elims      = [Elim]
type Dom        = Dom' Term

type ConInfo = ConOrigin

-- | A 'Term' in internal syntax.
--
-- Mikan's internal syntax represents terms in beta-normal form, meaning
-- that it is impossible to represent something like @(λ x → x) t@.
-- However, terms are not "delta"-normalised, and applications of
-- defined constants that may yet reduce can be represented by the 'Def'
-- constructor.
data Term
  = Var' {-# UNPACK #-} !Int Elims
  -- ^ Internal representation of (unshared) term variables; see 'Var'.

  | Lam ArgInfo (Abs Term)
    -- ^ Lambda abstraction. The 'ArgInfo' records the visibility.

  | Def QName Elims
    -- ^ Elimination of a defined name, which may be a redex.

  | Con ConHead ConInfo Elims
    -- ^ Application of a defined constructor. The 'Elims' should consist
    -- only of 'Apply' or 'IApply' elims.
    --
    -- If the constructor has a boundary, a 'Con' term may be a redex.

  | MetaV {-# UNPACK #-} !MetaId Elims
    -- ^ Elimination from a metavariable. The metavariable may be open or
    -- solved, local or remote.

  | Pi (Dom Type) (Abs Type)
    -- ^ Dependent or non-dependent function type, controlled by the
    -- 'Abs'.

  | Lit Literal -- ^ Embedding of 'Literal's.
  | Sort Sort   -- ^ Embedding of 'Sort's.
  | Level Level -- ^ Embedding of universe 'Level's.

  | DontCare Term
    -- ^ Terms containing irrelevant (i.e. @Prop@-sorted) stuff.
    --
    -- 'DontCare' wrappers are added by the elaborator, and they
    -- indicate to term traversals that whatever is inside does not
    -- matter for definitional equality.

  | Dummy DummyTermKind Elims
    -- ^ A (part of a) term or type which is only used for internal
    -- purposes.
    --
    -- The 'DummyTermKind' describes why this dummy was created;
    -- typically, it is a string describing the source location that
    -- created it, but dummy terms are also used when *leaving* the type
    -- checker (through reification) to convey out-of-band information.
    --
    -- The second field accumulates eliminations in case we apply a
    -- dummy term to more of them. Dummy terms should never be used in
    -- places where they can affect type checking, so syntactic checks
    -- are free to ignore the eliminations, which are only there to ease
    -- debugging when a dummy term incorrectly leaks into a relevant
    -- position.
  deriving Int -> Term -> ShowS
[Term] -> ShowS
Term -> [Char]
(Int -> Term -> ShowS)
-> (Term -> [Char]) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Term -> ShowS
showsPrec :: Int -> Term -> ShowS
$cshow :: Term -> [Char]
show :: Term -> [Char]
$cshowList :: [Term] -> ShowS
showList :: [Term] -> ShowS
Show

instance Suggest Term where
  suggestName :: Term -> Maybe ShortText
suggestName (Lam ArgInfo
_ Abs Term
v) = Abs Term -> Maybe ShortText
forall a. Suggest a => a -> Maybe ShortText
suggestName Abs Term
v
  suggestName Term
_         = Maybe ShortText
forall a. Maybe a
Nothing

-- Caching small variables
--------------------------------------------------------------------------------

-- | A lifted array of globally-shared 'Term' variables with no
-- eliminations.
--
-- Variables with de Bruijn index less than 'varTableSize' should be
-- drawn from this table instead of constructed. This is handled
-- automatically by the 'Var' pattern synonym and 'var' smart
-- constructor.
{-# NOINLINE varTable #-}
varTable :: AL.Array Term
varTable :: Array Term
varTable = Word -> Array Term -> Array Term
forall a. Word -> a -> a
Compact.compact Word
4096 (Array Term -> Array Term) -> Array Term -> Array Term
forall a b. (a -> b) -> a -> b
$
  [Term] -> Array Term
forall a. [a] -> Array a
AL.fromList [Int -> Elims -> Term
Var' Int
i [] | Int
i <- [Int
0..(Int
varTableSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]]

-- | Neutral elimnation of a variable in the context (represented by its
-- de Bruijn index).
--
-- Term variables with no eliminations are globally cached in a shared
-- compacted array, which allows them to be pointer-equal; this is the
-- 'varTable'.
pattern Var :: Int -> Elims -> Term
pattern $bVar :: Int -> Elims -> Term
$mVar :: forall {r}. Term -> (Int -> Elims -> r) -> ((# #) -> r) -> r
Var i es <- Var' i es where
  Var Int
i Elims
es = case Elims
es of
    [] -> case Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
varTableSize of
      Bool
True -> Array Term -> Int -> Term
forall a. Array a -> Int -> a
AL.unsafeIndex Array Term
varTable Int
i
      Bool
_    -> Int -> Elims -> Term
Var' Int
i Elims
es
    Elims
_  -> Int -> Elims -> Term
Var' Int
i Elims
es
{-# INLINE Var #-}
{-# COMPLETE Var, Lam, Lit, Def, Con, Pi, Sort, Level, MetaV, DontCare, Dummy #-}

{-# INLINE varTableSize #-}
varTableSize :: Int
varTableSize :: Int
varTableSize = Int
128

{-# INLINE CONLIKE unsharedVar #-}
-- | Create a neutral elimnation of a variable without
-- going through the global variable cache.
--
-- The main use of 'unsharedVar' is when you know statically
-- that a variable *must* have eliminations.
unsharedVar :: Nat -> Elims -> Term
unsharedVar :: Int -> Elims -> Term
unsharedVar = Int -> Elims -> Term
Var'

-- | An unapplied variable.
var :: Nat -> Term
var :: Int -> Term
var Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = case Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
varTableSize of
    Bool
True -> Array Term -> Int -> Term
forall a. Array a -> Int -> a
AL.unsafeIndex Array Term
varTable Int
i
    Bool
_    -> Int -> Elims -> Term
Var' Int
i []
  | Bool
otherwise = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Add an outer 'DontCare' only if the given 'Term' is not already a
-- @DontCare@.
dontCare :: Term -> Term
dontCare :: Term -> Term
dontCare Term
v = case Term
v of
  DontCare{} -> Term
v
  Term
_          -> Term -> Term
DontCare Term
v

-- | Removing a topmost 'DontCare' constructor.
stripDontCare :: Term -> Term
stripDontCare :: Term -> Term
stripDontCare = \case
  DontCare Term
v -> Term
v
  Term
v          -> Term
v

--------------------------------------------------------------------------
-- * Types and sorts
---------------------------------------------------------------------------

data Type'' t a = El { forall t a. Type'' t a -> Sort' t
_getSort :: Sort' t, forall t a. Type'' t a -> a
unEl :: a }
  deriving (Int -> Type'' t a -> ShowS
[Type'' t a] -> ShowS
Type'' t a -> [Char]
(Int -> Type'' t a -> ShowS)
-> (Type'' t a -> [Char])
-> ([Type'' t a] -> ShowS)
-> Show (Type'' t a)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
forall t a. (Show t, Show a) => Type'' t a -> [Char]
$cshowsPrec :: forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
showsPrec :: Int -> Type'' t a -> ShowS
$cshow :: forall t a. (Show t, Show a) => Type'' t a -> [Char]
show :: Type'' t a -> [Char]
$cshowList :: forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
showList :: [Type'' t a] -> ShowS
Show, (forall a b. (a -> b) -> Type'' t a -> Type'' t b)
-> (forall a b. a -> Type'' t b -> Type'' t a)
-> Functor (Type'' t)
forall a b. a -> Type'' t b -> Type'' t a
forall a b. (a -> b) -> Type'' t a -> Type'' t b
forall t a b. a -> Type'' t b -> Type'' t a
forall t a b. (a -> b) -> Type'' t a -> Type'' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t a b. (a -> b) -> Type'' t a -> Type'' t b
fmap :: forall a b. (a -> b) -> Type'' t a -> Type'' t b
$c<$ :: forall t a b. a -> Type'' t b -> Type'' t a
<$ :: forall a b. a -> Type'' t b -> Type'' t a
Functor, (forall m. Monoid m => Type'' t m -> m)
-> (forall m a. Monoid m => (a -> m) -> Type'' t a -> m)
-> (forall m a. Monoid m => (a -> m) -> Type'' t a -> m)
-> (forall a b. (a -> b -> b) -> b -> Type'' t a -> b)
-> (forall a b. (a -> b -> b) -> b -> Type'' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type'' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type'' t a -> b)
-> (forall a. (a -> a -> a) -> Type'' t a -> a)
-> (forall a. (a -> a -> a) -> Type'' t a -> a)
-> (forall a. Type'' t a -> [a])
-> (forall a. Type'' t a -> Bool)
-> (forall a. Type'' t a -> Int)
-> (forall a. Eq a => a -> Type'' t a -> Bool)
-> (forall a. Ord a => Type'' t a -> a)
-> (forall a. Ord a => Type'' t a -> a)
-> (forall a. Num a => Type'' t a -> a)
-> (forall a. Num a => Type'' t a -> a)
-> Foldable (Type'' t)
forall a. Eq a => a -> Type'' t a -> Bool
forall a. Num a => Type'' t a -> a
forall a. Ord a => Type'' t a -> a
forall m. Monoid m => Type'' t m -> m
forall a. Type'' t a -> Bool
forall a. Type'' t a -> Int
forall a. Type'' t a -> [a]
forall a. (a -> a -> a) -> Type'' t a -> a
forall t a. Eq a => a -> Type'' t a -> Bool
forall t a. Num a => Type'' t a -> a
forall t a. Ord a => Type'' t a -> a
forall m a. Monoid m => (a -> m) -> Type'' t a -> m
forall t m. Monoid m => Type'' t m -> m
forall t a. Type'' t a -> Bool
forall t a. Type'' t a -> Int
forall t a. Type'' t a -> [a]
forall b a. (b -> a -> b) -> b -> Type'' t a -> b
forall a b. (a -> b -> b) -> b -> Type'' t a -> b
forall t a. (a -> a -> a) -> Type'' t a -> a
forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall t m. Monoid m => Type'' t m -> m
fold :: forall m. Monoid m => Type'' t m -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
$cfoldr1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Type'' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
foldl1 :: forall a. (a -> a -> a) -> Type'' t a -> a
$ctoList :: forall t a. Type'' t a -> [a]
toList :: forall a. Type'' t a -> [a]
$cnull :: forall t a. Type'' t a -> Bool
null :: forall a. Type'' t a -> Bool
$clength :: forall t a. Type'' t a -> Int
length :: forall a. Type'' t a -> Int
$celem :: forall t a. Eq a => a -> Type'' t a -> Bool
elem :: forall a. Eq a => a -> Type'' t a -> Bool
$cmaximum :: forall t a. Ord a => Type'' t a -> a
maximum :: forall a. Ord a => Type'' t a -> a
$cminimum :: forall t a. Ord a => Type'' t a -> a
minimum :: forall a. Ord a => Type'' t a -> a
$csum :: forall t a. Num a => Type'' t a -> a
sum :: forall a. Num a => Type'' t a -> a
$cproduct :: forall t a. Num a => Type'' t a -> a
product :: forall a. Num a => Type'' t a -> a
Foldable, Functor (Type'' t)
Foldable (Type'' t)
(Functor (Type'' t), Foldable (Type'' t)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Type'' t a -> f (Type'' t b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Type'' t (f a) -> f (Type'' t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type'' t a -> m (Type'' t b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Type'' t (m a) -> m (Type'' t a))
-> Traversable (Type'' t)
forall t. Functor (Type'' t)
forall t. Foldable (Type'' t)
forall t (m :: * -> *) a.
Monad m =>
Type'' t (m a) -> m (Type'' t a)
forall t (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
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 => Type'' t (m a) -> m (Type'' t a)
forall (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
$csequence :: forall t (m :: * -> *) a.
Monad m =>
Type'' t (m a) -> m (Type'' t a)
sequence :: forall (m :: * -> *) a. Monad m => Type'' t (m a) -> m (Type'' t a)
Traversable)

type Type' a = Type'' Term a
type Type = Type' Term

instance Decoration (Type'' t) where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
traverseF a -> m b
f (El Sort' t
s a
a) = Sort' t -> b -> Type'' t b
forall t a. Sort' t -> a -> Type'' t a
El Sort' t
s (b -> Type'' t b) -> m b -> m (Type'' t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a

class LensSort a where
  lensSort :: Lens' a Sort

  getSort  :: a -> Sort
  getSort a
a = a
a a -> Getting Sort a Sort -> Sort
forall s a. s -> Getting a s a -> a
^. Getting Sort a Sort
forall a. LensSort a => Lens' a Sort
Lens' a Sort
lensSort

  default lensSort :: (a ~ f x, Decoration f, LensSort x) => Lens' a Sort
  lensSort = (x -> f x) -> a -> f a
(x -> f x) -> f x -> f (f x)
forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Functor m => (a -> m b) -> f a -> m (f b)
traverseF ((x -> f x) -> a -> f a)
-> ((Sort -> f Sort) -> x -> f x) -> (Sort -> f Sort) -> a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> f Sort) -> x -> f x
forall a. LensSort a => Lens' a Sort
Lens' x Sort
lensSort
  {-# INLINE lensSort #-}

instance LensSort Sort where
  lensSort :: Lens' Sort Sort
lensSort = (Sort -> f Sort) -> Sort -> f Sort
forall a. a -> a
id
  {-# INLINE lensSort #-}

instance LensSort (Type' a) where
  lensSort :: Lens' (Type' a) Sort
lensSort Sort -> f Sort
f (El Sort
s a
a) = Sort -> f Sort
f Sort
s f Sort -> (Sort -> Type' a) -> f (Type' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Sort
s' -> Sort -> a -> Type' a
forall t a. Sort' t -> a -> Type'' t a
El Sort
s' a
a
  {-# INLINE lensSort #-}

instance LensSort a => LensSort (Dom a)
instance LensSort a => LensSort (Arg a)

-- | Sorts.
--
-- The three sort constructors 'MetaS', 'DefS' and 'DummyS' are the sort
-- equivalents of the term constructors 'Meta', 'Def' and 'Dummy'.
data Sort' t
  = Univ Univ (Level' t)
    -- ^ @Prop ℓ@, @Type ℓ@, @SSet ℓ@.
  | Inf Univ !Integer
    -- ^ @Propωᵢ@, @Typeωᵢ@, @SSetωᵢ@.
  | LevelUniv
    -- ^ @LevelUniv@, a sort inhabited by type @Level@.
    --
    -- When @--level-universe@ isn't on, this universe /reduces/ to
    -- @'Univ' 'UType' ('ClosedLevel' 0)@.
  | IntervalUniv
    -- ^ @IntervalUniv@, a sort inhabited by the cubical interval.
  | CofUniv
    -- ^ @CofUniv@, a sort inhabited by the @IsOne@ predicate.
    --
    -- @'CofUniv'@ is definitionally irrelevant and small (like @'Univ'
    -- 'UProp'@), but non-fibrant.
  | PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))
    -- ^ Sort of a pi type, as a function of the sort of its domain and
    -- the sort of its codomain (which may depend on the domain).
  | FunSort (Sort' t) (Sort' t)
    -- ^ Sort of a (non-dependent) function type.
  | UnivSort (Sort' t)
    -- ^ Sort of another sort.
  | MetaS {-# UNPACK #-} !MetaId [Elim' t]
    -- ^ An unsolved sort metavariable.
  | DefS QName [Elim' t]
    -- ^ A postulated sort, used for unsolved sort metavariables left
    -- open in a module checked with @--allow-unsolved-metas@.
  | DummyS String
    -- ^ A dummy sort, like a 'Dummy' 'Term'.
    --
    -- The 'String' typically describes where this dummy was created.
    -- Use the '__DUMMY_SORT__' macro.
  deriving Int -> Sort' t -> ShowS
[Sort' t] -> ShowS
Sort' t -> [Char]
(Int -> Sort' t -> ShowS)
-> (Sort' t -> [Char]) -> ([Sort' t] -> ShowS) -> Show (Sort' t)
forall t. Show t => Int -> Sort' t -> ShowS
forall t. Show t => [Sort' t] -> ShowS
forall t. Show t => Sort' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Sort' t -> ShowS
showsPrec :: Int -> Sort' t -> ShowS
$cshow :: forall t. Show t => Sort' t -> [Char]
show :: Sort' t -> [Char]
$cshowList :: forall t. Show t => [Sort' t] -> ShowS
showList :: [Sort' t] -> ShowS
Show

pattern Prop, Type, SSet :: Level' t -> Sort' t
pattern $bProp :: forall t. Level' t -> Sort' t
$mProp :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
Prop l = Univ UProp l
pattern $bType :: forall t. Level' t -> Sort' t
$mType :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
Type l = Univ UType l
pattern $bSSet :: forall t. Level' t -> Sort' t
$mSSet :: forall {r} {t}. Sort' t -> (Level' t -> r) -> ((# #) -> r) -> r
SSet l = Univ USSet l

{-# COMPLETE
  Prop, Type, SSet, Inf,
  LevelUniv, IntervalUniv, CofUniv,
  PiSort, FunSort, UnivSort, MetaS, DefS, DummyS #-}

type Sort = Sort' Term

isSort :: Term -> Maybe Sort
isSort :: Term -> Maybe Sort
isSort = \case
  Sort Sort
s -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
  Term
_      -> Maybe Sort
forall a. Maybe a
Nothing

-- | Get the flavor of the universe. 'Nothing' could also mean "don't know".
sortUniv :: Sort' t -> Maybe Univ
sortUniv :: forall t. Sort' t -> Maybe Univ
sortUniv = \case
  Univ Univ
u Level' t
_ -> Univ -> Maybe Univ
forall a. a -> Maybe a
Just Univ
u
  Inf  Univ
u Integer
_ -> Univ -> Maybe Univ
forall a. a -> Maybe a
Just Univ
u
  Sort' t
_        -> Maybe Univ
forall a. Maybe a
Nothing

-- | Is this a universe of definitionally irrelevant types?
-- Answers are yes ('True') or maybe ('False').
isProp :: Sort' t -> Bool
isProp :: forall t. Sort' t -> Bool
isProp = \case
  Univ Univ
u Level' t
_     -> Univ
UProp Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u
  Inf Univ
u  Integer
_     -> Univ
UProp Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u
  Sort' t
CofUniv      -> Bool
True
  Sort' t
LevelUniv    -> Bool
False
  Sort' t
IntervalUniv -> Bool
False
  PiSort{}     -> Bool
False
  UnivSort{}   -> Bool
False
  FunSort{}    -> Bool
False
  MetaS{}      -> Bool
False
  DefS{}       -> Bool
False
  DummyS{}     -> Bool
False

-- | Is this a strict universe inhabitable by data types?
isStrictDataSort :: Sort' t -> Bool
isStrictDataSort :: forall t. Sort' t -> Bool
isStrictDataSort = Bool -> (Univ -> Bool) -> Maybe Univ -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((IsFibrant
IsStrict IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
==) (IsFibrant -> Bool) -> (Univ -> IsFibrant) -> Univ -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Univ -> IsFibrant
univFibrancy) (Maybe Univ -> Bool) -> (Sort' t -> Maybe Univ) -> Sort' t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' t -> Maybe Univ
forall t. Sort' t -> Maybe Univ
sortUniv

-- | Turn a known 'UProp' sort into a 'UType' sort, leave others unchanged.
propToType :: Sort' t -> Sort' t
propToType :: forall t. Sort' t -> Sort' t
propToType = \case
  Univ Univ
UProp Level' t
l -> Univ -> Level' t -> Sort' t
forall t. Univ -> Level' t -> Sort' t
Univ Univ
UType Level' t
l
  Inf  Univ
UProp Integer
l -> Univ -> Integer -> Sort' t
forall t. Univ -> Integer -> Sort' t
Inf  Univ
UType Integer
l
  Sort' t
s -> Sort' t
s

varSort :: Int -> Sort
varSort :: Int -> Sort
varSort Int
n = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel (Term -> Level) -> Term -> Level
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
n

tmSort :: Term -> Sort
tmSort :: Term -> Sort
tmSort Term
t = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel Term
t

tmSSort :: Term -> Sort
tmSSort :: Term -> Sort
tmSSort Term
t = Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel Term
t

mkType :: Integer -> Sort
mkType :: Integer -> Sort
mkType Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n

mkProp :: Integer -> Sort
mkProp :: Integer -> Sort
mkProp Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n

mkSSet :: Integer -> Sort
mkSSet :: Integer -> Sort
mkSSet Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n

---------------------------------------------------------------------------
-- * Universe levels
---------------------------------------------------------------------------

-- | A level is a maximum expression of a closed level and 0..n
--   'PlusLevel' expressions each of which is an atom plus a number.
data Level' t = Max !Integer [PlusLevel' t]
  deriving (Int -> Level' t -> ShowS
[Level' t] -> ShowS
Level' t -> [Char]
(Int -> Level' t -> ShowS)
-> (Level' t -> [Char]) -> ([Level' t] -> ShowS) -> Show (Level' t)
forall t. Show t => Int -> Level' t -> ShowS
forall t. Show t => [Level' t] -> ShowS
forall t. Show t => Level' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Level' t -> ShowS
showsPrec :: Int -> Level' t -> ShowS
$cshow :: forall t. Show t => Level' t -> [Char]
show :: Level' t -> [Char]
$cshowList :: forall t. Show t => [Level' t] -> ShowS
showList :: [Level' t] -> ShowS
Show, (forall a b. (a -> b) -> Level' a -> Level' b)
-> (forall a b. a -> Level' b -> Level' a) -> Functor Level'
forall a b. a -> Level' b -> Level' a
forall a b. (a -> b) -> Level' a -> Level' 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) -> Level' a -> Level' b
fmap :: forall a b. (a -> b) -> Level' a -> Level' b
$c<$ :: forall a b. a -> Level' b -> Level' a
<$ :: forall a b. a -> Level' b -> Level' a
Functor, (forall m. Monoid m => Level' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Level' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Level' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Level' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Level' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Level' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Level' a -> b)
-> (forall a. (a -> a -> a) -> Level' a -> a)
-> (forall a. (a -> a -> a) -> Level' a -> a)
-> (forall a. Level' a -> [a])
-> (forall a. Level' a -> Bool)
-> (forall a. Level' a -> Int)
-> (forall a. Eq a => a -> Level' a -> Bool)
-> (forall a. Ord a => Level' a -> a)
-> (forall a. Ord a => Level' a -> a)
-> (forall a. Num a => Level' a -> a)
-> (forall a. Num a => Level' a -> a)
-> Foldable Level'
forall a. Eq a => a -> Level' a -> Bool
forall a. Num a => Level' a -> a
forall a. Ord a => Level' a -> a
forall m. Monoid m => Level' m -> m
forall a. Level' a -> Bool
forall a. Level' a -> Int
forall a. Level' a -> [a]
forall a. (a -> a -> a) -> Level' a -> a
forall m a. Monoid m => (a -> m) -> Level' a -> m
forall b a. (b -> a -> b) -> b -> Level' a -> b
forall a b. (a -> b -> b) -> b -> Level' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Level' m -> m
fold :: forall m. Monoid m => Level' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Level' a -> a
foldr1 :: forall a. (a -> a -> a) -> Level' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Level' a -> a
foldl1 :: forall a. (a -> a -> a) -> Level' a -> a
$ctoList :: forall a. Level' a -> [a]
toList :: forall a. Level' a -> [a]
$cnull :: forall a. Level' a -> Bool
null :: forall a. Level' a -> Bool
$clength :: forall a. Level' a -> Int
length :: forall a. Level' a -> Int
$celem :: forall a. Eq a => a -> Level' a -> Bool
elem :: forall a. Eq a => a -> Level' a -> Bool
$cmaximum :: forall a. Ord a => Level' a -> a
maximum :: forall a. Ord a => Level' a -> a
$cminimum :: forall a. Ord a => Level' a -> a
minimum :: forall a. Ord a => Level' a -> a
$csum :: forall a. Num a => Level' a -> a
sum :: forall a. Num a => Level' a -> a
$cproduct :: forall a. Num a => Level' a -> a
product :: forall a. Num a => Level' a -> a
Foldable, Functor Level'
Foldable Level'
(Functor Level', Foldable Level') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Level' a -> f (Level' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Level' (f a) -> f (Level' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Level' a -> m (Level' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Level' (m a) -> m (Level' a))
-> Traversable Level'
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 => Level' (m a) -> m (Level' a)
forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
$csequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
sequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
Traversable)

type Level = Level' Term

data PlusLevel' t = Plus !Integer t
  deriving (Int -> PlusLevel' t -> ShowS
[PlusLevel' t] -> ShowS
PlusLevel' t -> [Char]
(Int -> PlusLevel' t -> ShowS)
-> (PlusLevel' t -> [Char])
-> ([PlusLevel' t] -> ShowS)
-> Show (PlusLevel' t)
forall t. Show t => Int -> PlusLevel' t -> ShowS
forall t. Show t => [PlusLevel' t] -> ShowS
forall t. Show t => PlusLevel' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> PlusLevel' t -> ShowS
showsPrec :: Int -> PlusLevel' t -> ShowS
$cshow :: forall t. Show t => PlusLevel' t -> [Char]
show :: PlusLevel' t -> [Char]
$cshowList :: forall t. Show t => [PlusLevel' t] -> ShowS
showList :: [PlusLevel' t] -> ShowS
Show, (forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' b)
-> (forall a b. a -> PlusLevel' b -> PlusLevel' a)
-> Functor PlusLevel'
forall a b. a -> PlusLevel' b -> PlusLevel' a
forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' 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) -> PlusLevel' a -> PlusLevel' b
fmap :: forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' b
$c<$ :: forall a b. a -> PlusLevel' b -> PlusLevel' a
<$ :: forall a b. a -> PlusLevel' b -> PlusLevel' a
Functor, (forall m. Monoid m => PlusLevel' m -> m)
-> (forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m)
-> (forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m)
-> (forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b)
-> (forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b)
-> (forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b)
-> (forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b)
-> (forall a. (a -> a -> a) -> PlusLevel' a -> a)
-> (forall a. (a -> a -> a) -> PlusLevel' a -> a)
-> (forall a. PlusLevel' a -> [a])
-> (forall a. PlusLevel' a -> Bool)
-> (forall a. PlusLevel' a -> Int)
-> (forall a. Eq a => a -> PlusLevel' a -> Bool)
-> (forall a. Ord a => PlusLevel' a -> a)
-> (forall a. Ord a => PlusLevel' a -> a)
-> (forall a. Num a => PlusLevel' a -> a)
-> (forall a. Num a => PlusLevel' a -> a)
-> Foldable PlusLevel'
forall a. Eq a => a -> PlusLevel' a -> Bool
forall a. Num a => PlusLevel' a -> a
forall a. Ord a => PlusLevel' a -> a
forall m. Monoid m => PlusLevel' m -> m
forall a. PlusLevel' a -> Bool
forall a. PlusLevel' a -> Int
forall a. PlusLevel' a -> [a]
forall a. (a -> a -> a) -> PlusLevel' a -> a
forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => PlusLevel' m -> m
fold :: forall m. Monoid m => PlusLevel' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
foldr1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
foldl1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
$ctoList :: forall a. PlusLevel' a -> [a]
toList :: forall a. PlusLevel' a -> [a]
$cnull :: forall a. PlusLevel' a -> Bool
null :: forall a. PlusLevel' a -> Bool
$clength :: forall a. PlusLevel' a -> Int
length :: forall a. PlusLevel' a -> Int
$celem :: forall a. Eq a => a -> PlusLevel' a -> Bool
elem :: forall a. Eq a => a -> PlusLevel' a -> Bool
$cmaximum :: forall a. Ord a => PlusLevel' a -> a
maximum :: forall a. Ord a => PlusLevel' a -> a
$cminimum :: forall a. Ord a => PlusLevel' a -> a
minimum :: forall a. Ord a => PlusLevel' a -> a
$csum :: forall a. Num a => PlusLevel' a -> a
sum :: forall a. Num a => PlusLevel' a -> a
$cproduct :: forall a. Num a => PlusLevel' a -> a
product :: forall a. Num a => PlusLevel' a -> a
Foldable, Functor PlusLevel'
Foldable PlusLevel'
(Functor PlusLevel', Foldable PlusLevel') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> PlusLevel' a -> f (PlusLevel' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    PlusLevel' (f a) -> f (PlusLevel' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> PlusLevel' a -> m (PlusLevel' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    PlusLevel' (m a) -> m (PlusLevel' a))
-> Traversable PlusLevel'
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 =>
PlusLevel' (m a) -> m (PlusLevel' a)
forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
PlusLevel' (m a) -> m (PlusLevel' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
PlusLevel' (m a) -> m (PlusLevel' a)
Traversable)

type PlusLevel = PlusLevel' Term
type LevelAtom = Term

-- | Constant level @n@
pattern ClosedLevel :: Integer -> Level
pattern $bClosedLevel :: Integer -> Level
$mClosedLevel :: forall {r}. Level -> (Integer -> r) -> ((# #) -> r) -> r
ClosedLevel n = Max n []

atomicLevel :: t -> Level' t
atomicLevel :: forall t. t -> Level' t
atomicLevel t
a = Integer -> [PlusLevel' t] -> Level' t
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [ Integer -> t -> PlusLevel' t
forall t. Integer -> t -> PlusLevel' t
Plus Integer
0 t
a ]

-- | Given a constant @m@ and level @l@, compute @m + l@
levelPlus :: Integer -> Level -> Level
levelPlus :: Integer -> Level -> Level
levelPlus Integer
m (Max Integer
n [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ (PlusLevel' Term -> PlusLevel' Term)
-> [PlusLevel' Term] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map' PlusLevel' Term -> PlusLevel' Term
pplus [PlusLevel' Term]
as
  where pplus :: PlusLevel' Term -> PlusLevel' Term
pplus (Plus Integer
n Term
l) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) Term
l

levelSuc :: Level -> Level
levelSuc :: Level -> Level
levelSuc = Integer -> Level -> Level
levelPlus Integer
1

---------------------------------------------------------------------------
-- * Blocked Terms
---------------------------------------------------------------------------

type Blocked    = Blocked' Term
type NotBlocked = NotBlocked' Term

-- | @'Mikan.Syntax.Internal.Term.Blocked'' a@ without the @a@.
type Blocked_ = Blocked ()

-----------------------------------------------------------------------------
-- * Explicit substitutions
-----------------------------------------------------------------------------

-- | Substitutions.
data Substitution' a

  = IdS
    -- ^ Identity substitution.
    --
    -- @
    --   Γ ⊢ IdS : Γ
    -- @

  | EmptyS Impossible
    -- ^ Empty substitution, lifts from the empty context. Apply this to
    -- closed terms you want to use in a non-empty context.
    --
    -- @
    --   Γ ⊢ EmptyS : ()
    -- @
    --
    -- The 'Impossible' argument stores where this substitution was
    -- created. It is used for reporting an internal error when applying
    -- this substitution to a term that was not actually closed.

  | a :# !(Substitution' a)
    -- ^ Substitution extension, "cons".
    --
    -- @
    --   Γ ⊢ u : Aρ  Γ ⊢ ρ : Δ
    --   ---------------------
    --     Γ ⊢ u :# ρ : Δ, A
    -- @

  | Strengthen Impossible !Int !(Substitution' a)
    -- ^ Strengthening substitution. In @'Strengthen' err n ρ@, the
    -- number @n@ must be non-negative. This substitution should only be
    -- applied to values @t@ for which none of the variables @0@ up to
    -- @n - 1@ are free in @t[ρ]@, and in that case @n@ is subtracted
    -- from all free de Bruijn indices in @t[ρ]@.
    --
    -- @
    --       Γ ⊢ ρ : Δ   |Θ| = n
    --   ---------------------------
    --    Γ ⊢ Strengthen n ρ : Δ, Θ
    -- @
    --
    -- The 'Impossible' argument stores where this substitution was
    -- created. It is used for reporting an internal error when applying
    -- this substitution to a term that mentions a variable @j <= n@.

  | Wk !Int !(Substitution' a)
    -- ^ Weakening substitution, lifts to an extended context.
    --
    -- @
    --        Γ ⊢ ρ : Δ
    --   -------------------
    --   Γ, Ψ ⊢ Wk |Ψ| ρ : Δ
    -- @


  | Lift !Int !(Substitution' a)
    -- ^ Lifting substitution. Use this to go under a binder.
    --   @Lift 1 ρ == var 0 :# Wk 1 ρ@.
    --
    -- @
    --           Γ ⊢ ρ : Δ
    --   -------------------------
    --   Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
    -- @

  deriving ( Int -> Substitution' a -> ShowS
[Substitution' a] -> ShowS
Substitution' a -> [Char]
(Int -> Substitution' a -> ShowS)
-> (Substitution' a -> [Char])
-> ([Substitution' a] -> ShowS)
-> Show (Substitution' a)
forall a. Show a => Int -> Substitution' a -> ShowS
forall a. Show a => [Substitution' a] -> ShowS
forall a. Show a => Substitution' a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Substitution' a -> ShowS
showsPrec :: Int -> Substitution' a -> ShowS
$cshow :: forall a. Show a => Substitution' a -> [Char]
show :: Substitution' a -> [Char]
$cshowList :: forall a. Show a => [Substitution' a] -> ShowS
showList :: [Substitution' a] -> ShowS
Show
           , (forall a b. (a -> b) -> Substitution' a -> Substitution' b)
-> (forall a b. a -> Substitution' b -> Substitution' a)
-> Functor Substitution'
forall a b. a -> Substitution' b -> Substitution' a
forall a b. (a -> b) -> Substitution' a -> Substitution' 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) -> Substitution' a -> Substitution' b
fmap :: forall a b. (a -> b) -> Substitution' a -> Substitution' b
$c<$ :: forall a b. a -> Substitution' b -> Substitution' a
<$ :: forall a b. a -> Substitution' b -> Substitution' a
Functor
           , (forall m. Monoid m => Substitution' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Substitution' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Substitution' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Substitution' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Substitution' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Substitution' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Substitution' a -> b)
-> (forall a. (a -> a -> a) -> Substitution' a -> a)
-> (forall a. (a -> a -> a) -> Substitution' a -> a)
-> (forall a. Substitution' a -> [a])
-> (forall a. Substitution' a -> Bool)
-> (forall a. Substitution' a -> Int)
-> (forall a. Eq a => a -> Substitution' a -> Bool)
-> (forall a. Ord a => Substitution' a -> a)
-> (forall a. Ord a => Substitution' a -> a)
-> (forall a. Num a => Substitution' a -> a)
-> (forall a. Num a => Substitution' a -> a)
-> Foldable Substitution'
forall a. Eq a => a -> Substitution' a -> Bool
forall a. Num a => Substitution' a -> a
forall a. Ord a => Substitution' a -> a
forall m. Monoid m => Substitution' m -> m
forall a. Substitution' a -> Bool
forall a. Substitution' a -> Int
forall a. Substitution' a -> [a]
forall a. (a -> a -> a) -> Substitution' a -> a
forall m a. Monoid m => (a -> m) -> Substitution' a -> m
forall b a. (b -> a -> b) -> b -> Substitution' a -> b
forall a b. (a -> b -> b) -> b -> Substitution' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Substitution' m -> m
fold :: forall m. Monoid m => Substitution' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
foldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
foldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
$ctoList :: forall a. Substitution' a -> [a]
toList :: forall a. Substitution' a -> [a]
$cnull :: forall a. Substitution' a -> Bool
null :: forall a. Substitution' a -> Bool
$clength :: forall a. Substitution' a -> Int
length :: forall a. Substitution' a -> Int
$celem :: forall a. Eq a => a -> Substitution' a -> Bool
elem :: forall a. Eq a => a -> Substitution' a -> Bool
$cmaximum :: forall a. Ord a => Substitution' a -> a
maximum :: forall a. Ord a => Substitution' a -> a
$cminimum :: forall a. Ord a => Substitution' a -> a
minimum :: forall a. Ord a => Substitution' a -> a
$csum :: forall a. Num a => Substitution' a -> a
sum :: forall a. Num a => Substitution' a -> a
$cproduct :: forall a. Num a => Substitution' a -> a
product :: forall a. Num a => Substitution' a -> a
Foldable
           , Functor Substitution'
Foldable Substitution'
(Functor Substitution', Foldable Substitution') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Substitution' a -> f (Substitution' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Substitution' (f a) -> f (Substitution' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Substitution' a -> m (Substitution' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Substitution' (m a) -> m (Substitution' a))
-> Traversable Substitution'
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 =>
Substitution' (m a) -> m (Substitution' a)
forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Substitution' (m a) -> m (Substitution' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Substitution' (m a) -> m (Substitution' a)
Traversable
           , (forall x. Substitution' a -> Rep (Substitution' a) x)
-> (forall x. Rep (Substitution' a) x -> Substitution' a)
-> Generic (Substitution' a)
forall x. Rep (Substitution' a) x -> Substitution' a
forall x. Substitution' a -> Rep (Substitution' a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Substitution' a) x -> Substitution' a
forall a x. Substitution' a -> Rep (Substitution' a) x
$cfrom :: forall a x. Substitution' a -> Rep (Substitution' a) x
from :: forall x. Substitution' a -> Rep (Substitution' a) x
$cto :: forall a x. Rep (Substitution' a) x -> Substitution' a
to :: forall x. Rep (Substitution' a) x -> Substitution' a
Generic
           )

type Substitution = Substitution' Term
type Renaming = Substitution' Nat

infixr 4 :#

instance Null (Substitution' a) where
  empty :: Substitution' a
empty = Substitution' a
forall a. Substitution' a
IdS
  null :: Substitution' a -> Bool
null Substitution' a
IdS = Bool
True
  null Substitution' a
_   = Bool
False

-- | Wrapper for types that do not contain variables (so applying a substitution is the identity).
--   Useful if you have a structure of types that support substitution mixed with types that don't
--   and need to apply a substitution to the full structure.
newtype NoSubst t a = NoSubst { forall t a. NoSubst t a -> a
unNoSubst :: a }
  deriving ((forall x. NoSubst t a -> Rep (NoSubst t a) x)
-> (forall x. Rep (NoSubst t a) x -> NoSubst t a)
-> Generic (NoSubst t a)
forall x. Rep (NoSubst t a) x -> NoSubst t a
forall x. NoSubst t a -> Rep (NoSubst t a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t a x. Rep (NoSubst t a) x -> NoSubst t a
forall t a x. NoSubst t a -> Rep (NoSubst t a) x
$cfrom :: forall t a x. NoSubst t a -> Rep (NoSubst t a) x
from :: forall x. NoSubst t a -> Rep (NoSubst t a) x
$cto :: forall t a x. Rep (NoSubst t a) x -> NoSubst t a
to :: forall x. Rep (NoSubst t a) x -> NoSubst t a
Generic, NoSubst t a -> ()
(NoSubst t a -> ()) -> NFData (NoSubst t a)
forall a. (a -> ()) -> NFData a
forall t a. NFData a => NoSubst t a -> ()
$crnf :: forall t a. NFData a => NoSubst t a -> ()
rnf :: NoSubst t a -> ()
NFData, (forall a b. (a -> b) -> NoSubst t a -> NoSubst t b)
-> (forall a b. a -> NoSubst t b -> NoSubst t a)
-> Functor (NoSubst t)
forall a b. a -> NoSubst t b -> NoSubst t a
forall a b. (a -> b) -> NoSubst t a -> NoSubst t b
forall t a b. a -> NoSubst t b -> NoSubst t a
forall t a b. (a -> b) -> NoSubst t a -> NoSubst t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t a b. (a -> b) -> NoSubst t a -> NoSubst t b
fmap :: forall a b. (a -> b) -> NoSubst t a -> NoSubst t b
$c<$ :: forall t a b. a -> NoSubst t b -> NoSubst t a
<$ :: forall a b. a -> NoSubst t b -> NoSubst t a
Functor)

-- | Newtype for terms that produce a dummy when applied to incompatible
-- eliminations, instead of crashing.
newtype BraveTerm = BraveTerm { BraveTerm -> Term
unBrave :: Term } deriving Int -> BraveTerm -> ShowS
[BraveTerm] -> ShowS
BraveTerm -> [Char]
(Int -> BraveTerm -> ShowS)
-> (BraveTerm -> [Char])
-> ([BraveTerm] -> ShowS)
-> Show BraveTerm
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BraveTerm -> ShowS
showsPrec :: Int -> BraveTerm -> ShowS
$cshow :: BraveTerm -> [Char]
show :: BraveTerm -> [Char]
$cshowList :: [BraveTerm] -> ShowS
showList :: [BraveTerm] -> ShowS
Show

---------------------------------------------------------------------------
-- * Views
---------------------------------------------------------------------------

---------------------------------------------------------------------------
-- * Dummy terms
---------------------------------------------------------------------------

-- | Terms used for internal purposes
data DummyTermKind
  = DummyNamed      String
  -- ^ Generic dummy term, the 'String' generally describes where the
  -- term was generated (as well as giving a disambiguator).
  --
  -- Should not be used to convey actual information.
  | DummyBrave Term
  -- ^ Collects applications to a 'BraveTerm'.
  | DummyDisplay
  -- ^ An underscore in the right-hand side of a @DISPLAY@ pragma.
  --
  -- This renders as an underscore when reified but it has the property
  -- of matching arbitrary patterns in display form matching.
  --
  -- Can be used to allow chaining display forms for projections into
  -- display forms for copies, when the parameters can't be
  -- reconstructed.
  deriving Int -> DummyTermKind -> ShowS
[DummyTermKind] -> ShowS
DummyTermKind -> [Char]
(Int -> DummyTermKind -> ShowS)
-> (DummyTermKind -> [Char])
-> ([DummyTermKind] -> ShowS)
-> Show DummyTermKind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DummyTermKind -> ShowS
showsPrec :: Int -> DummyTermKind -> ShowS
$cshow :: DummyTermKind -> [Char]
show :: DummyTermKind -> [Char]
$cshowList :: [DummyTermKind] -> ShowS
showList :: [DummyTermKind] -> ShowS
Show

instance IsString DummyTermKind where
  fromString :: [Char] -> DummyTermKind
fromString = [Char] -> DummyTermKind
DummyNamed

-- | Construct a string representing the call-site that created the dummy thing.
dummyLocName :: CallStack -> String
dummyLocName :: CallStack -> [Char]
dummyLocName CallStack
cs = [Char] -> (CallSite -> [Char]) -> Maybe CallSite -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ CallSite -> [Char]
prettyCallSite (CallStack -> Maybe CallSite
headCallSite CallStack
cs)

-- | Aux: A dummy term to constitute a dummy term/level/sort/type.
dummyTermWith :: String -> CallStack -> Term
dummyTermWith :: [Char] -> CallStack -> Term
dummyTermWith [Char]
kind CallStack
cs = (DummyTermKind -> Elims -> Term) -> Elims -> DummyTermKind -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip DummyTermKind -> Elims -> Term
Dummy [] (DummyTermKind -> Term)
-> ([Char] -> DummyTermKind) -> [Char] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> DummyTermKind
DummyNamed ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
kind, [Char]
": ", CallStack -> [Char]
dummyLocName CallStack
cs]

__DUMMY_TERM_WITH__ :: HasCallStack => String -> Term
__DUMMY_TERM_WITH__ :: HasCallStack => [Char] -> Term
__DUMMY_TERM_WITH__ = (CallStack -> Term) -> Term
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Term) -> Term)
-> ([Char] -> CallStack -> Term) -> [Char] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> CallStack -> Term
dummyTermWith

-- | A dummy term created at location.
--   Note: use macro '__DUMMY_TERM__' !
dummyTerm :: CallStack -> Term
dummyTerm :: CallStack -> Term
dummyTerm = [Char] -> CallStack -> Term
dummyTermWith [Char]
"dummyTerm"

__DUMMY_TERM__ :: HasCallStack => Term
__DUMMY_TERM__ :: HasCallStack => Term
__DUMMY_TERM__ = (CallStack -> Term) -> Term
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Term
dummyTerm

-- | A dummy level to constitute a level/sort created at location.
--   Note: use macro '__DUMMY_LEVEL__' !
dummyLevel :: CallStack -> Level
dummyLevel :: CallStack -> Level
dummyLevel = Term -> Level
forall t. t -> Level' t
atomicLevel (Term -> Level) -> (CallStack -> Term) -> CallStack -> Level
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> CallStack -> Term
dummyTermWith [Char]
"dummyLevel"

__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ = (CallStack -> Level) -> Level
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Level
dummyLevel

-- | A dummy sort created at location.
--   Note: use macro __DUMMY_SORT__ !
dummySort :: CallStack -> Sort
dummySort :: CallStack -> Sort
dummySort = [Char] -> Sort
forall t. [Char] -> Sort' t
DummyS ([Char] -> Sort) -> (CallStack -> [Char]) -> CallStack -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [Char]
dummyLocName

__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ = (CallStack -> Sort) -> Sort
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Sort
dummySort

-- | A dummy type created at location.
--   Note: use macro '__DUMMY_TYPE__' !
dummyType :: CallStack -> Type
dummyType :: CallStack -> Type
dummyType CallStack
cs = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (CallStack -> Sort
dummySort CallStack
cs) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ [Char] -> CallStack -> Term
dummyTermWith [Char]
"dummyType" CallStack
cs

__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ = (CallStack -> Type) -> Type
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Type
dummyType

-- | Context entries without a type have this dummy type.
--   Note: use macro '__DUMMY_DOM__' !
dummyDom :: CallStack -> Dom Type
dummyDom :: CallStack -> Dom Type
dummyDom = Type -> Dom Type
forall a t. a -> Dom' t a
defaultDom (Type -> Dom Type) -> (CallStack -> Type) -> CallStack -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Type
dummyType

__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ = (CallStack -> Dom Type) -> Dom Type
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Dom Type
dummyDom

impossibleTerm :: CallStack -> Term
impossibleTerm :: CallStack -> Term
impossibleTerm = (DummyTermKind -> Elims -> Term) -> Elims -> DummyTermKind -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip DummyTermKind -> Elims -> Term
Dummy [] (DummyTermKind -> Term)
-> (CallStack -> DummyTermKind) -> CallStack -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> DummyTermKind
DummyNamed ([Char] -> DummyTermKind)
-> (CallStack -> [Char]) -> CallStack -> DummyTermKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> [Char]
forall a. Show a => a -> [Char]
show (Impossible -> [Char])
-> (CallStack -> Impossible) -> CallStack -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Impossible

---------------------------------------------------------------------------
-- * Eliminations.
---------------------------------------------------------------------------

{-
Note: 'unSpine' is computed quite often, so it makes sense to optimize
it. The first optimization is to check with 'hasProj' and skip building
a new term if the spine doesn't contain projections.  The second
optimization is to use an unboxed sum type to distinguish the three
cases for reconstructing a term with spines ('Var', 'Def' and 'MetaV'),
thereby avoiding heap allocation.

Docs on unboxed sums: https://downloads.haskell.org/ghc/9.14.1/docs/users_guide/exts/primitives.html#unboxed-sums
-}

#if __GLASGOW_HASKELL__ < 906
data SpineHead' = SHVar !Int | SHDef !QName | SHMetaV {-# UNPACK #-} !MetaId
newtype SpineHead = SpineHead SpineHead'
#else
-- | A 'Term' head that can be applied to some 'Elims'.
data SpineHead'
  = SHVar !Int
    -- ^ A 'Term' headed by a variable.
  | SHDef !QName
    -- ^ A 'Term' headed by a defined symbol.
  | SHMetaV {-# UNPACK #-} !MetaId
    -- ^ A 'Term' headed by a metavariable.

data SpineHead = SpineHead {-# UNPACK #-} !SpineHead'
#endif

-- | Apply a 'SpineHead' to its 'Elims'.
applySpineHead :: SpineHead -> Elims -> Term
applySpineHead :: SpineHead -> Elims -> Term
applySpineHead SpineHead
h !Elims
es = case SpineHead
h of
  SpineHead (SHVar Int
x  ) -> Int -> Elims -> Term
Var Int
x Elims
es
  SpineHead (SHDef QName
f  ) -> QName -> Elims -> Term
Def QName
f Elims
es
  SpineHead (SHMetaV MetaId
x) -> MetaId -> Elims -> Term
MetaV MetaId
x Elims
es

unSpineLoop :: SpineHead -> Elims -> Elims -> Term
unSpineLoop :: SpineHead -> Elims -> Elims -> Term
unSpineLoop !SpineHead
h !Elims
res Elims
es = case Elims
es of
  []             -> SpineHead -> Elims -> Term
applySpineHead SpineHead
h (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims -> Elims
forall a. [a] -> [a]
reverse Elims
res
  Proj ProjOrigin
_ QName
f : Elims
es' -> let !v :: Arg Term
v = Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$! (SpineHead -> Elims -> Term
applySpineHead SpineHead
h (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims -> Elims
forall a. [a] -> [a]
reverse Elims
res) in
                    SpineHead -> Elims -> Elims -> Term
unSpineLoop (SpineHead' -> SpineHead
SpineHead (QName -> SpineHead'
SHDef QName
f)) [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
v] Elims
es'
  Elim' Term
e        : Elims
es' -> SpineHead -> Elims -> Elims -> Term
unSpineLoop SpineHead
h (Elim' Term
e Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
res) Elims
es'

-- | Convert top-level postfix projections into prefix projections.
unSpine :: Term -> Term
unSpine :: Term -> Term
unSpine Term
t = case Term
t of
  Var Int
i Elims
es   | Elims -> Bool
forall a. [Elim' a] -> Bool
hasProj Elims
es -> SpineHead -> Elims -> Elims -> Term
unSpineLoop (SpineHead' -> SpineHead
SpineHead (Int -> SpineHead'
SHVar Int
i  )) [] Elims
es
  Def QName
f Elims
es   | Elims -> Bool
forall a. [Elim' a] -> Bool
hasProj Elims
es -> SpineHead -> Elims -> Elims -> Term
unSpineLoop (SpineHead' -> SpineHead
SpineHead (QName -> SpineHead'
SHDef QName
f  )) [] Elims
es
  MetaV MetaId
x Elims
es | Elims -> Bool
forall a. [Elim' a] -> Bool
hasProj Elims
es -> SpineHead -> Elims -> Elims -> Term
unSpineLoop (SpineHead' -> SpineHead
SpineHead (MetaId -> SpineHead'
SHMetaV MetaId
x)) [] Elims
es
  Term
t -> Term
t

{-# INLINE hasElims #-}
-- | A view picking out those 'Term's built out of a head form that
-- supports eliminations ('Var', 'Def', 'MetaV').
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v = case Term
v of
  Var   Int
i Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (Int -> Elims -> Term
Var   Int
i, Elims
es)
  Def   QName
f Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def   QName
f, Elims
es)
  MetaV MetaId
x Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (MetaId -> Elims -> Term
MetaV MetaId
x, Elims
es)
  Con{}      -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Lit{}      -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Lam{}      -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Pi{}       -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Sort{}     -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Level{}    -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  DontCare{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
  Dummy{}    -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing


---------------------------------------------------------------------------
-- * Basic term traversals
---------------------------------------------------------------------------

-- @TypeOf a@ contains sufficient type information to do
-- a type-directed traversal of @a@.
type family TypeOf a

type instance TypeOf Term        = Type                  -- Type of the term
type instance TypeOf Elims       = (Type, Elims -> Term) -- Head symbol type + constructor
type instance TypeOf (Abs Term)  = (Dom Type, Abs Type)  -- Domain type + codomain type
type instance TypeOf (Abs Type)  = Dom Type              -- Domain type
type instance TypeOf (Arg a)     = Dom (TypeOf a)
type instance TypeOf (Dom a)     = TypeOf a
type instance TypeOf Type        = ()
type instance TypeOf Sort        = ()
type instance TypeOf Level       = ()
type instance TypeOf [PlusLevel] = ()
type instance TypeOf PlusLevel   = ()

-- | The size of a term is roughly the number of nodes in its syntax
-- tree.
--
-- This number is only used for heuristics, so it does not need to be
-- accurately computed. Things like sort annotations may be skipped.

class TermSize a where
  termSize :: a -> Int
  termSize = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize

  tsize :: a -> Sum Int

instance {-# OVERLAPPABLE #-} (Foldable t, TermSize a) => TermSize (t a) where
  tsize :: t a -> Sum Int
tsize = (a -> Sum Int) -> t a -> Sum Int
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize

instance TermSize Term where
  tsize :: Term -> Sum Int
tsize = \case
    Var Int
_ Elims
vs    -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Def QName
_ Elims
vs    -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Con ConHead
_ ConInfo
_ Elims
vs  -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    MetaV MetaId
_ Elims
vs  -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Level Level
l     -> Level -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Level
l
    Lam ArgInfo
_ Abs Term
f     -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Term
f
    Lit Literal
_       -> Sum Int
1
    Pi Dom Type
a Abs Type
b      -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Dom Type -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Dom Type
a Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Type -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Type
b
    Sort Sort
s      -> Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s
    DontCare Term
mv -> Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Term
mv
    Dummy{}     -> Sum Int
1

instance TermSize Sort where
  tsize :: Sort -> Sum Int
tsize = \case
    Univ Univ
_ Level
l       -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Level -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Level
l
    Inf Univ
_ Integer
_        -> Sum Int
1
    Sort
LevelUniv      -> Sum Int
1
    Sort
IntervalUniv   -> Sum Int
1
    Sort
CofUniv        -> Sum Int
1
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Dom' Term Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Dom' Term Term
a Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Sort
s2
    FunSort Sort
s1 Sort
s2  -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s2
    UnivSort Sort
s     -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s
    MetaS MetaId
_ Elims
es     -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
es
    DefS QName
_ Elims
es      -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
es
    DummyS{}       -> Sum Int
1

instance TermSize Level where
  tsize :: Level -> Sum Int
tsize (Max Integer
_ [PlusLevel' Term]
as) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ [PlusLevel' Term] -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize [PlusLevel' Term]
as

instance TermSize PlusLevel where
  tsize :: PlusLevel' Term -> Sum Int
tsize (Plus Integer
_ Term
a)      = Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Term
a

instance TermSize a => TermSize (Substitution' a) where
  tsize :: Substitution' a -> Sum Int
tsize Substitution' a
IdS                  = Sum Int
1
  tsize (EmptyS Impossible
_)           = Sum Int
1
  tsize (Wk Int
_ Substitution' a
rho)           = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (a
t :# Substitution' a
rho)           = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize a
t Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (Strengthen Impossible
_ Int
_ Substitution' a
rho) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (Lift Int
_ Substitution' a
rho)         = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho

---------------------------------------------------------------------------
-- * KillRange instances.
---------------------------------------------------------------------------

instance KillRange Term where
  killRange :: Term -> Term
killRange = \case
    Var Int
i Elims
vs    -> (Elims -> Term) -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Int -> Elims -> Term
Var Int
i) Elims
vs
    Def QName
c Elims
vs    -> (QName -> Elims -> Term) -> QName -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Elims -> Term
Def QName
c Elims
vs
    Con ConHead
c ConInfo
ci Elims
vs -> (ConHead -> ConInfo -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci Elims
vs
    MetaV MetaId
m Elims
vs  -> (Elims -> Term) -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (MetaId -> Elims -> Term
MetaV MetaId
m) Elims
vs
    Lam ArgInfo
i Abs Term
f     -> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo -> Abs Term -> Term
Lam ArgInfo
i Abs Term
f
    Lit Literal
l       -> (Literal -> Term) -> Literal -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Literal -> Term
Lit Literal
l
    Level Level
l     -> (Level -> Term) -> Level -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Level -> Term
Level Level
l
    Pi Dom Type
a Abs Type
b      -> (Dom Type -> Abs Type -> Term) -> Dom Type -> Abs Type -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b
    Sort Sort
s      -> (Sort -> Term) -> Sort -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort -> Term
Sort Sort
s
    DontCare Term
mv -> (Term -> Term) -> Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Term -> Term
DontCare Term
mv
    v :: Term
v@Dummy{}   -> Term
v

instance KillRange a => KillRange (Level' a) where
  killRange :: KillRangeT (Level' a)
killRange (Max Integer
n [PlusLevel' a]
as) = ([PlusLevel' a] -> Level' a) -> [PlusLevel' a] -> Level' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Integer -> [PlusLevel' a] -> Level' a
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) [PlusLevel' a]
as

instance KillRange a => KillRange (PlusLevel' a) where
  killRange :: KillRangeT (PlusLevel' a)
killRange (Plus Integer
n a
l) = (a -> PlusLevel' a) -> a -> PlusLevel' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Integer -> a -> PlusLevel' a
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) a
l

instance (KillRange a, KillRange b) => KillRange (Type'' a b) where
  killRange :: KillRangeT (Type'' a b)
killRange (El Sort' a
s b
v) = (Sort' a -> b -> Type'' a b) -> Sort' a -> b -> Type'' a b
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort' a -> b -> Type'' a b
forall t a. Sort' t -> a -> Type'' t a
El Sort' a
s b
v

instance KillRange a => KillRange (Sort' a) where
  killRange :: KillRangeT (Sort' a)
killRange = \case
    Inf Univ
u Integer
n        -> Univ -> Integer -> Sort' a
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
    Sort' a
LevelUniv      -> Sort' a
forall t. Sort' t
LevelUniv
    Sort' a
IntervalUniv   -> Sort' a
forall t. Sort' t
IntervalUniv
    Sort' a
CofUniv        -> Sort' a
forall t. Sort' t
CofUniv
    Univ Univ
u Level' a
a       -> (Level' a -> Sort' a) -> Level' a -> Sort' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Univ -> Level' a -> Sort' a
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u) Level' a
a
    PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2 -> (Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a)
-> Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2
    FunSort Sort' a
s1 Sort' a
s2  -> (Sort' a -> KillRangeT (Sort' a))
-> Sort' a -> KillRangeT (Sort' a)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort' a -> KillRangeT (Sort' a)
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' a
s1 Sort' a
s2
    UnivSort Sort' a
s     -> KillRangeT (Sort' a) -> KillRangeT (Sort' a)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN KillRangeT (Sort' a)
forall t. Sort' t -> Sort' t
UnivSort Sort' a
s
    MetaS MetaId
x [Elim' a]
es     -> ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (MetaId -> [Elim' a] -> Sort' a
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x) [Elim' a]
es
    DefS QName
d [Elim' a]
es      -> (QName -> [Elim' a] -> Sort' a) -> QName -> [Elim' a] -> Sort' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [Elim' a] -> Sort' a
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d [Elim' a]
es
    s :: Sort' a
s@DummyS{}     -> Sort' a
s

instance KillRange Substitution where
  killRange :: KillRangeT Substitution
killRange Substitution
IdS                    = Substitution
forall a. Substitution' a
IdS
  killRange (EmptyS Impossible
err)           = Impossible -> Substitution
forall a. Impossible -> Substitution' a
EmptyS Impossible
err
  killRange (Wk Int
n Substitution
rho)             = KillRangeT Substitution -> KillRangeT Substitution
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Int -> KillRangeT Substitution
forall a. Int -> Substitution' a -> Substitution' a
Wk Int
n) Substitution
rho
  killRange (Term
t :# Substitution
rho)             = (Term -> KillRangeT Substitution)
-> Term -> KillRangeT Substitution
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Term -> KillRangeT Substitution
forall a. a -> Substitution' a -> Substitution' a
(:#) Term
t Substitution
rho
  killRange (Strengthen Impossible
err Int
n Substitution
rho) = KillRangeT Substitution -> KillRangeT Substitution
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Impossible -> Int -> KillRangeT Substitution
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
err Int
n) Substitution
rho
  killRange (Lift Int
n Substitution
rho)           = KillRangeT Substitution -> KillRangeT Substitution
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Int -> KillRangeT Substitution
forall a. Int -> Substitution' a -> Substitution' a
Lift Int
n) Substitution
rho

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

-----------------------------------------------------------------------------
-- * Simple pretty printing
-----------------------------------------------------------------------------

instance Pretty a => Pretty (Substitution' a) where
  prettyPrec :: Int -> Substitution' a -> Doc
prettyPrec = Int -> Substitution' a -> Doc
forall {t} {a}.
(Ord t, Num t, Pretty a) =>
t -> Substitution' a -> Doc
pr
    where
    pr :: t -> Substitution' a -> Doc
pr t
p Substitution' a
rho = case Substitution' a
rho of
      Substitution' a
IdS                -> Doc -> Doc
hlKeyword Doc
"idS"
      EmptyS Impossible
_err        -> Doc -> Doc
hlKeyword Doc
"emptyS"
      a
t :# Substitution' a
rho           -> Bool -> Doc -> Doc
mparens (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
2) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                            [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ t -> Substitution' a -> Doc
pr t
2 Substitution' a
rho Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
",", Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
3 a
t ]
      Strengthen Impossible
_ Int
n Substitution' a
rho -> Bool -> Doc -> Doc
mparens (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                            Doc -> Doc
hlKeyword Doc
"strS" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
      Wk Int
n Substitution' a
rho           -> Bool -> Doc -> Doc
mparens (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                            Doc -> Doc
hlKeyword Doc
"wkS" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
      Lift Int
n Substitution' a
rho         -> Bool -> Doc -> Doc
mparens (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                            Doc -> Doc
hlKeyword Doc
"liftS" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho

instance Pretty Term where
  prettyPrec :: Int -> Term -> Doc
prettyPrec Int
p Term
v =
    case Term
v of
      Var Int
x Elims
els -> Doc -> Doc
hlBound ([Char] -> Doc
forall a. [Char] -> Doc a
text ([Char]
"@" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x)) Doc -> Elims -> Doc
`pApp` Elims
els
      Lam ArgInfo
ai Abs Term
b   ->
        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
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
P.lambda Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ArgInfo -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
ai Doc -> Doc
forall a. a -> a
id (ShortText -> Doc
forall a. Pretty a => a -> Doc
pretty (ShortText -> Doc) -> (Abs Term -> ShortText) -> Abs Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs Term -> ShortText
forall a. Abs a -> ShortText
absName (Abs Term -> Doc) -> Abs Term -> Doc
forall a b. (a -> b) -> a -> b
$ Abs Term
b) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
P.arrow
            , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Term -> Doc
forall a. Pretty a => a -> Doc
pretty (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b) ]
      Lit Literal
l                -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
      Def QName
q Elims
els            -> Doc -> Doc
hlFunction (QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q) Doc -> Elims -> Doc
`pApp` Elims
els
      Con ConHead
c ConInfo
_ci Elims
vs         -> Induction -> Doc -> Doc
hlConstructor (ConHead -> Induction
conInductive ConHead
c) (QName -> Doc
forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c)) Doc -> Elims -> Doc
`pApp` Elims
vs
      Pi Dom Type
a (NoAbs ShortText
_ Type
b)     -> 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
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Int -> Type -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
P.arrow
            , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
b ]
      Pi Dom Type
a Abs Type
b               -> 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
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ ArgInfo -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
pDom (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (ShortText -> Doc
forall a. Pretty a => a -> Doc
pretty (Abs Type -> ShortText
forall a. Abs a -> ShortText
absName Abs Type
b) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
colon Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
P.arrow
            , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Doc
forall a. Pretty a => a -> Doc
pretty (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b) ]
      Sort Sort
s      -> Int -> Sort -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Sort
s
      Level Level
l     -> Int -> Level -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Level
l
      MetaV (MetaId Word64
mid ModuleNameHash
_) Elims
els -> Doc -> Doc
hlNumber (Doc
"_" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc
forall a. Pretty a => a -> Doc
pretty Word64
mid) Doc -> Elims -> Doc
`pApp` Elims
els
      DontCare Term
v  -> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
v

      Dummy DummyTermKind
kind Elims
es -> case DummyTermKind
kind of
        DummyNamed [Char]
s  -> Doc -> Doc
parens ([Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
s) Doc -> Elims -> Doc
`pApp` Elims
es
        DummyBrave Term
hd -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
hd Doc -> Elims -> Doc
`pApp` Elims
es
        DummyTermKind
DummyDisplay  -> Doc
forall a. Underscore a => a
underscore
    where
      pApp :: Doc -> Elims -> Doc
pApp Doc
d Elims
els = Bool -> Doc -> Doc
mparens (Bool -> Bool
not (Elims -> Bool
forall a. Null a => a -> Bool
null Elims
els) Bool -> Bool -> Bool
&& Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                   [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
d, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Elim' Term -> Doc) -> Elims -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Elim' Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) Elims
els)]

prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
0 Int -> Doc
d = Int -> Doc
d Int
p
prettyPrecLevelSucs Int
p Integer
n Int -> Doc
d = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
hlPrimitive Doc
"lsuc" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
10 (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Int -> Doc
d

instance Pretty Level where
  prettyPrec :: Int -> Level -> Doc
prettyPrec Int
p (Max Integer
n [PlusLevel' Term]
as) =
    case [PlusLevel' Term]
as of
      []  -> Doc
prettyN
      [PlusLevel' Term
a] | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Int -> PlusLevel' Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p PlusLevel' Term
a
      [PlusLevel' Term]
_   -> Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc -> Doc) -> [Doc] -> Doc
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
List.foldr1 (\Doc
a Doc
b -> Doc -> Doc
hlPrimitive Doc
"lub" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
b) ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        [ Doc
prettyN | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++! (PlusLevel' Term -> Doc) -> [PlusLevel' Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> PlusLevel' Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [PlusLevel' Term]
as
    where
      prettyN :: Doc
prettyN = Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
n (Doc -> Int -> Doc
forall a b. a -> b -> a
const (Doc -> Doc
hlPrimitive Doc
"lzero"))

instance Pretty PlusLevel where
  prettyPrec :: Int -> PlusLevel' Term -> Doc
prettyPrec Int
p (Plus Integer
n Term
a) = Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
n ((Int -> Doc) -> Doc) -> (Int -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Int
p -> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
a

instance Pretty Sort where
  prettyPrec :: Int -> Sort -> Doc
prettyPrec Int
p Sort
s =
    case Sort
s of
      Univ Univ
u (ClosedLevel Integer
n) -> Doc -> Doc
hlPrimitive (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> ShowS
forall {a}. (Eq a, Num a, Show a) => a -> ShowS
suffix Integer
n ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Univ -> [Char]
showUniv Univ
u
      Univ Univ
u Level
l -> Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
hlPrimitive ([Char] -> Doc
forall a. [Char] -> Doc a
text (Univ -> [Char]
showUniv Univ
u)) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Level -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
      Inf Univ
u Integer
n -> Doc -> Doc
hlPrimitive (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> ShowS
forall {a}. (Eq a, Num a, Show a) => a -> ShowS
suffix Integer
n ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Univ -> [Char]
showUniv Univ
u [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++! [Char]
"ω"
      Sort
LevelUniv    -> Doc -> Doc
hlPrimitive Doc
"LevelUniv"
      Sort
CofUniv      -> Doc -> Doc
hlPrimitive Doc
"CofUniv"
      Sort
IntervalUniv -> Doc -> Doc
hlPrimitive Doc
"IntervalUniv"
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc
hlPrimitive Doc
"piSort"
          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ArgInfo -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
pDom (Dom' Term Term -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Term
a) (ShortText -> Doc
forall a. Pretty a => a -> Doc
pretty (Abs Sort -> ShortText
forall a. Abs a -> ShortText
absName Abs Sort
s2) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
colon Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
a) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
colon Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Sort -> Doc
forall a. Pretty a => a -> Doc
pretty Sort
s1)
          Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc -> Doc
parens (Sort -> Doc
forall a. Pretty a => a -> Doc
pretty (Abs Sort -> Sort
forall a. Abs a -> a
unAbs Abs Sort
s2))
      FunSort Sort
a Sort
b -> Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc
hlPrimitive Doc
"funSort" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Sort -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Sort -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
b
      UnivSort Sort
s -> Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
hlPrimitive Doc
"univSort" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Sort -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
s
      MetaS MetaId
x Elims
es -> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      DefS QName
d Elims
es  -> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      DummyS [Char]
s   -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
s
   where
     suffix :: a -> ShowS
suffix a
n = Bool -> ShowS -> ShowS
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0) ([Char] -> ShowS
forall a. [a] -> [a] -> [a]
++! a -> [Char]
forall a. Show a => a -> [Char]
show a
n)

instance Pretty Type where
  prettyPrec :: Int -> Type -> Doc
prettyPrec Int
p (El Sort
_ Term
a) = Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
a

instance Pretty a => Pretty (Blocked a) where
  pretty :: Blocked a -> Doc
pretty = \case
    NotBlocked NotBlocked' Term
ReallyNotBlocked a
a -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
    NotBlocked NotBlocked' Term
nb a
a -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (Doc
"[ blocked on" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> NotBlocked' Term -> Doc
forall a. Pretty a => a -> Doc
pretty NotBlocked' Term
nb Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"]")
    Blocked     Blocker
b a
a -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (Doc
"[ stuck on" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Blocker -> Doc
forall a. Pretty a => a -> Doc
pretty  Blocker
b Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"]")

instance Pretty a => Pretty (NoSubst t a) where
  pretty :: NoSubst t a -> Doc
pretty = a -> Doc
forall a. Pretty a => a -> Doc
pretty (a -> Doc) -> (NoSubst t a -> a) -> NoSubst t a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NoSubst t a -> a
forall t a. NoSubst t a -> a
unNoSubst

-----------------------------------------------------------------------------
-- * NFData instances
-----------------------------------------------------------------------------

-- Note: only strict in the shape of the terms.

instance NFData Term where
  rnf :: Term -> ()
rnf = \case
    Var Int
_ Elims
es   -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
    Lam ArgInfo
_ Abs Term
b    -> Term -> ()
forall a. NFData a => a -> ()
rnf (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
    Lit Literal
l      -> Literal -> ()
forall a. NFData a => a -> ()
rnf Literal
l
    Def QName
_ Elims
es   -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
    Con ConHead
_ ConInfo
_ Elims
vs -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
vs
    Pi Dom Type
a Abs Type
b     -> (Type, Type) -> ()
forall a. NFData a => a -> ()
rnf (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a, Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
    Sort Sort
s     -> Sort -> ()
forall a. NFData a => a -> ()
rnf Sort
s
    Level Level
l    -> Level -> ()
forall a. NFData a => a -> ()
rnf Level
l
    MetaV MetaId
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
    DontCare Term
v -> Term -> ()
forall a. NFData a => a -> ()
rnf Term
v
    Dummy DummyTermKind
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es

instance NFData Type where
  rnf :: Type -> ()
rnf (El Sort
s Term
v) = (Sort, Term) -> ()
forall a. NFData a => a -> ()
rnf (Sort
s, Term
v)

instance NFData Sort where
  rnf :: Sort -> ()
rnf = \case
    Univ Univ
_ Level
l     -> Level -> ()
forall a. NFData a => a -> ()
rnf Level
l
    Inf Univ
_ Integer
_      -> ()
    Sort
LevelUniv    -> ()
    Sort
CofUniv      -> ()
    Sort
IntervalUniv -> ()
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> (Dom' Term Term, Sort, Sort) -> ()
forall a. NFData a => a -> ()
rnf (Dom' Term Term
a, Sort
b, Abs Sort -> Sort
forall a. Abs a -> a
unAbs Abs Sort
c)
    FunSort Sort
a Sort
b  -> (Sort, Sort) -> ()
forall a. NFData a => a -> ()
rnf (Sort
a, Sort
b)
    UnivSort Sort
a   -> Sort -> ()
forall a. NFData a => a -> ()
rnf Sort
a
    MetaS MetaId
_ Elims
es   -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
    DefS QName
_ Elims
es    -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
    DummyS [Char]
_     -> ()

instance NFData Level where
  rnf :: Level -> ()
rnf (Max Integer
n [PlusLevel' Term]
as) = (Integer, [PlusLevel' Term]) -> ()
forall a. NFData a => a -> ()
rnf (Integer
n, [PlusLevel' Term]
as)

instance NFData PlusLevel where
  rnf :: PlusLevel' Term -> ()
rnf (Plus Integer
n Term
l) = (Integer, Term) -> ()
forall a. NFData a => a -> ()
rnf (Integer
n, Term
l)

instance NFData a => NFData (Substitution' a)