{-# LANGUAGE NondecreasingIndentation   #-}

{-|
    Translating from internal syntax to abstract syntax. Enables nice
    pretty printing of internal syntax.

    TODO

        - numbers on metas
        - fake dependent functions to independent functions
        - meta parameters
        - shadowing
-}
module Agda.Syntax.Translation.InternalToAbstract
  ( Reify(..)
  , MonadReify
  , NamedClause(..)
  , reifyPatterns
  , reifyUnblocked
  , blankNotInScope
  , reifyDisplayFormP
  ) where

import Prelude hiding (null)

import Control.Applicative ( liftA2 )
import Control.Arrow       ( (&&&) )
import Control.Monad       ( filterM, forM )

import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>) )
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (mapM)

import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..), TacticAttribute'(..))
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A hiding (Binder)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Abstract.UsedNames
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Scope.Base (inverseScopeLookupName)

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail))
import Agda.TypeChecking.DisplayForm
import Agda.TypeChecking.Level
import {-# SOURCE #-} Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.SyntacticEquality
import Agda.TypeChecking.Telescope

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible


-- | Like @reify@ but instantiates blocking metas, useful for reporting.
reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked :: forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked i
t = Lens' TCState Bool
-> (Bool -> Bool) -> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i))
-> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
forall a b. (a -> b) -> a -> b
$ i -> TCMT IO (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify i
t


-- Composition of reified applications ------------------------------------
--UNUSED Liang-Ting 2019-07-16
---- | Drops hidden arguments unless --show-implicit.
--napps :: Expr -> [NamedArg Expr] -> TCM Expr
--napps e = nelims e . map I.Apply

{-# SPECIALIZE apps :: Expr -> [Arg Expr] -> TCM Expr #-}
-- | Drops hidden arguments unless --show-implicit.
apps :: MonadReify m => Expr -> [Arg Expr] -> m Expr
apps :: forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
e = Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
e ([Elim' Expr] -> m Expr)
-> ([Arg Expr] -> [Elim' Expr]) -> [Arg Expr] -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Expr -> Elim' Expr) -> [Arg Expr] -> [Elim' Expr]
forall a b. (a -> b) -> [a] -> [b]
map Arg Expr -> Elim' Expr
forall a. Arg a -> Elim' a
I.Apply

-- Composition of reified eliminations ------------------------------------

{-# SPECIALIZE nelims :: Expr -> [I.Elim' (Named_ Expr)] -> TCM Expr #-}
-- | Drops hidden arguments unless --show-implicit.
nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr
nelims :: forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
e [] = Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
nelims Expr
e (I.IApply Named_ Expr
x Named_ Expr
y Named_ Expr
r : [Elim' (Named_ Expr)]
es) =
  Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Arg (Named_ Expr)
forall a. a -> Arg a
defaultArg Named_ Expr
r) [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Apply Arg (Named_ Expr)
arg : [Elim' (Named_ Expr)]
es) = do
  arg <- Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
reify Arg (Named_ Expr)
arg  -- This replaces the arg by _ if irrelevant
  dontShowImp <- not <$> showImplicitArguments
  let hd | Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Expr)
arg Bool -> Bool -> Bool
&& Bool
dontShowImp = Expr
e
         | Bool
otherwise                     = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e Arg (Named_ Expr)
arg
  nelims hd es
nelims Expr
e (I.Proj ProjOrigin
ProjPrefix QName
d : [Elim' (Named_ Expr)]
es)             = Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix Expr
e QName
d [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Proj ProjOrigin
o          QName
d : [Elim' (Named_ Expr)]
es) | Expr -> Bool
isSelf Expr
e  = Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [Elim' (Named_ Expr)]
es
                                    | Bool
otherwise =
  Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Arg (Named_ Expr)) -> Expr -> Arg (Named_ Expr)
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d)) [Elim' (Named_ Expr)]
es

{-# SPECIALIZE nelimsProjPrefix :: Expr -> QName -> [I.Elim' (Named_ Expr)] -> TCM Expr #-}
nelimsProjPrefix :: MonadReify m => Expr -> QName -> [I.Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix :: forall (m :: * -> *).
MonadReify m =>
Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix Expr
e QName
d [Elim' (Named_ Expr)]
es =
  Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
e) [Elim' (Named_ Expr)]
es

-- | If we are referencing the record from inside the record definition, we don't insert an
-- | A.App
isSelf :: Expr -> Bool
isSelf :: Expr -> Bool
isSelf = \case
  A.Var Name
n -> Name -> Bool
nameIsRecordName Name
n
  Expr
_ -> Bool
False

{-# SPECIALIZE elims :: Expr -> [I.Elim' Expr] -> TCM Expr #-}
-- | Drops hidden arguments unless --show-implicit.
elims :: MonadReify m => Expr -> [I.Elim' Expr] -> m Expr
elims :: forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
e = Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
e ([Elim' (Named_ Expr)] -> m Expr)
-> ([Elim' Expr] -> [Elim' (Named_ Expr)])
-> [Elim' Expr]
-> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Expr -> Elim' (Named_ Expr))
-> [Elim' Expr] -> [Elim' (Named_ Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Named_ Expr) -> Elim' Expr -> Elim' (Named_ Expr)
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Named_ Expr
forall a name. a -> Named name a
unnamed)

-- Omitting information ---------------------------------------------------

noExprInfo :: ExprInfo
noExprInfo :: ExprInfo
noExprInfo = Range -> ExprInfo
ExprRange Range
forall a. Range' a
noRange

-- Conditional reification to omit terms that are not shown --------------

{-# INLINE reifyWhenE #-}
reifyWhenE :: (Reify i, MonadReify m, Underscore (ReifiesTo i)) => Bool -> i -> m (ReifiesTo i)
reifyWhenE :: forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE Bool
True  i
i = i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify i
i
reifyWhenE Bool
False i
t = ReifiesTo i -> m (ReifiesTo i)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ReifiesTo i
forall a. Underscore a => a
underscore

-- Reification ------------------------------------------------------------

type MonadReify m =
  ( PureTCM m
  , MonadInteractionPoints m
  , MonadFresh NameId m
  )

class Reify i where
    type ReifiesTo i

    reify :: MonadReify m => i -> m (ReifiesTo i)

    --   @reifyWhen False@ should produce an 'underscore'.
    --   This function serves to reify hidden/irrelevant things.
    reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
_ = i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify

instance Reify Bool where
    type ReifiesTo Bool = Bool
    reify :: forall (m :: * -> *). MonadReify m => Bool -> m (ReifiesTo Bool)
reify = Bool -> m Bool
Bool -> m (ReifiesTo Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Reify Char where
    type ReifiesTo Char = Char
    reify :: forall (m :: * -> *). MonadReify m => Char -> m (ReifiesTo Char)
reify = Char -> m Char
Char -> m (ReifiesTo Char)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Reify Name where
    type ReifiesTo Name = Name
    reify :: forall (m :: * -> *). MonadReify m => Name -> m (ReifiesTo Name)
reify = Name -> m Name
Name -> m (ReifiesTo Name)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Reify Expr where
    type ReifiesTo Expr = Expr

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Expr -> m (ReifiesTo Expr)
reifyWhen = Bool -> Expr -> m (ReifiesTo Expr)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
    reify :: forall (m :: * -> *). MonadReify m => Expr -> m (ReifiesTo Expr)
reify = Expr -> m Expr
Expr -> m (ReifiesTo Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Reify MetaId where
    type ReifiesTo MetaId = Expr

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> MetaId -> m (ReifiesTo MetaId)
reifyWhen = Bool -> MetaId -> m (ReifiesTo MetaId)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
    reify :: forall (m :: * -> *).
MonadReify m =>
MetaId -> m (ReifiesTo MetaId)
reify MetaId
x = do
      b <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
      mvar <- lookupLocalMeta x
      let mi  = MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar
      let mi' = Info.MetaInfo
                 { metaRange :: Range
metaRange          = Closure Range -> Range
forall a. HasRange a => a -> Range
getRange (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
                 , metaScope :: ScopeInfo
metaScope          = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
                 , metaNumber :: Maybe MetaId
metaNumber         = if Bool
b then Maybe MetaId
forall a. Maybe a
Nothing else MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x
                 , metaNameSuggestion :: MetaNameSuggestion
metaNameSuggestion = if Bool
b then MetaNameSuggestion
"" else MetaInfo -> MetaNameSuggestion
miNameSuggestion MetaInfo
mi
                 , metaKind :: MetaKind
metaKind           =  MetaInstantiation -> MetaKind
metaInstantiationToMetaKind (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mvar)
                 }
          underscore = Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
mi'
      -- If we are printing a term that will be pasted into the user
      -- source, we turn all unsolved (non-interaction) metas into
      -- interaction points
      isInteractionMeta x >>= \case
        Maybe InteractionId
Nothing | Bool
b -> do
          ii <- Bool -> Range -> Maybe Nat -> m InteractionId
forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint Bool
False Range
forall a. Range' a
noRange Maybe Nat
forall a. Maybe a
Nothing
          connectInteractionPoint ii x
          return $ A.QuestionMark mi' ii
        Just InteractionId
ii | Bool
b -> m Expr
underscore
        Maybe InteractionId
Nothing     -> m Expr
underscore
        Just InteractionId
ii     -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> InteractionId -> Expr
A.QuestionMark MetaInfo
mi' InteractionId
ii
{-# SPECIALIZE reify :: MetaId -> TCM (ReifiesTo MetaId) #-}

instance Reify DisplayTerm where
  type ReifiesTo DisplayTerm = Expr

  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)
reifyWhen = Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify = \case
    DTerm' Term
v Elims
es       -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Expr -> [Elim' Expr] -> m Expr)
-> (m Expr, m [Elim' Expr]) -> m Expr
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> (m a, m b) -> m c
==<< (Bool -> Term -> m Expr
forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
False Term
v, Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify Elims
es)
    DDot'  Term
v Elims
es       -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Expr -> [Elim' Expr] -> m Expr)
-> (m Expr, m [Elim' Expr]) -> m Expr
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> (m a, m b) -> m c
==<< (Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v, Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify Elims
es)
    DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs      -> QName -> ConInfo -> [Arg Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> ConInfo -> [Arg Expr] -> m Expr
recOrCon (ConHead -> QName
conName ConHead
c) ConInfo
ci ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Arg DisplayTerm] -> m (ReifiesTo [Arg DisplayTerm])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Arg DisplayTerm] -> m (ReifiesTo [Arg DisplayTerm])
reify [Arg DisplayTerm]
vs
    DDef QName
f [Elim' DisplayTerm]
es         -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
f) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Elim' DisplayTerm] -> m (ReifiesTo [Elim' DisplayTerm])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim' DisplayTerm] -> m (ReifiesTo [Elim' DisplayTerm])
reify [Elim' DisplayTerm]
es
    DWithApp DisplayTerm
u List1 DisplayTerm
us Elims
es0 -> do
      (e, es) <- (DisplayTerm, List1 DisplayTerm)
-> m (ReifiesTo (DisplayTerm, List1 DisplayTerm))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(DisplayTerm, List1 DisplayTerm)
-> m (ReifiesTo (DisplayTerm, List1 DisplayTerm))
reify (DisplayTerm
u, List1 DisplayTerm
us)
      elims (A.WithApp noExprInfo e es) =<< reify es0
{-# SPECIALIZE reify :: DisplayTerm -> TCM (ReifiesTo DisplayTerm) #-}

{-# SPECIALIZE reifyDisplayForm :: QName -> I.Elims -> TCM A.Expr -> TCM A.Expr #-}
-- | @reifyDisplayForm f vs fallback@
--   tries to rewrite @f vs@ with a display form for @f@.
--   If successful, reifies the resulting display term,
--   otherwise, does @fallback@.
reifyDisplayForm :: MonadReify m => QName -> I.Elims -> m A.Expr -> m A.Expr
reifyDisplayForm :: forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
f Elims
es m Expr
fallback =
  m Bool -> m Expr -> m Expr -> m Expr
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled m Expr
fallback (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ {- else -}
    m (Maybe DisplayTerm)
-> m Expr -> (DisplayTerm -> m Expr) -> m Expr
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> Elims -> m (Maybe DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f Elims
es) m Expr
fallback DisplayTerm -> m Expr
DisplayTerm -> m (ReifiesTo DisplayTerm)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify

{-# SPECIALIZE reifyDisplayFormP :: QName -> A.Patterns -> A.Patterns -> TCM (QName, A.Patterns) #-}
-- | @reifyDisplayFormP@ tries to recursively
--   rewrite a lhs with a display form.
--
--   Note: we are not necessarily in the empty context upon entry!
reifyDisplayFormP ::
     forall m.
     MonadReify m
  => QName         -- ^ LHS head symbol
  -> A.Patterns    -- ^ Patterns to be taken into account to find display form.
  -> A.Patterns    -- ^ Remaining trailing patterns ("with patterns").
  -> m (QName, A.Patterns) -- ^ New head symbol and new patterns.
reifyDisplayFormP :: forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps Patterns
wps = do
  let fallback :: m (QName, Patterns)
fallback = (QName, Patterns) -> m (QName, Patterns)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Patterns
ps Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
wps)
  m Bool
-> m (QName, Patterns)
-> m (QName, Patterns)
-> m (QName, Patterns)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled m (QName, Patterns)
fallback (m (QName, Patterns) -> m (QName, Patterns))
-> m (QName, Patterns) -> m (QName, Patterns)
forall a b. (a -> b) -> a -> b
$ {- else -} do
    -- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt.
    -- Andreas, 2014-06-11  Issue 1177:
    -- I thought we need to add the placeholders for ps to the context,
    -- because otherwise displayForm will not raise the display term
    -- and we will have variable clashes.
    -- But apparently, it has no influence...
    -- Ulf, can you add an explanation?
    md <- -- addContext (replicate (length ps) "x") $
      QName -> Elims -> m (Maybe DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f (Elims -> m (Maybe DisplayTerm)) -> Elims -> m (Maybe DisplayTerm)
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Nat -> Elim' Term)
-> Patterns -> [Nat] -> Elims
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg (Named_ Pattern)
p Nat
i -> Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern)
p Arg (Named_ Pattern) -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
I.var Nat
i) Patterns
ps [Nat
0..]
    reportSLn "reify.display" 60 $
      "display form of " ++ prettyShow f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md
    case md of
      Just DisplayTerm
d  | DisplayTerm -> Bool
okDisplayForm DisplayTerm
d -> do
        -- In the display term @d@, @var i@ should be a placeholder
        -- for the @i@th pattern of @ps@.
        -- Andreas, 2014-06-11:
        -- Are we sure that @d@ did not use @var i@ otherwise?
        (f', ps', wps') <- Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d
        reportSDoc "reify.display" 70 $ do
          doc <- prettyA $ SpineLHS empty f' (ps' ++ wps' ++ wps)
          return $ vcat
            [ "rewritten lhs to"
            , "  lhs' = " <+> doc
            ]
        reifyDisplayFormP f' ps' (wps' ++ wps)
      Maybe DisplayTerm
_ -> do
        MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.display" Nat
70 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"display form absent or not valid as lhs"
        m (QName, Patterns)
fallback
  where
    -- Andreas, 2015-05-03: Ulf, please comment on what
    -- is the idea behind okDisplayForm.
    -- Ulf, 2016-04-15: okDisplayForm should return True if the display form
    -- can serve as a valid left-hand side. That means checking that it is a
    -- defined name applied to valid lhs eliminators (projections or
    -- applications to constructor patterns).
    okDisplayForm :: DisplayTerm -> Bool
    okDisplayForm :: DisplayTerm -> Bool
okDisplayForm = \case
      DWithApp DisplayTerm
d List1 DisplayTerm
ds Elims
es ->
        DisplayTerm -> Bool
okDisplayForm DisplayTerm
d Bool -> Bool -> Bool
&& (DisplayTerm -> Bool) -> List1 DisplayTerm -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DisplayTerm -> Bool
okDisplayTerm List1 DisplayTerm
ds  Bool -> Bool -> Bool
&& (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okToDropE Elims
es
        -- Andreas, 2016-05-03, issue #1950.
        -- We might drop trailing hidden trivial (=variable) patterns.
      DTerm' (I.Def QName
f Elims
es') Elims
es -> (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
es' Bool -> Bool -> Bool
&& (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
es
      DDef QName
f [Elim' DisplayTerm]
es               -> (Elim' DisplayTerm -> Bool) -> [Elim' DisplayTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' DisplayTerm -> Bool
okDElim [Elim' DisplayTerm]
es
      DDot'{}                 -> Bool
False
      DCon{}                  -> Bool
False
      DTerm'{}                -> Bool
False

    okDisplayTerm :: DisplayTerm -> Bool
    okDisplayTerm :: DisplayTerm -> Bool
okDisplayTerm = \case
      DTerm' Term
v Elims
es -> Elims -> Bool
forall a. Null a => a -> Bool
null Elims
es Bool -> Bool -> Bool
&& Term -> Bool
okTerm Term
v
      DDot'{}     -> Bool
True
      DCon{}      -> Bool
True
      DDef{}      -> Bool
False
      DWithApp{}  -> Bool
False

    okDElim :: Elim' DisplayTerm -> Bool
    okDElim :: Elim' DisplayTerm -> Bool
okDElim (I.IApply DisplayTerm
x DisplayTerm
y DisplayTerm
r) = DisplayTerm -> Bool
okDisplayTerm DisplayTerm
r
    okDElim (I.Apply Arg DisplayTerm
v) = DisplayTerm -> Bool
okDisplayTerm (DisplayTerm -> Bool) -> DisplayTerm -> Bool
forall a b. (a -> b) -> a -> b
$ Arg DisplayTerm -> DisplayTerm
forall e. Arg e -> e
unArg Arg DisplayTerm
v
    okDElim I.Proj{}    = Bool
True

    okToDropE :: Elim' Term -> Bool
    okToDropE :: Elim' Term -> Bool
okToDropE (I.Apply Arg Term
v) = Arg Term -> Bool
okToDrop Arg Term
v
    okToDropE I.Proj{}    = Bool
False
    okToDropE (I.IApply Term
x Term
y Term
r) = Bool
False

    okToDrop :: Arg I.Term -> Bool
    okToDrop :: Arg Term -> Bool
okToDrop Arg Term
arg = Arg Term -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg Term
arg Bool -> Bool -> Bool
&& case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg of
      I.Var Nat
_ []   -> Bool
True
      I.DontCare{} -> Bool
True  -- no matching on irrelevant things.  __IMPOSSIBLE__ anyway?
      I.Level{}    -> Bool
True  -- no matching on levels. __IMPOSSIBLE__ anyway?
      Term
_ -> Bool
False

    okArg :: Arg I.Term -> Bool
    okArg :: Arg Term -> Bool
okArg = Term -> Bool
okTerm (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg

    okElim :: Elim' I.Term -> Bool
    okElim :: Elim' Term -> Bool
okElim (I.IApply Term
x Term
y Term
r) = Term -> Bool
okTerm Term
r
    okElim (I.Apply Arg Term
a) = Arg Term -> Bool
okArg Arg Term
a
    okElim I.Proj{}  = Bool
True

    okTerm :: I.Term -> Bool
    okTerm :: Term -> Bool
okTerm (I.Var Nat
_ []) = Bool
True
    okTerm (I.Con ConHead
c ConInfo
ci Elims
vs) = (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
    okTerm (I.Def QName
x []) = QName -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Bool) -> QName -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> QName
qnameToConcrete QName
x -- Handling wildcards in display forms
    okTerm Term
_            = Bool
False

    -- Flatten a dt into (parentName, parentElims, withArgs).
    flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
    flattenWith :: DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith (DWithApp DisplayTerm
d List1 DisplayTerm
ds1 Elims
es2) =
      let (QName
f, [Elim' DisplayTerm]
es, [Elim' DisplayTerm]
ds0) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith DisplayTerm
d
      in  (QName
f, [Elim' DisplayTerm]
es, [Elim' DisplayTerm]
ds0 [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ (DisplayTerm -> Elim' DisplayTerm)
-> [DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (DisplayTerm -> Arg DisplayTerm)
-> DisplayTerm
-> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayTerm -> Arg DisplayTerm
forall a. a -> Arg a
defaultArg) (List1 DisplayTerm -> [Item (List1 DisplayTerm)]
forall l. IsList l => l -> [Item l]
List1.toList List1 DisplayTerm
ds1) [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es2)
    flattenWith (DDef QName
f [Elim' DisplayTerm]
es) = (QName
f, [Elim' DisplayTerm]
es, [])     -- .^ hacky, but we should only hit this when printing debug info
    flattenWith (DTerm' (I.Def QName
f Elims
es') Elims
es) = (QName
f, (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) (Elims -> [Elim' DisplayTerm]) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es, [])
    flattenWith DisplayTerm
_ = (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
forall a. HasCallStack => a
__IMPOSSIBLE__

    displayLHS
      :: MonadReify m
      => A.Patterns   -- Patterns to substituted into display term.
      -> DisplayTerm  -- Display term.
      -> m (QName, A.Patterns, A.Patterns)  -- New head, patterns, with-patterns.
    displayLHS :: MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d = do
        let (QName
f, [Elim' DisplayTerm]
vs, [Elim' DisplayTerm]
es) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith DisplayTerm
d
        ps  <- (Elim' DisplayTerm -> m (Arg (Named_ Pattern)))
-> [Elim' DisplayTerm] -> m Patterns
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat [Elim' DisplayTerm]
vs
        wps <- mapM (updateNamedArg (A.WithP empty) <.> elimToPat) es
        return (f, ps, wps)
      where
        argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern)
        argToPat :: MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat Arg DisplayTerm
arg = (DisplayTerm -> m (Named_ Pattern))
-> Arg DisplayTerm -> m (Arg (Named_ Pattern))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse MonadReify m => DisplayTerm -> m (Named_ Pattern)
DisplayTerm -> m (Named_ Pattern)
termToPat Arg DisplayTerm
arg

        elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern)
        elimToPat :: MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat (I.IApply DisplayTerm
_ DisplayTerm
_ DisplayTerm
r) = MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat (ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo DisplayTerm
r)
        elimToPat (I.Apply Arg DisplayTerm
arg) = MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat Arg DisplayTerm
arg
        elimToPat (I.Proj ProjOrigin
o QName
d)  = Arg (Named_ Pattern) -> m (Arg (Named_ Pattern))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Arg (Named_ Pattern) -> m (Arg (Named_ Pattern)))
-> Arg (Named_ Pattern) -> m (Arg (Named_ Pattern))
forall a b. (a -> b) -> a -> b
$ Pattern -> Arg (Named_ Pattern)
forall a. a -> NamedArg a
defaultNamedArg (Pattern -> Arg (Named_ Pattern))
-> Pattern -> Arg (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
o (AmbiguousQName -> Pattern) -> AmbiguousQName -> Pattern
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d

        -- Substitute variables in display term by patterns.
        termToPat :: MonadReify m => DisplayTerm -> m (Named_ A.Pattern)

        -- Main action HERE:
        termToPat :: MonadReify m => DisplayTerm -> m (Named_ Pattern)
termToPat (DTerm (I.Var Nat
n [])) =
          Named_ Pattern -> m (Named_ Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Named_ Pattern -> m (Named_ Pattern))
-> Named_ Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern) -> Named_ Pattern
forall e. Arg e -> e
unArg (Arg (Named_ Pattern) -> Named_ Pattern)
-> Arg (Named_ Pattern) -> Named_ Pattern
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern)
-> Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern)
forall a. a -> Maybe a -> a
fromMaybe Arg (Named_ Pattern)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern))
-> Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ Patterns
ps Patterns -> Nat -> Maybe (Arg (Named_ Pattern))
forall a. [a] -> Nat -> Maybe a
!!! Nat
n

        termToPat (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)          = (Pattern -> Named_ Pattern) -> m Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (m Pattern -> m (Named_ Pattern))
-> (Pattern -> m Pattern) -> Pattern -> m (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> m Pattern
forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP (Pattern -> m (Named_ Pattern)) -> m Pattern -> m (Named_ Pattern)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
           ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ci PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg DisplayTerm -> m (Arg (Named_ Pattern)))
-> [Arg DisplayTerm] -> m Patterns
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat [Arg DisplayTerm]
vs

        termToPat (DTerm' (I.Con ConHead
c ConInfo
ci Elims
vs) Elims
es) = (Pattern -> Named_ Pattern) -> m Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (m Pattern -> m (Named_ Pattern))
-> (Pattern -> m Pattern) -> Pattern -> m (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> m Pattern
forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP (Pattern -> m (Named_ Pattern)) -> m Pattern -> m (Named_ Pattern)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
           ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ci PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
             (Elim' Term -> m (Arg (Named_ Pattern))) -> Elims -> m Patterns
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat (Elim' DisplayTerm -> m (Arg (Named_ Pattern)))
-> (Elim' Term -> Elim' DisplayTerm)
-> Elim' Term
-> m (Arg (Named_ Pattern))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) (Elims
vs Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)

        termToPat (DTerm (I.Def QName
_ [])) = Named_ Pattern -> m (Named_ Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Named_ Pattern -> m (Named_ Pattern))
-> Named_ Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        termToPat (DDef QName
_ [])          = Named_ Pattern -> m (Named_ Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Named_ Pattern -> m (Named_ Pattern))
-> Named_ Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange

        termToPat (DTerm (I.Lit Literal
l))    = Named_ Pattern -> m (Named_ Pattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Named_ Pattern -> m (Named_ Pattern))
-> Named_ Pattern -> m (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
patNoRange Literal
l

        termToPat (DDot' Term
v Elims
es) =
          Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern)
-> (Expr -> Pattern) -> Expr -> Named_ Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Named_ Pattern) -> m Expr -> m (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Expr -> [Elim' Expr] -> m Expr)
-> (m Expr, m [Elim' Expr]) -> m Expr
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> (m a, m b) -> m c
==<< (MonadReify m => Term -> m Expr
Term -> m Expr
termToExpr Term
v, Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify Elims
es)

        termToPat DisplayTerm
v =
          Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern)
-> (Expr -> Pattern) -> Expr -> Named_ Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Named_ Pattern) -> m Expr -> m (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DisplayTerm -> m (ReifiesTo DisplayTerm)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify DisplayTerm
v

        len :: Nat
len = Patterns -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Patterns
ps

        argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
        argsToExpr :: MonadReify m => Args -> m [Arg Expr]
argsToExpr = (Arg Term -> m (Arg Expr)) -> Args -> m [Arg Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Term -> m Expr) -> Arg Term -> m (Arg Expr)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse MonadReify m => Term -> m Expr
Term -> m Expr
termToExpr)

        -- TODO: restructure this to avoid having to repeat the code for reify
        termToExpr :: MonadReify m => Term -> m A.Expr
        termToExpr :: MonadReify m => Term -> m Expr
termToExpr Term
v = do
          MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.display" Nat
60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"termToExpr " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ Term -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Term
v
          -- After unSpine, a Proj elimination is __IMPOSSIBLE__!
          case Term -> Term
unSpine Term
v of
            I.Con ConHead
c ConInfo
ci Elims
es -> do
              let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
              Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c))) ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Args -> m [Arg Expr]
MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
            I.Def QName
f Elims
es -> do
              let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
              Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (QName -> Expr
A.Def QName
f) ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Args -> m [Arg Expr]
MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
            I.Var Nat
n Elims
es -> do
              let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
              -- Andreas, 2014-06-11  Issue 1177
              -- due to β-normalization in substitution,
              -- even the pattern variables @n < len@ can be
              -- applied to some args @vs@.
              e <- if Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
len
                   then Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Pattern -> Expr
patternToExpr (Pattern -> Expr) -> Pattern -> Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg (Arg (Named_ Pattern) -> Pattern)
-> Arg (Named_ Pattern) -> Pattern
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern) -> Patterns -> Nat -> Arg (Named_ Pattern)
forall a. a -> [a] -> Nat -> a
indexWithDefault Arg (Named_ Pattern)
forall a. HasCallStack => a
__IMPOSSIBLE__ Patterns
ps Nat
n
                   else Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Nat -> Term
I.var (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
len))
              apps e =<< argsToExpr vs
            Term
_ -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall a. Underscore a => a
underscore

instance Reify Literal where
  type ReifiesTo Literal = Expr

  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Literal -> m (ReifiesTo Literal)
reifyWhen = Bool -> Literal -> m (ReifiesTo Literal)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *).
MonadReify m =>
Literal -> m (ReifiesTo Literal)
reify Literal
l = Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty Literal
l; {-# INLINE reify #-}

instance Reify Term where
  type ReifiesTo Term = Expr

  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Term -> m (ReifiesTo Term)
reifyWhen = Bool -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v = Bool -> Term -> m Expr
forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
True Term
v; {-# INLINE reify #-}

{-# SPECIALIZE reifyPathPConstAsPath :: QName -> Elims -> TCM (QName, Elims) #-}
reifyPathPConstAsPath :: MonadReify m => QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath :: forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x es :: Elims
es@[I.Apply Arg Term
l, I.Apply Arg Term
t, I.Apply Arg Term
lhs, I.Apply Arg Term
rhs] = do
   MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.def" Nat
100 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"reifying def path " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ (QName, Elims) -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show (QName
x,Elims
es)
   mpath  <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPath
   mpathp <- getBuiltinName' builtinPathP
   let fallback = (QName, Elims) -> m (QName, Elims)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,Elims
es)
   case (,) <$> mpath <*> mpathp of
     Just (QName
path,QName
pathp) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
pathp -> do
       let a :: Maybe Term
a = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t of
                I.Lam ArgInfo
_ (NoAbs MetaNameSuggestion
_ Term
b)    -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
b
                I.Lam ArgInfo
_ (Abs   MetaNameSuggestion
_ Term
b)
                  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Nat
0 Nat -> Term -> Bool
forall a. Free a => Nat -> a -> Bool
`freeIn` Term
b -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Impossible -> Term -> Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible Term
b)
                Term
_                      -> Maybe Term
forall a. Maybe a
Nothing
       case Maybe Term
a of
         Just Term
a -> (QName, Elims) -> m (QName, Elims)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
path, [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
l, Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
a), Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
lhs, Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
rhs])
         Maybe Term
Nothing -> m (QName, Elims)
fallback
     Maybe (QName, QName)
_ -> m (QName, Elims)
fallback
reifyPathPConstAsPath QName
x Elims
es = (QName, Elims) -> m (QName, Elims)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,Elims
es)

{-# SPECIALIZE tryReifyAsLetBinding :: Term -> TCM Expr -> TCM Expr #-}
-- | Check if the term matches an existing let-binding, in that case use the corresponding variable,
--   otherwise reify using the continuation.
tryReifyAsLetBinding :: MonadReify m => Term -> m Expr -> m Expr
tryReifyAsLetBinding :: forall (m :: * -> *). MonadReify m => Term -> m Expr -> m Expr
tryReifyAsLetBinding Term
v m Expr
fallback = m Bool -> m Expr -> m Expr -> m Expr
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC ((TCEnv -> Bool) -> m Bool) -> (TCEnv -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (TCEnv -> Bool) -> TCEnv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> Bool
envFoldLetBindings) m Expr
fallback (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
  letBindings <- do
    binds  <- (TCEnv -> [(Name, Open LetBinding)]) -> m [(Name, Open LetBinding)]
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (Map Name (Open LetBinding) -> [(Name, Open LetBinding)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map Name (Open LetBinding) -> [(Name, Open LetBinding)])
-> (TCEnv -> Map Name (Open LetBinding))
-> TCEnv
-> [(Name, Open LetBinding)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> Map Name (Open LetBinding)
envLetBindings)
    opened <- forM binds $ \ (Name
name, Open LetBinding
open) -> (,Name
name) (LetBinding -> (LetBinding, Name))
-> m LetBinding -> m (LetBinding, Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open LetBinding -> m LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
open
    return [ (body, name) | (LetBinding UserWritten body _, name) <- opened, not $ isNoName name ]  -- Only fold user-written lets
  matchingBindings <- filterM (\(Term, Name)
t -> Term
-> Term
-> (Term -> Term -> m Bool)
-> (Term -> Term -> m Bool)
-> m Bool
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality Term
v ((Term, Name) -> Term
forall a b. (a, b) -> a
fst (Term, Name)
t) (\Term
_ Term
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) (\Term
_ Term
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)) letBindings
  case matchingBindings of
    (Term
_, Name
name) : [(Term, Name)]
_ -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
name
    []            -> m Expr
fallback

{-# SPECIALIZE reifyTerm :: Bool -> Term -> TCM Expr #-}
reifyTerm ::
      MonadReify m
   => Bool           -- ^ Try to expand away anonymous definitions?
   -> Term
   -> m Expr
reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
expandAnonDefs0 Term
v0 = Term -> m Expr -> m Expr
forall (m :: * -> *). MonadReify m => Term -> m Expr -> m Expr
tryReifyAsLetBinding Term
v0 (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
  -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
  metasBare <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
  reportSDoc "reify.term" 80 $ pure $ "reifyTerm v0 = " <+> pretty v0
  v <- instantiate v0 >>= \case
    I.MetaV MetaId
x Elims
_ | Bool
metasBare -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x []
    Term
v -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  reportSDoc "reify.term" 80 $ pure $ "reifyTerm v = " <+> pretty v
  -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
  -- (i.e. when we don't care about nice printing)
  expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled

  -- Andreas, 2016-07-21 if --postfix-projections
  -- then we print system-generated projections as postfix, else prefix.
  havePfp <- optPostfixProjections <$> pragmaOptions

  -- Amy, 2024-01-07: postfix and system projections should still be
  -- turned into head symbols *if* they have display forms attached.
  hasDisplay <- liftReduce $ unKleisli hasDisplayForms
  let
    prefixize :: ProjOrigin -> QName -> Bool
    prefixize ProjOrigin
orig QName
name = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
      [ if Bool
havePfp then ProjOrigin
orig ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPrefix else ProjOrigin
orig ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPostfix
      , QName -> Bool
isOperator QName
name
          -- Andreas, 2024-06-13, issue #7318:
          -- print e.g. G .|_| as | G |
      , QName -> Bool
hasDisplay QName
name
      ]
  reportSDoc "reify.term" 80 $ pure $ "reifyTerm (unSpine v) = " <+> pretty (unSpine' prefixize v)

  case unSpine' prefixize v of
    -- Hack to print generalized field projections with nicer names. Should
    -- only show up in errors. Check the spined form!
    Term
_ | I.Var Nat
n (I.Proj ProjOrigin
_ QName
p : Elims
es) <- Term
v,
        Just MetaNameSuggestion
name <- QName -> Maybe MetaNameSuggestion
getGeneralizedFieldName QName
p -> do
      let fakeName :: Name
fakeName = (QName -> Name
qnameName QName
p) {nameConcrete = C.simpleName name} -- TODO: infix names!?
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
fakeName) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify Elims
es
    I.Var Nat
n Elims
es -> do
      x <- m Name -> m (Maybe Name) -> m Name
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ (MetaNameSuggestion -> m Name) -> MetaNameSuggestion -> m Name
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"@" MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ Nat -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Nat
n) (m (Maybe Name) -> m Name) -> m (Maybe Name) -> m Name
forall a b. (a -> b) -> a -> b
$ Nat -> m (Maybe Name)
forall (m :: * -> *).
(Applicative m, MonadDebug m, MonadTCEnv m) =>
Nat -> m (Maybe Name)
nameOfBV' Nat
n
      elims (A.Var x) =<< reify es
    I.Def QName
x Elims
es -> do
      MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
reportSDoc MetaNameSuggestion
"reify.def" Nat
80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reifying def" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
      (x, es) <- QName -> Elims -> m (QName, Elims)
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x Elims
es
      reifyDisplayForm x es $ reifyDef expandAnonDefs x es

    I.Con ConHead
c ConInfo
ci Elims
es -> do

      -- If the origin is a record expression, print a record expression.
      if ConInfo -> Bool
isRecOrigin ConInfo
ci then RecInfo -> Maybe (QName, RecordData) -> m Expr
recordExpression (ConInfo -> RecInfo
conOriginToRecInfo ConInfo
ci) Maybe (QName, RecordData)
forall a. Maybe a
Nothing else do
        QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
x m (Maybe (QName, RecordData))
-> (Maybe (QName, RecordData) -> m Expr) -> m Expr
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

          -- If it is a generated constructor, print a record expression.
          Just (QName
r, RecordData
def) | Bool -> Bool
not (RecordData -> Bool
_recNamedCon RecordData
def) -> RecInfo -> Maybe (QName, RecordData) -> m Expr
recordExpression (Range -> RecInfo
recInfoBrace Range
forall a. Range' a
noRange) (Maybe (QName, RecordData) -> m Expr)
-> Maybe (QName, RecordData) -> m Expr
forall a b. (a -> b) -> a -> b
$ (QName, RecordData) -> Maybe (QName, RecordData)
forall a. a -> Maybe a
Just (QName
r, RecordData
def)

          -- Otherwise, print a constructor application.
          Maybe (QName, RecordData)
_ -> m Expr
constructorApplication
      where
        x :: QName
x = ConHead -> QName
conName ConHead
c

        recordExpression :: RecInfo -> Maybe (QName, RecordData) -> m Expr
recordExpression RecInfo
ri Maybe (QName, RecordData)
mrdef = do
          (r, def) <- m (QName, RecordData)
-> ((QName, RecordData) -> m (QName, RecordData))
-> Maybe (QName, RecordData)
-> m (QName, RecordData)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((QName, RecordData)
-> Maybe (QName, RecordData) -> (QName, RecordData)
forall a. a -> Maybe a -> a
fromMaybe (QName, RecordData)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (QName, RecordData) -> (QName, RecordData))
-> m (Maybe (QName, RecordData)) -> m (QName, RecordData)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
x) (QName, RecordData) -> m (QName, RecordData)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, RecordData)
mrdef
          showImp <- showImplicitArguments
          let keep (Dom' Term Name
a, Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| Dom' Term Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term Name
a
          A.Rec ri
            . map (Left . uncurry FieldAssignment . mapFst unDom)
            . filter keep
            . zip (recordFieldNames def)
            . map unArg
            <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims es)

        constructorApplication :: m Expr
constructorApplication = QName -> Elims -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
es (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
          def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          let Constructor {conPars = np} = theDef def
          -- if we are the the module that defines constructor x
          -- then we have to drop at least the n module parameters
          n <- getDefFreeVars x
          -- the number of parameters is greater (if the data decl has
          -- extra parameters) or equal (if not) to n
          when (n > np) __IMPOSSIBLE__
          let h = AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
x)
          if null es
            then return h
            else do
              es <- reify $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
              -- Andreas, 2012-04-20: do not reify parameter arguments of constructor
              -- if the first regular constructor argument is hidden
              -- we turn it into a named argument, in order to avoid confusion
              -- with the parameter arguments which can be supplied in abstract syntax
              --
              -- Andreas, 2012-09-17: this does not remove all sources of confusion,
              -- since parameters could have the same name as regular arguments
              -- (see for example the parameter {i} to Data.Star.Star, which is also
              -- the first argument to the cons).
              -- @data Star {i}{I : Set i} ... where cons : {i :  I} ...@
              if np == 0
                then apps h es
                else do
                  -- Get name of first argument from type of constructor.
                  -- Here, we need the reducing version of @telView@
                  -- because target of constructor could be a definition
                  -- expanding into a function type.  See test/succeed/NameFirstIfHidden.agda.
                  TelV tel _ <- telView (defType def)
                  let (pars, rest) = splitAt np $ telToList tel
                  case rest of
                    -- Andreas, 2012-09-18
                    -- If the first regular constructor argument is hidden,
                    -- we keep the parameters to avoid confusion.
                    (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : [Dom (MetaNameSuggestion, Type)]
_) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
                      let us :: [Arg Expr]
us = [Dom (MetaNameSuggestion, Type)]
-> (Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Nat
-> [Dom (MetaNameSuggestion, Type)]
-> [Dom (MetaNameSuggestion, Type)]
forall a. Nat -> [a] -> [a]
drop Nat
n [Dom (MetaNameSuggestion, Type)]
pars) ((Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr])
-> (Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
forall a b. (a -> b) -> a -> b
$ \(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}) ->
                            -- setRelevance Relevant $
                            Arg Expr -> Arg Expr
forall a. LensHiding a => a -> a
hideOrKeepInstance (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Expr
forall a. Underscore a => a
underscore
                      Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h ([Arg Expr] -> m Expr) -> [Arg Expr] -> m Expr
forall a b. (a -> b) -> a -> b
$ [Arg Expr]
us [Arg Expr] -> [Arg Expr] -> [Arg Expr]
forall a. [a] -> [a] -> [a]
++ [Arg Expr]
es -- Note: unless --show-implicit, @apps@ will drop @us@.
                    -- otherwise, we drop all parameters
                    [Dom (MetaNameSuggestion, Type)]
_ -> Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es

--    I.Lam info b | isAbsurdBody b -> return $ A. AbsurdLam noExprInfo $ getHiding info
    I.Lam ArgInfo
info Abs Term
b    -> do
      (x,e) <- Abs Term -> m (ReifiesTo (Abs Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Abs Term -> m (ReifiesTo (Abs Term))
reify Abs Term
b
      -- #4160: Hacky solution: if --show-implicit, treat all lambdas as user-written. This will
      -- prevent them from being dropped by AbstractToConcrete (where we don't have easy access to
      -- the --show-implicit flag.
      info <- ifM showImplicitArguments (return $ setOrigin UserWritten info) (return info)
      return $ A.Lam exprNoRange (mkDomainFree $ unnamedArg info $ mkBinder_ x) e
      -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
    I.Lit Literal
l        -> Literal -> m (ReifiesTo Literal)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Literal -> m (ReifiesTo Literal)
reify Literal
l
    I.Level Level
l      -> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
l
    I.Pi Dom Type
a Abs Type
b       -> case Abs Type
b of
        NoAbs MetaNameSuggestion
_ Type
b'
          | Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Type
a, Bool -> Bool
not (Dom Type -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a) -> (Arg Expr -> Expr -> Expr) -> (Arg Expr, Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun (ExprInfo -> Arg Expr -> Expr -> Expr)
-> ExprInfo -> Arg Expr -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo
noExprInfo) ((Arg Expr, Expr) -> Expr) -> m (Arg Expr, Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom Type, Type) -> m (ReifiesTo (Dom Type, Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(Dom Type, Type) -> m (ReifiesTo (Dom Type, Type))
reify (Dom Type
a, Type
b')
            -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
            -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
            -- and (b) the name of the binder might matter.
            -- See issue 951 (a) and 952 (b).
            --
            -- Amy, 2022-09-05: Can't be finite either, since otherwise
            -- we say ".(IsOne φ) → A ≠ .(IsOne φ) → A" with no
            -- indication of which is finite and which isn't
          | Bool
otherwise   -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom Type -> m (ReifiesTo (Dom Type))
reify Dom Type
a
        Abs Type
b               -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          m Bool -> m (Arg Expr) -> m (Arg Expr) -> m (Arg Expr)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Dom Type -> Type -> m Bool
forall {m :: * -> *} {a} {t}.
(MonadTCEnv m, Free a, Free t) =>
t -> a -> m Bool
domainFree Dom Type
a (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b))
            {- then -} (Arg Expr -> m (Arg Expr)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m (Arg Expr)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) Expr
forall a. Underscore a => a
underscore)
            {- else -} (Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom Type -> m (ReifiesTo (Dom Type))
reify Dom Type
a)
      where
        mkPi :: Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg ArgInfo
info Expr
a') = m Bool -> m Expr -> m Expr -> m Expr
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ArgInfo -> m Bool
forall (m :: * -> *). MonadReify m => ArgInfo -> m Bool
skipGeneralizedParameter ArgInfo
info) ((Name, Expr) -> Expr
forall a b. (a, b) -> b
snd ((Name, Expr) -> Expr) -> m (Name, Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type -> m (ReifiesTo (Abs Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Abs Type -> m (ReifiesTo (Abs Type))
reify Abs Type
b) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
          tac <- Maybe (Ranged Expr) -> TacticAttribute' Expr
forall a. Maybe (Ranged a) -> TacticAttribute' a
TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute' Expr)
-> m (Maybe (Ranged Expr)) -> m (TacticAttribute' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do (Term -> m (Ranged Expr)) -> Maybe Term -> m (Maybe (Ranged Expr))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Range -> Expr -> Ranged Expr
forall a. Range -> a -> Ranged a
Ranged Range
forall a. Range' a
noRange (Expr -> Ranged Expr)
-> (Term -> m Expr) -> Term -> m (Ranged Expr)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify) (Maybe Term -> m (Maybe (Ranged Expr)))
-> Maybe Term -> m (Maybe (Ranged Expr))
forall a b. (a -> b) -> a -> b
$ Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a
          (x, b) <- reify b
          let xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> List1
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
 -> List1
      (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> List1
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
 -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged MetaNameSuggestion))
-> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
forall name a. Maybe name -> a -> Named name a
Named (Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall t e.
Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
domName Dom Type
a) (Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x
          return $ A.Pi noExprInfo
            (singleton $ TBind noRange (TypedBindingInfo tac (domIsFinite a)) xs a')
            b
        -- We can omit the domain type if it doesn't have any free variables
        -- and it's mentioned in the target type.
        domainFree :: t -> a -> m Bool
domainFree t
a a
b = do
          df <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintDomainFreePi
          return $ df && freeIn 0 b && closed a

        skipGeneralizedParameter :: MonadReify m => ArgInfo -> m Bool
        skipGeneralizedParameter :: forall (m :: * -> *). MonadReify m => ArgInfo -> m Bool
skipGeneralizedParameter ArgInfo
info = (Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
forall (m :: * -> *). HasOptions m => m Bool
showGeneralizedArguments) m Bool -> (Bool -> Bool) -> m Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Bool -> Bool -> Bool
&& (ArgInfo -> Origin
argInfoOrigin ArgInfo
info Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Generalization))

    I.Sort Sort
s     -> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s
    I.MetaV MetaId
x Elims
es -> do
          x' <- MetaId -> m (ReifiesTo MetaId)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
MetaId -> m (ReifiesTo MetaId)
reify MetaId
x

          es' <- reify es

          mv <- lookupLocalMeta x
          (msub1,meta_tel,msub2) <- do
            local_chkpt <- viewTC eCurrentCheckpoint
            (chkpt, tel, msub2) <- enterClosure mv $ \ Range
_ ->
                               (,,) (CheckpointId
 -> Tele (Dom Type)
 -> Maybe (Substitution' Term)
 -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m CheckpointId
-> m (Tele (Dom Type)
      -> Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv CheckpointId -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
                                    m (Tele (Dom Type)
   -> Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Tele (Dom Type))
-> m (Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
                                    m (Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Lens' TCEnv (Maybe (Substitution' Term))
-> m (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
eCheckpoints ((Map CheckpointId (Substitution' Term)
  -> f (Map CheckpointId (Substitution' Term)))
 -> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> Map CheckpointId (Substitution' Term)
    -> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
     (Map CheckpointId (Substitution' Term))
     (Maybe (Substitution' Term))
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key CheckpointId
local_chkpt)
            (,,) <$> viewTC (eCheckpoints . key chkpt) <*> pure tel <*> pure msub2

          opt_show_ids <- showIdentitySubstitutions
          let
              addNames []    [Elim' a]
es = (Elim' a -> Elim' (Named name a))
-> [Elim' a] -> [Elim' (Named name a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Named name a) -> Elim' a -> Elim' (Named name a)
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Named name a
forall a name. a -> Named name a
unnamed) [Elim' a]
es
              addNames [name]
_     [] = []
              addNames [name]
xs     (I.Proj{} : [Elim' a]
_) = [Elim' (Named name a)]
forall a. HasCallStack => a
__IMPOSSIBLE__
              addNames [name]
xs     (I.IApply a
x a
y a
r : [Elim' a]
es) =
                -- Needs to be I.Apply so it can have an Origin field.
                [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs (Arg a -> Elim' a
forall a. Arg a -> Elim' a
I.Apply (a -> Arg a
forall a. a -> Arg a
defaultArg a
r) Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
: [Elim' a]
es)
              addNames (name
x:[name]
xs) (I.Apply Arg a
arg : [Elim' a]
es) =
                Arg (Named name a) -> Elim' (Named name a)
forall a. Arg a -> Elim' a
I.Apply (Maybe name -> a -> Named name a
forall name a. Maybe name -> a -> Named name a
Named (name -> Maybe name
forall a. a -> Maybe a
Just name
x) (a -> Named name a) -> Arg a -> Arg (Named name a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Origin -> Arg a -> Arg a
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Substitution Arg a
arg)) Elim' (Named name a)
-> [Elim' (Named name a)] -> [Elim' (Named name a)]
forall a. a -> [a] -> [a]
: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs [Elim' a]
es

              p = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
              applyPerm Permutation
p [a]
vs = Permutation -> [a] -> [a]
forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP ([a] -> Nat
forall a. Sized a => a -> Nat
size [a]
vs) Permutation
p) [a]
vs

              names = (MetaNameSuggestion -> WithOrigin (Ranged MetaNameSuggestion))
-> [MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)]
forall a b. (a -> b) -> [a] -> [b]
map (Origin
-> Ranged MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged MetaNameSuggestion
 -> WithOrigin (Ranged MetaNameSuggestion))
-> (MetaNameSuggestion -> Ranged MetaNameSuggestion)
-> MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaNameSuggestion -> Ranged MetaNameSuggestion
forall a. a -> Ranged a
unranged) ([MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)])
-> [MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)]
forall a b. (a -> b) -> a -> b
$ Permutation
p Permutation -> [MetaNameSuggestion] -> [MetaNameSuggestion]
forall a. Permutation -> [a] -> [a]
`applyPerm` Tele (Dom Type) -> [MetaNameSuggestion]
teleNames Tele (Dom Type)
meta_tel
              named_es' = [WithOrigin (Ranged MetaNameSuggestion)]
-> [Elim' Expr] -> [Elim' (Named_ Expr)]
forall {name} {a}. [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [WithOrigin (Ranged MetaNameSuggestion)]
names [Elim' Expr]
es'

              dropIdentitySubs Substitution' Term
sub_local2G Substitution' Term
sub_tel2G =
                 let
                     args_G :: Args
args_G = Substitution' (SubstArg Args) -> Args -> Args
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Args)
sub_tel2G (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Permutation
p Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
`applyPerm` (Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
meta_tel :: [Arg Term])
                     es_G :: Elims
es_G = Substitution' Term
Substitution' (SubstArg Elims)
sub_local2G Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Elims
es
                     sameVar :: Arg a -> Elim' a -> Bool
sameVar Arg a
x (I.Apply Arg a
y) = Maybe Nat -> Bool
forall a. Maybe a -> Bool
isJust Maybe Nat
xv Bool -> Bool -> Bool
&& Maybe Nat
xv Maybe Nat -> Maybe Nat -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (Arg a -> a
forall e. Arg e -> e
unArg Arg a
y)
                      where
                       xv :: Maybe Nat
xv = a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (a -> Maybe Nat) -> a -> Maybe Nat
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
x
                     sameVar Arg a
_ Elim' a
_ = Bool
False
                     dropArg :: [Bool]
dropArg = Nat -> [Bool] -> [Bool]
forall a. Nat -> [a] -> [a]
take ([WithOrigin (Ranged MetaNameSuggestion)] -> Nat
forall a. Sized a => a -> Nat
size [WithOrigin (Ranged MetaNameSuggestion)]
names) ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term -> Bool) -> Args -> Elims -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Elim' Term -> Bool
forall {a} {a}.
(DeBruijn a, DeBruijn a) =>
Arg a -> Elim' a -> Bool
sameVar Args
args_G Elims
es_G
                     doDrop :: [Bool] -> [a] -> [a]
doDrop (Bool
b : [Bool]
xs)  (a
e : [a]
es) = (if Bool
b then [a] -> [a]
forall a. a -> a
id else (a
e a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [a] -> [a]
doDrop [Bool]
xs [a]
es
                     doDrop []        [a]
es = [a]
es
                     doDrop [Bool]
_         [] = []
                 in [Bool] -> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
forall {a}. [Bool] -> [a] -> [a]
doDrop [Bool]
dropArg ([Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)])
-> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
forall a b. (a -> b) -> a -> b
$ [Elim' (Named_ Expr)]
named_es'

              simpl_named_es' | Bool
opt_show_ids                 = [Elim' (Named_ Expr)]
named_es'
                              | Just Substitution' Term
sub_mtel2local <- Maybe (Substitution' Term)
msub1 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
dropIdentitySubs Substitution' Term
forall a. Substitution' a
IdS           Substitution' Term
sub_mtel2local
                              | Just Substitution' Term
sub_local2mtel <- Maybe (Substitution' Term)
msub2 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
dropIdentitySubs Substitution' Term
sub_local2mtel Substitution' Term
forall a. Substitution' a
IdS
                              | Bool
otherwise                    = [Elim' (Named_ Expr)]
named_es'

          nelims x' simpl_named_es'

    I.DontCare Term
v -> do
      showIrr <- PragmaOptions -> Bool
optShowIrrelevant (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      if | showIrr   -> reifyTerm expandAnonDefs v
         | otherwise -> return underscore
    I.Dummy MetaNameSuggestion
s [] -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString (MetaNameSuggestion -> Text
T.pack MetaNameSuggestion
s)
    I.Dummy MetaNameSuggestion
"applyE" Elims
es | I.Apply (Arg ArgInfo
_ Term
h) : Elims
es' <- Elims
es -> do
                            h <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
h
                            es' <- reify es'
                            elims h es'
                        | Bool
otherwise -> m Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    I.Dummy MetaNameSuggestion
s Elims
es -> do
      s <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (MetaNameSuggestion -> Elims -> Term
I.Dummy MetaNameSuggestion
s [])
      es <- reify es
      elims s es
  where
    -- Andreas, 2012-10-20  expand a copy if not in scope
    -- to improve error messages.
    -- Don't do this if we have just expanded into a display form,
    -- otherwise we loop!
    reifyDef :: MonadReify m => Bool -> QName -> I.Elims -> m Expr
    reifyDef :: forall (m :: * -> *).
MonadReify m =>
Bool -> QName -> Elims -> m Expr
reifyDef Bool
True QName
x Elims
es =
      m Bool -> m Expr -> m Expr -> m Expr
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> Bool
not (Bool -> Bool) -> (ScopeInfo -> Bool) -> ScopeInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> Bool
forall a. Null a => a -> Bool
null ([QName] -> Bool) -> (ScopeInfo -> [QName]) -> ScopeInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ScopeInfo -> [QName]
inverseScopeLookupName QName
x (ScopeInfo -> Bool) -> m ScopeInfo -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope) (QName -> Elims -> m Expr
forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
      r <- QName -> Elims -> m (Reduced () Term)
forall (m :: * -> *).
PureTCM m =>
QName -> Elims -> m (Reduced () Term)
reduceDefCopy QName
x Elims
es
      case r of
        YesReduction Simplification
_ Term
v -> do
          MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
reportS MetaNameSuggestion
"reify.anon" Nat
60
            [ MetaNameSuggestion
"reduction on defined ident. in anonymous module"
            , MetaNameSuggestion
"x = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ QName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow QName
x
            , MetaNameSuggestion
"v = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ Term -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Term
v
            ]
          Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
        NoReduction () -> do
          MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
reportS MetaNameSuggestion
"reify.anon" Nat
60
            [ MetaNameSuggestion
"no reduction on defined ident. in anonymous module"
            , MetaNameSuggestion
"x  = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ QName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow QName
x
            , MetaNameSuggestion
"es = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ Elims -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Elims
es
            ]
          QName -> Elims -> m Expr
forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es
    reifyDef Bool
_ QName
x Elims
es = QName -> Elims -> m Expr
forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es

    reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr
    reifyDef' :: forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es = do
      MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.def" Nat
60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"reifying call to " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ QName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow QName
x
      -- We should drop this many arguments from the local context.
      n <- QName -> m Nat
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
      reportSLn "reify.def" 70 $ "freeVars for " ++ prettyShow x ++ " = " ++ show n
      -- If the definition is not (yet) in the signature,
      -- we just do the obvious.
      let fallback SigError
_ = Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
x) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify (Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)
      caseEitherM (getConstInfo' x) fallback $ \ Definition
defn -> do
      let def :: Defn
def = Definition -> Defn
theDef Definition
defn

      -- Check if we have an absurd lambda.
      case Defn
def of
       Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
funClauses = [Clause
cl] }
          | QName -> Bool
isAbsurdLambdaName QName
x -> do
                  -- get hiding info from last pattern, which should be ()
                  let ([NamedArg DeBruijnPattern]
ps, NamedArg DeBruijnPattern
p) = ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
-> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
-> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
forall a. a -> Maybe a -> a
fromMaybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
 -> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern))
-> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
-> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern]
-> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
forall a. [a] -> Maybe ([a], a)
initLast ([NamedArg DeBruijnPattern]
 -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern))
-> [NamedArg DeBruijnPattern]
-> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                  let h :: Hiding
h = NamedArg DeBruijnPattern -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg DeBruijnPattern
p
                      n :: Nat
n = [NamedArg DeBruijnPattern] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [NamedArg DeBruijnPattern]
ps  -- drop all args before the absurd one
                      absLam :: Expr
absLam = ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
h
                  if | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Elims -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es -> do -- We don't have all arguments before the absurd one!
                        let name :: DeBruijnPattern -> MetaNameSuggestion
name (I.VarP PatternInfo
_ DBPatVar
x) = MetaNameSuggestion -> MetaNameSuggestion
patVarNameToString (MetaNameSuggestion -> MetaNameSuggestion)
-> MetaNameSuggestion -> MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ DBPatVar -> MetaNameSuggestion
dbPatVarName DBPatVar
x
                            name DeBruijnPattern
_            = MetaNameSuggestion
forall a. HasCallStack => a
__IMPOSSIBLE__  -- only variables before absurd pattern
                            vars :: [(ArgInfo, MetaNameSuggestion)]
vars = (NamedArg DeBruijnPattern -> (ArgInfo, MetaNameSuggestion))
-> [NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)]
forall a b. (a -> b) -> [a] -> [b]
map (NamedArg DeBruijnPattern -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (NamedArg DeBruijnPattern -> ArgInfo)
-> (NamedArg DeBruijnPattern -> MetaNameSuggestion)
-> NamedArg DeBruijnPattern
-> (ArgInfo, MetaNameSuggestion)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DeBruijnPattern -> MetaNameSuggestion
name (DeBruijnPattern -> MetaNameSuggestion)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> MetaNameSuggestion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) ([NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)])
-> [NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)]
forall a b. (a -> b) -> a -> b
$ Nat -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Nat -> [a] -> [a]
drop (Elims -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es) [NamedArg DeBruijnPattern]
ps
                            lam :: (ArgInfo, a) -> m (Expr -> Expr)
lam (ArgInfo
i, a
s) = do
                              x <- a -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => a -> m Name
freshName_ a
s
                              return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg i $ A.mkBinder_ x)
                        ((Expr -> Expr) -> Expr -> Expr) -> Expr -> [Expr -> Expr] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
($) Expr
absLam ([Expr -> Expr] -> Expr) -> m [Expr -> Expr] -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ArgInfo, MetaNameSuggestion) -> m (Expr -> Expr))
-> [(ArgInfo, MetaNameSuggestion)] -> m [Expr -> Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ArgInfo, MetaNameSuggestion) -> m (Expr -> Expr)
forall {m :: * -> *} {a}.
(FreshName a, MonadFresh NameId m) =>
(ArgInfo, a) -> m (Expr -> Expr)
lam [(ArgInfo, MetaNameSuggestion)]
vars
                      | Bool
otherwise -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
absLam ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
reify (Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)

      -- Otherwise (no absurd lambda):
       Defn
_ -> do

        -- Andrea(s), 2016-07-06
        -- Extended lambdas are not considered to be projection like,
        -- as they are mutually recursive with their parent.
        -- Thus we do not have to consider padding them.

        -- Check whether we have an extended lambda and display forms are on.
        df <- m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled

        -- #3004: give up if we have to print a pattern lambda inside its own body!
        alreadyPrinting <- viewTC ePrintingPatternLambdas

        extLam <- case def of
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just{}, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right{} } -> m (Maybe (Nat, Maybe System))
forall a. HasCallStack => a
__IMPOSSIBLE__
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
b Maybe System
sys) } ->
            (Nat, Maybe System) -> Maybe (Nat, Maybe System)
forall a. a -> Maybe a
Just ((Nat, Maybe System) -> Maybe (Nat, Maybe System))
-> (Tele (Dom Type) -> (Nat, Maybe System))
-> Tele (Dom Type)
-> Maybe (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Maybe System -> Maybe System
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy Maybe System
sys) (Nat -> (Nat, Maybe System))
-> (Tele (Dom Type) -> Nat)
-> Tele (Dom Type)
-> (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Maybe (Nat, Maybe System))
-> m (Tele (Dom Type)) -> m (Maybe (Nat, Maybe System))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
          Defn
_ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Nat, Maybe System)
forall a. Maybe a
Nothing

        -- Amy, 2023-04-12: Don't reify clauses generated by the cubical
        -- coverage checker when printing an extended lambda. We can
        -- identify these clauses by looking for patterns headed by DefP
        -- (either transpX or hcomp associated with a data type).
        --
        -- Since these are always automatically derived, printing them
        -- is noise, and shows up even in non-cubical modules, as long
        -- as an imported extended lambda is defined cubical-compatibly.
        let insClause = [NamedArg DeBruijnPattern] -> Bool
hasDefP ([NamedArg DeBruijnPattern] -> Bool)
-> (Clause -> [NamedArg DeBruijnPattern]) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats
        case extLam of
          Just (Nat
pars, Maybe System
sys) | Bool
df, QName
x QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [QName]
alreadyPrinting ->
            Lens' TCEnv [QName] -> ([QName] -> [QName]) -> m Expr -> m Expr
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
Lens' TCEnv [QName]
ePrintingPatternLambdas (QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$
            QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x (Definition -> ArgInfo
defArgInfo Definition
defn) Nat
pars Maybe System
sys
              ((Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
insClause) (Definition -> [Clause]
defClauses Definition
defn)) Elims
es

        -- Otherwise (ordinary function call):
          Maybe (Nat, Maybe System)
_ -> do
           (pad, nes :: [Elim' (Named_ Term)]) <- case Defn
def of

            Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projIndex :: Projection -> Nat
projIndex = Nat
np } } | Nat
np Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 -> do
              MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.def" Nat
70 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"  def. is a projection with projIndex = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ Nat -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Nat
np

              -- This is tricky:
              --  * getDefFreeVars x tells us how many arguments
              --    are part of the local context
              --  * some of those arguments might have been dropped
              --    due to projection likeness
              --  * when showImplicits is on we'd like to see the dropped
              --    projection arguments

              TelV tel _ <- Nat -> Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> Type -> m (TelV Type)
telViewUpTo Nat
np (Definition -> Type
defType Definition
defn)
              let (as, rest) = splitAt (np - 1) $ telToList tel
                  dom = Dom (MetaNameSuggestion, Type)
-> [Dom (MetaNameSuggestion, Type)]
-> Dom (MetaNameSuggestion, Type)
forall a. a -> [a] -> a
headWithDefault Dom (MetaNameSuggestion, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom (MetaNameSuggestion, Type)]
rest

              -- These are the dropped projection arguments
              scope <- getScope
              let underscore = MetaInfo -> Expr
A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo
Info.emptyMetaInfo { metaScope = scope }
              let pad :: [NamedArg Expr]
                  pad = [Dom (MetaNameSuggestion, Type)]
-> (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
-> [Arg (Named_ Expr)]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom (MetaNameSuggestion, Type)]
as ((Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
 -> [Arg (Named_ Expr)])
-> (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
-> [Arg (Named_ Expr)]
forall a b. (a -> b) -> a -> b
$ \ (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (MetaNameSuggestion
x, Type
_)}) ->
                    ArgInfo -> Named_ Expr -> Arg (Named_ Expr)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named_ Expr -> Arg (Named_ Expr))
-> Named_ Expr -> Arg (Named_ Expr)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged MetaNameSuggestion))
-> Expr -> Named_ Expr
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged MetaNameSuggestion)
-> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall a. a -> Maybe a
Just (WithOrigin (Ranged MetaNameSuggestion)
 -> Maybe (WithOrigin (Ranged MetaNameSuggestion)))
-> WithOrigin (Ranged MetaNameSuggestion)
-> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall a b. (a -> b) -> a -> b
$ Origin
-> Ranged MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged MetaNameSuggestion
 -> WithOrigin (Ranged MetaNameSuggestion))
-> Ranged MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion -> Ranged MetaNameSuggestion
forall a. a -> Ranged a
unranged MetaNameSuggestion
x) Expr
underscore
                      -- TODO #3353 Origin from Dom?

              -- Now pad' ++ es' = drop n (pad ++ es)
              let pad' = Nat -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. Nat -> [a] -> [a]
drop Nat
n [Arg (Named_ Expr)]
pad
                  es'  = Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
0 (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [Arg (Named_ Expr)] -> Nat
forall a. Sized a => a -> Nat
size [Arg (Named_ Expr)]
pad)) Elims
es
              -- Andreas, 2012-04-21: get rid of hidden underscores {_} and {{_}}
              -- Keep non-hidden arguments of the padding.
              --
              -- Andreas, 2016-12-20, issue #2348:
              -- Let @padTail@ be the list of arguments of the padding
              -- (*) after the last visible argument of the padding, and
              -- (*) with the same visibility as the first regular argument.
              -- If @padTail@ is not empty, we need to
              -- print the first regular argument with name.
              -- We further have to print all elements of @padTail@
              -- which have the same name and visibility of the
              -- first regular argument.
              showImp <- showImplicitArguments

              -- Get the visible arguments of the padding and the rest
              -- after the last visible argument.
              let (padVisNamed, padRest) = filterAndRest visible pad'

              -- Remove the names from the visible arguments.
              let padVis  = (Arg (Named_ Expr) -> Arg (Named_ Expr))
-> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Named_ Expr -> Named_ Expr)
-> Arg (Named_ Expr) -> Arg (Named_ Expr)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ Expr -> Named_ Expr)
 -> Arg (Named_ Expr) -> Arg (Named_ Expr))
-> (Named_ Expr -> Named_ Expr)
-> Arg (Named_ Expr)
-> Arg (Named_ Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Named_ Expr
forall a name. a -> Named name a
unnamed (Expr -> Named_ Expr)
-> (Named_ Expr -> Expr) -> Named_ Expr -> Named_ Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing) [Arg (Named_ Expr)]
padVisNamed

              -- Keep only the rest with the same visibility of @dom@...
              let padTail = (Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom (MetaNameSuggestion, Type)
dom) [Arg (Named_ Expr)]
padRest

              -- ... and even the same name.
              let padSame = (Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((MetaNameSuggestion -> Maybe MetaNameSuggestion
forall a. a -> Maybe a
Just ((MetaNameSuggestion, Type) -> MetaNameSuggestion
forall a b. (a, b) -> a
fst ((MetaNameSuggestion, Type) -> MetaNameSuggestion)
-> (MetaNameSuggestion, Type) -> MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ Dom (MetaNameSuggestion, Type) -> (MetaNameSuggestion, Type)
forall t e. Dom' t e -> e
unDom Dom (MetaNameSuggestion, Type)
dom) Maybe MetaNameSuggestion -> Maybe MetaNameSuggestion -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe MetaNameSuggestion -> Bool)
-> (Arg (Named_ Expr) -> Maybe MetaNameSuggestion)
-> Arg (Named_ Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> Maybe MetaNameSuggestion
forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged MetaNameSuggestion)) =>
a -> Maybe MetaNameSuggestion
bareNameOf) [Arg (Named_ Expr)]
padTail

              return $ if null padTail || not showImp
                then (padVis           , map (fmap unnamed) es')
                else (padVis ++ padSame, nameFirstIfHidden dom es')

            -- If it is not a projection(-like) function, we need no padding.
            Defn
_ -> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], (Elim' Term -> Elim' (Named_ Term))
-> Elims -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Named_ Term) -> Elim' Term -> Elim' (Named_ Term)
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Named_ Term
forall a name. a -> Named name a
unnamed) (Elims -> [Elim' (Named_ Term)]) -> Elims -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> a -> b
$ Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)

           reportSDoc "reify.def" 100 $ return $ vcat
             [ "  pad =" <+> pshow pad
             , "  nes =" <+> pshow nes
             ]
           let hd0 | Defn -> Bool
isProperProjection Defn
def = ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
AmbQ (List1 QName -> AmbiguousQName) -> List1 QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ QName -> List1 QName
forall el coll. Singleton el coll => el -> coll
singleton QName
x
                   | Bool
otherwise = QName -> Expr
A.Def QName
x
           let hd = (Expr -> Arg (Named_ Expr) -> Expr)
-> Expr -> [Arg (Named_ Expr)] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_) Expr
hd0 [Arg (Named_ Expr)]
pad
           nelims hd =<< reify nes

    -- Andreas, 2016-07-06 Issue #2047

    -- With parameter refinement, the "parameter" patterns of an extended
    -- lambda can now be different from variable patterns.  If we just drop
    -- them (plus the associated arguments to the extended lambda), we produce
    -- something

    -- i) that violates internal invariants.  In particular, the permutation
    -- dbPatPerm from the patterns to the telescope can no longer be
    -- computed.  (And in fact, dropping from the start of the telescope is
    -- just plainly unsound then.)

    -- ii) prints the wrong thing (old fix for #2047)

    -- What we do now, is more sound, although not entirely satisfying:
    -- When the "parameter" patterns of an external lambdas are not variable
    -- patterns, we fall back to printing the internal function created for the
    -- extended lambda, instead trying to construct the nice syntax.

    reifyExtLam
      :: MonadReify m
      => QName -> ArgInfo -> Int -> Maybe System -> [I.Clause]
      -> I.Elims -> m Expr
    reifyExtLam :: forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x ArgInfo
ai Nat
npars Maybe System
msys [Clause]
cls Elims
es = do
      MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.def" Nat
10 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"reifying extended lambda " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ QName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow QName
x
      MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.def" Nat
50 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> MetaNameSuggestion
forall a. Doc a -> MetaNameSuggestion
render (Doc -> MetaNameSuggestion) -> Doc -> MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ Nat -> Doc -> Doc
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
        [ Doc
"npars =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Nat -> Doc
forall a. Pretty a => a -> Doc
pretty Nat
npars
        , Doc
"es    =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Elim' Term -> Doc) -> Elims -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Nat -> Elim' Term -> Doc
forall a. Pretty a => Nat -> a -> Doc
prettyPrec Nat
10) Elims
es)
        , Doc
"def   =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ((Clause -> Doc) -> [Clause] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Doc
forall a. Pretty a => a -> Doc
pretty [Clause]
cls) ]
      -- As extended lambda clauses live in the top level, we add the whole
      -- section telescope to the number of parameters.
      let (Elims
pares, Elims
rest) = Nat -> Elims -> (Elims, Elims)
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars Elims
es
      let pars :: Args
pars = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
pares

      -- Since we applying the clauses to the parameters,
      -- we do not need to drop their initial "parameter" patterns
      -- (this is taken care of by @apply@).
      cls <- Maybe System -> m [Clause] -> (System -> m [Clause]) -> m [Clause]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
               ((Clause -> m Clause) -> [Clause] -> m [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (NamedClause -> m Clause
NamedClause -> m (ReifiesTo NamedClause)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify (NamedClause -> m Clause)
-> (Clause -> NamedClause) -> Clause -> m Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
x Bool
False (Clause -> NamedClause)
-> (Clause -> Clause) -> Clause -> NamedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cls)
               (QNamed System -> m [Clause]
QNamed System -> m (ReifiesTo (QNamed System))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
QNamed System -> m (ReifiesTo (QNamed System))
reify (QNamed System -> m [Clause])
-> (System -> QNamed System) -> System -> m [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> System -> QNamed System
forall a. QName -> a -> QNamed a
QNamed QName
x (System -> QNamed System)
-> (System -> System) -> System -> QNamed System
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (System -> Args -> System
forall t. Apply t => t -> Args -> t
`apply` Args
pars))
      let cx     = Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          dInfo  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cx Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef
                     (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x)
          erased = case ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
            Quantity0 Q0Origin
o -> Q0Origin -> Erased
Erased Q0Origin
o
            Quantityω QωOrigin
o -> QωOrigin -> Erased
NotErased QωOrigin
o
            Quantity1 Q1Origin
o -> Erased
forall a. HasCallStack => a
__IMPOSSIBLE__
          lam = case [Clause]
cls of
            []       -> ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
NotHidden
            (Clause
cl:[Clause]
cls) -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo Erased
erased QName
x (Clause
cl Clause -> [Clause] -> List1 Clause
forall a. a -> [a] -> NonEmpty a
:| [Clause]
cls)
      elims lam =<< reify rest

-- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden :: forall t a.
Dom (MetaNameSuggestion, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden Dom (MetaNameSuggestion, t)
dom (I.Apply (Arg ArgInfo
info a
e) : [Elim' a]
es) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info =
  Arg (Named_ a) -> Elim' (Named_ a)
forall a. Arg a -> Elim' a
I.Apply (ArgInfo -> Named_ a -> Arg (Named_ a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe (WithOrigin (Ranged MetaNameSuggestion)) -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged MetaNameSuggestion)
-> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall a. a -> Maybe a
Just (WithOrigin (Ranged MetaNameSuggestion)
 -> Maybe (WithOrigin (Ranged MetaNameSuggestion)))
-> WithOrigin (Ranged MetaNameSuggestion)
-> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall a b. (a -> b) -> a -> b
$ Origin
-> Ranged MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged MetaNameSuggestion
 -> WithOrigin (Ranged MetaNameSuggestion))
-> Ranged MetaNameSuggestion
-> WithOrigin (Ranged MetaNameSuggestion)
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion -> Ranged MetaNameSuggestion
forall a. a -> Ranged a
unranged (MetaNameSuggestion -> Ranged MetaNameSuggestion)
-> MetaNameSuggestion -> Ranged MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ (MetaNameSuggestion, t) -> MetaNameSuggestion
forall a b. (a, b) -> a
fst ((MetaNameSuggestion, t) -> MetaNameSuggestion)
-> (MetaNameSuggestion, t) -> MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ Dom (MetaNameSuggestion, t) -> (MetaNameSuggestion, t)
forall t e. Dom' t e -> e
unDom Dom (MetaNameSuggestion, t)
dom) a
e)) Elim' (Named_ a) -> [Elim' (Named_ a)] -> [Elim' (Named_ a)]
forall a. a -> [a] -> [a]
:
  (Elim' a -> Elim' (Named_ a)) -> [Elim' a] -> [Elim' (Named_ a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Named_ a) -> Elim' a -> Elim' (Named_ a)
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Named_ a
forall a name. a -> Named name a
unnamed) [Elim' a]
es
nameFirstIfHidden Dom (MetaNameSuggestion, t)
_ [Elim' a]
es =
  (Elim' a -> Elim' (Named_ a)) -> [Elim' a] -> [Elim' (Named_ a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Named_ a) -> Elim' a -> Elim' (Named_ a)
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Named_ a
forall a name. a -> Named name a
unnamed) [Elim' a]
es

instance Reify i => Reify (Named n i) where
  type ReifiesTo (Named n i) = Named n (ReifiesTo i)

  reify :: forall (m :: * -> *).
MonadReify m =>
Named n i -> m (ReifiesTo (Named n i))
reify = (i -> m (ReifiesTo i)) -> Named n i -> m (Named n (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named n a -> f (Named n b)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify
  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Named n i -> m (ReifiesTo (Named n i))
reifyWhen Bool
b = (i -> m (ReifiesTo i)) -> Named n i -> m (Named n (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named n a -> f (Named n b)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)

-- | Skip reification of implicit and irrelevant args if option is off.
instance Reify i => Reify (Arg i) where
  type ReifiesTo (Arg i) = Arg (ReifiesTo i)

  reify :: forall (m :: * -> *).
MonadReify m =>
Arg i -> m (ReifiesTo (Arg i))
reify (Arg ArgInfo
info i
i) = ArgInfo -> ReifiesTo i -> Arg (ReifiesTo i)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (ReifiesTo i -> Arg (ReifiesTo i))
-> m (ReifiesTo i) -> m (Arg (ReifiesTo i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Bool -> i -> m (ReifiesTo i)) -> i -> Bool -> m (ReifiesTo i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen i
i (Bool -> m (ReifiesTo i)) -> m Bool -> m (ReifiesTo i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Bool
condition)
    where condition :: m Bool
condition = (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> Hiding
argInfoHiding ArgInfo
info Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
/= Hiding
Hidden) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments)
              m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
showIrrelevantArguments)
  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Arg i -> m (ReifiesTo (Arg i))
reifyWhen Bool
b Arg i
i = (i -> m (ReifiesTo i)) -> Arg i -> m (Arg (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b) Arg i
i
{-# SPECIALIZE reify :: Reify i => Arg i -> TCM (ReifiesTo (Arg i)) #-}

-- instance Reify Elim Expr where
--   reifyWhen = reifyWhenE
--   reify = \case
--     I.IApply x y r -> appl "iapply" <$> reify (defaultArg r :: Arg Term)
--     I.Apply v -> appl "apply" <$> reify v
--     I.Proj f  -> appl "proj"  <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
--     where
--       appl :: String -> Arg Expr -> Expr
--       appl s v = A.App exprInfo (A.Lit empty (LitString s)) $ fmap unnamed v

data NamedClause = NamedClause QName Bool I.Clause
  -- ^ Also tracks whether module parameters should be dropped from the patterns.

-- The Monoid instance for Data.Map doesn't require that the values are a
-- monoid.
newtype MonoidMap k v = MonoidMap { forall k v. MonoidMap k v -> Map k v
_unMonoidMap :: Map.Map k v }

instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where
  MonoidMap Map k v
m1 <> :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
<> MonoidMap Map k v
m2 = Map k v -> MonoidMap k v
forall k v. Map k v -> MonoidMap k v
MonoidMap ((v -> v -> v) -> Map k v -> Map k v -> Map k v
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith v -> v -> v
forall a. Monoid a => a -> a -> a
mappend Map k v
m1 Map k v
m2)

instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
  mempty :: MonoidMap k v
mempty = Map k v -> MonoidMap k v
forall k v. Map k v -> MonoidMap k v
MonoidMap Map k v
forall k a. Map k a
Map.empty
  mappend :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
mappend = MonoidMap k v -> MonoidMap k v -> MonoidMap k v
forall a. Semigroup a => a -> a -> a
(<>)

-- | Removes argument names.  Preserves names present in the source.
removeNameUnlessUserWritten :: (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten :: forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten a
a
  | (NameOf a -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin (NameOf a -> Origin) -> Maybe (NameOf a) -> Maybe Origin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe (NameOf a)
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf a
a) Maybe Origin -> Maybe Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin -> Maybe Origin
forall a. a -> Maybe a
Just Origin
UserWritten = a
a
  | Bool
otherwise = Maybe (NameOf a) -> a -> a
forall a. LensNamed a => Maybe (NameOf a) -> a -> a
setNameOf Maybe (NameOf a)
forall a. Maybe a
Nothing a
a

{-# SPECIALIZE stripImplicits :: Set Name  -> A.Patterns -> A.Patterns -> TCM A.Patterns #-}
-- | Removes implicit arguments that are not needed, that is, that don't bind
--   any variables that are actually used and doesn't do pattern matching.
--   Doesn't strip any arguments that were written explicitly by the user.
stripImplicits :: MonadReify m
  => Set Name -- ^ Variables to always include (occurs on RHS of clause)
  -> A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits :: forall (m :: * -> *).
MonadReify m =>
Set Name -> Patterns -> Patterns -> m Patterns
stripImplicits Set Name
toKeep Patterns
params Patterns
ps = do
  -- if --show-implicit we don't need the names
  m Bool -> m Patterns -> m Patterns -> m Patterns
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (Patterns -> m Patterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Patterns -> m Patterns) -> Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> Patterns -> Patterns
forall a b. (a -> b) -> [a] -> [b]
map ((Named_ Pattern -> Named_ Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ Pattern -> Named_ Pattern
forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten) Patterns
ps) (m Patterns -> m Patterns) -> m Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ do
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
reportSDoc MetaNameSuggestion
"reify.implicit" Nat
100 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"stripping implicits"
      , Nat -> Doc -> Doc
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"ps   =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Patterns -> Doc
forall a. Show a => a -> Doc
pshow Patterns
ps
      ]
    let ps' :: Patterns
ps' = Patterns -> Patterns
blankDots (Patterns -> Patterns) -> Patterns -> Patterns
forall a b. (a -> b) -> a -> b
$ Patterns -> Patterns
strip Patterns
ps
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
reportSDoc MetaNameSuggestion
"reify.implicit" Nat
100 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Nat -> Doc -> Doc
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"ps'  =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Patterns -> Doc
forall a. Show a => a -> Doc
pshow Patterns
ps'
      ]
    Patterns -> m Patterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Patterns
ps'
    where
      -- Replace variables in dot patterns by an underscore _ if they are hidden
      -- in the pattern. This is slightly nicer than making the implicts explicit.
      blankDots :: Patterns -> Patterns
blankDots Patterns
ps = Set Name -> Patterns -> Patterns
forall a. BlankVars a => Set Name -> a -> a
blank (Patterns -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (Patterns -> Set Name) -> Patterns -> Set Name
forall a b. (a -> b) -> a -> b
$ Patterns
params Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
ps) Patterns
ps

      strip :: Patterns -> Patterns
strip Patterns
ps = Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
ps
        where
          stripArgs :: Bool -> Patterns -> Patterns
stripArgs Bool
_ [] = []
          stripArgs Bool
fixedPos (Arg (Named_ Pattern)
a : Patterns
as)
            -- A hidden non-UserWritten variable is removed if not needed for
            -- correct position of the following hidden arguments.
            | Arg (Named_ Pattern) -> Bool
canStrip Arg (Named_ Pattern)
a =
                 if   (Arg (Named_ Pattern) -> Bool) -> Patterns -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Arg (Named_ Pattern) -> Bool
canStrip (Patterns -> Bool) -> Patterns -> Bool
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Bool) -> Patterns -> Patterns
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Arg (Named_ Pattern) -> Bool
forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
isUnnamedHidden Patterns
as
                 then Bool -> Patterns -> Patterns
stripArgs Bool
False Patterns
as
                 else Patterns
goWild
            -- Other arguments are kept.
            | Bool
otherwise = Bool -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos (Arg (Named_ Pattern) -> Arg (Named_ Pattern)
stripArg Arg (Named_ Pattern)
a) Arg (Named_ Pattern) -> Patterns -> Patterns
forall a. a -> [a] -> [a]
: Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
as
            where
              a' :: Arg (Named_ Pattern)
a'     = Arg (Named_ Pattern) -> Pattern -> Arg (Named_ Pattern)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg Arg (Named_ Pattern)
a (Pattern -> Arg (Named_ Pattern))
-> Pattern -> Arg (Named_ Pattern)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP (PatInfo -> Pattern) -> PatInfo -> Pattern
forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
Info.PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern) -> Range
forall a. HasRange a => a -> Range
getRange Arg (Named_ Pattern)
a
              goWild :: Patterns
goWild = Bool -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos Arg (Named_ Pattern)
a' Arg (Named_ Pattern) -> Patterns -> Patterns
forall a. a -> [a] -> [a]
: Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
as

          stripName :: Bool -> f b -> f b
stripName Bool
True  = (b -> b) -> f b -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> b
forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten
          stripName Bool
False = f b -> f b
forall a. a -> a
id

          -- TODO: vars appearing in EqualPs shouldn't be stripped.
          canStrip :: Arg (Named_ Pattern) -> Bool
canStrip Arg (Named_ Pattern)
a = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ Arg (Named_ Pattern) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Pattern)
a
            , Arg (Named_ Pattern) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ Pattern)
a Origin -> [Origin] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ Origin
UserWritten , Origin
CaseSplit ]
            , (WithOrigin (Ranged MetaNameSuggestion) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin (WithOrigin (Ranged MetaNameSuggestion) -> Origin)
-> Maybe (WithOrigin (Ranged MetaNameSuggestion)) -> Maybe Origin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg (Named_ Pattern) -> Maybe (NameOf (Arg (Named_ Pattern)))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf Arg (Named_ Pattern)
a) Maybe Origin -> Maybe Origin -> Bool
forall a. Eq a => a -> a -> Bool
/= Origin -> Maybe Origin
forall a. a -> Maybe a
Just Origin
UserWritten
            , Pattern -> Bool
forall {e}. Pattern' e -> Bool
varOrDot (Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
a)
            , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Pattern -> Bool
mustKeepVar (Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
a)
            ]

          mustKeepVar :: Pattern -> Bool
mustKeepVar (A.VarP (A.BindName Name
x)) = Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
toKeep
          mustKeepVar Pattern
_                       = Bool
False

          isUnnamedHidden :: a -> Bool
isUnnamedHidden a
x = a -> Bool
forall a. LensHiding a => a -> Bool
notVisible a
x Bool -> Bool -> Bool
&& Maybe (NameOf a) -> Bool
forall a. Maybe a -> Bool
isNothing (a -> Maybe (NameOf a)
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf a
x) Bool -> Bool -> Bool
&& Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (a -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP a
x)

          stripArg :: Arg (Named_ Pattern) -> Arg (Named_ Pattern)
stripArg Arg (Named_ Pattern)
a = (Named_ Pattern -> Named_ Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
forall a b.
(a -> b)
-> Named (WithOrigin (Ranged MetaNameSuggestion)) a
-> Named (WithOrigin (Ranged MetaNameSuggestion)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
stripPat) Arg (Named_ Pattern)
a

          stripPat :: Pattern -> Pattern
stripPat = \case
            p :: Pattern
p@(A.VarP BindName
_)        -> Pattern
p
            A.ConP ConPatInfo
i AmbiguousQName
c Patterns
ps       -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c (Patterns -> Pattern) -> Patterns -> Pattern
forall a b. (a -> b) -> a -> b
$ Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
ps
            p :: Pattern
p@A.ProjP{}         -> Pattern
p
            p :: Pattern
p@(A.DefP PatInfo
_ AmbiguousQName
_ Patterns
_)    -> Pattern
p
            p :: Pattern
p@(A.DotP PatInfo
_ Expr
_e)     -> Pattern
p
            p :: Pattern
p@(A.WildP PatInfo
_)       -> Pattern
p
            p :: Pattern
p@(A.AbsurdP PatInfo
_)     -> Pattern
p
            p :: Pattern
p@(A.LitP PatInfo
_ Literal
_)      -> Pattern
p
            A.AsP PatInfo
i BindName
x Pattern
p         -> PatInfo -> BindName -> Pattern -> Pattern
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
stripPat Pattern
p
            A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.RecP ConPatInfo
i [FieldAssignment' Pattern]
fs         -> ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP ConPatInfo
i ([FieldAssignment' Pattern] -> Pattern)
-> [FieldAssignment' Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ (FieldAssignment' Pattern -> FieldAssignment' Pattern)
-> [FieldAssignment' Pattern] -> [FieldAssignment' Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern)
-> FieldAssignment' Pattern -> FieldAssignment' Pattern
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
stripPat) [FieldAssignment' Pattern]
fs  -- TODO Andreas: is this right?
            p :: Pattern
p@A.EqualP{}        -> Pattern
p -- EqualP cannot be blanked.
            A.WithP PatInfo
i Pattern
p         -> PatInfo -> Pattern -> Pattern
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
stripPat Pattern
p -- TODO #2822: right?

          varOrDot :: Pattern' e -> Bool
varOrDot A.VarP{}      = Bool
True
          varOrDot A.WildP{}     = Bool
True
          varOrDot A.DotP{}      = Bool
True
          varOrDot (A.ConP ConPatInfo
cpi AmbiguousQName
_ NAPs e
ps) | ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
cpi ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConOSystem
                                 = ConPatInfo -> ConPatLazy
conPatLazy ConPatInfo
cpi ConPatLazy -> ConPatLazy -> Bool
forall a. Eq a => a -> a -> Bool
== ConPatLazy
ConPatLazy Bool -> Bool -> Bool
|| (NamedArg (Pattern' e) -> Bool) -> NAPs e -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' e -> Bool
varOrDot (Pattern' e -> Bool)
-> (NamedArg (Pattern' e) -> Pattern' e)
-> NamedArg (Pattern' e)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg) NAPs e
ps
          varOrDot Pattern' e
_             = Bool
False

{-# SPECIALIZE blankNotInScope :: BlankVars a => a -> TCM a #-}
{-# SPECIALIZE blankNotInScope :: Expr -> TCM Expr #-}
-- | @blankNotInScope e@ replaces variables in expression @e@ with @_@
-- if they are currently not in scope.
blankNotInScope :: (MonadTCEnv m, MonadDebug m, BlankVars a) => a -> m a
blankNotInScope :: forall (m :: * -> *) a.
(MonadTCEnv m, MonadDebug m, BlankVars a) =>
a -> m a
blankNotInScope a
e = do
  ctxNames <- m [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  letNames <- map fst <$> getLetBindings
  let names = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ([Name] -> Set Name) -> ([Name] -> [Name]) -> [Name] -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter ((NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
C.InScope) (NameInScope -> Bool) -> (Name -> NameInScope) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope) ([Name] -> Set Name) -> [Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ [Name]
ctxNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
letNames
  reportSDoc "reify.blank" 80 . pure $ "names in scope for blanking:" <+> pretty names
  return $ blank names e


-- | @blank bound e@ replaces all variables in expression @e@ that are not in @bound@ by
--   an underscore @_@. It is used for printing dot patterns: we don't want to
--   make implicit variables explicit, so we blank them out in the dot patterns
--   instead (this is fine since dot patterns can be inferred anyway).

class BlankVars a where
  blank :: Set Name -> a -> a

  default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a
  blank = (b -> b) -> a -> a
(b -> b) -> f b -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> a -> a) -> (Set Name -> b -> b) -> Set Name -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Name -> b -> b
forall a. BlankVars a => Set Name -> a -> a
blank

instance BlankVars a => BlankVars (Arg a)
instance BlankVars a => BlankVars (Named s a)
instance BlankVars a => BlankVars [a]
instance BlankVars a => BlankVars (List1 a)
instance BlankVars a => BlankVars (FieldAssignment' a)
-- instance BlankVars a => BlankVars (A.Pattern' a)         -- see case EqualP !

instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
  blank :: Set Name -> (a, b) -> (a, b)
blank Set Name
bound (a
x, b
y) = (Set Name -> a -> a
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x, Set Name -> b -> b
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound b
y)

instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where
  blank :: Set Name -> Either a b -> Either a b
blank Set Name
bound (Left a
x)  = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Set Name -> a -> a
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x
  blank Set Name
bound (Right b
y) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Set Name -> b -> b
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound b
y

instance BlankVars A.ProblemEq where
  blank :: Set Name -> ProblemEq -> ProblemEq
blank Set Name
bound = ProblemEq -> ProblemEq
forall a. a -> a
id

instance BlankVars A.Clause where
  blank :: Set Name -> Clause -> Clause
blank Set Name
bound (A.Clause LHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
ca)
    | WhereDeclarations -> Bool
forall a. Null a => a -> Bool
null WhereDeclarations
wh =
        LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (Set Name -> LHS -> LHS
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' LHS
lhs)
                 (Set Name -> [ProblemEq] -> [ProblemEq]
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' [ProblemEq]
strippedPats)
                 (Set Name -> RHS -> RHS
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' RHS
rhs) WhereDeclarations
noWhereDecls Bool
ca
    | Bool
otherwise = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
    where bound' :: Set Name
bound' = LHS -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn LHS
lhs Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound

instance BlankVars A.LHS where
  blank :: Set Name -> LHS -> LHS
blank Set Name
bound (A.LHS LHSInfo
i LHSCore
core) = LHSInfo -> LHSCore -> LHS
A.LHS LHSInfo
i (LHSCore -> LHS) -> LHSCore -> LHS
forall a b. (a -> b) -> a -> b
$ Set Name -> LHSCore -> LHSCore
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound LHSCore
core

instance BlankVars A.LHSCore where
  blank :: Set Name -> LHSCore -> LHSCore
blank Set Name
bound (A.LHSHead QName
f Patterns
ps) = QName -> Patterns -> LHSCore
forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
f (Patterns -> LHSCore) -> Patterns -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name -> Patterns -> Patterns
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
  blank Set Name
bound (A.LHSProj AmbiguousQName
p NamedArg LHSCore
b Patterns
ps) = (NamedArg LHSCore -> Patterns -> LHSCore)
-> (NamedArg LHSCore, Patterns) -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AmbiguousQName -> NamedArg LHSCore -> Patterns -> LHSCore
forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSProj AmbiguousQName
p) ((NamedArg LHSCore, Patterns) -> LHSCore)
-> (NamedArg LHSCore, Patterns) -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name
-> (NamedArg LHSCore, Patterns) -> (NamedArg LHSCore, Patterns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (NamedArg LHSCore
b, Patterns
ps)
  blank Set Name
bound (A.LHSWith LHSCore
h List1 (Arg Pattern)
wps Patterns
ps) = ((LHSCore, List1 (Arg Pattern)) -> Patterns -> LHSCore)
-> ((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((LHSCore -> List1 (Arg Pattern) -> Patterns -> LHSCore)
-> (LHSCore, List1 (Arg Pattern)) -> Patterns -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry LHSCore -> List1 (Arg Pattern) -> Patterns -> LHSCore
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
A.LHSWith) (((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore)
-> ((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name
-> ((LHSCore, List1 (Arg Pattern)), Patterns)
-> ((LHSCore, List1 (Arg Pattern)), Patterns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound ((LHSCore
h, List1 (Arg Pattern)
wps), Patterns
ps)

instance BlankVars A.Pattern where
  blank :: Set Name -> Pattern -> Pattern
blank Set Name
bound Pattern
p = case Pattern
p of
    A.VarP BindName
_      -> Pattern
p   -- do not blank pattern vars
    A.ConP ConPatInfo
c AmbiguousQName
i Patterns
ps -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
c AmbiguousQName
i (Patterns -> Pattern) -> Patterns -> Pattern
forall a b. (a -> b) -> a -> b
$ Set Name -> Patterns -> Patterns
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
    A.ProjP{}     -> Pattern
p
    A.DefP PatInfo
i AmbiguousQName
f Patterns
ps -> PatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f (Patterns -> Pattern) -> Patterns -> Pattern
forall a b. (a -> b) -> a -> b
$ Set Name -> Patterns -> Patterns
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
    A.DotP PatInfo
i Expr
e    -> PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
i (Expr -> Pattern) -> Expr -> Pattern
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.WildP PatInfo
_     -> Pattern
p
    A.AbsurdP PatInfo
_   -> Pattern
p
    A.LitP PatInfo
_ Literal
_    -> Pattern
p
    A.AsP PatInfo
i BindName
n Pattern
p   -> PatInfo -> BindName -> Pattern -> Pattern
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
n (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Set Name -> Pattern -> Pattern
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p
    A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.RecP ConPatInfo
i [FieldAssignment' Pattern]
fs   -> ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP ConPatInfo
i ([FieldAssignment' Pattern] -> Pattern)
-> [FieldAssignment' Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ Set Name
-> [FieldAssignment' Pattern] -> [FieldAssignment' Pattern]
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound [FieldAssignment' Pattern]
fs
    A.EqualP{}    -> Pattern
p
    A.WithP PatInfo
i Pattern
p   -> PatInfo -> Pattern -> Pattern
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (Set Name -> Pattern -> Pattern
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p)

instance BlankVars A.Expr where
  blank :: Set Name -> Expr -> Expr
blank Set Name
bound Expr
e = case Expr
e of
    A.ScopedExpr ScopeInfo
i Expr
e         -> ScopeInfo -> Expr -> Expr
A.ScopedExpr ScopeInfo
i (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.Var Name
x                  -> if Name
x Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
bound then Expr
e
                                else MetaInfo -> Expr
A.Underscore MetaInfo
emptyMetaInfo  -- Here is the action!
    A.Def' QName
_ Suffix
_               -> Expr
e
    A.Proj{}                 -> Expr
e
    A.Con AmbiguousQName
_                  -> Expr
e
    A.Lit ExprInfo
_ Literal
_                -> Expr
e
    A.QuestionMark{}         -> Expr
e
    A.Underscore MetaInfo
_           -> Expr
e
    A.Dot ExprInfo
i Expr
e                -> ExprInfo -> Expr -> Expr
A.Dot ExprInfo
i (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.App AppInfo
i Expr
e1 Arg (Named_ Expr)
e2            -> (Expr -> Arg (Named_ Expr) -> Expr)
-> (Expr, Arg (Named_ Expr)) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
i) ((Expr, Arg (Named_ Expr)) -> Expr)
-> (Expr, Arg (Named_ Expr)) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, Arg (Named_ Expr)) -> (Expr, Arg (Named_ Expr))
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e1, Arg (Named_ Expr)
e2)
    A.WithApp ExprInfo
i Expr
e List1 Expr
es         -> (Expr -> List1 Expr -> Expr) -> (Expr, List1 Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> List1 Expr -> Expr
A.WithApp ExprInfo
i) ((Expr, List1 Expr) -> Expr) -> (Expr, List1 Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, List1 Expr) -> (Expr, List1 Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, List1 Expr
es)
    A.Lam ExprInfo
i LamBinding
b Expr
e              -> let bound' :: Set Name
bound' = LamBinding -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn LamBinding
b Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
                                in  ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (Set Name -> LamBinding -> LamBinding
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound LamBinding
b) (Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' Expr
e)
    A.AbsurdLam ExprInfo
_ Hiding
_          -> Expr
e
    A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f List1 Clause
cs -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f (List1 Clause -> Expr) -> List1 Clause -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> List1 Clause -> List1 Clause
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound List1 Clause
cs
    A.Pi ExprInfo
i Telescope1
tel Expr
e             -> let bound' :: Set Name
bound' = Telescope1 -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Telescope1
tel Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
                                in  (Telescope1 -> Expr -> Expr) -> (Telescope1, Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
i) ((Telescope1, Expr) -> Expr) -> (Telescope1, Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Telescope1, Expr) -> (Telescope1, Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' (Telescope1
tel, Expr
e)
    A.Generalized {}         -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Fun ExprInfo
i Arg Expr
a Expr
b              -> (Arg Expr -> Expr -> Expr) -> (Arg Expr, Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun ExprInfo
i) ((Arg Expr, Expr) -> Expr) -> (Arg Expr, Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Arg Expr, Expr) -> (Arg Expr, Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Arg Expr
a, Expr
b)
    A.Let ExprInfo
_ List1 LetBinding
_ Expr
_              -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Rec RecInfo
i RecordAssigns
es               -> RecInfo -> RecordAssigns -> Expr
A.Rec RecInfo
i (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> RecordAssigns -> RecordAssigns
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound RecordAssigns
es
    A.RecUpdate RecInfo
i Expr
e Assigns
es       -> (Expr -> Assigns -> Expr) -> (Expr, Assigns) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (RecInfo -> Expr -> Assigns -> Expr
A.RecUpdate RecInfo
i) ((Expr, Assigns) -> Expr) -> (Expr, Assigns) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, Assigns) -> (Expr, Assigns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, Assigns
es)
    A.Quote {}               -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.QuoteTerm {}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Unquote {}             -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DontCare Expr
v             -> Expr -> Expr
A.DontCare (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
v
    A.PatternSyn {}          -> Expr
e
    A.Macro {}               -> Expr
e

instance BlankVars A.ModuleName where
  blank :: Set Name -> ModuleName -> ModuleName
blank Set Name
bound = ModuleName -> ModuleName
forall a. a -> a
id

instance BlankVars RHS where
  blank :: Set Name -> RHS -> RHS
blank Set Name
bound (RHS Expr
e Maybe Expr
mc)             = Expr -> Maybe Expr -> RHS
RHS (Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e) Maybe Expr
mc
  blank Set Name
bound RHS
AbsurdRHS              = RHS
AbsurdRHS
  blank Set Name
bound (WithRHS QName
_ List1 WithExpr
es List1 Clause
clauses) = RHS
forall a. HasCallStack => a
__IMPOSSIBLE__ -- NZ
  blank Set Name
bound (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
_) = RHS
forall a. HasCallStack => a
__IMPOSSIBLE__ -- NZ

instance BlankVars A.LamBinding where
  blank :: Set Name -> LamBinding -> LamBinding
blank Set Name
bound b :: LamBinding
b@A.DomainFree{} = LamBinding
b
  blank Set Name
bound (A.DomainFull TypedBinding
bs) = TypedBinding -> LamBinding
A.DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Set Name -> TypedBinding -> TypedBinding
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound TypedBinding
bs

instance BlankVars TypedBinding where
  blank :: Set Name -> TypedBinding -> TypedBinding
blank Set Name
bound (TBind Range
r TypedBindingInfo
t List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
n Expr
e) = Range
-> TypedBindingInfo
-> List1
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
n (Expr -> TypedBinding) -> Expr -> TypedBinding
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
  blank Set Name
bound (TLet Range
_ List1 LetBinding
_)    = TypedBinding
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Since the internal syntax has no let bindings left


-- | Collect the binders in some abstract syntax lhs.

class Binder a where
  varsBoundIn :: a -> Set Name

  default varsBoundIn :: (Foldable f, Binder b, f b ~ a) => a -> Set Name
  varsBoundIn = (b -> Set Name) -> f b -> Set Name
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn

instance Binder A.LHS where
  varsBoundIn :: LHS -> Set Name
varsBoundIn (A.LHS LHSInfo
_ LHSCore
core) = LHSCore -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn LHSCore
core

instance Binder A.LHSCore where
  varsBoundIn :: LHSCore -> Set Name
varsBoundIn (A.LHSHead QName
_ Patterns
ps)     = Patterns -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Patterns
ps
  varsBoundIn (A.LHSProj AmbiguousQName
_ NamedArg LHSCore
b Patterns
ps)   = (NamedArg LHSCore, Patterns) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (NamedArg LHSCore
b, Patterns
ps)
  varsBoundIn (A.LHSWith LHSCore
h List1 (Arg Pattern)
wps Patterns
ps) = ((LHSCore, List1 (Arg Pattern)), Patterns) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn ((LHSCore
h, List1 (Arg Pattern)
wps), Patterns
ps)

instance Binder A.Pattern where
  varsBoundIn :: Pattern -> Set Name
varsBoundIn = (Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern ((Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name)
-> (Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name
forall a b. (a -> b) -> a -> b
$ \case
    A.VarP BindName
x            -> BindName -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
    A.AsP PatInfo
_ BindName
x Pattern' (ADotT Pattern)
_         -> Set Name
forall a. Null a => a
empty    -- Not x because of #2414 (?)
    A.ConP ConPatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_        -> Set Name
forall a. Null a => a
empty
    A.ProjP{}           -> Set Name
forall a. Null a => a
empty
    A.DefP PatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_        -> Set Name
forall a. Null a => a
empty
    A.WildP{}           -> Set Name
forall a. Null a => a
empty
    A.DotP{}            -> Set Name
forall a. Null a => a
empty
    A.AbsurdP{}         -> Set Name
forall a. Null a => a
empty
    A.LitP{}            -> Set Name
forall a. Null a => a
empty
    A.PatternSynP PatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_ -> Set Name
forall a. Null a => a
empty
    A.RecP ConPatInfo
_ [FieldAssignment' (Pattern' (ADotT Pattern))]
_          -> Set Name
forall a. Null a => a
empty
    A.EqualP{}          -> Set Name
forall a. Null a => a
empty
    A.WithP PatInfo
_ Pattern' (ADotT Pattern)
_         -> Set Name
forall a. Null a => a
empty

instance Binder a => Binder (A.Binder' a) where
  varsBoundIn :: Binder' a -> Set Name
varsBoundIn (A.Binder Maybe Pattern
p BinderNameOrigin
_ a
n) = (Maybe Pattern, a) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (Maybe Pattern
p, a
n)

instance Binder A.LamBinding where
  varsBoundIn :: LamBinding -> Set Name
varsBoundIn (A.DomainFree TacticAttribute' Expr
_ Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
x) = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
x
  varsBoundIn (A.DomainFull TypedBinding
b)   = TypedBinding -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn TypedBinding
b

instance Binder TypedBinding where
  varsBoundIn :: TypedBinding -> Set Name
varsBoundIn (TBind Range
_ TypedBindingInfo
_ List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
xs Expr
_) = List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
xs
  varsBoundIn (TLet Range
_ List1 LetBinding
bs)      = List1 LetBinding -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn List1 LetBinding
bs

instance Binder BindName where
  varsBoundIn :: BindName -> Set Name
varsBoundIn BindName
x = Name -> Set Name
forall el coll. Singleton el coll => el -> coll
singleton (BindName -> Name
unBind BindName
x)

instance Binder A.LetBinding where
  varsBoundIn :: LetBinding -> Set Name
varsBoundIn (LetBind LetInfo
_ ArgInfo
_ BindName
x Expr
_ Expr
_) = BindName -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
  varsBoundIn (LetAxiom LetInfo
_ ArgInfo
_ BindName
x Expr
_)  = BindName -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
  varsBoundIn (LetPatBind LetInfo
_ Pattern
p Expr
_)  = Pattern -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Pattern
p
  varsBoundIn LetApply{}          = Set Name
forall a. Null a => a
empty
  varsBoundIn LetOpen{}           = Set Name
forall a. Null a => a
empty
  varsBoundIn LetDeclaredVariable{} = Set Name
forall a. Null a => a
empty

instance Binder a => Binder (FieldAssignment' a)
instance Binder a => Binder (Arg a)
instance Binder a => Binder (Named x a)
instance Binder a => Binder [a]
instance Binder a => Binder (List1 a)
instance Binder a => Binder (Maybe a)

instance (Binder a, Binder b) => Binder (a, b) where
  varsBoundIn :: (a, b) -> Set Name
varsBoundIn (a
x, b
y) = a -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn a
x Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` b -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn b
y

{-# SPECIALIZE reifyPatterns :: [NamedArg I.DeBruijnPattern] -> TCM [NamedArg A.Pattern] #-}
-- | Assumes that pattern variables have been added to the context already.
--   Picks pattern variable names from context.
reifyPatterns :: MonadReify m => [NamedArg I.DeBruijnPattern] -> m [NamedArg A.Pattern]
reifyPatterns :: forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns = (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
-> [NamedArg DeBruijnPattern] -> m Patterns
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
 -> [NamedArg DeBruijnPattern] -> m Patterns)
-> (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
-> [NamedArg DeBruijnPattern]
-> m Patterns
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall p. NamedArg p -> NamedArg p
stripNameFromExplicit (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> Arg (Named_ Pattern)
-> Arg (Named_ Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall p. IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj) (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
-> NamedArg DeBruijnPattern
-> m (Arg (Named_ Pattern))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.>
                       (Named_ DeBruijnPattern -> m (Named_ Pattern))
-> NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((DeBruijnPattern -> m Pattern)
-> Named_ DeBruijnPattern -> m (Named_ Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> Named (WithOrigin (Ranged MetaNameSuggestion)) a
-> f (Named (WithOrigin (Ranged MetaNameSuggestion)) b)
traverse DeBruijnPattern -> m Pattern
forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
reifyPat)
  where
    -- #4399 strip also empty names
    stripNameFromExplicit :: NamedArg p -> NamedArg p
    stripNameFromExplicit :: forall p. NamedArg p -> NamedArg p
stripNameFromExplicit NamedArg p
a
      | NamedArg p -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg p
a Bool -> Bool -> Bool
|| Bool
-> (MetaNameSuggestion -> Bool) -> Maybe MetaNameSuggestion -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Bool -> Bool -> Bool)
-> (MetaNameSuggestion -> Bool)
-> (MetaNameSuggestion -> Bool)
-> MetaNameSuggestion
-> Bool
forall a b c.
(a -> b -> c)
-> (MetaNameSuggestion -> a)
-> (MetaNameSuggestion -> b)
-> MetaNameSuggestion
-> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) MetaNameSuggestion -> Bool
forall a. Null a => a -> Bool
null MetaNameSuggestion -> Bool
forall a. IsNoName a => a -> Bool
isNoName) (NamedArg p -> Maybe MetaNameSuggestion
forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged MetaNameSuggestion)) =>
a -> Maybe MetaNameSuggestion
bareNameOf NamedArg p
a) =
          (Named (WithOrigin (Ranged MetaNameSuggestion)) p
 -> Named (WithOrigin (Ranged MetaNameSuggestion)) p)
-> NamedArg p -> NamedArg p
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (p -> Named (WithOrigin (Ranged MetaNameSuggestion)) p
forall a name. a -> Named name a
unnamed (p -> Named (WithOrigin (Ranged MetaNameSuggestion)) p)
-> (Named (WithOrigin (Ranged MetaNameSuggestion)) p -> p)
-> Named (WithOrigin (Ranged MetaNameSuggestion)) p
-> Named (WithOrigin (Ranged MetaNameSuggestion)) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (WithOrigin (Ranged MetaNameSuggestion)) p -> p
forall name a. Named name a -> a
namedThing) NamedArg p
a
      | Bool
otherwise = NamedArg p
a

    stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p
    stripHidingFromPostfixProj :: forall p. IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj NamedArg p
a = case NamedArg p -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg p
a of
      Just (ProjOrigin
o, AmbiguousQName
_) | ProjOrigin
o ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPrefix -> Hiding -> NamedArg p -> NamedArg p
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden NamedArg p
a
      Maybe (ProjOrigin, AmbiguousQName)
_                             -> NamedArg p
a

    reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern
    reifyPat :: forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
reifyPat DeBruijnPattern
p = do
     MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
reportSDoc MetaNameSuggestion
"reify.pat" Nat
80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reifying pattern" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> DeBruijnPattern -> Doc
forall a. Pretty a => a -> Doc
pretty DeBruijnPattern
p
     keepVars <- PragmaOptions -> Bool
optKeepPatternVariables (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
     case p of
      -- Possibly expanded literal pattern (see #4215)
      DeBruijnPattern
p | Just (PatternInfo PatOrigin
PatOLit [Name]
asB) <- DeBruijnPattern -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p -> do
        Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (DeBruijnPattern -> Term
I.patternToTerm DeBruijnPattern
p) m Term -> (Term -> m Pattern) -> m Pattern
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          I.Lit Literal
l -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings [Name]
asB (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
forall a. Null a => a
empty Literal
l
          Term
_       -> m Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      I.VarP PatternInfo
i DBPatVar
x -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        o :: PatOrigin
o@PatOrigin
PatODot  -> PatOrigin -> Term -> m Pattern
forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o (Term -> m Pattern) -> Term -> m Pattern
forall a b. (a -> b) -> a -> b
$ Nat -> Term
var (Nat -> Term) -> Nat -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
        PatOrigin
PatOWild   -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOrigin
_          -> DBPatVar -> m Pattern
forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x
      I.DotP PatternInfo
i Term
v -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOrigin
PatOWild   -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        -- If Agda turned a user variable @x@ into @.x@, print it back as @x@.
        o :: PatOrigin
o@(PatOVar Name
x) | I.Var Nat
i [] <- Term
v -> do
          x' <- Nat -> m Name
forall (m :: * -> *).
(Applicative m, MonadDebug m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV Nat
i
          if nameConcrete x == nameConcrete x' then
            return $ A.VarP $ mkBindName x'
          else
            reifyDotP o v
        PatOrigin
o -> PatOrigin -> Term -> m Pattern
forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v
      I.LitP PatternInfo
i Literal
l  -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
forall a. Null a => a
empty Literal
l
      I.ProjP ProjOrigin
o QName
d -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
o (AmbiguousQName -> Pattern) -> AmbiguousQName -> Pattern
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d
      I.ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps | ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$
        case PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) of
          PatOrigin
PatOWild   -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
          PatOrigin
PatOAbsurd -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
          PatOVar Name
x | Bool
keepVars -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
          PatOrigin
_               -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps
      I.ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps
      I.DefP PatternInfo
i QName
f [NamedArg DeBruijnPattern]
ps  -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOrigin
PatOWild   -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOVar Name
x | Bool
keepVars -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
        PatOrigin
_ -> PatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
patNoRange (QName -> AmbiguousQName
unambiguous QName
f) (Patterns -> Pattern) -> m Patterns -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns [NamedArg DeBruijnPattern]
ps
      I.IApplyP PatternInfo
i Term
_ Term
_ DBPatVar
x -> [Name] -> m Pattern -> m Pattern
forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        o :: PatOrigin
o@PatOrigin
PatODot  -> PatOrigin -> Term -> m Pattern
forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o (Term -> m Pattern) -> Term -> m Pattern
forall a b. (a -> b) -> a -> b
$ Nat -> Term
var (Nat -> Term) -> Nat -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
        PatOrigin
PatOWild   -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOrigin
_          -> DBPatVar -> m Pattern
forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x

    reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
    reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x = do
      n <- Nat -> m Name
forall (m :: * -> *).
(Applicative m, MonadDebug m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV (Nat -> m Name) -> Nat -> m Name
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
      let y = DBPatVar -> MetaNameSuggestion
dbPatVarName DBPatVar
x
      if | y == "_" -> return $ A.VarP $ mkBindName n
           -- Andreas, 2017-09-03: TODO for #2580
           -- Patterns @VarP "()"@ should have been replaced by @AbsurdP@, but the
           -- case splitter still produces them.
         | prettyShow (nameConcrete n) == "()" -> return $ A.VarP (mkBindName n)
           -- Andreas, 2017-09-03, issue #2729
           -- Restore original pattern name.  AbstractToConcrete picks unique names.
         | otherwise -> return $ A.VarP $
             mkBindName n { nameConcrete = C.simpleName y }

    reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
    reifyDotP :: forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v = do
      keepVars <- PragmaOptions -> Bool
optKeepPatternVariables (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      if | PatOVar x <- o , keepVars       -> return $ A.VarP $ mkBindName x
         | otherwise                       -> A.DotP patNoRange <$> reify v

    reifyConP :: MonadReify m
              => ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
              -> m A.Pattern
    reifyConP :: forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps = do
      Pattern -> m Pattern
forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP (Pattern -> m Pattern) -> m Pattern -> m Pattern
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
ci (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns [NamedArg DeBruijnPattern]
ps
      where
        ci :: ConPatInfo
ci = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
origin PatInfo
patNoRange ConPatLazy
lazy
        lazy :: ConPatLazy
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
cpi = ConPatLazy
ConPatLazy
             | Bool
otherwise    = ConPatLazy
ConPatEager
        origin :: ConInfo
origin = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi

    addAsBindings :: Functor m => [A.Name] -> m A.Pattern -> m A.Pattern
    addAsBindings :: forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings [Name]
xs m Pattern
p = (Name -> m Pattern -> m Pattern)
-> m Pattern -> [Name] -> m Pattern
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Pattern -> Pattern) -> m Pattern -> m Pattern
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> Pattern) -> m Pattern -> m Pattern)
-> (Name -> Pattern -> Pattern) -> Name -> m Pattern -> m Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> BindName -> Pattern -> Pattern
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
patNoRange (BindName -> Pattern -> Pattern)
-> (Name -> BindName) -> Name -> Pattern -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName) m Pattern
p [Name]
xs

{-# SPECIALIZE tryRecPFromConP :: A.Pattern -> TCM A.Pattern #-}
-- | If the record constructor is generated or the user wrote a record pattern,
--   turn constructor pattern into record pattern.
--   Otherwise, keep constructor pattern.
tryRecPFromConP :: MonadReify m => A.Pattern -> m A.Pattern
tryRecPFromConP :: forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP Pattern
p = do
  let fallback :: m Pattern
fallback = Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
  case Pattern
p of
    A.ConP ConPatInfo
ci AmbiguousQName
c Patterns
ps -> do
        MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.pat" Nat
60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"tryRecPFromConP " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ AmbiguousQName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow AmbiguousQName
c
        m (Maybe (QName, RecordData))
-> m Pattern -> ((QName, RecordData) -> m Pattern) -> m Pattern
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (QName -> m (Maybe (QName, RecordData)))
-> QName -> m (Maybe (QName, RecordData))
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
c) m Pattern
fallback (((QName, RecordData) -> m Pattern) -> m Pattern)
-> ((QName, RecordData) -> m Pattern) -> m Pattern
forall a b. (a -> b) -> a -> b
$ \ (QName
r, RecordData
def) -> do
          -- If the record constructor is generated or the user wrote a record pattern,
          -- print record pattern.
          -- Otherwise, print constructor pattern.
          if RecordData -> Bool
_recNamedCon RecordData
def Bool -> Bool -> Bool
&& ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
ci ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= ConInfo
ConORec then m Pattern
fallback else do
            let fs :: [Dom' Term Name]
fs = RecordData -> [Dom' Term Name]
recordFieldNames RecordData
def
            Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([Dom' Term Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom' Term Name]
fs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Patterns -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Patterns
ps) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
            Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP ConPatInfo
ci ([FieldAssignment' Pattern] -> Pattern)
-> [FieldAssignment' Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ (Dom' Term Name
 -> Arg (Named_ Pattern) -> FieldAssignment' Pattern)
-> [Dom' Term Name] -> Patterns -> [FieldAssignment' Pattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Dom' Term Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern
forall {t} {a}. Dom' t Name -> NamedArg a -> FieldAssignment' a
mkFA [Dom' Term Name]
fs Patterns
ps
        where
          mkFA :: Dom' t Name -> NamedArg a -> FieldAssignment' a
mkFA Dom' t Name
ax NamedArg a
nap = Name -> a -> FieldAssignment' a
forall a. Name -> a -> FieldAssignment' a
FieldAssignment (Dom' t Name -> Name
forall t e. Dom' t e -> e
unDom Dom' t Name
ax) (NamedArg a -> a
forall a. NamedArg a -> a
namedArg NamedArg a
nap)
    Pattern
_ -> m Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__

isRecOrigin :: ConOrigin -> Bool
isRecOrigin :: ConInfo -> Bool
isRecOrigin ConInfo
ConORec = Bool
True
isRecOrigin ConInfo
ConORecWhere = Bool
True
isRecOrigin ConInfo
_ = Bool
False

conOriginToRecInfo :: ConOrigin -> RecInfo
conOriginToRecInfo :: ConInfo -> RecInfo
conOriginToRecInfo ConInfo
ConORecWhere = Range -> RecInfo
recInfoWhere Range
forall a. Range' a
noRange
conOriginToRecInfo ConInfo
_           = Range -> RecInfo
recInfoBrace Range
forall a. Range' a
noRange

{-# SPECIALIZE recOrCon :: QName -> ConOrigin -> [Arg Expr] -> TCM A.Expr #-}
-- | If the record constructor is generated or the user wrote a record expression,
--   turn constructor expression into record expression.
--   Otherwise, keep constructor expression.
recOrCon :: MonadReify m => QName -> ConOrigin -> [Arg Expr] -> m A.Expr
recOrCon :: forall (m :: * -> *).
MonadReify m =>
QName -> ConInfo -> [Arg Expr] -> m Expr
recOrCon QName
c ConInfo
co [Arg Expr]
es = do
  MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
reportSLn MetaNameSuggestion
"reify.expr" Nat
60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion
"recOrCon " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
forall a. [a] -> [a] -> [a]
++ QName -> MetaNameSuggestion
forall a. Pretty a => a -> MetaNameSuggestion
prettyShow QName
c
  m (Maybe (QName, RecordData))
-> m Expr -> ((QName, RecordData) -> m Expr) -> m Expr
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor QName
c) m Expr
fallback (((QName, RecordData) -> m Expr) -> m Expr)
-> ((QName, RecordData) -> m Expr) -> m Expr
forall a b. (a -> b) -> a -> b
$ \ (QName
r, RecordData
def) -> do
    -- If the record constructor is generated or the user wrote a record expression,
    -- print record expression.
    -- Otherwise, print constructor expression.
    if RecordData -> Bool
_recNamedCon RecordData
def Bool -> Bool -> Bool
&& Bool -> Bool
not (ConInfo -> Bool
isRecOrigin ConInfo
co) then m Expr
fallback else do
      let fs :: [Dom' Term Name]
fs = RecordData -> [Dom' Term Name]
recordFieldNames RecordData
def
      Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([Dom' Term Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom' Term Name]
fs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Expr] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Expr]
es) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ RecInfo -> RecordAssigns -> Expr
A.Rec (ConInfo -> RecInfo
conOriginToRecInfo ConInfo
co) (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ (Dom' Term Name -> Arg Expr -> RecordAssign)
-> [Dom' Term Name] -> [Arg Expr] -> RecordAssigns
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Dom' Term Name -> Arg Expr -> RecordAssign
forall {t} {b} {b}.
Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA [Dom' Term Name]
fs [Arg Expr]
es
  where
  fallback :: m Expr
fallback = Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
c)) [Arg Expr]
es
  mkFA :: Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA Dom' t Name
ax  = FieldAssignment' b -> Either (FieldAssignment' b) b
forall a b. a -> Either a b
Left (FieldAssignment' b -> Either (FieldAssignment' b) b)
-> (Arg b -> FieldAssignment' b)
-> Arg b
-> Either (FieldAssignment' b) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> b -> FieldAssignment' b
forall a. Name -> a -> FieldAssignment' a
FieldAssignment (Dom' t Name -> Name
forall t e. Dom' t e -> e
unDom Dom' t Name
ax) (b -> FieldAssignment' b)
-> (Arg b -> b) -> Arg b -> FieldAssignment' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg b -> b
forall e. Arg e -> e
unArg

instance Reify (QNamed I.Clause) where
  type ReifiesTo (QNamed I.Clause) = A.Clause

  reify :: forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify (QNamed QName
f Clause
cl) = NamedClause -> m (ReifiesTo NamedClause)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify (QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True Clause
cl); {-# INLINE reify #-}

instance Reify NamedClause where
  type ReifiesTo NamedClause = A.Clause

  reify :: forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify (NamedClause QName
f Bool
toDrop Clause
cl) = Tele (Dom Type)
-> m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (Clause -> Tele (Dom Type)
clauseTel Clause
cl) (m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause))
-> m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause)
forall a b. (a -> b) -> a -> b
$ do
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
reportSDoc MetaNameSuggestion
"reify.clause" Nat
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"reifying NamedClause"
      , Doc
"  f      =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
      , Doc
"  toDrop =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Doc
forall a. Show a => a -> Doc
pshow Bool
toDrop
      , Doc
"  cl     =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Clause -> Doc
forall a. Pretty a => a -> Doc
pretty Clause
cl
      ]

    let clBody :: Maybe Term
clBody = Clause -> Maybe Term
clauseBody Clause
cl
        rhsVars :: [Nat]
rhsVars = [Nat] -> (Term -> [Nat]) -> Maybe Term -> [Nat]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Term -> [Nat]
forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Maybe Term
clBody

    rhsBody     <- (Term -> m Expr) -> Maybe Term -> m (Maybe Expr)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Maybe Term
clBody
    rhsVarNames <- mapM nameOfBV' rhsVars
    let rhsUsedNames = Set Name -> (Expr -> Set Name) -> Maybe Expr -> Set Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Name
forall a. Monoid a => a
mempty Expr -> Set Name
allUsedNames Maybe Expr
rhsBody
        rhsUsedVars  = [Nat
i | (Nat
i, Just Name
n) <- [Nat] -> [Maybe Name] -> [(Nat, Maybe Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Nat]
rhsVars [Maybe Name]
rhsVarNames, Name
n Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
rhsUsedNames]

    reportSDoc "reify.clause" 60 $ return $ "RHS:" <+> pretty clBody
    reportSDoc "reify.clause" 60 $ return $ "variables occurring on RHS:" <+> pretty rhsVars
      <+> "variable names:" <+> pretty rhsVarNames
      <+> parens (maybe "no clause body" (const "there was a clause body") clBody)
    reportSDoc "reify.clause" 60 $ return $ "names occurring on RHS" <+> pretty (Set.toList rhsUsedNames)

    let ell = Clause -> ExpandedEllipsis
clauseEllipsis Clause
cl
    ps  <- reifyPatterns $ namedClausePats cl
    lhs <- uncurry (SpineLHS $ empty { lhsEllipsis = ell }) <$> reifyDisplayFormP f ps []
    -- Unless @toDrop@ we have already dropped the module patterns from the clauses
    -- (e.g. for extended lambdas). We still get here with toDrop = True and
    -- pattern lambdas when doing make-case, so take care to drop the right
    -- number of parameters.
    (params , lhs) <- if not toDrop then return ([] , lhs) else do
      nfv <- getDefModule f >>= \case
        Left SigError
_  -> Nat -> m Nat
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0
        Right ModuleName
m -> Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Nat) -> m (Tele (Dom Type)) -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
      return $ splitParams nfv lhs
    lhs <- stripImps rhsUsedNames params lhs
    let rhs    = Maybe Expr -> RHS -> (Expr -> RHS) -> RHS
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Expr
rhsBody RHS
AbsurdRHS ((Expr -> RHS) -> RHS) -> (Expr -> RHS) -> RHS
forall a b. (a -> b) -> a -> b
$ \ Expr
e -> Expr -> Maybe Expr -> RHS
RHS Expr
e Maybe Expr
forall a. Maybe a
Nothing
        result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls (Clause -> Bool
I.clauseCatchall Clause
cl)
    return result
    where
      splitParams :: Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams Nat
n (SpineLHS LHSInfo
i QName
f Patterns
ps) =
        let (Patterns
params , Patterns
pats) = Nat -> Patterns -> (Patterns, Patterns)
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Patterns
ps
        in  (Patterns
params , LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f Patterns
pats)
      stripImps :: MonadReify m => Set Name -> [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
      stripImps :: forall (m :: * -> *).
MonadReify m =>
Set Name -> Patterns -> SpineLHS -> m SpineLHS
stripImps Set Name
rhsUsedNames Patterns
params (SpineLHS LHSInfo
i QName
f Patterns
ps) =  LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f (Patterns -> SpineLHS) -> m Patterns -> m SpineLHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Name -> Patterns -> Patterns -> m Patterns
forall (m :: * -> *).
MonadReify m =>
Set Name -> Patterns -> Patterns -> m Patterns
stripImplicits Set Name
rhsUsedNames Patterns
params Patterns
ps
{-# SPECIALIZE reify :: NamedClause -> TCM (ReifiesTo NamedClause) #-}

instance Reify (QNamed System) where
  type ReifiesTo (QNamed System) = [A.Clause]

  reify :: forall (m :: * -> *).
MonadReify m =>
QNamed System -> m (ReifiesTo (QNamed System))
reify (QNamed QName
f (System Tele (Dom Type)
tel [(Face, Term)]
sys)) = Tele (Dom Type)
-> m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel (m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System)))
-> m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System))
forall a b. (a -> b) -> a -> b
$ do
    MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
reportS MetaNameSuggestion
"reify.system" Nat
40 ([MetaNameSuggestion] -> m ()) -> [MetaNameSuggestion] -> m ()
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Tele (Dom Type)
tel MetaNameSuggestion -> [MetaNameSuggestion] -> [MetaNameSuggestion]
forall a. a -> [a] -> [a]
: ((Face, Term) -> MetaNameSuggestion)
-> [(Face, Term)] -> [MetaNameSuggestion]
forall a b. (a -> b) -> [a] -> [b]
map (Face, Term) -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show [(Face, Term)]
sys
    view <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
    unview <- intervalUnview'
    sys <- flip filterM sys $ \ (Face
phi,Term
t) -> do
      Face -> ((Term, Bool) -> m Bool) -> m Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM Face
phi (((Term, Bool) -> m Bool) -> m Bool)
-> ((Term, Bool) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ (Term
u,Bool
b) -> do
        u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
        return $ case (view u, b) of
          (IntervalView
IZero, Bool
True) -> Bool
False
          (IntervalView
IOne, Bool
False) -> Bool
False
          (IntervalView, Bool)
_ -> Bool
True
    forM sys $ \ (Face
alpha,Term
u) -> do
      ps <- [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns ([NamedArg DeBruijnPattern] -> m Patterns)
-> [NamedArg DeBruijnPattern] -> m Patterns
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
tel
      ps <- List1.ifNull alpha (pure ps) {-else-} \ List1 (Term, Bool)
alpha -> do
        ep <- (List1 (Expr, Expr) -> Pattern)
-> m (List1 (Expr, Expr)) -> m Pattern
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatInfo -> List1 (Expr, Expr) -> Pattern
forall e. PatInfo -> List1 (e, e) -> Pattern' e
A.EqualP PatInfo
patNoRange) (m (List1 (Expr, Expr)) -> m Pattern)
-> (((Term, Bool) -> m (Expr, Expr)) -> m (List1 (Expr, Expr)))
-> ((Term, Bool) -> m (Expr, Expr))
-> m Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Term, Bool)
-> ((Term, Bool) -> m (Expr, Expr)) -> m (List1 (Expr, Expr))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 (Term, Bool)
alpha (((Term, Bool) -> m (Expr, Expr)) -> m Pattern)
-> ((Term, Bool) -> m (Expr, Expr)) -> m Pattern
forall a b. (a -> b) -> a -> b
$ \ (Term
phi,Bool
b) -> do
          let
              d :: Bool -> Term
d Bool
True = IntervalView -> Term
unview IntervalView
IOne
              d Bool
False = IntervalView -> Term
unview IntervalView
IZero
          (Term, Term) -> m (ReifiesTo (Term, Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(Term, Term) -> m (ReifiesTo (Term, Term))
reify (Term
phi, Bool -> Term
d Bool
b)
        pure $ ps ++ [defaultNamedArg ep]

      lhs <- SpineLHS empty f <$> stripImplicits mempty [] ps
      rhs <- reify u <&> (`RHS` Nothing)
      return $ A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls False
{-# SPECIALIZE reify :: QNamed System -> TCM (ReifiesTo (QNamed System)) #-}

instance Reify I.Type where
    type ReifiesTo I.Type = A.Type

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Type -> m (ReifiesTo Type)
reifyWhen = Bool -> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE; {-# INLINE reifyWhen #-}
    reify :: forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (I.El Sort
_ Term
t) = Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
t; {-# INLINE reify #-}

instance Reify Sort where
    type ReifiesTo Sort = Expr

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Sort -> m (ReifiesTo Sort)
reifyWhen = Bool -> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE

    reify :: forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s = do
      s <- Sort -> m Sort
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort
s
      SortKit{..} <- infallibleSortKit
      case s of
        I.Univ Univ
u (I.ClosedLevel Integer
0) -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (UnivSize -> Univ -> QName
nameOfUniv UnivSize
USmall Univ
u) Suffix
A.NoSuffix
        I.Univ Univ
u (I.ClosedLevel Integer
n) -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (UnivSize -> Univ -> QName
nameOfUniv UnivSize
USmall Univ
u) (Integer -> Suffix
A.Suffix Integer
n)
        I.Univ Univ
u Level
a -> do
          a <- Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
a
          return $ A.App defaultAppInfo_ (A.Def $ nameOfUniv USmall u) (defaultNamedArg a)
        I.Inf Univ
u Integer
0 -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (UnivSize -> Univ -> QName
nameOfUniv UnivSize
ULarge Univ
u) Suffix
A.NoSuffix
        I.Inf Univ
u Integer
n -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (UnivSize -> Univ -> QName
nameOfUniv UnivSize
ULarge Univ
u) (Integer -> Suffix
A.Suffix Integer
n)
        Sort
I.SizeUniv  -> do
          sizeU <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinSizeUniv
          return $ A.Def sizeU
        Sort
I.LockUniv  -> do
          lockU <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimitiveId -> m (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' PrimitiveId
builtinLockUniv
          return $ A.Def lockU
        Sort
I.LevelUniv -> do
          levelU <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' BuiltinId
builtinLevelUniv
          return $ A.Def levelU
        Sort
I.IntervalUniv -> do
          intervalU <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' BuiltinId
builtinIntervalUniv
          return $ A.Def intervalU
        I.PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
          pis <- MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ (MetaNameSuggestion
"piSort" :: String) -- TODO: hack
          (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
          let app Expr
x Expr
y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
y)
          return $ A.Var pis `app` e1 `app` e2
        I.FunSort Sort
s1 Sort
s2 -> do
          funs <- MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ (MetaNameSuggestion
"funSort" :: String) -- TODO: hack
          (e1,e2) <- reify (s1 , s2)
          let app Expr
x Expr
y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
y)
          return $ A.Var funs `app` e1 `app` e2
        I.UnivSort Sort
s -> do
          univs <- MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ (MetaNameSuggestion
"univSort" :: String) -- TODO: hack
          e <- reify s
          return $ A.App defaultAppInfo_ (A.Var univs) $ defaultNamedArg e
        I.MetaS MetaId
x Elims
es -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x Elims
es
        I.DefS QName
d Elims
es -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
d Elims
es
        I.DummyS MetaNameSuggestion
s -> Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ MetaNameSuggestion -> Text
T.pack MetaNameSuggestion
s
{-# SPECIALIZE reify :: Sort -> TCM (ReifiesTo Sort) #-}

instance Reify Level where
  type ReifiesTo Level = Expr

  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Level -> m (ReifiesTo Level)
reifyWhen = Bool -> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
l   = m Bool
-> m (ReifiesTo Level)
-> m (ReifiesTo Level)
-> m (ReifiesTo Level)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasBuiltins m => m Bool
haveLevels (Term -> m Expr
Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> m Expr) -> m Term -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l) (m (ReifiesTo Level) -> m (ReifiesTo Level))
-> m (ReifiesTo Level) -> m (ReifiesTo Level)
forall a b. (a -> b) -> a -> b
$ {-else-} do
    -- Andreas, 2017-09-18, issue #2754
    -- While type checking the level builtins, they are not
    -- available for debug printing.  Thus, print some garbage instead.
    name <- MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ (MetaNameSuggestion
".#Lacking_Level_Builtins#" :: String)
    return $ A.Var name
{-# SPECIALIZE reify :: Level -> TCM (ReifiesTo Level) #-}

instance (Free i, Reify i) => Reify (Abs i) where
  type ReifiesTo (Abs i) = (Name, ReifiesTo i)

  reify :: forall (m :: * -> *).
MonadReify m =>
Abs i -> m (ReifiesTo (Abs i))
reify (NoAbs MetaNameSuggestion
x i
v) = MetaNameSuggestion -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
MetaNameSuggestion -> m Name
freshName_ MetaNameSuggestion
x m Name -> (Name -> m (Name, ReifiesTo i)) -> m (Name, ReifiesTo i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
name -> (Name
name,) (ReifiesTo i -> (Name, ReifiesTo i))
-> m (ReifiesTo i) -> m (Name, ReifiesTo i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify i
v
  reify (Abs MetaNameSuggestion
s i
v) = do

    -- If the bound variable is free in the body, then the name "_" is
    -- replaced by "z".
    s <- MetaNameSuggestion -> m MetaNameSuggestion
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaNameSuggestion -> m MetaNameSuggestion)
-> MetaNameSuggestion -> m MetaNameSuggestion
forall a b. (a -> b) -> a -> b
$ if MetaNameSuggestion -> Bool
forall a. Underscore a => a -> Bool
isUnderscore MetaNameSuggestion
s Bool -> Bool -> Bool
&& Nat
0 Nat -> i -> Bool
forall a. Free a => Nat -> a -> Bool
`freeIn` i
v then MetaNameSuggestion
"z" else MetaNameSuggestion
s

    x <- C.setNotInScope <$> freshName_ s
    e <- addContext x -- type doesn't matter
         $ reify v
    return (x,e)
{-# SPECIALIZE reify :: (Free i, Reify i) -> Abs i -> TCM (ReifiesTo (Abs i)) #-}

instance Reify I.Telescope where
  type ReifiesTo I.Telescope = A.Telescope

  reify :: forall (m :: * -> *).
MonadReify m =>
Tele (Dom Type) -> m (ReifiesTo (Tele (Dom Type)))
reify Tele (Dom Type)
EmptyTel = [TypedBinding] -> m [TypedBinding]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  reify (ExtendTel Dom Type
arg Abs (Tele (Dom Type))
tel) = do
    Arg info e <- Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom Type -> m (ReifiesTo (Dom Type))
reify Dom Type
arg
    (x, bs)  <- reify tel
    let r    = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
        name = Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall t e.
Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
domName Dom Type
arg
    tac <- TacticAttribute <$> do traverse (Ranged noRange <.> reify) $ domTactic arg
    let xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> List1
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
 -> List1
      (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> List1
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
 -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged MetaNameSuggestion))
-> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged MetaNameSuggestion))
name (Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
    return $ TBind r (TypedBindingInfo tac (domIsFinite arg)) xs e : bs
{-# SPECIALIZE reify :: I.Telescope -> TCM (ReifiesTo I.Telescope) #-}

instance Reify i => Reify (Dom i) where
    type ReifiesTo (Dom i) = Arg (ReifiesTo i)

    reify :: forall (m :: * -> *).
MonadReify m =>
Dom i -> m (ReifiesTo (Dom i))
reify (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = i
i}) = ArgInfo -> ReifiesTo i -> Arg (ReifiesTo i)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (ReifiesTo i -> Arg (ReifiesTo i))
-> m (ReifiesTo i) -> m (Arg (ReifiesTo i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify i
i
    {-# INLINE reify #-}

instance Reify i => Reify (I.Elim' i)  where
  type ReifiesTo (I.Elim' i) = I.Elim' (ReifiesTo i)

  reify :: forall (m :: * -> *).
MonadReify m =>
Elim' i -> m (ReifiesTo (Elim' i))
reify = (i -> m (ReifiesTo i)) -> Elim' i -> m (Elim' (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify
  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Elim' i -> m (ReifiesTo (Elim' i))
reifyWhen Bool
b = (i -> m (ReifiesTo i)) -> Elim' i -> m (Elim' (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)

instance Reify i => Reify [i] where
  type ReifiesTo [i] = [ReifiesTo i]

  reify :: forall (m :: * -> *). MonadReify m => [i] -> m (ReifiesTo [i])
reify = (i -> m (ReifiesTo i)) -> [i] -> m [ReifiesTo i]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify
  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> [i] -> m (ReifiesTo [i])
reifyWhen Bool
b = (i -> m (ReifiesTo i)) -> [i] -> m [ReifiesTo i]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)

instance Reify i => Reify (List1 i) where
  type ReifiesTo (List1 i) = List1 (ReifiesTo i)

  reify :: forall (m :: * -> *).
MonadReify m =>
List1 i -> m (ReifiesTo (List1 i))
reify = (i -> m (ReifiesTo i)) -> List1 i -> m (NonEmpty (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
reify
  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> List1 i -> m (ReifiesTo (List1 i))
reifyWhen Bool
b = (i -> m (ReifiesTo i)) -> List1 i -> m (NonEmpty (ReifiesTo i))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)

instance (Reify i1, Reify i2) => Reify (i1, i2) where
    type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo i2)
    reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2) -> m (ReifiesTo (i1, i2))
reify (i1
x,i2
y) = (,) (ReifiesTo i1 -> ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
-> m (ReifiesTo i1)
-> m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i1 -> m (ReifiesTo i1)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
reify i1
x m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
-> m (ReifiesTo i2) -> m (ReifiesTo i1, ReifiesTo i2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i2 -> m (ReifiesTo i2)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
reify i2
y

instance (Reify i1, Reify i2, Reify i3) => Reify (i1,i2,i3) where
    type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
    reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2, i3) -> m (ReifiesTo (i1, i2, i3))
reify (i1
x,i2
y,i3
z) = (,,) (ReifiesTo i1
 -> ReifiesTo i2
 -> ReifiesTo i3
 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
-> m (ReifiesTo i1)
-> m (ReifiesTo i2
      -> ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i1 -> m (ReifiesTo i1)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
reify i1
x m (ReifiesTo i2
   -> ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
-> m (ReifiesTo i2)
-> m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i2 -> m (ReifiesTo i2)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
reify i2
y m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
-> m (ReifiesTo i3) -> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i3 -> m (ReifiesTo i3)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i3 -> m (ReifiesTo i3)
reify i3
z

instance (Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1,i2,i3,i4) where
    type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)
    reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4))
reify (i1
x,i2
y,i3
z,i4
w) = (,,,) (ReifiesTo i1
 -> ReifiesTo i2
 -> ReifiesTo i3
 -> ReifiesTo i4
 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
-> m (ReifiesTo i1)
-> m (ReifiesTo i2
      -> ReifiesTo i3
      -> ReifiesTo i4
      -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i1 -> m (ReifiesTo i1)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
reify i1
x m (ReifiesTo i2
   -> ReifiesTo i3
   -> ReifiesTo i4
   -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
-> m (ReifiesTo i2)
-> m (ReifiesTo i3
      -> ReifiesTo i4
      -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i2 -> m (ReifiesTo i2)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
reify i2
y m (ReifiesTo i3
   -> ReifiesTo i4
   -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
-> m (ReifiesTo i3)
-> m (ReifiesTo i4
      -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i3 -> m (ReifiesTo i3)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i3 -> m (ReifiesTo i3)
reify i3
z m (ReifiesTo i4
   -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
-> m (ReifiesTo i4)
-> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> i4 -> m (ReifiesTo i4)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => i4 -> m (ReifiesTo i4)
reify i4
w