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 Data.Function (on)
import qualified Data.List as List
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>), Sum(..) )
import GHC.Generics (Generic)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Pretty (prettyHiding)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal.Blockers
import Agda.Syntax.Internal.Elim
import Agda.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.Null
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Dom' t e = Dom
{ forall t e. Dom' t e -> ArgInfo
domInfo :: ArgInfo
, forall t e. Dom' t e -> Maybe NamedName
domName :: Maybe NamedName
, forall t e. Dom' t e -> Bool
domIsFinite :: Bool
, forall t e. Dom' t e -> Maybe t
domTactic :: Maybe 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 a b. (a -> b) -> Dom' t a -> Dom' t b)
-> (forall a b. a -> Dom' t b -> Dom' t a) -> Functor (Dom' t)
forall a b. a -> Dom' t b -> Dom' t a
forall a b. (a -> b) -> Dom' t a -> Dom' t b
forall t a b. a -> Dom' t b -> Dom' t a
forall t a b. (a -> b) -> Dom' t a -> Dom' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t a b. (a -> b) -> Dom' t a -> Dom' t b
fmap :: forall a b. (a -> b) -> Dom' t a -> Dom' t b
$c<$ :: forall t a b. a -> Dom' t b -> Dom' t a
<$ :: forall a b. a -> Dom' t b -> Dom' t a
Functor, (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 t m. Monoid m => Dom' t m -> m
forall m a. Monoid m => (a -> m) -> Dom' t a -> 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)
type Dom = Dom' Term
instance Decoration (Dom' t) where
traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
traverseF a -> m b
f (Dom ArgInfo
ai Maybe NamedName
x Bool
t Maybe t
b a
a) = ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> b -> Dom' t b
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
ai Maybe NamedName
x Bool
t Maybe t
b (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 a) => KillRange (Dom' t a) where
killRange :: KillRangeT (Dom' t a)
killRange (Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b a
a) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a)
-> ArgInfo -> Maybe NamedName -> Bool -> Maybe 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 -> a -> Dom' t a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b a
a
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
_ 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
_ 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
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 { domName = 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 { domInfo = ai }
mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
mapArgInfo ArgInfo -> ArgInfo
f Dom' t e
dom = Dom' t e
dom { domInfo = f $ domInfo dom }
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 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
instance LensRelevance (Dom' t e) where
instance LensQuantity (Dom' t e) where
instance LensCohesion (Dom' t e) where
argFromDom :: Dom' t a -> Arg a
argFromDom :: forall t a. Dom' t a -> Arg a
argFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i, unDom :: forall t e. Dom' t e -> e
unDom = a
a} = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
a
namedArgFromDom :: Dom' t a -> NamedArg a
namedArgFromDom :: forall t a. Dom' t a -> NamedArg a
namedArgFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i, domName :: forall t e. Dom' t e -> Maybe NamedName
domName = Maybe NamedName
s, unDom :: forall t e. Dom' t e -> e
unDom = a
a} = 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 a
a
domFromArg :: Arg a -> Dom a
domFromArg :: forall a. Arg a -> Dom a
domFromArg (Arg ArgInfo
i a
a) = ArgInfo
-> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom' Term a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
i Maybe NamedName
forall a. Maybe a
Nothing Bool
False Maybe Term
forall a. Maybe a
Nothing a
a
domFromNamedArg :: NamedArg a -> Dom a
domFromNamedArg :: forall a. NamedArg a -> Dom a
domFromNamedArg (Arg ArgInfo
i Named_ a
a) = ArgInfo
-> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom' Term a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe 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 (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
defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom :: forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x = Arg a -> Dom a
forall a. Arg a -> Dom a
domFromArg (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
x)
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom :: forall a. ArgInfo -> [Char] -> a -> Dom a
defaultNamedArgDom ArgInfo
info [Char]
s a
x = (ArgInfo -> a -> Dom' Term a
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x) { domName = Just $ WithOrigin Inserted $ unranged s }
type Args = [Arg Term]
type NamedArgs = [NamedArg Term]
data DataOrRecord' p
= IsData
| IsRecord p
deriving (Int -> DataOrRecord' p -> ShowS
[DataOrRecord' p] -> ShowS
DataOrRecord' p -> [Char]
(Int -> DataOrRecord' p -> ShowS)
-> (DataOrRecord' p -> [Char])
-> ([DataOrRecord' p] -> ShowS)
-> Show (DataOrRecord' p)
forall p. Show p => Int -> DataOrRecord' p -> ShowS
forall p. Show p => [DataOrRecord' p] -> ShowS
forall p. Show p => DataOrRecord' p -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall p. Show p => Int -> DataOrRecord' p -> ShowS
showsPrec :: Int -> DataOrRecord' p -> ShowS
$cshow :: forall p. Show p => DataOrRecord' p -> [Char]
show :: DataOrRecord' p -> [Char]
$cshowList :: forall p. Show p => [DataOrRecord' p] -> ShowS
showList :: [DataOrRecord' p] -> ShowS
Show, DataOrRecord' p -> DataOrRecord' p -> Bool
(DataOrRecord' p -> DataOrRecord' p -> Bool)
-> (DataOrRecord' p -> DataOrRecord' p -> Bool)
-> Eq (DataOrRecord' p)
forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
== :: DataOrRecord' p -> DataOrRecord' p -> Bool
$c/= :: forall p. Eq p => DataOrRecord' p -> DataOrRecord' p -> Bool
/= :: DataOrRecord' p -> DataOrRecord' p -> Bool
Eq, (forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x)
-> (forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p)
-> Generic (DataOrRecord' p)
forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p
forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p x. Rep (DataOrRecord' p) x -> DataOrRecord' p
forall p x. DataOrRecord' p -> Rep (DataOrRecord' p) x
$cfrom :: forall p x. DataOrRecord' p -> Rep (DataOrRecord' p) x
from :: forall x. DataOrRecord' p -> Rep (DataOrRecord' p) x
$cto :: forall p x. Rep (DataOrRecord' p) x -> DataOrRecord' p
to :: forall x. Rep (DataOrRecord' p) x -> DataOrRecord' p
Generic)
type DataOrRecord = DataOrRecord' PatternOrCopattern
instance PatternMatchingAllowed DataOrRecord where
patternMatchingAllowed :: DataOrRecord -> Bool
patternMatchingAllowed = \case
DataOrRecord
IsData -> Bool
True
IsRecord PatternOrCopattern
patCopat -> PatternOrCopattern -> Bool
forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed PatternOrCopattern
patCopat
instance CopatternMatchingAllowed DataOrRecord where
copatternMatchingAllowed :: DataOrRecord -> Bool
copatternMatchingAllowed = \case
DataOrRecord
IsData -> Bool
False
IsRecord PatternOrCopattern
patCopat -> PatternOrCopattern -> Bool
forall a. CopatternMatchingAllowed a => a -> Bool
copatternMatchingAllowed PatternOrCopattern
patCopat
data ConHead = ConHead
{ ConHead -> QName
conName :: QName
, ConHead -> DataOrRecord
conDataRecord :: DataOrRecord
, ConHead -> Induction
conInductive :: Induction
, ConHead -> [Arg QName]
conFields :: [Arg QName]
} 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 }
data Term = Var {-# UNPACK #-} !Int Elims
| Lam ArgInfo (Abs Term)
| Lit Literal
| Def QName Elims
| Con ConHead ConInfo Elims
| Pi (Dom Type) (Abs Type)
| Sort Sort
| Level Level
| MetaV {-# UNPACK #-} !MetaId Elims
| DontCare Term
| Dummy String Elims
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
type ConInfo = ConOrigin
type Elim = Elim' Term
type Elims = [Elim]
data Abs a = Abs { forall a. Abs a -> [Char]
absName :: ArgName, forall a. Abs a -> a
unAbs :: a }
| NoAbs { absName :: ArgName, unAbs :: a }
deriving ((forall a b. (a -> b) -> Abs a -> Abs b)
-> (forall a b. a -> Abs b -> Abs a) -> Functor Abs
forall a b. a -> Abs b -> Abs a
forall a b. (a -> b) -> Abs a -> Abs b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Abs a -> Abs b
fmap :: forall a b. (a -> b) -> Abs a -> Abs b
$c<$ :: forall a b. a -> Abs b -> Abs a
<$ :: forall a b. a -> Abs b -> Abs a
Functor, (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 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
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 -> Lens' a Sort -> Sort
forall o i. o -> Lens' o i -> i
^. (Sort -> f Sort) -> a -> f a
forall a. LensSort a => Lens' a Sort
Lens' a Sort
lensSort
instance LensSort Sort where
lensSort :: Lens' Sort Sort
lensSort Sort -> f Sort
f Sort
s = Sort -> f Sort
f Sort
s f Sort -> (Sort -> Sort) -> f Sort
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Sort
s' -> Sort
s'
instance LensSort (Type' a) where
lensSort :: Lens' (Type' a) Sort
lensSort Sort -> f Sort
f (El Sort
s a
a) = Sort -> f Sort
f Sort
s f Sort -> (Sort -> Type' a) -> f (Type' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Sort
s' -> Sort -> a -> Type' a
forall t a. Sort' t -> a -> Type'' t a
El Sort
s' a
a
instance LensSort a => LensSort (Dom a) where
lensSort :: Lens' (Dom a) Sort
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 -> f Sort) -> a -> f a)
-> (Sort -> f Sort)
-> Dom a
-> f (Dom a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> f Sort) -> a -> f a
forall a. LensSort a => Lens' a Sort
Lens' a Sort
lensSort
instance LensSort a => LensSort (Arg a) where
lensSort :: Lens' (Arg a) Sort
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 -> f Sort) -> a -> f a)
-> (Sort -> f Sort)
-> Arg a
-> f (Arg a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> f Sort) -> a -> f a
forall a. LensSort a => Lens' a Sort
Lens' a Sort
lensSort
data Tele a = EmptyTel
| ExtendTel a (Abs (Tele a))
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)
type Telescope = Tele (Dom Type)
data UnivSize
= USmall
| ULarge
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)
data Sort' t
= Univ Univ (Level' t)
| Inf Univ !Integer
| SizeUniv
| LockUniv
| LevelUniv
| IntervalUniv
| PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))
| FunSort (Sort' t) (Sort' t)
| UnivSort (Sort' t)
| MetaS {-# UNPACK #-} !MetaId [Elim' t]
| DefS QName [Elim' t]
| DummyS String
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
isStrictDataSort :: Sort' t -> Bool
isStrictDataSort :: forall t. Sort' t -> Bool
isStrictDataSort = \case
Univ Univ
u Level' t
_ -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsStrict
Inf Univ
u Integer
_ -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsStrict
Sort' t
_ -> Bool
False
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
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
type Blocked = Blocked' Term
type NotBlocked = NotBlocked' Term
type Blocked_ = Blocked ()
type NAPs = [NamedArg DeBruijnPattern]
data Clause = Clause
{ Clause -> Range
clauseLHSRange :: Range
, Clause -> Range
clauseFullRange :: Range
, Clause -> Telescope
clauseTel :: Telescope
, Clause -> NAPs
namedClausePats :: NAPs
, Clause -> Maybe Term
clauseBody :: Maybe Term
, Clause -> Maybe (Arg Type)
clauseType :: Maybe (Arg Type)
, Clause -> Bool
clauseCatchall :: Bool
, Clause -> Maybe Bool
clauseExact :: Maybe Bool
, Clause -> Maybe Bool
clauseRecursive :: Maybe Bool
, Clause -> Maybe Bool
clauseUnreachable :: Maybe Bool
, Clause -> ExpandedEllipsis
clauseEllipsis :: ExpandedEllipsis
, Clause -> Maybe ModuleName
clauseWhereModule :: Maybe ModuleName
}
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
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 []
data PatOrigin
= PatOSystem
| PatOSplit
| PatOVar Name
| PatODot
| PatOWild
| PatOCon
| PatORec
| PatOLit
| PatOAbsurd
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)
data Pattern' x
= VarP PatternInfo x
| DotP PatternInfo Term
| ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
| LitP PatternInfo Literal
| ProjP ProjOrigin QName
| IApplyP PatternInfo Term Term x
| DefP PatternInfo QName [NamedArg (Pattern' x)]
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
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
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
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
data ConPatternInfo = ConPatternInfo
{ ConPatternInfo -> PatternInfo
conPInfo :: PatternInfo
, ConPatternInfo -> Bool
conPRecord :: Bool
, ConPatternInfo -> Bool
conPFallThrough :: Bool
, ConPatternInfo -> Maybe (Arg Type)
conPType :: Maybe (Arg Type)
, ConPatternInfo -> Bool
conPLazy :: Bool
}
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
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ConORec = ConPatternInfo
noConPatternInfo{ conPInfo = PatternInfo PatORec [] , conPRecord = True }
toConPatternInfo ConInfo
_ = ConPatternInfo
noConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
i = PatOrigin -> ConInfo
patToConO (PatOrigin -> ConInfo) -> PatOrigin -> ConInfo
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 -> ConInfo
patToConO = \case
PatOrigin
PatOSystem -> ConInfo
ConOSystem
PatOrigin
PatOSplit -> ConInfo
ConOSplit
PatOVar{} -> ConInfo
ConOSystem
PatOrigin
PatODot -> ConInfo
ConOSystem
PatOrigin
PatOWild -> ConInfo
ConOSystem
PatOrigin
PatOCon -> ConInfo
ConOCon
PatOrigin
PatORec -> ConInfo
ConORec
PatOrigin
PatOLit -> ConInfo
ConOCon
PatOrigin
PatOAbsurd -> ConInfo
ConOSystem
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 (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
$ a -> Either a Term
forall a b. a -> Either a b
Left 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 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
$ a -> Either a Term
forall a b. a -> Either a b
Left a
x]
instance PatternVars (NamedArg (Pattern' a)) where
type PatternVarOut (NamedArg (Pattern' a)) = a
patternVars :: NamedArg (Pattern' a)
-> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)]
patternVars = 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
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
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
properlyMatching :: Pattern' a -> Bool
properlyMatching :: forall a. Pattern' a -> Bool
properlyMatching = Bool -> Bool -> Pattern' a -> Bool
forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
True Bool
True
properlyMatching'
:: Bool
-> Bool
-> Pattern' a
-> Bool
properlyMatching' :: forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
absP Bool
projP = \case
Pattern' a
p | Bool
absP Bool -> Bool -> Bool
&& Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p Maybe PatOrigin -> Maybe PatOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== PatOrigin -> Maybe PatOrigin
forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd -> Bool
True
ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' a)]
ps
| ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci -> (NamedArg (Pattern' a) -> Bool) -> [NamedArg (Pattern' a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any (Pattern' a -> Bool
forall a. Pattern' a -> Bool
properlyMatching (Pattern' a -> Bool)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps
| Bool
otherwise -> Bool
True
LitP{} -> Bool
True
DefP{} -> Bool
True
ProjP{} -> Bool
projP
VarP{} -> Bool
False
DotP{} -> Bool
False
IApplyP{} -> Bool
False
instance IsProjP (Pattern' a) where
isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP = \case
ProjP ProjOrigin
o QName
d -> (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
data Substitution' a
= IdS
| EmptyS Impossible
| a :# Substitution' a
| Strengthen Impossible !Int (Substitution' a)
| Wk !Int (Substitution' a)
| Lift !Int (Substitution' a)
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
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
data EqualityView
= EqualityViewType EqualityTypeData
| OtherType Type
| IdiomType Type
data EqualityTypeData = EqualityTypeData
{ EqualityTypeData -> Sort
_eqtSort :: Sort
, EqualityTypeData -> QName
_eqtName :: QName
, EqualityTypeData -> Args
_eqtParams :: Args
, EqualityTypeData -> Arg Term
_eqtType :: Arg Term
, EqualityTypeData -> Arg Term
_eqtLhs :: Arg Term
, EqualityTypeData -> Arg Term
_eqtRhs :: Arg Term
}
pattern EqualityType
:: Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
pattern $mEqualityType :: forall {r}.
EqualityView
-> (Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> r)
-> ((# #) -> r)
-> r
$bEqualityType :: Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType{ EqualityView -> Sort
eqtSort, EqualityView -> QName
eqtName, EqualityView -> Args
eqtParams, EqualityView -> Arg Term
eqtType, EqualityView -> Arg Term
eqtLhs, EqualityView -> Arg Term
eqtRhs } =
EqualityViewType (EqualityTypeData eqtSort eqtName eqtParams eqtType eqtLhs eqtRhs)
{-# COMPLETE EqualityType, OtherType, IdiomType #-}
isEqualityType :: EqualityView -> Bool
isEqualityType :: EqualityView -> Bool
isEqualityType EqualityType{} = Bool
True
isEqualityType OtherType{} = Bool
False
isEqualityType IdiomType{} = Bool
False
data PathView
= PathType
{ PathView -> Sort
pathSort :: Sort
, PathView -> QName
pathName :: QName
, PathView -> Arg Term
pathLevel :: Arg Term
, PathView -> Arg Term
pathType :: Arg Term
, PathView -> Arg Term
pathLhs :: Arg Term
, PathView -> Arg Term
pathRhs :: Arg Term
}
| OType Type
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
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 -> Elims -> 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
var :: Nat -> Term
var :: Int -> Term
var Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int -> Elims -> Term
Var Int
i []
| Bool
otherwise = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
dontCare :: Term -> Term
dontCare :: Term -> Term
dontCare Term
v =
case Term
v of
DontCare{} -> Term
v
Term
_ -> Term -> Term
DontCare Term
v
type DummyTermKind = String
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)
dummyTermWith :: DummyTermKind -> CallStack -> Term
dummyTermWith :: [Char] -> CallStack -> Term
dummyTermWith [Char]
kind CallStack
cs = ([Char] -> Elims -> Term) -> Elims -> [Char] -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> Elims -> Term
Dummy [] ([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]
dummyLevel :: CallStack -> Level
dummyLevel :: CallStack -> Level
dummyLevel = Term -> Level
forall t. t -> Level' t
atomicLevel (Term -> Level) -> (CallStack -> Term) -> CallStack -> Level
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> CallStack -> Term
dummyTermWith [Char]
"dummyLevel"
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
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ = (CallStack -> Level) -> Level
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Level
dummyLevel
dummySort :: CallStack -> Sort
dummySort :: CallStack -> Sort
dummySort = [Char] -> Sort
forall t. [Char] -> Sort' t
DummyS ([Char] -> Sort) -> (CallStack -> [Char]) -> CallStack -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [Char]
dummyLocName
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ = (CallStack -> Sort) -> Sort
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Sort
dummySort
dummyType :: CallStack -> Type
dummyType :: CallStack -> Type
dummyType CallStack
cs = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (CallStack -> Sort
dummySort CallStack
cs) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ [Char] -> CallStack -> Term
dummyTermWith [Char]
"dummyType" CallStack
cs
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ = (CallStack -> Type) -> Type
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Type
dummyType
dummyDom :: CallStack -> Dom Type
dummyDom :: CallStack -> Dom Type
dummyDom = Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> (CallStack -> Type) -> CallStack -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Type
dummyType
__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ = (CallStack -> Dom Type) -> Dom Type
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Dom Type
dummyDom
pattern ClosedLevel :: Integer -> Level
pattern $mClosedLevel :: forall {r}. Level -> (Integer -> r) -> ((# #) -> r) -> r
$bClosedLevel :: Integer -> Level
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
varSort Int
n = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel (Term -> Level) -> Term -> Level
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
n
tmSort :: Term -> Sort
tmSort :: Term -> Sort
tmSort Term
t = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel Term
t
tmSSort :: Term -> Sort
tmSSort :: Term -> Sort
tmSSort Term
t = Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Term -> Level
forall t. t -> Level' t
atomicLevel Term
t
levelPlus :: Integer -> Level -> Level
levelPlus :: Integer -> Level -> Level
levelPlus Integer
m (Max Integer
n [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ (PlusLevel' Term -> PlusLevel' Term)
-> [PlusLevel' Term] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> PlusLevel' Term
pplus [PlusLevel' Term]
as
where pplus :: PlusLevel' Term -> PlusLevel' Term
pplus (Plus Integer
n Term
l) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) Term
l
levelSuc :: Level -> Level
levelSuc :: Level -> Level
levelSuc = Integer -> Level -> Level
levelPlus Integer
1
mkType :: Integer -> Sort
mkType :: Integer -> Sort
mkType Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
mkProp :: Integer -> Sort
mkProp :: Integer -> Sort
mkProp Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
mkSSet :: Integer -> Sort
mkSSet :: Integer -> Sort
mkSSet Integer
n = Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
isSort :: Term -> Maybe Sort
isSort :: Term -> Maybe Sort
isSort = \case
Sort Sort
s -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
Term
_ -> Maybe Sort
forall a. Maybe a
Nothing
impossibleTerm :: CallStack -> Term
impossibleTerm :: CallStack -> Term
impossibleTerm = ([Char] -> Elims -> Term) -> Elims -> [Char] -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> Elims -> Term
Dummy [] ([Char] -> Term) -> (CallStack -> [Char]) -> CallStack -> Term
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
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]
f 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)
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)
replaceEmptyName :: ArgName -> Tele a -> Tele a
replaceEmptyName :: forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
x = ShowS -> Tele a -> Tele a
forall a. ShowS -> Tele a -> Tele a
mapAbsNames (ShowS -> Tele a -> Tele a) -> ShowS -> Tele a -> Tele a
forall a b. (a -> b) -> a -> b
$ \ [Char]
y -> if [Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
y then [Char]
x else [Char]
y
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 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)
telFromList :: ListTel -> Telescope
telFromList :: ListTel -> Telescope
telFromList = ShowS -> ListTel -> Telescope
forall a. (a -> [Char]) -> ListTel' a -> Telescope
telFromList' ShowS
forall a. a -> a
id
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]
: 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__
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
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) -> Arg [Char]) -> ListTel -> [Arg [Char]])
-> (Dom ([Char], Type) -> Arg [Char]) -> ListTel -> [Arg [Char]]
forall a b. (a -> b) -> a -> b
$ \ 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
class SgTel a where
sgTel :: a -> Telescope
instance SgTel (ArgName, Dom Type) where
sgTel :: ([Char], Dom Type) -> Telescope
sgTel ([Char]
x, !Dom Type
dom) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom 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 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 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 Type -> Telescope
sgTel Dom Type
dom = ([Char], Dom Type) -> Telescope
forall a. SgTel a => a -> Telescope
sgTel (ShowS
stringToArgName [Char]
"_", Dom Type
dom)
stripDontCare :: Term -> Term
stripDontCare :: Term -> Term
stripDontCare = \case
DontCare Term
v -> Term
v
Term
v -> Term
v
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 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
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
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
unSpine :: Term -> Term
unSpine :: Term -> Term
unSpine = (ProjOrigin -> QName -> Bool) -> Term -> Term
unSpine' ((ProjOrigin -> QName -> Bool) -> Term -> Term)
-> (ProjOrigin -> QName -> Bool) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ \ProjOrigin
_ QName
_ -> Bool
True
unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
unSpine' ProjOrigin -> QName -> Bool
p Term
v =
case Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v of
Just (Elims -> Term
h, Elims
es) -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h [] Elims
es
Maybe (Elims -> Term, Elims)
Nothing -> Term
v
where
loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h Elims
res Elims
es =
case Elims
es of
[] -> Term
v
Proj ProjOrigin
o QName
f : Elims
es' | ProjOrigin -> QName -> Bool
p ProjOrigin
o QName
f -> (Elims -> Term) -> Elims -> Elims -> Term
loop (QName -> Elims -> Term
Def QName
f) [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v)] Elims
es'
Elim' Term
e : Elims
es' -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h (Elim' Term
e Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
res) Elims
es'
where v :: Term
v = Elims -> Term
h (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. [a] -> [a]
reverse Elims
res
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v =
case Term
v of
Var Int
i Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (Int -> Elims -> Term
Var Int
i, Elims
es)
Def QName
f Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def QName
f, Elims
es)
MetaV MetaId
x Elims
es -> (Elims -> Term, Elims) -> Maybe (Elims -> Term, Elims)
forall a. a -> Maybe a
Just (MetaId -> Elims -> Term
MetaV MetaId
x, Elims
es)
Con{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Lit{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Lam{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Pi{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Sort{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Level{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
DontCare{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
Dummy{} -> Maybe (Elims -> Term, Elims)
forall a. Maybe a
Nothing
type family TypeOf a
type instance TypeOf Term = Type
type instance TypeOf Elims = (Type, Elims -> Term)
type instance TypeOf (Abs Term) = (Dom Type, Abs Type)
type instance TypeOf (Abs Type) = Dom 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 = ()
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 Clause where
empty :: Clause
empty = Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause 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 Bool
False Maybe Bool
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing 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)
_ Bool
_ Maybe Bool
_ Maybe Bool
_ 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
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 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
class TermSize a where
termSize :: a -> Int
termSize = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize
tsize :: a -> Sum Int
instance {-# OVERLAPPABLE #-} (Foldable t, TermSize a) => TermSize (t a) where
tsize :: t a -> Sum Int
tsize = (a -> Sum Int) -> t a -> Sum Int
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize
instance TermSize Term where
tsize :: Term -> Sum Int
tsize = \case
Var Int
_ Elims
vs -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Def QName
_ Elims
vs -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Con ConHead
_ ConInfo
_ Elims
vs -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
MetaV MetaId
_ Elims
vs -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Level Level
l -> Level -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Level
l
Lam ArgInfo
_ Abs Term
f -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Term
f
Lit Literal
_ -> Sum Int
1
Pi Dom Type
a Abs Type
b -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Dom Type -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Dom Type
a Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Type -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Type
b
Sort Sort
s -> Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s
DontCare Term
mv -> Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Term
mv
Dummy{} -> Sum Int
1
instance TermSize Sort where
tsize :: Sort -> Sum Int
tsize = \case
Univ Univ
_ Level
l -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Level -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Level
l
Inf Univ
_ Integer
_ -> Sum Int
1
Sort
SizeUniv -> Sum Int
1
Sort
LockUniv -> Sum Int
1
Sort
LevelUniv -> Sum Int
1
Sort
IntervalUniv -> Sum Int
1
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Dom' Term Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Dom' Term Term
a Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Abs Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Abs Sort
s2
FunSort Sort
s1 Sort
s2 -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s2
UnivSort Sort
s -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Sort -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Sort
s
MetaS MetaId
_ Elims
es -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
es
DefS QName
_ Elims
es -> Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Elims -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Elims
es
DummyS{} -> Sum Int
1
instance TermSize Level where
tsize :: Level -> Sum Int
tsize (Max Integer
_ [PlusLevel' Term]
as) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ [PlusLevel' Term] -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize [PlusLevel' Term]
as
instance TermSize PlusLevel where
tsize :: PlusLevel' Term -> Sum Int
tsize (Plus Integer
_ Term
a) = Term -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Term
a
instance TermSize a => TermSize (Substitution' a) where
tsize :: Substitution' a -> Sum Int
tsize Substitution' a
IdS = Sum Int
1
tsize (EmptyS Impossible
_) = Sum Int
1
tsize (Wk Int
_ Substitution' a
rho) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (a
t :# Substitution' a
rho) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize a
t Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (Strengthen Impossible
_ Int
_ Substitution' a
rho) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (Lift Int
_ Substitution' a
rho) = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Substitution' a -> Sum Int
forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
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 Elims
vs -> (Elims -> Term) -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Int -> Elims -> Term
Var Int
i) Elims
vs
Def QName
c Elims
vs -> (QName -> Elims -> Term) -> QName -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Elims -> Term
Def QName
c Elims
vs
Con ConHead
c ConInfo
ci Elims
vs -> (ConHead -> ConInfo -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci Elims
vs
MetaV MetaId
m Elims
vs -> (Elims -> Term) -> Elims -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (MetaId -> Elims -> Term
MetaV MetaId
m) Elims
vs
Lam ArgInfo
i Abs Term
f -> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo -> Abs Term -> Term
Lam ArgInfo
i Abs Term
f
Lit Literal
l -> (Literal -> Term) -> Literal -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Literal -> Term
Lit Literal
l
Level Level
l -> (Level -> Term) -> Level -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Level -> Term
Level Level
l
Pi Dom Type
a Abs Type
b -> (Dom Type -> Abs Type -> Term) -> Dom Type -> Abs Type -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b
Sort Sort
s -> (Sort -> Term) -> Sort -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort -> Term
Sort Sort
s
DontCare Term
mv -> (Term -> Term) -> Term -> Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Term -> Term
DontCare Term
mv
v :: Term
v@Dummy{} -> Term
v
instance KillRange Level where
killRange :: Level -> Level
killRange (Max Integer
n [PlusLevel' Term]
as) = ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) [PlusLevel' Term]
as
instance KillRange PlusLevel where
killRange :: PlusLevel' Term -> PlusLevel' Term
killRange (Plus Integer
n Term
l) = (Term -> PlusLevel' Term) -> Term -> PlusLevel' Term
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) Term
l
instance (KillRange a) => KillRange (Type' a) where
killRange :: KillRangeT (Type' a)
killRange (El Sort
s a
v) = (Sort -> a -> Type' a) -> Sort -> a -> Type' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort -> a -> Type' a
forall t a. Sort' t -> a -> Type'' t a
El Sort
s a
v
instance KillRange Sort where
killRange :: Sort -> Sort
killRange = \case
Inf Univ
u Integer
n -> Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
Sort
SizeUniv -> Sort
forall t. Sort' t
SizeUniv
Sort
LockUniv -> Sort
forall t. Sort' t
LockUniv
Sort
LevelUniv -> Sort
forall t. Sort' t
LevelUniv
Sort
IntervalUniv -> Sort
forall t. Sort' t
IntervalUniv
Univ Univ
u Level
a -> (Level -> Sort) -> Level -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u) Level
a
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2
FunSort Sort
s1 Sort
s2 -> (Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2
UnivSort Sort
s -> (Sort -> Sort) -> Sort -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s
MetaS MetaId
x Elims
es -> (Elims -> Sort) -> Elims -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x) Elims
es
DefS QName
d Elims
es -> (QName -> Elims -> Sort) -> QName -> Elims -> Sort
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es
s :: Sort
s@DummyS{} -> Sort
s
instance KillRange Substitution where
killRange :: KillRangeT Substitution
killRange Substitution
IdS = 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 = KillRangeT PatOrigin
forall a. a -> a
id
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 Clause where
killRange :: KillRangeT Clause
killRange (Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
(Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause)
-> Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> 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)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm
instance KillRange a => KillRange (Tele a) where
killRange :: KillRangeT (Tele a)
killRange = (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
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 Elims
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 -> Elims -> Doc Aspects
`pApp` Elims
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 Elims
els -> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q Doc Aspects -> Elims -> Doc Aspects
`pApp` Elims
els
Con ConHead
c ConInfo
ci Elims
vs -> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (ConHead -> QName
conName ConHead
c) Doc Aspects -> Elims -> Doc Aspects
`pApp` Elims
vs
Pi Dom 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 [ Int -> Type -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
1 (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom 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 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 Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
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 Type -> Type
forall t e. Dom' t e -> e
unDom Dom 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
s -> Int -> Sort -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Sort
s
Level Level
l -> Int -> Level -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Level
l
MetaV MetaId
x Elims
els -> MetaId -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty MetaId
x Doc Aspects -> Elims -> Doc Aspects
`pApp` Elims
els
DontCare Term
v -> Int -> Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
p Term
v
Dummy [Char]
s Elims
es -> Doc Aspects -> Doc Aspects
parens ([Char] -> Doc Aspects
forall a. [Char] -> Doc a
text [Char]
s) Doc Aspects -> Elims -> Doc Aspects
`pApp` Elims
es
where
pApp :: Doc Aspects -> Elims -> Doc Aspects
pApp Doc Aspects
d Elims
els = Bool -> Doc Aspects -> Doc Aspects
mparens (Bool -> Bool
not (Elims -> Bool
forall a. Null a => a -> Bool
null Elims
els) Bool -> Bool -> Bool
&& Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc 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' Term -> Doc Aspects) -> Elims -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Elim' Term -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10) Elims
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 (e -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (e -> Doc Aspects) -> e -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ 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 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 -> 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 -> Doc Aspects
prettyPrec Int
p Sort
s =
case Sort
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
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 -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10 Level
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
SizeUniv -> Doc Aspects
"SizeUniv"
Sort
LockUniv -> Doc Aspects
"LockUniv"
Sort
LevelUniv -> Doc Aspects
"LevelUniv"
Sort
IntervalUniv -> Doc Aspects
"IntervalUniv"
PiSort Dom' Term Term
a Sort
s1 Abs Sort
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 -> [Char]
forall a. Abs a -> [Char]
absName Abs Sort
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 -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Sort
s1)
Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects -> Doc Aspects
parens (Sort -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (Abs Sort -> Sort
forall a. Abs a -> a
unAbs Abs Sort
s2))
FunSort Sort
a Sort
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 -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10 Sort
a Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Sort -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10 Sort
b
UnivSort Sort
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 -> Doc Aspects
forall a. Pretty a => Int -> a -> Doc Aspects
prettyPrec Int
10 Sort
s
MetaS MetaId
x Elims
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 -> Elims -> Term
MetaV MetaId
x Elims
es
DefS QName
d Elims
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 -> Elims -> Term
Def QName
d Elims
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
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
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
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 NFData Term where
rnf :: Term -> ()
rnf = \case
Var Int
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
Lam ArgInfo
_ Abs Term
b -> Term -> ()
forall a. NFData a => a -> ()
rnf (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
Lit Literal
l -> Literal -> ()
forall a. NFData a => a -> ()
rnf Literal
l
Def QName
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
Con ConHead
_ ConInfo
_ Elims
vs -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
vs
Pi Dom Type
a Abs Type
b -> (Type, Type) -> ()
forall a. NFData a => a -> ()
rnf (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a, Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
Sort Sort
s -> Sort -> ()
forall a. NFData a => a -> ()
rnf Sort
s
Level Level
l -> Level -> ()
forall a. NFData a => a -> ()
rnf Level
l
MetaV MetaId
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
DontCare Term
v -> Term -> ()
forall a. NFData a => a -> ()
rnf Term
v
Dummy [Char]
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
instance NFData Type where
rnf :: Type -> ()
rnf (El Sort
s Term
v) = (Sort, Term) -> ()
forall a. NFData a => a -> ()
rnf (Sort
s, Term
v)
instance NFData Sort where
rnf :: Sort -> ()
rnf = \case
Univ Univ
_ Level
l -> Level -> ()
forall a. NFData a => a -> ()
rnf Level
l
Inf Univ
_ Integer
_ -> ()
Sort
SizeUniv -> ()
Sort
LockUniv -> ()
Sort
LevelUniv -> ()
Sort
IntervalUniv -> ()
PiSort Dom' Term Term
a Sort
b Abs Sort
c -> (Dom' Term Term, Sort, Sort) -> ()
forall a. NFData a => a -> ()
rnf (Dom' Term Term
a, Sort
b, Abs Sort -> Sort
forall a. Abs a -> a
unAbs Abs Sort
c)
FunSort Sort
a Sort
b -> (Sort, Sort) -> ()
forall a. NFData a => a -> ()
rnf (Sort
a, Sort
b)
UnivSort Sort
a -> Sort -> ()
forall a. NFData a => a -> ()
rnf Sort
a
MetaS MetaId
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
DefS QName
_ Elims
es -> Elims -> ()
forall a. NFData a => a -> ()
rnf Elims
es
DummyS [Char]
_ -> ()
instance NFData Level where
rnf :: Level -> ()
rnf (Max Integer
n [PlusLevel' Term]
as) = (Integer, [PlusLevel' Term]) -> ()
forall a. NFData a => a -> ()
rnf (Integer
n, [PlusLevel' Term]
as)
instance NFData PlusLevel where
rnf :: PlusLevel' Term -> ()
rnf (Plus Integer
n Term
l) = (Integer, Term) -> ()
forall a. NFData a => a -> ()
rnf (Integer
n, Term
l)
instance NFData e => NFData (Dom e) where
rnf :: Dom e -> ()
rnf (Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e e
f) = 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` e -> ()
forall a. NFData a => a -> ()
rnf e
f
instance NFData DataOrRecord
instance NFData ConHead
instance NFData a => NFData (Abs a)
instance NFData a => NFData (Tele a)
instance NFData IsFibrant
instance NFData Clause
instance NFData PatternInfo
instance NFData PatOrigin
instance NFData x => NFData (Pattern' x)
instance NFData DBPatVar
instance NFData ConPatternInfo
instance NFData a => NFData (Substitution' a)