{-# LANGUAGE NondecreasingIndentation   #-}

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

    TODO

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

import Prelude hiding (null)

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

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

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

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

import Agda.Interaction.Options

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

import Agda.Utils.Impossible


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


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

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

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

-- | Drops hidden arguments unless --show-implicit.
nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr
nelims :: forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
e [] = 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) =
  forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Named_ Expr
r) [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Apply Arg (Named_ Expr)
arg : [Elim' (Named_ Expr)]
es) = do
  Arg (Named_ Expr)
arg <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Arg (Named_ Expr)
arg  -- This replaces the arg by _ if irrelevant
  Bool
dontShowImp <- Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
  let hd :: Expr
hd | forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Expr)
arg Bool -> Bool -> Bool
&& Bool
dontShowImp = Expr
e
         | Bool
otherwise                     = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e Arg (Named_ Expr)
arg
  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)             = 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  = forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [Elim' (Named_ Expr)]
es
                                    | Bool
otherwise =
  forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d)) [Elim' (Named_ Expr)]
es

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

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

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

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

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

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

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

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

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

class Reify i where
    type ReifiesTo i

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

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

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

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

instance Reify Expr where
    type ReifiesTo Expr = Expr

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

instance Reify MetaId where
    type ReifiesTo MetaId = Expr

    reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> MetaId -> m (ReifiesTo MetaId)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
    reify :: forall (m :: * -> *).
MonadReify m =>
MetaId -> m (ReifiesTo MetaId)
reify MetaId
x = do
      Bool
b <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
      MetaInfo
mi  <- MetaVariable -> MetaInfo
mvInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
      let mi' :: MetaInfo
mi' = Info.MetaInfo
                 { metaRange :: Range
metaRange          = forall a. HasRange a => a -> Range
getRange forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
                 , metaScope :: ScopeInfo
metaScope          = forall a. Closure a -> ScopeInfo
clScope forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
                 , metaNumber :: Maybe MetaId
metaNumber         = if Bool
b then forall a. Maybe a
Nothing else 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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
      forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe InteractionId
Nothing | Bool
b -> do
          InteractionId
ii <- forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint Bool
False forall a. Range' a
noRange forall a. Maybe a
Nothing
          forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
x
          forall (m :: * -> *) a. Monad m => a -> m a
return 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     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaInfo -> InteractionId -> Expr
A.QuestionMark MetaInfo
mi' InteractionId
ii

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

instance Reify DisplayTerm where
  type ReifiesTo DisplayTerm = Expr

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

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

-- | @reifyDisplayFormP@ tries to recursively
--   rewrite a lhs with a display form.
--
--   Note: we are not necessarily in the empty context upon entry!
reifyDisplayFormP
  :: MonadReify m
  => QName         -- ^ LHS head symbol
  -> A.Patterns    -- ^ Patterns to be taken into account to find display form.
  -> A.Patterns    -- ^ Remaining trailing patterns ("with patterns").
  -> m (QName, A.Patterns) -- ^ New head symbol and new patterns.
reifyDisplayFormP :: forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps Patterns
wps = do
  let fallback :: m (QName, Patterns)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Patterns
ps forall a. [a] -> [a] -> [a]
++ Patterns
wps)
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled m (QName, Patterns)
fallback 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") $
      forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg (Named_ Pattern)
p Nat
i -> forall a. Arg a -> Elim' a
I.Apply forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern)
p forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
I.var Nat
i) Patterns
ps [Nat
0..]
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
60 forall a b. (a -> b) -> a -> b
$
      String
"display form of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Patterns
ps forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Patterns
wps forall a. [a] -> [a] -> [a]
++ String
":\n  " forall a. [a] -> [a] -> [a]
++ 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') <- forall (m :: * -> *).
MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d
        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.display" Nat
70 forall a b. (a -> b) -> a -> b
$ do
          Doc
doc <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS forall a. Null a => a
empty QName
f' (Patterns
ps' forall a. [a] -> [a] -> [a]
++ Patterns
wps' forall a. [a] -> [a] -> [a]
++ Patterns
wps)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
            [ Doc
"rewritten lhs to"
            , Doc
"  lhs' = " Doc -> Doc -> Doc
<+> Doc
doc
            ]
        forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f' Patterns
ps' (Patterns
wps' forall a. [a] -> [a] -> [a]
++ Patterns
wps)
      Maybe DisplayTerm
_ -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
70 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
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DisplayTerm -> Bool
okDisplayTerm [DisplayTerm]
ds  Bool -> Bool -> 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)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
    okDisplayForm (DDef QName
f [Elim' DisplayTerm]
es)          = 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 forall a b. (a -> b) -> a -> b
$ 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 = forall a. LensHiding a => a -> Bool
notVisible Arg Term
arg Bool -> Bool -> Bool
&& case 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
    okTerm (I.Def QName
x []) = forall a. IsNoName a => a -> Bool
isNoName 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 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
I.Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Arg a
defaultArg) [DisplayTerm]
ds1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (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, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es, [])
    flattenWith DisplayTerm
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

        termToPat (DTerm (I.Con ConHead
c ConInfo
ci Elims
vs)) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
           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)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
MonadReify m =>
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
vs

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

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

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

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

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

        -- TODO: restructure this to avoid having to repeat the code for reify
        termToExpr :: MonadReify m => Term -> m A.Expr
        termToExpr :: forall (m :: * -> *). MonadReify m => Term -> m Expr
termToExpr Term
v = do
          forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
60 forall a b. (a -> b) -> a -> b
$ String
"termToExpr " forall a. [a] -> [a] -> [a]
++ 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
              forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c))) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
            I.Def QName
f Elims
es -> do
              let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
              forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (QName -> Expr
A.Def QName
f) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
            I.Var Nat
n Elims
es -> do
              let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 forall a. Ord a => a -> a -> Bool
< Nat
len
                   then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pattern -> Expr
A.patternToExpr forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Nat -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Patterns
ps Nat
n
                   else forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Nat -> Term
I.var (Nat
n forall a. Num a => a -> a -> a
- Nat
len))
              forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
            Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Underscore a => a
underscore

instance Reify Literal where
  type ReifiesTo Literal = Expr

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

instance Reify Term where
  type ReifiesTo Term = Expr

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

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

reifyTerm :: MonadReify m => Bool -> Term -> m Expr
reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
expandAnonDefs0 Term
v0 = do
  -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
  Bool
metasBare <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
  Term
v <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    I.MetaV MetaId
x Elims
_ | Bool
metasBare -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x []
    Term
v -> 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 <- forall (m :: * -> *) a. Monad m => a -> m a
return Bool
expandAnonDefs0 forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let pred :: ProjOrigin -> Bool
pred = if Bool
havePfp then (forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPrefix) else (forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPostfix)
  case (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
pred Term
v of
    -- Hack to print generalized field projections with nicer names. Should
    -- only show up in errors. Check the spined form!
    Term
_ | I.Var Nat
n (I.Proj ProjOrigin
_ QName
p : Elims
es) <- Term
v,
        Just String
name <- QName -> Maybe String
getGeneralizedFieldName QName
p -> do
      let fakeName :: Name
fakeName = (QName -> Name
qnameName QName
p) {nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
name} -- TODO: infix names!?
      forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
fakeName) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
    I.Var Nat
n Elims
es -> do
      Name
x <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ forall a b. (a -> b) -> a -> b
$ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Nat
n) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Maybe Name)
nameOfBV' Nat
n
      forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
x) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
    I.Def QName
x Elims
es -> do
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.def" Nat
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reifying def" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
x
      (QName
x, Elims
es) <- forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x Elims
es
      forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
es forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
isGeneratedRecordConstructor QName
x
      if Bool
isR Bool -> Bool -> Bool
|| ConInfo
ci forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec
        then do
          Bool
showImp <- forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
          let keep :: (Dom' Term Name, Expr) -> Bool
keep (Dom' Term Name
a, Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| forall a. LensHiding a => a -> Bool
visible Dom' Term Name
a
          QName
r <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
x
          [Dom' Term Name]
xs <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
          [Expr]
vs <- forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
vs)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
noExprInfo forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Name -> a -> FieldAssignment' a
FieldAssignment forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall t e. Dom' t e -> e
unDom) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Dom' Term Name, Expr) -> Bool
keep forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Dom' Term Name]
xs [Expr]
vs
        else forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
vs forall a b. (a -> b) -> a -> b
$ do
          Definition
def <- 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 <- 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
np) forall a. HasCallStack => a
__IMPOSSIBLE__
          let h :: Expr
h = AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
x)
          if forall a. Null a => a -> Bool
null Elims
vs
            then forall (m :: * -> *) a. Monad m => a -> m a
return Expr
h
            else do
              [Arg Expr]
es <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Eq a => a -> a -> Bool
== Nat
0
                then forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es
                else do
                  -- Get name of first argument from type of constructor.
                  -- Here, we need the reducing version of @telView@
                  -- because target of constructor could be a definition
                  -- expanding into a function type.  See test/succeed/NameFirstIfHidden.agda.
                  TelV Telescope
tel Type
_ <- 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) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
np forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                  case [Dom (String, Type)]
rest of
                    -- Andreas, 2012-09-18
                    -- If the first regular constructor argument is hidden,
                    -- we keep the parameters to avoid confusion.
                    (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : [Dom (String, Type)]
_) | forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
                      let us :: [Arg Expr]
us = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall a. Nat -> [a] -> [a]
drop Nat
n [Dom (String, Type)]
pars) forall a b. (a -> b) -> a -> b
$ \(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}) ->
                            -- setRelevance Relevant $
                            forall a. LensHiding a => a -> a
hideOrKeepInstance forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a. Underscore a => a
underscore
                      forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h forall a b. (a -> b) -> a -> b
$ [Arg Expr]
us forall a. [a] -> [a] -> [a]
++ [Arg Expr]
es -- Note: unless --show-implicit, @apps@ will drop @us@.
                    -- otherwise, we drop all parameters
                    [Dom (String, Type)]
_ -> 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) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Term
b
      -- #4160: Hacky solution: if --show-implicit, treat all lambdas as user-written. This will
      -- prevent them from being dropped by AbstractToConcrete (where we don't have easy access to
      -- the --show-implicit flag.
      ArgInfo
info <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten ArgInfo
info) (forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info 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        -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Literal
l
    I.Level Level
l      -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
l
    I.Pi Dom Type
a Abs Type
b       -> case Abs Type
b of
        NoAbs String
_ Type
b'
          | forall a. LensHiding a => a -> Bool
visible Dom Type
a, Bool -> Bool
not (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a) -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun forall a b. (a -> b) -> a -> b
$ ExprInfo
noExprInfo) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Dom Type
a, Type
b')
            -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
            -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
            -- and (b) the name of the binder might matter.
            -- See issue 951 (a) and 952 (b).
            --
            -- Amy, 2022-09-05: Can't be finite either, since otherwise
            -- we say ".(IsOne φ) → A ≠ .(IsOne φ) → A" with no
            -- indication of which is finite and which isn't
          | Bool
otherwise   -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
a
        Abs Type
b               -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall {m :: * -> *} {a} {t}.
(MonadTCEnv m, Free a, Free t) =>
t -> a -> m Bool
domainFree Dom Type
a (forall a. Subst a => Abs a -> a
absBody Abs Type
b))
            {- then -} (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a. Underscore a => a
underscore)
            {- else -} (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
a)
      where
        mkPi :: Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg ArgInfo
info Expr
a') = do
          Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a
          (Name
x, Expr
b) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Type
b
          let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named (forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
domName Dom Type
a) forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
noExprInfo
            (forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind forall a. Range' a
noRange (Maybe Expr -> Bool -> TypedBindingInfo
TypedBindingInfo Maybe Expr
tac (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a)) List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
a')
            Expr
b
        -- We can omit the domain type if it doesn't have any free variables
        -- and it's mentioned in the target type.
        domainFree :: t -> a -> m Bool
domainFree t
a a
b = do
          Bool
df <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintDomainFreePi
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
df Bool -> Bool -> Bool
&& forall a. Free a => Nat -> a -> Bool
freeIn Nat
0 a
b Bool -> Bool -> Bool
&& forall t. Free t => t -> Bool
closed t
a

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

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

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

          Bool
opt_show_ids <- forall (m :: * -> *). HasOptions m => m Bool
showIdentitySubstitutions
          let
              addNames :: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames []    [Elim' a]
es = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) [Elim' a]
es
              addNames [name]
_     [] = []
              addNames [name]
xs     (I.Proj{} : [Elim' 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 (forall a. Arg a -> Elim' a
I.Apply (forall a. a -> Arg a
defaultArg a
r) forall a. a -> [a] -> [a]
: [Elim' a]
es)
              addNames (name
x:[name]
xs) (I.Apply Arg a
arg : [Elim' a]
es) =
                forall a. Arg a -> Elim' a
I.Apply (forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just name
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Substitution Arg a
arg)) 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 = forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP (forall a. Sized a => a -> Nat
size [a]
vs) Permutation
p) [a]
vs

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

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

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

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

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

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

        -- #3004: give up if we have to print a pattern lambda inside its own body!
        [QName]
alreadyPrinting <- 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right{} } -> forall a. HasCallStack => a
__IMPOSSIBLE__
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
b Maybe System
sys) } ->
            forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy Maybe System
sys) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Nat
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
          Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        case Maybe (Nat, Maybe System)
extLam of
          Just (Nat
pars, Maybe System
sys) | Bool
df, QName
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [QName]
alreadyPrinting ->
            forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' [QName] TCEnv
ePrintingPatternLambdas (QName
x forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x (Definition -> ArgInfo
defArgInfo Definition
defn) Nat
pars Maybe System
sys
              (Definition -> [Clause]
defClauses Definition
defn) Elims
es

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

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

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

              TelV Telescope
tel Type
_ <- 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) = forall a. Nat -> [a] -> ([a], [a])
splitAt (Nat
np forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
                  dom :: Dom (String, Type)
dom = forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom (String, Type)]
rest

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

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

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

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

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

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

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

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

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

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

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

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

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

    reifyExtLam
      :: MonadReify m
      => QName -> ArgInfo -> Int -> Maybe System -> [I.Clause]
      -> I.Elims -> m Expr
    reifyExtLam :: forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x ArgInfo
ai Nat
npars Maybe System
msys [Clause]
cls Elims
es = do
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
10 forall a b. (a -> b) -> a -> b
$ String
"reifying extended lambda " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x
      forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
50 forall a b. (a -> b) -> a -> b
$ Doc -> String
render forall a b. (a -> b) -> a -> b
$ Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
        [ Doc
"npars =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Nat
npars
        , Doc
"es    =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Nat -> a -> Doc
prettyPrec Nat
10) Elims
es)
        , Doc
"def   =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map 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) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars Elims
es
      let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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 <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
               (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
x Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cls)
               (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. QName -> a -> QNamed a
QNamed QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. Apply t => t -> Args -> t
`apply` Args
pars))
      let cx :: Name
cx     = Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          dInfo :: DefInfo' Expr
dInfo  = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cx Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef
                     (forall a. HasRange a => a -> Range
getRange QName
x)
          erased :: Erased
erased = case forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
            Quantity0 Q0Origin
o -> Q0Origin -> Erased
Erased Q0Origin
o
            Quantityω QωOrigin
o -> QωOrigin -> Erased
NotErased QωOrigin
o
            Quantity1 Q1Origin
o -> forall a. HasCallStack => a
__IMPOSSIBLE__
          lam :: Expr
lam = case [Clause]
cls of
            []       -> ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
NotHidden
            (Clause
cl:[Clause]
cls) -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo Erased
erased QName
x (Clause
cl forall a. a -> [a] -> NonEmpty a
:| [Clause]
cls)
      forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
lam forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
rest

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

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

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

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

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

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

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

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

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

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


-- | Removes implicit arguments that are not needed, that is, that don't bind
--   any variables that are actually used and doesn't do pattern matching.
--   Doesn't strip any arguments that were written explicitly by the user.
stripImplicits :: MonadReify m => A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits :: forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits Patterns
params Patterns
ps = do
  -- if --show-implicit we don't need the names
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten) Patterns
ps) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"stripping implicits"
      , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"ps   =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow Patterns
ps
      ]
    let ps' :: Patterns
ps' = Patterns -> Patterns
blankDots forall a b. (a -> b) -> a -> b
$ forall {e}. [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip Patterns
ps
    forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"ps'  =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow Patterns
ps'
      ]
    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 = forall a. BlankVars a => Set Name -> a -> a
blank (forall a. Binder a => a -> Set Name
varsBoundIn forall a b. (a -> b) -> a -> b
$ Patterns
params forall a. [a] -> [a] -> [a]
++ Patterns
ps) Patterns
ps

      strip :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip [NamedArg (Pattern' e)]
ps = 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.
            | forall {e}. Arg (Named_ (Pattern' e)) -> Bool
canStrip NamedArg (Pattern' e)
a =
                 if   forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {e}. Arg (Named_ (Pattern' e)) -> Bool
canStrip forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
isUnnamedHidden [NamedArg (Pattern' e)]
as
                 then Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
False [NamedArg (Pattern' e)]
as
                 else [NamedArg (Pattern' e)]
goWild
            -- Other arguments are kept.
            | Bool
otherwise = forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos (NamedArg (Pattern' e) -> NamedArg (Pattern' e)
stripArg NamedArg (Pattern' e)
a) 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'     = forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' e)
a forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
Info.PatRange forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange NamedArg (Pattern' e)
a
              goWild :: [NamedArg (Pattern' e)]
goWild = forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos NamedArg (Pattern' e)
a' 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  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten
          stripName Bool
False = 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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ (Pattern' e))
a
            , forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ (Pattern' e))
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ Origin
UserWritten , Origin
CaseSplit ]
            , (forall a. LensOrigin a => a -> Origin
getOrigin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf Arg (Named_ (Pattern' e))
a) forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Origin
UserWritten
            , forall {e}. Pattern' e -> Bool
varOrDot (forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' e))
a)
            ]

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

          stripArg :: NamedArg (Pattern' e) -> NamedArg (Pattern' e)
stripArg NamedArg (Pattern' e)
a = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' e -> Pattern' e
stripPat) NamedArg (Pattern' e)
a

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

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

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

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

instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
  blank :: Set Name -> (a, b) -> (a, b)
blank Set Name
bound (a
x, b
y) = (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x, 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)  = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x
  blank Set Name
bound (Right b
y) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> 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 = forall a. a -> a
id

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

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

instance BlankVars A.Pattern where
  blank :: Set Name -> Pattern -> Pattern
blank Set Name
bound Pattern
p = case Pattern
p of
    A.VarP BindName
_      -> Pattern
p   -- do not blank pattern vars
    A.ConP ConPatInfo
c AmbiguousQName
i Patterns
ps -> forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
c AmbiguousQName
i forall a b. (a -> b) -> a -> b
$ 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 -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
    A.DotP PatInfo
i Expr
e    -> forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.WildP PatInfo
_     -> Pattern
p
    A.AbsurdP PatInfo
_   -> Pattern
p
    A.LitP PatInfo
_ Literal
_    -> Pattern
p
    A.AsP PatInfo
i BindName
n Pattern
p   -> forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
n forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p
    A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.RecP PatInfo
i [FieldAssignment' Pattern]
fs   -> forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i forall a b. (a -> b) -> a -> b
$ 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   -> forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p)
    A.AnnP PatInfo
i Expr
a Pattern
p  -> forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
a) (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 forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.Var Name
x                  -> if Name
x forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
bound then Expr
e
                                else MetaInfo -> Expr
A.Underscore MetaInfo
emptyMetaInfo  -- Here is the action!
    A.Def' QName
_ Suffix
_               -> Expr
e
    A.Proj{}                 -> Expr
e
    A.Con AmbiguousQName
_                  -> Expr
e
    A.Lit ExprInfo
_ Literal
_                -> Expr
e
    A.QuestionMark{}         -> Expr
e
    A.Underscore MetaInfo
_           -> Expr
e
    A.Dot ExprInfo
i Expr
e                -> ExprInfo -> Expr -> Expr
A.Dot ExprInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
    A.App AppInfo
i Expr
e1 Arg (Named_ Expr)
e2            -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e1, Arg (Named_ Expr)
e2)
    A.WithApp ExprInfo
i Expr
e [Expr]
es         -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> [Expr] -> Expr
A.WithApp ExprInfo
i) forall a b. (a -> b) -> a -> b
$ 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' = forall a. Binder a => a -> Set Name
varsBoundIn LamBinding
b forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
                                in  ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound LamBinding
b) (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' Expr
e)
    A.AbsurdLam ExprInfo
_ Hiding
_          -> Expr
e
    A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f List1 Clause
cs -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound List1 Clause
cs
    A.Pi ExprInfo
i Telescope1
tel Expr
e             -> let bound' :: Set Name
bound' = forall a. Binder a => a -> Set Name
varsBoundIn Telescope1
tel forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
                                in  forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' (Telescope1
tel, Expr
e)
    A.Generalized {}         -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Fun ExprInfo
i Arg Expr
a Expr
b              -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Arg Expr
a, Expr
b)
    A.Let ExprInfo
_ List1 LetBinding
_ Expr
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Rec ExprInfo
i RecordAssigns
es               -> ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound RecordAssigns
es
    A.RecUpdate ExprInfo
i Expr
e Assigns
es       -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> Assigns -> Expr
A.RecUpdate ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, Assigns
es)
    A.Quote {}               -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.QuoteTerm {}           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Unquote {}             -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.DontCare Expr
v             -> Expr -> Expr
A.DontCare forall a b. (a -> b) -> a -> b
$ 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 = 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 (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e) Maybe Expr
mc
  blank Set Name
bound RHS
AbsurdRHS              = RHS
AbsurdRHS
  blank Set Name
bound (WithRHS QName
_ [WithExpr]
es [Clause]
clauses) = forall a. HasCallStack => a
__IMPOSSIBLE__ -- NZ
  blank Set Name
bound (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
_) = 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 forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound TypedBinding
bs

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

instance Binder A.LHS where
  varsBoundIn :: LHS -> Set Name
varsBoundIn (A.LHS LHSInfo
_ LHSCore
core) = 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)     = forall a. Binder a => a -> Set Name
varsBoundIn Patterns
ps
  varsBoundIn (A.LHSProj AmbiguousQName
_ NamedArg LHSCore
b Patterns
ps)   = forall a. Binder a => a -> Set Name
varsBoundIn (NamedArg LHSCore
b, Patterns
ps)
  varsBoundIn (A.LHSWith LHSCore
h [Arg Pattern]
wps Patterns
ps) = forall a. Binder a => a -> Set Name
varsBoundIn ((LHSCore
h, [Arg Pattern]
wps), Patterns
ps)

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

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

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

instance Binder BindName where
  varsBoundIn :: BindName -> Set Name
varsBoundIn BindName
x = 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
_) = forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
  varsBoundIn (LetPatBind LetInfo
_ Pattern
p Expr
_)  = forall a. Binder a => a -> Set Name
varsBoundIn Pattern
p
  varsBoundIn LetApply{}          = forall a. Null a => a
empty
  varsBoundIn LetOpen{}           = forall a. Null a => a
empty
  varsBoundIn LetDeclaredVariable{} = forall a. Null a => a
empty

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

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


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

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

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

    reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
    reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x = do
      Name
n <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
      let y :: String
y = DBPatVar -> String
dbPatVarName DBPatVar
x
      if | String
y forall a. Eq a => a -> a -> Bool
== String
"_" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP 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.
         | forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
n) forall a. Eq a => a -> a -> Bool
== String
"()" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$
             Name -> BindName
mkBindName Name
n { nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
y }

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

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

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


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

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

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

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

instance Reify NamedClause where
  type ReifiesTo NamedClause = A.Clause

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

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

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

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

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

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

instance Reify Sort where
    type ReifiesTo Sort = Expr

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

instance Reify Level where
  type ReifiesTo Level = Expr

  reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Level -> m (ReifiesTo Level)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
  reify :: forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
l   = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasBuiltins m => m Bool
haveLevels (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l) 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 <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
".#Lacking_Level_Builtins#" :: String)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
name

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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