{-# LANGUAGE CPP                        #-}
{-# LANGUAGE PatternSynonyms            #-}

module Agda.Syntax.Internal
    ( module Agda.Syntax.Internal
    , module Agda.Syntax.Internal.Blockers
    , module Agda.Syntax.Internal.Elim
    , module Agda.Syntax.Abstract.Name
    , MetaId(..), ProblemId(..)
    ) where

import Prelude hiding (null)

import Control.Monad.Identity
import Control.DeepSeq

import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>), Sum(..) )
import qualified Data.Set as Set
import Data.Set (Set)

import Data.Traversable

import GHC.Generics (Generic)

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Pretty (prettyHiding)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal.Blockers
import Agda.Syntax.Internal.Elim

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

import Agda.Utils.Empty

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Pretty
import Agda.Utils.Tuple

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Function type domain
---------------------------------------------------------------------------

-- | Similar to 'Arg', but we need to distinguish
--   an irrelevance annotation in a function domain
--   (the domain itself is not irrelevant!)
--   from an irrelevant argument.
--
--   @Dom@ is used in 'Pi' of internal syntax, in 'Context' and 'Telescope'.
--   'Arg' is used for actual arguments ('Var', 'Con', 'Def' etc.)
--   and in 'Abstract' syntax and other situations.
--
--   [ cubical ] When @annFinite (argInfoAnnotation domInfo) = True@ for
--   the domain of a 'Pi' type, the elements should be compared by
--   tabulating the domain type.  Only supported in case the domain type
--   is primIsOne, to obtain the correct equality for partial elements.
--
data Dom' t e = Dom
  { forall t e. Dom' t e -> ArgInfo
domInfo   :: ArgInfo
  , forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName   :: Maybe NamedName  -- ^ e.g. @x@ in @{x = y : A} -> B@.
  , forall t e. Dom' t e -> Bool
domIsFinite :: Bool
    -- ^ Is this a Π-type (False), or a partial type (True)?
  , forall t e. Dom' t e -> Maybe t
domTactic :: Maybe t        -- ^ "@tactic e".
  , forall t e. Dom' t e -> e
unDom     :: e
  } deriving (Int -> Dom' t e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
forall t e. (Show t, Show e) => Dom' t e -> ArgName
showList :: [Dom' t e] -> ShowS
$cshowList :: forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
show :: Dom' t e -> ArgName
$cshow :: forall t e. (Show t, Show e) => Dom' t e -> ArgName
showsPrec :: Int -> Dom' t e -> ShowS
$cshowsPrec :: forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
Show, forall a b. a -> Dom' t b -> Dom' t a
forall a b. (a -> b) -> Dom' t a -> Dom' t b
forall t a b. a -> Dom' t b -> Dom' t a
forall t a b. (a -> b) -> Dom' t a -> Dom' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Dom' t b -> Dom' t a
$c<$ :: forall t a b. a -> Dom' t b -> Dom' t a
fmap :: forall a b. (a -> b) -> Dom' t a -> Dom' t b
$cfmap :: forall t a b. (a -> b) -> Dom' t a -> Dom' t b
Functor, forall a. Dom' t a -> Bool
forall t a. Eq a => a -> Dom' t a -> Bool
forall t a. Num a => Dom' t a -> a
forall t a. Ord a => Dom' t a -> a
forall m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t m. Monoid m => Dom' t m -> m
forall t e. Dom' t e -> Bool
forall t a. Dom' t a -> Int
forall t a. Dom' t a -> [a]
forall a b. (a -> b -> b) -> b -> Dom' t a -> b
forall t a. (a -> a -> a) -> Dom' t a -> a
forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
forall t a b. (a -> b -> b) -> b -> Dom' 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
product :: forall a. Num a => Dom' t a -> a
$cproduct :: forall t a. Num a => Dom' t a -> a
sum :: forall a. Num a => Dom' t a -> a
$csum :: forall t a. Num a => Dom' t a -> a
minimum :: forall a. Ord a => Dom' t a -> a
$cminimum :: forall t a. Ord a => Dom' t a -> a
maximum :: forall a. Ord a => Dom' t a -> a
$cmaximum :: forall t a. Ord a => Dom' t a -> a
elem :: forall a. Eq a => a -> Dom' t a -> Bool
$celem :: forall t a. Eq a => a -> Dom' t a -> Bool
length :: forall a. Dom' t a -> Int
$clength :: forall t a. Dom' t a -> Int
null :: forall a. Dom' t a -> Bool
$cnull :: forall t e. Dom' t e -> Bool
toList :: forall a. Dom' t a -> [a]
$ctoList :: forall t a. Dom' t a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$cfoldr1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
fold :: forall m. Monoid m => Dom' t m -> m
$cfold :: forall t m. Monoid m => Dom' t m -> m
Foldable, forall t. Functor (Dom' t)
forall t. Foldable (Dom' t)
forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' 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 (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
sequence :: forall (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
$csequence :: forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
Traversable)

type Dom = Dom' Term

instance Decoration (Dom' t) where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
traverseF a -> m b
f (Dom ArgInfo
ai Maybe (WithOrigin (Ranged ArgName))
x Bool
t Maybe t
b a
a) = forall t e.
ArgInfo
-> Maybe (WithOrigin (Ranged ArgName))
-> Bool
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
ai Maybe (WithOrigin (Ranged ArgName))
x Bool
t Maybe t
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a

instance HasRange a => HasRange (Dom' t a) where
  getRange :: Dom' t a -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom

instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
  killRange :: KillRangeT (Dom' t a)
killRange (Dom ArgInfo
info Maybe (WithOrigin (Ranged ArgName))
x Bool
t Maybe t
b a
a) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 forall t e.
ArgInfo
-> Maybe (WithOrigin (Ranged ArgName))
-> Bool
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
info Maybe (WithOrigin (Ranged ArgName))
x Bool
t Maybe t
b a
a

-- | Ignores 'Origin' and 'FreeVariables' and tactic.
instance Eq a => Eq (Dom' t a) where
  Dom (ArgInfo Hiding
h1 Modality
m1 Origin
_ FreeVariables
_ Annotation
a1) Maybe (WithOrigin (Ranged ArgName))
s1 Bool
f1 Maybe t
_ a
x1 == :: Dom' t a -> Dom' t a -> Bool
== Dom (ArgInfo Hiding
h2 Modality
m2 Origin
_ FreeVariables
_ Annotation
a2) Maybe (WithOrigin (Ranged ArgName))
s2 Bool
f2 Maybe t
_ a
x2 =
    (Hiding
h1, Modality
m1, Annotation
a1, Maybe (WithOrigin (Ranged ArgName))
s1, Bool
f1, a
x1) forall a. Eq a => a -> a -> Bool
== (Hiding
h2, Modality
m2, Annotation
a2, Maybe (WithOrigin (Ranged ArgName))
s2, Bool
f2, a
x2)

instance LensNamed (Dom' t e) where
  type NameOf (Dom' t e) = NamedName
  lensNamed :: Lens' (Maybe (NameOf (Dom' t e))) (Dom' t e)
lensNamed Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f Dom' t e
dom = Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f (forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName Dom' t e
dom) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Maybe (WithOrigin (Ranged ArgName))
nm -> Dom' t e
dom { domName :: Maybe (WithOrigin (Ranged ArgName))
domName = Maybe (WithOrigin (Ranged ArgName))
nm }

instance LensArgInfo (Dom' t e) where
  getArgInfo :: Dom' t e -> ArgInfo
getArgInfo        = forall t e. Dom' t e -> ArgInfo
domInfo
  setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e
setArgInfo ArgInfo
ai Dom' t e
dom = Dom' t e
dom { domInfo :: ArgInfo
domInfo = ArgInfo
ai }
  mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
mapArgInfo ArgInfo -> ArgInfo
f  Dom' t e
dom = Dom' t e
dom { domInfo :: ArgInfo
domInfo = ArgInfo -> ArgInfo
f forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom' t e
dom }

-- The other lenses are defined through LensArgInfo

instance LensHiding        (Dom' t e) where
instance LensModality      (Dom' t e) where
instance LensOrigin        (Dom' t e) where
instance LensFreeVariables (Dom' t e) where
instance LensAnnotation    (Dom' t e) where

-- Since we have LensModality, we get relevance and quantity by default

instance LensRelevance (Dom' t e) where
instance LensQuantity  (Dom' t e) where
instance LensCohesion  (Dom' t e) where

argFromDom :: Dom' t a -> Arg a
argFromDom :: forall t a. Dom' t a -> Arg a
argFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i, unDom :: forall t e. Dom' t e -> e
unDom = a
a} = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
a

namedArgFromDom :: Dom' t a -> NamedArg a
namedArgFromDom :: forall t a. Dom' t a -> NamedArg a
namedArgFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i, domName :: forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName = Maybe (WithOrigin (Ranged ArgName))
s, unDom :: forall t e. Dom' t e -> e
unDom = a
a} = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
s a
a

-- The following functions are less general than they could be:
-- @Dom@ could be replaced by @Dom' t@.
-- However, this causes problems with instance resolution in several places.
-- often for class AddContext.

domFromArg :: Arg a -> Dom a
domFromArg :: forall a. Arg a -> Dom a
domFromArg (Arg ArgInfo
i a
a) = forall t e.
ArgInfo
-> Maybe (WithOrigin (Ranged ArgName))
-> Bool
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
i forall a. Maybe a
Nothing Bool
False forall a. Maybe a
Nothing a
a

domFromNamedArg :: NamedArg a -> Dom a
domFromNamedArg :: forall a. NamedArg a -> Dom a
domFromNamedArg (Arg ArgInfo
i Named_ a
a) = forall t e.
ArgInfo
-> Maybe (WithOrigin (Ranged ArgName))
-> Bool
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
i (forall name a. Named name a -> Maybe name
nameOf Named_ a
a) Bool
False forall a. Maybe a
Nothing (forall name a. Named name a -> a
namedThing Named_ a
a)

defaultDom :: a -> Dom a
defaultDom :: forall a. a -> Dom a
defaultDom = forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
defaultArgInfo

defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom :: forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x = forall a. Arg a -> Dom a
domFromArg (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
x)

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom :: forall a. ArgInfo -> ArgName -> a -> Dom a
defaultNamedArgDom ArgInfo
info ArgName
s a
x = (forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x) { domName :: Maybe (WithOrigin (Ranged ArgName))
domName = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged ArgName
s }

-- | Type of argument lists.
--
type Args       = [Arg Term]
type NamedArgs  = [NamedArg Term]

data DataOrRecord
  = IsData
  | IsRecord PatternOrCopattern
  deriving (Int -> DataOrRecord -> ShowS
[DataOrRecord] -> ShowS
DataOrRecord -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DataOrRecord] -> ShowS
$cshowList :: [DataOrRecord] -> ShowS
show :: DataOrRecord -> ArgName
$cshow :: DataOrRecord -> ArgName
showsPrec :: Int -> DataOrRecord -> ShowS
$cshowsPrec :: Int -> DataOrRecord -> ShowS
Show, DataOrRecord -> DataOrRecord -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataOrRecord -> DataOrRecord -> Bool
$c/= :: DataOrRecord -> DataOrRecord -> Bool
== :: DataOrRecord -> DataOrRecord -> Bool
$c== :: DataOrRecord -> DataOrRecord -> Bool
Eq, forall x. Rep DataOrRecord x -> DataOrRecord
forall x. DataOrRecord -> Rep DataOrRecord x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataOrRecord x -> DataOrRecord
$cfrom :: forall x. DataOrRecord -> Rep DataOrRecord x
Generic)

-- | Store the names of the record fields in the constructor.
--   This allows reduction of projection redexes outside of TCM.
--   For instance, during substitution and application.
data ConHead = ConHead
  { ConHead -> QName
conName       :: QName         -- ^ The name of the constructor.
  , ConHead -> DataOrRecord
conDataRecord :: DataOrRecord  -- ^ Data or record constructor?
  , ConHead -> Induction
conInductive  :: Induction     -- ^ Record constructors can be coinductive.
  , ConHead -> [Arg QName]
conFields     :: [Arg QName]   -- ^ The name of the record fields.
      --   'Arg' is stored since the info in the constructor args
      --   might not be accurate because of subtyping (issue #2170).
  } deriving (Int -> ConHead -> ShowS
[ConHead] -> ShowS
ConHead -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ConHead] -> ShowS
$cshowList :: [ConHead] -> ShowS
show :: ConHead -> ArgName
$cshow :: ConHead -> ArgName
showsPrec :: Int -> ConHead -> ShowS
$cshowsPrec :: Int -> ConHead -> ShowS
Show, forall x. Rep ConHead x -> ConHead
forall x. ConHead -> Rep ConHead x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConHead x -> ConHead
$cfrom :: forall x. ConHead -> Rep ConHead x
Generic)

instance Eq ConHead where
  == :: ConHead -> ConHead -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ConHead -> QName
conName

instance Ord ConHead where
  <= :: ConHead -> ConHead -> Bool
(<=) = forall a. Ord a => a -> a -> Bool
(<=) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ConHead -> QName
conName

instance Pretty ConHead where
  pretty :: ConHead -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName

instance HasRange ConHead where
  getRange :: ConHead -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName

instance SetRange ConHead where
  setRange :: Range -> ConHead -> ConHead
setRange Range
r = forall a. LensConName a => (QName -> QName) -> a -> a
mapConName (forall a. SetRange a => Range -> a -> a
setRange Range
r)

class LensConName a where
  getConName :: a -> QName
  setConName :: QName -> a -> a
  setConName = forall a. LensConName a => (QName -> QName) -> a -> a
mapConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapConName :: (QName -> QName) -> a -> a
  mapConName QName -> QName
f a
a = forall a. LensConName a => QName -> a -> a
setConName (QName -> QName
f (forall a. LensConName a => a -> QName
getConName a
a)) a
a

instance LensConName ConHead where
  getConName :: ConHead -> QName
getConName = ConHead -> QName
conName
  setConName :: QName -> ConHead -> ConHead
setConName QName
c ConHead
con = ConHead
con { conName :: QName
conName = QName
c }


-- | Raw values.
--
--   @Def@ is used for both defined and undefined constants.
--   Assume there is a type declaration and a definition for
--     every constant, even if the definition is an empty
--     list of clauses.
--
data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
          | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
          | Lit Literal
          | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
          | Con ConHead ConInfo Elims
          -- ^ @c es@ or @record { fs = es }@
          --   @es@ allows only Apply and IApply eliminations,
          --   and IApply only for data constructors.
          | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
          | Sort Sort
          | Level Level
          | MetaV {-# UNPACK #-} !MetaId Elims
          | DontCare Term
            -- ^ Irrelevant stuff in relevant position, but created
            --   in an irrelevant context.  Basically, an internal
            --   version of the irrelevance axiom @.irrAx : .A -> A@.
          | Dummy String Elims
            -- ^ A (part of a) term or type which is only used for internal purposes.
            --   Replaces the @Sort Prop@ hack.
            --   The @String@ typically describes the location where we create this dummy,
            --   but can contain other information as well.
            --   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
            --   eliminators, which are only there to ease debugging when a dummy term incorrectly
            --   leaks into a relevant position.
  deriving Int -> Term -> ShowS
[Term] -> ShowS
Term -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> ArgName
$cshow :: Term -> ArgName
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show

type ConInfo = ConOrigin

type Elim = Elim' Term
type Elims = [Elim]  -- ^ eliminations ordered left-to-right.

-- | Binder.
--
--   'Abs': The bound variable might appear in the body.
--   'NoAbs' is pseudo-binder, it does not introduce a fresh variable,
--      similar to the @const@ of Haskell.
--
data Abs a = Abs   { forall a. Abs a -> ArgName
absName :: ArgName, forall a. Abs a -> a
unAbs :: a }
               -- ^ The body has (at least) one free variable.
               --   Danger: 'unAbs' doesn't shift variables properly
           | NoAbs { absName :: ArgName, unAbs :: a }
  deriving (forall a b. a -> Abs b -> Abs a
forall a b. (a -> b) -> Abs a -> Abs b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Abs b -> Abs a
$c<$ :: forall a b. a -> Abs b -> Abs a
fmap :: forall a b. (a -> b) -> Abs a -> Abs b
$cfmap :: forall a b. (a -> b) -> Abs a -> Abs b
Functor, forall a. Eq a => a -> Abs a -> Bool
forall a. Num a => Abs a -> a
forall a. Ord a => Abs a -> a
forall m. Monoid m => Abs m -> m
forall a. Abs a -> Bool
forall a. Abs a -> Int
forall a. Abs a -> [a]
forall a. (a -> a -> a) -> Abs a -> a
forall m a. Monoid m => (a -> m) -> Abs a -> m
forall b a. (b -> a -> b) -> b -> Abs a -> b
forall a b. (a -> b -> b) -> b -> Abs 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
product :: forall a. Num a => Abs a -> a
$cproduct :: forall a. Num a => Abs a -> a
sum :: forall a. Num a => Abs a -> a
$csum :: forall a. Num a => Abs a -> a
minimum :: forall a. Ord a => Abs a -> a
$cminimum :: forall a. Ord a => Abs a -> a
maximum :: forall a. Ord a => Abs a -> a
$cmaximum :: forall a. Ord a => Abs a -> a
elem :: forall a. Eq a => a -> Abs a -> Bool
$celem :: forall a. Eq a => a -> Abs a -> Bool
length :: forall a. Abs a -> Int
$clength :: forall a. Abs a -> Int
null :: forall a. Abs a -> Bool
$cnull :: forall a. Abs a -> Bool
toList :: forall a. Abs a -> [a]
$ctoList :: forall a. Abs a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Abs a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Abs a -> a
foldr1 :: forall a. (a -> a -> a) -> Abs a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Abs a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
fold :: forall m. Monoid m => Abs m -> m
$cfold :: forall m. Monoid m => Abs m -> m
Foldable, Functor Abs
Foldable Abs
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 => Abs (m a) -> m (Abs a)
forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
sequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
$csequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Abs a) x -> Abs a
forall a x. Abs a -> Rep (Abs a) x
$cto :: forall a x. Rep (Abs a) x -> Abs a
$cfrom :: forall a x. Abs a -> Rep (Abs a) x
Generic)

instance Decoration Abs where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Abs a -> m (Abs b)
traverseF a -> m b
f (Abs   ArgName
x a
a) = forall a. ArgName -> a -> Abs a
Abs   ArgName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
  traverseF a -> m b
f (NoAbs ArgName
x a
a) = forall a. ArgName -> a -> Abs a
NoAbs ArgName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a

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

class LensSort a where
  lensSort ::  Lens' Sort a
  getSort  :: a -> Sort
  getSort a
a = a
a forall o i. o -> Lens' i o -> i
^. forall a. LensSort a => Lens' Sort a
lensSort

instance LensSort Sort where
  lensSort :: Lens' Sort Sort
lensSort Sort -> f Sort
f Sort
s = Sort -> f Sort
f Sort
s forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Sort
s' -> Sort
s'

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

-- General instance leads to overlapping instances.
-- instance (Decoration f, LensSort a) => LensSort (f a) where
instance LensSort a => LensSort (Dom a) where
  lensSort :: Lens' Sort (Dom a)
lensSort = forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => Lens' Sort a
lensSort

instance LensSort a => LensSort (Arg a) where
  lensSort :: Lens' Sort (Arg a)
lensSort = forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => Lens' Sort a
lensSort


-- | Sequence of types. An argument of the first type is bound in later types
--   and so on.
data Tele a = EmptyTel
            | ExtendTel a (Abs (Tele a))  -- ^ 'Abs' is never 'NoAbs'.
  deriving (Int -> Tele a -> ShowS
forall a. Show a => Int -> Tele a -> ShowS
forall a. Show a => [Tele a] -> ShowS
forall a. Show a => Tele a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Tele a] -> ShowS
$cshowList :: forall a. Show a => [Tele a] -> ShowS
show :: Tele a -> ArgName
$cshow :: forall a. Show a => Tele a -> ArgName
showsPrec :: Int -> Tele a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Tele a -> ShowS
Show, forall a b. a -> Tele b -> Tele a
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Tele b -> Tele a
$c<$ :: forall a b. a -> Tele b -> Tele a
fmap :: forall a b. (a -> b) -> Tele a -> Tele b
$cfmap :: forall a b. (a -> b) -> Tele a -> Tele b
Functor, forall a. Eq a => a -> Tele a -> Bool
forall a. Num a => Tele a -> a
forall a. Ord a => Tele a -> a
forall m. Monoid m => Tele m -> m
forall a. Tele a -> Bool
forall a. Tele a -> Int
forall a. Tele a -> [a]
forall a. (a -> a -> a) -> Tele a -> a
forall m a. Monoid m => (a -> m) -> Tele a -> m
forall b a. (b -> a -> b) -> b -> Tele a -> b
forall a b. (a -> b -> b) -> b -> Tele 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
product :: forall a. Num a => Tele a -> a
$cproduct :: forall a. Num a => Tele a -> a
sum :: forall a. Num a => Tele a -> a
$csum :: forall a. Num a => Tele a -> a
minimum :: forall a. Ord a => Tele a -> a
$cminimum :: forall a. Ord a => Tele a -> a
maximum :: forall a. Ord a => Tele a -> a
$cmaximum :: forall a. Ord a => Tele a -> a
elem :: forall a. Eq a => a -> Tele a -> Bool
$celem :: forall a. Eq a => a -> Tele a -> Bool
length :: forall a. Tele a -> Int
$clength :: forall a. Tele a -> Int
null :: forall a. Tele a -> Bool
$cnull :: forall a. Tele a -> Bool
toList :: forall a. Tele a -> [a]
$ctoList :: forall a. Tele a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Tele a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Tele a -> a
foldr1 :: forall a. (a -> a -> a) -> Tele a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Tele a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
fold :: forall m. Monoid m => Tele m -> m
$cfold :: forall m. Monoid m => Tele m -> m
Foldable, Functor Tele
Foldable Tele
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
sequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
$csequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Tele a) x -> Tele a
forall a x. Tele a -> Rep (Tele a) x
$cto :: forall a x. Rep (Tele a) x -> Tele a
$cfrom :: forall a x. Tele a -> Rep (Tele a) x
Generic)

type Telescope = Tele (Dom Type)

data IsFibrant = IsFibrant | IsStrict
  deriving (Int -> IsFibrant -> ShowS
[IsFibrant] -> ShowS
IsFibrant -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IsFibrant] -> ShowS
$cshowList :: [IsFibrant] -> ShowS
show :: IsFibrant -> ArgName
$cshow :: IsFibrant -> ArgName
showsPrec :: Int -> IsFibrant -> ShowS
$cshowsPrec :: Int -> IsFibrant -> ShowS
Show, IsFibrant -> IsFibrant -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFibrant -> IsFibrant -> Bool
$c/= :: IsFibrant -> IsFibrant -> Bool
== :: IsFibrant -> IsFibrant -> Bool
$c== :: IsFibrant -> IsFibrant -> Bool
Eq, Eq IsFibrant
IsFibrant -> IsFibrant -> Bool
IsFibrant -> IsFibrant -> Ordering
IsFibrant -> IsFibrant -> IsFibrant
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: IsFibrant -> IsFibrant -> IsFibrant
$cmin :: IsFibrant -> IsFibrant -> IsFibrant
max :: IsFibrant -> IsFibrant -> IsFibrant
$cmax :: IsFibrant -> IsFibrant -> IsFibrant
>= :: IsFibrant -> IsFibrant -> Bool
$c>= :: IsFibrant -> IsFibrant -> Bool
> :: IsFibrant -> IsFibrant -> Bool
$c> :: IsFibrant -> IsFibrant -> Bool
<= :: IsFibrant -> IsFibrant -> Bool
$c<= :: IsFibrant -> IsFibrant -> Bool
< :: IsFibrant -> IsFibrant -> Bool
$c< :: IsFibrant -> IsFibrant -> Bool
compare :: IsFibrant -> IsFibrant -> Ordering
$ccompare :: IsFibrant -> IsFibrant -> Ordering
Ord, forall x. Rep IsFibrant x -> IsFibrant
forall x. IsFibrant -> Rep IsFibrant x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IsFibrant x -> IsFibrant
$cfrom :: forall x. IsFibrant -> Rep IsFibrant x
Generic)

-- | Sorts.
--
data Sort' t
  = Type (Level' t)  -- ^ @Set ℓ@.
  | Prop (Level' t)  -- ^ @Prop ℓ@.
  | Inf IsFibrant !Integer      -- ^ @Setωᵢ@.
  | SSet (Level' t)  -- ^ @SSet ℓ@.
  | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
  | LockUniv    -- ^ @LockUniv@, a sort for locks.
  | IntervalUniv -- ^ @IntervalUniv@, a sort inhabited by the cubical interval.
  | PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) -- ^ Sort of the pi type.
  | FunSort (Sort' t) (Sort' t) -- ^ Sort of a (non-dependent) function type.
  | UnivSort (Sort' t) -- ^ Sort of another sort.
  | MetaS {-# UNPACK #-} !MetaId [Elim' t]
  | DefS QName [Elim' t] -- ^ A postulated sort.
  | DummyS String
    -- ^ A (part of a) term or type which is only used for internal purposes.
    --   Replaces the abuse of @Prop@ for a dummy sort.
    --   The @String@ typically describes the location where we create this dummy,
    --   but can contain other information as well.
  deriving Int -> Sort' t -> ShowS
forall t. Show t => Int -> Sort' t -> ShowS
forall t. Show t => [Sort' t] -> ShowS
forall t. Show t => Sort' t -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Sort' t] -> ShowS
$cshowList :: forall t. Show t => [Sort' t] -> ShowS
show :: Sort' t -> ArgName
$cshow :: forall t. Show t => Sort' t -> ArgName
showsPrec :: Int -> Sort' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Sort' t -> ShowS
Show

type Sort = Sort' Term

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

type Level = Level' Term

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

type PlusLevel = PlusLevel' Term
type LevelAtom = Term

---------------------------------------------------------------------------
-- * Brave Terms
---------------------------------------------------------------------------

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

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

type Blocked    = Blocked' Term
type NotBlocked = NotBlocked' Term
--
-- | @'Blocked a@ without the @a@.
type Blocked_ = Blocked ()

---------------------------------------------------------------------------
-- * Definitions
---------------------------------------------------------------------------

-- | Named pattern arguments.
type NAPs = [NamedArg DeBruijnPattern]

-- | A clause is a list of patterns and the clause body.
--
--  The telescope contains the types of the pattern variables and the
--  de Bruijn indices say how to get from the order the variables occur in
--  the patterns to the order they occur in the telescope. The body
--  binds the variables in the order they appear in the telescope.
--
--  @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
--
--  Terms in dot patterns are valid in the clause telescope.
--
--  For the purpose of the permutation and the body dot patterns count
--  as variables. TODO: Change this!
data Clause = Clause
    { Clause -> Range
clauseLHSRange    :: Range
    , Clause -> Range
clauseFullRange   :: Range
    , Clause -> Telescope
clauseTel         :: Telescope
      -- ^ @Δ@: The types of the pattern variables in dependency order.
    , Clause -> NAPs
namedClausePats   :: NAPs
      -- ^ @Δ ⊢ ps@.  The de Bruijn indices refer to @Δ@.
    , Clause -> Maybe Term
clauseBody        :: Maybe Term
      -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an
      --   absurd one.
    , Clause -> Maybe (Arg Type)
clauseType        :: Maybe (Arg Type)
      -- ^ @Δ ⊢ t@.  The type of the rhs under @clauseTel@.
      --   Used, e.g., by @TermCheck@.
      --   Can be 'Irrelevant' if we encountered an irrelevant projection
      --   pattern on the lhs.
    , Clause -> Bool
clauseCatchall    :: Bool
      -- ^ Clause has been labelled as CATCHALL.
    , Clause -> Maybe Bool
clauseExact       :: Maybe Bool
      -- ^ Pattern matching of this clause is exact, no catch-all case.
      --   Computed by the coverage checker.
      --   @Nothing@ means coverage checker has not run yet (clause may be inexact).
      --   @Just False@ means clause is not exact.
      --   @Just True@ means clause is exact.
    , Clause -> Maybe Bool
clauseRecursive   :: Maybe Bool
      -- ^ @clauseBody@ contains recursive calls; computed by termination checker.
      --   @Nothing@ means that termination checker has not run yet,
      --   or that @clauseBody@ contains meta-variables;
      --   these could be filled with recursive calls later!
      --   @Just False@ means definitely no recursive call.
      --   @Just True@ means definitely a recursive call.
    , Clause -> Maybe Bool
clauseUnreachable :: Maybe Bool
      -- ^ Clause has been labelled as unreachable by the coverage checker.
      --   @Nothing@ means coverage checker has not run yet (clause may be unreachable).
      --   @Just False@ means clause is not unreachable.
      --   @Just True@ means clause is unreachable.
    , Clause -> ExpandedEllipsis
clauseEllipsis    :: ExpandedEllipsis
      -- ^ Was this clause created by expansion of an ellipsis?
    , Clause -> Maybe ModuleName
clauseWhereModule :: Maybe ModuleName
      -- ^ Keeps track of the module name associate with the clause's where clause.
    }
  deriving (Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> ArgName
$cshow :: Clause -> ArgName
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Clause x -> Clause
$cfrom :: forall x. Clause -> Rep Clause x
Generic)

clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats

instance HasRange Clause where
  getRange :: Clause -> Range
getRange = Clause -> Range
clauseLHSRange

-- | Pattern variables.
type PatVarName = ArgName

patVarNameToString :: PatVarName -> String
patVarNameToString :: ShowS
patVarNameToString = ShowS
argNameToString

nameToPatVarName :: Name -> PatVarName
nameToPatVarName :: Name -> ArgName
nameToPatVarName = Name -> ArgName
nameToArgName

data PatternInfo = PatternInfo
  { PatternInfo -> PatOrigin
patOrigin :: PatOrigin
  , PatternInfo -> [Name]
patAsNames :: [Name]
  } deriving (Int -> PatternInfo -> ShowS
[PatternInfo] -> ShowS
PatternInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PatternInfo] -> ShowS
$cshowList :: [PatternInfo] -> ShowS
show :: PatternInfo -> ArgName
$cshow :: PatternInfo -> ArgName
showsPrec :: Int -> PatternInfo -> ShowS
$cshowsPrec :: Int -> PatternInfo -> ShowS
Show, PatternInfo -> PatternInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatternInfo -> PatternInfo -> Bool
$c/= :: PatternInfo -> PatternInfo -> Bool
== :: PatternInfo -> PatternInfo -> Bool
$c== :: PatternInfo -> PatternInfo -> Bool
Eq, forall x. Rep PatternInfo x -> PatternInfo
forall x. PatternInfo -> Rep PatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatternInfo x -> PatternInfo
$cfrom :: forall x. PatternInfo -> Rep PatternInfo x
Generic)

defaultPatternInfo :: PatternInfo
defaultPatternInfo :: PatternInfo
defaultPatternInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSystem []

-- | Origin of the pattern: what did the user write in this position?
data PatOrigin
  = PatOSystem         -- ^ Pattern inserted by the system
  | PatOSplit          -- ^ Pattern generated by case split
  | PatOVar Name       -- ^ User wrote a variable pattern
  | PatODot            -- ^ User wrote a dot pattern
  | PatOWild           -- ^ User wrote a wildcard pattern
  | PatOCon            -- ^ User wrote a constructor pattern
  | PatORec            -- ^ User wrote a record pattern
  | PatOLit            -- ^ User wrote a literal pattern
  | PatOAbsurd         -- ^ User wrote an absurd pattern
  deriving (Int -> PatOrigin -> ShowS
[PatOrigin] -> ShowS
PatOrigin -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PatOrigin] -> ShowS
$cshowList :: [PatOrigin] -> ShowS
show :: PatOrigin -> ArgName
$cshow :: PatOrigin -> ArgName
showsPrec :: Int -> PatOrigin -> ShowS
$cshowsPrec :: Int -> PatOrigin -> ShowS
Show, PatOrigin -> PatOrigin -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatOrigin -> PatOrigin -> Bool
$c/= :: PatOrigin -> PatOrigin -> Bool
== :: PatOrigin -> PatOrigin -> Bool
$c== :: PatOrigin -> PatOrigin -> Bool
Eq, forall x. Rep PatOrigin x -> PatOrigin
forall x. PatOrigin -> Rep PatOrigin x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatOrigin x -> PatOrigin
$cfrom :: forall x. PatOrigin -> Rep PatOrigin x
Generic)

-- | Patterns are variables, constructors, or wildcards.
--   @QName@ is used in @ConP@ rather than @Name@ since
--     a constructor might come from a particular namespace.
--     This also meshes well with the fact that values (i.e.
--     the arguments we are matching with) use @QName@.
--
data Pattern' x
  = VarP PatternInfo x
    -- ^ @x@
  | DotP PatternInfo Term
    -- ^ @.t@
  | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
    -- ^ @c ps@
    --   The subpatterns do not contain any projection copatterns.
  | LitP PatternInfo Literal
    -- ^ E.g. @5@, @"hello"@.
  | ProjP ProjOrigin QName
    -- ^ Projection copattern.  Can only appear by itself.
  | IApplyP PatternInfo Term Term x
    -- ^ Path elimination pattern, like @VarP@ but keeps track of endpoints.
  | DefP PatternInfo QName [NamedArg (Pattern' x)]
    -- ^ Used for HITs, the QName should be the one from primHComp.
  deriving (Int -> Pattern' x -> ShowS
forall x. Show x => Int -> Pattern' x -> ShowS
forall x. Show x => [Pattern' x] -> ShowS
forall x. Show x => Pattern' x -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pattern' x] -> ShowS
$cshowList :: forall x. Show x => [Pattern' x] -> ShowS
show :: Pattern' x -> ArgName
$cshow :: forall x. Show x => Pattern' x -> ArgName
showsPrec :: Int -> Pattern' x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> Pattern' x -> ShowS
Show, forall a b. a -> Pattern' b -> Pattern' a
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pattern' b -> Pattern' a
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
Functor, forall a. Eq a => a -> Pattern' a -> Bool
forall a. Num a => Pattern' a -> a
forall a. Ord a => Pattern' a -> a
forall m. Monoid m => Pattern' m -> m
forall a. Pattern' a -> Bool
forall a. Pattern' a -> Int
forall a. Pattern' a -> [a]
forall a. (a -> a -> a) -> Pattern' a -> a
forall m a. Monoid m => (a -> m) -> Pattern' a -> m
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall a b. (a -> b -> b) -> b -> Pattern' 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
product :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cmaximum :: forall a. Ord a => Pattern' a -> a
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
length :: forall a. Pattern' a -> Int
$clength :: forall a. Pattern' a -> Int
null :: forall a. Pattern' a -> Bool
$cnull :: forall a. Pattern' a -> Bool
toList :: forall a. Pattern' a -> [a]
$ctoList :: forall a. Pattern' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
fold :: forall m. Monoid m => Pattern' m -> m
$cfold :: forall m. Monoid m => Pattern' m -> m
Foldable, Functor Pattern'
Foldable Pattern'
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 => Pattern' (m a) -> m (Pattern' a)
forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall x x. Rep (Pattern' x) x -> Pattern' x
forall x x. Pattern' x -> Rep (Pattern' x) x
$cto :: forall x x. Rep (Pattern' x) x -> Pattern' x
$cfrom :: forall x x. Pattern' x -> Rep (Pattern' x) x
Generic)

type Pattern = Pattern' PatVarName
    -- ^ The @PatVarName@ is a name suggestion.

varP :: a -> Pattern' a
varP :: forall a. a -> Pattern' a
varP = forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo

dotP :: Term -> Pattern' a
dotP :: forall a. Term -> Pattern' a
dotP = forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo

litP :: Literal -> Pattern' a
litP :: forall a. Literal -> Pattern' a
litP = forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
defaultPatternInfo

-- | Type used when numbering pattern variables.
data DBPatVar = DBPatVar
  { DBPatVar -> ArgName
dbPatVarName  :: PatVarName
  , DBPatVar -> Int
dbPatVarIndex :: !Int
  } deriving (Int -> DBPatVar -> ShowS
[DBPatVar] -> ShowS
DBPatVar -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DBPatVar] -> ShowS
$cshowList :: [DBPatVar] -> ShowS
show :: DBPatVar -> ArgName
$cshow :: DBPatVar -> ArgName
showsPrec :: Int -> DBPatVar -> ShowS
$cshowsPrec :: Int -> DBPatVar -> ShowS
Show, DBPatVar -> DBPatVar -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DBPatVar -> DBPatVar -> Bool
$c/= :: DBPatVar -> DBPatVar -> Bool
== :: DBPatVar -> DBPatVar -> Bool
$c== :: DBPatVar -> DBPatVar -> Bool
Eq, forall x. Rep DBPatVar x -> DBPatVar
forall x. DBPatVar -> Rep DBPatVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DBPatVar x -> DBPatVar
$cfrom :: forall x. DBPatVar -> Rep DBPatVar x
Generic)

type DeBruijnPattern = Pattern' DBPatVar

namedVarP :: PatVarName -> Named_ Pattern
namedVarP :: ArgName -> Named_ Pattern
namedVarP ArgName
x = forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
named forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP ArgName
x
  where named :: Maybe (WithOrigin (Ranged ArgName))
named = if forall a. Underscore a => a -> Bool
isUnderscore ArgName
x then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged ArgName
x

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP :: Int -> ArgName -> Named_ DeBruijnPattern
namedDBVarP Int
m = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\ArgName
x -> ArgName -> Int -> DBPatVar
DBPatVar ArgName
x Int
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Named_ Pattern
namedVarP

-- | Make an absurd pattern with the given de Bruijn index.
absurdP :: Int -> DeBruijnPattern
absurdP :: Int -> DeBruijnPattern
absurdP = forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Int -> DBPatVar
DBPatVar ArgName
absurdPatternName

-- | The @ConPatternInfo@ states whether the constructor belongs to
--   a record type (@True@) or data type (@False@).
--   In the former case, the @PatOrigin@ of the @conPInfo@ says
--   whether the record pattern orginates from the expansion of an
--   implicit pattern.
--   The @Type@ is the type of the whole record pattern.
--   The scope used for the type is given by any outer scope
--   plus the clause's telescope ('clauseTel').
data ConPatternInfo = ConPatternInfo
  { ConPatternInfo -> PatternInfo
conPInfo   :: PatternInfo
    -- ^ Information on the origin of the pattern.
  , ConPatternInfo -> Bool
conPRecord :: Bool
    -- ^ @False@ if data constructor.
    --   @True@ if record constructor.
  , ConPatternInfo -> Bool
conPFallThrough :: Bool
    -- ^ Should the match block on non-canonical terms or can it
    --   proceed to the catch-all clause?
  , ConPatternInfo -> Maybe (Arg Type)
conPType   :: Maybe (Arg Type)
    -- ^ The type of the whole constructor pattern.
    --   Should be present (@Just@) if constructor pattern is
    --   is generated ordinarily by type-checking.
    --   Could be absent (@Nothing@) if pattern comes from some
    --   plugin (like Agsy).
    --   Needed e.g. for with-clause stripping.
  , ConPatternInfo -> Bool
conPLazy :: Bool
    -- ^ Lazy patterns are generated by the forcing translation in the unifier
    --   ('Agda.TypeChecking.Rules.LHS.Unify.unifyStep') and are dropped by
    --   the clause compiler (TODO: not yet)
    --   ('Agda.TypeChecking.CompiledClause.Compile.compileClauses') when the
    --   variables they bind are unused. The GHC backend compiles lazy matches
    --   to lazy patterns in Haskell (TODO: not yet).
  }
  deriving (Int -> ConPatternInfo -> ShowS
[ConPatternInfo] -> ShowS
ConPatternInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ConPatternInfo] -> ShowS
$cshowList :: [ConPatternInfo] -> ShowS
show :: ConPatternInfo -> ArgName
$cshow :: ConPatternInfo -> ArgName
showsPrec :: Int -> ConPatternInfo -> ShowS
$cshowsPrec :: Int -> ConPatternInfo -> ShowS
Show, forall x. Rep ConPatternInfo x -> ConPatternInfo
forall x. ConPatternInfo -> Rep ConPatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConPatternInfo x -> ConPatternInfo
$cfrom :: forall x. ConPatternInfo -> Rep ConPatternInfo x
Generic)

noConPatternInfo :: ConPatternInfo
noConPatternInfo :: ConPatternInfo
noConPatternInfo = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False forall a. Maybe a
Nothing Bool
False

-- | Build partial 'ConPatternInfo' from 'ConInfo'
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ConORec = ConPatternInfo
noConPatternInfo{ conPInfo :: PatternInfo
conPInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatORec [] , conPRecord :: Bool
conPRecord = Bool
True }
toConPatternInfo ConInfo
_ = ConPatternInfo
noConPatternInfo

-- | Build 'ConInfo' from 'ConPatternInfo'.
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
i = PatOrigin -> ConInfo
patToConO forall a b. (a -> b) -> a -> b
$ PatternInfo -> PatOrigin
patOrigin forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i
  where
    patToConO :: PatOrigin -> ConOrigin
    patToConO :: PatOrigin -> ConInfo
patToConO = \case
      PatOrigin
PatOSystem -> ConInfo
ConOSystem
      PatOrigin
PatOSplit  -> ConInfo
ConOSplit
      PatOVar{}  -> ConInfo
ConOSystem
      PatOrigin
PatODot    -> ConInfo
ConOSystem
      PatOrigin
PatOWild   -> ConInfo
ConOSystem
      PatOrigin
PatOCon    -> ConInfo
ConOCon
      PatOrigin
PatORec    -> ConInfo
ConORec
      PatOrigin
PatOLit    -> ConInfo
ConOCon
      PatOrigin
PatOAbsurd -> ConInfo
ConOSystem

-- | Extract pattern variables in left-to-right order.
--   A 'DotP' is also treated as variable (see docu for 'Clause').
class PatternVars a where
  type PatternVarOut a
  patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]

instance PatternVars (Arg (Pattern' a)) where
  type PatternVarOut (Arg (Pattern' a)) = a

  -- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
  patternVars :: Arg (Pattern' a)
-> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
patternVars (Arg ArgInfo
i (VarP PatternInfo
_ a
x)   ) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
x]
  patternVars (Arg ArgInfo
i (DotP PatternInfo
_ Term
t)   ) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Term
t]
  patternVars (Arg ArgInfo
_ (ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps)) = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
  patternVars (Arg ArgInfo
_ (DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps)) = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
  patternVars (Arg ArgInfo
_ (LitP PatternInfo
_ Literal
_)   ) = []
  patternVars (Arg ArgInfo
_ ProjP{}      ) = []
  patternVars (Arg ArgInfo
i (IApplyP PatternInfo
_ Term
_ Term
_ a
x)) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
x]


instance PatternVars (NamedArg (Pattern' a)) where
  type PatternVarOut (NamedArg (Pattern' a)) = a

  patternVars :: NamedArg (Pattern' a)
-> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)]
patternVars = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing

instance PatternVars a => PatternVars [a] where
  type PatternVarOut [a] = PatternVarOut a

  patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)]
patternVars = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars

-- | Retrieve the PatternInfo from a pattern
patternInfo :: Pattern' x -> Maybe PatternInfo
patternInfo :: forall x. Pattern' x -> Maybe PatternInfo
patternInfo (VarP PatternInfo
i x
_)        = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DotP PatternInfo
i Term
_)        = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (LitP PatternInfo
i Literal
_)        = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' x)]
_)     = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
ci
patternInfo ProjP{}           = forall a. Maybe a
Nothing
patternInfo (IApplyP PatternInfo
i Term
_ Term
_ x
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DefP PatternInfo
i QName
_ [NamedArg (Pattern' x)]
_)      = forall a. a -> Maybe a
Just PatternInfo
i

-- | Retrieve the origin of a pattern
patternOrigin :: Pattern' x -> Maybe PatOrigin
patternOrigin :: forall x. Pattern' x -> Maybe PatOrigin
patternOrigin = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PatternInfo -> PatOrigin
patOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Pattern' x -> Maybe PatternInfo
patternInfo

-- | Does the pattern perform a match that could fail?
properlyMatching :: Pattern' a -> Bool
properlyMatching :: forall a. Pattern' a -> Bool
properlyMatching = forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
True Bool
True

properlyMatching'
  :: Bool       -- ^ Should absurd patterns count as proper match?
  -> Bool       -- ^ Should projection patterns count as proper match?
  -> Pattern' a -- ^ The pattern.
  -> Bool
properlyMatching' :: forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
absP Bool
projP = \case
  Pattern' a
p | Bool
absP Bool -> Bool -> Bool
&& forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd -> Bool
True
  ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' a)]
ps    -- record constructors do not count as proper matches themselves
    | ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any (forall a. Pattern' a -> Bool
properlyMatching forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps
    | Bool
otherwise     -> Bool
True
  LitP{}    -> Bool
True
  DefP{}    -> Bool
True
  ProjP{}   -> Bool
projP
  VarP{}    -> Bool
False
  DotP{}    -> Bool
False
  IApplyP{} -> Bool
False

instance IsProjP (Pattern' a) where
  isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP = \case
    ProjP ProjOrigin
o QName
d -> forall a. a -> Maybe a
Just (ProjOrigin
o, QName -> AmbiguousQName
unambiguous QName
d)
    Pattern' a
_ -> forall a. Maybe a
Nothing

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

-- | Substitutions.

data Substitution' a

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

  | EmptyS Impossible
    -- ^ Empty substitution, lifts from the empty context. First argument is @__IMPOSSIBLE__@.
    --   Apply this to closed terms you want to use in a non-empty context.
    --   @Γ ⊢ EmptyS : ()@

  | a :# Substitution' a
    -- ^ Substitution extension, ``cons''.
    --   @
    --     Γ ⊢ u : Aρ   Γ ⊢ ρ : Δ
    --     ----------------------
    --     Γ ⊢ u :# ρ : Δ, A
    --   @

  | Strengthen Impossible !Int (Substitution' a)
    -- ^ Strengthening substitution.  First argument is @__IMPOSSIBLE__@.
    --   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 ρ : Δ, Θ
    --   @

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

type Substitution = Substitution' Term
type PatternSubstitution = Substitution' DeBruijnPattern

infixr 4 :#

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


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

-- | View type as equality type.

data EqualityView
  = EqualityViewType EqualityTypeData
  | OtherType Type -- ^ reduced
  | IdiomType Type -- ^ reduced

data EqualityTypeData = EqualityTypeData
    { EqualityTypeData -> Sort
_eqtSort   :: Sort        -- ^ Sort of this type.
    , EqualityTypeData -> QName
_eqtName   :: QName       -- ^ Builtin EQUALITY.
    , EqualityTypeData -> Args
_eqtParams :: Args        -- ^ Hidden.  Empty or @Level@.
    , EqualityTypeData -> Arg Term
_eqtType   :: Arg Term    -- ^ Hidden.
    , EqualityTypeData -> Arg Term
_eqtLhs    :: Arg Term    -- ^ NotHidden.
    , EqualityTypeData -> Arg Term
_eqtRhs    :: Arg Term    -- ^ NotHidden.
    }

pattern EqualityType
  :: Sort
  -> QName
  -> Args
  -> Arg Term
  -> Arg Term
  -> Arg Term
  -> EqualityView
pattern $bEqualityType :: Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
$mEqualityType :: forall {r}.
EqualityView
-> (Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> r)
-> ((# #) -> r)
-> r
EqualityType{ EqualityView -> Sort
eqtSort, EqualityView -> QName
eqtName, EqualityView -> Args
eqtParams, EqualityView -> Arg Term
eqtType, EqualityView -> Arg Term
eqtLhs, EqualityView -> Arg Term
eqtRhs } =
  EqualityViewType (EqualityTypeData eqtSort eqtName eqtParams eqtType eqtLhs eqtRhs)

-- The COMPLETE pragma is new in GHC 8.2
#if __GLASGOW_HASKELL__ >= 802
{-# COMPLETE EqualityType, OtherType, IdiomType #-}
#endif

isEqualityType :: EqualityView -> Bool
isEqualityType :: EqualityView -> Bool
isEqualityType EqualityType{} = Bool
True
isEqualityType OtherType{}    = Bool
False
isEqualityType IdiomType{}    = Bool
False

-- | View type as path type.

data PathView
  = PathType
    { PathView -> Sort
pathSort  :: Sort     -- ^ Sort of this type.
    , PathView -> QName
pathName  :: QName    -- ^ Builtin PATH.
    , PathView -> Arg Term
pathLevel :: Arg Term -- ^ Hidden
    , PathView -> Arg Term
pathType  :: Arg Term -- ^ Hidden
    , PathView -> Arg Term
pathLhs   :: Arg Term -- ^ NotHidden
    , PathView -> Arg Term
pathRhs   :: Arg Term -- ^ NotHidden
    }
  | OType Type -- ^ reduced

isPathType :: PathView -> Bool
isPathType :: PathView -> Bool
isPathType PathType{} = Bool
True
isPathType OType{}    = Bool
False

data IntervalView
      = IZero
      | IOne
      | IMin (Arg Term) (Arg Term)
      | IMax (Arg Term) (Arg Term)
      | INeg (Arg Term)
      | OTerm Term
      deriving Int -> IntervalView -> ShowS
[IntervalView] -> ShowS
IntervalView -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IntervalView] -> ShowS
$cshowList :: [IntervalView] -> ShowS
show :: IntervalView -> ArgName
$cshow :: IntervalView -> ArgName
showsPrec :: Int -> IntervalView -> ShowS
$cshowsPrec :: Int -> IntervalView -> ShowS
Show

isIOne :: IntervalView -> Bool
isIOne :: IntervalView -> Bool
isIOne IntervalView
IOne = Bool
True
isIOne IntervalView
_ = Bool
False

---------------------------------------------------------------------------
-- * Absurd Lambda
---------------------------------------------------------------------------

-- | Absurd lambdas are internally represented as identity
--   with variable name "()".
absurdBody :: Abs Term
absurdBody :: Abs Term
absurdBody = forall a. ArgName -> a -> Abs a
Abs ArgName
absurdPatternName forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 []

isAbsurdBody :: Abs Term -> Bool
isAbsurdBody :: Abs Term -> Bool
isAbsurdBody (Abs ArgName
x (Var Int
0 [])) = ArgName -> Bool
isAbsurdPatternName ArgName
x
isAbsurdBody Abs Term
_                  = Bool
False

absurdPatternName :: PatVarName
absurdPatternName :: ArgName
absurdPatternName = ArgName
"()"

isAbsurdPatternName :: PatVarName -> Bool
isAbsurdPatternName :: ArgName -> Bool
isAbsurdPatternName ArgName
x = ArgName
x forall a. Eq a => a -> a -> Bool
== ArgName
absurdPatternName

---------------------------------------------------------------------------
-- * Smart constructors
---------------------------------------------------------------------------

-- | An unapplied variable.
var :: Nat -> Term
var :: Int -> Term
var Int
i | Int
i forall a. Ord a => a -> a -> Bool
>= Int
0    = Int -> Elims -> Term
Var Int
i []
      | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Add 'DontCare' is it 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

type DummyTermKind = String

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

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

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

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

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

__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_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 = forall t. ArgName -> Sort' t
DummyS forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> ArgName
dummyLocName

__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_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 = forall t a. Sort' t -> a -> Type'' t a
El (CallStack -> Sort
dummySort CallStack
cs) forall a b. (a -> b) -> a -> b
$ ArgName -> CallStack -> Term
dummyTermWith ArgName
"dummyType" CallStack
cs

__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_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' Term Type
dummyDom = forall a. a -> Dom a
defaultDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Type
dummyType

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

-- | 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 = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [ forall t. Integer -> t -> PlusLevel' t
Plus Integer
0 t
a ]

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

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

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

-- | 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]
as) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
m forall a. Num a => a -> a -> a
+ Integer
n) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map PlusLevel -> PlusLevel
pplus [PlusLevel]
as
  where pplus :: PlusLevel -> PlusLevel
pplus (Plus Integer
n Term
l) = forall t. Integer -> t -> PlusLevel' t
Plus (Integer
m forall a. Num a => a -> a -> a
+ Integer
n) Term
l

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

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

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

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

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

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

---------------------------------------------------------------------------
-- * Telescopes.
---------------------------------------------------------------------------

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

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

-- Ulf, 2013-11-06
-- The record parameter is named "" inside the record module so we can avoid
-- printing it (issue 208), but we don't want that to show up in the type of
-- the functions in the module (issue 892). This function is used on the record
-- module telescope before adding it to a type in
-- TypeChecking.Monad.Signature.addConstant (to handle functions defined in
-- record modules) and TypeChecking.Rules.Record.checkProjection (to handle
-- record projections).
replaceEmptyName :: ArgName -> Tele a -> Tele a
replaceEmptyName :: forall a. ArgName -> Tele a -> Tele a
replaceEmptyName ArgName
x = forall a. ShowS -> Tele a -> Tele a
mapAbsNames forall a b. (a -> b) -> a -> b
$ \ ArgName
y -> if forall a. Null a => a -> Bool
null ArgName
y then ArgName
x else ArgName
y

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

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

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

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

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

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

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

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

-- | Constructing a singleton telescope.
class SgTel a where
  sgTel :: a -> Telescope

instance SgTel (ArgName, Dom Type) where
  sgTel :: (ArgName, Dom' Term Type) -> Telescope
sgTel (ArgName
x, !Dom' Term Type
dom) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
dom forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
x forall a. Tele a
EmptyTel

instance SgTel (Dom (ArgName, Type)) where
  sgTel :: Dom (ArgName, Type) -> Telescope
sgTel Dom (ArgName, Type)
dom = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (ArgName, Type)
dom) forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (ArgName, Type)
dom) forall a. Tele a
EmptyTel

instance SgTel (Dom Type) where
  sgTel :: Dom' Term Type -> Telescope
sgTel Dom' Term Type
dom = forall a. SgTel a => a -> Telescope
sgTel (ShowS
stringToArgName ArgName
"_", Dom' Term Type
dom)

---------------------------------------------------------------------------
-- * Simple operations on terms and types.
---------------------------------------------------------------------------

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

-- | Doesn't do any reduction.
arity :: Type -> Nat
arity :: Type -> Int
arity Type
t = case forall t a. Type'' t a -> a
unEl Type
t of
  Pi  Dom' Term Type
_ Abs Type
b -> Int
1 forall a. Num a => a -> a -> a
+ Type -> Int
arity (forall a. Abs a -> a
unAbs Abs Type
b)
  Term
_       -> Int
0

-- | Suggest a name if available (i.e. name is not "_")
class Suggest a where
  suggestName :: a -> Maybe String

instance Suggest String where
  suggestName :: ArgName -> Maybe ArgName
suggestName ArgName
"_" = forall a. Maybe a
Nothing
  suggestName  ArgName
x  = forall a. a -> Maybe a
Just ArgName
x

instance Suggest (Abs b) where
  suggestName :: Abs b -> Maybe ArgName
suggestName = forall a. Suggest a => a -> Maybe ArgName
suggestName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> ArgName
absName

instance Suggest Name where
  suggestName :: Name -> Maybe ArgName
suggestName = forall a. Suggest a => a -> Maybe ArgName
suggestName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> ArgName
nameToArgName

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

-- Wrapping @forall a. (Suggest a) => a@ into a datatype because
-- GHC doesn't support impredicative polymorphism
data Suggestion = forall a. Suggest a => Suggestion a

suggests :: [Suggestion] -> String
suggests :: [Suggestion] -> ArgName
suggests []     = ArgName
"x"
suggests (Suggestion a
x : [Suggestion]
xs) = forall a. a -> Maybe a -> a
fromMaybe ([Suggestion] -> ArgName
suggests [Suggestion]
xs) forall a b. (a -> b) -> a -> b
$ forall a. Suggest a => a -> Maybe ArgName
suggestName a
x

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

-- | Convert top-level postfix projections into prefix projections.
unSpine :: Term -> Term
unSpine :: Term -> Term
unSpine = (ProjOrigin -> Bool) -> Term -> Term
unSpine' forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True

-- | Convert 'Proj' projection eliminations
--   according to their 'ProjOrigin' into
--   'Def' projection applications.
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
p Term
v =
  case Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v of
    Just (Elims -> Term
h, Elims
es) -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h [] Elims
es
    Maybe (Elims -> Term, Elims)
Nothing      -> Term
v
  where
    loop :: (Elims -> Term) -> Elims -> Elims -> Term
    loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h Elims
res Elims
es =
      case Elims
es of
        []                   -> Term
v
        Proj ProjOrigin
o QName
f : Elims
es' | ProjOrigin -> Bool
p ProjOrigin
o -> (Elims -> Term) -> Elims -> Elims -> Term
loop (QName -> Elims -> Term
Def QName
f) [forall a. Arg a -> Elim' a
Apply (forall a. a -> Arg a
defaultArg Term
v)] Elims
es'
        Elim' Term
e        : Elims
es'       -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h (Elim' Term
e forall a. a -> [a] -> [a]
: Elims
res) Elims
es'
      where v :: Term
v = Elims -> Term
h forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse Elims
res

-- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which
--   can be projected.
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v =
  case Term
v of
    Var   Int
i Elims
es -> forall a. a -> Maybe a
Just (Int -> Elims -> Term
Var   Int
i, Elims
es)
    Def   QName
f Elims
es -> forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def   QName
f, Elims
es)
    MetaV MetaId
x Elims
es -> forall a. a -> Maybe a
Just (MetaId -> Elims -> Term
MetaV MetaId
x, Elims
es)
    Con{}      -> forall a. Maybe a
Nothing
    Lit{}      -> forall a. Maybe a
Nothing
    -- Andreas, 2016-04-13, Issue 1932: We convert λ x → x .f  into f
    Lam ArgInfo
h (Abs ArgName
_ Term
v) | forall a. LensHiding a => a -> Bool
visible ArgInfo
h -> case Term
v of
      Var Int
0 [Proj ProjOrigin
_o QName
f] -> forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def QName
f, [])
      Term
_ -> forall a. Maybe a
Nothing
    Lam{}      -> forall a. Maybe a
Nothing
    Pi{}       -> forall a. Maybe a
Nothing
    Sort{}     -> forall a. Maybe a
Nothing
    Level{}    -> forall a. Maybe a
Nothing
    DontCare{} -> forall a. Maybe a
Nothing
    Dummy{}    -> forall a. Maybe a
Nothing

---------------------------------------------------------------------------
-- * Null instances.
---------------------------------------------------------------------------

instance Null (Tele a) where
  empty :: Tele a
empty = forall a. Tele a
EmptyTel
  null :: Tele a -> Bool
null Tele a
EmptyTel    = Bool
True
  null ExtendTel{} = Bool
False

-- | A 'null' clause is one with no patterns and no rhs.
--   Should not exist in practice.
instance Null Clause where
  empty :: Clause
empty = Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty Bool
False forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Null a => a
empty forall a. Null a => a
empty
  null :: Clause -> Bool
null (Clause Range
_ Range
_ Telescope
tel NAPs
pats Maybe Term
body Maybe (Arg Type)
_ Bool
_ Maybe Bool
_ Maybe Bool
_ Maybe Bool
_ ExpandedEllipsis
_ Maybe ModuleName
wm)
    =  forall a. Null a => a -> Bool
null Telescope
tel
    Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null NAPs
pats
    Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Maybe Term
body
    Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Maybe ModuleName
wm


---------------------------------------------------------------------------
-- * Show instances.
---------------------------------------------------------------------------

instance Show a => Show (Abs a) where
  showsPrec :: Int -> Abs a -> ShowS
showsPrec Int
p (Abs ArgName
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
    ArgName -> ShowS
showString ArgName
"Abs " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows ArgName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ShowS
showString ArgName
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a
  showsPrec Int
p (NoAbs ArgName
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
    ArgName -> ShowS
showString ArgName
"NoAbs " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows ArgName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ShowS
showString ArgName
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a

-- instance Show t => Show (Blocked t) where
--   showsPrec p (Blocked m x) = showParen (p > 0) $
--     showString "Blocked " . shows m . showString " " . showsPrec 10 x
--   showsPrec p (NotBlocked x) = showsPrec p x

---------------------------------------------------------------------------
-- * Sized instances and TermSize.
---------------------------------------------------------------------------

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

instance Sized a => Sized (Abs a) where
  size :: Abs a -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> a
unAbs

-- | The size of a term is roughly the number of nodes in its
--   syntax tree.  This number need not be precise for logical
--   correctness of Agda, it is only used for reporting
--   (and maybe decisions regarding performance).
--
--   Not counting towards the term size are:
--
--     * sort and color annotations,
--     * projections.
--
class TermSize a where
  termSize :: a -> Int
  termSize = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap 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 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Def QName
_ Elims
vs    -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Con ConHead
_ ConInfo
_ Elims
vs    -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    MetaV MetaId
_ Elims
vs  -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
    Level Level
l     -> forall a. TermSize a => a -> Sum Int
tsize Level
l
    Lam ArgInfo
_ Abs Term
f     -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Term
f
    Lit Literal
_       -> Sum Int
1
    Pi Dom' Term Type
a Abs Type
b      -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Dom' Term Type
a forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Type
b
    Sort Sort
s      -> forall a. TermSize a => a -> Sum Int
tsize Sort
s
    DontCare Term
mv -> forall a. TermSize a => a -> Sum Int
tsize Term
mv
    Dummy{}     -> Sum Int
1

instance TermSize Sort where
  tsize :: Sort -> Sum Int
tsize = \case
    Type Level
l    -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
    Prop Level
l    -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
    Inf IsFibrant
_ Integer
_   -> Sum Int
1
    SSet Level
l    -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
    Sort
SizeUniv  -> Sum Int
1
    Sort
LockUniv  -> Sum Int
1
    Sort
IntervalUniv -> Sum Int
1
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Dom' Term Term
a forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Sort
s2
    FunSort Sort
s1 Sort
s2 -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s2
    UnivSort Sort
s -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s
    MetaS MetaId
_ Elims
es -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
es
    DefS QName
_ Elims
es  -> Sum Int
1 forall a. Num a => a -> a -> a
+ 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]
as) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize [PlusLevel]
as

instance TermSize PlusLevel where
  tsize :: PlusLevel -> Sum Int
tsize (Plus Integer
_ Term
a)      = 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 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (a
t :# Substitution' a
rho)           = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize a
t forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (Strengthen Impossible
_ Int
_ Substitution' a
rho) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
  tsize (Lift Int
_ Substitution' a
rho)         = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho

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

instance KillRange DataOrRecord where
  killRange :: KillRangeT DataOrRecord
killRange = forall a. a -> a
id

instance KillRange ConHead where
  killRange :: ConHead -> ConHead
killRange (ConHead QName
c DataOrRecord
d Induction
i [Arg QName]
fs) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
d Induction
i [Arg QName]
fs

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

instance KillRange Level where
  killRange :: Level -> Level
killRange (Max Integer
n [PlusLevel]
as) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) [PlusLevel]
as

instance KillRange PlusLevel where
  killRange :: PlusLevel -> PlusLevel
killRange (Plus Integer
n Term
l) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) Term
l

instance (KillRange a) => KillRange (Type' a) where
  killRange :: KillRangeT (Type' a)
killRange (El Sort
s a
v) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t a. Sort' t -> a -> Type'' t a
El Sort
s a
v

instance KillRange Sort where
  killRange :: Sort -> Sort
killRange = \case
    Inf IsFibrant
f Integer
n    -> forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    Sort
SizeUniv   -> forall t. Sort' t
SizeUniv
    Sort
LockUniv   -> forall t. Sort' t
LockUniv
    Sort
IntervalUniv -> forall t. Sort' t
IntervalUniv
    Type Level
a     -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
Type Level
a
    Prop Level
a     -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
Prop Level
a
    SSet Level
a     -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
SSet Level
a
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2
    FunSort Sort
s1 Sort
s2 -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2
    UnivSort Sort
s -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Sort' t -> Sort' t
UnivSort Sort
s
    MetaS MetaId
x Elims
es -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x) Elims
es
    DefS QName
d Elims
es  -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es
    s :: Sort
s@DummyS{} -> Sort
s

instance KillRange Substitution where
  killRange :: KillRangeT Substitution
killRange Substitution
IdS                    = forall a. Substitution' a
IdS
  killRange (EmptyS Impossible
err)           = forall a. Impossible -> Substitution' a
EmptyS Impossible
err
  killRange (Wk Int
n Substitution
rho)             = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Int -> Substitution' a -> Substitution' a
Wk Int
n) Substitution
rho
  killRange (Term
t :# Substitution
rho)             = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall a. a -> Substitution' a -> Substitution' a
(:#) Term
t Substitution
rho
  killRange (Strengthen Impossible
err Int
n Substitution
rho) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
err Int
n) Substitution
rho
  killRange (Lift Int
n Substitution
rho)           = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Int -> Substitution' a -> Substitution' a
Lift Int
n) Substitution
rho

instance KillRange PatOrigin where
  killRange :: KillRangeT PatOrigin
killRange = forall a. a -> a
id

instance KillRange PatternInfo where
  killRange :: KillRangeT PatternInfo
killRange (PatternInfo PatOrigin
o [Name]
xs) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
o [Name]
xs

instance KillRange ConPatternInfo where
  killRange :: KillRangeT ConPatternInfo
killRange (ConPatternInfo PatternInfo
i Bool
mr Bool
b Maybe (Arg Type)
mt Bool
lz) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
i Bool
mr Bool
b) Maybe (Arg Type)
mt Bool
lz

instance KillRange DBPatVar where
  killRange :: KillRangeT DBPatVar
killRange (DBPatVar ArgName
x Int
i) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ArgName -> Int -> DBPatVar
DBPatVar ArgName
x Int
i

instance KillRange a => KillRange (Pattern' a) where
  killRange :: KillRangeT (Pattern' a)
killRange Pattern' a
p =
    case Pattern' a
p of
      VarP PatternInfo
o a
x         -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o a
x
      DotP PatternInfo
o Term
v         -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
v
      ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps
      LitP PatternInfo
o Literal
l         -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
      ProjP ProjOrigin
o QName
q        -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o) QName
q
      IApplyP PatternInfo
o Term
u Term
t a
x  -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 (forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o) Term
u Term
t a
x
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps      -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 (forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o) QName
q [NamedArg (Pattern' a)]
ps

instance KillRange Clause where
  killRange :: KillRangeT Clause
killRange (Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
    forall a b c d e f g h i j k l.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f, KillRange g, KillRange h, KillRange i, KillRange j,
 KillRange k) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
killRange11 Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm

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

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

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

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

instance Pretty a => Pretty (Substitution' a) where
  prettyPrec :: Int -> Substitution' a -> Doc
prettyPrec = 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
"idS"
      EmptyS Impossible
err         -> Doc
"emptyS"
      a
t :# Substitution' a
rho           -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
2) forall a b. (a -> b) -> a -> b
$
                            forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ t -> Substitution' a -> Doc
pr t
2 Substitution' a
rho forall a. Semigroup a => a -> a -> 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 forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$
                            ArgName -> Doc
text (ArgName
"strS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n) Doc -> Doc -> Doc
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
      Wk Int
n Substitution' a
rho           -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$
                            ArgName -> Doc
text (ArgName
"wkS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n) Doc -> Doc -> Doc
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
      Lift Int
n Substitution' a
rho         -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$
                            ArgName -> Doc
text (ArgName
"liftS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n) Doc -> Doc -> Doc
<+> 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 -> ArgName -> Doc
text (ArgName
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
x) Doc -> Elims -> Doc
`pApp` Elims
els
      Lam ArgInfo
ai Abs Term
b   ->
        Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"λ" Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
ai forall a. a -> a
id (ArgName -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> ArgName
absName forall a b. (a -> b) -> a -> b
$ Abs Term
b) Doc -> Doc -> Doc
<+> Doc
"->"
            , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Term
b) ]
      Lit Literal
l                -> forall a. Pretty a => a -> Doc
pretty Literal
l
      Def QName
q Elims
els            -> forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Elims -> Doc
`pApp` Elims
els
      Con ConHead
c ConInfo
ci Elims
vs          -> forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c) Doc -> Elims -> Doc
`pApp` Elims
vs
      Pi Dom' Term Type
a (NoAbs ArgName
_ Type
b)     -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 (forall t e. Dom' t e -> e
unDom Dom' Term Type
a) Doc -> Doc -> Doc
<+> Doc
"->"
            , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Type
b ]
      Pi Dom' Term Type
a Abs Type
b               -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. LensHiding a => a -> Doc -> Doc
pDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
a) (ArgName -> Doc
text (forall a. Abs a -> ArgName
absName Abs Type
b) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom' Term Type
a)) Doc -> Doc -> Doc
<+> Doc
"->"
            , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Type
b) ]
      Sort Sort
s      -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Sort
s
      Level Level
l     -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Level
l
      MetaV MetaId
x Elims
els -> forall a. Pretty a => a -> Doc
pretty MetaId
x Doc -> Elims -> Doc
`pApp` Elims
els
      DontCare Term
v  -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
v
      Dummy ArgName
s Elims
es  -> Doc -> Doc
parens (ArgName -> Doc
text ArgName
s) Doc -> Elims -> Doc
`pApp` Elims
es
    where
      pApp :: Doc -> Elims -> Doc
pApp Doc
d Elims
els = Bool -> Doc -> Doc
mparens (Bool -> Bool
not (forall a. Null a => a -> Bool
null Elims
els) Bool -> Bool -> Bool
&& Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
                   forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
d, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) Elims
els)]

instance Pretty t => Pretty (Abs t) where
  pretty :: Abs t -> Doc
pretty (Abs   ArgName
x t
t) = Doc
"Abs"   Doc -> Doc -> Doc
<+> (ArgName -> Doc
text ArgName
x forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t
  pretty (NoAbs ArgName
x t
t) = Doc
"NoAbs" Doc -> Doc -> Doc
<+> (ArgName -> Doc
text ArgName
x forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t

instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
  pretty :: Dom' t e -> Doc
pretty Dom' t e
dom = Doc
pTac Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> Doc -> Doc
pDom Dom' t e
dom (forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t e
dom)
    where
      pTac :: Doc
pTac | Just t
t <- forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Doc
"@" forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc
"tactic" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t)
           | Bool
otherwise               = forall a. Null a => a
empty

pDom :: LensHiding a => a -> Doc -> Doc
pDom :: forall a. LensHiding a => a -> Doc -> Doc
pDom a
i =
  case forall a. LensHiding a => a -> Hiding
getHiding a
i of
    Hiding
NotHidden  -> Doc -> Doc
parens
    Hiding
Hidden     -> Doc -> Doc
braces
    Instance{} -> Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
braces

instance Pretty Clause where
  pretty :: Clause -> Doc
pretty Clause{clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
b, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
t} =
    forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty Telescope
tel Doc -> Doc -> Doc
<+> Doc
"|-"
        , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) NAPs
ps) Doc -> Doc -> Doc
<+> Doc
"="
                       , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall {a} {a}. (Pretty a, Pretty a) => Maybe a -> Maybe a -> Doc
pBody Maybe Term
b Maybe (Arg Type)
t ] ]
    where
      pBody :: Maybe a -> Maybe a -> Doc
pBody Maybe a
Nothing Maybe a
_ = Doc
"(absurd)"
      pBody (Just a
b) Maybe a
Nothing  = forall a. Pretty a => a -> Doc
pretty a
b
      pBody (Just a
b) (Just a
t) = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty a
b Doc -> Doc -> Doc
<+> Doc
":", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty a
t ]

instance Pretty a => Pretty (Tele (Dom a)) where
  pretty :: Tele (Dom a) -> Doc
pretty Tele (Dom a)
tel = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [ forall a. LensHiding a => a -> Doc -> Doc
pDom Dom a
a (ArgName -> Doc
text ArgName
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom a
a)) | (ArgName
x, Dom a
a) <- forall {b}. Tele b -> [(ArgName, b)]
telToList Tele (Dom a)
tel ]
    where
      telToList :: Tele b -> [(ArgName, b)]
telToList Tele b
EmptyTel = []
      telToList (ExtendTel b
a Abs (Tele b)
tel) = (forall a. Abs a -> ArgName
absName Abs (Tele b)
tel, b
a) forall a. a -> [a] -> [a]
: Tele b -> [(ArgName, b)]
telToList (forall a. Abs a -> a
unAbs Abs (Tele b)
tel)

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

instance Pretty PlusLevel where
  prettyPrec :: Int -> PlusLevel -> Doc
prettyPrec Int
p (Plus Integer
n Term
a) = Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
n forall a b. (a -> b) -> a -> b
$ \Int
p -> 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
      Type (ClosedLevel Integer
0) -> Doc
"Set"
      Type (ClosedLevel Integer
n) -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"Set" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
      Type Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"Set" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
      Prop (ClosedLevel Integer
0) -> Doc
"Prop"
      Prop (ClosedLevel Integer
n) -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"Prop" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
      Prop Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"Prop" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
      Inf IsFibrant
f Integer
0 -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ IsFibrant -> ShowS
addS IsFibrant
f ArgName
"Setω"
      Inf IsFibrant
f Integer
n -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ IsFibrant -> ShowS
addS IsFibrant
f ArgName
"Setω" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
      SSet Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"SSet" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
      Sort
SizeUniv -> Doc
"SizeUniv"
      Sort
LockUniv -> Doc
"LockUniv"
      Sort
IntervalUniv -> Doc
"IntervalUniv"
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
        Doc
"piSort" Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> Doc -> Doc
pDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Term
a) (ArgName -> Doc
text (forall a. Abs a -> ArgName
absName Abs Sort
s2) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom' Term Term
a) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Sort
s1)
                      Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Sort
s2))
      FunSort Sort
a Sort
b -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
        Doc
"funSort" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
a Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
b
      UnivSort Sort
s -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"univSort" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
s
      MetaS MetaId
x Elims
es -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      DefS QName
d Elims
es  -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      DummyS ArgName
s   -> Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ ArgName -> Doc
text ArgName
s
   where
     addS :: IsFibrant -> ShowS
addS IsFibrant
IsFibrant ArgName
t = ArgName
t
     addS IsFibrant
IsStrict  ArgName
t = ArgName
"S" forall a. [a] -> [a] -> [a]
++ ArgName
t

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

instance Pretty DBPatVar where
  prettyPrec :: Int -> DBPatVar -> Doc
prettyPrec Int
_ DBPatVar
x = ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ShowS
patVarNameToString (DBPatVar -> ArgName
dbPatVarName DBPatVar
x) forall a. [a] -> [a] -> [a]
++ ArgName
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (DBPatVar -> Int
dbPatVarIndex DBPatVar
x)

instance Pretty a => Pretty (Pattern' a) where
  prettyPrec :: Int -> Pattern' a -> Doc
prettyPrec Int
n (VarP PatternInfo
_o a
x)   = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x
  prettyPrec Int
_ (DotP PatternInfo
_o Term
t)   = Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Term
t
  prettyPrec Int
n (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
nps)= Bool -> Doc -> Doc
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
    (Doc
lazy forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c)) Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
          lazy :: Doc
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Doc
"~"
               | Bool
otherwise  = forall a. Null a => a
empty
  prettyPrec Int
n (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
nps)= Bool -> Doc -> Doc
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
    forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
  -- -- Version with printing record type:
  -- prettyPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
  --   text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
  --   where
  --     b = maybe False (== ConOSystem) $ conPRecord i
  --     prTy d = caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> pretty t
  prettyPrec Int
_ (LitP PatternInfo
_ Literal
l)    = forall a. Pretty a => a -> Doc
pretty Literal
l
  prettyPrec Int
_ (ProjP ProjOrigin
_o QName
q)  = ArgName -> Doc
text (ArgName
"." forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
q)
  prettyPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x
--  prettyPrec n (IApplyP _o u0 u1 x) = text "@[" <> prettyPrec 0 u0 <> text ", " <> prettyPrec 0 u1 <> text "]" <> prettyPrec n x

instance Pretty a => Pretty (Blocked a) where
  pretty :: Blocked a -> Doc
pretty (Blocked Blocker
x a
a) = (Doc
"[" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty a
a Doc -> Doc -> Doc
<+> Doc
"]") forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty Blocker
x
  pretty (NotBlocked NotBlocked' Term
_ a
x) = forall a. Pretty a => a -> Doc
pretty a
x

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

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

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

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

instance NFData Sort where
  rnf :: Sort -> ()
rnf = \case
    Type Level
l   -> forall a. NFData a => a -> ()
rnf Level
l
    Prop Level
l   -> forall a. NFData a => a -> ()
rnf Level
l
    Inf IsFibrant
_ Integer
_  -> ()
    SSet Level
l   -> forall a. NFData a => a -> ()
rnf Level
l
    Sort
SizeUniv -> ()
    Sort
LockUniv -> ()
    Sort
IntervalUniv -> ()
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall a. NFData a => a -> ()
rnf (Dom' Term Term
a, Sort
b, forall a. Abs a -> a
unAbs Abs Sort
c)
    FunSort Sort
a Sort
b -> forall a. NFData a => a -> ()
rnf (Sort
a, Sort
b)
    UnivSort Sort
a -> forall a. NFData a => a -> ()
rnf Sort
a
    MetaS MetaId
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
    DefS QName
_ Elims
es  -> forall a. NFData a => a -> ()
rnf Elims
es
    DummyS ArgName
_   -> ()

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

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

instance NFData e => NFData (Dom e) where
  rnf :: Dom e -> ()
rnf (Dom ArgInfo
a Maybe (WithOrigin (Ranged ArgName))
c Bool
d Maybe Term
e e
f) = forall a. NFData a => a -> ()
rnf ArgInfo
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe (WithOrigin (Ranged ArgName))
c seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Bool
d seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe Term
e seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf e
f

instance NFData DataOrRecord
instance NFData ConHead
instance NFData a => NFData (Abs a)
instance NFData a => NFData (Tele a)
instance NFData IsFibrant
instance NFData Clause
instance NFData PatternInfo
instance NFData PatOrigin
instance NFData x => NFData (Pattern' x)
instance NFData DBPatVar
instance NFData ConPatternInfo
instance NFData a => NFData (Substitution' a)