{-# LANGUAGE CPP #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wunused-imports #-}
-- {-# OPTIONS_GHC -Wunused-matches #-}

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

import Prelude hiding (null)

import Control.Monad.Identity
import Control.DeepSeq
import GHC.Exts

import qualified Data.List as List
import Data.Maybe
import Data.Semigroup ( Sum(..) )
import System.IO.Unsafe (unsafePerformIO)

import GHC.Generics (Generic)

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal.Blockers
import Agda.Syntax.Internal.Elim
import Agda.Syntax.Internal.Univ
import Agda.Syntax.Common.Pretty

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

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

import Agda.Utils.Impossible

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

data RewDom' t = RewDom
  { forall t. RewDom' t -> LocalEquation' t
rewDomEq  :: LocalEquation' t
    -- ^ Elaborated "@rewrite" equation
  , forall t. RewDom' t -> Maybe RewriteRule
rewDomRew :: Maybe RewriteRule
    -- ^ "@rewrite" equation transformed into a directed rewrite rule.
    --
    -- @Nothing@ iff invalidated by a substitution. If we are checking
    -- against an "@rewrite" domain, this is fine, but if we are inside an "@rewrite"
    -- context, this is probably an internal error.
  } deriving (Int -> RewDom' t -> ShowS
[RewDom' t] -> ShowS
RewDom' t -> [Char]
(Int -> RewDom' t -> ShowS)
-> (RewDom' t -> [Char])
-> ([RewDom' t] -> ShowS)
-> Show (RewDom' t)
forall t. Show t => Int -> RewDom' t -> ShowS
forall t. Show t => [RewDom' t] -> ShowS
forall t. Show t => RewDom' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> RewDom' t -> ShowS
showsPrec :: Int -> RewDom' t -> ShowS
$cshow :: forall t. Show t => RewDom' t -> [Char]
show :: RewDom' t -> [Char]
$cshowList :: forall t. Show t => [RewDom' t] -> ShowS
showList :: [RewDom' t] -> ShowS
Show, (forall x. RewDom' t -> Rep (RewDom' t) x)
-> (forall x. Rep (RewDom' t) x -> RewDom' t)
-> Generic (RewDom' t)
forall x. Rep (RewDom' t) x -> RewDom' t
forall x. RewDom' t -> Rep (RewDom' t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (RewDom' t) x -> RewDom' t
forall t x. RewDom' t -> Rep (RewDom' t) x
$cfrom :: forall t x. RewDom' t -> Rep (RewDom' t) x
from :: forall x. RewDom' t -> Rep (RewDom' t) x
$cto :: forall t x. Rep (RewDom' t) x -> RewDom' t
to :: forall x. Rep (RewDom' t) x -> RewDom' t
Generic)

type RewDom = RewDom' Term

data DomInfo t = DomInfo {
    forall t. DomInfo t -> ArgInfo
domInfoArgInfo  :: ArgInfo
  , forall t. DomInfo t -> Maybe NamedName
domInfoName     :: (Maybe NamedName)
  -- ^ e.g. @x@ in @{x = y : A} -> B@.
  , forall t. DomInfo t -> Bool
domInfoIsFinite :: Bool
  -- ^ Is this a Π-type (False), or a partial type (True)?
  , forall t. DomInfo t -> Maybe t
domInfoTactic   :: (Maybe t)
  -- ^ "@tactic e".
  , forall t. DomInfo t -> Maybe (RewDom' t)
domInfoRew      :: (Maybe (RewDom' t))
  -- ^ Elaborated "@rewrite" equation
  --
  -- Will only be present if domain annotated with "@rewrite" (@annRewrite@
  -- is @IsRewrite@) AND the type successfully elaborated into a rewrite rule.
  }

instance Show t => Show (DomInfo t) where
  show :: DomInfo t -> [Char]
show (DomInfo ArgInfo
a Maybe NamedName
b Bool
c Maybe t
d Maybe (RewDom' t)
e) = (ArgInfo, Maybe NamedName, Bool, Maybe t, Maybe (RewDom' t))
-> [Char]
forall a. Show a => a -> [Char]
show (ArgInfo
a,Maybe NamedName
b,Bool
c,Maybe t
d,Maybe (RewDom' t)
e)

{-# INLINE domInfo #-}
domInfo :: Dom' t e -> ArgInfo
domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo Dom' t e
d = DomInfo t -> ArgInfo
forall t. DomInfo t -> ArgInfo
domInfoArgInfo (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
d)

{-# INLINE dInfo #-}
dInfo :: Lens' (Dom' t e) ArgInfo
dInfo :: forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo = \ArgInfo -> f ArgInfo
f Dom' t e
d ->
  ArgInfo -> f ArgInfo
f (Dom' t e -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' t e
d) f ArgInfo -> (ArgInfo -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ArgInfo
x -> Dom' t e
d {domDomInfo = (domDomInfo d){domInfoArgInfo = x}}

{-# INLINE domName #-}
domName :: Dom' t e -> Maybe NamedName
domName :: forall t e. Dom' t e -> Maybe NamedName
domName Dom' t e
d = DomInfo t -> Maybe NamedName
forall t. DomInfo t -> Maybe NamedName
domInfoName (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
d)

{-# INLINE dName #-}
dName :: Lens' (Dom' t e) (Maybe NamedName)
dName :: forall t e (f :: * -> *).
Functor f =>
(Maybe NamedName -> f (Maybe NamedName))
-> Dom' t e -> f (Dom' t e)
dName = \Maybe NamedName -> f (Maybe NamedName)
f Dom' t e
d ->
  Maybe NamedName -> f (Maybe NamedName)
f (Dom' t e -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
domName Dom' t e
d) f (Maybe NamedName)
-> (Maybe NamedName -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Maybe NamedName
x -> Dom' t e
d {domDomInfo = (domDomInfo d){domInfoName = x}}

{-# INLINE domIsFinite #-}
domIsFinite :: Dom' t e -> Bool
domIsFinite :: forall t e. Dom' t e -> Bool
domIsFinite Dom' t e
d =
  DomInfo t -> Bool
forall t. DomInfo t -> Bool
domInfoIsFinite (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
d)

{-# INLINE dIsFinite #-}
dIsFinite :: Lens' (Dom' t e) Bool
dIsFinite :: forall t e (f :: * -> *).
Functor f =>
(Bool -> f Bool) -> Dom' t e -> f (Dom' t e)
dIsFinite = \Bool -> f Bool
f Dom' t e
d ->
  Bool -> f Bool
f (Dom' t e -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom' t e
d) f Bool -> (Bool -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Bool
x -> Dom' t e
d {domDomInfo = (domDomInfo d){domInfoIsFinite = x}}

{-# INLINE domTactic #-}
domTactic :: Dom' t e -> Maybe t
domTactic :: forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
d =
  DomInfo t -> Maybe t
forall t. DomInfo t -> Maybe t
domInfoTactic (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
d)

{-# INLINE dTactic #-}
dTactic :: Lens' (Dom' t e) (Maybe t)
dTactic :: forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic = \Maybe t -> f (Maybe t)
f Dom' t e
d ->
  Maybe t -> f (Maybe t)
f (Dom' t e -> Maybe t
forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
d) f (Maybe t) -> (Maybe t -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Maybe t
x -> Dom' t e
d {domDomInfo = (domDomInfo d){domInfoTactic = x}}

{-# INLINE rewDom #-}
rewDom :: Dom' t e -> Maybe (RewDom' t)
rewDom :: forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom' t e
d =
  DomInfo t -> Maybe (RewDom' t)
forall t. DomInfo t -> Maybe (RewDom' t)
domInfoRew (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
d)

{-# INLINE dRew #-}
dRew :: Lens' (Dom' t e) (Maybe (RewDom' t))
dRew :: forall t e (f :: * -> *).
Functor f =>
(Maybe (RewDom' t) -> f (Maybe (RewDom' t)))
-> Dom' t e -> f (Dom' t e)
dRew = \Maybe (RewDom' t) -> f (Maybe (RewDom' t))
f Dom' t e
d ->
  Maybe (RewDom' t) -> f (Maybe (RewDom' t))
f (Dom' t e -> Maybe (RewDom' t)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom' t e
d) f (Maybe (RewDom' t))
-> (Maybe (RewDom' t) -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Maybe (RewDom' t)
x -> Dom' t e
d {domDomInfo = (domDomInfo d){domInfoRew = x}}

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

pattern Dom :: ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> Maybe (RewDom' t) -> e -> Dom' t e
pattern $mDom :: forall {r} {t} {e}.
Dom' t e
-> (ArgInfo
    -> Maybe NamedName
    -> Bool
    -> Maybe t
    -> Maybe (RewDom' t)
    -> e
    -> r)
-> ((# #) -> r)
-> r
$bDom :: forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom a b c d e f = Dom' (DomInfo a b c d e) f
{-# INLINE Dom #-}
{-# COMPLETE Dom #-}

instance Functor (Dom' t) where
  {-# INLINE fmap #-}
  fmap :: forall a b. (a -> b) -> Dom' t a -> Dom' t b
fmap a -> b
fn = \(Dom ArgInfo
a Maybe NamedName
b Bool
c Maybe t
d Maybe (RewDom' t)
e a
f) -> ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> b
-> Dom' t b
forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom ArgInfo
a Maybe NamedName
b Bool
c Maybe t
d Maybe (RewDom' t)
e (b -> Dom' t b) -> b -> Dom' t b
forall a b. (a -> b) -> a -> b
$! a -> b
fn a
f

type Dom = Dom' Term

{-# INLINE domEq #-}
domEq :: Dom' t e -> Maybe (LocalEquation' t)
domEq :: forall t e. Dom' t e -> Maybe (LocalEquation' t)
domEq = (RewDom' t -> LocalEquation' t)
-> Maybe (RewDom' t) -> Maybe (LocalEquation' t)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RewDom' t -> LocalEquation' t
forall t. RewDom' t -> LocalEquation' t
rewDomEq (Maybe (RewDom' t) -> Maybe (LocalEquation' t))
-> (Dom' t e -> Maybe (RewDom' t))
-> Dom' t e
-> Maybe (LocalEquation' t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t e -> Maybe (RewDom' t)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom

-- | Is this Dom annotated as a local rewrite rule and if so, has the rewrite
--   been invalidated due to a substitution?
invalidRew :: Dom' t e -> Bool
invalidRew :: forall t e. Dom' t e -> Bool
invalidRew Dom' t e
d = case Dom' t e -> Maybe (RewDom' t)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom' t e
d of
  Just (RewDom {rewDomRew :: forall t. RewDom' t -> Maybe RewriteRule
rewDomRew = Maybe RewriteRule
Nothing}) -> Bool
True
  Maybe (RewDom' t)
_                                   -> Bool
False


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 NamedName
x Bool
t Maybe t
b Maybe (RewDom' t)
r a
a) = ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> b
-> Dom' t b
forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom ArgInfo
ai Maybe NamedName
x Bool
t Maybe t
b Maybe (RewDom' t)
r (b -> Dom' t b) -> m b -> m (Dom' 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 = a -> Range
forall a. HasRange a => a -> Range
getRange (a -> Range) -> (Dom' t a -> a) -> Dom' t a -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t a -> a
forall t e. Dom' t e -> e
unDom

instance KillRange t => KillRange (RewDom' t) where
  killRange :: KillRangeT (RewDom' t)
killRange (RewDom LocalEquation' t
eq Maybe RewriteRule
rew) = (LocalEquation' t -> Maybe RewriteRule -> RewDom' t)
-> LocalEquation' t -> Maybe RewriteRule -> RewDom' t
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LocalEquation' t -> Maybe RewriteRule -> RewDom' t
forall t. LocalEquation' t -> Maybe RewriteRule -> RewDom' t
RewDom LocalEquation' t
eq Maybe RewriteRule
rew

instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
  killRange :: KillRangeT (Dom' t a)
killRange (Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b Maybe (RewDom' t)
r a
a) = (ArgInfo
 -> Maybe NamedName
 -> Bool
 -> Maybe t
 -> Maybe (RewDom' t)
 -> a
 -> Dom' t a)
-> ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> a
-> Dom' t a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> a
-> Dom' t a
forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b Maybe (RewDom' t)
r 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 NamedName
s1 Bool
f1 Maybe t
_ Maybe (RewDom' t)
_ a
x1 == :: Dom' t a -> Dom' t a -> Bool
== Dom (ArgInfo Hiding
h2 Modality
m2 Origin
_ FreeVariables
_ Annotation
a2) Maybe NamedName
s2 Bool
f2 Maybe t
_ Maybe (RewDom' t)
_ a
x2 =
    (Hiding
h1, Modality
m1, Annotation
a1, Maybe NamedName
s1, Bool
f1, a
x1) (Hiding, Modality, Annotation, Maybe NamedName, Bool, a)
-> (Hiding, Modality, Annotation, Maybe NamedName, Bool, a) -> Bool
forall a. Eq a => a -> a -> Bool
== (Hiding
h2, Modality
m2, Annotation
a2, Maybe NamedName
s2, Bool
f2, a
x2)

instance LensNamed (Dom' t e) where
  type NameOf (Dom' t e) = NamedName
  {-# INLINE lensNamed #-}
  lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (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 (Dom' t e -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
domName Dom' t e
dom) f (Maybe NamedName)
-> (Maybe NamedName -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Maybe NamedName
nm -> Dom' t e
dom { domDomInfo = (domDomInfo dom){domInfoName = nm }}

instance LensArgInfo (Dom' t e) where
  getArgInfo :: Dom' t e -> ArgInfo
getArgInfo        = Dom' t e -> ArgInfo
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 { domDomInfo = (domDomInfo dom) {domInfoArgInfo = ai} }

instance LensLock (Dom' t e) where
  getLock :: Dom' t e -> Lock
getLock = ArgInfo -> Lock
forall a. LensLock a => a -> Lock
getLock (ArgInfo -> Lock) -> (Dom' t e -> ArgInfo) -> Dom' t e -> Lock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t e -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo
  setLock :: Lock -> Dom' t e -> Dom' t e
setLock = (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ((ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e)
-> (Lock -> ArgInfo -> ArgInfo) -> Lock -> Dom' t e -> Dom' t e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lock -> ArgInfo -> ArgInfo
forall a. LensLock a => Lock -> a -> a
setLock

instance LensRewriteAnn (Dom' t e) where
  getRewriteAnn :: Dom' t e -> RewriteAnn
getRewriteAnn = ArgInfo -> RewriteAnn
forall a. LensRewriteAnn a => a -> RewriteAnn
getRewriteAnn (ArgInfo -> RewriteAnn)
-> (Dom' t e -> ArgInfo) -> Dom' t e -> RewriteAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t e -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo
  setRewriteAnn :: RewriteAnn -> Dom' t e -> Dom' t e
setRewriteAnn = (RewriteAnn -> RewriteAnn) -> Dom' t e -> Dom' t e
forall a. LensRewriteAnn a => (RewriteAnn -> RewriteAnn) -> a -> a
mapRewriteAnn ((RewriteAnn -> RewriteAnn) -> Dom' t e -> Dom' t e)
-> (RewriteAnn -> RewriteAnn -> RewriteAnn)
-> RewriteAnn
-> Dom' t e
-> Dom' t e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteAnn -> RewriteAnn -> RewriteAnn
forall a. LensRewriteAnn a => RewriteAnn -> a -> a
setRewriteAnn

instance LensLocalEquation (Dom e) where
  getLocalEq :: Dom e -> Maybe LocalEquation
getLocalEq = Dom e -> Maybe LocalEquation
forall t e. Dom' t e -> Maybe (LocalEquation' t)
domEq

-- 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
instance LensModalPolarity (Dom' t e) where

argFromDom :: Dom' t a -> Arg a
argFromDom :: forall t a. Dom' t a -> Arg a
argFromDom Dom' t a
d = let !i :: ArgInfo
i = Dom' t a -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' t a
d in ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Dom' t a -> a
forall t e. Dom' t e -> e
unDom Dom' t a
d)

namedArgFromDom :: Dom' t a -> NamedArg a
namedArgFromDom :: forall t a. Dom' t a -> NamedArg a
namedArgFromDom Dom' t a
d =
  let !i :: ArgInfo
i = Dom' t a -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' t a
d
      !s :: Maybe NamedName
s = Dom' t a -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
domName Dom' t a
d
  in ArgInfo -> Named_ a -> Arg (Named_ a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Named_ a -> Arg (Named_ a)) -> Named_ a -> Arg (Named_ a)
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
s (Dom' t a -> a
forall t e. Dom' t e -> e
unDom Dom' t a
d)

-- 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.

domFromArgRew :: Maybe RewDom -> Arg a -> Dom a
domFromArgRew :: forall a. Maybe RewDom -> Arg a -> Dom a
domFromArgRew Maybe RewDom
rew (Arg ArgInfo
i a
a) = ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe Term
-> Maybe RewDom
-> a
-> Dom' Term a
forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom ArgInfo
i Maybe NamedName
forall a. Maybe a
Nothing Bool
False Maybe Term
forall a. Maybe a
Nothing Maybe RewDom
rew a
a

domFromArg :: Arg a -> Dom a
domFromArg :: forall a. Arg a -> Dom a
domFromArg = Maybe RewDom -> Arg a -> Dom a
forall a. Maybe RewDom -> Arg a -> Dom a
domFromArgRew Maybe RewDom
forall a. Maybe a
Nothing

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

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

defaultArgDomRew :: ArgInfo -> Maybe RewDom -> a -> Dom a
defaultArgDomRew :: forall a. ArgInfo -> Maybe RewDom -> a -> Dom a
defaultArgDomRew ArgInfo
info Maybe RewDom
rew a
x = Maybe RewDom -> Arg a -> Dom a
forall a. Maybe RewDom -> Arg a -> Dom a
domFromArgRew Maybe RewDom
rew (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
x)

defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom :: forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info = ArgInfo -> Maybe RewDom -> a -> Dom a
forall a. ArgInfo -> Maybe RewDom -> a -> Dom a
defaultArgDomRew ArgInfo
info Maybe RewDom
forall a. Maybe a
Nothing

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom :: forall a. ArgInfo -> [Char] -> a -> Dom a
defaultNamedArgDom ArgInfo
info ([Char] -> Ranged [Char]
forall a. a -> Ranged a
unranged -> !Ranged [Char]
s) a
x =
  ASetter
  (Dom' Term a) (Dom' Term a) (Maybe NamedName) (Maybe NamedName)
-> Maybe NamedName -> Dom' Term a -> Dom' Term a
forall s t a b. ASetter s t a b -> b -> s -> t
set (Maybe (NameOf (Dom' Term a))
 -> Identity (Maybe (NameOf (Dom' Term a))))
-> Dom' Term a -> Identity (Dom' Term a)
ASetter
  (Dom' Term a) (Dom' Term a) (Maybe NamedName) (Maybe NamedName)
forall a. LensNamed a => Lens' a (Maybe (NameOf a))
Lens' (Dom' Term a) (Maybe (NameOf (Dom' Term a)))
lensNamed (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged [Char] -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted Ranged [Char]
s) (ArgInfo -> a -> Dom' Term a
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x)

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

-- | 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 -> [Char]
(Int -> ConHead -> ShowS)
-> (ConHead -> [Char]) -> ([ConHead] -> ShowS) -> Show ConHead
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConHead -> ShowS
showsPrec :: Int -> ConHead -> ShowS
$cshow :: ConHead -> [Char]
show :: ConHead -> [Char]
$cshowList :: [ConHead] -> ShowS
showList :: [ConHead] -> ShowS
Show, (forall x. ConHead -> Rep ConHead x)
-> (forall x. Rep ConHead x -> ConHead) -> Generic ConHead
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
$cfrom :: forall x. ConHead -> Rep ConHead x
from :: forall x. ConHead -> Rep ConHead x
$cto :: forall x. Rep ConHead x -> ConHead
to :: forall x. Rep ConHead x -> ConHead
Generic)

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

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

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

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

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

instance CopatternMatchingAllowed ConHead where
  copatternMatchingAllowed :: ConHead -> Bool
copatternMatchingAllowed = DataOrRecord -> Bool
forall a. CopatternMatchingAllowed a => a -> Bool
copatternMatchingAllowed (DataOrRecord -> Bool)
-> (ConHead -> DataOrRecord) -> ConHead -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> DataOrRecord
conDataRecord

class LensConName a where
  getConName :: a -> QName
  setConName :: QName -> a -> a
  setConName = (QName -> QName) -> a -> a
forall a. LensConName a => (QName -> QName) -> a -> a
mapConName ((QName -> QName) -> a -> a)
-> (QName -> QName -> QName) -> QName -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName -> QName
forall a b. a -> b -> a
const
  mapConName :: (QName -> QName) -> a -> a
  mapConName QName -> QName
f a
a = QName -> a -> a
forall a. LensConName a => QName -> a -> a
setConName (QName -> QName
f (a -> QName
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 = c }


-- | Terms used for internal purposes
data DummyTermKind
  = DummyNamed      String
  -- ^ Generic dummy term, the 'String' generally describes where the
  -- term was generated (as well as giving a disambiguator).
  --
  -- Should not be used to convey actual information.

  | DummyBrave Term
  -- ^ Collects applications to a 'BraveTerm'.
  deriving Int -> DummyTermKind -> ShowS
[DummyTermKind] -> ShowS
DummyTermKind -> [Char]
(Int -> DummyTermKind -> ShowS)
-> (DummyTermKind -> [Char])
-> ([DummyTermKind] -> ShowS)
-> Show DummyTermKind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DummyTermKind -> ShowS
showsPrec :: Int -> DummyTermKind -> ShowS
$cshow :: DummyTermKind -> [Char]
show :: DummyTermKind -> [Char]
$cshowList :: [DummyTermKind] -> ShowS
showList :: [DummyTermKind] -> ShowS
Show

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

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

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

{-# NOINLINE varTable #-}
varTable :: AL.Array Term
varTable :: Array Term
varTable = IO (Array Term) -> Array Term
forall a. IO a -> a
unsafePerformIO (IO (Array Term) -> Array Term) -> IO (Array Term) -> Array Term
forall a b. (a -> b) -> a -> b
$ do
  !c <- Word -> IO Compact
Compact.new Word
4096
  let !tbl = [Term] -> Array Term
forall a. [a] -> Array a
AL.fromList [Int -> [Elim] -> Term
Var' Int
i [] | Int
i <- [Int
0..(Int
varTableSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]]
  Compact.add c tbl

pattern Var :: Int -> Elims -> Term
pattern $mVar :: forall {r}. Term -> (Int -> [Elim] -> r) -> ((# #) -> r) -> r
$bVar :: Int -> [Elim] -> Term
Var i es <- Var' i es where
  Var Int
i [Elim]
es = case [Elim]
es of
    [] -> case Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
varTableSize of
      Bool
True -> Array Term -> Int -> Term
forall a. Array a -> Int -> a
AL.unsafeIndex Array Term
varTable Int
i
      Bool
_    -> Int -> [Elim] -> Term
Var' Int
i [Elim]
es
    [Elim]
_  -> Int -> [Elim] -> Term
Var' Int
i [Elim]
es
{-# INLINE Var #-}
{-# COMPLETE Var, Lam, Lit, Def, Con, Pi, Sort, Level, MetaV, DontCare, Dummy #-}

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

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

--------------------------------------------------------------------------------

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

instance Functor Abs where
  fmap :: forall a b. (a -> b) -> Abs a -> Abs b
fmap a -> b
f = \case
    Abs [Char]
x a
y   -> [Char] -> b -> Abs b
forall a. [Char] -> a -> Abs a
Abs [Char]
x (b -> Abs b) -> b -> Abs b
forall a b. (a -> b) -> a -> b
$! a -> b
f a
y
    NoAbs [Char]
x a
y -> [Char] -> b -> Abs b
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x (b -> Abs b) -> b -> Abs b
forall a b. (a -> b) -> a -> b
$! a -> b
f a
y

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

type Type' a = Type'' Term a

type Type = Type' Term

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

class LensSort a where
  lensSort ::  Lens' a Sort
  getSort  :: a -> Sort
  getSort a
a = a
a a -> Getting (Sort' Term) a (Sort' Term) -> Sort' Term
forall s a. s -> Getting a s a -> a
^. Getting (Sort' Term) a (Sort' Term)
forall a. LensSort a => Lens' a (Sort' Term)
Lens' a (Sort' Term)
lensSort

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

instance LensSort (Type' a) where
  lensSort :: Lens' (Type' a) (Sort' Term)
lensSort Sort' Term -> f (Sort' Term)
f (El Sort' Term
s a
a) = Sort' Term -> f (Sort' Term)
f Sort' Term
s f (Sort' Term) -> (Sort' Term -> Type' a) -> f (Type' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Sort' Term
s' -> Sort' Term -> a -> Type' a
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
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' (Dom a) (Sort' Term)
lensSort = (a -> f a) -> Dom a -> f (Dom a)
forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Dom' Term a -> m (Dom' Term b)
traverseF ((a -> f a) -> Dom a -> f (Dom a))
-> ((Sort' Term -> f (Sort' Term)) -> a -> f a)
-> (Sort' Term -> f (Sort' Term))
-> Dom a
-> f (Dom a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort' Term -> f (Sort' Term)) -> a -> f a
forall a. LensSort a => Lens' a (Sort' Term)
Lens' a (Sort' Term)
lensSort

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

instance ExpandCase (Tele a) where type Result (Tele a) = Tele a

type Telescope = Tele (Dom Type)

data UnivSize
  = USmall  -- ^ @Prop/Set/SSet ℓ@.
  | ULarge  -- ^ @(Prop/Set/SSet)ωᵢ@.
  deriving stock (UnivSize -> UnivSize -> Bool
(UnivSize -> UnivSize -> Bool)
-> (UnivSize -> UnivSize -> Bool) -> Eq UnivSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnivSize -> UnivSize -> Bool
== :: UnivSize -> UnivSize -> Bool
$c/= :: UnivSize -> UnivSize -> Bool
/= :: UnivSize -> UnivSize -> Bool
Eq, Int -> UnivSize -> ShowS
[UnivSize] -> ShowS
UnivSize -> [Char]
(Int -> UnivSize -> ShowS)
-> (UnivSize -> [Char]) -> ([UnivSize] -> ShowS) -> Show UnivSize
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnivSize -> ShowS
showsPrec :: Int -> UnivSize -> ShowS
$cshow :: UnivSize -> [Char]
show :: UnivSize -> [Char]
$cshowList :: [UnivSize] -> ShowS
showList :: [UnivSize] -> ShowS
Show)

-- | Sorts.
--
data Sort' t
  = Univ Univ (Level' t)
      -- ^ @Prop ℓ@, @Set ℓ@, @SSet ℓ@.
  | Inf Univ !Integer
      -- ^ @Propωᵢ@, @(S)Setωᵢ@.
  | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
  | LockUniv    -- ^ @LockUniv@, a sort for locks.
  | LevelUniv   -- ^ @LevelUniv@, a sort inhabited by type @Level@. When --level-universe isn't on, this universe reduces to @Set 0@
  | 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
[Sort' t] -> ShowS
Sort' t -> [Char]
(Int -> Sort' t -> ShowS)
-> (Sort' t -> [Char]) -> ([Sort' t] -> ShowS) -> Show (Sort' t)
forall t. Show t => Int -> Sort' t -> ShowS
forall t. Show t => [Sort' t] -> ShowS
forall t. Show t => Sort' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Sort' t -> ShowS
showsPrec :: Int -> Sort' t -> ShowS
$cshow :: forall t. Show t => Sort' t -> [Char]
show :: Sort' t -> [Char]
$cshowList :: forall t. Show t => [Sort' t] -> ShowS
showList :: [Sort' t] -> ShowS
Show

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

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

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

type Level = Level' Term

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

type PlusLevel = PlusLevel' Term
type LevelAtom = Term

---------------------------------------------------------------------------
-- * 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 -> [Char]
(Int -> BraveTerm -> ShowS)
-> (BraveTerm -> [Char])
-> ([BraveTerm] -> ShowS)
-> Show BraveTerm
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BraveTerm -> ShowS
showsPrec :: Int -> BraveTerm -> ShowS
$cshow :: BraveTerm -> [Char]
show :: BraveTerm -> [Char]
$cshowList :: [BraveTerm] -> ShowS
showList :: [BraveTerm] -> ShowS
Show

---------------------------------------------------------------------------
-- * 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]

-- | Does the clause body contain calls to any of the mutually recursive functions?
data ClauseRecursive
  = YesRecursive
      -- ^ Definitely a call to a mutually recursive function.
  | NotRecursive
      -- ^ Definitely no call to a mutually recursive function.
  | MaybeRecursive
      -- ^ Don't know because the analysis has not run yet.
  deriving (ClauseRecursive
ClauseRecursive -> ClauseRecursive -> Bounded ClauseRecursive
forall a. a -> a -> Bounded a
$cminBound :: ClauseRecursive
minBound :: ClauseRecursive
$cmaxBound :: ClauseRecursive
maxBound :: ClauseRecursive
Bounded, Int -> ClauseRecursive
ClauseRecursive -> Int
ClauseRecursive -> [ClauseRecursive]
ClauseRecursive -> ClauseRecursive
ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
(ClauseRecursive -> ClauseRecursive)
-> (ClauseRecursive -> ClauseRecursive)
-> (Int -> ClauseRecursive)
-> (ClauseRecursive -> Int)
-> (ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive
    -> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> Enum ClauseRecursive
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ClauseRecursive -> ClauseRecursive
succ :: ClauseRecursive -> ClauseRecursive
$cpred :: ClauseRecursive -> ClauseRecursive
pred :: ClauseRecursive -> ClauseRecursive
$ctoEnum :: Int -> ClauseRecursive
toEnum :: Int -> ClauseRecursive
$cfromEnum :: ClauseRecursive -> Int
fromEnum :: ClauseRecursive -> Int
$cenumFrom :: ClauseRecursive -> [ClauseRecursive]
enumFrom :: ClauseRecursive -> [ClauseRecursive]
$cenumFromThen :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromThen :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
$cenumFromTo :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromTo :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
$cenumFromThenTo :: ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromThenTo :: ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
Enum, ClauseRecursive -> ClauseRecursive -> Bool
(ClauseRecursive -> ClauseRecursive -> Bool)
-> (ClauseRecursive -> ClauseRecursive -> Bool)
-> Eq ClauseRecursive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ClauseRecursive -> ClauseRecursive -> Bool
== :: ClauseRecursive -> ClauseRecursive -> Bool
$c/= :: ClauseRecursive -> ClauseRecursive -> Bool
/= :: ClauseRecursive -> ClauseRecursive -> Bool
Eq, (forall x. ClauseRecursive -> Rep ClauseRecursive x)
-> (forall x. Rep ClauseRecursive x -> ClauseRecursive)
-> Generic ClauseRecursive
forall x. Rep ClauseRecursive x -> ClauseRecursive
forall x. ClauseRecursive -> Rep ClauseRecursive x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ClauseRecursive -> Rep ClauseRecursive x
from :: forall x. ClauseRecursive -> Rep ClauseRecursive x
$cto :: forall x. Rep ClauseRecursive x -> ClauseRecursive
to :: forall x. Rep ClauseRecursive x -> ClauseRecursive
Generic, Int -> ClauseRecursive -> ShowS
[ClauseRecursive] -> ShowS
ClauseRecursive -> [Char]
(Int -> ClauseRecursive -> ShowS)
-> (ClauseRecursive -> [Char])
-> ([ClauseRecursive] -> ShowS)
-> Show ClauseRecursive
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ClauseRecursive -> ShowS
showsPrec :: Int -> ClauseRecursive -> ShowS
$cshow :: ClauseRecursive -> [Char]
show :: ClauseRecursive -> [Char]
$cshowList :: [ClauseRecursive] -> ShowS
showList :: [ClauseRecursive] -> ShowS
Show)

couldBeRecursive :: ClauseRecursive -> Bool
couldBeRecursive :: ClauseRecursive -> Bool
couldBeRecursive = \case
  ClauseRecursive
YesRecursive   -> Bool
True
  ClauseRecursive
NotRecursive   -> Bool
False
  ClauseRecursive
MaybeRecursive -> Bool
True

decideRecursive :: Bool -> ClauseRecursive
decideRecursive :: Bool -> ClauseRecursive
decideRecursive = \case
  Bool
True  -> ClauseRecursive
YesRecursive
  Bool
False -> ClauseRecursive
NotRecursive

-- | 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 -> Catchall
clauseCatchall    :: Catchall
      -- ^ Clause has been labelled as CATCHALL.
    , Clause -> ClauseRecursive
clauseRecursive   :: ClauseRecursive
      -- ^ @clauseBody@ contains recursive calls? Computed by termination checker.
    , 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 -> [Char]
(Int -> Clause -> ShowS)
-> (Clause -> [Char]) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Clause -> ShowS
showsPrec :: Int -> Clause -> ShowS
$cshow :: Clause -> [Char]
show :: Clause -> [Char]
$cshowList :: [Clause] -> ShowS
showList :: [Clause] -> ShowS
Show, (forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
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
$cfrom :: forall x. Clause -> Rep Clause x
from :: forall x. Clause -> Rep Clause x
$cto :: forall x. Rep Clause x -> Clause
to :: forall x. Rep Clause x -> Clause
Generic)

clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = (Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern)
-> NAPs -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named_ DeBruijnPattern -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) (NAPs -> [Arg DeBruijnPattern])
-> (Clause -> NAPs) -> Clause -> [Arg DeBruijnPattern]
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 -> [Char]
nameToPatVarName = Name -> [Char]
nameToArgName

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

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

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

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

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

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

type DeBruijnPattern = Pattern' DBPatVar

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

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP :: Int -> [Char] -> Named_ DeBruijnPattern
namedDBVarP Int
m = ((Pattern -> DeBruijnPattern)
-> Named_ Pattern -> Named_ DeBruijnPattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> DeBruijnPattern)
 -> Named_ Pattern -> Named_ DeBruijnPattern)
-> (([Char] -> DBPatVar) -> Pattern -> DeBruijnPattern)
-> ([Char] -> DBPatVar)
-> Named_ Pattern
-> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> DBPatVar) -> Pattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\[Char]
x -> [Char] -> Int -> DBPatVar
DBPatVar [Char]
x Int
m) (Named_ Pattern -> Named_ DeBruijnPattern)
-> ([Char] -> Named_ Pattern) -> [Char] -> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Named_ Pattern
namedVarP

-- | Make an absurd pattern with the given de Bruijn index.
absurdP :: Int -> DeBruijnPattern
absurdP :: Int -> DeBruijnPattern
absurdP = PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) (DBPatVar -> DeBruijnPattern)
-> (Int -> DBPatVar) -> Int -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Int -> DBPatVar
DBPatVar [Char]
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 -> [Char]
(Int -> ConPatternInfo -> ShowS)
-> (ConPatternInfo -> [Char])
-> ([ConPatternInfo] -> ShowS)
-> Show ConPatternInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConPatternInfo -> ShowS
showsPrec :: Int -> ConPatternInfo -> ShowS
$cshow :: ConPatternInfo -> [Char]
show :: ConPatternInfo -> [Char]
$cshowList :: [ConPatternInfo] -> ShowS
showList :: [ConPatternInfo] -> ShowS
Show, (forall x. ConPatternInfo -> Rep ConPatternInfo x)
-> (forall x. Rep ConPatternInfo x -> ConPatternInfo)
-> Generic ConPatternInfo
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
$cfrom :: forall x. ConPatternInfo -> Rep ConPatternInfo x
from :: forall x. ConPatternInfo -> Rep ConPatternInfo x
$cto :: forall x. Rep ConPatternInfo x -> ConPatternInfo
to :: forall x. Rep ConPatternInfo x -> ConPatternInfo
Generic)

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

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

-- | Build 'ConInfo' from 'ConPatternInfo'.
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo :: ConPatternInfo -> ConOrigin
fromConPatternInfo ConPatternInfo
i = PatOrigin -> ConOrigin
patToConO (PatOrigin -> ConOrigin) -> PatOrigin -> ConOrigin
forall a b. (a -> b) -> a -> b
$ PatternInfo -> PatOrigin
patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i
  where
    patToConO :: PatOrigin -> ConOrigin
    patToConO :: PatOrigin -> ConOrigin
patToConO = \case
      PatOrigin
PatOSystem -> ConOrigin
ConOSystem
      PatOrigin
PatOSplit  -> ConOrigin
ConOSplit
      PatOSplitArg{} -> ConOrigin
ConOSystem
      PatOVar{}  -> ConOrigin
ConOSystem
      PatOrigin
PatODot    -> ConOrigin
ConOSystem
      PatOrigin
PatOWild   -> ConOrigin
ConOSystem
      PatOrigin
PatOCon    -> ConOrigin
ConOCon
      PatOrigin
PatORec    -> ConOrigin
ConORec
      PatOrigin
PatOLit    -> ConOrigin
ConOCon
      PatOrigin
PatOAbsurd -> ConOrigin
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)   ) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ PatternVarOut (Arg (Pattern' a))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. a -> Either a b
Left a
PatternVarOut (Arg (Pattern' a))
x]
  patternVars (Arg ArgInfo
i (DotP PatternInfo
_ Term
t)   ) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. b -> Either a b
Right Term
t]
  patternVars (Arg ArgInfo
_ (ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps)) = [NamedArg (Pattern' a)]
-> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
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)) = [NamedArg (Pattern' a)]
-> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
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)) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ PatternVarOut (Arg (Pattern' a))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. a -> Either a b
Left a
PatternVarOut (Arg (Pattern' 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 = Arg (Pattern' a) -> [Arg (Either a Term)]
Arg (Pattern' a)
-> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars (Arg (Pattern' a) -> [Arg (Either a Term)])
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> [Arg (Either a Term)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ (Pattern' a) -> Pattern' a
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 = (a -> [Arg (Either (PatternVarOut a) Term)])
-> [a] -> [Arg (Either (PatternVarOut a) Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [Arg (Either (PatternVarOut a) Term)]
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
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DotP PatternInfo
i Term
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (LitP PatternInfo
i Literal
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' x)]
_)     = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just (PatternInfo -> Maybe PatternInfo)
-> PatternInfo -> Maybe PatternInfo
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
ci
patternInfo ProjP{}           = Maybe PatternInfo
forall a. Maybe a
Nothing
patternInfo (IApplyP PatternInfo
i Term
_ Term
_ x
_) = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DefP PatternInfo
i QName
_ [NamedArg (Pattern' x)]
_)      = PatternInfo -> Maybe PatternInfo
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 = (PatternInfo -> PatOrigin) -> Maybe PatternInfo -> Maybe PatOrigin
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PatternInfo -> PatOrigin
patOrigin (Maybe PatternInfo -> Maybe PatOrigin)
-> (Pattern' x -> Maybe PatternInfo)
-> Pattern' x
-> Maybe PatOrigin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' x -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo

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

type Substitution = Substitution' Term
type PatternSubstitution = Substitution' DeBruijnPattern
type Renaming = Substitution' Nat

infixr 4 :#

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

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

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

-- | View type as equality type.

data EqualityView
  = EqualityViewType EqualityTypeData
      -- ^ A type of the form @u ≡ v@ decomposed into its parts.
      --   Used as type for the @rewrite@ expression.
  | OtherType Type
      -- ^ A reduced type used as type for a @with@ expression.
  | IdiomType Type
      -- ^ A reduced type used as type for the @with@ inspect idiom.

data EqualityTypeData = EqualityTypeData
    { EqualityTypeData -> Range
_eqtRange  :: Range       -- ^ Range of the @rewrite@ expression, if any.
    , EqualityTypeData -> Sort' Term
_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 ::
     Range
  -> Sort
  -> QName
  -> Args
  -> Arg Term
  -> Arg Term
  -> Arg Term
  -> EqualityView
pattern $mEqualityType :: forall {r}.
EqualityView
-> (Range
    -> Sort' Term
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> r)
-> ((# #) -> r)
-> r
$bEqualityType :: Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType{ EqualityView -> Range
eqtRange, EqualityView -> Sort' Term
eqtSort, EqualityView -> QName
eqtName, EqualityView -> Args
eqtParams, EqualityView -> Arg Term
eqtType, EqualityView -> Arg Term
eqtLhs, EqualityView -> Arg Term
eqtRhs } =
  EqualityViewType (EqualityTypeData eqtRange eqtSort eqtName eqtParams eqtType eqtLhs eqtRhs)

{-# COMPLETE EqualityType, OtherType, IdiomType #-}

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' Term
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 -> [Char]
(Int -> IntervalView -> ShowS)
-> (IntervalView -> [Char])
-> ([IntervalView] -> ShowS)
-> Show IntervalView
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntervalView -> ShowS
showsPrec :: Int -> IntervalView -> ShowS
$cshow :: IntervalView -> [Char]
show :: IntervalView -> [Char]
$cshowList :: [IntervalView] -> ShowS
showList :: [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 = [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
absurdPatternName (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> [Elim] -> Term
Var Int
0 []

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

absurdPatternName :: PatVarName
absurdPatternName :: [Char]
absurdPatternName = [Char]
"()"

isAbsurdPatternName :: PatVarName -> Bool
isAbsurdPatternName :: [Char] -> Bool
isAbsurdPatternName [Char]
x = [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
absurdPatternName

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

-- | 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

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

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

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

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

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

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

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

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

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

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

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

-- | Context entries without a type have this dummy type.
--   Note: use macro __DUMMY_DOM__ !
dummyDom :: CallStack -> Dom Type
dummyDom :: CallStack -> Dom' Term Type
dummyDom = Type -> Dom' Term Type
forall a. a -> Dom a
defaultDom (Type -> Dom' Term Type)
-> (CallStack -> Type) -> CallStack -> Dom' Term Type
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__ = (CallStack -> Dom' Term Type) -> Dom' Term Type
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Dom' Term Type
dummyDom

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

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------
-- * Sorts.
---------------------------------------------------------------------------

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

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

-- | Is this a Prop universe?  Answers are yes ('True') or maybe ('False').
isProp :: Sort' t -> Bool
isProp :: forall t. Sort' t -> Bool
isProp = (Univ -> Maybe Univ
forall a. a -> Maybe a
Just Univ
UProp Maybe Univ -> Maybe Univ -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Univ -> Bool) -> (Sort' t -> Maybe Univ) -> Sort' t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' t -> Maybe Univ
forall t. Sort' t -> Maybe Univ
sortUniv

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

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

---------------------------------------------------------------------------
-- * 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 =>
([Char] -> m [Char]) -> Tele a -> m (Tele a)
mapAbsNamesM [Char] -> m [Char]
_ Tele a
EmptyTel                  = Tele a -> m (Tele a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele a
forall a. Tele a
EmptyTel
mapAbsNamesM [Char] -> m [Char]
f (ExtendTel a
a (  Abs [Char]
x Tele a
b)) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (  [Char] -> Tele a -> Abs (Tele a)
forall a. [Char] -> a -> Abs a
Abs ([Char] -> Tele a -> Abs (Tele a))
-> m [Char] -> m (Tele a -> Abs (Tele a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> m [Char]
f [Char]
x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Char] -> m [Char]) -> Tele a -> m (Tele a)
forall (m :: * -> *) a.
Applicative m =>
([Char] -> m [Char]) -> Tele a -> m (Tele a)
mapAbsNamesM [Char] -> m [Char]
f Tele a
b)
mapAbsNamesM [Char] -> m [Char]
f (ExtendTel a
a (NoAbs [Char]
x Tele a
b)) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Tele a -> Abs (Tele a)
forall a. [Char] -> a -> Abs a
NoAbs ([Char] -> Tele a -> Abs (Tele a))
-> m [Char] -> m (Tele a -> Abs (Tele a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> m [Char]
f [Char]
x m (Tele a -> Abs (Tele a)) -> m (Tele a) -> m (Abs (Tele a))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Char] -> m [Char]) -> Tele a -> m (Tele a)
forall (m :: * -> *) a.
Applicative m =>
([Char] -> m [Char]) -> Tele a -> m (Tele a)
mapAbsNamesM [Char] -> m [Char]
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 = Identity (Tele a) -> Tele a
forall a. Identity a -> a
runIdentity (Identity (Tele a) -> Tele a)
-> (Tele a -> Identity (Tele a)) -> Tele a -> Tele a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Identity [Char]) -> Tele a -> Identity (Tele a)
forall (m :: * -> *) a.
Applicative m =>
([Char] -> m [Char]) -> Tele a -> m (Tele a)
mapAbsNamesM ([Char] -> Identity [Char]
forall a. a -> Identity a
Identity ([Char] -> Identity [Char]) -> ShowS -> [Char] -> Identity [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
f)

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

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

-- | Convert a list telescope to a telescope.
telFromList :: ListTel -> Telescope
telFromList :: ListTel -> Telescope
telFromList = ShowS -> ListTel -> Telescope
forall a. (a -> [Char]) -> ListTel' a -> Telescope
telFromList' ShowS
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 ([Char], t)]
telToList Tele (Dom t)
EmptyTel                    = []
telToList (ExtendTel Dom t
arg (Abs [Char]
x Tele (Dom t)
tel)) = ((t -> ([Char], t)) -> Dom t -> Dom ([Char], t)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char]
x,) Dom t
arg Dom ([Char], t) -> [Dom ([Char], t)] -> [Dom ([Char], t)]
forall a. a -> [a] -> [a]
:) ([Dom ([Char], t)] -> [Dom ([Char], t)])
-> [Dom ([Char], t)] -> [Dom ([Char], t)]
forall a b. (a -> b) -> a -> b
$! Tele (Dom t) -> [Dom ([Char], t)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom t)
tel
telToList (ExtendTel Dom t
_    NoAbs{}   ) = [Dom ([Char], t)]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

instance SgTel (Dom Type) where
  sgTel :: Dom' Term Type -> Telescope
sgTel Dom' Term Type
dom = ([Char], Dom' Term Type) -> Telescope
forall a. SgTel a => a -> Telescope
sgTel (ShowS
stringToArgName [Char]
"_", 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 Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
  Pi  Dom' Term Type
_ Abs Type
b -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
arity (Abs Type -> Type
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 :: [Char] -> Maybe [Char]
suggestName [Char]
"_" = Maybe [Char]
forall a. Maybe a
Nothing
  suggestName  [Char]
x  = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
x

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

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

instance Suggest Term where
  suggestName :: Term -> Maybe [Char]
suggestName (Lam ArgInfo
_ Abs Term
v) = Abs Term -> Maybe [Char]
forall a. Suggest a => a -> Maybe [Char]
suggestName Abs Term
v
  suggestName Term
_         = Maybe [Char]
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] -> [Char]
suggests []     = [Char]
"x"
suggests (Suggestion a
x : [Suggestion]
xs) = [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe ([Suggestion] -> [Char]
suggests [Suggestion]
xs) (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> Maybe [Char]
forall a. Suggest a => a -> Maybe [Char]
suggestName a
x

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

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

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

hasProj :: Elims -> Bool
hasProj :: [Elim] -> Bool
hasProj = \case
  []       -> Bool
False
  Proj{}:[Elim]
_ -> Bool
True
  Elim
_:[Elim]
es     -> [Elim] -> Bool
hasProj [Elim]
es

#if __GLASGOW_HASKELL__ < 906
data SpineHead' = SHVar !Int | SHDef !QName | SHMetaV {-# UNPACK #-} !MetaId
newtype SpineHead = SpineHead SpineHead'
#else
data SpineHead' = SHVar !Int | SHDef !QName | SHMetaV {-# UNPACK #-} !MetaId
data SpineHead = SpineHead {-# UNPACK #-} !SpineHead'
#endif

applySpineHead :: SpineHead -> Elims -> Term
applySpineHead :: SpineHead -> [Elim] -> Term
applySpineHead SpineHead
h ![Elim]
es = case SpineHead
h of
  SpineHead (SHVar Int
x  ) -> Int -> [Elim] -> Term
Var Int
x [Elim]
es
  SpineHead (SHDef QName
f  ) -> QName -> [Elim] -> Term
Def QName
f [Elim]
es
  SpineHead (SHMetaV MetaId
x) -> MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
es

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

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

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

{-# INLINE hasElims #-}
-- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which
--   can be projected.
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims :: Term -> Maybe ([Elim] -> Term, [Elim])
hasElims Term
v =
  case Term
v of
    Var   Int
i [Elim]
es -> ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (Int -> [Elim] -> Term
Var   Int
i, [Elim]
es)
    Def   QName
f [Elim]
es -> ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def   QName
f, [Elim]
es)
    MetaV MetaId
x [Elim]
es -> ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (MetaId -> [Elim] -> Term
MetaV MetaId
x, [Elim]
es)
    Con{}      -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Lit{}      -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Lam{}      -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Pi{}       -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Sort{}     -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Level{}    -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    DontCare{} -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    Dummy{}    -> Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing


---------------------------------------------------------------------------
-- * Type family for type-directed operations.
---------------------------------------------------------------------------

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

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

---------------------------------------------------------------------------
-- * (Local) rewrite rules
---------------------------------------------------------------------------

-- | NLPat might become definitionally singular (after a substitution)
data DefSing
  = NeverSing
    -- ^ Never definitionally singular
  | MaybeSing
    -- ^ Might become definitionally singular after a substitution
  | AlwaysSing
    -- ^ Always definitionally singular (e.g. irrelevant or in |Prop|)
  deriving (Int -> DefSing -> ShowS
[DefSing] -> ShowS
DefSing -> [Char]
(Int -> DefSing -> ShowS)
-> (DefSing -> [Char]) -> ([DefSing] -> ShowS) -> Show DefSing
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefSing -> ShowS
showsPrec :: Int -> DefSing -> ShowS
$cshow :: DefSing -> [Char]
show :: DefSing -> [Char]
$cshowList :: [DefSing] -> ShowS
showList :: [DefSing] -> ShowS
Show, (forall x. DefSing -> Rep DefSing x)
-> (forall x. Rep DefSing x -> DefSing) -> Generic DefSing
forall x. Rep DefSing x -> DefSing
forall x. DefSing -> Rep DefSing x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DefSing -> Rep DefSing x
from :: forall x. DefSing -> Rep DefSing x
$cto :: forall x. Rep DefSing x -> DefSing
to :: forall x. Rep DefSing x -> DefSing
Generic, Int -> DefSing
DefSing -> Int
DefSing -> [DefSing]
DefSing -> DefSing
DefSing -> DefSing -> [DefSing]
DefSing -> DefSing -> DefSing -> [DefSing]
(DefSing -> DefSing)
-> (DefSing -> DefSing)
-> (Int -> DefSing)
-> (DefSing -> Int)
-> (DefSing -> [DefSing])
-> (DefSing -> DefSing -> [DefSing])
-> (DefSing -> DefSing -> [DefSing])
-> (DefSing -> DefSing -> DefSing -> [DefSing])
-> Enum DefSing
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: DefSing -> DefSing
succ :: DefSing -> DefSing
$cpred :: DefSing -> DefSing
pred :: DefSing -> DefSing
$ctoEnum :: Int -> DefSing
toEnum :: Int -> DefSing
$cfromEnum :: DefSing -> Int
fromEnum :: DefSing -> Int
$cenumFrom :: DefSing -> [DefSing]
enumFrom :: DefSing -> [DefSing]
$cenumFromThen :: DefSing -> DefSing -> [DefSing]
enumFromThen :: DefSing -> DefSing -> [DefSing]
$cenumFromTo :: DefSing -> DefSing -> [DefSing]
enumFromTo :: DefSing -> DefSing -> [DefSing]
$cenumFromThenTo :: DefSing -> DefSing -> DefSing -> [DefSing]
enumFromThenTo :: DefSing -> DefSing -> DefSing -> [DefSing]
Enum, DefSing
DefSing -> DefSing -> Bounded DefSing
forall a. a -> a -> Bounded a
$cminBound :: DefSing
minBound :: DefSing
$cmaxBound :: DefSing
maxBound :: DefSing
Bounded)

relToDefSing :: Relevance -> DefSing
relToDefSing :: Relevance -> DefSing
relToDefSing Relevance
r = if Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r then DefSing
AlwaysSing else DefSing
NeverSing

-- Only approximate if both sides are |NotDefSingIfInj| with non-empty
-- injective constraints
minDefSing :: DefSing -> DefSing -> DefSing
minDefSing :: DefSing -> DefSing -> DefSing
minDefSing DefSing
s DefSing
s' = Int -> DefSing
forall a. Enum a => Int -> a
toEnum (Int -> DefSing) -> Int -> DefSing
forall a b. (a -> b) -> a -> b
$ DefSing -> Int
forall a. Enum a => a -> Int
fromEnum DefSing
s Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` DefSing -> Int
forall a. Enum a => a -> Int
fromEnum DefSing
s'

maxDefSing :: DefSing -> DefSing -> DefSing
maxDefSing :: DefSing -> DefSing -> DefSing
maxDefSing DefSing
s DefSing
s' = Int -> DefSing
forall a. Enum a => Int -> a
toEnum (Int -> DefSing) -> Int -> DefSing
forall a b. (a -> b) -> a -> b
$ DefSing -> Int
forall a. Enum a => a -> Int
fromEnum DefSing
s Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` DefSing -> Int
forall a. Enum a => a -> Int
fromEnum DefSing
s'

isAlwaysSing :: DefSing -> Bool
isAlwaysSing :: DefSing -> Bool
isAlwaysSing DefSing
AlwaysSing = Bool
True
isAlwaysSing DefSing
_          = Bool
False

-- | Non-linear (non-constructor) first-order pattern.
data NLPat
  = PVar DefSing !Int [Arg Int]
    -- ^ Matches anything (modulo non-linearity) that only contains bound
    --   variables that occur in the given arguments.
    --   Tracks the definitional singularity of the surrounding pattern (not
    --   the type of the variable itself)
  | PDef QName PElims
    -- ^ Matches @f es@
  | PLam ArgInfo (Abs NLPat)
    -- ^ Matches @λ x → t@
  | PPi (Dom NLPType) (Abs NLPType)
    -- ^ Matches @(x : A) → B@
  | PSort NLPSort
    -- ^ Matches a sort of the given shape.
  | PBoundVar {-# UNPACK #-} !Int PElims
    -- ^ Matches @x es@ where x is a lambda-bound variable
  | PTerm Term
    -- ^ Matches the term modulo β (ideally βη).
  deriving (Int -> NLPat -> ShowS
[NLPat] -> ShowS
NLPat -> [Char]
(Int -> NLPat -> ShowS)
-> (NLPat -> [Char]) -> ([NLPat] -> ShowS) -> Show NLPat
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NLPat -> ShowS
showsPrec :: Int -> NLPat -> ShowS
$cshow :: NLPat -> [Char]
show :: NLPat -> [Char]
$cshowList :: [NLPat] -> ShowS
showList :: [NLPat] -> ShowS
Show, (forall x. NLPat -> Rep NLPat x)
-> (forall x. Rep NLPat x -> NLPat) -> Generic NLPat
forall x. Rep NLPat x -> NLPat
forall x. NLPat -> Rep NLPat x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NLPat -> Rep NLPat x
from :: forall x. NLPat -> Rep NLPat x
$cto :: forall x. Rep NLPat x -> NLPat
to :: forall x. Rep NLPat x -> NLPat
Generic)
type PElims = [Elim' NLPat]


type instance TypeOf NLPat = Type
type instance TypeOf [Elim' NLPat] = (Type, Elims -> Term)


data NLPType = NLPType
  { NLPType -> NLPSort
nlpTypeSort :: NLPSort
  , NLPType -> NLPat
nlpTypeUnEl :: NLPat
  } deriving (Int -> NLPType -> ShowS
[NLPType] -> ShowS
NLPType -> [Char]
(Int -> NLPType -> ShowS)
-> (NLPType -> [Char]) -> ([NLPType] -> ShowS) -> Show NLPType
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NLPType -> ShowS
showsPrec :: Int -> NLPType -> ShowS
$cshow :: NLPType -> [Char]
show :: NLPType -> [Char]
$cshowList :: [NLPType] -> ShowS
showList :: [NLPType] -> ShowS
Show, (forall x. NLPType -> Rep NLPType x)
-> (forall x. Rep NLPType x -> NLPType) -> Generic NLPType
forall x. Rep NLPType x -> NLPType
forall x. NLPType -> Rep NLPType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NLPType -> Rep NLPType x
from :: forall x. NLPType -> Rep NLPType x
$cto :: forall x. Rep NLPType x -> NLPType
to :: forall x. Rep NLPType x -> NLPType
Generic)


data NLPSort
  = PUniv Univ NLPat
  | PInf Univ Integer
  | PSizeUniv
  | PLockUniv
  | PLevelUniv
  | PIntervalUniv
  deriving (Int -> NLPSort -> ShowS
[NLPSort] -> ShowS
NLPSort -> [Char]
(Int -> NLPSort -> ShowS)
-> (NLPSort -> [Char]) -> ([NLPSort] -> ShowS) -> Show NLPSort
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NLPSort -> ShowS
showsPrec :: Int -> NLPSort -> ShowS
$cshow :: NLPSort -> [Char]
show :: NLPSort -> [Char]
$cshowList :: [NLPSort] -> ShowS
showList :: [NLPSort] -> ShowS
Show, (forall x. NLPSort -> Rep NLPSort x)
-> (forall x. Rep NLPSort x -> NLPSort) -> Generic NLPSort
forall x. Rep NLPSort x -> NLPSort
forall x. NLPSort -> Rep NLPSort x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NLPSort -> Rep NLPSort x
from :: forall x. NLPSort -> Rep NLPSort x
$cto :: forall x. Rep NLPSort x -> NLPSort
to :: forall x. Rep NLPSort x -> NLPSort
Generic)

pattern PType, PProp, PSSet :: NLPat -> NLPSort
pattern $mPType :: forall {r}. NLPSort -> (NLPat -> r) -> ((# #) -> r) -> r
$bPType :: NLPat -> NLPSort
PType p = PUniv UType p
pattern $mPProp :: forall {r}. NLPSort -> (NLPat -> r) -> ((# #) -> r) -> r
$bPProp :: NLPat -> NLPSort
PProp p = PUniv UProp p
pattern $mPSSet :: forall {r}. NLPSort -> (NLPat -> r) -> ((# #) -> r) -> r
$bPSSet :: NLPat -> NLPSort
PSSet p = PUniv USSet p

{-# COMPLETE
  PType, PSSet, PProp, PInf,
  PSizeUniv, PLockUniv, PLevelUniv, PIntervalUniv #-}

data RewriteHead
  = RewDefHead QName
  | RewVarHead Nat
    -- ^ de Bruijn index of head symbol (excluding rewContext variables)
  deriving (Int -> RewriteHead -> ShowS
[RewriteHead] -> ShowS
RewriteHead -> [Char]
(Int -> RewriteHead -> ShowS)
-> (RewriteHead -> [Char])
-> ([RewriteHead] -> ShowS)
-> Show RewriteHead
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RewriteHead -> ShowS
showsPrec :: Int -> RewriteHead -> ShowS
$cshow :: RewriteHead -> [Char]
show :: RewriteHead -> [Char]
$cshowList :: [RewriteHead] -> ShowS
showList :: [RewriteHead] -> ShowS
Show, (forall x. RewriteHead -> Rep RewriteHead x)
-> (forall x. Rep RewriteHead x -> RewriteHead)
-> Generic RewriteHead
forall x. Rep RewriteHead x -> RewriteHead
forall x. RewriteHead -> Rep RewriteHead x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RewriteHead -> Rep RewriteHead x
from :: forall x. RewriteHead -> Rep RewriteHead x
$cto :: forall x. Rep RewriteHead x -> RewriteHead
to :: forall x. Rep RewriteHead x -> RewriteHead
Generic, RewriteHead -> RewriteHead -> Bool
(RewriteHead -> RewriteHead -> Bool)
-> (RewriteHead -> RewriteHead -> Bool) -> Eq RewriteHead
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RewriteHead -> RewriteHead -> Bool
== :: RewriteHead -> RewriteHead -> Bool
$c/= :: RewriteHead -> RewriteHead -> Bool
/= :: RewriteHead -> RewriteHead -> Bool
Eq)

headToPat :: Nat -> RewriteHead -> PElims -> NLPat
headToPat :: Int -> RewriteHead -> [Elim' NLPat] -> NLPat
headToPat Int
_        (RewDefHead QName
f) = QName -> [Elim' NLPat] -> NLPat
PDef QName
f
headToPat Int
telStart (RewVarHead Int
x) = Int -> [Elim' NLPat] -> NLPat
PBoundVar (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
telStart)

headToTerm :: Nat -> RewriteHead -> Elims -> Term
headToTerm :: Int -> RewriteHead -> [Elim] -> Term
headToTerm Int
_        (RewDefHead QName
f) = QName -> [Elim] -> Term
Def QName
f
headToTerm Int
telStart (RewVarHead Int
x) = Int -> [Elim] -> Term
Var (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
telStart)

-- | Undirected equational constraint ("the LHS and RHS
--   must be convertible in the calling context").
--   Admits arbitrary substitution.
data LocalEquation' t = LocalEquation
  { forall t. LocalEquation' t -> Tele (Dom' t (Type'' t t))
lEqContext :: !(Tele (Dom' t (Type'' t t)))
  , forall t. LocalEquation' t -> t
lEqLHS     :: t
  , forall t. LocalEquation' t -> t
lEqRHS     :: t
  , forall t. LocalEquation' t -> Type'' t t
lEqType    :: Type'' t t
  }
  deriving (Int -> LocalEquation' t -> ShowS
[LocalEquation' t] -> ShowS
LocalEquation' t -> [Char]
(Int -> LocalEquation' t -> ShowS)
-> (LocalEquation' t -> [Char])
-> ([LocalEquation' t] -> ShowS)
-> Show (LocalEquation' t)
forall t. Show t => Int -> LocalEquation' t -> ShowS
forall t. Show t => [LocalEquation' t] -> ShowS
forall t. Show t => LocalEquation' t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> LocalEquation' t -> ShowS
showsPrec :: Int -> LocalEquation' t -> ShowS
$cshow :: forall t. Show t => LocalEquation' t -> [Char]
show :: LocalEquation' t -> [Char]
$cshowList :: forall t. Show t => [LocalEquation' t] -> ShowS
showList :: [LocalEquation' t] -> ShowS
Show, (forall x. LocalEquation' t -> Rep (LocalEquation' t) x)
-> (forall x. Rep (LocalEquation' t) x -> LocalEquation' t)
-> Generic (LocalEquation' t)
forall x. Rep (LocalEquation' t) x -> LocalEquation' t
forall x. LocalEquation' t -> Rep (LocalEquation' t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (LocalEquation' t) x -> LocalEquation' t
forall t x. LocalEquation' t -> Rep (LocalEquation' t) x
$cfrom :: forall t x. LocalEquation' t -> Rep (LocalEquation' t) x
from :: forall x. LocalEquation' t -> Rep (LocalEquation' t) x
$cto :: forall t x. Rep (LocalEquation' t) x -> LocalEquation' t
to :: forall x. Rep (LocalEquation' t) x -> LocalEquation' t
Generic)

type LocalEquation = LocalEquation' Term

-- | Directed rewrite rules generic over the type of head symbol.
--   Generally unstable under substitution.
data RewriteRule = RewriteRule
  { RewriteRule -> Telescope
rewContext :: Telescope
  , RewriteRule -> RewriteHead
rewHead    :: RewriteHead
  , RewriteRule -> [Elim' NLPat]
rewPats    :: PElims     -- patterns (including rewContext variables)
  , RewriteRule -> Term
rewRHS     :: Term
  , RewriteRule -> Type
rewType    :: Type
  }
  deriving (Int -> RewriteRule -> ShowS
[RewriteRule] -> ShowS
RewriteRule -> [Char]
(Int -> RewriteRule -> ShowS)
-> (RewriteRule -> [Char])
-> ([RewriteRule] -> ShowS)
-> Show RewriteRule
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RewriteRule -> ShowS
showsPrec :: Int -> RewriteRule -> ShowS
$cshow :: RewriteRule -> [Char]
show :: RewriteRule -> [Char]
$cshowList :: [RewriteRule] -> ShowS
showList :: [RewriteRule] -> ShowS
Show, (forall x. RewriteRule -> Rep RewriteRule x)
-> (forall x. Rep RewriteRule x -> RewriteRule)
-> Generic RewriteRule
forall x. Rep RewriteRule x -> RewriteRule
forall x. RewriteRule -> Rep RewriteRule x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RewriteRule -> Rep RewriteRule x
from :: forall x. RewriteRule -> Rep RewriteRule x
$cto :: forall x. Rep RewriteRule x -> RewriteRule
to :: forall x. Rep RewriteRule x -> RewriteRule
Generic)

lrewHasProjectionPattern :: RewriteRule -> Bool
lrewHasProjectionPattern :: RewriteRule -> Bool
lrewHasProjectionPattern RewriteRule
rew = (Elim' NLPat -> Bool) -> [Elim' NLPat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (ProjOrigin, QName) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (ProjOrigin, QName) -> Bool)
-> (Elim' NLPat -> Maybe (ProjOrigin, QName))
-> Elim' NLPat
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' NLPat -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim) ([Elim' NLPat] -> Bool) -> [Elim' NLPat] -> Bool
forall a b. (a -> b) -> a -> b
$ RewriteRule -> [Elim' NLPat]
rewPats RewriteRule
rew

class LensLocalEquation a where
  getLocalEq :: a -> Maybe LocalEquation

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

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

instance Null ClauseRecursive where
  empty :: ClauseRecursive
empty = ClauseRecursive
MaybeRecursive

-- | 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)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
forall a. Null a => a
empty Range
forall a. Null a => a
empty Telescope
forall a. Null a => a
empty NAPs
forall a. Null a => a
empty Maybe Term
forall a. Null a => a
empty Maybe (Arg Type)
forall a. Null a => a
empty Catchall
forall a. Null a => a
empty ClauseRecursive
forall a. Null a => a
empty Maybe Bool
forall a. Null a => a
empty ExpandedEllipsis
forall a. Null a => a
empty Maybe ModuleName
forall a. Null a => a
empty
  null :: Clause -> Bool
null (Clause Range
_ Range
_ Telescope
tel NAPs
pats Maybe Term
body Maybe (Arg Type)
_ Catchall
_ ClauseRecursive
_ Maybe Bool
_ ExpandedEllipsis
_ Maybe ModuleName
wm)
    =  Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel
    Bool -> Bool -> Bool
&& NAPs -> Bool
forall a. Null a => a -> Bool
null NAPs
pats
    Bool -> Bool -> Bool
&& Maybe Term -> Bool
forall a. Null a => a -> Bool
null Maybe Term
body
    Bool -> Bool -> Bool
&& Maybe ModuleName -> 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 [Char]
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    [Char] -> ShowS
showString [Char]
"Abs " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
forall a. Show a => a -> ShowS
shows [Char]
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a
  showsPrec Int
p (NoAbs [Char]
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    [Char] -> ShowS
showString [Char]
"NoAbs " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
forall a. Show a => a -> ShowS
shows [Char]
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Abs (Tele a) -> Int
forall a. Sized a => a -> Int
size Abs (Tele a)
tel

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

instance Sized a => Sized (Abs a) where
  size :: Abs a -> Int
size    = a -> Int
forall a. Sized a => a -> Int
size    (a -> Int) -> (Abs a -> a) -> Abs a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs a -> a
forall a. Abs a -> a
unAbs
  natSize :: Abs a -> Peano
natSize = a -> Peano
forall a. Sized a => a -> Peano
natSize (a -> Peano) -> (Abs a -> a) -> Abs a -> Peano
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs a -> a
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 = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize

  tsize :: a -> Sum Int

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

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

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

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

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

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

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

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

instance KillRange ConHead where
  killRange :: ConHead -> ConHead
killRange (ConHead QName
c DataOrRecord
d Induction
i [Arg QName]
fs) = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
-> QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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 [Elim]
vs    -> ([Elim] -> Term) -> [Elim] -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Int -> [Elim] -> Term
Var Int
i) [Elim]
vs
    Def QName
c [Elim]
vs    -> (QName -> [Elim] -> Term) -> QName -> [Elim] -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [Elim] -> Term
Def QName
c [Elim]
vs
    Con ConHead
c ConOrigin
ci [Elim]
vs -> (ConHead -> ConOrigin -> [Elim] -> Term)
-> ConHead -> ConOrigin -> [Elim] -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConHead -> ConOrigin -> [Elim] -> Term
Con ConHead
c ConOrigin
ci [Elim]
vs
    MetaV MetaId
m [Elim]
vs  -> ([Elim] -> Term) -> [Elim] -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (MetaId -> [Elim] -> Term
MetaV MetaId
m) [Elim]
vs
    Lam ArgInfo
i Abs Term
f     -> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo -> Abs Term -> Term
Lam ArgInfo
i Abs Term
f
    Lit Literal
l       -> (Literal -> Term) -> Literal -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Literal -> Term
Lit Literal
l
    Level Level' Term
l     -> (Level' Term -> Term) -> Level' Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Level' Term -> Term
Level Level' Term
l
    Pi Dom' Term Type
a Abs Type
b      -> (Dom' Term Type -> Abs Type -> Term)
-> Dom' Term Type -> Abs Type -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom' Term Type -> Abs Type -> Term
Pi Dom' Term Type
a Abs Type
b
    Sort Sort' Term
s      -> (Sort' Term -> Term) -> Sort' Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort' Term -> Term
Sort Sort' Term
s
    DontCare Term
mv -> (Term -> Term) -> Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Term -> Term
DontCare Term
mv
    v :: Term
v@Dummy{}   -> Term
v

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

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

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

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

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

instance KillRange PatOrigin where
  killRange :: KillRangeT PatOrigin
killRange = \case
    PatOrigin
PatOSystem     -> PatOrigin
PatOSystem
    PatOrigin
PatOSplit      -> PatOrigin
PatOSplit
    PatOSplitArg [Char]
n -> ([Char] -> PatOrigin) -> [Char] -> PatOrigin
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [Char] -> PatOrigin
PatOSplitArg [Char]
n
    PatOVar Name
n      -> (Name -> PatOrigin) -> Name -> PatOrigin
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> PatOrigin
PatOVar Name
n
    PatOrigin
PatODot        -> PatOrigin
PatODot
    PatOrigin
PatOWild       -> PatOrigin
PatOWild
    PatOrigin
PatOCon        -> PatOrigin
PatOCon
    PatOrigin
PatORec        -> PatOrigin
PatORec
    PatOrigin
PatOLit        -> PatOrigin
PatOLit
    PatOrigin
PatOAbsurd     -> PatOrigin
PatOAbsurd

instance KillRange PatternInfo where
  killRange :: KillRangeT PatternInfo
killRange (PatternInfo PatOrigin
o [Name]
xs) = (PatOrigin -> [Name] -> PatternInfo)
-> PatOrigin -> [Name] -> PatternInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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) = (Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Maybe (Arg Type) -> Bool -> ConPatternInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (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 [Char]
x Int
i) = ([Char] -> Int -> DBPatVar) -> [Char] -> Int -> DBPatVar
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [Char] -> Int -> DBPatVar
DBPatVar [Char]
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         -> (PatternInfo -> a -> Pattern' a) -> PatternInfo -> a -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o a
x
      DotP PatternInfo
o Term
v         -> (PatternInfo -> Term -> Pattern' a)
-> PatternInfo -> Term -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
v
      ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps -> (ConHead
 -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
-> ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' a)]
-> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps
      LitP PatternInfo
o Literal
l         -> (PatternInfo -> Literal -> Pattern' a)
-> PatternInfo -> Literal -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
      ProjP ProjOrigin
o QName
q        -> (QName -> Pattern' a) -> QName -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ProjOrigin -> QName -> Pattern' a
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o) QName
q
      IApplyP PatternInfo
o Term
u Term
t a
x  -> (Term -> Term -> a -> Pattern' a)
-> Term -> Term -> a -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (PatternInfo -> Term -> Term -> a -> Pattern' a
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      -> (QName -> [NamedArg (Pattern' a)] -> Pattern' a)
-> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o) QName
q [NamedArg (Pattern' a)]
ps

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

instance KillRange Clause where
  killRange :: KillRangeT Clause
killRange (Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
    (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Catchall
 -> ClauseRecursive
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm


instance KillRange NLPat where
  killRange :: KillRangeT NLPat
killRange (PVar DefSing
s Int
x [Arg Int]
y)    = (Int -> [Arg Int] -> NLPat) -> Int -> [Arg Int] -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (DefSing -> Int -> [Arg Int] -> NLPat
PVar DefSing
s) Int
x [Arg Int]
y
  killRange (PDef QName
x [Elim' NLPat]
y)      = (QName -> [Elim' NLPat] -> NLPat)
-> QName -> [Elim' NLPat] -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [Elim' NLPat] -> NLPat
PDef QName
x [Elim' NLPat]
y
  killRange (PLam ArgInfo
x Abs NLPat
y)      = (ArgInfo -> Abs NLPat -> NLPat) -> ArgInfo -> Abs NLPat -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
x Abs NLPat
y
  killRange (PPi Dom' Term NLPType
x Abs NLPType
y)       = (Dom' Term NLPType -> Abs NLPType -> NLPat)
-> Dom' Term NLPType -> Abs NLPType -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom' Term NLPType -> Abs NLPType -> NLPat
PPi Dom' Term NLPType
x Abs NLPType
y
  killRange (PSort NLPSort
x)       = (NLPSort -> NLPat) -> NLPSort -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN NLPSort -> NLPat
PSort NLPSort
x
  killRange (PBoundVar Int
x [Elim' NLPat]
y) = (Int -> [Elim' NLPat] -> NLPat) -> Int -> [Elim' NLPat] -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
x [Elim' NLPat]
y
  killRange (PTerm Term
x)       = (Term -> NLPat) -> Term -> NLPat
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Term -> NLPat
PTerm Term
x

instance KillRange NLPType where
  killRange :: KillRangeT NLPType
killRange (NLPType NLPSort
s NLPat
a) = (NLPSort -> NLPat -> NLPType) -> NLPSort -> NLPat -> NLPType
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN NLPSort -> NLPat -> NLPType
NLPType NLPSort
s NLPat
a

instance KillRange NLPSort where
  killRange :: KillRangeT NLPSort
killRange (PUniv Univ
u NLPat
l) = (NLPat -> NLPSort) -> NLPat -> NLPSort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Univ -> NLPat -> NLPSort
PUniv Univ
u) NLPat
l
  killRange s :: NLPSort
s@(PInf Univ
_f Integer
_n) = NLPSort
s
  killRange NLPSort
PSizeUniv = NLPSort
PSizeUniv
  killRange NLPSort
PLockUniv = NLPSort
PLockUniv
  killRange NLPSort
PLevelUniv = NLPSort
PLevelUniv
  killRange NLPSort
PIntervalUniv = NLPSort
PIntervalUniv

instance KillRange RewriteHead where
  killRange :: KillRangeT RewriteHead
killRange (RewVarHead Int
a) =
    (Int -> RewriteHead) -> Int -> RewriteHead
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Int -> RewriteHead
RewVarHead Int
a
  killRange (RewDefHead QName
a) =
    (QName -> RewriteHead) -> QName -> RewriteHead
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> RewriteHead
RewDefHead QName
a

instance KillRange t => KillRange (LocalEquation' t) where
  killRange :: KillRangeT (LocalEquation' t)
killRange (LocalEquation Tele (Dom' t (Type'' t t))
a t
b t
c Type'' t t
d) =
    (Tele (Dom' t (Type'' t t))
 -> t -> t -> Type'' t t -> LocalEquation' t)
-> Tele (Dom' t (Type'' t t))
-> t
-> t
-> Type'' t t
-> LocalEquation' t
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Tele (Dom' t (Type'' t t))
-> t -> t -> Type'' t t -> LocalEquation' t
forall t.
Tele (Dom' t (Type'' t t))
-> t -> t -> Type'' t t -> LocalEquation' t
LocalEquation Tele (Dom' t (Type'' t t))
a t
b t
c Type'' t t
d

instance KillRange RewriteRule where
  killRange :: KillRangeT RewriteRule
killRange (RewriteRule Telescope
a RewriteHead
b [Elim' NLPat]
c Term
d Type
e) =
    (Telescope
 -> RewriteHead -> [Elim' NLPat] -> Term -> Type -> RewriteRule)
-> Telescope
-> RewriteHead
-> [Elim' NLPat]
-> Term
-> Type
-> RewriteRule
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Telescope
-> RewriteHead -> [Elim' NLPat] -> Term -> Type -> RewriteRule
RewriteRule Telescope
a RewriteHead
b [Elim' NLPat]
c Term
d Type
e

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

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

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

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

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

instance Pretty Term where
  prettyPrec :: Int -> Term -> Doc Aspects
prettyPrec Int
p Term
v =
    case Term
v of
      Var Int
x [Elim]
els -> [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char]
"@" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x) Doc Aspects -> [Elim] -> Doc Aspects
`pApp` [Elim]
els
      Lam ArgInfo
ai Abs Term
b   ->
        Bool -> Doc Aspects -> Doc Aspects
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
        [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"λ" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> ArgInfo
-> (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a.
LensHiding a =>
a -> (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
prettyHiding ArgInfo
ai Doc Aspects -> Doc Aspects
forall a. a -> a
id ([Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char] -> Doc Aspects)
-> (Abs Term -> [Char]) -> Abs Term -> Doc Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs Term -> [Char]
forall a. Abs a -> [Char]
absName (Abs Term -> Doc Aspects) -> Abs Term -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Abs Term
b) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"->"
            , Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Term -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b) ]
      Lit Literal
l                -> Literal -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Literal
l
      Def QName
q [Elim]
els            -> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q Doc Aspects -> [Elim] -> Doc Aspects
`pApp` [Elim]
els
      Con ConHead
c ConOrigin
_ci [Elim]
vs         -> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (ConHead -> QName
conName ConHead
c) Doc Aspects -> [Elim] -> Doc Aspects
`pApp` [Elim]
vs
      Pi Dom' Term Type
a (NoAbs [Char]
_ Type
b)     -> Bool -> Doc Aspects -> Doc Aspects
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
        [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Modality -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Dom' Term Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom' Term Type
a) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Type -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
1 (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
a) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"->"
            , Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Type -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Type
b ]
      Pi Dom' Term Type
a Abs Type
b               -> Bool -> Doc Aspects -> Doc Aspects
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
        [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ ArgInfo -> Doc Aspects -> Doc Aspects
forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
pDom (Dom' Term Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
a) (Modality -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Dom' Term Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom' Term Type
a) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text (Abs Type -> [Char]
forall a. Abs a -> [Char]
absName Abs Type
b) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
a)) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"->"
            , Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Type -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b) ]
      Sort Sort' Term
s      -> Int -> Sort' Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Sort' Term
s
      Level Level' Term
l     -> Int -> Level' Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Level' Term
l
      MetaV MetaId
x [Elim]
els -> MetaId -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty MetaId
x Doc Aspects -> [Elim] -> Doc Aspects
`pApp` [Elim]
els
      DontCare Term
v  -> Int -> Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Term
v

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

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

instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
  pretty :: Dom' t e -> Doc Aspects
pretty Dom' t e
dom = Doc Aspects
pLock Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
pTac Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Dom' t e -> Doc Aspects -> Doc Aspects
forall a. LensHiding a => a -> Doc Aspects -> Doc Aspects
pDom Dom' t e
dom (Modality -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Dom' t e -> Modality
forall a. LensModality a => a -> Modality
getModality Dom' t e
dom) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> e -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Dom' t e -> e
forall t e. Dom' t e -> e
unDom Dom' t e
dom))
    where
      pTac :: Doc Aspects
pTac | Just t
t <- Dom' t e -> Maybe t
forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Doc Aspects
"@" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects -> Doc Aspects
parens (Doc Aspects
"tactic" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> t -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty t
t)
           | Bool
otherwise               = Doc Aspects
forall a. Null a => a
empty
      pLock :: Doc Aspects
pLock | IsLock{} <- Dom' t e -> Lock
forall a. LensLock a => a -> Lock
getLock Dom' t e
dom = Doc Aspects
"@lock"
            | Bool
otherwise = Doc Aspects
forall a. Null a => a
empty

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

instance Pretty ClauseRecursive where
  pretty :: ClauseRecursive -> Doc Aspects
pretty = \case
    ClauseRecursive
YesRecursive   -> Doc Aspects
"+Rec"
    ClauseRecursive
NotRecursive   -> Doc Aspects
"-Rec"
    ClauseRecursive
MaybeRecursive -> Doc Aspects
"?Rec"

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

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

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

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

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

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

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

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

instance Pretty a => Pretty (Pattern' a) where
  prettyPrec :: Int -> Pattern' a -> Doc Aspects
prettyPrec Int
n (VarP PatternInfo
_o a
x)   = Int -> a -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
n a
x
  prettyPrec Int
_ (DotP PatternInfo
_o Term
t)   = Doc Aspects
"." Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Int -> Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10 Term
t
  prettyPrec Int
n (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
nps)= Bool -> Doc Aspects -> Doc Aspects
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
    (Doc Aspects
lazy Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (ConHead -> QName
conName ConHead
c)) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ((Arg (Pattern' a) -> Doc Aspects)
-> [Arg (Pattern' a)] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Arg (Pattern' a) -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
          lazy :: Doc Aspects
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Doc Aspects
"~"
               | Bool
otherwise  = Doc Aspects
forall a. Null a => a
empty
  prettyPrec Int
n (DefP PatternInfo
_o QName
q [NamedArg (Pattern' a)]
nps)= Bool -> Doc Aspects -> Doc Aspects
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
    QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ((Arg (Pattern' a) -> Doc Aspects)
-> [Arg (Pattern' a)] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Arg (Pattern' a) -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
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)    = Literal -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Literal
l
  prettyPrec Int
_ (ProjP ProjOrigin
_o QName
q)  = [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char]
"." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++! QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q)
  prettyPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = Int -> a -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
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 Aspects
pretty = \case
    NotBlocked NotBlocked' Term
ReallyNotBlocked a
a -> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a
    NotBlocked NotBlocked' Term
nb a
a -> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> (Doc Aspects
"[ blocked on" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> NotBlocked' Term -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty NotBlocked' Term
nb Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"]")
    Blocked     Blocker
b a
a -> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> (Doc Aspects
"[ stuck on" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Blocker -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty  Blocker
b Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"]")

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

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

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

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

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

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

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

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

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

instance NFData a => NFData (DataOrRecord' a)
instance NFData ConHead
instance NFData a => NFData (Abs a)
instance NFData a => NFData (Tele a)
instance NFData IsFibrant
instance NFData ClauseRecursive
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)
instance NFData DefSing
instance NFData NLPat
instance NFData NLPType
instance NFData NLPSort
instance NFData RewriteHead
instance NFData LocalEquation
instance NFData RewriteRule
instance NFData RewDom