{-# LANGUAGE NondecreasingIndentation   #-}

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

    TODO

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

import Prelude hiding (null)

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

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

import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A hiding (Binder)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.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.Telescope

import Agda.Interaction.Options

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

import Agda.Utils.Impossible


-- | Like @reify@ but instantiates blocking metas, useful for reporting.
reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked :: forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked i
t = Lens' Bool TCState
-> (Bool -> Bool) -> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
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)
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

-- | 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 ------------------------------------

-- | 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 (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 (Named_ Expr)
arg <- Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Arg (Named_ Expr)
arg  -- This replaces the arg by _ if irrelevant
  Bool
dontShowImp <- 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
showImplicitArguments
  let hd :: Expr
hd | Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Expr)
arg Bool -> Bool -> Bool
&& Bool
dontShowImp = Expr
e
         | Bool
otherwise                     = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e Arg (Named_ Expr)
arg
  Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
hd [Elim' (Named_ Expr)]
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

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

-- | 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 (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 --------------

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)
reify i
i
reifyWhenE Bool
False i
t = ReifiesTo i -> m (ReifiesTo i)
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)
reify

instance Reify Bool where
    type ReifiesTo Bool = Bool
    reify :: forall (m :: * -> *). MonadReify m => Bool -> m (ReifiesTo Bool)
reify = Bool -> m (ReifiesTo Bool)
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 (ReifiesTo Name)
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 (ReifiesTo Expr)
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 x :: MetaId
x@(MetaId Nat
n) = do
      Bool
b <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
      MetaInfo
mi  <- MetaVariable -> MetaInfo
mvInfo (MetaVariable -> MetaInfo) -> m MetaVariable -> m MetaInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
      let mi' :: MetaInfo
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 :: String
metaNameSuggestion = if Bool
b then String
"" else MetaInfo -> String
miNameSuggestion MetaInfo
mi
                 }
          underscore :: m Expr
underscore = Expr -> m Expr
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
      MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
x m (Maybe InteractionId)
-> (Maybe InteractionId -> m Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe InteractionId
Nothing | Bool
b -> do
          InteractionId
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
          InteractionId -> MetaId -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
x
          Expr -> m Expr
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
        Just InteractionId
ii | Bool
b -> m Expr
underscore
        Maybe InteractionId
Nothing     -> m Expr
underscore
        Just InteractionId
ii     -> Expr -> m Expr
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

-- Does not print with-applications correctly:
-- instance Reify DisplayTerm Expr where
--   reifyWhen = reifyWhenE
--   reify d = reifyTerm False $ dtermToTerm d

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 -> Bool -> Term -> m Expr
forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
False Term
v
    DDot  Term
v -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
    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)
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)
reify [Elim' DisplayTerm]
es
    DWithApp DisplayTerm
u [DisplayTerm]
us Elims
es0 -> do
      (Expr
e, [Expr]
es) <- (DisplayTerm, [DisplayTerm])
-> m (ReifiesTo (DisplayTerm, [DisplayTerm]))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (DisplayTerm
u, [DisplayTerm]
us)
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (if [Expr] -> Bool
forall a. Null a => a -> Bool
null [Expr]
es then Expr
e else ExprInfo -> Expr -> [Expr] -> Expr
A.WithApp ExprInfo
noExprInfo Expr
e [Expr]
es) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es0

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

-- | @reifyDisplayFormP@ tries to recursively
--   rewrite a lhs with a display form.
--
--   Note: we are not necessarily in the empty context upon entry!
reifyDisplayFormP
  :: 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 (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?
    Maybe DisplayTerm
md <- -- addContext (replicate (length ps) "x") $
      QName -> Elims -> m (Maybe DisplayTerm)
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f (Elims -> m (Maybe DisplayTerm)) -> Elims -> m (Maybe DisplayTerm)
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Nat -> Elim' Term)
-> Patterns -> [Nat] -> Elims
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg (Named_ Pattern)
p Nat
i -> Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern)
p Arg (Named_ Pattern) -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
I.var Nat
i) Patterns
ps [Nat
0..]
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$
      String
"display form of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show Patterns
ps String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show Patterns
wps String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe DisplayTerm -> String
forall a. Show a => a -> String
show Maybe DisplayTerm
md
    case Maybe DisplayTerm
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?
        (QName
f', Patterns
ps', Patterns
wps') <- Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
forall (m :: * -> *).
MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d
        String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.display" Nat
70 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ do
          Doc
doc <- SpineLHS -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (SpineLHS -> TCM Doc) -> SpineLHS -> TCM Doc
forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
f' (Patterns
ps' Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
wps' Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
wps)
          Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
            [ Doc
"rewritten lhs to"
            , Doc
"  lhs' = " Doc -> Doc -> Doc
<+> Doc
doc
            ]
        QName -> Patterns -> Patterns -> m (QName, Patterns)
forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f' Patterns
ps' (Patterns
wps' Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
wps)
      Maybe DisplayTerm
_ -> do
        String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
70 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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 (DWithApp DisplayTerm
d [DisplayTerm]
ds Elims
es) =
      DisplayTerm -> Bool
okDisplayForm DisplayTerm
d Bool -> Bool -> Bool
&& (DisplayTerm -> Bool) -> [DisplayTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DisplayTerm -> Bool
okDisplayTerm [DisplayTerm]
ds  Bool -> Bool -> Bool
&& (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okToDropE Elims
es
      -- Andreas, 2016-05-03, issue #1950.
      -- We might drop trailing hidden trivial (=variable) patterns.
    okDisplayForm (DTerm (I.Def QName
f Elims
vs)) = (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
    okDisplayForm (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
    okDisplayForm DDot{}               = Bool
False
    okDisplayForm DCon{}               = Bool
False
    okDisplayForm DTerm{}              = Bool
False

    okDisplayTerm :: DisplayTerm -> Bool
    okDisplayTerm :: DisplayTerm -> Bool
okDisplayTerm (DTerm Term
v) = Term -> Bool
okTerm Term
v
    okDisplayTerm DDot{}    = Bool
True
    okDisplayTerm DCon{}    = Bool
True
    okDisplayTerm DDef{}    = Bool
False
    okDisplayTerm DisplayTerm
_         = Bool
False

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
        argsToExpr :: forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr = (Arg Term -> m (Arg Expr)) -> Args -> m [Arg Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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)
traverse Term -> m Expr
forall (m :: * -> *). MonadReify m => Term -> m Expr
termToExpr)

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

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

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

reifyTerm :: MonadReify m => Bool -> Term -> m Expr
reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
expandAnonDefs0 Term
v0 = do
  -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
  Bool
metasBare <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
  Term
v <- Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v0 m Term -> (Term -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    I.MetaV MetaId
x Elims
_ | Bool
metasBare -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x []
    Term
v -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
  -- (i.e. when we don't care about nice printing)
  Bool
expandAnonDefs <- Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
expandAnonDefs0 m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled
  -- Andreas, 2016-07-21 if --postfix-projections
  -- then we print system-generated projections as postfix, else prefix.
  Bool
havePfp <- PragmaOptions -> Bool
optPostfixProjections (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
  let pred :: ProjOrigin -> Bool
pred = if Bool
havePfp then (ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPrefix) else (ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPostfix)
  case (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
pred Term
v of
    -- Hack to print generalized field projections with nicer names. Should
    -- only show up in errors. Check the spined form!
    Term
_ | I.Var Nat
n (I.Proj ProjOrigin
_ QName
p : Elims
es) <- Term
v,
        Just String
name <- QName -> Maybe String
getGeneralizedFieldName QName
p -> do
      let fakeName :: Name
fakeName = (QName -> Name
qnameName QName
p) {nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
name} -- TODO: infix names!?
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
fakeName) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
    I.Var Nat
n Elims
es -> do
      Name
x <- m Name -> m (Maybe Name) -> m Name
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String -> m Name) -> String -> m Name
forall a b. (a -> b) -> a -> b
$ String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show Nat
n) (m (Maybe Name) -> m Name) -> m (Maybe Name) -> m Name
forall a b. (a -> b) -> a -> b
$ Nat -> m (Maybe Name)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Maybe Name)
nameOfBV' Nat
n
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
x) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
    I.Def QName
x Elims
es -> do
      String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.def" Nat
80 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reifying def" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
      (QName
x, Elims
es) <- QName -> Elims -> m (QName, Elims)
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x Elims
es
      QName -> Elims -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
es (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
Bool -> QName -> Elims -> m Expr
reifyDef Bool
expandAnonDefs QName
x Elims
es
    I.Con ConHead
c ConInfo
ci Elims
vs -> do
      let x :: QName
x = ConHead -> QName
conName ConHead
c
      Bool
isR <- QName -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
isGeneratedRecordConstructor QName
x
      if Bool
isR Bool -> Bool -> Bool
|| ConInfo
ci ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec
        then do
          Bool
showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
          let keep :: (Dom' Term Name, Expr) -> Bool
keep (Dom' Term Name
a, Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| Dom' Term Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term Name
a
          QName
r <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
x
          [Dom' Term Name]
xs <- [Dom' Term Name] -> Maybe [Dom' Term Name] -> [Dom' Term Name]
forall a. a -> Maybe a -> a
fromMaybe [Dom' Term Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Dom' Term Name] -> [Dom' Term Name])
-> m (Maybe [Dom' Term Name]) -> m [Dom' Term Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe [Dom' Term Name])
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
          [Expr]
vs <- (Arg Expr -> Expr) -> [Arg Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Arg Expr -> Expr
forall e. Arg e -> e
unArg ([Arg Expr] -> [Expr]) -> m [Arg Expr] -> m [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args -> m (ReifiesTo Args)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
vs)
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
noExprInfo (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ ((Dom' Term Name, Expr) -> RecordAssign)
-> [(Dom' Term Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map (Assign -> RecordAssign
forall a b. a -> Either a b
Left (Assign -> RecordAssign)
-> ((Dom' Term Name, Expr) -> Assign)
-> (Dom' Term Name, Expr)
-> RecordAssign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Expr -> Assign) -> (Name, Expr) -> Assign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Expr -> Assign
forall a. Name -> a -> FieldAssignment' a
FieldAssignment ((Name, Expr) -> Assign)
-> ((Dom' Term Name, Expr) -> (Name, Expr))
-> (Dom' Term Name, Expr)
-> Assign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term Name -> Name) -> (Dom' Term Name, Expr) -> (Name, Expr)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Dom' Term Name -> Name
forall t e. Dom' t e -> e
unDom) ([(Dom' Term Name, Expr)] -> RecordAssigns)
-> [(Dom' Term Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> a -> b
$ ((Dom' Term Name, Expr) -> Bool)
-> [(Dom' Term Name, Expr)] -> [(Dom' Term Name, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Dom' Term Name, Expr) -> Bool
keep ([(Dom' Term Name, Expr)] -> [(Dom' Term Name, Expr)])
-> [(Dom' Term Name, Expr)] -> [(Dom' Term Name, Expr)]
forall a b. (a -> b) -> a -> b
$ [Dom' Term Name] -> [Expr] -> [(Dom' Term Name, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Dom' Term Name]
xs [Expr]
vs
        else QName -> Elims -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
vs (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
          Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          let Constructor {conPars :: Defn -> Nat
conPars = Nat
np} = Definition -> Defn
theDef Definition
def
          -- if we are the the module that defines constructor x
          -- then we have to drop at least the n module parameters
          Nat
n <- QName -> m Nat
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
          -- the number of parameters is greater (if the data decl has
          -- extra parameters) or equal (if not) to n
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
np) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          let h :: Expr
h = AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
x)
          if Elims -> Bool
forall a. Null a => a -> Bool
null Elims
vs
            then Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
h
            else do
              [Arg Expr]
es <- Args -> m (ReifiesTo Args)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify ((Elim' Term -> Arg Term) -> Elims -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term)
-> (Elim' Term -> Maybe (Arg Term)) -> Elim' Term -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim) Elims
vs)
              -- 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 Nat
np Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0
                then Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
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 Telescope
tel Type
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Definition -> Type
defType Definition
def)
                  let ([Dom (String, Type)]
pars, [Dom (String, Type)]
rest) = Nat
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
np ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                  case [Dom (String, Type)]
rest of
                    -- Andreas, 2012-09-18
                    -- If the first regular constructor argument is hidden,
                    -- we keep the parameters to avoid confusion.
                    (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : [Dom (String, Type)]
_) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
                      let us :: [Arg Expr]
us = [Dom (String, Type)]
-> (Dom (String, Type) -> Arg Expr) -> [Arg Expr]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. Nat -> [a] -> [a]
drop Nat
n [Dom (String, Type)]
pars) ((Dom (String, Type) -> Arg Expr) -> [Arg Expr])
-> (Dom (String, Type) -> Arg Expr) -> [Arg Expr]
forall a b. (a -> b) -> a -> b
$ \(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}) ->
                            -- setRelevance Relevant $
                            Arg Expr -> Arg Expr
forall a. LensHiding a => a -> a
hideOrKeepInstance (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Expr
forall a. Underscore a => a
underscore
                      Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h ([Arg Expr] -> m Expr) -> [Arg Expr] -> m Expr
forall a b. (a -> b) -> a -> b
$ [Arg Expr]
us [Arg Expr] -> [Arg Expr] -> [Arg Expr]
forall a. [a] -> [a] -> [a]
++ [Arg Expr]
es -- Note: unless --show-implicit, @apps@ will drop @us@.
                    -- otherwise, we drop all parameters
                    [Dom (String, 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
      (Name
x,Expr
e) <- Abs Term -> m (ReifiesTo (Abs Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
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.
      ArgInfo
info <- m Bool -> m ArgInfo -> m ArgInfo -> m ArgInfo
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (ArgInfo -> m ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
forall a b. (a -> b) -> a -> b
$ Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten ArgInfo
info) (ArgInfo -> m ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info)
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
mkDomainFree (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding)
-> Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> Arg (Named (WithOrigin (Ranged String)) Binder))
-> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x) Expr
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)
reify Literal
l
    I.Level Level
l      -> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
l
    I.Pi Dom Type
a Abs Type
b       -> case Abs Type
b of
        NoAbs String
_ 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)
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)
reify Dom Type
a
        Abs Type
b               -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          m Bool -> m (Arg Expr) -> m (Arg Expr) -> m (Arg Expr)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Dom Type -> Type -> m Bool
forall {m :: * -> *} {a} {t}.
(MonadTCEnv m, Free a, Free t) =>
t -> a -> m Bool
domainFree Dom Type
a (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b))
            {- then -} (Arg Expr -> m (Arg Expr)
forall (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)
reify Dom Type
a)
      where
        mkPi :: Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg ArgInfo
info Expr
a') = do
          Maybe Expr
tac <- (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)
traverse Term -> m Expr
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Maybe Term -> m (Maybe Expr)) -> Maybe Term -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a
          (Name
x, Expr
b) <- Abs Type -> m (ReifiesTo (Abs Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Type
b
          let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs = Arg (Named (WithOrigin (Ranged String)) Binder)
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged String)) Binder)
 -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder)))
-> Arg (Named (WithOrigin (Ranged String)) Binder)
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Named (WithOrigin (Ranged String)) Binder
-> Arg (Named (WithOrigin (Ranged String)) Binder)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named (WithOrigin (Ranged String)) Binder
 -> Arg (Named (WithOrigin (Ranged String)) Binder))
-> Named (WithOrigin (Ranged String)) Binder
-> Arg (Named (WithOrigin (Ranged String)) Binder)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged String))
-> Binder -> Named (WithOrigin (Ranged String)) Binder
forall name a. Maybe name -> a -> Named name a
Named (Dom Type -> Maybe (WithOrigin (Ranged String))
forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
domName Dom Type
a) (Binder -> Named (WithOrigin (Ranged String)) Binder)
-> Binder -> Named (WithOrigin (Ranged String)) Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
noExprInfo (TypedBinding -> Telescope1
forall el coll. Singleton el coll => el -> coll
singleton (TypedBinding -> Telescope1) -> TypedBinding -> Telescope1
forall a b. (a -> b) -> a -> b
$ Range
-> Maybe Expr
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind Range
forall a. Range' a
noRange Maybe Expr
tac List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
a') Expr
b
        -- We can omit the domain type if it doesn't have any free variables
        -- and it's mentioned in the target type.
        domainFree :: t -> a -> m Bool
domainFree t
a a
b = do
          Bool
df <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintDomainFreePi
          Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool
df Bool -> Bool -> Bool
&& Nat -> a -> Bool
forall a. Free a => Nat -> a -> Bool
freeIn Nat
0 a
b Bool -> Bool -> Bool
&& t -> Bool
forall t. Free t => t -> Bool
closed t
a

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

          [Elim' Expr]
es' <- Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es

          MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
          (Maybe (Substitution' Term)
msub1,Telescope
meta_tel,Maybe (Substitution' Term)
msub2) <- do
            CheckpointId
local_chkpt <- Lens' CheckpointId TCEnv -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
            (CheckpointId
chkpt, Telescope
tel, Maybe (Substitution' Term)
msub2) <- MetaVariable
-> (Range
    -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m (CheckpointId, Telescope, Maybe (Substitution' Term))
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
 -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> (Range
    -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m (CheckpointId, Telescope, Maybe (Substitution' Term))
forall a b. (a -> b) -> a -> b
$ \ 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' CheckpointId TCEnv -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
                                    m (Telescope
   -> Maybe (Substitution' Term)
   -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
-> m Telescope
-> m (Maybe (Substitution' Term)
      -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Telescope
forall (m :: * -> *). (Applicative 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Lens' (Maybe (Substitution' Term)) TCEnv
-> m (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId (Substitution' Term)) TCEnv
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'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
local_chkpt)
            (,,) (Maybe (Substitution' Term)
 -> Telescope
 -> Maybe (Substitution' Term)
 -> (Maybe (Substitution' Term), Telescope,
     Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Telescope
      -> Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Telescope,
          Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Maybe (Substitution' Term)) TCEnv
-> m (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId (Substitution' Term)) TCEnv
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'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
chkpt) m (Telescope
   -> Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Telescope,
       Maybe (Substitution' Term)))
-> m Telescope
-> m (Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Telescope,
          Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Telescope -> m Telescope
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
tel m (Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Telescope,
       Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Maybe (Substitution' Term), Telescope,
      Maybe (Substitution' Term))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Substitution' Term) -> m (Maybe (Substitution' Term))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Substitution' Term)
msub2

          Bool
opt_show_ids <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showIdentitySubstitutions
          let
              addNames :: [name] -> [Elim' a] -> [Elim' (Named name a)]
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 (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 :: Permutation
p = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
              applyPerm :: Permutation -> [a] -> [a]
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 :: [WithOrigin (Ranged String)]
names = (String -> WithOrigin (Ranged String))
-> [String] -> [WithOrigin (Ranged String)]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> Ranged String -> WithOrigin (Ranged String)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> WithOrigin (Ranged String))
-> (String -> Ranged String)
-> String
-> WithOrigin (Ranged String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Ranged String
forall a. a -> Ranged a
unranged) ([String] -> [WithOrigin (Ranged String)])
-> [String] -> [WithOrigin (Ranged String)]
forall a b. (a -> b) -> a -> b
$ Permutation
p Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
`applyPerm` Telescope -> [String]
teleNames Telescope
meta_tel
              named_es' :: [Elim' (Named_ Expr)]
named_es' = [WithOrigin (Ranged String)]
-> [Elim' Expr] -> [Elim' (Named_ Expr)]
forall {name} {a}. [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [WithOrigin (Ranged String)]
names [Elim' Expr]
es'

              dropIdentitySubs :: Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
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 :: Elims
es_G = Substitution' Term
Substitution' (SubstArg Elims)
sub_local2G Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Elims
es
                     sameVar :: Arg a -> Elim' a -> Bool
sameVar Arg a
x (I.Apply Arg a
y) = Maybe Nat -> Bool
forall a. Maybe a -> Bool
isJust Maybe Nat
xv Bool -> Bool -> Bool
&& Maybe Nat
xv Maybe Nat -> Maybe Nat -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (Arg a -> a
forall e. Arg e -> e
unArg Arg a
y)
                      where
                       xv :: Maybe Nat
xv = a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (a -> Maybe Nat) -> a -> Maybe Nat
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
x
                     sameVar Arg a
_ Elim' a
_ = Bool
False
                     dropArg :: [Bool]
dropArg = Nat -> [Bool] -> [Bool]
forall a. Nat -> [a] -> [a]
take ([WithOrigin (Ranged String)] -> Nat
forall a. Sized a => a -> Nat
size [WithOrigin (Ranged String)]
names) ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term -> Bool) -> Args -> Elims -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Elim' Term -> Bool
forall {a} {a}.
(DeBruijn a, DeBruijn a) =>
Arg a -> Elim' a -> Bool
sameVar Args
args_G Elims
es_G
                     doDrop :: [Bool] -> [a] -> [a]
doDrop (Bool
b : [Bool]
xs)  (a
e : [a]
es) = (if Bool
b then [a] -> [a]
forall a. a -> a
id else (a
e a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [a] -> [a]
doDrop [Bool]
xs [a]
es
                     doDrop []        [a]
es = [a]
es
                     doDrop [Bool]
_         [] = []
                 in [Bool] -> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
forall {a}. [Bool] -> [a] -> [a]
doDrop [Bool]
dropArg ([Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)])
-> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
forall a b. (a -> b) -> a -> b
$ [Elim' (Named_ Expr)]
named_es'

              simpl_named_es' :: [Elim' (Named_ Expr)]
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'

          Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
x' [Elim' (Named_ Expr)]
simpl_named_es'

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

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

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

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

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

        -- Check whether we have an extended lambda and display forms are on.
        Bool
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!
        [QName]
alreadyPrinting <- Lens' [QName] TCEnv -> m [QName]
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' [QName] TCEnv
ePrintingPatternLambdas

        Maybe (Nat, Maybe System)
extLam <- case Defn
def of
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just{}, funProjection :: Defn -> Maybe Projection
funProjection = Just{} } -> 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 a. Maybe a -> Maybe a
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 :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
          Defn
_ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Nat, Maybe System)
forall a. Maybe a
Nothing
        case Maybe (Nat, Maybe System)
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' [QName] TCEnv -> ([QName] -> [QName]) -> m Expr -> m Expr
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' [QName] TCEnv
ePrintingPatternLambdas (QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$
            QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x (Definition -> ArgInfo
defArgInfo Definition
defn) Nat
pars Maybe System
sys
              (Definition -> [Clause]
defClauses Definition
defn) Elims
es

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

            Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just Projection{ projIndex :: Projection -> Nat
projIndex = Nat
np } } | Nat
np Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 -> do
              String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
70 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"  def. is a projection with projIndex = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
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 Telescope
tel Type
_ <- 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 ([Dom (String, Type)]
as, [Dom (String, Type)]
rest) = Nat
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt (Nat
np Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                  dom :: Dom (String, Type)
dom = Dom (String, Type) -> [Dom (String, Type)] -> Dom (String, Type)
forall a. a -> [a] -> a
headWithDefault Dom (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom (String, Type)]
rest

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

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

              -- Get the visible arguments of the padding and the rest
              -- after the last visible argument.
              let ([Arg (Named_ Expr)]
padVisNamed, [Arg (Named_ Expr)]
padRest) = (Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)]
-> ([Arg (Named_ Expr)], [Arg (Named_ Expr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
filterAndRest Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible [Arg (Named_ Expr)]
pad'

              -- Remove the names from the visible arguments.
              let padVis :: [Arg (Named_ Expr)]
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 (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)]
padTail = (Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Dom (String, Type) -> Arg (Named_ Expr) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom (String, Type)
dom) [Arg (Named_ Expr)]
padRest

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

              ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall (m :: * -> *) a. Monad m => a -> m a
return (([Arg (Named_ Expr)], [Elim' (Named_ Term)])
 -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)]))
-> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
-> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
forall a b. (a -> b) -> a -> b
$ if [Arg (Named_ Expr)] -> Bool
forall a. Null a => a -> Bool
null [Arg (Named_ Expr)]
padTail Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
showImp
                then ([Arg (Named_ Expr)]
padVis           , (Elim' Term -> Elim' (Named_ Term))
-> Elims -> [Elim' (Named_ Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Named_ Term) -> Elim' Term -> Elim' (Named_ Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Named_ Term
forall a name. a -> Named name a
unnamed) Elims
es')
                else ([Arg (Named_ Expr)]
padVis [Arg (Named_ Expr)] -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Expr)]
padSame, Dom (String, Type) -> Elims -> [Elim' (Named_ Term)]
forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden Dom (String, Type)
dom Elims
es')

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

           String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.def" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
             [ Doc
"  pad =" Doc -> Doc -> Doc
<+> [Arg (Named_ Expr)] -> Doc
forall a. Show a => a -> Doc
pshow [Arg (Named_ Expr)]
pad
             , Doc
"  nes =" Doc -> Doc -> Doc
<+> [Elim' (Named_ Term)] -> Doc
forall a. Show a => a -> Doc
pshow [Elim' (Named_ Term)]
nes
             ]
           let hd0 :: Expr
hd0 | Defn -> Bool
isProperProjection Defn
def = ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
AmbQ (List1 QName -> AmbiguousQName) -> List1 QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ QName -> List1 QName
forall el coll. Singleton el coll => el -> coll
singleton QName
x
                   | Bool
otherwise = QName -> Expr
A.Def QName
x
           let hd :: Expr
hd = (Expr -> Arg (Named_ Expr) -> Expr)
-> Expr -> [Arg (Named_ Expr)] -> Expr
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
           Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
hd ([Elim' (Named_ Expr)] -> m Expr)
-> m [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Elim' (Named_ Term)] -> m (ReifiesTo [Elim' (Named_ Term)])
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify [Elim' (Named_ Term)]
nes

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

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

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

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

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

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

      -- Since we applying the clauses to the parameters,
      -- we do not need to drop their initial "parameter" patterns
      -- (this is taken care of by @apply@).
      [Clause]
cls <- Maybe System -> m [Clause] -> (System -> m [Clause]) -> m [Clause]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
               ((Clause -> m Clause) -> [Clause] -> m [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (NamedClause -> m Clause
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (NamedClause -> m Clause)
-> (Clause -> NamedClause) -> Clause -> m Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
x Bool
False (Clause -> NamedClause)
-> (Clause -> Clause) -> Clause -> NamedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cls)
               (QNamed System -> m [Clause]
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (QNamed System -> m [Clause])
-> (System -> QNamed System) -> System -> m [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> System -> QNamed System
forall a. QName -> a -> QNamed a
QNamed QName
x (System -> QNamed System)
-> (System -> System) -> System -> QNamed System
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (System -> Args -> System
forall t. Apply t => t -> Args -> t
`apply` Args
pars))
      let cx :: Name
cx     = Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          dInfo :: DefInfo' Expr
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 :: Erased
erased = case ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
i 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__
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo Erased
erased QName
x (List1 Clause -> Expr) -> List1 Clause -> Expr
forall a b. (a -> b) -> a -> b
$
             [Clause] -> List1 Clause
forall a. [a] -> NonEmpty a
List1.fromList [Clause]
cls)
        ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m (ReifiesTo Elims)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
rest

-- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden :: forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden Dom (String, 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 String)) -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
forall a. a -> Maybe a
Just (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String)))
-> WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged String -> WithOrigin (Ranged String)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> WithOrigin (Ranged String))
-> Ranged String -> WithOrigin (Ranged String)
forall a b. (a -> b) -> a -> b
$ String -> Ranged String
forall a. a -> Ranged a
unranged (String -> Ranged String) -> String -> Ranged String
forall a b. (a -> b) -> a -> b
$ (String, t) -> String
forall a b. (a, b) -> a
fst ((String, t) -> String) -> (String, t) -> String
forall a b. (a -> b) -> a -> b
$ Dom (String, t) -> (String, t)
forall t e. Dom' t e -> e
unDom Dom (String, 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 (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 (String, 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 (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)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
reifyWhen i
i (Bool -> m (ReifiesTo i)) -> m Bool -> m (ReifiesTo i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Bool
condition)
    where condition :: m Bool
condition = (Bool -> m Bool
forall (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 (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant) 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)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b) Arg i
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


-- | 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 => A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits :: forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits 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 (m :: * -> *) a. Monad m => a -> m a
return (Patterns -> m Patterns) -> Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> Patterns -> Patterns
forall a b. (a -> b) -> [a] -> [b]
map ((Named_ Pattern -> Named_ Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ Pattern -> Named_ Pattern
forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten) Patterns
ps) (m Patterns -> m Patterns) -> m Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ do
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"stripping implicits"
      , Nat -> Doc -> Doc
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"ps   =" Doc -> Doc -> Doc
<+> Patterns -> Doc
forall a. Show a => a -> Doc
pshow Patterns
ps
      ]
    let ps' :: Patterns
ps' = Patterns -> Patterns
blankDots (Patterns -> Patterns) -> Patterns -> Patterns
forall a b. (a -> b) -> a -> b
$ Patterns -> Patterns
forall {e}. [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip Patterns
ps
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Nat -> Doc -> Doc
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"ps'  =" Doc -> Doc -> Doc
<+> Patterns -> Doc
forall a. Show a => a -> Doc
pshow Patterns
ps'
      ]
    Patterns -> m Patterns
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 :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip [NamedArg (Pattern' e)]
ps = Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall {e}.
Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
ps
        where
          stripArgs :: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
_ [] = []
          stripArgs Bool
fixedPos (NamedArg (Pattern' e)
a : [NamedArg (Pattern' e)]
as)
            -- A hidden non-UserWritten variable is removed if not needed for
            -- correct position of the following hidden arguments.
            | NamedArg (Pattern' e) -> Bool
forall {e}. NamedArg (Pattern' e) -> Bool
canStrip NamedArg (Pattern' e)
a =
                 if   (NamedArg (Pattern' e) -> Bool) -> [NamedArg (Pattern' e)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all NamedArg (Pattern' e) -> Bool
forall {e}. NamedArg (Pattern' e) -> Bool
canStrip ([NamedArg (Pattern' e)] -> Bool)
-> [NamedArg (Pattern' e)] -> Bool
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' e) -> Bool)
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile NamedArg (Pattern' e) -> Bool
forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
isUnnamedHidden [NamedArg (Pattern' e)]
as
                 then Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
False [NamedArg (Pattern' e)]
as
                 else [NamedArg (Pattern' e)]
goWild
            -- Other arguments are kept.
            | Bool
otherwise = Bool -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos (NamedArg (Pattern' e) -> NamedArg (Pattern' e)
stripArg NamedArg (Pattern' e)
a) NamedArg (Pattern' e)
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. a -> [a] -> [a]
: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
as
            where
              a' :: NamedArg (Pattern' e)
a'     = NamedArg (Pattern' e) -> Pattern' e -> NamedArg (Pattern' e)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' e)
a (Pattern' e -> NamedArg (Pattern' e))
-> Pattern' e -> NamedArg (Pattern' e)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
A.WildP (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
Info.PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' e) -> Range
forall a. HasRange a => a -> Range
getRange NamedArg (Pattern' e)
a
              goWild :: [NamedArg (Pattern' e)]
goWild = Bool -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos NamedArg (Pattern' e)
a' NamedArg (Pattern' e)
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. a -> [a] -> [a]
: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
as

          stripName :: Bool -> f b -> f b
stripName Bool
True  = (b -> b) -> f b -> 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 :: NamedArg (Pattern' e) -> Bool
canStrip NamedArg (Pattern' e)
a = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ NamedArg (Pattern' e) -> Bool
forall a. LensHiding a => a -> Bool
notVisible NamedArg (Pattern' e)
a
            , NamedArg (Pattern' e) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin NamedArg (Pattern' e)
a Origin -> [Origin] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ Origin
UserWritten , Origin
CaseSplit ]
            , (WithOrigin (Ranged String) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin (WithOrigin (Ranged String) -> Origin)
-> Maybe (WithOrigin (Ranged String)) -> Maybe Origin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg (Pattern' e) -> Maybe (NameOf (NamedArg (Pattern' e)))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg (Pattern' e)
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' e -> Bool
forall {e}. Pattern' e -> Bool
varOrDot (NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' e)
a)
            ]

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

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

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

-- | @blankNotInScope e@ replaces variables in expression @e@ with @_@
-- if they are currently not in scope.
blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope :: forall (m :: * -> *) a. (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope a
e = do
  Set Name
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) -> m [Name] -> m (Set Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Set Name -> a -> a
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
names a
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
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> a -> a) -> (Set Name -> b -> b) -> Set Name -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Name -> b -> b
forall a. BlankVars a => Set Name -> a -> a
blank

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

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

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

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

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

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

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

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

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

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

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

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

instance BlankVars TypedBinding where
  blank :: Set Name -> TypedBinding -> TypedBinding
blank Set Name
bound (TBind Range
r Maybe Expr
t List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
n Expr
e) = Range
-> Maybe Expr
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind Range
r Maybe Expr
t List1 (Arg (Named (WithOrigin (Ranged String)) 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 (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn

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

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

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

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

instance Binder A.LamBinding where
  varsBoundIn :: LamBinding -> Set Name
varsBoundIn (A.DomainFree Maybe Expr
_ Arg (Named (WithOrigin (Ranged String)) Binder)
x) = Arg (Named (WithOrigin (Ranged String)) Binder) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Arg (Named (WithOrigin (Ranged String)) 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
_ Maybe Expr
_ List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
_) = List1 (Arg (Named (WithOrigin (Ranged String)) Binder)) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn List1 (Arg (Named (WithOrigin (Ranged String)) 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 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 (LetPatBind LetInfo
_ Pattern
p Expr
_)  = Pattern -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Pattern
p
  varsBoundIn LetApply{}          = Set Name
forall a. Null a => a
empty
  varsBoundIn LetOpen{}           = Set Name
forall a. Null a => a
empty
  varsBoundIn LetDeclaredVariable{} = Set Name
forall a. Null a => a
empty

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

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


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

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

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

    reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
    reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x = do
      Name
n <- Nat -> m Name
forall (m :: * -> *).
(Applicative m, MonadFail 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 :: String
y = DBPatVar -> String
dbPatVarName DBPatVar
x
      if | String
y String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"_" -> Pattern -> m Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
n
           -- Andreas, 2017-09-03: TODO for #2580
           -- Patterns @VarP "()"@ should have been replaced by @AbsurdP@, but the
           -- case splitter still produces them.
         | Name -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
n) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"()" -> Pattern -> m Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (Name -> BindName
mkBindName Name
n)
           -- Andreas, 2017-09-03, issue #2729
           -- Restore original pattern name.  AbstractToConcrete picks unique names.
         | Bool
otherwise -> Pattern -> m Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$
             Name -> BindName
mkBindName Name
n { nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
y }

    reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
    reifyDotP :: forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v = do
      Bool
keepVars <- PragmaOptions -> Bool
optKeepPatternVariables (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      if | PatOVar Name
x <- PatOrigin
o , Bool
keepVars       -> Pattern -> m Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
         | Bool
otherwise                       -> PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange (Expr -> Pattern) -> m Expr -> m Pattern
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)
reify Term
v

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

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


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

-- | 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
  String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.expr" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"recOrCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
c
  m (Maybe (QName, Defn))
-> m Expr -> ((QName, Defn) -> 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, Defn))
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) m Expr
fallback (((QName, Defn) -> m Expr) -> m Expr)
-> ((QName, Defn) -> m Expr) -> m Expr
forall a b. (a -> b) -> a -> b
$ \ (QName
r, Defn
def) -> do
    -- If the record constructor is generated or the user wrote a record expression,
    -- print record expression.
    -- Otherwise, print constructor expression.
    if Defn -> Bool
recNamedCon Defn
def Bool -> Bool -> Bool
&& ConInfo
co ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= ConInfo
ConORec then m Expr
fallback else do
      [Dom' Term Name]
fs <- [Dom' Term Name] -> Maybe [Dom' Term Name] -> [Dom' Term Name]
forall a. a -> Maybe a -> a
fromMaybe [Dom' Term Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Dom' Term Name] -> [Dom' Term Name])
-> m (Maybe [Dom' Term Name]) -> m [Dom' Term Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe [Dom' Term Name])
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Dom' Term Name] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom' Term Name]
fs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Expr] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Expr]
es) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
forall a. Null a => a
empty (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ (Dom' Term Name -> Arg Expr -> RecordAssign)
-> [Dom' Term Name] -> [Arg Expr] -> RecordAssigns
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Dom' Term Name -> Arg Expr -> RecordAssign
forall {t} {b} {b}.
Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA [Dom' Term Name]
fs [Arg Expr]
es
  where
  fallback :: m Expr
fallback = Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
c)) [Arg Expr]
es
  mkFA :: Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA Dom' t Name
ax  = FieldAssignment' b -> Either (FieldAssignment' b) b
forall a b. a -> Either a b
Left (FieldAssignment' b -> Either (FieldAssignment' b) b)
-> (Arg b -> FieldAssignment' b)
-> Arg b
-> Either (FieldAssignment' b) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> b -> FieldAssignment' b
forall a. Name -> a -> FieldAssignment' a
FieldAssignment (Dom' t Name -> Name
forall t e. Dom' t e -> e
unDom Dom' t Name
ax) (b -> FieldAssignment' b)
-> (Arg b -> b) -> Arg b -> FieldAssignment' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg b -> b
forall e. Arg e -> e
unArg

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

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

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
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
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.clause" Nat
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"reifying NamedClause"
      , Doc
"  f      =" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
      , Doc
"  toDrop =" Doc -> Doc -> Doc
<+> Bool -> Doc
forall a. Show a => a -> Doc
pshow Bool
toDrop
      , Doc
"  cl     =" Doc -> Doc -> Doc
<+> Clause -> Doc
forall a. Pretty a => a -> Doc
pretty Clause
cl
      ]
    let ell :: ExpandedEllipsis
ell = Clause -> ExpandedEllipsis
clauseEllipsis Clause
cl
    Patterns
ps  <- [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns ([NamedArg DeBruijnPattern] -> m Patterns)
-> [NamedArg DeBruijnPattern] -> m Patterns
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
    SpineLHS
lhs <- (QName -> Patterns -> SpineLHS) -> (QName, Patterns) -> SpineLHS
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS (LHSInfo -> QName -> Patterns -> SpineLHS)
-> LHSInfo -> QName -> Patterns -> SpineLHS
forall a b. (a -> b) -> a -> b
$ LHSInfo
forall a. Null a => a
empty { lhsEllipsis :: ExpandedEllipsis
lhsEllipsis = ExpandedEllipsis
ell }) ((QName, Patterns) -> SpineLHS)
-> m (QName, Patterns) -> m SpineLHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Patterns -> Patterns -> m (QName, Patterns)
forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
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.
    (Patterns
params , SpineLHS
lhs) <- if Bool -> Bool
not Bool
toDrop then (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ([] , SpineLHS
lhs) else do
      Nat
nfv <- QName -> m (Either SigError ModuleName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ModuleName)
getDefModule QName
f m (Either SigError ModuleName)
-> (Either SigError ModuleName -> m Nat) -> m Nat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left SigError
_  -> Nat -> m Nat
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 :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
      (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Patterns, SpineLHS) -> m (Patterns, SpineLHS))
-> (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall a b. (a -> b) -> a -> b
$ Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams Nat
nfv SpineLHS
lhs
    SpineLHS
lhs <- Patterns -> SpineLHS -> m SpineLHS
forall (m :: * -> *).
MonadReify m =>
Patterns -> SpineLHS -> m SpineLHS
stripImps Patterns
params SpineLHS
lhs
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reifying NamedClause, lhs =" Doc -> Doc -> Doc
<?> SpineLHS -> Doc
forall a. Show a => a -> Doc
pshow SpineLHS
lhs
    RHS
rhs <- Maybe Term -> m RHS -> (Term -> m RHS) -> m RHS
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Clause -> Maybe Term
clauseBody Clause
cl) (RHS -> m RHS
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
AbsurdRHS) ((Term -> m RHS) -> m RHS) -> (Term -> m RHS) -> m RHS
forall a b. (a -> b) -> a -> b
$ \ Term
e ->
      Expr -> Maybe Expr -> RHS
RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
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)
reify Term
e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Expr -> m (Maybe Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
forall a. Maybe a
Nothing
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reifying NamedClause, rhs =" Doc -> Doc -> Doc
<?> RHS -> Doc
forall a. Show a => a -> Doc
pshow RHS
rhs
    let result :: Clause
result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls (Clause -> Bool
I.clauseCatchall Clause
cl)
    String -> Nat -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCM Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"reified NamedClause, result =" Doc -> Doc -> Doc
<?> Clause -> Doc
forall a. Show a => a -> Doc
pshow Clause
result
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
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 => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
      stripImps :: forall (m :: * -> *).
MonadReify m =>
Patterns -> SpineLHS -> m SpineLHS
stripImps 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
<$> Patterns -> Patterns -> m Patterns
forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits Patterns
params Patterns
ps

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
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
    String -> Nat -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.system" Nat
40 ([String] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ Telescope -> String
forall a. Show a => a -> String
show Telescope
tel String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((Face, Term) -> String) -> [(Face, Term)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Face, Term) -> String
forall a. Show a => a -> String
show [(Face, Term)]
sys
    Term -> IntervalView
view <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
    IntervalView -> Term
unview <- m (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
    [(Face, Term)]
sys <- (((Face, Term) -> m Bool) -> [(Face, Term)] -> m [(Face, Term)])
-> [(Face, Term)] -> ((Face, Term) -> m Bool) -> m [(Face, Term)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Face, Term) -> m Bool) -> [(Face, Term)] -> m [(Face, Term)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [(Face, Term)]
sys (((Face, Term) -> m Bool) -> m [(Face, Term)])
-> ((Face, Term) -> m Bool) -> m [(Face, Term)]
forall a b. (a -> b) -> a -> b
$ \ (Face
phi,Term
t) -> do
      Face -> ((Term, Bool) -> m Bool) -> m Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM Face
phi (((Term, Bool) -> m Bool) -> m Bool)
-> ((Term, Bool) -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ (Term
u,Bool
b) -> do
        Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
        Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case (Term -> IntervalView
view Term
u, Bool
b) of
          (IntervalView
IZero, Bool
True) -> Bool
False
          (IntervalView
IOne, Bool
False) -> Bool
False
          (IntervalView, Bool)
_ -> Bool
True
    [(Face, Term)] -> ((Face, Term) -> m Clause) -> m [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Face, Term)]
sys (((Face, Term) -> m Clause) -> m [Clause])
-> ((Face, Term) -> m Clause) -> m [Clause]
forall a b. (a -> b) -> a -> b
$ \ (Face
alpha,Term
u) -> do
      RHS
rhs <- Expr -> Maybe Expr -> RHS
RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
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)
reify Term
u m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Expr -> m (Maybe Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
forall a. Maybe a
Nothing
      Pattern
ep <- ([(Expr, Expr)] -> Pattern) -> m [(Expr, Expr)] -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PatInfo -> [(Expr, Expr)] -> Pattern
forall e. PatInfo -> [(e, e)] -> Pattern' e
A.EqualP PatInfo
patNoRange) (m [(Expr, Expr)] -> m Pattern)
-> (((Term, Bool) -> m (Expr, Expr)) -> m [(Expr, Expr)])
-> ((Term, Bool) -> m (Expr, Expr))
-> m Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Face -> ((Term, Bool) -> m (Expr, Expr)) -> m [(Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Face
alpha (((Term, Bool) -> m (Expr, Expr)) -> m Pattern)
-> ((Term, Bool) -> m (Expr, Expr)) -> m Pattern
forall a b. (a -> b) -> a -> b
$ \ (Term
phi,Bool
b) -> do
        let
            d :: Bool -> Term
d Bool
True = IntervalView -> Term
unview IntervalView
IOne
            d Bool
False = IntervalView -> Term
unview IntervalView
IZero
        (Term, Term) -> m (ReifiesTo (Term, Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term
phi, Bool -> Term
d Bool
b)

      Patterns
ps <- [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns ([NamedArg DeBruijnPattern] -> m Patterns)
-> [NamedArg DeBruijnPattern] -> m Patterns
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
tel
      Patterns
ps <- Patterns -> Patterns -> m Patterns
forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits [] (Patterns -> m Patterns) -> Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ Patterns
ps Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ [Pattern -> Arg (Named_ Pattern)
forall a. a -> NamedArg a
defaultNamedArg Pattern
ep]
      let
        lhs :: SpineLHS
lhs = LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
forall a. Null a => a
empty QName
f Patterns
ps
        result :: Clause
result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls Bool
False
      Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
result

instance Reify Type where
    type ReifiesTo Type = Expr

    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
    reify :: forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (I.El Sort
_ Term
t) = Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
t

instance Reify Sort where
    type ReifiesTo Sort = Expr

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Sort -> m (ReifiesTo Sort)
reifyWhen = Bool -> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
    reify :: forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s = do
      Sort
s <- Sort -> m Sort
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort
s
      SortKit{QName
IsFibrant -> QName
nameOfSetOmega :: SortKit -> IsFibrant -> QName
nameOfSSet :: SortKit -> QName
nameOfProp :: SortKit -> QName
nameOfSet :: SortKit -> QName
nameOfSetOmega :: IsFibrant -> QName
nameOfSSet :: QName
nameOfProp :: QName
nameOfSet :: QName
..} <- m SortKit
forall (m :: * -> *). HasBuiltins m => m SortKit
sortKit
      case Sort
s of
        I.Type (I.ClosedLevel Integer
0) -> Expr -> m Expr
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' QName
nameOfSet Suffix
A.NoSuffix
        I.Type (I.ClosedLevel Integer
n) -> Expr -> m Expr
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' QName
nameOfSet (Integer -> Suffix
A.Suffix Integer
n)
        I.Type Level
a -> do
          Expr
a <- Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
nameOfSet) (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        I.Prop (I.ClosedLevel Integer
0) -> Expr -> m Expr
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' QName
nameOfProp Suffix
A.NoSuffix
        I.Prop (I.ClosedLevel Integer
n) -> Expr -> m Expr
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' QName
nameOfProp (Integer -> Suffix
A.Suffix Integer
n)
        I.Prop Level
a -> do
          Expr
a <- Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
nameOfProp) (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        I.Inf IsFibrant
f Integer
0 -> Expr -> m Expr
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' (IsFibrant -> QName
nameOfSetOmega IsFibrant
f) Suffix
A.NoSuffix
        I.Inf IsFibrant
f Integer
n -> Expr -> m Expr
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' (IsFibrant -> QName
nameOfSetOmega IsFibrant
f) (Integer -> Suffix
A.Suffix Integer
n)
        I.SSet Level
a  -> do
          I.Def QName
sset [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinStrictSet
          Expr
a <- Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
sset) (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        Sort
I.SizeUniv  -> do
          I.Def QName
sizeU [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSizeUniv
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
sizeU
        Sort
I.LockUniv  -> do
          QName
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
<$> String -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
builtinLockUniv
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
lockU
        I.PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
          Name
pis <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"piSort" :: String) -- TODO: hack
          (Expr
e1,Expr
e2) <- (Sort, Term) -> m (ReifiesTo (Sort, Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Sort
s1, ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ (Sort -> Term) -> Abs Sort -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort Abs Sort
s2)
          let app :: Expr -> Expr -> Expr
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)
          Expr -> m Expr
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
pis Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
        I.FunSort Sort
s1 Sort
s2 -> do
          Name
funs <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"funSort" :: String) -- TODO: hack
          (Expr
e1,Expr
e2) <- (Sort, Sort) -> m (ReifiesTo (Sort, Sort))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Sort
s1 , Sort
s2)
          let app :: Expr -> Expr -> Expr
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)
          Expr -> m Expr
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
funs Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
        I.UnivSort Sort
s -> do
          Name
univs <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"univSort" :: String) -- TODO: hack
          Expr
e <- Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (Name -> Expr
A.Var Name
univs) (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
        I.MetaS MetaId
x Elims
es -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x Elims
es
        I.DefS QName
d Elims
es -> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
d Elims
es
        I.DummyS String
s -> Expr -> m Expr
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
$ String -> Text
T.pack String
s

instance Reify Level where
  type ReifiesTo Level = Expr

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

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 String
x i
v) = String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
x m Name -> (Name -> m (Name, ReifiesTo i)) -> m (Name, ReifiesTo i)
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)
reify i
v
  reify (Abs String
s i
v) = do

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

    Name
x <- Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> m Name -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
    ReifiesTo i
e <- Name -> m (ReifiesTo i) -> m (ReifiesTo i)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Name
x -- type doesn't matter
         (m (ReifiesTo i) -> m (ReifiesTo i))
-> m (ReifiesTo i) -> m (ReifiesTo i)
forall a b. (a -> b) -> a -> b
$ i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
v
    (Name, ReifiesTo i) -> m (Name, ReifiesTo i)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x,ReifiesTo i
e)

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

  reify :: forall (m :: * -> *).
MonadReify m =>
Telescope -> m (ReifiesTo Telescope)
reify Telescope
EmptyTel = Telescope -> m Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return []
  reify (ExtendTel Dom Type
arg Abs Telescope
tel) = do
    Arg ArgInfo
info Expr
e <- Dom Type -> m (ReifiesTo (Dom Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
arg
    (Name
x, Telescope
bs)  <- Abs Telescope -> m (ReifiesTo (Abs Telescope))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Telescope
tel
    let r :: Range
r    = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
        name :: Maybe (WithOrigin (Ranged String))
name = Dom Type -> Maybe (WithOrigin (Ranged String))
forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
domName Dom Type
arg
    Maybe Expr
tac <- (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)
traverse Term -> m Expr
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Maybe Term -> m (Maybe Expr)) -> Maybe Term -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
arg
    let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs = Arg (Named (WithOrigin (Ranged String)) Binder)
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named (WithOrigin (Ranged String)) Binder)
 -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder)))
-> Arg (Named (WithOrigin (Ranged String)) Binder)
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Named (WithOrigin (Ranged String)) Binder
-> Arg (Named (WithOrigin (Ranged String)) Binder)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named (WithOrigin (Ranged String)) Binder
 -> Arg (Named (WithOrigin (Ranged String)) Binder))
-> Named (WithOrigin (Ranged String)) Binder
-> Arg (Named (WithOrigin (Ranged String)) Binder)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged String))
-> Binder -> Named (WithOrigin (Ranged String)) Binder
forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged String))
name (Binder -> Named (WithOrigin (Ranged String)) Binder)
-> Binder -> Named (WithOrigin (Ranged String)) Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
    Telescope -> m Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> m Telescope) -> Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ Range
-> Maybe Expr
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind Range
r Maybe Expr
tac List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
e TypedBinding -> Telescope -> Telescope
forall a. a -> [a] -> [a]
: Telescope
bs

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

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

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)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
traverse i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
traverse (Bool -> i -> m (ReifiesTo i)
forall i (m :: * -> *).
(Reify i, 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)
reify i1
x m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
-> m (ReifiesTo i2) -> m (ReifiesTo i1, ReifiesTo i2)
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)
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)
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 (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)
reify i2
y m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
-> m (ReifiesTo i3) -> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
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)
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)
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 (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)
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 (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)
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 (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)
reify i4
w