{-# LANGUAGE PatternSynonyms #-}
module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Internal.Blockers
, module Agda.Syntax.Internal.Elim
, module Agda.Syntax.Abstract.Name
, MetaId(..), ProblemId(..)
) where
import Prelude hiding (null)
import Control.Monad.Identity
import Control.DeepSeq
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>), Sum(..) )
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Traversable
import Data.Data (Data)
import GHC.Generics (Generic)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Pretty (prettyHiding)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal.Blockers
import Agda.Syntax.Internal.Elim
import Agda.Utils.CallStack
( CallStack
, HasCallStack
, prettyCallSite
, headCallSite
, withCallerCallStack
)
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Pretty
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Dom' t e = Dom
{ forall t e. Dom' t e -> ArgInfo
domInfo :: ArgInfo
, forall t e. Dom' t e -> Bool
domFinite :: !Bool
, forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName :: Maybe NamedName
, forall t e. Dom' t e -> Maybe t
domTactic :: Maybe t
, forall t e. Dom' t e -> e
unDom :: e
} deriving (Dom' t e -> Constr
Dom' t e -> DataType
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {t} {e}. (Data t, Data e) => Typeable (Dom' t e)
forall t e. (Data t, Data e) => Dom' t e -> Constr
forall t e. (Data t, Data e) => Dom' t e -> DataType
forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Dom' t e -> Dom' t e
forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Dom' t e -> u
forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Dom' t e -> [u]
forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dom' t e)
forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dom' t e -> c (Dom' t e)
forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Dom' t e))
forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dom' t e))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dom' t e)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dom' t e -> c (Dom' t e)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dom' t e))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
$cgmapMo :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
$cgmapMp :: forall t e (m :: * -> *).
(Data t, Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
$cgmapM :: forall t e (m :: * -> *).
(Data t, Data e, Monad m) =>
(forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Dom' t e -> u
$cgmapQi :: forall t e u.
(Data t, Data e) =>
Int -> (forall d. Data d => d -> u) -> Dom' t e -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Dom' t e -> [u]
$cgmapQ :: forall t e u.
(Data t, Data e) =>
(forall d. Data d => d -> u) -> Dom' t e -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
$cgmapQr :: forall t e r r'.
(Data t, Data e) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
$cgmapQl :: forall t e r r'.
(Data t, Data e) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Dom' t e -> r
gmapT :: (forall b. Data b => b -> b) -> Dom' t e -> Dom' t e
$cgmapT :: forall t e.
(Data t, Data e) =>
(forall b. Data b => b -> b) -> Dom' t e -> Dom' t e
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dom' t e))
$cdataCast2 :: forall t e (t :: * -> * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dom' t e))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Dom' t e))
$cdataCast1 :: forall t e (t :: * -> *) (c :: * -> *).
(Data t, Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Dom' t e))
dataTypeOf :: Dom' t e -> DataType
$cdataTypeOf :: forall t e. (Data t, Data e) => Dom' t e -> DataType
toConstr :: Dom' t e -> Constr
$ctoConstr :: forall t e. (Data t, Data e) => Dom' t e -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dom' t e)
$cgunfold :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dom' t e)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dom' t e -> c (Dom' t e)
$cgfoldl :: forall t e (c :: * -> *).
(Data t, Data e) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dom' t e -> c (Dom' t e)
Data, Int -> Dom' t e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
forall t e. (Show t, Show e) => Dom' t e -> ArgName
showList :: [Dom' t e] -> ShowS
$cshowList :: forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
show :: Dom' t e -> ArgName
$cshow :: forall t e. (Show t, Show e) => Dom' t e -> ArgName
showsPrec :: Int -> Dom' t e -> ShowS
$cshowsPrec :: forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
Show, forall a b. a -> Dom' t b -> Dom' t a
forall a b. (a -> b) -> Dom' t a -> Dom' t b
forall t a b. a -> Dom' t b -> Dom' t a
forall t a b. (a -> b) -> Dom' t a -> Dom' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Dom' t b -> Dom' t a
$c<$ :: forall t a b. a -> Dom' t b -> Dom' t a
fmap :: forall a b. (a -> b) -> Dom' t a -> Dom' t b
$cfmap :: forall t a b. (a -> b) -> Dom' t a -> Dom' t b
Functor, forall a. Dom' t a -> Bool
forall t a. Eq a => a -> Dom' t a -> Bool
forall t a. Num a => Dom' t a -> a
forall t a. Ord a => Dom' t a -> a
forall m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t m. Monoid m => Dom' t m -> m
forall t e. Dom' t e -> Bool
forall t a. Dom' t a -> Int
forall t a. Dom' t a -> [a]
forall a b. (a -> b -> b) -> b -> Dom' t a -> b
forall t a. (a -> a -> a) -> Dom' t a -> a
forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Dom' t a -> a
$cproduct :: forall t a. Num a => Dom' t a -> a
sum :: forall a. Num a => Dom' t a -> a
$csum :: forall t a. Num a => Dom' t a -> a
minimum :: forall a. Ord a => Dom' t a -> a
$cminimum :: forall t a. Ord a => Dom' t a -> a
maximum :: forall a. Ord a => Dom' t a -> a
$cmaximum :: forall t a. Ord a => Dom' t a -> a
elem :: forall a. Eq a => a -> Dom' t a -> Bool
$celem :: forall t a. Eq a => a -> Dom' t a -> Bool
length :: forall a. Dom' t a -> Int
$clength :: forall t a. Dom' t a -> Int
null :: forall a. Dom' t a -> Bool
$cnull :: forall t e. Dom' t e -> Bool
toList :: forall a. Dom' t a -> [a]
$ctoList :: forall t a. Dom' t a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$cfoldr1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
fold :: forall m. Monoid m => Dom' t m -> m
$cfold :: forall t m. Monoid m => Dom' t m -> m
Foldable, forall t. Functor (Dom' t)
forall t. Foldable (Dom' t)
forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
sequence :: forall (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
$csequence :: forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
Traversable)
type Dom = Dom' Term
instance Decoration (Dom' t) where
traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
traverseF a -> m b
f (Dom ArgInfo
ai Bool
b Maybe (WithOrigin (Ranged ArgName))
x Maybe t
t a
a) = forall t e.
ArgInfo
-> Bool
-> Maybe (WithOrigin (Ranged ArgName))
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
ai Bool
b Maybe (WithOrigin (Ranged ArgName))
x Maybe t
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
instance HasRange a => HasRange (Dom' t a) where
getRange :: Dom' t a -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom
instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
killRange :: KillRangeT (Dom' t a)
killRange (Dom ArgInfo
info Bool
b Maybe (WithOrigin (Ranged ArgName))
x Maybe t
t a
a) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 forall t e.
ArgInfo
-> Bool
-> Maybe (WithOrigin (Ranged ArgName))
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
info Bool
b Maybe (WithOrigin (Ranged ArgName))
x Maybe t
t a
a
instance Eq a => Eq (Dom' t a) where
Dom (ArgInfo Hiding
h1 Modality
m1 Origin
_ FreeVariables
_ Annotation
a1) Bool
b1 Maybe (WithOrigin (Ranged ArgName))
s1 Maybe t
_ a
x1 == :: Dom' t a -> Dom' t a -> Bool
== Dom (ArgInfo Hiding
h2 Modality
m2 Origin
_ FreeVariables
_ Annotation
a2) Bool
b2 Maybe (WithOrigin (Ranged ArgName))
s2 Maybe t
_ a
x2 =
(Hiding
h1, Modality
m1, Annotation
a1, Bool
b1, Maybe (WithOrigin (Ranged ArgName))
s1, a
x1) forall a. Eq a => a -> a -> Bool
== (Hiding
h2, Modality
m2, Annotation
a2, Bool
b2, Maybe (WithOrigin (Ranged ArgName))
s2, a
x2)
instance LensNamed (Dom' t e) where
type NameOf (Dom' t e) = NamedName
lensNamed :: Lens' (Maybe (NameOf (Dom' t e))) (Dom' t e)
lensNamed Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f Dom' t e
dom = Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f (forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName Dom' t e
dom) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Maybe (WithOrigin (Ranged ArgName))
nm -> Dom' t e
dom { domName :: Maybe (WithOrigin (Ranged ArgName))
domName = Maybe (WithOrigin (Ranged ArgName))
nm }
instance LensArgInfo (Dom' t e) where
getArgInfo :: Dom' t e -> ArgInfo
getArgInfo = forall t e. Dom' t e -> ArgInfo
domInfo
setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e
setArgInfo ArgInfo
ai Dom' t e
dom = Dom' t e
dom { domInfo :: ArgInfo
domInfo = ArgInfo
ai }
mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e
mapArgInfo ArgInfo -> ArgInfo
f Dom' t e
dom = Dom' t e
dom { domInfo :: ArgInfo
domInfo = ArgInfo -> ArgInfo
f forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom' t e
dom }
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} = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
a
namedArgFromDom :: Dom' t a -> NamedArg a
namedArgFromDom :: forall t a. Dom' t a -> NamedArg a
namedArgFromDom Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i, domName :: forall t e. Dom' t e -> Maybe (WithOrigin (Ranged ArgName))
domName = Maybe (WithOrigin (Ranged ArgName))
s, unDom :: forall t e. Dom' t e -> e
unDom = a
a} = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
s a
a
domFromArg :: Arg a -> Dom a
domFromArg :: forall a. Arg a -> Dom a
domFromArg (Arg ArgInfo
i a
a) = forall t e.
ArgInfo
-> Bool
-> Maybe (WithOrigin (Ranged ArgName))
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
i Bool
False forall a. Maybe a
Nothing forall a. Maybe a
Nothing a
a
domFromNamedArg :: NamedArg a -> Dom a
domFromNamedArg :: forall a. NamedArg a -> Dom a
domFromNamedArg (Arg ArgInfo
i Named_ a
a) = forall t e.
ArgInfo
-> Bool
-> Maybe (WithOrigin (Ranged ArgName))
-> Maybe t
-> e
-> Dom' t e
Dom ArgInfo
i Bool
False (forall name a. Named name a -> Maybe name
nameOf Named_ a
a) forall a. Maybe a
Nothing (forall name a. Named name a -> a
namedThing Named_ a
a)
defaultDom :: a -> Dom a
defaultDom :: forall a. a -> Dom a
defaultDom = forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
defaultArgInfo
defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom :: forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x = forall a. Arg a -> Dom a
domFromArg (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
x)
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom :: forall a. ArgInfo -> ArgName -> a -> Dom a
defaultNamedArgDom ArgInfo
info ArgName
s a
x = (forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info a
x) { domName :: Maybe (WithOrigin (Ranged ArgName))
domName = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged ArgName
s }
type Args = [Arg Term]
type NamedArgs = [NamedArg Term]
data DataOrRecord
= IsData
| IsRecord PatternOrCopattern
deriving (Typeable DataOrRecord
DataOrRecord -> Constr
DataOrRecord -> DataType
(forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u
forall u. (forall d. Data d => d -> u) -> DataOrRecord -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataOrRecord
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataOrRecord)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataOrRecord)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DataOrRecord -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataOrRecord -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r
gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord
$cgmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataOrRecord)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataOrRecord)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataOrRecord)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataOrRecord)
dataTypeOf :: DataOrRecord -> DataType
$cdataTypeOf :: DataOrRecord -> DataType
toConstr :: DataOrRecord -> Constr
$ctoConstr :: DataOrRecord -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataOrRecord
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataOrRecord
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord
Data, Int -> DataOrRecord -> ShowS
[DataOrRecord] -> ShowS
DataOrRecord -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DataOrRecord] -> ShowS
$cshowList :: [DataOrRecord] -> ShowS
show :: DataOrRecord -> ArgName
$cshow :: DataOrRecord -> ArgName
showsPrec :: Int -> DataOrRecord -> ShowS
$cshowsPrec :: Int -> DataOrRecord -> ShowS
Show, DataOrRecord -> DataOrRecord -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataOrRecord -> DataOrRecord -> Bool
$c/= :: DataOrRecord -> DataOrRecord -> Bool
== :: DataOrRecord -> DataOrRecord -> Bool
$c== :: DataOrRecord -> DataOrRecord -> Bool
Eq, forall x. Rep DataOrRecord x -> DataOrRecord
forall x. DataOrRecord -> Rep DataOrRecord x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataOrRecord x -> DataOrRecord
$cfrom :: forall x. DataOrRecord -> Rep DataOrRecord x
Generic)
data ConHead = ConHead
{ ConHead -> QName
conName :: QName
, ConHead -> DataOrRecord
conDataRecord :: DataOrRecord
, ConHead -> Induction
conInductive :: Induction
, ConHead -> [Arg QName]
conFields :: [Arg QName]
} deriving (Typeable ConHead
ConHead -> Constr
ConHead -> DataType
(forall b. Data b => b -> b) -> ConHead -> ConHead
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ConHead -> u
forall u. (forall d. Data d => d -> u) -> ConHead -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConHead
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConHead -> c ConHead
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConHead)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConHead -> m ConHead
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ConHead -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ConHead -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ConHead -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ConHead -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConHead -> r
gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead
$cgmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConHead)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConHead)
dataTypeOf :: ConHead -> DataType
$cdataTypeOf :: ConHead -> DataType
toConstr :: ConHead -> Constr
$ctoConstr :: ConHead -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConHead
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConHead
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConHead -> c ConHead
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConHead -> c ConHead
Data, Int -> ConHead -> ShowS
[ConHead] -> ShowS
ConHead -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ConHead] -> ShowS
$cshowList :: [ConHead] -> ShowS
show :: ConHead -> ArgName
$cshow :: ConHead -> ArgName
showsPrec :: Int -> ConHead -> ShowS
$cshowsPrec :: Int -> ConHead -> ShowS
Show, forall x. Rep ConHead x -> ConHead
forall x. ConHead -> Rep ConHead x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConHead x -> ConHead
$cfrom :: forall x. ConHead -> Rep ConHead x
Generic)
instance Eq ConHead where
== :: ConHead -> ConHead -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ConHead -> QName
conName
instance Ord ConHead where
<= :: ConHead -> ConHead -> Bool
(<=) = forall a. Ord a => a -> a -> Bool
(<=) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ConHead -> QName
conName
instance Pretty ConHead where
pretty :: ConHead -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName
instance HasRange ConHead where
getRange :: ConHead -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName
instance SetRange ConHead where
setRange :: Range -> ConHead -> ConHead
setRange Range
r = forall a. LensConName a => (QName -> QName) -> a -> a
mapConName (forall a. SetRange a => Range -> a -> a
setRange Range
r)
class LensConName a where
getConName :: a -> QName
setConName :: QName -> a -> a
setConName = forall a. LensConName a => (QName -> QName) -> a -> a
mapConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
mapConName :: (QName -> QName) -> a -> a
mapConName QName -> QName
f a
a = forall a. LensConName a => QName -> a -> a
setConName (QName -> QName
f (forall a. LensConName a => a -> QName
getConName a
a)) a
a
instance LensConName ConHead where
getConName :: ConHead -> QName
getConName = ConHead -> QName
conName
setConName :: QName -> ConHead -> ConHead
setConName QName
c ConHead
con = ConHead
con { conName :: QName
conName = QName
c }
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 (Typeable Term
Term -> Constr
Term -> DataType
(forall b. Data b => b -> b) -> Term -> Term
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
forall u. (forall d. Data d => d -> u) -> Term -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapT :: (forall b. Data b => b -> b) -> Term -> Term
$cgmapT :: (forall b. Data b => b -> b) -> Term -> Term
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
dataTypeOf :: Term -> DataType
$cdataTypeOf :: Term -> DataType
toConstr :: Term -> Constr
$ctoConstr :: Term -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
Data, Int -> Term -> ShowS
[Term] -> ShowS
Term -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> ArgName
$cshow :: Term -> ArgName
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show)
type ConInfo = ConOrigin
type Elim = Elim' Term
type Elims = [Elim]
data Abs a = Abs { forall a. Abs a -> ArgName
absName :: ArgName, forall a. Abs a -> a
unAbs :: a }
| NoAbs { absName :: ArgName, unAbs :: a }
deriving (Abs a -> Constr
Abs a -> DataType
forall {a}. Data a => Typeable (Abs a)
forall a. Data a => Abs a -> Constr
forall a. Data a => Abs a -> DataType
forall a. Data a => (forall b. Data b => b -> b) -> Abs a -> Abs a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Abs a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Abs a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Abs a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Abs a -> c (Abs a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Abs a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Abs a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Abs a -> c (Abs a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Abs a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Abs a -> m (Abs a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Abs a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Abs a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Abs a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Abs a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r
gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Abs a -> Abs a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Abs a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Abs a))
dataTypeOf :: Abs a -> DataType
$cdataTypeOf :: forall a. Data a => Abs a -> DataType
toConstr :: Abs a -> Constr
$ctoConstr :: forall a. Data a => Abs a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Abs a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Abs a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Abs a -> c (Abs a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Abs a -> c (Abs a)
Data, forall a b. a -> Abs b -> Abs a
forall a b. (a -> b) -> Abs a -> Abs b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Abs b -> Abs a
$c<$ :: forall a b. a -> Abs b -> Abs a
fmap :: forall a b. (a -> b) -> Abs a -> Abs b
$cfmap :: forall a b. (a -> b) -> Abs a -> Abs b
Functor, forall a. Eq a => a -> Abs a -> Bool
forall a. Num a => Abs a -> a
forall a. Ord a => Abs a -> a
forall m. Monoid m => Abs m -> m
forall a. Abs a -> Bool
forall a. Abs a -> Int
forall a. Abs a -> [a]
forall a. (a -> a -> a) -> Abs a -> a
forall m a. Monoid m => (a -> m) -> Abs a -> m
forall b a. (b -> a -> b) -> b -> Abs a -> b
forall a b. (a -> b -> b) -> b -> Abs a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Abs a -> a
$cproduct :: forall a. Num a => Abs a -> a
sum :: forall a. Num a => Abs a -> a
$csum :: forall a. Num a => Abs a -> a
minimum :: forall a. Ord a => Abs a -> a
$cminimum :: forall a. Ord a => Abs a -> a
maximum :: forall a. Ord a => Abs a -> a
$cmaximum :: forall a. Ord a => Abs a -> a
elem :: forall a. Eq a => a -> Abs a -> Bool
$celem :: forall a. Eq a => a -> Abs a -> Bool
length :: forall a. Abs a -> Int
$clength :: forall a. Abs a -> Int
null :: forall a. Abs a -> Bool
$cnull :: forall a. Abs a -> Bool
toList :: forall a. Abs a -> [a]
$ctoList :: forall a. Abs a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Abs a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Abs a -> a
foldr1 :: forall a. (a -> a -> a) -> Abs a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Abs a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
fold :: forall m. Monoid m => Abs m -> m
$cfold :: forall m. Monoid m => Abs m -> m
Foldable, Functor Abs
Foldable Abs
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
sequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
$csequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Abs a) x -> Abs a
forall a x. Abs a -> Rep (Abs a) x
$cto :: forall a x. Rep (Abs a) x -> Abs a
$cfrom :: forall a x. Abs a -> Rep (Abs a) x
Generic)
instance Decoration Abs where
traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Abs a -> m (Abs b)
traverseF a -> m b
f (Abs ArgName
x a
a) = forall a. ArgName -> a -> Abs a
Abs ArgName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
traverseF a -> m b
f (NoAbs ArgName
x a
a) = forall a. ArgName -> a -> Abs a
NoAbs ArgName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
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 (Type'' t a -> Constr
Type'' t a -> DataType
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {t} {a}. (Data t, Data a) => Typeable (Type'' t a)
forall t a. (Data t, Data a) => Type'' t a -> Constr
forall t a. (Data t, Data a) => Type'' t a -> DataType
forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Type'' t a -> Type'' t a
forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Type'' t a -> u
forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Type'' t a -> [u]
forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Type'' t a)
forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type'' t a -> c (Type'' t a)
forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Type'' t a))
forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Type'' t a))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Type'' t a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type'' t a -> c (Type'' t a)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Type'' t a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
$cgmapMo :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
$cgmapMp :: forall t a (m :: * -> *).
(Data t, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
$cgmapM :: forall t a (m :: * -> *).
(Data t, Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Type'' t a -> m (Type'' t a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type'' t a -> u
$cgmapQi :: forall t a u.
(Data t, Data a) =>
Int -> (forall d. Data d => d -> u) -> Type'' t a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type'' t a -> [u]
$cgmapQ :: forall t a u.
(Data t, Data a) =>
(forall d. Data d => d -> u) -> Type'' t a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
$cgmapQr :: forall t a r r'.
(Data t, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
$cgmapQl :: forall t a r r'.
(Data t, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Type'' t a -> r
gmapT :: (forall b. Data b => b -> b) -> Type'' t a -> Type'' t a
$cgmapT :: forall t a.
(Data t, Data a) =>
(forall b. Data b => b -> b) -> Type'' t a -> Type'' t a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Type'' t a))
$cdataCast2 :: forall t a (t :: * -> * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Type'' t a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Type'' t a))
$cdataCast1 :: forall t a (t :: * -> *) (c :: * -> *).
(Data t, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Type'' t a))
dataTypeOf :: Type'' t a -> DataType
$cdataTypeOf :: forall t a. (Data t, Data a) => Type'' t a -> DataType
toConstr :: Type'' t a -> Constr
$ctoConstr :: forall t a. (Data t, Data a) => Type'' t a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Type'' t a)
$cgunfold :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Type'' t a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type'' t a -> c (Type'' t a)
$cgfoldl :: forall t a (c :: * -> *).
(Data t, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type'' t a -> c (Type'' t a)
Data, Int -> Type'' t a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
forall t a. (Show t, Show a) => Type'' t a -> ArgName
showList :: [Type'' t a] -> ShowS
$cshowList :: forall t a. (Show t, Show a) => [Type'' t a] -> ShowS
show :: Type'' t a -> ArgName
$cshow :: forall t a. (Show t, Show a) => Type'' t a -> ArgName
showsPrec :: Int -> Type'' t a -> ShowS
$cshowsPrec :: forall t a. (Show t, Show a) => Int -> Type'' t a -> ShowS
Show, forall a b. a -> Type'' t b -> Type'' t a
forall a b. (a -> b) -> Type'' t a -> Type'' t b
forall t a b. a -> Type'' t b -> Type'' t a
forall t a b. (a -> b) -> Type'' t a -> Type'' t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Type'' t b -> Type'' t a
$c<$ :: forall t a b. a -> Type'' t b -> Type'' t a
fmap :: forall a b. (a -> b) -> Type'' t a -> Type'' t b
$cfmap :: forall t a b. (a -> b) -> Type'' t a -> Type'' t b
Functor, forall a. Type'' t a -> Bool
forall t a. Eq a => a -> Type'' t a -> Bool
forall t a. Num a => Type'' t a -> a
forall t a. Ord a => Type'' t a -> a
forall m a. Monoid m => (a -> m) -> Type'' t a -> m
forall t m. Monoid m => Type'' t m -> m
forall t a. Type'' t a -> Bool
forall t a. Type'' t a -> Int
forall t a. Type'' t a -> [a]
forall a b. (a -> b -> b) -> b -> Type'' t a -> b
forall t a. (a -> a -> a) -> Type'' t a -> a
forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Type'' t a -> a
$cproduct :: forall t a. Num a => Type'' t a -> a
sum :: forall a. Num a => Type'' t a -> a
$csum :: forall t a. Num a => Type'' t a -> a
minimum :: forall a. Ord a => Type'' t a -> a
$cminimum :: forall t a. Ord a => Type'' t a -> a
maximum :: forall a. Ord a => Type'' t a -> a
$cmaximum :: forall t a. Ord a => Type'' t a -> a
elem :: forall a. Eq a => a -> Type'' t a -> Bool
$celem :: forall t a. Eq a => a -> Type'' t a -> Bool
length :: forall a. Type'' t a -> Int
$clength :: forall t a. Type'' t a -> Int
null :: forall a. Type'' t a -> Bool
$cnull :: forall t a. Type'' t a -> Bool
toList :: forall a. Type'' t a -> [a]
$ctoList :: forall t a. Type'' t a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Type'' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Type'' t a -> a
$cfoldr1 :: forall t a. (a -> a -> a) -> Type'' t a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Type'' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Type'' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Type'' t a -> b
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Type'' t a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Type'' t a -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Type'' t a -> m
fold :: forall m. Monoid m => Type'' t m -> m
$cfold :: forall t m. Monoid m => Type'' t m -> m
Foldable, forall t. Functor (Type'' t)
forall t. Foldable (Type'' t)
forall t (m :: * -> *) a.
Monad m =>
Type'' t (m a) -> m (Type'' t a)
forall t (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
sequence :: forall (m :: * -> *) a. Monad m => Type'' t (m a) -> m (Type'' t a)
$csequence :: forall t (m :: * -> *) a.
Monad m =>
Type'' t (m a) -> m (Type'' t a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Type'' t (f a) -> f (Type'' t a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' t a -> f (Type'' t b)
Traversable)
type Type' a = Type'' Term a
type Type = Type' Term
instance Decoration (Type'' t) where
traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Type'' t a -> m (Type'' t b)
traverseF a -> m b
f (El Sort' t
s a
a) = forall t a. Sort' t -> a -> Type'' t a
El Sort' t
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
class LensSort a where
lensSort :: Lens' Sort a
getSort :: a -> Sort
getSort a
a = a
a forall o i. o -> Lens' i o -> i
^. forall a. LensSort a => Lens' Sort a
lensSort
instance LensSort Sort where
lensSort :: Lens' Sort Sort
lensSort Sort -> f Sort
f Sort
s = Sort -> f Sort
f Sort
s forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Sort
s' -> Sort
s'
instance LensSort (Type' a) where
lensSort :: Lens' Sort (Type' a)
lensSort Sort -> f Sort
f (El Sort
s a
a) = Sort -> f Sort
f Sort
s forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Sort
s' -> forall t a. Sort' t -> a -> Type'' t a
El Sort
s' a
a
instance LensSort a => LensSort (Dom a) where
lensSort :: Lens' Sort (Dom a)
lensSort = forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => Lens' Sort a
lensSort
instance LensSort a => LensSort (Arg a) where
lensSort :: Lens' Sort (Arg a)
lensSort = forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => Lens' Sort a
lensSort
data Tele a = EmptyTel
| ExtendTel a (Abs (Tele a))
deriving (Tele a -> Constr
Tele a -> DataType
forall {a}. Data a => Typeable (Tele a)
forall a. Data a => Tele a -> Constr
forall a. Data a => Tele a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> Tele a -> Tele a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Tele a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Tele a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Tele a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tele a -> c (Tele a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Tele a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Tele a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tele a -> c (Tele a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Tele a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Tele a -> m (Tele a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Tele a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Tele a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Tele a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Tele a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r
gmapT :: (forall b. Data b => b -> b) -> Tele a -> Tele a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Tele a -> Tele a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Tele a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Tele a))
dataTypeOf :: Tele a -> DataType
$cdataTypeOf :: forall a. Data a => Tele a -> DataType
toConstr :: Tele a -> Constr
$ctoConstr :: forall a. Data a => Tele a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Tele a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Tele a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tele a -> c (Tele a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Tele a -> c (Tele a)
Data, Int -> Tele a -> ShowS
forall a. Show a => Int -> Tele a -> ShowS
forall a. Show a => [Tele a] -> ShowS
forall a. Show a => Tele a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Tele a] -> ShowS
$cshowList :: forall a. Show a => [Tele a] -> ShowS
show :: Tele a -> ArgName
$cshow :: forall a. Show a => Tele a -> ArgName
showsPrec :: Int -> Tele a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Tele a -> ShowS
Show, forall a b. a -> Tele b -> Tele a
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Tele b -> Tele a
$c<$ :: forall a b. a -> Tele b -> Tele a
fmap :: forall a b. (a -> b) -> Tele a -> Tele b
$cfmap :: forall a b. (a -> b) -> Tele a -> Tele b
Functor, forall a. Eq a => a -> Tele a -> Bool
forall a. Num a => Tele a -> a
forall a. Ord a => Tele a -> a
forall m. Monoid m => Tele m -> m
forall a. Tele a -> Bool
forall a. Tele a -> Int
forall a. Tele a -> [a]
forall a. (a -> a -> a) -> Tele a -> a
forall m a. Monoid m => (a -> m) -> Tele a -> m
forall b a. (b -> a -> b) -> b -> Tele a -> b
forall a b. (a -> b -> b) -> b -> Tele a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Tele a -> a
$cproduct :: forall a. Num a => Tele a -> a
sum :: forall a. Num a => Tele a -> a
$csum :: forall a. Num a => Tele a -> a
minimum :: forall a. Ord a => Tele a -> a
$cminimum :: forall a. Ord a => Tele a -> a
maximum :: forall a. Ord a => Tele a -> a
$cmaximum :: forall a. Ord a => Tele a -> a
elem :: forall a. Eq a => a -> Tele a -> Bool
$celem :: forall a. Eq a => a -> Tele a -> Bool
length :: forall a. Tele a -> Int
$clength :: forall a. Tele a -> Int
null :: forall a. Tele a -> Bool
$cnull :: forall a. Tele a -> Bool
toList :: forall a. Tele a -> [a]
$ctoList :: forall a. Tele a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Tele a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Tele a -> a
foldr1 :: forall a. (a -> a -> a) -> Tele a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Tele a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Tele a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Tele a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Tele a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Tele a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Tele a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Tele a -> m
fold :: forall m. Monoid m => Tele m -> m
$cfold :: forall m. Monoid m => Tele m -> m
Foldable, Functor Tele
Foldable Tele
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
sequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
$csequence :: forall (m :: * -> *) a. Monad m => Tele (m a) -> m (Tele a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tele a -> m (Tele b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Tele (f a) -> f (Tele a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Tele a -> f (Tele b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Tele a) x -> Tele a
forall a x. Tele a -> Rep (Tele a) x
$cto :: forall a x. Rep (Tele a) x -> Tele a
$cfrom :: forall a x. Tele a -> Rep (Tele a) x
Generic)
type Telescope = Tele (Dom Type)
data IsFibrant = IsFibrant | IsStrict
deriving (Typeable IsFibrant
IsFibrant -> Constr
IsFibrant -> DataType
(forall b. Data b => b -> b) -> IsFibrant -> IsFibrant
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> IsFibrant -> u
forall u. (forall d. Data d => d -> u) -> IsFibrant -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IsFibrant
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IsFibrant -> c IsFibrant
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IsFibrant)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsFibrant)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IsFibrant -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IsFibrant -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> IsFibrant -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> IsFibrant -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> IsFibrant -> r
gmapT :: (forall b. Data b => b -> b) -> IsFibrant -> IsFibrant
$cgmapT :: (forall b. Data b => b -> b) -> IsFibrant -> IsFibrant
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsFibrant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsFibrant)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IsFibrant)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IsFibrant)
dataTypeOf :: IsFibrant -> DataType
$cdataTypeOf :: IsFibrant -> DataType
toConstr :: IsFibrant -> Constr
$ctoConstr :: IsFibrant -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IsFibrant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IsFibrant
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IsFibrant -> c IsFibrant
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IsFibrant -> c IsFibrant
Data, Int -> IsFibrant -> ShowS
[IsFibrant] -> ShowS
IsFibrant -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IsFibrant] -> ShowS
$cshowList :: [IsFibrant] -> ShowS
show :: IsFibrant -> ArgName
$cshow :: IsFibrant -> ArgName
showsPrec :: Int -> IsFibrant -> ShowS
$cshowsPrec :: Int -> IsFibrant -> ShowS
Show, IsFibrant -> IsFibrant -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFibrant -> IsFibrant -> Bool
$c/= :: IsFibrant -> IsFibrant -> Bool
== :: IsFibrant -> IsFibrant -> Bool
$c== :: IsFibrant -> IsFibrant -> Bool
Eq, Eq IsFibrant
IsFibrant -> IsFibrant -> Bool
IsFibrant -> IsFibrant -> Ordering
IsFibrant -> IsFibrant -> IsFibrant
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: IsFibrant -> IsFibrant -> IsFibrant
$cmin :: IsFibrant -> IsFibrant -> IsFibrant
max :: IsFibrant -> IsFibrant -> IsFibrant
$cmax :: IsFibrant -> IsFibrant -> IsFibrant
>= :: IsFibrant -> IsFibrant -> Bool
$c>= :: IsFibrant -> IsFibrant -> Bool
> :: IsFibrant -> IsFibrant -> Bool
$c> :: IsFibrant -> IsFibrant -> Bool
<= :: IsFibrant -> IsFibrant -> Bool
$c<= :: IsFibrant -> IsFibrant -> Bool
< :: IsFibrant -> IsFibrant -> Bool
$c< :: IsFibrant -> IsFibrant -> Bool
compare :: IsFibrant -> IsFibrant -> Ordering
$ccompare :: IsFibrant -> IsFibrant -> Ordering
Ord, forall x. Rep IsFibrant x -> IsFibrant
forall x. IsFibrant -> Rep IsFibrant x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IsFibrant x -> IsFibrant
$cfrom :: forall x. IsFibrant -> Rep IsFibrant x
Generic)
data Sort' t
= Type (Level' t)
| Prop (Level' t)
| Inf IsFibrant Integer
| SSet (Level' t)
| SizeUniv
| LockUniv
| 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 (Sort' t -> Constr
Sort' t -> DataType
forall {t}. Data t => Typeable (Sort' t)
forall t. Data t => Sort' t -> Constr
forall t. Data t => Sort' t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> Sort' t -> Sort' t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Sort' t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> Sort' t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sort' t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort' t -> c (Sort' t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Sort' t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sort' t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sort' t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort' t -> c (Sort' t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Sort' t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort' t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Sort' t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Sort' t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Sort' t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sort' t -> r
gmapT :: (forall b. Data b => b -> b) -> Sort' t -> Sort' t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Sort' t -> Sort' t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sort' t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sort' t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Sort' t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Sort' t))
dataTypeOf :: Sort' t -> DataType
$cdataTypeOf :: forall t. Data t => Sort' t -> DataType
toConstr :: Sort' t -> Constr
$ctoConstr :: forall t. Data t => Sort' t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sort' t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Sort' t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort' t -> c (Sort' t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort' t -> c (Sort' t)
Data, Int -> Sort' t -> ShowS
forall t. Show t => Int -> Sort' t -> ShowS
forall t. Show t => [Sort' t] -> ShowS
forall t. Show t => Sort' t -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Sort' t] -> ShowS
$cshowList :: forall t. Show t => [Sort' t] -> ShowS
show :: Sort' t -> ArgName
$cshow :: forall t. Show t => Sort' t -> ArgName
showsPrec :: Int -> Sort' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Sort' t -> ShowS
Show)
type Sort = Sort' Term
data Level' t = Max Integer [PlusLevel' t]
deriving (Int -> Level' t -> ShowS
forall t. Show t => Int -> Level' t -> ShowS
forall t. Show t => [Level' t] -> ShowS
forall t. Show t => Level' t -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Level' t] -> ShowS
$cshowList :: forall t. Show t => [Level' t] -> ShowS
show :: Level' t -> ArgName
$cshow :: forall t. Show t => Level' t -> ArgName
showsPrec :: Int -> Level' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Level' t -> ShowS
Show, Level' t -> Constr
Level' t -> DataType
forall {t}. Data t => Typeable (Level' t)
forall t. Data t => Level' t -> Constr
forall t. Data t => Level' t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> Level' t -> Level' t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Level' t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> Level' t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Level' t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Level' t -> c (Level' t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Level' t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Level' t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Level' t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Level' t -> c (Level' t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Level' t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Level' t -> m (Level' t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Level' t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Level' t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Level' t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Level' t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Level' t -> r
gmapT :: (forall b. Data b => b -> b) -> Level' t -> Level' t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Level' t -> Level' t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Level' t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Level' t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Level' t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Level' t))
dataTypeOf :: Level' t -> DataType
$cdataTypeOf :: forall t. Data t => Level' t -> DataType
toConstr :: Level' t -> Constr
$ctoConstr :: forall t. Data t => Level' t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Level' t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Level' t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Level' t -> c (Level' t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Level' t -> c (Level' t)
Data, forall a b. a -> Level' b -> Level' a
forall a b. (a -> b) -> Level' a -> Level' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Level' b -> Level' a
$c<$ :: forall a b. a -> Level' b -> Level' a
fmap :: forall a b. (a -> b) -> Level' a -> Level' b
$cfmap :: forall a b. (a -> b) -> Level' a -> Level' b
Functor, forall a. Eq a => a -> Level' a -> Bool
forall a. Num a => Level' a -> a
forall a. Ord a => Level' a -> a
forall m. Monoid m => Level' m -> m
forall a. Level' a -> Bool
forall a. Level' a -> Int
forall a. Level' a -> [a]
forall a. (a -> a -> a) -> Level' a -> a
forall m a. Monoid m => (a -> m) -> Level' a -> m
forall b a. (b -> a -> b) -> b -> Level' a -> b
forall a b. (a -> b -> b) -> b -> Level' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Level' a -> a
$cproduct :: forall a. Num a => Level' a -> a
sum :: forall a. Num a => Level' a -> a
$csum :: forall a. Num a => Level' a -> a
minimum :: forall a. Ord a => Level' a -> a
$cminimum :: forall a. Ord a => Level' a -> a
maximum :: forall a. Ord a => Level' a -> a
$cmaximum :: forall a. Ord a => Level' a -> a
elem :: forall a. Eq a => a -> Level' a -> Bool
$celem :: forall a. Eq a => a -> Level' a -> Bool
length :: forall a. Level' a -> Int
$clength :: forall a. Level' a -> Int
null :: forall a. Level' a -> Bool
$cnull :: forall a. Level' a -> Bool
toList :: forall a. Level' a -> [a]
$ctoList :: forall a. Level' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Level' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Level' a -> a
foldr1 :: forall a. (a -> a -> a) -> Level' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Level' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Level' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Level' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Level' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Level' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Level' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Level' a -> m
fold :: forall m. Monoid m => Level' m -> m
$cfold :: forall m. Monoid m => Level' m -> m
Foldable, Functor Level'
Foldable Level'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
sequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
$csequence :: forall (m :: * -> *) a. Monad m => Level' (m a) -> m (Level' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Level' a -> m (Level' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Level' (f a) -> f (Level' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Level' a -> f (Level' b)
Traversable)
type Level = Level' Term
data PlusLevel' t = Plus Integer t
deriving (Int -> PlusLevel' t -> ShowS
forall t. Show t => Int -> PlusLevel' t -> ShowS
forall t. Show t => [PlusLevel' t] -> ShowS
forall t. Show t => PlusLevel' t -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PlusLevel' t] -> ShowS
$cshowList :: forall t. Show t => [PlusLevel' t] -> ShowS
show :: PlusLevel' t -> ArgName
$cshow :: forall t. Show t => PlusLevel' t -> ArgName
showsPrec :: Int -> PlusLevel' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> PlusLevel' t -> ShowS
Show, PlusLevel' t -> Constr
PlusLevel' t -> DataType
forall {t}. Data t => Typeable (PlusLevel' t)
forall t. Data t => PlusLevel' t -> Constr
forall t. Data t => PlusLevel' t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> PlusLevel' t -> PlusLevel' t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> PlusLevel' t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> PlusLevel' t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PlusLevel' t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlusLevel' t -> c (PlusLevel' t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PlusLevel' t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PlusLevel' t))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PlusLevel' t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlusLevel' t -> c (PlusLevel' t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PlusLevel' t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> PlusLevel' t -> m (PlusLevel' t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PlusLevel' t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> PlusLevel' t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PlusLevel' t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> PlusLevel' t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PlusLevel' t -> r
gmapT :: (forall b. Data b => b -> b) -> PlusLevel' t -> PlusLevel' t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> PlusLevel' t -> PlusLevel' t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PlusLevel' t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PlusLevel' t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PlusLevel' t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PlusLevel' t))
dataTypeOf :: PlusLevel' t -> DataType
$cdataTypeOf :: forall t. Data t => PlusLevel' t -> DataType
toConstr :: PlusLevel' t -> Constr
$ctoConstr :: forall t. Data t => PlusLevel' t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PlusLevel' t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PlusLevel' t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlusLevel' t -> c (PlusLevel' t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PlusLevel' t -> c (PlusLevel' t)
Data, forall a b. a -> PlusLevel' b -> PlusLevel' a
forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> PlusLevel' b -> PlusLevel' a
$c<$ :: forall a b. a -> PlusLevel' b -> PlusLevel' a
fmap :: forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' b
$cfmap :: forall a b. (a -> b) -> PlusLevel' a -> PlusLevel' b
Functor, forall a. Eq a => a -> PlusLevel' a -> Bool
forall a. Num a => PlusLevel' a -> a
forall a. Ord a => PlusLevel' a -> a
forall m. Monoid m => PlusLevel' m -> m
forall a. PlusLevel' a -> Bool
forall a. PlusLevel' a -> Int
forall a. PlusLevel' a -> [a]
forall a. (a -> a -> a) -> PlusLevel' a -> a
forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => PlusLevel' a -> a
$cproduct :: forall a. Num a => PlusLevel' a -> a
sum :: forall a. Num a => PlusLevel' a -> a
$csum :: forall a. Num a => PlusLevel' a -> a
minimum :: forall a. Ord a => PlusLevel' a -> a
$cminimum :: forall a. Ord a => PlusLevel' a -> a
maximum :: forall a. Ord a => PlusLevel' a -> a
$cmaximum :: forall a. Ord a => PlusLevel' a -> a
elem :: forall a. Eq a => a -> PlusLevel' a -> Bool
$celem :: forall a. Eq a => a -> PlusLevel' a -> Bool
length :: forall a. PlusLevel' a -> Int
$clength :: forall a. PlusLevel' a -> Int
null :: forall a. PlusLevel' a -> Bool
$cnull :: forall a. PlusLevel' a -> Bool
toList :: forall a. PlusLevel' a -> [a]
$ctoList :: forall a. PlusLevel' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
foldr1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> PlusLevel' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> PlusLevel' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> PlusLevel' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> PlusLevel' a -> m
fold :: forall m. Monoid m => PlusLevel' m -> m
$cfold :: forall m. Monoid m => PlusLevel' m -> m
Foldable, Functor PlusLevel'
Foldable PlusLevel'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
PlusLevel' (m a) -> m (PlusLevel' a)
forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
sequence :: forall (m :: * -> *) a.
Monad m =>
PlusLevel' (m a) -> m (PlusLevel' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
PlusLevel' (m a) -> m (PlusLevel' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PlusLevel' a -> m (PlusLevel' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
PlusLevel' (f a) -> f (PlusLevel' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PlusLevel' a -> f (PlusLevel' b)
Traversable)
type PlusLevel = PlusLevel' Term
type LevelAtom = Term
newtype BraveTerm = BraveTerm { BraveTerm -> Term
unBrave :: Term } deriving (Typeable BraveTerm
BraveTerm -> Constr
BraveTerm -> DataType
(forall b. Data b => b -> b) -> BraveTerm -> BraveTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BraveTerm -> u
forall u. (forall d. Data d => d -> u) -> BraveTerm -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BraveTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BraveTerm -> c BraveTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BraveTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BraveTerm)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BraveTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BraveTerm -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BraveTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BraveTerm -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BraveTerm -> r
gmapT :: (forall b. Data b => b -> b) -> BraveTerm -> BraveTerm
$cgmapT :: (forall b. Data b => b -> b) -> BraveTerm -> BraveTerm
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BraveTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BraveTerm)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BraveTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BraveTerm)
dataTypeOf :: BraveTerm -> DataType
$cdataTypeOf :: BraveTerm -> DataType
toConstr :: BraveTerm -> Constr
$ctoConstr :: BraveTerm -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BraveTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BraveTerm
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BraveTerm -> c BraveTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BraveTerm -> c BraveTerm
Data, Int -> BraveTerm -> ShowS
[BraveTerm] -> ShowS
BraveTerm -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [BraveTerm] -> ShowS
$cshowList :: [BraveTerm] -> ShowS
show :: BraveTerm -> ArgName
$cshow :: BraveTerm -> ArgName
showsPrec :: Int -> BraveTerm -> ShowS
$cshowsPrec :: Int -> BraveTerm -> ShowS
Show)
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
}
deriving (Typeable Clause
Clause -> Constr
Clause -> DataType
(forall b. Data b => b -> b) -> Clause -> Clause
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
forall u. (forall d. Data d => d -> u) -> Clause -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
$cgmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
dataTypeOf :: Clause -> DataType
$cdataTypeOf :: Clause -> DataType
toConstr :: Clause -> Constr
$ctoConstr :: Clause -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
Data, Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> ArgName
$cshow :: Clause -> ArgName
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Clause x -> Clause
$cfrom :: forall x. Clause -> Rep Clause x
Generic)
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats
instance HasRange Clause where
getRange :: Clause -> Range
getRange = Clause -> Range
clauseLHSRange
type PatVarName = ArgName
patVarNameToString :: PatVarName -> String
patVarNameToString :: ShowS
patVarNameToString = ShowS
argNameToString
nameToPatVarName :: Name -> PatVarName
nameToPatVarName :: Name -> ArgName
nameToPatVarName = Name -> ArgName
nameToArgName
data PatternInfo = PatternInfo
{ PatternInfo -> PatOrigin
patOrigin :: PatOrigin
, PatternInfo -> [Name]
patAsNames :: [Name]
} deriving (Typeable PatternInfo
PatternInfo -> Constr
PatternInfo -> DataType
(forall b. Data b => b -> b) -> PatternInfo -> PatternInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PatternInfo -> u
forall u. (forall d. Data d => d -> u) -> PatternInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatternInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatternInfo -> c PatternInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatternInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PatternInfo)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PatternInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PatternInfo -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PatternInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PatternInfo -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatternInfo -> r
gmapT :: (forall b. Data b => b -> b) -> PatternInfo -> PatternInfo
$cgmapT :: (forall b. Data b => b -> b) -> PatternInfo -> PatternInfo
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PatternInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PatternInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatternInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatternInfo)
dataTypeOf :: PatternInfo -> DataType
$cdataTypeOf :: PatternInfo -> DataType
toConstr :: PatternInfo -> Constr
$ctoConstr :: PatternInfo -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatternInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatternInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatternInfo -> c PatternInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatternInfo -> c PatternInfo
Data, Int -> PatternInfo -> ShowS
[PatternInfo] -> ShowS
PatternInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PatternInfo] -> ShowS
$cshowList :: [PatternInfo] -> ShowS
show :: PatternInfo -> ArgName
$cshow :: PatternInfo -> ArgName
showsPrec :: Int -> PatternInfo -> ShowS
$cshowsPrec :: Int -> PatternInfo -> ShowS
Show, PatternInfo -> PatternInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatternInfo -> PatternInfo -> Bool
$c/= :: PatternInfo -> PatternInfo -> Bool
== :: PatternInfo -> PatternInfo -> Bool
$c== :: PatternInfo -> PatternInfo -> Bool
Eq, forall x. Rep PatternInfo x -> PatternInfo
forall x. PatternInfo -> Rep PatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatternInfo x -> PatternInfo
$cfrom :: forall x. PatternInfo -> Rep PatternInfo x
Generic)
defaultPatternInfo :: PatternInfo
defaultPatternInfo :: PatternInfo
defaultPatternInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSystem []
data PatOrigin
= PatOSystem
| PatOSplit
| PatOVar Name
| PatODot
| PatOWild
| PatOCon
| PatORec
| PatOLit
| PatOAbsurd
deriving (Typeable PatOrigin
PatOrigin -> Constr
PatOrigin -> DataType
(forall b. Data b => b -> b) -> PatOrigin -> PatOrigin
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PatOrigin -> u
forall u. (forall d. Data d => d -> u) -> PatOrigin -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatOrigin
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatOrigin -> c PatOrigin
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatOrigin)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PatOrigin -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PatOrigin -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PatOrigin -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PatOrigin -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PatOrigin -> r
gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin
$cgmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatOrigin)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatOrigin)
dataTypeOf :: PatOrigin -> DataType
$cdataTypeOf :: PatOrigin -> DataType
toConstr :: PatOrigin -> Constr
$ctoConstr :: PatOrigin -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatOrigin
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatOrigin
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatOrigin -> c PatOrigin
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatOrigin -> c PatOrigin
Data, Int -> PatOrigin -> ShowS
[PatOrigin] -> ShowS
PatOrigin -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PatOrigin] -> ShowS
$cshowList :: [PatOrigin] -> ShowS
show :: PatOrigin -> ArgName
$cshow :: PatOrigin -> ArgName
showsPrec :: Int -> PatOrigin -> ShowS
$cshowsPrec :: Int -> PatOrigin -> ShowS
Show, PatOrigin -> PatOrigin -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatOrigin -> PatOrigin -> Bool
$c/= :: PatOrigin -> PatOrigin -> Bool
== :: PatOrigin -> PatOrigin -> Bool
$c== :: PatOrigin -> PatOrigin -> Bool
Eq, forall x. Rep PatOrigin x -> PatOrigin
forall x. PatOrigin -> Rep PatOrigin x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatOrigin x -> PatOrigin
$cfrom :: forall x. PatOrigin -> Rep PatOrigin x
Generic)
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 (Pattern' x -> Constr
Pattern' x -> DataType
forall {x}. Data x => Typeable (Pattern' x)
forall x. Data x => Pattern' x -> Constr
forall x. Data x => Pattern' x -> DataType
forall x.
Data x =>
(forall b. Data b => b -> b) -> Pattern' x -> Pattern' x
forall x u.
Data x =>
Int -> (forall d. Data d => d -> u) -> Pattern' x -> u
forall x u.
Data x =>
(forall d. Data d => d -> u) -> Pattern' x -> [u]
forall x r r'.
Data x =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
forall x r r'.
Data x =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
forall x (m :: * -> *).
(Data x, Monad m) =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
forall x (c :: * -> *).
Data x =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pattern' x)
forall x (c :: * -> *).
Data x =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x)
forall x (t :: * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Pattern' x))
forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pattern' x))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pattern' x)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Pattern' x))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
$cgmapMo :: forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
$cgmapMp :: forall x (m :: * -> *).
(Data x, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
$cgmapM :: forall x (m :: * -> *).
(Data x, Monad m) =>
(forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pattern' x -> u
$cgmapQi :: forall x u.
Data x =>
Int -> (forall d. Data d => d -> u) -> Pattern' x -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Pattern' x -> [u]
$cgmapQ :: forall x u.
Data x =>
(forall d. Data d => d -> u) -> Pattern' x -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
$cgmapQr :: forall x r r'.
Data x =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
$cgmapQl :: forall x r r'.
Data x =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Pattern' x -> r
gmapT :: (forall b. Data b => b -> b) -> Pattern' x -> Pattern' x
$cgmapT :: forall x.
Data x =>
(forall b. Data b => b -> b) -> Pattern' x -> Pattern' x
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pattern' x))
$cdataCast2 :: forall x (t :: * -> * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Pattern' x))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Pattern' x))
$cdataCast1 :: forall x (t :: * -> *) (c :: * -> *).
(Data x, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Pattern' x))
dataTypeOf :: Pattern' x -> DataType
$cdataTypeOf :: forall x. Data x => Pattern' x -> DataType
toConstr :: Pattern' x -> Constr
$ctoConstr :: forall x. Data x => Pattern' x -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pattern' x)
$cgunfold :: forall x (c :: * -> *).
Data x =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Pattern' x)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x)
$cgfoldl :: forall x (c :: * -> *).
Data x =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x)
Data, Int -> Pattern' x -> ShowS
forall x. Show x => Int -> Pattern' x -> ShowS
forall x. Show x => [Pattern' x] -> ShowS
forall x. Show x => Pattern' x -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pattern' x] -> ShowS
$cshowList :: forall x. Show x => [Pattern' x] -> ShowS
show :: Pattern' x -> ArgName
$cshow :: forall x. Show x => Pattern' x -> ArgName
showsPrec :: Int -> Pattern' x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> Pattern' x -> ShowS
Show, forall a b. a -> Pattern' b -> Pattern' a
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pattern' b -> Pattern' a
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
Functor, forall a. Eq a => a -> Pattern' a -> Bool
forall a. Num a => Pattern' a -> a
forall a. Ord a => Pattern' a -> a
forall m. Monoid m => Pattern' m -> m
forall a. Pattern' a -> Bool
forall a. Pattern' a -> Int
forall a. Pattern' a -> [a]
forall a. (a -> a -> a) -> Pattern' a -> a
forall m a. Monoid m => (a -> m) -> Pattern' a -> m
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall a b. (a -> b -> b) -> b -> Pattern' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cmaximum :: forall a. Ord a => Pattern' a -> a
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
length :: forall a. Pattern' a -> Int
$clength :: forall a. Pattern' a -> Int
null :: forall a. Pattern' a -> Bool
$cnull :: forall a. Pattern' a -> Bool
toList :: forall a. Pattern' a -> [a]
$ctoList :: forall a. Pattern' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
fold :: forall m. Monoid m => Pattern' m -> m
$cfold :: forall m. Monoid m => Pattern' m -> m
Foldable, Functor Pattern'
Foldable Pattern'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall x x. Rep (Pattern' x) x -> Pattern' x
forall x x. Pattern' x -> Rep (Pattern' x) x
$cto :: forall x x. Rep (Pattern' x) x -> Pattern' x
$cfrom :: forall x x. Pattern' x -> Rep (Pattern' x) x
Generic)
type Pattern = Pattern' PatVarName
varP :: a -> Pattern' a
varP :: forall a. a -> Pattern' a
varP = forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo
dotP :: Term -> Pattern' a
dotP :: forall a. Term -> Pattern' a
dotP = forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo
litP :: Literal -> Pattern' a
litP :: forall a. Literal -> Pattern' a
litP = forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
defaultPatternInfo
data DBPatVar = DBPatVar
{ DBPatVar -> ArgName
dbPatVarName :: PatVarName
, DBPatVar -> Int
dbPatVarIndex :: Int
} deriving (Typeable DBPatVar
DBPatVar -> Constr
DBPatVar -> DataType
(forall b. Data b => b -> b) -> DBPatVar -> DBPatVar
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DBPatVar -> u
forall u. (forall d. Data d => d -> u) -> DBPatVar -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBPatVar
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBPatVar -> c DBPatVar
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBPatVar)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBPatVar -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBPatVar -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DBPatVar -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DBPatVar -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DBPatVar -> r
gmapT :: (forall b. Data b => b -> b) -> DBPatVar -> DBPatVar
$cgmapT :: (forall b. Data b => b -> b) -> DBPatVar -> DBPatVar
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBPatVar)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBPatVar)
dataTypeOf :: DBPatVar -> DataType
$cdataTypeOf :: DBPatVar -> DataType
toConstr :: DBPatVar -> Constr
$ctoConstr :: DBPatVar -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBPatVar
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBPatVar
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBPatVar -> c DBPatVar
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBPatVar -> c DBPatVar
Data, Int -> DBPatVar -> ShowS
[DBPatVar] -> ShowS
DBPatVar -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DBPatVar] -> ShowS
$cshowList :: [DBPatVar] -> ShowS
show :: DBPatVar -> ArgName
$cshow :: DBPatVar -> ArgName
showsPrec :: Int -> DBPatVar -> ShowS
$cshowsPrec :: Int -> DBPatVar -> ShowS
Show, DBPatVar -> DBPatVar -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DBPatVar -> DBPatVar -> Bool
$c/= :: DBPatVar -> DBPatVar -> Bool
== :: DBPatVar -> DBPatVar -> Bool
$c== :: DBPatVar -> DBPatVar -> Bool
Eq, forall x. Rep DBPatVar x -> DBPatVar
forall x. DBPatVar -> Rep DBPatVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DBPatVar x -> DBPatVar
$cfrom :: forall x. DBPatVar -> Rep DBPatVar x
Generic)
type DeBruijnPattern = Pattern' DBPatVar
namedVarP :: PatVarName -> Named_ Pattern
namedVarP :: ArgName -> Named_ Pattern
namedVarP ArgName
x = forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
named forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP ArgName
x
where named :: Maybe (WithOrigin (Ranged ArgName))
named = if forall a. Underscore a => a -> Bool
isUnderscore ArgName
x then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged ArgName
x
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP :: Int -> ArgName -> Named_ DeBruijnPattern
namedDBVarP Int
m = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\ArgName
x -> ArgName -> Int -> DBPatVar
DBPatVar ArgName
x Int
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Named_ Pattern
namedVarP
absurdP :: Int -> DeBruijnPattern
absurdP :: Int -> DeBruijnPattern
absurdP = forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Int -> DBPatVar
DBPatVar ArgName
absurdPatternName
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 (Typeable ConPatternInfo
ConPatternInfo -> Constr
ConPatternInfo -> DataType
(forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u
forall u. (forall d. Data d => d -> u) -> ConPatternInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConPatternInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ConPatternInfo)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ConPatternInfo -> m ConPatternInfo
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ConPatternInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ConPatternInfo -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r
gmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo
$cgmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ConPatternInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ConPatternInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo)
dataTypeOf :: ConPatternInfo -> DataType
$cdataTypeOf :: ConPatternInfo -> DataType
toConstr :: ConPatternInfo -> Constr
$ctoConstr :: ConPatternInfo -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConPatternInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConPatternInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo
Data, Int -> ConPatternInfo -> ShowS
[ConPatternInfo] -> ShowS
ConPatternInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ConPatternInfo] -> ShowS
$cshowList :: [ConPatternInfo] -> ShowS
show :: ConPatternInfo -> ArgName
$cshow :: ConPatternInfo -> ArgName
showsPrec :: Int -> ConPatternInfo -> ShowS
$cshowsPrec :: Int -> ConPatternInfo -> ShowS
Show, forall x. Rep ConPatternInfo x -> ConPatternInfo
forall x. ConPatternInfo -> Rep ConPatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConPatternInfo x -> ConPatternInfo
$cfrom :: forall x. ConPatternInfo -> Rep ConPatternInfo x
Generic)
noConPatternInfo :: ConPatternInfo
noConPatternInfo :: ConPatternInfo
noConPatternInfo = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False forall a. Maybe a
Nothing Bool
False
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ConORec = ConPatternInfo
noConPatternInfo{ conPInfo :: PatternInfo
conPInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatORec [] , conPRecord :: Bool
conPRecord = Bool
True }
toConPatternInfo ConInfo
_ = ConPatternInfo
noConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
i = PatOrigin -> ConInfo
patToConO forall a b. (a -> b) -> a -> b
$ PatternInfo -> PatOrigin
patOrigin forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i
where
patToConO :: PatOrigin -> ConOrigin
patToConO :: PatOrigin -> ConInfo
patToConO = \case
PatOrigin
PatOSystem -> ConInfo
ConOSystem
PatOrigin
PatOSplit -> ConInfo
ConOSplit
PatOVar{} -> ConInfo
ConOSystem
PatOrigin
PatODot -> ConInfo
ConOSystem
PatOrigin
PatOWild -> ConInfo
ConOSystem
PatOrigin
PatOCon -> ConInfo
ConOCon
PatOrigin
PatORec -> ConInfo
ConORec
PatOrigin
PatOLit -> ConInfo
ConOCon
PatOrigin
PatOAbsurd -> ConInfo
ConOSystem
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) ) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
x]
patternVars (Arg ArgInfo
i (DotP PatternInfo
_ Term
t) ) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Term
t]
patternVars (Arg ArgInfo
_ (ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps)) = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
patternVars (Arg ArgInfo
_ (DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps)) = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
patternVars (Arg ArgInfo
_ (LitP PatternInfo
_ Literal
_) ) = []
patternVars (Arg ArgInfo
_ ProjP{} ) = []
patternVars (Arg ArgInfo
i (IApplyP PatternInfo
_ Term
_ Term
_ a
x)) = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
x]
instance PatternVars (NamedArg (Pattern' a)) where
type PatternVarOut (NamedArg (Pattern' a)) = a
patternVars :: NamedArg (Pattern' a)
-> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)]
patternVars = forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing
instance PatternVars a => PatternVars [a] where
type PatternVarOut [a] = PatternVarOut a
patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)]
patternVars = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars
patternInfo :: Pattern' x -> Maybe PatternInfo
patternInfo :: forall x. Pattern' x -> Maybe PatternInfo
patternInfo (VarP PatternInfo
i x
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DotP PatternInfo
i Term
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (LitP PatternInfo
i Literal
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' x)]
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
ci
patternInfo ProjP{} = forall a. Maybe a
Nothing
patternInfo (IApplyP PatternInfo
i Term
_ Term
_ x
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DefP PatternInfo
i QName
_ [NamedArg (Pattern' x)]
_) = forall a. a -> Maybe a
Just PatternInfo
i
patternOrigin :: Pattern' x -> Maybe PatOrigin
patternOrigin :: forall x. Pattern' x -> Maybe PatOrigin
patternOrigin = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PatternInfo -> PatOrigin
patOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Pattern' x -> Maybe PatternInfo
patternInfo
properlyMatching :: Pattern' a -> Bool
properlyMatching :: forall a. Pattern' a -> Bool
properlyMatching = forall a. Bool -> Bool -> Pattern' a -> Bool
properlyMatching' Bool
True Bool
True
properlyMatching'
:: Bool
-> 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
&& forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd -> Bool
True
ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' a)]
ps
| ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any (forall a. Pattern' a -> Bool
properlyMatching forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps
| Bool
otherwise -> Bool
True
LitP{} -> Bool
True
DefP{} -> Bool
True
ProjP{} -> Bool
projP
VarP{} -> Bool
False
DotP{} -> Bool
False
IApplyP{} -> Bool
False
instance IsProjP (Pattern' a) where
isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP = \case
ProjP ProjOrigin
o QName
d -> forall a. a -> Maybe a
Just (ProjOrigin
o, QName -> AmbiguousQName
unambiguous QName
d)
Pattern' a
_ -> forall a. Maybe a
Nothing
data Substitution' a
= IdS
| EmptyS Impossible
| a :# Substitution' a
| Strengthen Impossible (Substitution' a)
| Wk !Int (Substitution' a)
| Lift !Int (Substitution' a)
deriving ( Int -> Substitution' a -> ShowS
forall a. Show a => Int -> Substitution' a -> ShowS
forall a. Show a => [Substitution' a] -> ShowS
forall a. Show a => Substitution' a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Substitution' a] -> ShowS
$cshowList :: forall a. Show a => [Substitution' a] -> ShowS
show :: Substitution' a -> ArgName
$cshow :: forall a. Show a => Substitution' a -> ArgName
showsPrec :: Int -> Substitution' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Substitution' a -> ShowS
Show
, forall a b. a -> Substitution' b -> Substitution' a
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Substitution' b -> Substitution' a
$c<$ :: forall a b. a -> Substitution' b -> Substitution' a
fmap :: forall a b. (a -> b) -> Substitution' a -> Substitution' b
$cfmap :: forall a b. (a -> b) -> Substitution' a -> Substitution' b
Functor
, forall a. Eq a => a -> Substitution' a -> Bool
forall a. Num a => Substitution' a -> a
forall a. Ord a => Substitution' a -> a
forall m. Monoid m => Substitution' m -> m
forall a. Substitution' a -> Bool
forall a. Substitution' a -> Int
forall a. Substitution' a -> [a]
forall a. (a -> a -> a) -> Substitution' a -> a
forall m a. Monoid m => (a -> m) -> Substitution' a -> m
forall b a. (b -> a -> b) -> b -> Substitution' a -> b
forall a b. (a -> b -> b) -> b -> Substitution' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Substitution' a -> a
$cproduct :: forall a. Num a => Substitution' a -> a
sum :: forall a. Num a => Substitution' a -> a
$csum :: forall a. Num a => Substitution' a -> a
minimum :: forall a. Ord a => Substitution' a -> a
$cminimum :: forall a. Ord a => Substitution' a -> a
maximum :: forall a. Ord a => Substitution' a -> a
$cmaximum :: forall a. Ord a => Substitution' a -> a
elem :: forall a. Eq a => a -> Substitution' a -> Bool
$celem :: forall a. Eq a => a -> Substitution' a -> Bool
length :: forall a. Substitution' a -> Int
$clength :: forall a. Substitution' a -> Int
null :: forall a. Substitution' a -> Bool
$cnull :: forall a. Substitution' a -> Bool
toList :: forall a. Substitution' a -> [a]
$ctoList :: forall a. Substitution' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Substitution' a -> a
foldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Substitution' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Substitution' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Substitution' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Substitution' a -> m
fold :: forall m. Monoid m => Substitution' m -> m
$cfold :: forall m. Monoid m => Substitution' m -> m
Foldable
, Functor Substitution'
Foldable Substitution'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Substitution' (m a) -> m (Substitution' a)
forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Substitution' (m a) -> m (Substitution' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Substitution' (m a) -> m (Substitution' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Substitution' a -> m (Substitution' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Substitution' (f a) -> f (Substitution' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Substitution' a -> f (Substitution' b)
Traversable
, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Substitution' a) x -> Substitution' a
forall a x. Substitution' a -> Rep (Substitution' a) x
$cto :: forall a x. Rep (Substitution' a) x -> Substitution' a
$cfrom :: forall a x. Substitution' a -> Rep (Substitution' a) x
Generic
)
type Substitution = Substitution' Term
type PatternSubstitution = Substitution' DeBruijnPattern
infixr 4 :#
instance Null (Substitution' a) where
empty :: Substitution' a
empty = forall a. Substitution' a
IdS
null :: Substitution' a -> Bool
null Substitution' a
IdS = Bool
True
null Substitution' a
_ = Bool
False
data EqualityView
= EqualityType
{ EqualityView -> Sort
eqtSort :: Sort
, EqualityView -> QName
eqtName :: QName
, EqualityView -> [Arg Term]
eqtParams :: [Arg Term]
, EqualityView -> Arg Term
eqtType :: Arg Term
, EqualityView -> Arg Term
eqtLhs :: Arg Term
, EqualityView -> Arg Term
eqtRhs :: Arg Term
}
| OtherType Type
| IdiomType Type
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 -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IntervalView] -> ShowS
$cshowList :: [IntervalView] -> ShowS
show :: IntervalView -> ArgName
$cshow :: IntervalView -> ArgName
showsPrec :: Int -> IntervalView -> ShowS
$cshowsPrec :: Int -> IntervalView -> ShowS
Show
isIOne :: IntervalView -> Bool
isIOne :: IntervalView -> Bool
isIOne IntervalView
IOne = Bool
True
isIOne IntervalView
_ = Bool
False
absurdBody :: Abs Term
absurdBody :: Abs Term
absurdBody = forall a. ArgName -> a -> Abs a
Abs ArgName
absurdPatternName forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 []
isAbsurdBody :: Abs Term -> Bool
isAbsurdBody :: Abs Term -> Bool
isAbsurdBody (Abs ArgName
x (Var Int
0 [])) = ArgName -> Bool
isAbsurdPatternName ArgName
x
isAbsurdBody Abs Term
_ = Bool
False
absurdPatternName :: PatVarName
absurdPatternName :: ArgName
absurdPatternName = ArgName
"()"
isAbsurdPatternName :: PatVarName -> Bool
isAbsurdPatternName :: ArgName -> Bool
isAbsurdPatternName ArgName
x = ArgName
x forall a. Eq a => a -> a -> Bool
== ArgName
absurdPatternName
var :: Nat -> Term
var :: Int -> Term
var Int
i | Int
i forall a. Ord a => a -> a -> Bool
>= Int
0 = Int -> Elims -> Term
Var Int
i []
| Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
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 -> ArgName
dummyLocName CallStack
cs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ CallSite -> ArgName
prettyCallSite (CallStack -> Maybe CallSite
headCallSite CallStack
cs)
dummyTermWith :: DummyTermKind -> CallStack -> Term
dummyTermWith :: ArgName -> CallStack -> Term
dummyTermWith ArgName
kind CallStack
cs = forall a b c. (a -> b -> c) -> b -> a -> c
flip ArgName -> Elims -> Term
Dummy [] forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ArgName
kind, ArgName
": ", CallStack -> ArgName
dummyLocName CallStack
cs]
dummyLevel :: CallStack -> Level
dummyLevel :: CallStack -> Level
dummyLevel = forall t. t -> Level' t
atomicLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> CallStack -> Term
dummyTermWith ArgName
"dummyLevel"
dummyTerm :: CallStack -> Term
dummyTerm :: CallStack -> Term
dummyTerm = ArgName -> CallStack -> Term
dummyTermWith ArgName
"dummyTerm"
__DUMMY_TERM__ :: HasCallStack => Term
__DUMMY_TERM__ :: HasCallStack => Term
__DUMMY_TERM__ = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Term
dummyTerm
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Level
dummyLevel
dummySort :: CallStack -> Sort
dummySort :: CallStack -> Sort
dummySort = forall t. ArgName -> Sort' t
DummyS forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> ArgName
dummyLocName
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Sort
dummySort
dummyType :: CallStack -> Type
dummyType :: CallStack -> Type
dummyType CallStack
cs = forall t a. Sort' t -> a -> Type'' t a
El (CallStack -> Sort
dummySort CallStack
cs) forall a b. (a -> b) -> a -> b
$ ArgName -> CallStack -> Term
dummyTermWith ArgName
"dummyType" CallStack
cs
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Type
dummyType
dummyDom :: CallStack -> Dom Type
dummyDom :: CallStack -> Dom' Term Type
dummyDom = forall a. a -> Dom a
defaultDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Type
dummyType
__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ :: HasCallStack => Dom' Term Type
__DUMMY_DOM__ = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Dom' Term Type
dummyDom
pattern ClosedLevel :: Integer -> Level
pattern $bClosedLevel :: Integer -> Level
$mClosedLevel :: forall {r}. Level -> (Integer -> r) -> ((# #) -> r) -> r
ClosedLevel n = Max n []
atomicLevel :: t -> Level' t
atomicLevel :: forall t. t -> Level' t
atomicLevel t
a = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [ forall t. Integer -> t -> PlusLevel' t
Plus Integer
0 t
a ]
varSort :: Int -> Sort
varSort :: Int -> Sort
varSort Int
n = forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ forall t. t -> Level' t
atomicLevel forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
n
tmSort :: Term -> Sort
tmSort :: Term -> Sort
tmSort Term
t = forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ forall t. t -> Level' t
atomicLevel Term
t
tmSSort :: Term -> Sort
tmSSort :: Term -> Sort
tmSSort Term
t = forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ forall t. t -> Level' t
atomicLevel Term
t
levelPlus :: Integer -> Level -> Level
levelPlus :: Integer -> Level -> Level
levelPlus Integer
m (Max Integer
n [PlusLevel]
as) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
m forall a. Num a => a -> a -> a
+ Integer
n) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map PlusLevel -> PlusLevel
pplus [PlusLevel]
as
where pplus :: PlusLevel -> PlusLevel
pplus (Plus Integer
n Term
l) = forall t. Integer -> t -> PlusLevel' t
Plus (Integer
m forall a. Num a => a -> a -> a
+ Integer
n) Term
l
levelSuc :: Level -> Level
levelSuc :: Level -> Level
levelSuc = Integer -> Level -> Level
levelPlus Integer
1
mkType :: Integer -> Sort
mkType :: Integer -> Sort
mkType Integer
n = forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
mkProp :: Integer -> Sort
mkProp :: Integer -> Sort
mkProp Integer
n = forall t. Level' t -> Sort' t
Prop forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
mkSSet :: Integer -> Sort
mkSSet :: Integer -> Sort
mkSSet Integer
n = forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n
isSort :: Term -> Maybe Sort
isSort :: Term -> Maybe Sort
isSort = \case
Sort Sort
s -> forall a. a -> Maybe a
Just Sort
s
Term
_ -> forall a. Maybe a
Nothing
impossibleTerm :: CallStack -> Term
impossibleTerm :: CallStack -> Term
impossibleTerm = forall a b c. (a -> b -> c) -> b -> a -> c
flip ArgName -> Elims -> Term
Dummy [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Impossible
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM :: forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
f Tele a
EmptyTel = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Tele a
EmptyTel
mapAbsNamesM ArgName -> m ArgName
f (ExtendTel a
a ( Abs ArgName
x Tele a
b)) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( forall a. ArgName -> a -> Abs a
Abs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m ArgName
f ArgName
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
f Tele a
b)
mapAbsNamesM ArgName -> m ArgName
f (ExtendTel a
a (NoAbs ArgName
x Tele a
b)) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. ArgName -> a -> Abs a
NoAbs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m ArgName
f ArgName
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM ArgName -> m ArgName
f Tele a
b)
mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames :: forall a. ShowS -> Tele a -> Tele a
mapAbsNames ShowS
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
Applicative m =>
(ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
f)
replaceEmptyName :: ArgName -> Tele a -> Tele a
replaceEmptyName :: forall a. ArgName -> Tele a -> Tele a
replaceEmptyName ArgName
x = forall a. ShowS -> Tele a -> Tele a
mapAbsNames forall a b. (a -> b) -> a -> b
$ \ ArgName
y -> if forall a. Null a => a -> Bool
null ArgName
y then ArgName
x else ArgName
y
type ListTel' a = [Dom (a, Type)]
type ListTel = ListTel' ArgName
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
telFromList' :: forall a. (a -> ArgName) -> ListTel' a -> Telescope
telFromList' a -> ArgName
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr Dom' Term (a, Type) -> Telescope -> Telescope
extTel forall a. Tele a
EmptyTel
where
extTel :: Dom' Term (a, Type) -> Telescope -> Telescope
extTel dom :: Dom' Term (a, Type)
dom@Dom{unDom :: forall t e. Dom' t e -> e
unDom = (a
x, Type
a)} = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Dom' Term (a, Type)
dom{unDom :: Type
unDom = Type
a}) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ArgName -> a -> Abs a
Abs (a -> ArgName
f a
x)
telFromList :: ListTel -> Telescope
telFromList :: ListTel -> Telescope
telFromList = forall a. (a -> ArgName) -> ListTel' a -> Telescope
telFromList' forall a. a -> a
id
telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
telToList :: forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
EmptyTel = []
telToList (ExtendTel Dom t
arg (Abs ArgName
x Tele (Dom t)
tel)) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName
x,) Dom t
arg forall a. a -> [a] -> [a]
: forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
tel
telToList (ExtendTel Dom t
_ NoAbs{} ) = forall a. HasCallStack => a
__IMPOSSIBLE__
listTel :: Lens' ListTel Telescope
listTel :: Lens' ListTel Telescope
listTel ListTel -> f ListTel
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListTel -> f ListTel
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList
class TelToArgs a where
telToArgs :: a -> [Arg ArgName]
instance TelToArgs ListTel where
telToArgs :: ListTel -> [Arg ArgName]
telToArgs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ \ Dom (ArgName, Type)
dom -> forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom (ArgName, Type)
dom) (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (ArgName, Type)
dom)
instance TelToArgs Telescope where
telToArgs :: Telescope -> [Arg ArgName]
telToArgs = forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList
class SgTel a where
sgTel :: a -> Telescope
instance SgTel (ArgName, Dom Type) where
sgTel :: (ArgName, Dom' Term Type) -> Telescope
sgTel (ArgName
x, !Dom' Term Type
dom) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
dom forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
x forall a. Tele a
EmptyTel
instance SgTel (Dom (ArgName, Type)) where
sgTel :: Dom (ArgName, Type) -> Telescope
sgTel Dom (ArgName, Type)
dom = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (ArgName, Type)
dom) forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (ArgName, Type)
dom) forall a. Tele a
EmptyTel
instance SgTel (Dom Type) where
sgTel :: Dom' Term Type -> Telescope
sgTel Dom' Term Type
dom = forall a. SgTel a => a -> Telescope
sgTel (ShowS
stringToArgName ArgName
"_", Dom' Term Type
dom)
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 forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom' Term Type
_ Abs Type
b -> Int
1 forall a. Num a => a -> a -> a
+ Type -> Int
arity (forall a. Abs a -> a
unAbs Abs Type
b)
Term
_ -> Int
0
class Suggest a where
suggestName :: a -> Maybe String
instance Suggest String where
suggestName :: ArgName -> Maybe ArgName
suggestName ArgName
"_" = forall a. Maybe a
Nothing
suggestName ArgName
x = forall a. a -> Maybe a
Just ArgName
x
instance Suggest (Abs b) where
suggestName :: Abs b -> Maybe ArgName
suggestName = forall a. Suggest a => a -> Maybe ArgName
suggestName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> ArgName
absName
instance Suggest Name where
suggestName :: Name -> Maybe ArgName
suggestName = forall a. Suggest a => a -> Maybe ArgName
suggestName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> ArgName
nameToArgName
instance Suggest Term where
suggestName :: Term -> Maybe ArgName
suggestName (Lam ArgInfo
_ Abs Term
v) = forall a. Suggest a => a -> Maybe ArgName
suggestName Abs Term
v
suggestName Term
_ = forall a. Maybe a
Nothing
data Suggestion = forall a. Suggest a => Suggestion a
suggests :: [Suggestion] -> String
suggests :: [Suggestion] -> ArgName
suggests [] = ArgName
"x"
suggests (Suggestion a
x : [Suggestion]
xs) = forall a. a -> Maybe a -> a
fromMaybe ([Suggestion] -> ArgName
suggests [Suggestion]
xs) forall a b. (a -> b) -> a -> b
$ forall a. Suggest a => a -> Maybe ArgName
suggestName a
x
unSpine :: Term -> Term
unSpine :: Term -> Term
unSpine = (ProjOrigin -> Bool) -> Term -> Term
unSpine' forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
p Term
v =
case Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v of
Just (Elims -> Term
h, Elims
es) -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h [] Elims
es
Maybe (Elims -> Term, Elims)
Nothing -> Term
v
where
loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h Elims
res Elims
es =
case Elims
es of
[] -> Term
v
Proj ProjOrigin
o QName
f : Elims
es' | ProjOrigin -> Bool
p ProjOrigin
o -> (Elims -> Term) -> Elims -> Elims -> Term
loop (QName -> Elims -> Term
Def QName
f) [forall a. Arg a -> Elim' a
Apply (forall a. a -> Arg a
defaultArg Term
v)] Elims
es'
Elim' Term
e : Elims
es' -> (Elims -> Term) -> Elims -> Elims -> Term
loop Elims -> Term
h (Elim' Term
e forall a. a -> [a] -> [a]
: Elims
res) Elims
es'
where v :: Term
v = Elims -> Term
h forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse Elims
res
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims Term
v =
case Term
v of
Var Int
i Elims
es -> forall a. a -> Maybe a
Just (Int -> Elims -> Term
Var Int
i, Elims
es)
Def QName
f Elims
es -> forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def QName
f, Elims
es)
MetaV MetaId
x Elims
es -> forall a. a -> Maybe a
Just (MetaId -> Elims -> Term
MetaV MetaId
x, Elims
es)
Con{} -> forall a. Maybe a
Nothing
Lit{} -> forall a. Maybe a
Nothing
Lam ArgInfo
h (Abs ArgName
_ Term
v) | forall a. LensHiding a => a -> Bool
visible ArgInfo
h -> case Term
v of
Var Int
0 [Proj ProjOrigin
_o QName
f] -> forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def QName
f, [])
Term
_ -> forall a. Maybe a
Nothing
Lam{} -> forall a. Maybe a
Nothing
Pi{} -> forall a. Maybe a
Nothing
Sort{} -> forall a. Maybe a
Nothing
Level{} -> forall a. Maybe a
Nothing
DontCare{} -> forall a. Maybe a
Nothing
Dummy{} -> forall a. Maybe a
Nothing
instance Null (Tele a) where
empty :: Tele a
empty = forall a. Tele a
EmptyTel
null :: Tele a -> Bool
null Tele a
EmptyTel = Bool
True
null ExtendTel{} = Bool
False
instance Null Clause where
empty :: Clause
empty = Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty forall a. Null a => a
empty Bool
False forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Null a => a
empty
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
_)
= forall a. Null a => a -> Bool
null Telescope
tel
Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null NAPs
pats
Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Maybe Term
body
instance Show a => Show (Abs a) where
showsPrec :: Int -> Abs a -> ShowS
showsPrec Int
p (Abs ArgName
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
ArgName -> ShowS
showString ArgName
"Abs " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows ArgName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ShowS
showString ArgName
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a
showsPrec Int
p (NoAbs ArgName
x a
a) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
ArgName -> ShowS
showString ArgName
"NoAbs " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows ArgName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ShowS
showString ArgName
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a
instance Sized (Tele a) where
size :: Tele a -> Int
size Tele a
EmptyTel = Int
0
size (ExtendTel a
_ Abs (Tele a)
tel) = Int
1 forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Int
size Abs (Tele a)
tel
instance Sized a => Sized (Abs a) where
size :: Abs a -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> a
unAbs
class TermSize a where
termSize :: a -> Int
termSize = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermSize a => a -> Sum Int
tsize
tsize :: a -> Sum Int
instance {-# OVERLAPPABLE #-} (Foldable t, TermSize a) => TermSize (t a) where
tsize :: t a -> Sum Int
tsize = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. TermSize a => a -> Sum Int
tsize
instance TermSize Term where
tsize :: Term -> Sum Int
tsize = \case
Var Int
_ Elims
vs -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Def QName
_ Elims
vs -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Con ConHead
_ ConInfo
_ Elims
vs -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
MetaV MetaId
_ Elims
vs -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
vs
Level Level
l -> forall a. TermSize a => a -> Sum Int
tsize Level
l
Lam ArgInfo
_ Abs Term
f -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Term
f
Lit Literal
_ -> Sum Int
1
Pi Dom' Term Type
a Abs Type
b -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Dom' Term Type
a forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Type
b
Sort Sort
s -> forall a. TermSize a => a -> Sum Int
tsize Sort
s
DontCare Term
mv -> forall a. TermSize a => a -> Sum Int
tsize Term
mv
Dummy{} -> Sum Int
1
instance TermSize Sort where
tsize :: Sort -> Sum Int
tsize = \case
Type Level
l -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
Prop Level
l -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
Inf IsFibrant
_ Integer
_ -> Sum Int
1
SSet Level
l -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Level
l
Sort
SizeUniv -> Sum Int
1
Sort
LockUniv -> Sum Int
1
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Dom' Term Term
a forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Abs Sort
s2
FunSort Sort
s1 Sort
s2 -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s2
UnivSort Sort
s -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Sort
s
MetaS MetaId
_ Elims
es -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
es
DefS QName
_ Elims
es -> Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Elims
es
DummyS{} -> Sum Int
1
instance TermSize Level where
tsize :: Level -> Sum Int
tsize (Max Integer
_ [PlusLevel]
as) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize [PlusLevel]
as
instance TermSize PlusLevel where
tsize :: PlusLevel -> Sum Int
tsize (Plus Integer
_ Term
a) = forall a. TermSize a => a -> Sum Int
tsize Term
a
instance TermSize a => TermSize (Substitution' a) where
tsize :: Substitution' a -> Sum Int
tsize Substitution' a
IdS = Sum Int
1
tsize (EmptyS Impossible
_) = Sum Int
1
tsize (Wk Int
_ Substitution' a
rho) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (a
t :# Substitution' a
rho) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize a
t forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (Strengthen Impossible
_ Substitution' a
rho) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
tsize (Lift Int
_ Substitution' a
rho) = Sum Int
1 forall a. Num a => a -> a -> a
+ forall a. TermSize a => a -> Sum Int
tsize Substitution' a
rho
instance KillRange DataOrRecord where
killRange :: DataOrRecord -> DataOrRecord
killRange = forall a. a -> a
id
instance KillRange ConHead where
killRange :: ConHead -> ConHead
killRange (ConHead QName
c DataOrRecord
d Induction
i [Arg QName]
fs) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
d Induction
i [Arg QName]
fs
instance KillRange Term where
killRange :: Term -> Term
killRange = \case
Var Int
i Elims
vs -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (Int -> Elims -> Term
Var Int
i) Elims
vs
Def QName
c Elims
vs -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 QName -> Elims -> Term
Def QName
c Elims
vs
Con ConHead
c ConInfo
ci Elims
vs -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci Elims
vs
MetaV MetaId
m Elims
vs -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (MetaId -> Elims -> Term
MetaV MetaId
m) Elims
vs
Lam ArgInfo
i Abs Term
f -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ArgInfo -> Abs Term -> Term
Lam ArgInfo
i Abs Term
f
Lit Literal
l -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Literal -> Term
Lit Literal
l
Level Level
l -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Level -> Term
Level Level
l
Pi Dom' Term Type
a Abs Type
b -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Dom' Term Type -> Abs Type -> Term
Pi Dom' Term Type
a Abs Type
b
Sort Sort
s -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Sort -> Term
Sort Sort
s
DontCare Term
mv -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Term -> Term
DontCare Term
mv
v :: Term
v@Dummy{} -> Term
v
instance KillRange Level where
killRange :: Level -> Level
killRange (Max Integer
n [PlusLevel]
as) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n) [PlusLevel]
as
instance KillRange PlusLevel where
killRange :: PlusLevel -> PlusLevel
killRange (Plus Integer
n Term
l) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. Integer -> t -> PlusLevel' t
Plus Integer
n) Term
l
instance (KillRange a) => KillRange (Type' a) where
killRange :: KillRangeT (Type' a)
killRange (El Sort
s a
v) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t a. Sort' t -> a -> Type'' t a
El Sort
s a
v
instance KillRange Sort where
killRange :: Sort -> Sort
killRange = \case
Inf IsFibrant
f Integer
n -> forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
Sort
SizeUniv -> forall t. Sort' t
SizeUniv
Sort
LockUniv -> forall t. Sort' t
LockUniv
Type Level
a -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
Type Level
a
Prop Level
a -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
Prop Level
a
SSet Level
a -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Level' t -> Sort' t
SSet Level
a
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2
FunSort Sort
s1 Sort
s2 -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2
UnivSort Sort
s -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall t. Sort' t -> Sort' t
UnivSort Sort
s
MetaS MetaId
x Elims
es -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x) Elims
es
DefS QName
d Elims
es -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d Elims
es
s :: Sort
s@DummyS{} -> Sort
s
instance KillRange Substitution where
killRange :: KillRangeT Substitution
killRange Substitution
IdS = forall a. Substitution' a
IdS
killRange (EmptyS Impossible
err) = forall a. Impossible -> Substitution' a
EmptyS Impossible
err
killRange (Wk Int
n Substitution
rho) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Int -> Substitution' a -> Substitution' a
Wk Int
n) Substitution
rho
killRange (Term
t :# Substitution
rho) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall a. a -> Substitution' a -> Substitution' a
(:#) Term
t Substitution
rho
killRange (Strengthen Impossible
err Substitution
rho) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
err) Substitution
rho
killRange (Lift Int
n Substitution
rho) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Int -> Substitution' a -> Substitution' a
Lift Int
n) Substitution
rho
instance KillRange PatOrigin where
killRange :: PatOrigin -> PatOrigin
killRange = forall a. a -> a
id
instance KillRange PatternInfo where
killRange :: PatternInfo -> PatternInfo
killRange (PatternInfo PatOrigin
o [Name]
xs) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
o [Name]
xs
instance KillRange ConPatternInfo where
killRange :: ConPatternInfo -> ConPatternInfo
killRange (ConPatternInfo PatternInfo
i Bool
mr Bool
b Maybe (Arg Type)
mt Bool
lz) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
i Bool
mr Bool
b) Maybe (Arg Type)
mt Bool
lz
instance KillRange DBPatVar where
killRange :: DBPatVar -> DBPatVar
killRange (DBPatVar ArgName
x Int
i) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ArgName -> Int -> DBPatVar
DBPatVar ArgName
x Int
i
instance KillRange a => KillRange (Pattern' a) where
killRange :: KillRangeT (Pattern' a)
killRange Pattern' a
p =
case Pattern' a
p of
VarP PatternInfo
o a
x -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o a
x
DotP PatternInfo
o Term
v -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
v
ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps
LitP PatternInfo
o Literal
l -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
ProjP ProjOrigin
o QName
q -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o) QName
q
IApplyP PatternInfo
o Term
u Term
t a
x -> forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 (forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o) Term
u Term
t a
x
DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps -> forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 (forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o) QName
q [NamedArg (Pattern' a)]
ps
instance KillRange Clause where
killRange :: Clause -> 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) =
forall a b c d e f g h i j k.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
killRange10 Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> 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
instance KillRange a => KillRange (Tele a) where
killRange :: KillRangeT (Tele a)
killRange = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. KillRange a => KillRangeT a
killRange
instance KillRange a => KillRange (Blocked a) where
killRange :: KillRangeT (Blocked a)
killRange = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. KillRange a => KillRangeT a
killRange
instance KillRange a => KillRange (Abs a) where
killRange :: KillRangeT (Abs a)
killRange = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. KillRange a => KillRangeT a
killRange
instance Pretty a => Pretty (Substitution' a) where
prettyPrec :: Int -> Substitution' a -> Doc
prettyPrec = forall {t} {a}.
(Ord t, Num t, Pretty a) =>
t -> Substitution' a -> Doc
pr
where
pr :: t -> Substitution' a -> Doc
pr t
p Substitution' a
rho = case Substitution' a
rho of
Substitution' a
IdS -> Doc
"idS"
EmptyS Impossible
err -> Doc
"emptyS"
a
t :# Substitution' a
rho -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
2) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ t -> Substitution' a -> Doc
pr t
2 Substitution' a
rho forall a. Semigroup a => a -> a -> a
<> Doc
",", forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
3 a
t ]
Strengthen Impossible
_ Substitution' a
rho -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ Doc
"strS" Doc -> Doc -> Doc
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
Wk Int
n Substitution' a
rho -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ ArgName -> Doc
text (ArgName
"wkS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n) Doc -> Doc -> Doc
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
Lift Int
n Substitution' a
rho -> Bool -> Doc -> Doc
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ ArgName -> Doc
text (ArgName
"liftS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
n) Doc -> Doc -> Doc
<+> t -> Substitution' a -> Doc
pr t
10 Substitution' a
rho
instance Pretty Term where
prettyPrec :: Int -> Term -> Doc
prettyPrec Int
p Term
v =
case Term
v of
Var Int
x Elims
els -> ArgName -> Doc
text (ArgName
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
x) Doc -> Elims -> Doc
`pApp` Elims
els
Lam ArgInfo
ai Abs Term
b ->
Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"λ" Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
ai forall a. a -> a
id (ArgName -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> ArgName
absName forall a b. (a -> b) -> a -> b
$ Abs Term
b) Doc -> Doc -> Doc
<+> Doc
"->"
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Term
b) ]
Lit Literal
l -> forall a. Pretty a => a -> Doc
pretty Literal
l
Def QName
q Elims
els -> forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Elims -> Doc
`pApp` Elims
els
Con ConHead
c ConInfo
ci Elims
vs -> forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c) Doc -> Elims -> Doc
`pApp` Elims
vs
Pi Dom' Term Type
a (NoAbs ArgName
_ Type
b) -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 (forall t e. Dom' t e -> e
unDom Dom' Term Type
a) Doc -> Doc -> Doc
<+> Doc
"->"
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Type
b ]
Pi Dom' Term Type
a Abs Type
b -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. LensHiding a => a -> Doc -> Doc
pDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Type
a) (ArgName -> Doc
text (forall a. Abs a -> ArgName
absName Abs Type
b) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom' Term Type
a)) Doc -> Doc -> Doc
<+> Doc
"->"
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Type
b) ]
Sort Sort
s -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Sort
s
Level Level
l -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Level
l
MetaV MetaId
x Elims
els -> forall a. Pretty a => a -> Doc
pretty MetaId
x Doc -> Elims -> Doc
`pApp` Elims
els
DontCare Term
v -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
v
Dummy ArgName
s Elims
es -> Doc -> Doc
parens (ArgName -> Doc
text ArgName
s) Doc -> Elims -> Doc
`pApp` Elims
es
where
pApp :: Doc -> Elims -> Doc
pApp Doc
d Elims
els = Bool -> Doc -> Doc
mparens (Bool -> Bool
not (forall a. Null a => a -> Bool
null Elims
els) Bool -> Bool -> Bool
&& Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
d, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) Elims
els)]
instance Pretty t => Pretty (Abs t) where
pretty :: Abs t -> Doc
pretty (Abs ArgName
x t
t) = Doc
"Abs" Doc -> Doc -> Doc
<+> (ArgName -> Doc
text ArgName
x forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t
pretty (NoAbs ArgName
x t
t) = Doc
"NoAbs" Doc -> Doc -> Doc
<+> (ArgName -> Doc
text ArgName
x forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t
instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
pretty :: Dom' t e -> Doc
pretty Dom' t e
dom = Doc
pTac Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> Doc -> Doc
pDom Dom' t e
dom (forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t e
dom)
where
pTac :: Doc
pTac | Just t
t <- forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Doc
"@" forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc
"tactic" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty t
t)
| Bool
otherwise = forall a. Null a => a
empty
pDom :: LensHiding a => a -> Doc -> Doc
pDom :: forall a. LensHiding a => a -> Doc -> Doc
pDom a
i =
case forall a. LensHiding a => a -> Hiding
getHiding a
i of
Hiding
NotHidden -> Doc -> Doc
parens
Hiding
Hidden -> Doc -> Doc
braces
Instance{} -> Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
braces
instance Pretty Clause where
pretty :: Clause -> Doc
pretty Clause{clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
b, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
t} =
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty Telescope
tel Doc -> Doc -> Doc
<+> Doc
"|-"
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) NAPs
ps) Doc -> Doc -> Doc
<+> Doc
"="
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall {a} {a}. (Pretty a, Pretty a) => Maybe a -> Maybe a -> Doc
pBody Maybe Term
b Maybe (Arg Type)
t ] ]
where
pBody :: Maybe a -> Maybe a -> Doc
pBody Maybe a
Nothing Maybe a
_ = Doc
"(absurd)"
pBody (Just a
b) Maybe a
Nothing = forall a. Pretty a => a -> Doc
pretty a
b
pBody (Just a
b) (Just a
t) = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty a
b Doc -> Doc -> Doc
<+> Doc
":", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty a
t ]
instance Pretty a => Pretty (Tele (Dom a)) where
pretty :: Tele (Dom a) -> Doc
pretty Tele (Dom a)
tel = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [ forall a. LensHiding a => a -> Doc -> Doc
pDom Dom a
a (ArgName -> Doc
text ArgName
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom a
a)) | (ArgName
x, Dom a
a) <- forall {b}. Tele b -> [(ArgName, b)]
telToList Tele (Dom a)
tel ]
where
telToList :: Tele b -> [(ArgName, b)]
telToList Tele b
EmptyTel = []
telToList (ExtendTel b
a Abs (Tele b)
tel) = (forall a. Abs a -> ArgName
absName Abs (Tele b)
tel, b
a) forall a. a -> [a] -> [a]
: Tele b -> [(ArgName, b)]
telToList (forall a. Abs a -> a
unAbs Abs (Tele b)
tel)
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
0 Int -> Doc
d = Int -> Doc
d Int
p
prettyPrecLevelSucs Int
p Integer
n Int -> Doc
d = Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"lsuc" Doc -> Doc -> Doc
<+> Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
10 (Integer
n forall a. Num a => a -> a -> a
- Integer
1) Int -> Doc
d
instance Pretty Level where
prettyPrec :: Int -> Level -> Doc
prettyPrec Int
p (Max Integer
n [PlusLevel]
as) =
case [PlusLevel]
as of
[] -> Doc
prettyN
[PlusLevel
a] | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p PlusLevel
a
[PlusLevel]
_ -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
List.foldr1 (\Doc
a Doc
b -> Doc
"lub" Doc -> Doc -> Doc
<+> Doc
a Doc -> Doc -> Doc
<+> Doc
b) forall a b. (a -> b) -> a -> b
$
[ Doc
prettyN | Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0 ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [PlusLevel]
as
where
prettyN :: Doc
prettyN = Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
n (forall a b. a -> b -> a
const Doc
"lzero")
instance Pretty PlusLevel where
prettyPrec :: Int -> PlusLevel -> Doc
prettyPrec Int
p (Plus Integer
n Term
a) = Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs Int
p Integer
n forall a b. (a -> b) -> a -> b
$ \Int
p -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
a
instance Pretty Sort where
prettyPrec :: Int -> Sort -> Doc
prettyPrec Int
p Sort
s =
case Sort
s of
Type (ClosedLevel Integer
0) -> Doc
"Set"
Type (ClosedLevel Integer
n) -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"Set" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
Type Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"Set" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
Prop (ClosedLevel Integer
0) -> Doc
"Prop"
Prop (ClosedLevel Integer
n) -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"Prop" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
Prop Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"Prop" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
Inf IsFibrant
f Integer
0 -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ IsFibrant -> ShowS
addS IsFibrant
f ArgName
"Setω"
Inf IsFibrant
f Integer
n -> ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ IsFibrant -> ShowS
addS IsFibrant
f ArgName
"Setω" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Integer
n
SSet Level
l -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"SSet" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Level
l
Sort
SizeUniv -> Doc
"SizeUniv"
Sort
LockUniv -> Doc
"LockUniv"
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
Doc
"piSort" Doc -> Doc -> Doc
<+> forall a. LensHiding a => a -> Doc -> Doc
pDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Term
a) (ArgName -> Doc
text (forall a. Abs a -> ArgName
absName Abs Sort
s2) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall t e. Dom' t e -> e
unDom Dom' Term Term
a))
Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ ArgName -> Doc
text (ArgName
"λ " forall a. [a] -> [a] -> [a]
++ forall a. Abs a -> ArgName
absName Abs Sort
s2 forall a. [a] -> [a] -> [a]
++ ArgName
" ->")
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty (forall a. Abs a -> a
unAbs Abs Sort
s2) ])
FunSort Sort
a Sort
b -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
Doc
"funSort" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
a Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
b
UnivSort Sort
s -> Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Doc
"univSort" Doc -> Doc -> Doc
<+> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Sort
s
MetaS MetaId
x Elims
es -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
DefS QName
d Elims
es -> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
DummyS ArgName
s -> Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ ArgName -> Doc
text ArgName
s
where
addS :: IsFibrant -> ShowS
addS IsFibrant
IsFibrant ArgName
t = ArgName
t
addS IsFibrant
IsStrict ArgName
t = ArgName
"S" forall a. [a] -> [a] -> [a]
++ ArgName
t
instance Pretty Type where
prettyPrec :: Int -> Type -> Doc
prettyPrec Int
p (El Sort
_ Term
a) = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term
a
instance Pretty DBPatVar where
prettyPrec :: Int -> DBPatVar -> Doc
prettyPrec Int
_ DBPatVar
x = ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ ShowS
patVarNameToString (DBPatVar -> ArgName
dbPatVarName DBPatVar
x) forall a. [a] -> [a] -> [a]
++ ArgName
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
instance Pretty a => Pretty (Pattern' a) where
prettyPrec :: Int -> Pattern' a -> Doc
prettyPrec Int
n (VarP PatternInfo
_o a
x) = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x
prettyPrec Int
_ (DotP PatternInfo
_o Term
t) = Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Term
t
prettyPrec Int
n (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
nps)= Bool -> Doc -> Doc
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
(Doc
lazy forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c)) Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
where ps :: [Arg (Pattern' a)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
lazy :: Doc
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Doc
"~"
| Bool
otherwise = forall a. Null a => a
empty
prettyPrec Int
n (DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
nps)= Bool -> Doc -> Doc
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
where ps :: [Arg (Pattern' a)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
prettyPrec Int
_ (LitP PatternInfo
_ Literal
l) = forall a. Pretty a => a -> Doc
pretty Literal
l
prettyPrec Int
_ (ProjP ProjOrigin
_o QName
q) = ArgName -> Doc
text (ArgName
"." forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
q)
prettyPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x
instance NFData Term where
rnf :: Term -> ()
rnf = \case
Var Int
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
Lam ArgInfo
_ Abs Term
b -> forall a. NFData a => a -> ()
rnf (forall a. Abs a -> a
unAbs Abs Term
b)
Lit Literal
l -> forall a. NFData a => a -> ()
rnf Literal
l
Def QName
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
Con ConHead
_ ConInfo
_ Elims
vs -> forall a. NFData a => a -> ()
rnf Elims
vs
Pi Dom' Term Type
a Abs Type
b -> forall a. NFData a => a -> ()
rnf (forall t e. Dom' t e -> e
unDom Dom' Term Type
a, forall a. Abs a -> a
unAbs Abs Type
b)
Sort Sort
s -> forall a. NFData a => a -> ()
rnf Sort
s
Level Level
l -> forall a. NFData a => a -> ()
rnf Level
l
MetaV MetaId
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
DontCare Term
v -> forall a. NFData a => a -> ()
rnf Term
v
Dummy ArgName
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
instance NFData Type where
rnf :: Type -> ()
rnf (El Sort
s Term
v) = forall a. NFData a => a -> ()
rnf (Sort
s, Term
v)
instance NFData Sort where
rnf :: Sort -> ()
rnf = \case
Type Level
l -> forall a. NFData a => a -> ()
rnf Level
l
Prop Level
l -> forall a. NFData a => a -> ()
rnf Level
l
Inf IsFibrant
_ Integer
_ -> ()
SSet Level
l -> forall a. NFData a => a -> ()
rnf Level
l
Sort
SizeUniv -> ()
Sort
LockUniv -> ()
PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall a. NFData a => a -> ()
rnf (Dom' Term Term
a, Sort
b, forall a. Abs a -> a
unAbs Abs Sort
c)
FunSort Sort
a Sort
b -> forall a. NFData a => a -> ()
rnf (Sort
a, Sort
b)
UnivSort Sort
a -> forall a. NFData a => a -> ()
rnf Sort
a
MetaS MetaId
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
DefS QName
_ Elims
es -> forall a. NFData a => a -> ()
rnf Elims
es
DummyS ArgName
_ -> ()
instance NFData Level where
rnf :: Level -> ()
rnf (Max Integer
n [PlusLevel]
as) = forall a. NFData a => a -> ()
rnf (Integer
n, [PlusLevel]
as)
instance NFData PlusLevel where
rnf :: PlusLevel -> ()
rnf (Plus Integer
n Term
l) = forall a. NFData a => a -> ()
rnf (Integer
n, Term
l)
instance NFData e => NFData (Dom e) where
rnf :: Dom e -> ()
rnf (Dom ArgInfo
a Bool
b Maybe (WithOrigin (Ranged ArgName))
c Maybe Term
d e
e) = forall a. NFData a => a -> ()
rnf ArgInfo
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Bool
b seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe (WithOrigin (Ranged ArgName))
c seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe Term
d seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf e
e
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)