module Mikan.Syntax.Internal.Dom
  ( -- * Abstractions
    Abs(..), isAbs

    -- * Domains
  , DomInfo(..), Dom'(.., Dom)
  , domTactic, dTactic
  , domIsFinite, dIsFinite
  , domInfo, dInfo

  , defaultArgDom, defaultNamedArgDom, defaultDom
  , argFromDom, domFromArg
  , domFromNamedArg, namedArgFromDom
  )
  where

import Control.DeepSeq
import Data.Text.Short (ShortText)

import GHC.Generics (Generic)

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

import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.Size

-- | A binder, which may or may not actually introduce a new variable.
data Abs a
  = Abs   { forall a. Abs a -> ArgName
absName :: ArgName, forall a. Abs a -> a
unAbs :: a }
  -- ^ The body has an extra free variable.
  | NoAbs { absName :: ArgName, unAbs :: a }
  -- ^ The body does not actually depend on the bound variable.
  deriving ((forall m. Monoid m => Abs m -> m)
-> (forall m a. Monoid m => (a -> m) -> Abs a -> m)
-> (forall m a. Monoid m => (a -> m) -> Abs a -> m)
-> (forall a b. (a -> b -> b) -> b -> Abs a -> b)
-> (forall a b. (a -> b -> b) -> b -> Abs a -> b)
-> (forall b a. (b -> a -> b) -> b -> Abs a -> b)
-> (forall b a. (b -> a -> b) -> b -> Abs a -> b)
-> (forall a. (a -> a -> a) -> Abs a -> a)
-> (forall a. (a -> a -> a) -> Abs a -> a)
-> (forall a. Abs a -> [a])
-> (forall a. Abs a -> Bool)
-> (forall a. Abs a -> Int)
-> (forall a. Eq a => a -> Abs a -> Bool)
-> (forall a. Ord a => Abs a -> a)
-> (forall a. Ord a => Abs a -> a)
-> (forall a. Num a => Abs a -> a)
-> (forall a. Num a => Abs a -> a)
-> Foldable Abs
forall a. Eq a => a -> Abs a -> Bool
forall a. Num a => Abs a -> a
forall a. Ord a => Abs a -> a
forall m. Monoid m => Abs m -> m
forall a. Abs a -> Bool
forall a. Abs a -> Int
forall a. Abs a -> [a]
forall a. (a -> a -> a) -> Abs a -> a
forall m a. Monoid m => (a -> m) -> Abs a -> m
forall b a. (b -> a -> b) -> b -> Abs a -> b
forall a b. (a -> b -> b) -> b -> Abs a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Abs m -> m
fold :: forall m. Monoid m => Abs m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Abs a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Abs a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Abs a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Abs a -> a
foldr1 :: forall a. (a -> a -> a) -> Abs a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Abs a -> a
foldl1 :: forall a. (a -> a -> a) -> Abs a -> a
$ctoList :: forall a. Abs a -> [a]
toList :: forall a. Abs a -> [a]
$cnull :: forall a. Abs a -> Bool
null :: forall a. Abs a -> Bool
$clength :: forall a. Abs a -> Int
length :: forall a. Abs a -> Int
$celem :: forall a. Eq a => a -> Abs a -> Bool
elem :: forall a. Eq a => a -> Abs a -> Bool
$cmaximum :: forall a. Ord a => Abs a -> a
maximum :: forall a. Ord a => Abs a -> a
$cminimum :: forall a. Ord a => Abs a -> a
minimum :: forall a. Ord a => Abs a -> a
$csum :: forall a. Num a => Abs a -> a
sum :: forall a. Num a => Abs a -> a
$cproduct :: forall a. Num a => Abs a -> a
product :: forall a. Num a => Abs a -> a
Foldable, Functor Abs
Foldable Abs
(Functor Abs, Foldable Abs) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Abs a -> f (Abs b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Abs (f a) -> f (Abs a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Abs a -> m (Abs b))
-> (forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a))
-> Traversable Abs
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Abs (f a) -> f (Abs a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Abs a -> m (Abs b)
$csequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
sequence :: forall (m :: * -> *) a. Monad m => Abs (m a) -> m (Abs a)
Traversable, (forall x. Abs a -> Rep (Abs a) x)
-> (forall x. Rep (Abs a) x -> Abs a) -> Generic (Abs a)
forall x. Rep (Abs a) x -> Abs a
forall x. Abs a -> Rep (Abs a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Abs a) x -> Abs a
forall a x. Abs a -> Rep (Abs a) x
$cfrom :: forall a x. Abs a -> Rep (Abs a) x
from :: forall x. Abs a -> Rep (Abs a) x
$cto :: forall a x. Rep (Abs a) x -> Abs a
to :: forall x. Rep (Abs a) x -> Abs a
Generic)

isAbs :: Abs a -> Bool
isAbs :: forall a. Abs a -> Bool
isAbs (Abs {}) = Bool
True
isAbs (NoAbs {}) = Bool
False

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

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

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

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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Abs " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ShowS
forall a. Show a => a -> ShowS
shows ArgName
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
a

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

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

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

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

instance NFData a => NFData (Abs a)

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

data DomInfo t = DomInfo
  { forall t. DomInfo t -> ArgInfo
domInfoArgInfo  :: !ArgInfo
  , forall t. DomInfo t -> Maybe NamedName
domInfoName     :: !(Maybe NamedName)
  -- ^ e.g. @x@ in @{x = y : A} -> B@.
  , forall t. DomInfo t -> Bool
domInfoIsFinite :: !Bool
  -- ^ Is this a Π-type (False), or a partial type (True)?
  , forall t. DomInfo t -> Maybe t
domInfoTactic   :: !(Maybe t)
  -- ^ "@tactic e".
  }

instance Show t => Show (DomInfo t) where
  show :: DomInfo t -> String
show (DomInfo ArgInfo
a Maybe NamedName
b Bool
c Maybe t
d) = (ArgInfo, Maybe NamedName, Bool, Maybe t) -> String
forall a. Show a => a -> String
show (ArgInfo
a,Maybe NamedName
b,Bool
c,Maybe t
d)

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

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

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

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

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

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

-- | Similar to 'Arg', but for domain types of functions and telescopes.
--
--   @Dom@ is used in 'Pi' of internal syntax, in 'Context' and 'Telescope'.
--   'Arg' is used for actual arguments ('Var', 'Con', 'Def' etc.)
--   and in 'Abstract' syntax and other situations.
--
--   [ cubical ] When @annFinite (argInfoAnnotation domInfo) = True@ for
--   the domain of a 'Pi' type, the elements should be compared by
--   tabulating the domain type.  Only supported in case the domain type
--   is primIsOne, to obtain the correct equality for partial elements.
--
data Dom' t e = Dom'
  { forall t e. Dom' t e -> DomInfo t
domDomInfo :: !(DomInfo t)
  , forall t e. Dom' t e -> e
unDom      :: e
  }
  deriving (Int -> Dom' t e -> ShowS
[Dom' t e] -> ShowS
Dom' t e -> String
(Int -> Dom' t e -> ShowS)
-> (Dom' t e -> String) -> ([Dom' t e] -> ShowS) -> Show (Dom' t e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([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 -> String
$cshowsPrec :: forall t e. (Show t, Show e) => Int -> Dom' t e -> ShowS
showsPrec :: Int -> Dom' t e -> ShowS
$cshow :: forall t e. (Show t, Show e) => Dom' t e -> String
show :: Dom' t e -> String
$cshowList :: forall t e. (Show t, Show e) => [Dom' t e] -> ShowS
showList :: [Dom' t e] -> ShowS
Show, (forall m. Monoid m => Dom' t m -> m)
-> (forall m a. Monoid m => (a -> m) -> Dom' t a -> m)
-> (forall m a. Monoid m => (a -> m) -> Dom' t a -> m)
-> (forall a b. (a -> b -> b) -> b -> Dom' t a -> b)
-> (forall a b. (a -> b -> b) -> b -> Dom' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dom' t a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dom' t a -> b)
-> (forall a. (a -> a -> a) -> Dom' t a -> a)
-> (forall a. (a -> a -> a) -> Dom' t a -> a)
-> (forall a. Dom' t a -> [a])
-> (forall a. Dom' t a -> Bool)
-> (forall a. Dom' t a -> Int)
-> (forall a. Eq a => a -> Dom' t a -> Bool)
-> (forall a. Ord a => Dom' t a -> a)
-> (forall a. Ord a => Dom' t a -> a)
-> (forall a. Num a => Dom' t a -> a)
-> (forall a. Num a => Dom' t a -> a)
-> Foldable (Dom' t)
forall a. Eq a => a -> Dom' t a -> Bool
forall a. Num a => Dom' t a -> a
forall a. Ord a => Dom' t a -> a
forall m. Monoid m => Dom' t m -> m
forall a. Dom' t a -> Bool
forall a. Dom' t a -> Int
forall a. Dom' t a -> [a]
forall a. (a -> a -> a) -> Dom' t a -> a
forall t a. Eq a => a -> Dom' t a -> Bool
forall t a. Num a => Dom' t a -> a
forall t a. Ord a => Dom' t a -> a
forall t m. Monoid m => Dom' t m -> m
forall m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t e. Dom' t e -> Bool
forall t a. Dom' t a -> Int
forall t a. Dom' t a -> [a]
forall b a. (b -> a -> b) -> b -> Dom' t a -> b
forall a b. (a -> b -> b) -> b -> Dom' t a -> b
forall t a. (a -> a -> a) -> Dom' t a -> a
forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall t m. Monoid m => Dom' t m -> m
fold :: forall m. Monoid m => Dom' t m -> m
$cfoldMap :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Dom' t a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Dom' t a -> m
$cfoldr :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldr' :: forall t a b. (a -> b -> b) -> b -> Dom' t a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Dom' t a -> b
$cfoldl :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldl' :: forall t b a. (b -> a -> b) -> b -> Dom' t a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Dom' t a -> b
$cfoldr1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldr1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$cfoldl1 :: forall t a. (a -> a -> a) -> Dom' t a -> a
foldl1 :: forall a. (a -> a -> a) -> Dom' t a -> a
$ctoList :: forall t a. Dom' t a -> [a]
toList :: forall a. Dom' t a -> [a]
$cnull :: forall t e. Dom' t e -> Bool
null :: forall a. Dom' t a -> Bool
$clength :: forall t a. Dom' t a -> Int
length :: forall a. Dom' t a -> Int
$celem :: forall t a. Eq a => a -> Dom' t a -> Bool
elem :: forall a. Eq a => a -> Dom' t a -> Bool
$cmaximum :: forall t a. Ord a => Dom' t a -> a
maximum :: forall a. Ord a => Dom' t a -> a
$cminimum :: forall t a. Ord a => Dom' t a -> a
minimum :: forall a. Ord a => Dom' t a -> a
$csum :: forall t a. Num a => Dom' t a -> a
sum :: forall a. Num a => Dom' t a -> a
$cproduct :: forall t a. Num a => Dom' t a -> a
product :: forall a. Num a => Dom' t a -> a
Foldable, Functor (Dom' t)
Foldable (Dom' t)
(Functor (Dom' t), Foldable (Dom' t)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Dom' t a -> f (Dom' t b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Dom' t (f a) -> f (Dom' t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dom' t a -> m (Dom' t b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Dom' t (m a) -> m (Dom' t a))
-> Traversable (Dom' t)
forall t. Functor (Dom' t)
forall t. Foldable (Dom' t)
forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
forall (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
$ctraverse :: forall t (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' t a -> f (Dom' t b)
$csequenceA :: forall t (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Dom' t (f a) -> f (Dom' t a)
$cmapM :: forall t (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom' t a -> m (Dom' t b)
$csequence :: forall t (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
sequence :: forall (m :: * -> *) a. Monad m => Dom' t (m a) -> m (Dom' t a)
Traversable)

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

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

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

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

instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
  killRange :: KillRangeT (Dom' t a)
killRange (Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b a
a) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a)
-> ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
info Maybe NamedName
x Bool
t Maybe t
b a
a

-- | Ignores 'Origin' and 'FreeVariables' and tactic.
instance Eq a => Eq (Dom' t a) where
  Dom (ArgInfo Hiding
h1 Origin
_ FreeVariables
_) Maybe NamedName
s1 Bool
f1 Maybe t
_ a
x1 == :: Dom' t a -> Dom' t a -> Bool
== Dom (ArgInfo Hiding
h2 Origin
_ FreeVariables
_) Maybe NamedName
s2 Bool
f2 Maybe t
_ a
x2 =
    (Hiding
h1, Maybe NamedName
s1, Bool
f1, a
x1) (Hiding, Maybe NamedName, Bool, a)
-> (Hiding, Maybe NamedName, Bool, a) -> Bool
forall a. Eq a => a -> a -> Bool
== (Hiding
h2, Maybe NamedName
s2, Bool
f2, a
x2)

instance LensNamed (Dom' t e) where
  type NameOf (Dom' t e) = NamedName
  {-# INLINE lensNamed #-}
  lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (Dom' t e)))
lensNamed = \Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f Dom' t e
dom ->
    let !nm :: Maybe NamedName
nm = DomInfo t -> Maybe NamedName
forall t. DomInfo t -> Maybe NamedName
domInfoName (Dom' t e -> DomInfo t
forall t e. Dom' t e -> DomInfo t
domDomInfo Dom' t e
dom) in
    Maybe (NameOf (Dom' t e)) -> f (Maybe (NameOf (Dom' t e)))
f Maybe (NameOf (Dom' t e))
Maybe NamedName
nm f (Maybe NamedName)
-> (Maybe NamedName -> Dom' t e) -> f (Dom' t e)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Maybe NamedName
nm -> Dom' t e
dom { domDomInfo = (domDomInfo dom){ domInfoName = nm }}

instance LensArgInfo (Dom' t e) where
  getArgInfo :: Dom' t e -> ArgInfo
getArgInfo        = Dom' t e -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo
  setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e
setArgInfo ArgInfo
ai Dom' t e
dom = Dom' t e
dom { domDomInfo = (domDomInfo dom) {domInfoArgInfo = ai} }

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

-- The other lenses are defined through LensArgInfo

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

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

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

{-# INLINE domFromArg #-}
domFromArg :: Arg a -> Dom' t a
domFromArg :: forall a t. Arg a -> Dom' t a
domFromArg (Arg ArgInfo
i a
a) = ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> a -> Dom' t a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
i Maybe NamedName
forall a. Maybe a
Nothing Bool
False Maybe t
forall a. Maybe a
Nothing a
a

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

{-# INLINE defaultDom #-}
defaultDom :: a -> Dom' t a
defaultDom :: forall a t. a -> Dom' t a
defaultDom = ArgInfo -> a -> Dom' t a
forall a t. ArgInfo -> a -> Dom' t a
defaultArgDom ArgInfo
defaultArgInfo

{-# INLINE defaultArgDom #-}
defaultArgDom :: ArgInfo -> a -> Dom' t a
defaultArgDom :: forall a t. ArgInfo -> a -> Dom' t a
defaultArgDom ArgInfo
info a
x = Arg a -> Dom' t a
forall a t. Arg a -> Dom' t a
domFromArg (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
x)

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

-----------------------------------------------------------------------------
-- * Pretty printing
-----------------------------------------------------------------------------

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. Doc a -> Doc a -> Doc a
<+> Dom' t e -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
pDom Dom' t e
dom (e -> Doc
forall a. Pretty a => a -> Doc
pretty (Dom' t e -> e
forall t e. Dom' t e -> e
unDom Dom' t e
dom)) where
    pTac :: Doc
pTac | Just t
t <- Dom' t e -> Maybe t
forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc
"tactic" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> t -> Doc
forall a. Pretty a => a -> Doc
pretty t
t)
         | Bool
otherwise               = Doc
forall a. Monoid a => a
mempty