{-# 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.Monad.Trans.Maybe
import Control.Applicative ( liftA2 )
import Control.Monad       ( filterM, forM )

import Data.List qualified as List
import Data.Map qualified as Map
import Data.Maybe
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as T
import Data.Traversable (mapM)

import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Common.Aspect qualified as Asp
import Agda.Syntax.Concrete.Name qualified as C
import Agda.Syntax.Concrete (FieldAssignment'(..), TacticAttribute'(..))
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A hiding (Binder)
import Agda.Syntax.Abstract qualified 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 {-# SOURCE #-} Agda.TypeChecking.Records

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Function (applyUnless)
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List1 qualified as List1
import Agda.Utils.Maybe.Strict qualified 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.SmallSet (SmallSet)
import Agda.Utils.SmallSet qualified as SmallSet
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
    drop
      | Origin
ConversionFail <- ArgInfo -> Origin
argInfoOrigin (Arg (Named_ Expr) -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg (Named_ Expr)
arg) = Bool
False
      | Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Expr)
arg                                = Bool
dontShowImp
      | Bool
otherwise                                     = Bool
False
    hd | Bool
drop      = 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 <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
ePrintMetasBare
      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 [Elim]
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, [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify [Elim]
es)
    DDot'  Term
v [Elim]
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, [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify [Elim]
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 NonEmpty DisplayTerm
us [Elim]
es0 -> do
      (e, es) <- (DisplayTerm, NonEmpty DisplayTerm)
-> m (ReifiesTo (DisplayTerm, NonEmpty DisplayTerm))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(DisplayTerm, NonEmpty DisplayTerm)
-> m (ReifiesTo (DisplayTerm, NonEmpty DisplayTerm))
reify (DisplayTerm
u, NonEmpty 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 -> [Elim] -> m Expr -> m Expr
reifyDisplayForm QName
f [Elim]
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 -> [Elim] -> m (Maybe DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> [Elim] -> m (Maybe DisplayTerm)
displayForm QName
f [Elim]
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 -> [Elim] -> m (Maybe DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> [Elim] -> m (Maybe DisplayTerm)
displayForm QName
f ([Elim] -> m (Maybe DisplayTerm))
-> [Elim] -> m (Maybe DisplayTerm)
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ (Pattern' Expr)) -> Nat -> Elim)
-> Patterns -> [Nat] -> [Elim]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\ Arg (Named_ (Pattern' Expr))
p Nat
i -> Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Pattern' Expr))
p Arg (Named_ (Pattern' Expr)) -> 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" 95 $
      "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)
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 NonEmpty DisplayTerm
ds [Elim]
es ->
        DisplayTerm -> Bool
okDisplayForm DisplayTerm
d Bool -> Bool -> Bool
&& (DisplayTerm -> Bool) -> NonEmpty DisplayTerm -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DisplayTerm -> Bool
okDisplayTerm NonEmpty DisplayTerm
ds  Bool -> Bool -> Bool
&& (Elim -> Bool) -> [Elim] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim -> Bool
okToDropE [Elim]
es
        -- Andreas, 2016-05-03, issue #1950.
        -- We might drop trailing hidden trivial (=variable) patterns.
      DTerm' (I.Def QName
f [Elim]
es') [Elim]
es -> (Elim -> Bool) -> [Elim] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim -> Bool
okElim [Elim]
es' Bool -> Bool -> Bool
&& (Elim -> Bool) -> [Elim] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim -> Bool
okElim [Elim]
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 [Elim]
es -> [Elim] -> Bool
forall a. Null a => a -> Bool
null [Elim]
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 -> 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 -> 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 [Elim]
vs) = (Elim -> Bool) -> [Elim] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim -> Bool
okElim [Elim]
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 NonEmpty DisplayTerm
ds1 [Elim]
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) (NonEmpty DisplayTerm -> [Item (NonEmpty DisplayTerm)]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty DisplayTerm
ds1) [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++! (Elim -> Elim' DisplayTerm) -> [Elim] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Elim -> 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) [Elim]
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 [Elim]
es') [Elim]
es) = (QName
f, (Elim -> Elim' DisplayTerm) -> [Elim] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Elim -> 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) ([Elim] -> [Elim' DisplayTerm]) -> [Elim] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ [Elim]
es' [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
es, [])
    flattenWith DisplayTerm
_ = (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
forall a. HasCallStack => a
__IMPOSSIBLE__

    displayLHS
      :: A.Patterns   -- Patterns to substituted into display term.
      -> DisplayTerm  -- Display term.
      -> m (QName, A.Patterns, A.Patterns)  -- New head, patterns, with-patterns.
    displayLHS :: 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' Expr))))
-> [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 Elim' DisplayTerm -> m (Arg (Named_ (Pattern' Expr)))
elimToPat [Elim' DisplayTerm]
vs
        wps <- mapM (updateNamedArg (A.WithP empty) <.> elimToPat) es
        return (f, ps, wps)
      where
        argToPat :: Arg DisplayTerm -> m (NamedArg A.Pattern)
        argToPat :: Arg DisplayTerm -> m (Arg (Named_ (Pattern' Expr)))
argToPat Arg DisplayTerm
arg = (DisplayTerm -> m (Named_ (Pattern' Expr)))
-> Arg DisplayTerm -> m (Arg (Named_ (Pattern' 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 DisplayTerm -> m (Named_ (Pattern' Expr))
termToPat Arg DisplayTerm
arg

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

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

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

        termToPat (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)          = (Pattern' Expr -> Named_ (Pattern' Expr))
-> m (Pattern' Expr) -> m (Named_ (Pattern' Expr))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' Expr -> Named_ (Pattern' Expr)
forall a name. a -> Named name a
unnamed (m (Pattern' Expr) -> m (Named_ (Pattern' Expr)))
-> (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr
-> m (Named_ (Pattern' Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' Expr -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Pattern' Expr -> m (Pattern' Expr)
tryRecPFromConP (Pattern' Expr -> m (Named_ (Pattern' Expr)))
-> m (Pattern' Expr) -> m (Named_ (Pattern' Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
           ConPatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
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' Expr) -> m Patterns -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg DisplayTerm -> m (Arg (Named_ (Pattern' Expr))))
-> [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 Arg DisplayTerm -> m (Arg (Named_ (Pattern' Expr)))
argToPat [Arg DisplayTerm]
vs

        termToPat (DTerm' (I.Con ConHead
c ConInfo
ci [Elim]
vs) [Elim]
es) = (Pattern' Expr -> Named_ (Pattern' Expr))
-> m (Pattern' Expr) -> m (Named_ (Pattern' Expr))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' Expr -> Named_ (Pattern' Expr)
forall a name. a -> Named name a
unnamed (m (Pattern' Expr) -> m (Named_ (Pattern' Expr)))
-> (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr
-> m (Named_ (Pattern' Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' Expr -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Pattern' Expr -> m (Pattern' Expr)
tryRecPFromConP (Pattern' Expr -> m (Named_ (Pattern' Expr)))
-> m (Pattern' Expr) -> m (Named_ (Pattern' Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
           ConPatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
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' Expr) -> m Patterns -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
             (Elim -> m (Arg (Named_ (Pattern' Expr)))) -> [Elim] -> 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 (Elim' DisplayTerm -> m (Arg (Named_ (Pattern' Expr)))
elimToPat (Elim' DisplayTerm -> m (Arg (Named_ (Pattern' Expr))))
-> (Elim -> Elim' DisplayTerm)
-> Elim
-> m (Arg (Named_ (Pattern' Expr)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Elim -> 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) ([Elim]
vs [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
es)

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

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

        termToPat (DDot' Term
v [Elim]
es) =
          Pattern' Expr -> Named_ (Pattern' Expr)
forall a name. a -> Named name a
unnamed (Pattern' Expr -> Named_ (Pattern' Expr))
-> (Expr -> Pattern' Expr) -> Expr -> Named_ (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> Expr -> Pattern' Expr
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Named_ (Pattern' Expr))
-> m Expr -> m (Named_ (Pattern' Expr))
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
==<< (Term -> m Expr
termToExpr Term
v, [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify [Elim]
es)

        termToPat DisplayTerm
v =
          Pattern' Expr -> Named_ (Pattern' Expr)
forall a name. a -> Named name a
unnamed (Pattern' Expr -> Named_ (Pattern' Expr))
-> (Expr -> Pattern' Expr) -> Expr -> Named_ (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> Expr -> Pattern' Expr
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Named_ (Pattern' Expr))
-> m Expr -> m (Named_ (Pattern' Expr))
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 :: I.Args -> m [Arg A.Expr]
        argsToExpr :: 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 Term -> m Expr
termToExpr)

        -- TODO: restructure this to avoid having to repeat the code for reify
        termToExpr :: Term -> m A.Expr
        termToExpr :: 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 [Elim]
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 -> Maybe (Arg Term)) -> [Elim] -> 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 -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim [Elim]
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]
argsToExpr Args
vs
            I.Def QName
f [Elim]
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 -> Maybe (Arg Term)) -> [Elim] -> 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 -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim [Elim]
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]
argsToExpr Args
vs
            I.Var Nat
n [Elim]
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 -> Maybe (Arg Term)) -> [Elim] -> 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 -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim [Elim]
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 -> Expr
patternToExpr (Pattern' Expr -> Expr) -> Pattern' Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Pattern' Expr)) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg (Arg (Named_ (Pattern' Expr)) -> Pattern' Expr)
-> Arg (Named_ (Pattern' Expr)) -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Pattern' Expr))
-> Patterns -> Nat -> Arg (Named_ (Pattern' Expr))
forall a. a -> [a] -> Nat -> a
indexWithDefault Arg (Named_ (Pattern' Expr))
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 -> [Elim] -> m (QName, [Elim])
reifyPathPConstAsPath QName
x es :: [Elim]
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, [Elim]) -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show (QName
x,[Elim]
es)
   mpath  <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPath
   mpathp <- getBuiltinName' builtinPathP
   let fallback = (QName, [Elim]) -> m (QName, [Elim])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,[Elim]
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 t. Free t => Nat -> t -> 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, [Elim]) -> m (QName, [Elim])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
path, [Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply Arg Term
l, Arg Term -> Elim
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
forall a. Arg a -> Elim' a
I.Apply Arg Term
lhs, Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply Arg Term
rhs])
         Maybe Term
Nothing -> m (QName, [Elim])
fallback
     Maybe (QName, QName)
_ -> m (QName, [Elim])
fallback
reifyPathPConstAsPath QName
x [Elim]
es = (QName, [Elim]) -> m (QName, [Elim])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,[Elim]
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 (Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eFoldLetBindings) m Expr
fallback (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
  letBindings <- do
    binds  <- Map Name (Open LetBinding) -> [(Name, Open LetBinding)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map Name (Open LetBinding) -> [(Name, Open LetBinding)])
-> m (Map Name (Open LetBinding)) -> m [(Name, Open LetBinding)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv (Map Name (Open LetBinding))
-> m (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings
    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 _isAxiom 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 ::
      forall m. 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 <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
ePrintMetasBare
  reportS "reify.term" 80 $ "reifyTerm v0 = " <+> pretty v0
  v <- instantiate v0 >>= \case
    I.MetaV MetaId
x [Elim]
_ | 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 -> [Elim] -> 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
  reportS "reify.term" 80 $ "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
      ]
  reportS "reify.term" 80 $ "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 : [Elim]
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
=<< [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify [Elim]
es
    I.Var Nat
n [Elim]
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 :: * -> *). MonadTCEnv m => Nat -> m (Maybe Name)
nameOfBV' Nat
n
      elims (A.Var x) =<< reify es
    I.Def QName
x [Elim]
es -> do
      MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.def" Nat
80 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"reifying def" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
x
      (x, es) <- QName -> [Elim] -> m (QName, [Elim])
forall (m :: * -> *).
MonadReify m =>
QName -> [Elim] -> m (QName, [Elim])
reifyPathPConstAsPath QName
x [Elim]
es
      reifyDisplayForm x es $ reifyDef expandAnonDefs x es

    I.Con ConHead
c ConInfo
ci [Elim]
es -> do

      -- If the origin is a record expression, print a record expression.
      if ConInfo
ci ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec then Maybe (QName, RecordData) -> m Expr
recordExpression Maybe (QName, RecordData)
forall a. Maybe a
Nothing else do
        QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, 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) -> Maybe (QName, RecordData) -> m Expr
recordExpression (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 :: Maybe (QName, RecordData) -> m Expr
recordExpression 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 :: * -> *).
(HasCallStack, 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, Arg Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| Origin
ConversionFail Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Origin
argInfoOrigin (Arg Expr -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Expr
v) Bool -> Bool -> Bool
|| Dom' Term Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term Name
a
          A.Rec empty noExprInfo
            . map' (Left . uncurry FieldAssignment . first unDom . second unArg)
            . filter' keep
            . zip' (recordFieldNames def)
            <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims es)

        constructorApplication :: m Expr
constructorApplication = QName -> [Elim] -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> [Elim] -> m Expr -> m Expr
reifyDisplayForm QName
x [Elim]
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, HasCallStack) =>
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.
                    ((Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
-> Dom' Term (MetaNameSuggestion, Type) -> ArgInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo -> ArgInfo
info) : [Dom' Term (MetaNameSuggestion, Type)]
_) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
                      let us :: [Arg Expr]
us = [Dom' Term (MetaNameSuggestion, Type)]
-> (Dom' Term (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Nat
-> [Dom' Term (MetaNameSuggestion, Type)]
-> [Dom' Term (MetaNameSuggestion, Type)]
forall a. Nat -> [a] -> [a]
drop Nat
n [Dom' Term (MetaNameSuggestion, Type)]
pars) ((Dom' Term (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr])
-> (Dom' Term (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
forall a b. (a -> b) -> a -> b
$ \(Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
-> Dom' Term (MetaNameSuggestion, Type) -> ArgInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo -> 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' Term (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' Term
l      -> Level' Term -> m (ReifiesTo (Level' Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Level' Term -> m (ReifiesTo (Level' Term))
reify Level' Term
l
    I.Pi Dom Type
a Abs Type
b       -> case Abs Type
b of
      Abs Type
_ | Dom Type -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Dom Type
a, Dom Type -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a -> Term -> Abs Type -> m Expr -> m Expr
mkPartial (Type -> Term
forall t a. Type'' t a -> a
unEl (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) Abs Type
b (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> 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
=<< 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
      NoAbs MetaNameSuggestion
_ Type
b'
        | Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible 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).
        | 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 :: * -> *} {t} {t}.
(MonadTCEnv m, Free t, Free t) =>
t -> t -> 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
        mkPartial :: Term -> Abs I.Type -> m Expr -> m Expr
        mkPartial :: Term -> Abs Type -> m Expr -> m Expr
mkPartial (I.Def QName
io [I.Apply Arg Term
fm]) Abs Type
body m Expr
cont = do
          ion <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIsOne
          case reAbs body of
            Abs Type
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
io Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe QName
ion -> m Expr
cont
            NoAbs MetaNameSuggestion
_ Type
b' -> do
              pn <- 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
builtinPartial
              hd <- reify (I.Def pn [])
              apps hd =<< traverse reify [ fm, defaultArg (unEl b') ]
            Abs MetaNameSuggestion
nm Type
b' -> do
              pn <- 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
builtinPartialP
              hd <- reify (I.Def pn [])
              apps hd =<< traverse reify
                [ fm, defaultArg (I.Lam (setRelevance irrelevant defaultArgInfo) (Abs nm (unEl b'))) ]
        mkPartial Term
_ Abs Type
_ m Expr
fallback = m Expr
fallback

        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
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)
-> NonEmpty
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
 -> NonEmpty
      (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> NonEmpty
     (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 -> t -> m Bool
domainFree t
a t
b = do
          df <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
ePrintDomainFreePi
          return $! df && freeIn 0 b && closed a

        skipGeneralizedParameter :: ArgInfo -> m Bool
        skipGeneralizedParameter :: 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' Term
s     -> Sort' Term -> m (ReifiesTo (Sort' Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Sort' Term -> m (ReifiesTo (Sort' Term))
reify Sort' Term
s
    I.MetaV MetaId
x [Elim]
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
 -> Telescope
 -> Maybe (Substitution' Term)
 -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m CheckpointId
-> m (Telescope
      -> Maybe (Substitution' Term)
      -> (CheckpointId, Telescope, 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 (Telescope
   -> Maybe (Substitution' Term)
   -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m Telescope
-> m (Maybe (Substitution' Term)
      -> (CheckpointId, Telescope, 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 Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
                                    m (Maybe (Substitution' Term)
   -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (CheckpointId, Telescope, 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` Telescope -> [MetaNameSuggestion]
teleNames Telescope
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` (Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
meta_tel :: [Arg Term])
                     es_G :: [Elim]
es_G = Substitution' Term
Substitution' (SubstArg [Elim])
sub_local2G Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Elim]
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 -> Bool) -> Args -> [Elim] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Arg Term -> Elim -> Bool
forall {a} {a}.
(DeBruijn a, DeBruijn a) =>
Arg a -> Elim' a -> Bool
sameVar Args
args_G [Elim]
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 DummyTermKind
s [Elim]
es -> DummyTermKind -> [Elim] -> m Expr
forall {i} {m :: * -> *}.
(ReifiesTo i ~ [Elim' Expr], PureTCM m, MonadInteractionPoints m,
 MonadFresh NameId m, Reify i) =>
DummyTermKind -> i -> m Expr
reifyDummy DummyTermKind
s [Elim]
es
  where
    reifyDummy :: DummyTermKind -> i -> m Expr
reifyDummy DummyTermKind
kind i
es =
      case DummyTermKind
kind of
        I.DummyBrave Term
h -> m Expr -> m Expr
elims' (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)
        I.DummyNamed MetaNameSuggestion
s -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (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)) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m 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
es
      where
        elims' :: m Expr -> m Expr
elims' m Expr
a = do { h <- m Expr
a ; es <- reify es ; elims h es }
        asp :: OtherAspect -> Aspects
asp OtherAspect
o = Aspects
forall a. Null a => a
empty { Asp.otherAspects = Set.singleton o }

    -- 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 :: Bool -> QName -> I.Elims -> m Expr
    reifyDef :: Bool -> QName -> [Elim] -> m Expr
reifyDef Bool
True QName
x [Elim]
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 -> [Elim] -> m Expr
reifyDef' QName
x [Elim]
es) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
      r <- QName -> [Elim] -> m (Reduced () Term)
forall (m :: * -> *).
PureTCM m =>
QName -> [Elim] -> m (Reduced () Term)
reduceDefCopy QName
x [Elim]
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]
++! [Elim] -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show [Elim]
es
            ]
          QName -> [Elim] -> m Expr
reifyDef' QName
x [Elim]
es
    reifyDef Bool
_ QName
x [Elim]
es = QName -> [Elim] -> m Expr
reifyDef' QName
x [Elim]
es

    discontiguous :: I.Elims -> Bool
    discontiguous :: [Elim] -> Bool
discontiguous []              = Bool
False
    discontiguous (I.IApply{}:[Elim]
es) = [Elim] -> Bool
discontiguous [Elim]
es
    discontiguous (I.Proj{}:[Elim]
es)   = [Elim] -> Bool
discontiguous [Elim]
es
    discontiguous (I.Apply (Arg ArgInfo
info Term
_):[Elim]
es) =
      (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info Bool -> Bool -> Bool
&& Origin
ConversionFail Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Origin
argInfoOrigin ArgInfo
info) Bool -> Bool -> Bool
|| [Elim] -> Bool
discontiguous [Elim]
es

    reifyDef' :: QName -> I.Elims -> m Expr
    reifyDef' :: QName -> [Elim] -> m Expr
reifyDef' QName
x [Elim]
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 :: * -> *).
(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.
      showImp <- showImplicitArguments
      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
=<< [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify (Nat -> [Elim] -> [Elim]
forall a. Nat -> [a] -> [a]
drop Nat
n [Elim]
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 ([Arg (Named_ DeBruijnPattern)]
ps, Arg (Named_ DeBruijnPattern)
p) = ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
-> Maybe
     ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
-> ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
forall a. a -> Maybe a -> a
fromMaybe ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe
   ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
 -> ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern)))
-> Maybe
     ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
-> ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
forall a b. (a -> b) -> a -> b
$ [Arg (Named_ DeBruijnPattern)]
-> Maybe
     ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
forall a. [a] -> Maybe ([a], a)
initLast ([Arg (Named_ DeBruijnPattern)]
 -> Maybe
      ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern)))
-> [Arg (Named_ DeBruijnPattern)]
-> Maybe
     ([Arg (Named_ DeBruijnPattern)], Arg (Named_ DeBruijnPattern))
forall a b. (a -> b) -> a -> b
$ Clause -> [Arg (Named_ DeBruijnPattern)]
namedClausePats Clause
cl
                  let h :: Hiding
h = Arg (Named_ DeBruijnPattern) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Arg (Named_ DeBruijnPattern)
p
                      n :: Nat
n = [Arg (Named_ DeBruijnPattern)] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg (Named_ 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
> [Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
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 = (Arg (Named_ DeBruijnPattern) -> (ArgInfo, MetaNameSuggestion))
-> [Arg (Named_ DeBruijnPattern)]
-> [(ArgInfo, MetaNameSuggestion)]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg (Named_ DeBruijnPattern) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (Arg (Named_ DeBruijnPattern) -> ArgInfo)
-> (Arg (Named_ DeBruijnPattern) -> MetaNameSuggestion)
-> Arg (Named_ 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)
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> MetaNameSuggestion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) ([Arg (Named_ DeBruijnPattern)] -> [(ArgInfo, MetaNameSuggestion)])
-> [Arg (Named_ DeBruijnPattern)]
-> [(ArgInfo, MetaNameSuggestion)]
forall a b. (a -> b) -> a -> b
$ Nat
-> [Arg (Named_ DeBruijnPattern)] -> [Arg (Named_ DeBruijnPattern)]
forall a. Nat -> [a] -> [a]
drop ([Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
es) [Arg (Named_ 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
=<< [Elim] -> m (ReifiesTo [Elim])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
[Elim] -> m (ReifiesTo [Elim])
reify (Nat -> [Elim] -> [Elim]
forall a. Nat -> [a] -> [a]
drop Nat
n [Elim]
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))
-> (Telescope -> (Nat, Maybe System))
-> Telescope
-> 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))
-> (Telescope -> Nat) -> Telescope -> (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> Nat
forall a. Sized a => a -> Nat
size (Telescope -> Maybe (Nat, Maybe System))
-> m Telescope -> m (Maybe (Nat, Maybe System))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m Telescope
forall (m :: * -> *). ReadTCState m => ModuleName -> m Telescope
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 = [Arg (Named_ DeBruijnPattern)] -> Bool
hasDefP ([Arg (Named_ DeBruijnPattern)] -> Bool)
-> (Clause -> [Arg (Named_ DeBruijnPattern)]) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Arg (Named_ 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] -> [Elim] -> 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)) [Elim]
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' Term (MetaNameSuggestion, Type)
-> [Dom' Term (MetaNameSuggestion, Type)]
-> Dom' Term (MetaNameSuggestion, Type)
forall a. a -> [a] -> a
headWithDefault Dom' Term (MetaNameSuggestion, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom' Term (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' Term (MetaNameSuggestion, Type)]
-> (Dom' Term (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
-> [Arg (Named_ Expr)]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom' Term (MetaNameSuggestion, Type)]
as ((Dom' Term (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
 -> [Arg (Named_ Expr)])
-> (Dom' Term (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
-> [Arg (Named_ Expr)]
forall a b. (a -> b) -> a -> b
$ \ Dom' Term (MetaNameSuggestion, Type)
d -> let ai :: ArgInfo
ai = Dom' Term (MetaNameSuggestion, Type)
d Dom' Term (MetaNameSuggestion, Type)
-> Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (MetaNameSuggestion, Type)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo; x :: MetaNameSuggestion
x = (MetaNameSuggestion, Type) -> MetaNameSuggestion
forall a b. (a, b) -> a
fst (Dom' Term (MetaNameSuggestion, Type) -> (MetaNameSuggestion, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (MetaNameSuggestion, Type)
d) in
                    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 -> [Elim] -> [Elim]
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)) [Elim]
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' Term (MetaNameSuggestion, Type) -> Arg (Named_ Expr) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom' Term (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' Term (MetaNameSuggestion, Type) -> (MetaNameSuggestion, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (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 the conversion checker asked us to show an implicit
            -- argument that would otherwise be hidden, it might need to
            -- be named.
            Defn
_ | Bool -> Bool
not Bool
showImp Bool -> Bool -> Bool
&& [Elim] -> Bool
discontiguous [Elim]
es ->
              MaybeT m [Elim' (Named_ Term)] -> m (Maybe [Elim' (Named_ Term)])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (Bool -> Term -> Type -> [Elim] -> MaybeT m [Elim' (Named_ Term)]
nameElims Bool
False (QName -> [Elim] -> Term
I.Def QName
x []) (Definition -> Type
defType Definition
defn) (Nat -> [Elim] -> [Elim]
forall a. Nat -> [a] -> [a]
drop Nat
n [Elim]
es)) m (Maybe [Elim' (Named_ Term)])
-> (Maybe [Elim' (Named_ Term)]
    -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)]))
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Just [Elim' (Named_ Term)]
xs -> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [Elim' (Named_ Term)]
xs)
                Maybe [Elim' (Named_ Term)]
Nothing -> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], (Elim -> Elim' (Named_ Term)) -> [Elim] -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> Named_ Term) -> Elim -> 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) ([Elim] -> [Elim' (Named_ Term)])
-> [Elim] -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> a -> b
$ Nat -> [Elim] -> [Elim]
forall a. Nat -> [a] -> [a]
drop Nat
n [Elim]
es)

            -- Otherwise, 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 -> Elim' (Named_ Term)) -> [Elim] -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> Named_ Term) -> Elim -> 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) ([Elim] -> [Elim' (Named_ Term)])
-> [Elim] -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> a -> b
$ Nat -> [Elim] -> [Elim]
forall a. Nat -> [a] -> [a]
drop Nat
n [Elim]
es)

           reportS "reify.def" 100 $ 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
$ QName -> AmbiguousQName
unambiguous 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

    -- Name any 'ConversionFail' arguments that are in the wrong position in the spine.
    nameElims :: Bool -> I.Term -> I.Type -> I.Elims -> MaybeT m [Elim' (Named_ Term)]
    nameElims :: Bool -> Term -> Type -> [Elim] -> MaybeT m [Elim' (Named_ Term)]
nameElims Bool
_       Term
_   Type
_  []                   = [Elim' (Named_ Term)] -> MaybeT m [Elim' (Named_ Term)]
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    nameElims Bool
needs Term
acc Type
ty (I.IApply Term
_ Term
_ Term
tm:[Elim]
as) = Bool -> Term -> Type -> [Elim] -> MaybeT m [Elim' (Named_ Term)]
nameElims Bool
needs Term
acc Type
ty (Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
tm)Elim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:[Elim]
as)
    nameElims Bool
needs Term
acc Type
ty (elim :: Elim
elim@(I.Apply (Arg ArgInfo
info Term
tm)):[Elim]
as) =
      Type
-> (Type -> MaybeT m [Elim' (Named_ Term)])
-> (Dom Type -> Abs Type -> MaybeT m [Elim' (Named_ Term)])
-> MaybeT m [Elim' (Named_ Term)]
forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType Type
ty (\Type
_ -> MaybeT m [Elim' (Named_ Term)]
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero) \Dom Type
dom Abs Type
cod -> do
        let
          forced :: Bool
forced = ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info Bool -> Bool -> Bool
&& (Origin
ConversionFail Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Origin
argInfoOrigin ArgInfo
info)
          arg :: Elim' (Named_ Term)
arg = Arg (Named_ Term) -> Elim' (Named_ Term)
forall a. Arg a -> Elim' a
I.Apply if Bool
forced Bool -> Bool -> Bool
&& Bool
needs
            then ArgInfo -> Named_ Term -> Arg (Named_ Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe (WithOrigin (Ranged MetaNameSuggestion))
-> Term -> Named_ Term
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
$ Abs Type -> MetaNameSuggestion
forall a. Abs a -> MetaNameSuggestion
absName Abs Type
cod) Term
tm)
            else ArgInfo -> Named_ Term -> Arg (Named_ Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Named_ Term
forall a name. a -> Named name a
unnamed Term
tm)
        (Elim' (Named_ Term)
argElim' (Named_ Term)
-> [Elim' (Named_ Term)] -> [Elim' (Named_ Term)]
forall a. a -> [a] -> [a]
:) ([Elim' (Named_ Term)] -> [Elim' (Named_ Term)])
-> MaybeT m [Elim' (Named_ Term)] -> MaybeT m [Elim' (Named_ Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Term -> Type -> [Elim] -> MaybeT m [Elim' (Named_ Term)]
nameElims
          (if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info then Bool
False else Bool -> Bool
not Bool
forced)
          (Term
acc Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [Elim
elim]) (Abs Type
cod Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Term
SubstArg Type
tm) [Elim]
as
    nameElims Bool
_ Term
tm Type
ty (I.Proj ProjOrigin
o QName
n:[Elim]
as) = do
      ty <- Type -> MaybeT m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
      projectTyped tm ty o n >>= \case
        Maybe (Dom Type, Term, Type)
Nothing          -> MaybeT m [Elim' (Named_ Term)]
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
        Just (Dom Type
_, Term
tm, Type
ty) -> (ProjOrigin -> QName -> Elim' (Named_ Term)
forall a. ProjOrigin -> QName -> Elim' a
I.Proj ProjOrigin
o QName
nElim' (Named_ Term)
-> [Elim' (Named_ Term)] -> [Elim' (Named_ Term)]
forall a. a -> [a] -> [a]
:) ([Elim' (Named_ Term)] -> [Elim' (Named_ Term)])
-> MaybeT m [Elim' (Named_ Term)] -> MaybeT m [Elim' (Named_ Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Term -> Type -> [Elim] -> MaybeT m [Elim' (Named_ Term)]
nameElims Bool
False Term
tm Type
ty [Elim]
as

    -- 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
      :: QName -> ArgInfo -> Int -> Maybe System -> [I.Clause]
      -> I.Elims -> m Expr
    reifyExtLam :: QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> [Elim] -> m Expr
reifyExtLam QName
x ArgInfo
ai Nat
npars Maybe System
msys [Clause]
cls [Elim]
es = do
      MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.def" Nat
10 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"reifying extended lambda" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
x
      MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.def" Nat
50 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
        [ Doc Aspects
"npars =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Nat -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Nat
npars
        , Doc Aspects
"es    =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ((Elim -> Doc Aspects) -> [Elim] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat -> Elim -> Doc Aspects
forall a. Pretty a => Nat -> a -> Doc Aspects
prettyPrec Nat
10) [Elim]
es)
        , Doc Aspects
"def   =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ((Clause -> Doc Aspects) -> [Clause] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map' Clause -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [Clause]
cls) ]
      -- As extended lambda clauses live in the top level, we add the whole
      -- section telescope to the number of parameters.
      let ([Elim]
pares, [Elim]
rest) = Nat -> [Elim] -> ([Elim], [Elim])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars [Elim]
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
$ [Elim] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
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' LHS]
-> (System -> m [Clause' LHS])
-> m [Clause' LHS]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
               ((Clause -> m (Clause' LHS)) -> [Clause] -> m [Clause' LHS]
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' LHS)
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' LHS))
-> (Clause -> NamedClause) -> Clause -> m (Clause' LHS)
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' LHS]
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' LHS])
-> (System -> QNamed System) -> System -> m [Clause' LHS]
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' LHS]
cls of
            []       -> ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
NotHidden
            (Clause' LHS
cl:[Clause' LHS]
cls) -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 (Clause' LHS) -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo Erased
erased QName
x (Clause' LHS
cl Clause' LHS -> [Clause' LHS] -> List1 (Clause' LHS)
forall a. a -> [a] -> NonEmpty a
:| [Clause' LHS]
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
      | Origin
ConversionFail <- ArgInfo -> Origin
argInfoOrigin ArgInfo
info = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      | Bool
otherwise = (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' Expr)) -> Arg (Named_ (Pattern' Expr)))
-> Patterns -> Patterns
forall a b. (a -> b) -> [a] -> [b]
map' ((Named_ (Pattern' Expr) -> Named_ (Pattern' Expr))
-> Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ (Pattern' Expr) -> Named_ (Pattern' Expr)
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 -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.implicit" Nat
100 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Doc Aspects
"stripping implicits"
      , Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"ps   =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Patterns -> Doc Aspects
forall a. Show a => a -> Doc Aspects
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 -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.implicit" Nat
100 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"ps'  =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Patterns -> Doc Aspects
forall a. Show a => a -> Doc Aspects
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' Expr))
a : Patterns
as)
            -- A hidden non-UserWritten variable is removed if not needed for
            -- correct position of the following hidden arguments.
            | Arg (Named_ (Pattern' Expr)) -> Bool
canStrip Arg (Named_ (Pattern' Expr))
a =
                 if   (Arg (Named_ (Pattern' Expr)) -> Bool) -> Patterns -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Arg (Named_ (Pattern' Expr)) -> Bool
canStrip (Patterns -> Bool) -> Patterns -> Bool
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ (Pattern' Expr)) -> Bool) -> Patterns -> Patterns
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Arg (Named_ (Pattern' Expr)) -> 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' Expr)) -> Arg (Named_ (Pattern' Expr))
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos (Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
stripArg Arg (Named_ (Pattern' Expr))
a) Arg (Named_ (Pattern' Expr)) -> Patterns -> Patterns
forall a. a -> [a] -> [a]
: Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
as
            where
              a' :: Arg (Named_ (Pattern' Expr))
a'     = Arg (Named_ (Pattern' Expr))
-> Pattern' Expr -> Arg (Named_ (Pattern' Expr))
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg Arg (Named_ (Pattern' Expr))
a (Pattern' Expr -> Arg (Named_ (Pattern' Expr)))
-> Pattern' Expr -> Arg (Named_ (Pattern' Expr))
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP (PatInfo -> Pattern' Expr) -> PatInfo -> Pattern' Expr
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' Expr)) -> Range
forall a. HasRange a => a -> Range
getRange Arg (Named_ (Pattern' Expr))
a
              goWild :: Patterns
goWild = Bool
-> Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos Arg (Named_ (Pattern' Expr))
a' Arg (Named_ (Pattern' Expr)) -> 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' Expr)) -> Bool
canStrip Arg (Named_ (Pattern' Expr))
a = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ Arg (Named_ (Pattern' Expr)) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ (Pattern' Expr))
a
            , Arg (Named_ (Pattern' Expr)) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ (Pattern' Expr))
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' Expr))
-> Maybe (NameOf (Arg (Named_ (Pattern' Expr))))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf Arg (Named_ (Pattern' Expr))
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' Expr -> Bool
forall {e}. Pattern' e -> Bool
varOrDot (Arg (Named_ (Pattern' Expr)) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' Expr))
a)
            , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Bool
mustKeepVar (Arg (Named_ (Pattern' Expr)) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' Expr))
a)
            ]

          mustKeepVar :: Pattern' Expr -> 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' Expr
_                       = 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' Expr)) -> Arg (Named_ (Pattern' Expr))
stripArg Arg (Named_ (Pattern' Expr))
a = (Named_ (Pattern' Expr) -> Named_ (Pattern' Expr))
-> Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern' Expr -> Pattern' Expr)
-> Named_ (Pattern' Expr) -> Named_ (Pattern' Expr)
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' Expr -> Pattern' Expr
stripPat) Arg (Named_ (Pattern' Expr))
a

          stripPat :: Pattern' Expr -> Pattern' Expr
stripPat = \case
            p :: Pattern' Expr
p@(A.VarP BindName
_)        -> Pattern' Expr
p
            A.ConP ConPatInfo
i AmbiguousQName
c Patterns
ps       -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c (Patterns -> Pattern' Expr) -> Patterns -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Bool -> Patterns -> Patterns
stripArgs Bool
True Patterns
ps
            p :: Pattern' Expr
p@A.ProjP{}         -> Pattern' Expr
p
            p :: Pattern' Expr
p@(A.DefP PatInfo
_ AmbiguousQName
_ Patterns
_)    -> Pattern' Expr
p
            p :: Pattern' Expr
p@(A.DotP PatInfo
_ Expr
_e)     -> Pattern' Expr
p
            p :: Pattern' Expr
p@(A.WildP PatInfo
_)       -> Pattern' Expr
p
            p :: Pattern' Expr
p@(A.AbsurdP PatInfo
_)     -> Pattern' Expr
p
            p :: Pattern' Expr
p@(A.LitP PatInfo
_ Literal
_)      -> Pattern' Expr
p
            A.AsP PatInfo
i BindName
x Pattern' Expr
p         -> PatInfo -> BindName -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x (Pattern' Expr -> Pattern' Expr) -> Pattern' Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Pattern' Expr
stripPat Pattern' Expr
p
            A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> Pattern' Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
            A.RecP KwRange
kwr ConPatInfo
i [FieldAssignment' (Pattern' Expr)]
fs     -> KwRange
-> ConPatInfo
-> [FieldAssignment' (Pattern' Expr)]
-> Pattern' Expr
forall e.
KwRange
-> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP KwRange
kwr ConPatInfo
i ([FieldAssignment' (Pattern' Expr)] -> Pattern' Expr)
-> [FieldAssignment' (Pattern' Expr)] -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ (FieldAssignment' (Pattern' Expr)
 -> FieldAssignment' (Pattern' Expr))
-> [FieldAssignment' (Pattern' Expr)]
-> [FieldAssignment' (Pattern' Expr)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Pattern' Expr -> Pattern' Expr)
-> FieldAssignment' (Pattern' Expr)
-> FieldAssignment' (Pattern' Expr)
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' Expr -> Pattern' Expr
stripPat) [FieldAssignment' (Pattern' Expr)]
fs  -- TODO Andreas: is this right?
            p :: Pattern' Expr
p@A.EqualP{}        -> Pattern' Expr
p -- EqualP cannot be blanked.
            A.WithP PatInfo
i Pattern' Expr
p         -> PatInfo -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (Pattern' Expr -> Pattern' Expr) -> Pattern' Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Pattern' Expr
stripPat Pattern' Expr
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
|| (Arg (Named_ (Pattern' e)) -> Bool) -> NAPs e -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' e -> Bool
varOrDot (Pattern' e -> Bool)
-> (Arg (Named_ (Pattern' e)) -> Pattern' e)
-> Arg (Named_ (Pattern' e))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ (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 :: * -> *). 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
  reportS "reify.blank" 80 $ "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 c) => BlankVars (a, b, c) where
  blank :: Set Name -> (a, b, c) -> (a, b, c)
blank Set Name
bound (a
x, b
y, c
z) = (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, Set Name -> c -> c
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound c
z)

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' LHS -> Clause' LHS
blank Set Name
bound (A.Clause LHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Catchall
ca)
    | WhereDeclarations -> Bool
forall a. Null a => a -> Bool
null WhereDeclarations
wh =
        LHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' LHS
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> 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 Catchall
ca
    | Bool
otherwise = Clause' LHS
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 Arg (Named_ LHSCore)
b Patterns
ps) = (Arg (Named_ LHSCore) -> Patterns -> LHSCore)
-> (Arg (Named_ LHSCore), Patterns) -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AmbiguousQName -> Arg (Named_ LHSCore) -> Patterns -> LHSCore
forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSProj AmbiguousQName
p) ((Arg (Named_ LHSCore), Patterns) -> LHSCore)
-> (Arg (Named_ LHSCore), Patterns) -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name
-> (Arg (Named_ LHSCore), Patterns)
-> (Arg (Named_ LHSCore), Patterns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Arg (Named_ LHSCore)
b, Patterns
ps)
  blank Set Name
bound (A.LHSWith LHSCore
h NonEmpty (Arg (Pattern' Expr))
wps Patterns
ps) = ((LHSCore, NonEmpty (Arg (Pattern' Expr))) -> Patterns -> LHSCore)
-> ((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns) -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((LHSCore -> NonEmpty (Arg (Pattern' Expr)) -> Patterns -> LHSCore)
-> (LHSCore, NonEmpty (Arg (Pattern' Expr))) -> Patterns -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry LHSCore -> NonEmpty (Arg (Pattern' Expr)) -> Patterns -> LHSCore
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
A.LHSWith) (((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns) -> LHSCore)
-> ((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns) -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name
-> ((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns)
-> ((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound ((LHSCore
h, NonEmpty (Arg (Pattern' Expr))
wps), Patterns
ps)

instance BlankVars A.Pattern where
  blank :: Set Name -> Pattern' Expr -> Pattern' Expr
blank Set Name
bound Pattern' Expr
p = case Pattern' Expr
p of
    A.VarP BindName
_      -> Pattern' Expr
p   -- do not blank pattern vars
    A.ConP ConPatInfo
c AmbiguousQName
i Patterns
ps -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
c AmbiguousQName
i (Patterns -> Pattern' Expr) -> Patterns -> Pattern' Expr
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' Expr
p
    A.DefP PatInfo
i AmbiguousQName
f Patterns
ps -> PatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f (Patterns -> Pattern' Expr) -> Patterns -> Pattern' Expr
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' Expr
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
i (Expr -> Pattern' Expr) -> Expr -> Pattern' 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.WildP PatInfo
_     -> Pattern' Expr
p
    A.AbsurdP PatInfo
_   -> Pattern' Expr
p
    A.LitP PatInfo
_ Literal
_    -> Pattern' Expr
p
    A.AsP PatInfo
i BindName
n Pattern' Expr
p   -> PatInfo -> BindName -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
n (Pattern' Expr -> Pattern' Expr) -> Pattern' Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> Pattern' Expr -> Pattern' Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern' Expr
p
    A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> Pattern' Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.RecP KwRange
kwr ConPatInfo
i [FieldAssignment' (Pattern' Expr)]
fs -> KwRange
-> ConPatInfo
-> [FieldAssignment' (Pattern' Expr)]
-> Pattern' Expr
forall e.
KwRange
-> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP KwRange
kwr ConPatInfo
i ([FieldAssignment' (Pattern' Expr)] -> Pattern' Expr)
-> [FieldAssignment' (Pattern' Expr)] -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Set Name
-> [FieldAssignment' (Pattern' Expr)]
-> [FieldAssignment' (Pattern' Expr)]
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound [FieldAssignment' (Pattern' Expr)]
fs
    A.EqualP{}    -> Pattern' Expr
p
    A.WithP PatInfo
i Pattern' Expr
p   -> PatInfo -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (Set Name -> Pattern' Expr -> Pattern' Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern' Expr
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 NonEmpty Expr
es         -> (Expr -> NonEmpty Expr -> Expr) -> (Expr, NonEmpty Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> NonEmpty Expr -> Expr
A.WithApp ExprInfo
i) ((Expr, NonEmpty Expr) -> Expr) -> (Expr, NonEmpty Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, NonEmpty Expr) -> (Expr, NonEmpty Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, NonEmpty 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' LHS)
cs -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 (Clause' LHS) -> Expr
A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f (List1 (Clause' LHS) -> Expr) -> List1 (Clause' LHS) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> List1 (Clause' LHS) -> List1 (Clause' LHS)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound List1 (Clause' LHS)
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 KwRange
kwr ExprInfo
i RecordAssigns
es           -> KwRange -> ExprInfo -> RecordAssigns -> Expr
A.Rec KwRange
kwr ExprInfo
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 KwRange
kwr ExprInfo
i Expr
e [Assign]
es   -> (Expr -> [Assign] -> Expr) -> (Expr, [Assign]) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (KwRange -> ExprInfo -> Expr -> [Assign] -> Expr
A.RecUpdate KwRange
kwr ExprInfo
i) ((Expr, [Assign]) -> Expr) -> (Expr, [Assign]) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, [Assign]) -> (Expr, [Assign])
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, [Assign]
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
    A.Highlighted Aspects
q Expr
e        -> Aspects -> Expr -> Expr
A.Highlighted Aspects
q (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.Qualified ModuleName
q Expr
e          -> ModuleName -> Expr -> Expr
A.Qualified ModuleName
q (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

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' LHS)
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 NonEmpty
  (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
n Expr
e) = Range
-> TypedBindingInfo
-> NonEmpty
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t NonEmpty
  (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
_ Arg (Named_ LHSCore)
b Patterns
ps)   = (Arg (Named_ LHSCore), Patterns) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (Arg (Named_ LHSCore)
b, Patterns
ps)
  varsBoundIn (A.LHSWith LHSCore
h NonEmpty (Arg (Pattern' Expr))
wps Patterns
ps) = ((LHSCore, NonEmpty (Arg (Pattern' Expr))), Patterns) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn ((LHSCore
h, NonEmpty (Arg (Pattern' Expr))
wps), Patterns
ps)

instance Binder A.Pattern where
  varsBoundIn :: Pattern' Expr -> Set Name
varsBoundIn = (Pattern' (ADotT (Pattern' Expr)) -> Set Name)
-> Pattern' Expr -> Set Name
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern ((Pattern' (ADotT (Pattern' Expr)) -> Set Name)
 -> Pattern' Expr -> Set Name)
-> (Pattern' (ADotT (Pattern' Expr)) -> Set Name)
-> Pattern' Expr
-> 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' Expr))
_         -> Set Name
forall a. Null a => a
empty    -- Not x because of #2414 (?)
    A.ConP ConPatInfo
_ AmbiguousQName
_ NAPs (ADotT (Pattern' Expr))
_        -> 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' Expr))
_        -> 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' Expr))
_ -> Set Name
forall a. Null a => a
empty
    A.RecP KwRange
_ ConPatInfo
_ [FieldAssignment' (Pattern' (ADotT (Pattern' Expr)))]
_        -> Set Name
forall a. Null a => a
empty
    A.EqualP{}          -> Set Name
forall a. Null a => a
empty
    A.WithP PatInfo
_ Pattern' (ADotT (Pattern' Expr))
_         -> 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' Expr)
p BinderNameOrigin
_ a
n) = (Maybe (Pattern' Expr), a) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (Maybe (Pattern' Expr)
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
_ NonEmpty
  (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
xs Expr
_) = NonEmpty
  (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
-> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn NonEmpty
  (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
_ ArgInfo
_ Pattern' Expr
p Expr
_)= Pattern' Expr -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Pattern' Expr
p
  varsBoundIn LetApply{}          = Set Name
forall a. Null a => a
empty
  varsBoundIn LetOpen{}           = 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 =>
[Arg (Named_ DeBruijnPattern)] -> m Patterns
reifyPatterns = (Arg (Named_ DeBruijnPattern) -> m (Arg (Named_ (Pattern' Expr))))
-> [Arg (Named_ 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 ((Arg (Named_ DeBruijnPattern) -> m (Arg (Named_ (Pattern' Expr))))
 -> [Arg (Named_ DeBruijnPattern)] -> m Patterns)
-> (Arg (Named_ DeBruijnPattern)
    -> m (Arg (Named_ (Pattern' Expr))))
-> [Arg (Named_ DeBruijnPattern)]
-> m Patterns
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
forall p. NamedArg p -> NamedArg p
stripNameFromExplicit (Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr)))
-> (Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr)))
-> Arg (Named_ (Pattern' Expr))
-> Arg (Named_ (Pattern' Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr))
forall p. IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj) (Arg (Named_ (Pattern' Expr)) -> Arg (Named_ (Pattern' Expr)))
-> (Arg (Named_ DeBruijnPattern)
    -> m (Arg (Named_ (Pattern' Expr))))
-> Arg (Named_ DeBruijnPattern)
-> m (Arg (Named_ (Pattern' Expr)))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.>
                       (Named_ DeBruijnPattern -> m (Named_ (Pattern' Expr)))
-> Arg (Named_ DeBruijnPattern) -> m (Arg (Named_ (Pattern' 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 ((DeBruijnPattern -> m (Pattern' Expr))
-> Named_ DeBruijnPattern -> m (Named_ (Pattern' 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)
-> Named (WithOrigin (Ranged MetaNameSuggestion)) a
-> f (Named (WithOrigin (Ranged MetaNameSuggestion)) b)
traverse DeBruijnPattern -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
DeBruijnPattern -> m (Pattern' Expr)
reifyPat)
  where
    -- #4399 strip also empty names
    stripNameFromExplicit :: NamedArg p -> NamedArg p
    stripNameFromExplicit :: forall p. NamedArg p -> NamedArg p
stripNameFromExplicit Arg (Named_ p)
a
      | Arg (Named_ p) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ 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) (Arg (Named_ p) -> Maybe MetaNameSuggestion
forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged MetaNameSuggestion)) =>
a -> Maybe MetaNameSuggestion
bareNameOf Arg (Named_ p)
a) =
          (Named_ p -> Named_ p) -> Arg (Named_ p) -> Arg (Named_ 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_ p
forall a name. a -> Named name a
unnamed (p -> Named_ p) -> (Named_ p -> p) -> Named_ p -> Named_ p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ p -> p
forall name a. Named name a -> a
namedThing) Arg (Named_ p)
a
      | Bool
otherwise = Arg (Named_ p)
a

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

    reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern
    reifyPat :: forall (m :: * -> *).
MonadReify m =>
DeBruijnPattern -> m (Pattern' Expr)
reifyPat DeBruijnPattern
p = do
     MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.pat" Nat
80 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"reifying pattern" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> DeBruijnPattern -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
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' Expr)) -> m (Pattern' 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
          I.Lit Literal
l -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings [Name]
asB (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern' Expr
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
forall a. Null a => a
empty Literal
l
          Term
_       -> m (Pattern' Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
      I.VarP PatternInfo
i DBPatVar
x -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        o :: PatOrigin
o@PatOrigin
PatODot  -> Bool -> PatOrigin -> Term -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Bool -> PatOrigin -> Term -> m (Pattern' Expr)
reifyDotP Bool
keepVars PatOrigin
o (Term -> m (Pattern' Expr)) -> Term -> m (Pattern' Expr)
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' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOrigin
_          -> DBPatVar -> m (Pattern' Expr)
forall (m :: * -> *). MonadReify m => DBPatVar -> m (Pattern' Expr)
reifyVarP DBPatVar
x
      I.DotP PatternInfo
i Term
v -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOrigin
PatOWild   -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
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 :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
nameOfBV Nat
i
          if nameConcrete x == nameConcrete x' then
            return $! A.VarP $ mkBindName x'
          else
            reifyDotP keepVars o v
        PatOrigin
o -> Bool -> PatOrigin -> Term -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Bool -> PatOrigin -> Term -> m (Pattern' Expr)
reifyDotP Bool
keepVars PatOrigin
o Term
v
      I.LitP LitPatternInfo
i Literal
l  -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames (LitPatternInfo -> PatternInfo
litPInfo LitPatternInfo
i)) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern' Expr
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
forall a. Null a => a
empty Literal
l
      I.ProjP ProjOrigin
o QName
d -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$! PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' Expr
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
o (AmbiguousQName -> Pattern' Expr)
-> AmbiguousQName -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d
      I.ConP ConHead
c ConPatternInfo
cpi [Arg (Named_ DeBruijnPattern)]
ps | ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$
        case PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) of
          PatOrigin
PatOWild   -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
          PatOrigin
PatOAbsurd -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
          PatOVar Name
x | Bool
keepVars -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern' Expr) -> BindName -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
          PatOrigin
_               -> ConHead
-> ConPatternInfo
-> [Arg (Named_ DeBruijnPattern)]
-> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo
-> [Arg (Named_ DeBruijnPattern)]
-> m (Pattern' Expr)
reifyConP ConHead
c ConPatternInfo
cpi [Arg (Named_ DeBruijnPattern)]
ps
      I.ConP ConHead
c ConPatternInfo
cpi [Arg (Named_ DeBruijnPattern)]
ps -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ ConHead
-> ConPatternInfo
-> [Arg (Named_ DeBruijnPattern)]
-> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo
-> [Arg (Named_ DeBruijnPattern)]
-> m (Pattern' Expr)
reifyConP ConHead
c ConPatternInfo
cpi [Arg (Named_ DeBruijnPattern)]
ps
      I.DefP PatternInfo
i QName
f [Arg (Named_ DeBruijnPattern)]
ps  -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        PatOrigin
PatOWild   -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOVar Name
x | Bool
keepVars -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern' Expr) -> BindName -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
        PatOrigin
_ -> PatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
patNoRange (QName -> AmbiguousQName
unambiguous QName
f) (Patterns -> Pattern' Expr) -> m Patterns -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg (Named_ DeBruijnPattern)] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[Arg (Named_ DeBruijnPattern)] -> m Patterns
reifyPatterns [Arg (Named_ DeBruijnPattern)]
ps
      I.IApplyP PatternInfo
i Term
_ Term
_ DBPatVar
x -> [Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *).
Functor m =>
[Name] -> m (Pattern' Expr) -> m (Pattern' Expr)
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) (m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
        o :: PatOrigin
o@PatOrigin
PatODot  -> Bool -> PatOrigin -> Term -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Bool -> PatOrigin -> Term -> m (Pattern' Expr)
reifyDotP Bool
keepVars PatOrigin
o (Term -> m (Pattern' Expr)) -> Term -> m (Pattern' Expr)
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' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
        PatOrigin
PatOAbsurd -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
        PatOrigin
_          -> DBPatVar -> m (Pattern' Expr)
forall (m :: * -> *). MonadReify m => DBPatVar -> m (Pattern' Expr)
reifyVarP DBPatVar
x

    reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
    reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m (Pattern' Expr)
reifyVarP DBPatVar
x = do
      n <- Nat -> m Name
forall (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 => Bool -> PatOrigin -> Term -> m A.Pattern
    reifyDotP :: forall (m :: * -> *).
MonadReify m =>
Bool -> PatOrigin -> Term -> m (Pattern' Expr)
reifyDotP Bool
keepVars PatOrigin
o Term
v = do
      if | PatOVar Name
x <- PatOrigin
o , Bool
keepVars       -> Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' Expr -> m (Pattern' Expr))
-> Pattern' Expr -> m (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$! BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern' Expr) -> BindName -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
         | PatOSplitArg MetaNameSuggestion
x <- PatOrigin
o , Bool
keepVars  -> BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern' Expr)
-> (Name -> BindName) -> Name -> Pattern' Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName (Name -> Pattern' Expr) -> m Name -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> MetaNameSuggestion -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> MetaNameSuggestion -> m Name
freshName Range
forall a. Range' a
noRange MetaNameSuggestion
x
         | Bool
otherwise                       -> PatInfo -> Expr -> Pattern' Expr
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Pattern' Expr) -> m Expr -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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

    reifyConP :: MonadReify m
              => ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
              -> m A.Pattern
    reifyConP :: forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo
-> [Arg (Named_ DeBruijnPattern)]
-> m (Pattern' Expr)
reifyConP ConHead
c ConPatternInfo
cpi [Arg (Named_ DeBruijnPattern)]
ps = do
      Pattern' Expr -> m (Pattern' Expr)
forall (m :: * -> *).
MonadReify m =>
Pattern' Expr -> m (Pattern' Expr)
tryRecPFromConP (Pattern' Expr -> m (Pattern' Expr))
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do ConPatInfo -> AmbiguousQName -> Patterns -> Pattern' Expr
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
ci (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) (Patterns -> Pattern' Expr) -> m Patterns -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg (Named_ DeBruijnPattern)] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[Arg (Named_ DeBruijnPattern)] -> m Patterns
reifyPatterns [Arg (Named_ 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' Expr) -> m (Pattern' Expr)
addAsBindings [Name]
xs m (Pattern' Expr)
p = (Name -> m (Pattern' Expr) -> m (Pattern' Expr))
-> m (Pattern' Expr) -> [Name] -> m (Pattern' Expr)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Pattern' Expr -> Pattern' Expr)
-> m (Pattern' Expr) -> m (Pattern' Expr)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern' Expr -> Pattern' Expr)
 -> m (Pattern' Expr) -> m (Pattern' Expr))
-> (Name -> Pattern' Expr -> Pattern' Expr)
-> Name
-> m (Pattern' Expr)
-> m (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatInfo -> BindName -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
patNoRange (BindName -> Pattern' Expr -> Pattern' Expr)
-> (Name -> BindName) -> Name -> Pattern' Expr -> Pattern' Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName) m (Pattern' Expr)
p [Name]
xs

{-# SPECIALIZE reifyRecordFields :: SmallSet Origin -> RecordData -> (NamedArg A.Pattern -> A.Pattern) -> [NamedArg A.Pattern] -> TCM [FieldAssignment' A.Pattern] #-}
{-# SPECIALIZE reifyRecordFields :: SmallSet Origin -> RecordData -> (Arg Expr -> Expr) -> [Arg Expr] -> TCM [FieldAssignment' Expr] #-}
-- | Pair the fields of a record type with the arguments of its constructor,
--   producing the field assignments of a record pattern or record expression.
--
--   Andreas, 2025-09-29, issue #8787:
--   Invisible (hidden and instance) fields are dropped unless @--show-implicit@ is on.
--   This conforms the printing of records to the printing of applications
--   of a record constructor (see 'stripImplicits' and 'nelims').
reifyRecordFields :: (MonadReify m, LensOrigin a)
  => SmallSet Origin  -- ^ Set of origins that make us keep an invisible field anyway.
  -> RecordData       -- ^ Definition of the record type, supplying the field names.
  -> (a -> e)         -- ^ How to extract the content of a constructor argument.
  -> [a]              -- ^ The arguments of the record constructor.
  -> m [FieldAssignment' e]
reifyRecordFields :: forall (m :: * -> *) a e.
(MonadReify m, LensOrigin a) =>
SmallSet Origin
-> RecordData -> (a -> e) -> [a] -> m [FieldAssignment' e]
reifyRecordFields SmallSet Origin
keepOrigins RecordData
def a -> e
content [a]
args = 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
== [a] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
args) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
  let keep (Dom' Term Name
f, a
a) = Dom' Term Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term Name
f Bool -> Bool -> Bool
|| a -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin a
a Origin -> SmallSet Origin -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` SmallSet Origin
keepOrigins
  return $! map' (\ (Dom' Term Name
f, a
a) -> Name -> e -> FieldAssignment' e
forall a. Name -> a -> FieldAssignment' a
FieldAssignment (Dom' Term Name -> Name
forall t e. Dom' t e -> e
unDom Dom' Term Name
f) (a -> e
content a
a))
         $  applyUnless showImp (filter' keep)
         $  zip' fs args

{-# 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' Expr -> m (Pattern' Expr)
tryRecPFromConP Pattern' Expr
p = do
  let fallback :: m (Pattern' Expr)
fallback = Pattern' Expr -> m (Pattern' Expr)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' Expr
p
  case Pattern' Expr
p of
    A.ConP ConPatInfo
ci AmbiguousQName
c Patterns
ps -> do
        MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.pat" Nat
60 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"tryRecPFromConP" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> AmbiguousQName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty AmbiguousQName
c
        m (Maybe (QName, RecordData))
-> m (Pattern' Expr)
-> ((QName, RecordData) -> m (Pattern' Expr))
-> m (Pattern' 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 :: * -> *).
(HasCallStack, 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' Expr)
fallback (((QName, RecordData) -> m (Pattern' Expr)) -> m (Pattern' Expr))
-> ((QName, RecordData) -> m (Pattern' Expr)) -> m (Pattern' 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 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' Expr)
fallback else
            -- Andreas, 2025-09-29, issue #8787: Keep the invisible fields
            -- the user wrote, just like 'stripImplicits' does for constructor patterns.
            KwRange
-> ConPatInfo
-> [FieldAssignment' (Pattern' Expr)]
-> Pattern' Expr
forall e.
KwRange
-> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP KwRange
forall a. Null a => a
empty ConPatInfo
ci ([FieldAssignment' (Pattern' Expr)] -> Pattern' Expr)
-> m [FieldAssignment' (Pattern' Expr)] -> m (Pattern' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SmallSet Origin
-> RecordData
-> (Arg (Named_ (Pattern' Expr)) -> Pattern' Expr)
-> Patterns
-> m [FieldAssignment' (Pattern' Expr)]
forall (m :: * -> *) a e.
(MonadReify m, LensOrigin a) =>
SmallSet Origin
-> RecordData -> (a -> e) -> [a] -> m [FieldAssignment' e]
reifyRecordFields SmallSet Origin
recordPatternKeeperOrigins RecordData
def Arg (Named_ (Pattern' Expr)) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg Patterns
ps
    Pattern' Expr
_ -> m (Pattern' Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 'Origin' values (e.g. 'UserWritten') that indicate an implicit record field
--   should be kept during printing of a record pattern.
recordPatternKeeperOrigins :: SmallSet Origin
recordPatternKeeperOrigins :: SmallSet Origin
recordPatternKeeperOrigins = [Origin] -> SmallSet Origin
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [ Origin
UserWritten, Origin
CaseSplit ]

-- | 'Origin' values (e.g. 'ConversionFail') that indicate an implicit record field
--   should be kept during printing of a record expression.
recordExpressionKeeperOrigins :: SmallSet Origin
recordExpressionKeeperOrigins :: SmallSet Origin
recordExpressionKeeperOrigins = [Origin] -> SmallSet Origin
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [ Origin
ConversionFail ]

{-# 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 -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.expr" Nat
60 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"recOrCon" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty 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 :: * -> *).
(HasCallStack, 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
&& ConInfo
co ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= ConInfo
ConORec then m Expr
fallback else
      -- Andreas, 2025-09-29, issue #8787: Keep the invisible fields
      -- the conversion checker insists on, just like 'nelims' does for applications.
      KwRange -> ExprInfo -> RecordAssigns -> Expr
A.Rec KwRange
forall a. Null a => a
empty ExprInfo
forall a. Null a => a
empty (RecordAssigns -> Expr)
-> ([Assign] -> RecordAssigns) -> [Assign] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assign -> RecordAssign) -> [Assign] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map' Assign -> RecordAssign
forall a b. a -> Either a b
Left ([Assign] -> Expr) -> m [Assign] -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SmallSet Origin
-> RecordData -> (Arg Expr -> Expr) -> [Arg Expr] -> m [Assign]
forall (m :: * -> *) a e.
(MonadReify m, LensOrigin a) =>
SmallSet Origin
-> RecordData -> (a -> e) -> [a] -> m [FieldAssignment' e]
reifyRecordFields SmallSet Origin
recordExpressionKeeperOrigins RecordData
def Arg Expr -> Expr
forall e. Arg e -> e
unArg [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

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) = Telescope -> m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Clause -> Telescope
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 -> Doc Aspects -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
MetaNameSuggestion -> Nat -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
MetaNameSuggestion -> Nat -> Doc Aspects -> m ()
reportS MetaNameSuggestion
"reify.clause" Nat
60 (Doc Aspects -> m ()) -> Doc Aspects -> m ()
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
      [ Doc Aspects
"reifying NamedClause"
      , Doc Aspects
"  f      =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
f
      , Doc Aspects
"  toDrop =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Doc Aspects
forall a. Show a => a -> Doc Aspects
pshow Bool
toDrop
      , Doc Aspects
"  cl     =" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Clause -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Clause
cl
      ]

    let clBody :: Maybe Term
clBody = Clause -> Maybe Term
clauseBody Clause
cl
        rhsVars :: [Nat]
rhsVars = Maybe Term -> [Nat]
forall t. Free t => t -> [Nat]
freeVarList 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]

    reportS "reify.clause" 60 $ "RHS:" <+> pretty clBody
    reportS "reify.clause" 60 $ "variables occurring on RHS:" <+> pretty rhsVars
      <+> "variable names:" <+> pretty rhsVarNames
      <+> parens (maybe "no clause body" (const "there was a clause body") clBody)
    reportS "reify.clause" 60 $ "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 -> Telescope -> Nat
forall a. Sized a => a -> Nat
size (Telescope -> Nat) -> m Telescope -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m Telescope
forall (m :: * -> *). ReadTCState m => ModuleName -> m Telescope
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
-> Catchall
-> Clause' LHS
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
A.Clause (SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls (Clause -> Catchall
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 Telescope
tel [(Face, Term)]
sys)) = Telescope
-> 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 =>
Telescope -> m a -> m a
addContext Telescope
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
$ Telescope -> MetaNameSuggestion
forall a. Show a => a -> MetaNameSuggestion
show Telescope
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
forallM 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 <- [Arg (Named_ DeBruijnPattern)] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[Arg (Named_ DeBruijnPattern)] -> m Patterns
reifyPatterns ([Arg (Named_ DeBruijnPattern)] -> m Patterns)
-> [Arg (Named_ DeBruijnPattern)] -> m Patterns
forall a b. (a -> b) -> a -> b
$ Telescope -> [Arg (Named_ DeBruijnPattern)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
tel
      ps <- List1.ifNull alpha (pure ps) {-else-} \ List1 (Term, Bool)
alpha -> do
        ep <- (NonEmpty (Expr, Expr) -> Pattern' Expr)
-> m (NonEmpty (Expr, Expr)) -> m (Pattern' Expr)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatInfo -> NonEmpty (Expr, Expr) -> Pattern' Expr
forall e. PatInfo -> List1 (e, e) -> Pattern' e
A.EqualP PatInfo
patNoRange) (m (NonEmpty (Expr, Expr)) -> m (Pattern' Expr))
-> (((Term, Bool) -> m (Expr, Expr)) -> m (NonEmpty (Expr, Expr)))
-> ((Term, Bool) -> m (Expr, Expr))
-> m (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Term, Bool)
-> ((Term, Bool) -> m (Expr, Expr)) -> m (NonEmpty (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' Expr))
-> ((Term, Bool) -> m (Expr, Expr)) -> m (Pattern' Expr)
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 empty
{-# 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
_ 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' Term -> m (ReifiesTo (Sort' Term))
reifyWhen = Bool -> Sort' Term -> m (ReifiesTo (Sort' Term))
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE

    reify :: forall (m :: * -> *).
MonadReify m =>
Sort' Term -> m (ReifiesTo (Sort' Term))
reify Sort' Term
s = do
      s <- Sort' Term -> m (Sort' Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort' Term
s
      SortKit{ nameOfUniv } <- 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' Term
a -> do
          a <- Level' Term -> m (ReifiesTo (Level' Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Level' Term -> m (ReifiesTo (Level' Term))
reify Level' Term
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' Term
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' Term
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' Term
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' Term
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' Term
s1 Abs (Sort' Term)
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' Term
s1 Sort' Term
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' Term
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 [Elim]
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 -> [Elim] -> Term
I.MetaV MetaId
x [Elim]
es
        I.DefS QName
d [Elim]
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 -> [Elim] -> Term
I.Def QName
d [Elim]
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' Term -> m (ReifiesTo (Level' Term))
reifyWhen = Bool -> Level' Term -> m (ReifiesTo (Level' Term))
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *).
MonadReify m =>
Level' Term -> m (ReifiesTo (Level' Term))
reify Level' Term
l   = m Bool
-> m (ReifiesTo (Level' Term))
-> m (ReifiesTo (Level' Term))
-> m (ReifiesTo (Level' Term))
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' Term -> m Term
forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l) (m (ReifiesTo (Level' Term)) -> m (ReifiesTo (Level' Term)))
-> m (ReifiesTo (Level' Term)) -> m (ReifiesTo (Level' Term))
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 t. Free t => Nat -> t -> 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 =>
Telescope -> m (ReifiesTo Telescope)
reify Telescope
EmptyTel = [TypedBinding] -> m [TypedBinding]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  reify (ExtendTel Dom Type
arg Abs Telescope
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)
-> NonEmpty
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
 -> NonEmpty
      (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> NonEmpty
     (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 i
d = ArgInfo -> ReifiesTo i -> Arg (ReifiesTo i)
forall e. ArgInfo -> e -> Arg e
Arg (Dom i
d Dom i -> Getting ArgInfo (Dom i) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom i) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) (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 (Dom i -> i
forall t e. Dom' t e -> e
unDom Dom i
d)
    {-# INLINE reify #-}

instance Reify Context where
  type ReifiesTo Context = [A.TypedBinding]

  reify :: forall (m :: * -> *).
MonadReify m =>
Context -> m (ReifiesTo Context)
reify = Telescope -> m [TypedBinding]
Telescope -> m (ReifiesTo Telescope)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Telescope -> m (ReifiesTo Telescope)
reify (Telescope -> m [TypedBinding])
-> (Context -> Telescope) -> Context -> m [TypedBinding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Telescope
contextToTel

instance Reify ContextEntry where
  type ReifiesTo ContextEntry = A.TypedBinding

  reify :: forall (m :: * -> *).
MonadReify m =>
ContextEntry -> m (ReifiesTo ContextEntry)
reify (CtxVar Name
x Dom Type
a) = do
    Arg info (y,t) <- Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
reify (Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type))))
-> Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
forall a b. (a -> b) -> a -> b
$ (Name
x,) (Type -> (Name, Type)) -> Dom Type -> Dom' Term (Name, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a
    let r = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
        name = Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
forall t e.
Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
domName Dom Type
a
        xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> NonEmpty
     (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
 -> NonEmpty
      (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
-> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
-> NonEmpty
     (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
y
    tac <- TacticAttribute <$> do traverse (Ranged noRange <.> reify) $ domTactic a
    return $! TBind r (TypedBindingInfo tac (domIsFinite a)) xs t

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