{-# LANGUAGE NondecreasingIndentation   #-}
{-# LANGUAGE TypeFamilies               #-}  -- for type equality ~
{-# LANGUAGE UndecidableInstances       #-}

{-|
    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 (mapM_, mapM, null)

import Control.Applicative (liftA2)
import Control.Arrow ((&&&))
import Control.Monad.State hiding (mapM_, mapM)

import Data.Foldable (Foldable, foldMap)
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup, (<>) )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse, mapM)

import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
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.Monad.Builtin
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 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 a => i -> TCM a
reifyUnblocked :: i -> TCM a
reifyUnblocked i
t = Lens' Bool TCState -> (Bool -> Bool) -> TCM a -> TCM a
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) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ i -> TCM a
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 :: 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 :: 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 -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> NamedArg Expr
forall a. a -> Arg a
defaultArg Named_ Expr
r) [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Apply NamedArg Expr
arg : [Elim' (Named_ Expr)]
es) = do
  NamedArg Expr
arg <- NamedArg Expr -> m (NamedArg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify NamedArg 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 | NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
notVisible NamedArg Expr
arg Bool -> Bool -> Bool
&& Bool
dontShowImp = Expr
e
         | Bool
otherwise                     = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e NamedArg 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 -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> NamedArg Expr) -> Expr -> NamedArg 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 :: 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 -> NamedArg 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) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg 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 :: 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 Expr, MonadReify m) => Bool -> i -> m Expr
reifyWhenE :: Bool -> i -> m Expr
reifyWhenE Bool
True  i
i = i -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify i
i
reifyWhenE Bool
False i
t = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall a. Underscore a => a
underscore

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

type MonadReify m =
  ( MonadReduce m
  , MonadAddContext m
  , MonadInteractionPoints m
  , MonadFresh NameId m
  , HasConstInfo m
  , HasOptions m
  , HasBuiltins m
  , MonadDebug m
  )

class Reify i a | i -> a where
    reify     :: MonadReify m => i -> m a

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

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

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

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

instance Reify MetaId Expr where
    reifyWhen :: Bool -> MetaId -> m Expr
reifyWhen = Bool -> MetaId -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
    reify :: MetaId -> m Expr
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' = MetaInfo :: Range -> ScopeInfo -> Maybe MetaId -> String -> MetaInfo
Info.MetaInfo
                 { metaRange :: Range
metaRange          = Closure Range -> Range
forall t. HasRange t => t -> 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 Expr where
  reifyWhen :: Bool -> DisplayTerm -> m Expr
reifyWhen = Bool -> DisplayTerm -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
  reify :: DisplayTerm -> m Expr
reify DisplayTerm
d = case DisplayTerm
d of
    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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
    DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs -> 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
=<< [Arg DisplayTerm] -> m [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify [Elim' DisplayTerm]
es
    DWithApp DisplayTerm
u [DisplayTerm]
us Elims
es0 -> do
      (Expr
e, [Expr]
es) <- (DisplayTerm, [DisplayTerm]) -> m (Expr, [Expr])
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 :: 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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 :: 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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
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 :: 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 :: 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 :: 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 :: 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
$ Literal -> Pattern
forall e. Literal -> Pattern' e
A.LitP 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 :: 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 :: 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Expr where
  reifyWhen :: Bool -> Literal -> m Expr
reifyWhen = Bool -> Literal -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
  reify :: Literal -> m Expr
reify Literal
l = Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> Expr
A.Lit Literal
l)

instance Reify Term Expr where
  reifyWhen :: Bool -> Term -> m Expr
reifyWhen = Bool -> Term -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
  reify :: Term -> m Expr
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 :: 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 (Empty -> Term -> Term
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
forall a. HasCallStack => a
__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 :: 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 = Range -> NameInScope -> [NamePart] -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
C.InScope [String -> NamePart
C.Id 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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
es
    I.Def QName
x Elims
es   -> 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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow 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
      case Bool
isR Bool -> Bool -> Bool
|| ConInfo
ci ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec of
        Bool
True -> do
          Bool
showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
          let keep :: (Dom Name, Expr) -> Bool
keep (Dom Name
a, Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| Dom Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Name
a
          QName
r  <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
x
          [Dom Name]
xs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
forall a. a -> Maybe a -> a
fromMaybe [Dom Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
-> m (Maybe [Dom Name]) -> m [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe [Dom Name])
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom 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 [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Name, Expr) -> Either (FieldAssignment' Expr) ModuleName)
-> [(Dom Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map (FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left (FieldAssignment' Expr
 -> Either (FieldAssignment' Expr) ModuleName)
-> ((Dom Name, Expr) -> FieldAssignment' Expr)
-> (Dom Name, Expr)
-> Either (FieldAssignment' Expr) ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Expr -> FieldAssignment' Expr)
-> (Name, Expr) -> FieldAssignment' Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment ((Name, Expr) -> FieldAssignment' Expr)
-> ((Dom Name, Expr) -> (Name, Expr))
-> (Dom Name, Expr)
-> FieldAssignment' Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Name -> Name) -> (Dom Name, Expr) -> (Name, Expr)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Dom Name -> Name
forall t e. Dom' t e -> e
unDom) ([(Dom Name, Expr)] -> RecordAssigns)
-> [(Dom Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> a -> b
$ ((Dom Name, Expr) -> Bool)
-> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Dom Name, Expr) -> Bool
keep ([(Dom Name, Expr)] -> [(Dom Name, Expr)])
-> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
forall a b. (a -> b) -> a -> b
$ [Dom Name] -> [Expr] -> [(Dom Name, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Dom Name]
xs [Expr]
vs
        Bool
False -> 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 [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Tele (Dom Type)
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
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
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 (Name, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Abs Term
b
      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 (NamedArg Binder -> LamBinding
mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> NamedArg Binder) -> Binder -> NamedArg 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Literal
l
    I.Level Level
l      -> Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 (Arg Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 (Arg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 t a. Subst t 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 (Arg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 (Name, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Abs Type
b
          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 -> Telescope -> Expr -> Expr
A.Pi ExprInfo
noExprInfo [Range -> Maybe Expr -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
forall a. Range' a
noRange Maybe Expr
tac [ArgInfo -> Named NamedName Binder -> NamedArg Binder
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named NamedName Binder -> NamedArg Binder)
-> Named NamedName Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Binder -> Named NamedName Binder
forall name a. Maybe name -> a -> Named name a
Named (Dom Type -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
domName Dom Type
a) (Binder -> Named NamedName Binder)
-> Binder -> Named NamedName Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x] 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] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
df, Nat -> a -> Bool
forall a. Free a => Nat -> a -> Bool
freeIn Nat
0 a
b, t -> Bool
forall t. Free t => t -> Bool
closed t
a]

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

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

          MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
          (Maybe (Substitution' Term)
msub1,Tele (Dom Type)
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, Tele (Dom Type)
tel, Maybe (Substitution' Term)
msub2) <- MetaVariable
-> (Range
    -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (CheckpointId, Tele (Dom Type), 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, Tele (Dom Type), Maybe (Substitution' Term)))
 -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> (Range
    -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall a b. (a -> b) -> a -> b
$ \ Range
_ ->
                               (,,) (CheckpointId
 -> Tele (Dom Type)
 -> Maybe (Substitution' Term)
 -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m CheckpointId
-> m (Tele (Dom Type)
      -> Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' CheckpointId TCEnv -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
                                    m (Tele (Dom Type)
   -> Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Tele (Dom Type))
-> m (Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
                                    m (Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall (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)
 -> Tele (Dom Type)
 -> Maybe (Substitution' Term)
 -> (Maybe (Substitution' Term), Tele (Dom Type),
     Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Tele (Dom Type)
      -> Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Tele (Dom Type),
          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 (Tele (Dom Type)
   -> Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Tele (Dom Type),
       Maybe (Substitution' Term)))
-> m (Tele (Dom Type))
-> m (Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Tele (Dom Type),
          Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tele (Dom Type) -> m (Tele (Dom Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele (Dom Type)
tel m (Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Tele (Dom Type),
       Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Maybe (Substitution' Term), Tele (Dom Type),
      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
          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 :: [NamedName]
names = (String -> NamedName) -> [String] -> [NamedName]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> Ranged String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName)
-> (String -> Ranged String) -> String -> NamedName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Ranged String
forall a. a -> Ranged a
unranged) ([String] -> [NamedName]) -> [String] -> [NamedName]
forall a b. (a -> b) -> a -> b
$ Permutation
p Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
`applyPerm` Tele (Dom Type) -> [String]
teleNames Tele (Dom Type)
meta_tel
              named_es' :: [Elim' (Named_ Expr)]
named_es' = [NamedName] -> [Elim' Expr] -> [Elim' (Named_ Expr)]
forall name a. [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [NamedName]
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' Term -> Args -> Args
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sub_tel2G (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Permutation
p Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
`applyPerm` (Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
meta_tel :: [Arg Term])
                     es_G :: Elims
es_G = Substitution' Term
sub_local2G Substitution' Term -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> 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 ([NamedName] -> Nat
forall a. Sized a => a -> Nat
size [NamedName]
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' | 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
$ Literal -> Expr
A.Lit (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> String -> Literal
LitString Range
forall a. Range' a
noRange String
s
    I.Dummy String
"applyE" Elims
es | I.Apply (Arg ArgInfo
_ Term
h) : Elims
es' <- Elims
es -> do
                            Expr
h <- Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
h
                            [Elim' Expr]
es' <- Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (String -> Elims -> Term
I.Dummy String
s [])
      [Elim' Expr]
es <- Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 :: 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 :: * -> *).
(MonadReduce m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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' :: 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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 CompiledClauses
Fail, funClauses :: Defn -> [Clause]
funClauses = [Clause
cl] }
                | QName -> Bool
isAbsurdLambdaName QName
x -> do
                  -- get hiding info from last pattern, which should be ()
                  let h :: Hiding
h = NamedArg DeBruijnPattern -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (NamedArg DeBruijnPattern -> Hiding)
-> NamedArg DeBruijnPattern -> Hiding
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a. [a] -> a
last ([NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                      n :: Nat
n = [NamedArg DeBruijnPattern] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1  -- 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] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a]
init ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                            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 (NamedArg Binder -> LamBinding
A.mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
i (Binder -> NamedArg Binder) -> Binder -> NamedArg 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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Maybe System
sys) } ->
            (Nat, Maybe System) -> Maybe (Nat, Maybe System)
forall a. a -> Maybe a
Just ((Nat, Maybe System) -> Maybe (Nat, Maybe System))
-> (Tele (Dom Type) -> (Nat, Maybe System))
-> Tele (Dom Type)
-> Maybe (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Maybe System -> Maybe System
forall a. Maybe a -> Maybe a
Strict.toLazy Maybe System
sys) (Nat -> (Nat, Maybe System))
-> (Tele (Dom Type) -> Nat)
-> Tele (Dom Type)
-> (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Maybe (Nat, Maybe System))
-> m (Tele (Dom Type)) -> m (Maybe (Nat, Maybe System))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
          Defn
_ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
forall (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 -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem QName
x [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 -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x Nat
pars Maybe System
sys (Definition -> [Clause]
defClauses Definition
defn) Elims
es

        -- Otherwise (ordinary function call):
          Maybe (Nat, Maybe System)
_ -> do
           ([NamedArg Expr]
pad, [Elim' (Named NamedName 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 Tele (Dom Type)
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
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
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 :: [NamedArg Expr]
pad = [Dom (String, Type)]
-> (Dom (String, Type) -> NamedArg Expr) -> [NamedArg Expr]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom (String, Type)]
as ((Dom (String, Type) -> NamedArg Expr) -> [NamedArg Expr])
-> (Dom (String, Type) -> NamedArg Expr) -> [NamedArg 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 -> NamedArg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named_ Expr -> NamedArg Expr) -> Named_ Expr -> NamedArg Expr
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Expr -> Named_ Expr
forall name a. Maybe name -> a -> Named name a
Named (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
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' :: [NamedArg Expr]
pad' = Nat -> [NamedArg Expr] -> [NamedArg Expr]
forall a. Nat -> [a] -> [a]
drop Nat
n [NamedArg 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
- [NamedArg Expr] -> Nat
forall a. Sized a => a -> Nat
size [NamedArg 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 ([NamedArg Expr]
padVisNamed, [NamedArg Expr]
padRest) = (NamedArg Expr -> Bool)
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
filterAndRest NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible [NamedArg Expr]
pad'

              -- Remove the names from the visible arguments.
              let padVis :: [NamedArg Expr]
padVis  = (NamedArg Expr -> NamedArg Expr)
-> [NamedArg Expr] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((Named_ Expr -> Named_ Expr) -> NamedArg Expr -> NamedArg Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ Expr -> Named_ Expr) -> NamedArg Expr -> NamedArg Expr)
-> (Named_ Expr -> Named_ Expr) -> NamedArg Expr -> NamedArg 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) [NamedArg Expr]
padVisNamed

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

              -- ... and even the same name.
              let padSame :: [NamedArg Expr]
padSame = (NamedArg Expr -> Bool) -> [NamedArg Expr] -> [NamedArg 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)
-> (NamedArg Expr -> Maybe String) -> NamedArg Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Maybe String
forall a. LensNamed NamedName a => a -> Maybe String
bareNameOf) [NamedArg Expr]
padTail

              ([NamedArg Expr], [Elim' (Named NamedName Term)])
-> m ([NamedArg Expr], [Elim' (Named NamedName Term)])
forall (m :: * -> *) a. Monad m => a -> m a
return (([NamedArg Expr], [Elim' (Named NamedName Term)])
 -> m ([NamedArg Expr], [Elim' (Named NamedName Term)]))
-> ([NamedArg Expr], [Elim' (Named NamedName Term)])
-> m ([NamedArg Expr], [Elim' (Named NamedName Term)])
forall a b. (a -> b) -> a -> b
$ if [NamedArg Expr] -> Bool
forall a. Null a => a -> Bool
null [NamedArg Expr]
padTail Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
showImp
                then ([NamedArg Expr]
padVis           , (Elim' Term -> Elim' (Named NamedName Term))
-> Elims -> [Elim' (Named NamedName Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Named NamedName Term)
-> Elim' Term -> Elim' (Named NamedName Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Named NamedName Term
forall a name. a -> Named name a
unnamed) Elims
es')
                else ([NamedArg Expr]
padVis [NamedArg Expr] -> [NamedArg Expr] -> [NamedArg Expr]
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr]
padSame, Dom (String, Type) -> Elims -> [Elim' (Named NamedName 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
_ -> ([NamedArg Expr], [Elim' (Named NamedName Term)])
-> m ([NamedArg Expr], [Elim' (Named NamedName Term)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], (Elim' Term -> Elim' (Named NamedName Term))
-> Elims -> [Elim' (Named NamedName Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Named NamedName Term)
-> Elim' Term -> Elim' (Named NamedName Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Named NamedName Term
forall a name. a -> Named name a
unnamed) (Elims -> [Elim' (Named NamedName Term)])
-> Elims -> [Elim' (Named NamedName Term)]
forall a b. (a -> b) -> a -> b
$ Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)

           String -> Nat -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.def" Nat
70
             [ String
"  pad = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr] -> String
forall a. Show a => a -> String
show [NamedArg Expr]
pad
             , String
"  nes = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Elim' (Named NamedName Term)] -> String
forall a. Show a => a -> String
show [Elim' (Named NamedName 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
$ NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> NonEmpty QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty 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 -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_) Expr
hd0 [NamedArg 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 NamedName Term)] -> m [Elim' (Named_ Expr)]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify [Elim' (Named NamedName 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

    -- * 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.)

    -- * 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 -> Int -> Maybe System -> [I.Clause] -> I.Elims -> m Expr
    reifyExtLam :: QName -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x 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
vcat
        [ Doc
"npars =" Doc -> Doc -> Doc
<+> Nat -> Doc
forall a. Pretty a => a -> Doc
pretty Nat
npars
        , Doc
"es    =" Doc -> Doc -> Doc
<+> [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
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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 t. HasRange t => t -> Range
getRange QName
x)
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (ExprInfo -> DefInfo' Expr -> QName -> [Clause] -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo QName
x [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 [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
rest

-- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden :: 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 NamedName -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
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 a => Reify (Named n i) (Named n a) where
  reify :: Named n i -> m (Named n a)
reify = (i -> m a) -> Named n i -> m (Named n a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse i -> m a
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify
  reifyWhen :: Bool -> Named n i -> m (Named n a)
reifyWhen Bool
b = (i -> m a) -> Named n i -> m (Named n a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Bool -> i -> m a
forall i a (m :: * -> *).
(Reify i a, MonadReify m) =>
Bool -> i -> m a
reifyWhen Bool
b)

-- | Skip reification of implicit and irrelevant args if option is off.
instance (Reify i a) => Reify (Arg i) (Arg a) where
  reify :: Arg i -> m (Arg a)
reify (Arg ArgInfo
info i
i) = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a) -> m a -> m (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Bool -> i -> m a) -> i -> Bool -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> i -> m a
forall i a (m :: * -> *).
(Reify i a, MonadReify m) =>
Bool -> i -> m a
reifyWhen i
i (Bool -> m a) -> m Bool -> m a
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 :: Bool -> Arg i -> m (Arg a)
reifyWhen Bool
b Arg i
i = (i -> m a) -> Arg i -> m (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Bool -> i -> m a
forall i a (m :: * -> *).
(Reify i a, MonadReify m) =>
Bool -> i -> m a
reifyWhen Bool
b) Arg i
i

-- instance Reify Elim Expr where
--   reifyWhen = reifyWhenE
--   reify e = case e of
--     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 (LitString noRange 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 { 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 n a, LensOrigin n) => a -> a
removeNameUnlessUserWritten :: a -> a
removeNameUnlessUserWritten a
a
  | (n -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin (n -> Origin) -> Maybe n -> Maybe Origin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe n
forall name a. LensNamed name a => a -> Maybe name
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 n -> a -> a
forall name a. LensNamed name a => Maybe name -> a -> a
setNameOf Maybe n
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 :: 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 n a. (LensNamed n a, LensOrigin n) => a -> a
removeNameUnlessUserWritten) Patterns
ps) (m Patterns -> m Patterns) -> m Patterns -> m Patterns
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.implicit" Nat
30
      [ String
"stripping implicits"
      , String
"  ps   = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show 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 -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.implicit" Nat
30
      [ String
"  ps'  = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show 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. Arg (Named_ (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. Arg (Named_ (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 a. (LensHiding a, LensNamed a 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 :: * -> *) n b.
(Functor f, LensNamed n b, LensOrigin n) =>
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 t. HasRange t => t -> Range
getRange NamedArg (Pattern' e)
a
              goWild :: [NamedArg (Pattern' e)]
goWild = Bool -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
forall (f :: * -> *) n b.
(Functor f, LensNamed n b, LensOrigin n) =>
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 n a. (LensNamed n a, LensOrigin n) => a -> a
removeNameUnlessUserWritten
          stripName Bool
False = f b -> f b
forall a. a -> a
id

          -- TODO: vars appearing in EqualPs shouldn't be stripped.
          canStrip :: Arg (Named_ (Pattern' e)) -> Bool
canStrip Arg (Named_ (Pattern' e))
a = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ Arg (Named_ (Pattern' e)) -> Bool
forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ (Pattern' e))
a
            , Arg (Named_ (Pattern' e)) -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ (Pattern' e))
a Origin -> [Origin] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ Origin
UserWritten , Origin
CaseSplit ]
            , (NamedName -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin (NamedName -> Origin) -> Maybe NamedName -> Maybe Origin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg (Named_ (Pattern' e)) -> Maybe NamedName
forall name a. LensNamed name a => a -> Maybe name
getNameOf Arg (Named_ (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 (Arg (Named_ (Pattern' e)) -> Pattern' e
forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' e))
a)
            ]

          isUnnamedHidden :: a -> Bool
isUnnamedHidden a
x = a -> Bool
forall a. LensHiding a => a -> Bool
notVisible a
x Bool -> Bool -> Bool
&& Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing (a -> Maybe a
forall name a. LensNamed name a => a -> Maybe name
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 NamedName (Pattern' e) -> Named NamedName (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 NamedName (Pattern' e) -> Named NamedName (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 Pattern' e
p = case Pattern' e
p of
            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
            A.ProjP{}     -> Pattern' e
p
            A.DefP PatInfo
_ AmbiguousQName
_ [NamedArg (Pattern' e)]
_  -> Pattern' e
p
            A.DotP PatInfo
_ e
e    -> Pattern' e
p
            A.WildP PatInfo
_     -> Pattern' e
p
            A.AbsurdP PatInfo
_   -> Pattern' e
p
            A.LitP 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__ -- p
            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?
            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?

          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 :: 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) -> f b -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> f b -> f b)
-> (Set Name -> b -> b) -> Set Name -> f b -> f b
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)              where
instance BlankVars a => BlankVars (Named s a)          where
instance BlankVars a => BlankVars [a]                  where
-- instance BlankVars a => BlankVars (A.Pattern' a)       where  -- see case EqualP !
instance BlankVars a => BlankVars (FieldAssignment' a) where

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 (A.WhereDecls Maybe ModuleName
_ []) Bool
ca) =
    let 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
    in  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
  blank Set Name
bound (A.Clause LHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
_ Bool
ca) = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__

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 [Pattern]
wps Patterns
ps) = ((LHSCore, [Pattern]) -> Patterns -> LHSCore)
-> ((LHSCore, [Pattern]), Patterns) -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((LHSCore -> [Pattern] -> Patterns -> LHSCore)
-> (LHSCore, [Pattern]) -> Patterns -> LHSCore
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry LHSCore -> [Pattern] -> Patterns -> LHSCore
forall e.
LHSCore' e -> [Pattern' e] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith) (((LHSCore, [Pattern]), Patterns) -> LHSCore)
-> ((LHSCore, [Pattern]), Patterns) -> LHSCore
forall a b. (a -> b) -> a -> b
$ Set Name
-> ((LHSCore, [Pattern]), Patterns)
-> ((LHSCore, [Pattern]), Patterns)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound ((LHSCore
h, [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 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)

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
_                -> Expr
e
    A.Proj{}               -> Expr
e
    A.Con AmbiguousQName
_                -> Expr
e
    A.Lit 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 NamedArg Expr
e2          -> (Expr -> NamedArg Expr -> Expr) -> (Expr, NamedArg Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
i) ((Expr, NamedArg Expr) -> Expr) -> (Expr, NamedArg Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Expr, NamedArg Expr) -> (Expr, NamedArg Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e1, NamedArg 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 QName
f [Clause]
cs -> ExprInfo -> DefInfo' Expr -> QName -> [Clause] -> Expr
A.ExtendedLam ExprInfo
i DefInfo' Expr
d QName
f ([Clause] -> Expr) -> [Clause] -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> [Clause] -> [Clause]
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound [Clause]
cs
    A.Pi ExprInfo
i Telescope
tel Expr
e           -> let bound' :: Set Name
bound' = Telescope -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn Telescope
tel Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
                              in  (Telescope -> Expr -> Expr) -> (Telescope, Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Telescope -> Expr -> Expr
A.Pi ExprInfo
i) ((Telescope, Expr) -> Expr) -> (Telescope, Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Set Name -> (Telescope, Expr) -> (Telescope, Expr)
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' (Telescope
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.Set ExprInfo
_ Integer
_              -> Expr
e
    A.Prop ExprInfo
_ Integer
_             -> Expr
e
    A.Let ExprInfo
_ [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.Tactic {}            -> 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
_ [WithHiding Expr]
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 [NamedArg Binder]
n Expr
e) = Range -> Maybe Expr -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
r Maybe Expr
t [NamedArg 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
_ [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 [Pattern]
wps Patterns
ps) = ((LHSCore, [Pattern]), Patterns) -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn ((LHSCore
h, [Pattern]
wps), Patterns
ps)

instance Binder A.Pattern where
  varsBoundIn :: Pattern -> Set Name
varsBoundIn = (Pattern -> Set Name) -> Pattern -> Set Name
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m) -> p -> m
foldAPattern ((Pattern -> Set Name) -> Pattern -> Set Name)
-> (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
_         -> Set Name
forall a. Null a => a
empty    -- Not x because of #2414 (?)
    A.ConP ConPatInfo
_ AmbiguousQName
_ Patterns
_        -> Set Name
forall a. Null a => a
empty
    A.ProjP{}           -> Set Name
forall a. Null a => a
empty
    A.DefP PatInfo
_ AmbiguousQName
_ Patterns
_        -> 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
_ Patterns
_ -> Set Name
forall a. Null a => a
empty
    A.RecP PatInfo
_ [FieldAssignment' Pattern]
_          -> Set Name
forall a. Null a => a
empty
    A.EqualP{}          -> Set Name
forall a. Null a => a
empty
    A.WithP PatInfo
_ Pattern
_         -> Set Name
forall a. Null a => a
empty

instance Binder a => Binder (A.Binder' a) where
  varsBoundIn :: Binder' a -> Set Name
varsBoundIn (A.Binder Maybe Pattern
p 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
_ NamedArg Binder
x) = NamedArg Binder -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn NamedArg 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
_ [NamedArg Binder]
xs Expr
_) = [NamedArg Binder] -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn [NamedArg Binder]
xs
  varsBoundIn (TLet Range
_ [LetBinding]
bs)      = [LetBinding] -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn [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) where
instance Binder a => Binder (Arg a)              where
instance Binder a => Binder (Named x a)          where
instance Binder a => Binder [a]                  where
instance Binder a => Binder (Maybe a)            where

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 :: [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 NamedName 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 NamedName 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 :: 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 NamedName a => a -> Maybe String
bareNameOf NamedArg p
a) =
          (Named NamedName p -> Named NamedName p)
-> NamedArg p -> NamedArg p
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (p -> Named NamedName p
forall a name. a -> Named name a
unnamed (p -> Named NamedName p)
-> (Named NamedName p -> p)
-> Named NamedName p
-> Named NamedName p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName 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 :: 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 :: DeBruijnPattern -> m Pattern
reifyPat DeBruijnPattern
p = do
     String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.pat" Nat
80 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reifying pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DeBruijnPattern -> String
forall a. Show a => a -> String
show 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
$ Literal -> Pattern
forall e. Literal -> Pattern' e
A.LitP 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
$ Literal -> Pattern
forall e. Literal -> Pattern' e
A.LitP 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 :: 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 = Range -> NameInScope -> [NamePart] -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
C.InScope [ String -> NamePart
C.Id String
y ] }

    reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
    reifyDotP :: 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v

    reifyConP :: MonadReify m
              => ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
              -> m A.Pattern
    reifyConP :: 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 :: [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 :: 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
        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 Name]
fs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
forall a. a -> Maybe a -> a
fromMaybe [Dom Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
-> m (Maybe [Dom Name]) -> m [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe [Dom Name])
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom Name])
getRecordFieldNames_ QName
r
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Dom Name] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom 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 Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern)
-> [Dom Name] -> Patterns -> [FieldAssignment' Pattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Dom Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern
forall t a. Dom' t Name -> NamedArg a -> FieldAssignment' a
mkFA [Dom 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__

instance Reify (QNamed I.Clause) A.Clause where
  reify :: QNamed Clause -> m Clause
reify (QNamed QName
f Clause
cl) = NamedClause -> m Clause
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True Clause
cl)

instance Reify NamedClause A.Clause where
  reify :: NamedClause -> m Clause
reify (NamedClause QName
f Bool
toDrop Clause
cl) = Tele (Dom Type) -> m Clause -> m Clause
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Tele (Dom Type)
clauseTel Clause
cl) (m Clause -> m Clause) -> m Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ do
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.clause" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reifying NamedClause"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  f      = " 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
"\n  toDrop = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
toDrop
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  cl     = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clause -> String
forall a. Show a => a -> String
show 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 -> Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Nat) -> m (Tele (Dom Type)) -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
      (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 -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.clause" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reifying NamedClause, lhs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpineLHS -> String
forall a. Show a => a -> String
show 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.clause" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reifying NamedClause, rhs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RHS -> String
forall a. Show a => a -> String
show 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 -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.clause" Nat
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reified NamedClause, result = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clause -> String
forall a. Show a => a -> String
show 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 :: 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) [A.Clause] where
  reify :: QNamed System -> m [Clause]
reify (QNamed QName
f (System Tele (Dom Type)
tel [(Face, Term)]
sys)) = Tele (Dom Type) -> m [Clause] -> m [Clause]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (m [Clause] -> m [Clause]) -> m [Clause] -> m [Clause]
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
$ Tele (Dom Type) -> String
forall a. Show a => a -> String
show Tele (Dom Type)
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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 (Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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
$ Tele (Dom Type) -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
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 Expr where
    reifyWhen :: Bool -> Type -> m Expr
reifyWhen = Bool -> Type -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
    reify :: Type -> m Expr
reify (I.El Sort
_ Term
t) = Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
t

instance Reify Sort Expr where
    reifyWhen :: Bool -> Sort -> m Expr
reifyWhen = Bool -> Sort -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
    reify :: Sort -> m Expr
reify Sort
s = do
      Sort
s <- Sort -> m Sort
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort
s
      case Sort
s of
        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
$ ExprInfo -> Integer -> Expr
A.Set ExprInfo
noExprInfo Integer
n
        I.Type Level
a -> do
          Expr
a <- Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Integer -> Expr
A.Set ExprInfo
noExprInfo Integer
0) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        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
$ ExprInfo -> Integer -> Expr
A.Prop ExprInfo
noExprInfo Integer
n
        I.Prop Level
a -> do
          Expr
a <- Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Integer -> Expr
A.Prop ExprInfo
noExprInfo Integer
0) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        Sort
I.Inf       -> do
          I.Def QName
inf [] <- 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
builtinSetOmega
          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
inf
        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
        I.PiSort Dom Type
a Abs Sort
s -> 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 (Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a, 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
s)
          let app :: Expr -> Expr -> Expr
app Expr
x Expr
y = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> NamedArg 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 (Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Sort
s1 , Sort
s2)
          let app :: Expr -> Expr -> Expr
app Expr
x Expr
y = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> NamedArg 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 Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (Name -> Expr
A.Var Name
univs) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e
        I.MetaS MetaId
x Elims
es -> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> Term -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x Elims
es
        I.DefS QName
d Elims
es -> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> Term -> m Expr
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
$ Literal -> Expr
A.Lit (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> String -> Literal
LitString Range
forall a. Range' a
noRange String
s

instance Reify Level Expr where
  reifyWhen :: Bool -> Level -> m Expr
reifyWhen = Bool -> Level -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
  reify :: Level -> m Expr
reify Level
l   = m Bool -> m Expr -> m Expr -> m Expr
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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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 Expr -> m Expr) -> m Expr -> m Expr
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 a) => Reify (Abs i) (Name, a) where
  reify :: Abs i -> m (Name, a)
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, a)) -> m (Name, a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
name -> (Name
name,) (a -> (Name, a)) -> m a -> m (Name, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> m a
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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
    a
e <- Name -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Name
x -- type doesn't matter
         (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ i -> m a
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify i
v
    (Name, a) -> m (Name, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x,a
e)

instance Reify I.Telescope A.Telescope where
  reify :: Tele (Dom Type) -> m Telescope
reify Tele (Dom Type)
EmptyTel = Telescope -> m Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return []
  reify (ExtendTel Dom Type
arg Abs (Tele (Dom Type))
tel) = do
    Arg ArgInfo
info Expr
e <- Dom Type -> m (Arg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Dom Type
arg
    (Name
x, Telescope
bs)  <- Abs (Tele (Dom Type)) -> m (Name, Telescope)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Abs (Tele (Dom Type))
tel
    let r :: Range
r    = Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e
        name :: Maybe NamedName
name = Dom Type -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
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 a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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
    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 -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
r Maybe Expr
tac [ArgInfo -> Named NamedName Binder -> NamedArg Binder
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named NamedName Binder -> NamedArg Binder)
-> Named NamedName Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Binder -> Named NamedName Binder
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
name (Binder -> Named NamedName Binder)
-> Binder -> Named NamedName Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x] Expr
e TypedBinding -> Telescope -> Telescope
forall a. a -> [a] -> [a]
: Telescope
bs

instance Reify i a => Reify (Dom i) (Arg a) where
    reify :: Dom i -> m (Arg a)
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 -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a) -> m a -> m (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> m a
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify i
i

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

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

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

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

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