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

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

    TODO

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

import Prelude hiding (mapM_, mapM, null)

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

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

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

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

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible


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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Reify DisplayTerm Expr where
  reifyWhen :: Bool -> DisplayTerm -> m Expr
reifyWhen = Bool -> DisplayTerm -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
  reify :: DisplayTerm -> m Expr
reify d :: DisplayTerm
d = case DisplayTerm
d of
    DTerm v :: Term
v -> Bool -> Term -> m Expr
forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
False Term
v
    DDot  v :: Term
v -> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
    DCon c :: ConHead
c ci :: ConInfo
ci vs :: [Arg DisplayTerm]
vs -> Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c))) ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Arg DisplayTerm] -> m [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify [Arg DisplayTerm]
vs
    DDef f :: QName
f es :: [Elim' DisplayTerm]
es -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
f) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Elim' DisplayTerm] -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify [Elim' DisplayTerm]
es
    DWithApp u :: DisplayTerm
u us :: [DisplayTerm]
us es0 :: Elims
es0 -> do
      (e :: Expr
e, es :: [Expr]
es) <- (DisplayTerm, [DisplayTerm]) -> m (Expr, [Expr])
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (DisplayTerm
u, [DisplayTerm]
us)
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (if [Expr] -> Bool
forall a. Null a => a -> Bool
null [Expr]
es then Expr
e else ExprInfo -> Expr -> [Expr] -> Expr
A.WithApp ExprInfo
noExprInfo Expr
e [Expr]
es) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
es0

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

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

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

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

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

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

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

    okElim :: Elim' I.Term -> Bool
    okElim :: Elim' Term -> Bool
okElim (I.IApply x :: Term
x y :: Term
y r :: Term
r) = Term -> Bool
okTerm Term
r
    okElim (I.Apply a :: 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 _ []) = Bool
True
    okTerm (I.Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs) = (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
    okTerm (I.Def x :: QName
x []) = QName -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Bool) -> QName -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> QName
qnameToConcrete QName
x -- Handling wildcards in display forms
    okTerm _            = 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 d :: DisplayTerm
d ds1 :: [DisplayTerm]
ds1 es2 :: Elims
es2) =
      let (f :: QName
f, es :: [Elim' DisplayTerm]
es, ds0 :: [Elim' DisplayTerm]
ds0) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith DisplayTerm
d
      in  (QName
f, [Elim' DisplayTerm]
es, [Elim' DisplayTerm]
ds0 [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ (DisplayTerm -> Elim' DisplayTerm)
-> [DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (DisplayTerm -> Arg DisplayTerm)
-> DisplayTerm
-> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayTerm -> Arg DisplayTerm
forall a. a -> Arg a
defaultArg) [DisplayTerm]
ds1 [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es2)
    flattenWith (DDef f :: QName
f es :: [Elim' DisplayTerm]
es) = (QName
f, [Elim' DisplayTerm]
es, [])     -- .^ hacky, but we should only hit this when printing debug info
    flattenWith (DTerm (I.Def f :: QName
f es :: Elims
es)) = (QName
f, (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es, [])
    flattenWith _ = (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

reifyTerm :: MonadReify m => Bool -> Term -> m Expr
reifyTerm :: Bool -> Term -> m Expr
reifyTerm expandAnonDefs0 :: Bool
expandAnonDefs0 v0 :: Term
v0 = do
  -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
  Bool
metasBare <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
  Term
v <- Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v0 m Term -> (Term -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    I.MetaV x :: MetaId
x _ | Bool
metasBare -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x []
    v :: Term
v -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
  -- (i.e. when we don't care about nice printing)
  Bool
expandAnonDefs <- Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
expandAnonDefs0 m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` m Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled
  -- Andreas, 2016-07-21 if --postfix-projections
  -- then we print system-generated projections as postfix, else prefix.
  Bool
havePfp <- PragmaOptions -> Bool
optPostfixProjections (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let pred :: ProjOrigin -> Bool
pred = if Bool
havePfp then (ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPrefix) else (ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPostfix)
  case (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
pred Term
v of
    -- Hack to print generalized field projections with nicer names. Should
    -- only show up in errors. Check the spined form!
    _ | I.Var n :: Nat
n (I.Proj _ p :: QName
p : es :: Elims
es) <- Term
v,
        Just name :: String
name <- QName -> Maybe String
getGeneralizedFieldName QName
p -> do
      let fakeName :: Name
fakeName = (QName -> Name
qnameName QName
p) { nameConcrete :: Name
nameConcrete = Range -> NameInScope -> [NamePart] -> Name
C.Name Range
forall a. Range' a
noRange NameInScope
C.InScope [String -> NamePart
C.Id String
name] } -- TODO: infix names!?
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
fakeName) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
es
    I.Var n :: Nat
n es :: Elims
es   -> do
        Name
x  <- m Name -> m (Maybe Name) -> m Name
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String -> m Name) -> String -> m Name
forall a b. (a -> b) -> a -> b
$ "@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show Nat
n) (m (Maybe Name) -> m Name) -> m (Maybe Name) -> m Name
forall a b. (a -> b) -> a -> b
$ Nat -> m (Maybe Name)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Maybe Name)
nameOfBV' Nat
n
        Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
x) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
es
    I.Def x :: QName
x es :: Elims
es   -> do
      String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.def" 100 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reifying def " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
      (x :: QName
x,es :: Elims
es) <- QName -> Elims -> m (QName, Elims)
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x Elims
es
      QName -> Elims -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
es (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
Bool -> QName -> Elims -> m Expr
reifyDef Bool
expandAnonDefs QName
x Elims
es
    I.Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs -> do
      let x :: QName
x = ConHead -> QName
conName ConHead
c
      Bool
isR <- QName -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
isGeneratedRecordConstructor QName
x
      case Bool
isR Bool -> Bool -> Bool
|| ConInfo
ci ConInfo -> ConInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec of
        True -> do
          Bool
showImp <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
          let keep :: (Dom Name, Expr) -> Bool
keep (a :: Dom Name
a, v :: Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| Dom Name -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Name
a
          QName
r  <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
x
          [Dom Name]
xs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
forall a. a -> Maybe a -> a
fromMaybe [Dom Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
-> m (Maybe [Dom Name]) -> m [Dom Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe [Dom Name])
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom Name])
getRecordFieldNames_ QName
r
          [Expr]
vs <- (Arg Expr -> Expr) -> [Arg Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Arg Expr -> Expr
forall e. Arg e -> e
unArg ([Arg Expr] -> [Expr]) -> m [Arg Expr] -> m [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args -> m [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
vs)
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
noExprInfo (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ ((Dom Name, Expr) -> Either (FieldAssignment' Expr) ModuleName)
-> [(Dom Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map (FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left (FieldAssignment' Expr
 -> Either (FieldAssignment' Expr) ModuleName)
-> ((Dom Name, Expr) -> FieldAssignment' Expr)
-> (Dom Name, Expr)
-> Either (FieldAssignment' Expr) ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Expr -> FieldAssignment' Expr)
-> (Name, Expr) -> FieldAssignment' Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment ((Name, Expr) -> FieldAssignment' Expr)
-> ((Dom Name, Expr) -> (Name, Expr))
-> (Dom Name, Expr)
-> FieldAssignment' Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Name -> Name) -> (Dom Name, Expr) -> (Name, Expr)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Dom Name -> Name
forall t e. Dom' t e -> e
unDom) ([(Dom Name, Expr)] -> RecordAssigns)
-> [(Dom Name, Expr)] -> RecordAssigns
forall a b. (a -> b) -> a -> b
$ ((Dom Name, Expr) -> Bool)
-> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Dom Name, Expr) -> Bool
keep ([(Dom Name, Expr)] -> [(Dom Name, Expr)])
-> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
forall a b. (a -> b) -> a -> b
$ [Dom Name] -> [Expr] -> [(Dom Name, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Dom Name]
xs [Expr]
vs
        False -> QName -> Elims -> m Expr -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
vs (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ do
          Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
          let Constructor{conPars :: Defn -> Nat
conPars = Nat
np} = Definition -> Defn
theDef Definition
def
          -- if we are the the module that defines constructor x
          -- then we have to drop at least the n module parameters
          Nat
n  <- QName -> m Nat
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
          -- the number of parameters is greater (if the data decl has
          -- extra parameters) or equal (if not) to n
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
np) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          let h :: Expr
h = AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
x)
          if Elims -> Bool
forall a. Null a => a -> Bool
null Elims
vs then Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
h else do
            [Arg Expr]
es <- Args -> m [Arg Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify ((Elim' Term -> Arg Term) -> Elims -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term)
-> (Elim' Term -> Maybe (Arg Term)) -> Elim' Term -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim) Elims
vs)
            -- Andreas, 2012-04-20: do not reify parameter arguments of constructor
            -- if the first regular constructor argument is hidden
            -- we turn it into a named argument, in order to avoid confusion
            -- with the parameter arguments which can be supplied in abstract syntax
            --
            -- Andreas, 2012-09-17: this does not remove all sources of confusion,
            -- since parameters could have the same name as regular arguments
            -- (see for example the parameter {i} to Data.Star.Star, which is also
            -- the first argument to the cons).
            -- @data Star {i}{I : Set i} ... where cons : {i :  I} ...@
            if Nat
np Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es else do
              -- Get name of first argument from type of constructor.
              -- Here, we need the reducing version of @telView@
              -- because target of constructor could be a definition
              -- expanding into a function type.  See test/succeed/NameFirstIfHidden.agda.
              TelV tel :: Tele (Dom Type)
tel _ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Definition -> Type
defType Definition
def)
              let (pars :: [Dom (String, Type)]
pars, rest :: [Dom (String, Type)]
rest) = Nat
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
np ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel
              case [Dom (String, Type)]
rest of
                -- Andreas, 2012-09-18
                -- If the first regular constructor argument is hidden,
                -- we keep the parameters to avoid confusion.
                (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : _) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
                  let us :: [Arg Expr]
us = [Dom (String, Type)]
-> (Dom (String, Type) -> Arg Expr) -> [Arg Expr]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. Nat -> [a] -> [a]
drop Nat
n [Dom (String, Type)]
pars) ((Dom (String, Type) -> Arg Expr) -> [Arg Expr])
-> (Dom (String, Type) -> Arg Expr) -> [Arg Expr]
forall a b. (a -> b) -> a -> b
$ \ (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}) ->
                             -- setRelevance Relevant $
                             Arg Expr -> Arg Expr
forall a. LensHiding a => a -> a
hideOrKeepInstance (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Expr
forall a. Underscore a => a
underscore
                  Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h ([Arg Expr] -> m Expr) -> [Arg Expr] -> m Expr
forall a b. (a -> b) -> a -> b
$ [Arg Expr]
us [Arg Expr] -> [Arg Expr] -> [Arg Expr]
forall a. [a] -> [a] -> [a]
++ [Arg Expr]
es  -- Note: unless --show-implicit, @apps@ will drop @us@.
                -- otherwise, we drop all parameters
                _ -> Expr -> [Arg Expr] -> m Expr
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es

--    I.Lam info b | isAbsurdBody b -> return $ A. AbsurdLam noExprInfo $ getHiding info
    I.Lam info :: ArgInfo
info b :: Abs Term
b    -> do
      (x :: Name
x,e :: Expr
e) <- Abs Term -> m (Name, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Abs Term
b
      Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x) Expr
e
      -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
    I.Lit l :: Literal
l        -> Literal -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Literal
l
    I.Level l :: Level
l      -> Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Level
l
    I.Pi a :: Dom Type
a b :: Abs Type
b       -> case Abs Type
b of
        NoAbs _ b' :: Type
b'
          | Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Type
a   -> (Arg Expr -> Expr -> Expr) -> (Arg Expr, Expr) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun (ExprInfo -> Arg Expr -> Expr -> Expr)
-> ExprInfo -> Arg Expr -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo
noExprInfo) ((Arg Expr, Expr) -> Expr) -> m (Arg Expr, Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom Type, Type) -> m (Arg Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Dom Type
a, Type
b')
            -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
            -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
            -- and (b) the name of the binder might matter.
            -- See issue 951 (a) and 952 (b).
          | Bool
otherwise   -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Dom Type -> m (Arg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Dom Type
a
        b :: Abs Type
b               -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          m Bool -> m (Arg Expr) -> m (Arg Expr) -> m (Arg Expr)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Dom Type -> Type -> m Bool
forall (m :: * -> *) a t.
(MonadTCEnv m, Free a, Free t) =>
t -> a -> m Bool
domainFree Dom Type
a (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b))
            {- then -} (Arg Expr -> m (Arg Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m (Arg Expr)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) Expr
forall a. Underscore a => a
underscore)
            {- else -} (Dom Type -> m (Arg Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Dom Type
a)
      where
        mkPi :: Abs Type -> Arg Expr -> m Expr
mkPi b :: Abs Type
b (Arg info :: ArgInfo
info a' :: Expr
a') = do
          Maybe Expr
tac <- (Term -> m Expr) -> Maybe Term -> m (Maybe Expr)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Maybe Term -> m (Maybe Expr)) -> Maybe Term -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a
          (x :: Name
x, b :: Expr
b) <- Abs Type -> m (Name, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Abs Type
b
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope -> Expr -> Expr
A.Pi ExprInfo
noExprInfo [Range -> Maybe Expr -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
forall a. Range' a
noRange Maybe Expr
tac [ArgInfo -> Named NamedName Binder -> NamedArg Binder
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named NamedName Binder -> NamedArg Binder)
-> Named NamedName Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Binder -> Named NamedName Binder
forall name a. Maybe name -> a -> Named name a
Named (Dom Type -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
domName Dom Type
a) (Binder -> Named NamedName Binder)
-> Binder -> Named NamedName Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x] Expr
a'] Expr
b
        -- We can omit the domain type if it doesn't have any free variables
        -- and it's mentioned in the target type.
        domainFree :: t -> a -> m Bool
domainFree a :: t
a b :: a
b = do
          Bool
df <- (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintDomainFreePi
          Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
df, Nat -> a -> Bool
forall a. Free a => Nat -> a -> Bool
freeIn 0 a
b, t -> Bool
forall t. Free t => t -> Bool
closed t
a]

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

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

          MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
          (msub1 :: Maybe (Substitution' Term)
msub1,meta_tel :: Tele (Dom Type)
meta_tel,msub2 :: Maybe (Substitution' Term)
msub2) <- do
            CheckpointId
local_chkpt <- Lens' CheckpointId TCEnv -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
            (chkpt :: CheckpointId
chkpt, tel :: Tele (Dom Type)
tel, msub2 :: Maybe (Substitution' Term)
msub2) <- MetaVariable
-> (Range
    -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range
  -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
 -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> (Range
    -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall a b. (a -> b) -> a -> b
$ \ _ ->
                               (,,) (CheckpointId
 -> Tele (Dom Type)
 -> Maybe (Substitution' Term)
 -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m CheckpointId
-> m (Tele (Dom Type)
      -> Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' CheckpointId TCEnv -> m CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
                                    m (Tele (Dom Type)
   -> Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Tele (Dom Type))
-> m (Maybe (Substitution' Term)
      -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
                                    m (Maybe (Substitution' Term)
   -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Lens' (Maybe (Substitution' Term)) TCEnv
-> m (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints ((Map CheckpointId (Substitution' Term)
  -> f (Map CheckpointId (Substitution' Term)))
 -> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> Map CheckpointId (Substitution' Term)
    -> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
local_chkpt)
            (,,) (Maybe (Substitution' Term)
 -> Tele (Dom Type)
 -> Maybe (Substitution' Term)
 -> (Maybe (Substitution' Term), Tele (Dom Type),
     Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Tele (Dom Type)
      -> Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Tele (Dom Type),
          Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Maybe (Substitution' Term)) TCEnv
-> m (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC ((Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints ((Map CheckpointId (Substitution' Term)
  -> f (Map CheckpointId (Substitution' Term)))
 -> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> Map CheckpointId (Substitution' Term)
    -> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
chkpt) m (Tele (Dom Type)
   -> Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Tele (Dom Type),
       Maybe (Substitution' Term)))
-> m (Tele (Dom Type))
-> m (Maybe (Substitution' Term)
      -> (Maybe (Substitution' Term), Tele (Dom Type),
          Maybe (Substitution' Term)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tele (Dom Type) -> m (Tele (Dom Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele (Dom Type)
tel m (Maybe (Substitution' Term)
   -> (Maybe (Substitution' Term), Tele (Dom Type),
       Maybe (Substitution' Term)))
-> m (Maybe (Substitution' Term))
-> m (Maybe (Substitution' Term), Tele (Dom Type),
      Maybe (Substitution' Term))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Substitution' Term) -> m (Maybe (Substitution' Term))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Substitution' Term)
msub2
          let
              addNames :: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames []    es :: [Elim' a]
es = (Elim' a -> Elim' (Named name a))
-> [Elim' a] -> [Elim' (Named name a)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Named name a) -> Elim' a -> Elim' (Named name a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Named name a
forall a name. a -> Named name a
unnamed) [Elim' a]
es
              addNames _     [] = []
              addNames xs :: [name]
xs     (I.Proj{} : _) = [Elim' (Named name a)]
forall a. HasCallStack => a
__IMPOSSIBLE__
              addNames xs :: [name]
xs     (I.IApply x :: a
x y :: a
y r :: a
r : es :: [Elim' a]
es) =
                -- Needs to be I.Apply so it can have an Origin field.
                [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs (Arg a -> Elim' a
forall a. Arg a -> Elim' a
I.Apply (a -> Arg a
forall a. a -> Arg a
defaultArg a
r) Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
: [Elim' a]
es)
              addNames (x :: name
x:xs :: [name]
xs) (I.Apply arg :: Arg a
arg : es :: [Elim' a]
es) =
                Arg (Named name a) -> Elim' (Named name a)
forall a. Arg a -> Elim' a
I.Apply (Maybe name -> a -> Named name a
forall name a. Maybe name -> a -> Named name a
Named (name -> Maybe name
forall a. a -> Maybe a
Just name
x) (a -> Named name a) -> Arg a -> Arg (Named name a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Origin -> Arg a -> Arg a
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Substitution Arg a
arg)) Elim' (Named name a)
-> [Elim' (Named name a)] -> [Elim' (Named name a)]
forall a. a -> [a] -> [a]
: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs [Elim' a]
es

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

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

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

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

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

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

    reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr
    reifyDef' :: QName -> Elims -> m Expr
reifyDef' x :: QName
x es :: Elims
es = do
      String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.def" 60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reifying call to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
      -- We should drop this many arguments from the local context.
      Nat
n <- QName -> m Nat
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
      String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.def" 70 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "freeVars for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show Nat
n
      -- If the definition is not (yet) in the signature,
      -- we just do the obvious.
      let fallback :: SigError -> m Expr
fallback _ = Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
x) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)
      m (Either SigError Definition)
-> (SigError -> m Expr) -> (Definition -> m Expr) -> m Expr
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (QName -> m (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x) SigError -> m Expr
fallback ((Definition -> m Expr) -> m Expr)
-> (Definition -> m Expr) -> m Expr
forall a b. (a -> b) -> a -> b
$ \ defn :: 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 = [cl :: Clause
cl] }
                | QName -> Bool
isAbsurdLambdaName QName
x -> do
                  -- get hiding info from last pattern, which should be ()
                  let h :: Hiding
h = NamedArg DeBruijnPattern -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (NamedArg DeBruijnPattern -> Hiding)
-> NamedArg DeBruijnPattern -> Hiding
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a. [a] -> a
last ([NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                      n :: Nat
n = [NamedArg DeBruijnPattern] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- 1  -- drop all args before the absurd one
                      absLam :: Expr
absLam = ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
h
                  if | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Elims -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es -> do -- We don't have all arguments before the absurd one!
                        let name :: DeBruijnPattern -> String
name (I.VarP _ x :: DBPatVar
x) = String -> String
patVarNameToString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ DBPatVar -> String
dbPatVarName DBPatVar
x
                            name _            = String
forall a. HasCallStack => a
__IMPOSSIBLE__  -- only variables before absurd pattern
                            vars :: [(ArgInfo, String)]
vars = (NamedArg DeBruijnPattern -> (ArgInfo, String))
-> [NamedArg DeBruijnPattern] -> [(ArgInfo, String)]
forall a b. (a -> b) -> [a] -> [b]
map (NamedArg DeBruijnPattern -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (NamedArg DeBruijnPattern -> ArgInfo)
-> (NamedArg DeBruijnPattern -> String)
-> NamedArg DeBruijnPattern
-> (ArgInfo, String)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DeBruijnPattern -> String
name (DeBruijnPattern -> String)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) ([NamedArg DeBruijnPattern] -> [(ArgInfo, String)])
-> [NamedArg DeBruijnPattern] -> [(ArgInfo, String)]
forall a b. (a -> b) -> a -> b
$ Nat -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Nat -> [a] -> [a]
drop (Elims -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es) ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a]
init ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
                            lam :: (ArgInfo, a) -> m (Expr -> Expr)
lam (i :: ArgInfo
i, s :: a
s) = do
                              Name
x <- a -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ a
s
                              (Expr -> Expr) -> m (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr -> Expr) -> m (Expr -> Expr))
-> (Expr -> Expr) -> m (Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
A.mkDomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
i (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x)
                        ((Expr -> Expr) -> Expr -> Expr) -> Expr -> [Expr -> Expr] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
($) Expr
absLam ([Expr -> Expr] -> Expr) -> m [Expr -> Expr] -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ArgInfo, String) -> m (Expr -> Expr))
-> [(ArgInfo, String)] -> m [Expr -> Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ArgInfo, String) -> m (Expr -> Expr)
forall (m :: * -> *) a.
(FreshName a, MonadFresh NameId m) =>
(ArgInfo, a) -> m (Expr -> Expr)
lam [(ArgInfo, String)]
vars
                      | Bool
otherwise -> Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
absLam ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Nat -> Elims -> Elims
forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)

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

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

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

        -- #3004: give up if we have to print a pattern lambda inside its own body!
        [QName]
alreadyPrinting <- Lens' [QName] TCEnv -> m [QName]
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' [QName] TCEnv
ePrintingPatternLambdas

        Maybe (Nat, Maybe System)
extLam <- case Defn
def of
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just{}, funProjection :: Defn -> Maybe Projection
funProjection = Just{} } -> m (Maybe (Nat, Maybe System))
forall a. HasCallStack => a
__IMPOSSIBLE__
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo m :: ModuleName
m sys :: Maybe System
sys) } ->
            (Nat, Maybe System) -> Maybe (Nat, Maybe System)
forall a. a -> Maybe a
Just ((Nat, Maybe System) -> Maybe (Nat, Maybe System))
-> (Tele (Dom Type) -> (Nat, Maybe System))
-> Tele (Dom Type)
-> Maybe (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Maybe System -> Maybe System
forall a. Maybe a -> Maybe a
Strict.toLazy Maybe System
sys) (Nat -> (Nat, Maybe System))
-> (Tele (Dom Type) -> Nat)
-> Tele (Dom Type)
-> (Nat, Maybe System)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Maybe (Nat, Maybe System))
-> m (Tele (Dom Type)) -> m (Maybe (Nat, Maybe System))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
          _ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Nat, Maybe System)
forall a. Maybe a
Nothing
        case Maybe (Nat, Maybe System)
extLam of
          Just (pars :: Nat
pars, sys :: Maybe System
sys) | Bool
df, QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem QName
x [QName]
alreadyPrinting ->
            Lens' [QName] TCEnv -> ([QName] -> [QName]) -> m Expr -> m Expr
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' [QName] TCEnv
ePrintingPatternLambdas (QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:) (m Expr -> m Expr) -> m Expr -> m Expr
forall a b. (a -> b) -> a -> b
$
            QName -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
forall (m :: * -> *).
MonadReify m =>
QName -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x Nat
pars Maybe System
sys (Definition -> [Clause]
defClauses Definition
defn) Elims
es

        -- Otherwise (ordinary function call):
          _ -> do
           (pad :: [NamedArg Expr]
pad, [Elim' (Named NamedName Term)]
nes :: [Elim' (Named_ Term)]) <- case Defn
def of

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

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

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

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

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

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

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

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

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

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

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

           String -> Nat -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS "reify.def" 70
             [ "  pad = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr] -> String
forall a. Show a => a -> String
show [NamedArg Expr]
pad
             , "  nes = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Elim' (Named NamedName Term)] -> String
forall a. Show a => a -> String
show [Elim' (Named NamedName Term)]
nes
             ]
           let hd0 :: Expr
hd0 | Defn -> Bool
isProperProjection Defn
def = ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> NonEmpty QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty QName
forall el coll. Singleton el coll => el -> coll
singleton QName
x
                   | Bool
otherwise = QName -> Expr
A.Def QName
x
           let hd :: Expr
hd = (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_) Expr
hd0 [NamedArg Expr]
pad
           Expr -> [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
hd ([Elim' (Named_ Expr)] -> m Expr)
-> m [Elim' (Named_ Expr)] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Elim' (Named NamedName Term)] -> m [Elim' (Named_ Expr)]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify [Elim' (Named NamedName Term)]
nes

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

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

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

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

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

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

      -- Since we applying the clauses to the parameters,
      -- we do not need to drop their initial "parameter" patterns
      -- (this is taken care of by @apply@).
      [Clause]
cls <- Maybe System -> m [Clause] -> (System -> m [Clause]) -> m [Clause]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
               ((Clause -> m Clause) -> [Clause] -> m [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (NamedClause -> m Clause
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (NamedClause -> m Clause)
-> (Clause -> NamedClause) -> Clause -> m Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
x Bool
False (Clause -> NamedClause)
-> (Clause -> Clause) -> Clause -> NamedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cls)
               (QNamed System -> m [Clause]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (QNamed System -> m [Clause])
-> (System -> QNamed System) -> System -> m [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> System -> QNamed System
forall a. QName -> a -> QNamed a
QNamed QName
x (System -> QNamed System)
-> (System -> System) -> System -> QNamed System
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (System -> Args -> System
forall t. Apply t => t -> Args -> t
`apply` Args
pars))
      let cx :: Name
cx    = Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          dInfo :: DefInfo' Expr
dInfo = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cx Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
x)
      Expr -> [Elim' Expr] -> m Expr
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (ExprInfo -> DefInfo' Expr -> QName -> [Clause] -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo QName
x [Clause]
cls) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> m [Elim' Expr]
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Elims
rest

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

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

-- | Skip reification of implicit and irrelevant args if option is off.
instance (Reify i a) => Reify (Arg i) (Arg a) where
  reify :: Arg i -> m (Arg a)
reify (Arg info :: ArgInfo
info i :: i
i) = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a) -> m a -> m (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Bool -> i -> m a) -> i -> Bool -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> i -> m a
forall i a (m :: * -> *).
(Reify i a, MonadReify m) =>
Bool -> i -> m a
reifyWhen i
i (Bool -> m a) -> m Bool -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Bool
condition)
    where condition :: m Bool
condition = (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> Hiding
argInfoHiding ArgInfo
info Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
/= Hiding
Hidden) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments)
              m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
showIrrelevantArguments)
  reifyWhen :: Bool -> Arg i -> m (Arg a)
reifyWhen b :: Bool
b i :: Arg i
i = (i -> m a) -> Arg i -> m (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Bool -> i -> m a
forall i a (m :: * -> *).
(Reify i a, MonadReify m) =>
Bool -> i -> m a
reifyWhen Bool
b) Arg i
i

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

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

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

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

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

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


-- | Removes implicit arguments that are not needed, that is, that don't bind
--   any variables that are actually used and doesn't do pattern matching.
--   Doesn't strip any arguments that were written explicitly by the user.
stripImplicits :: MonadReify m => A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits :: Patterns -> Patterns -> m Patterns
stripImplicits params :: Patterns
params ps :: Patterns
ps = do
  -- if --show-implicit we don't need the names
  m Bool -> m Patterns -> m Patterns -> m Patterns
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (Patterns -> m Patterns
forall (m :: * -> *) a. Monad m => a -> m a
return (Patterns -> m Patterns) -> Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
-> Patterns -> Patterns
forall a b. (a -> b) -> [a] -> [b]
map ((Named_ Pattern -> Named_ Pattern)
-> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ Pattern -> Named_ Pattern
forall n a. (LensNamed n a, LensOrigin n) => a -> a
removeNameUnlessUserWritten) Patterns
ps) (m Patterns -> m Patterns) -> m Patterns -> m Patterns
forall a b. (a -> b) -> a -> b
$ do
    String -> Nat -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS "reify.implicit" 30
      [ "stripping implicits"
      , "  ps   = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show Patterns
ps
      ]
    let ps' :: Patterns
ps' = Patterns -> Patterns
blankDots (Patterns -> Patterns) -> Patterns -> Patterns
forall a b. (a -> b) -> a -> b
$ Patterns -> Patterns
forall e. [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip Patterns
ps
    String -> Nat -> [String] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS "reify.implicit" 30
      [ "  ps'  = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Patterns -> String
forall a. Show a => a -> String
show Patterns
ps'
      ]
    Patterns -> m Patterns
forall (m :: * -> *) a. Monad m => a -> m a
return Patterns
ps'
    where
      -- Replace variables in dot patterns by an underscore _ if they are hidden
      -- in the pattern. This is slightly nicer than making the implicts explicit.
      blankDots :: Patterns -> Patterns
blankDots ps :: Patterns
ps = Set Name -> Patterns -> Patterns
forall a. BlankVars a => Set Name -> a -> a
blank (Patterns -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn (Patterns -> Set Name) -> Patterns -> Set Name
forall a b. (a -> b) -> a -> b
$ Patterns
params Patterns -> Patterns -> Patterns
forall a. [a] -> [a] -> [a]
++ Patterns
ps) Patterns
ps

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance BlankVars TypedBinding where
  blank :: Set Name -> TypedBinding -> TypedBinding
blank bound :: Set Name
bound (TBind r :: Range
r t :: Maybe Expr
t n :: [NamedArg Binder]
n e :: Expr
e) = Range -> Maybe Expr -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
r Maybe Expr
t [NamedArg Binder]
n (Expr -> TypedBinding) -> Expr -> TypedBinding
forall a b. (a -> b) -> a -> b
$ Set Name -> Expr -> Expr
forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
  blank bound :: Set Name
bound (TLet _ _)    = TypedBinding
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Since the internal syntax has no let bindings left


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

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

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

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

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

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

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

instance Binder A.LamBinding where
  varsBoundIn :: LamBinding -> Set Name
varsBoundIn (A.DomainFree _ x :: NamedArg Binder
x) = NamedArg Binder -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn NamedArg Binder
x
  varsBoundIn (A.DomainFull b :: TypedBinding
b)   = TypedBinding -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn TypedBinding
b

instance Binder TypedBinding where
  varsBoundIn :: TypedBinding -> Set Name
varsBoundIn (TBind _ _ xs :: [NamedArg Binder]
xs _) = [NamedArg Binder] -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn [NamedArg Binder]
xs
  varsBoundIn (TLet _ bs :: [LetBinding]
bs)      = [LetBinding] -> Set Name
forall a. Binder a => a -> Set Name
varsBoundIn [LetBinding]
bs

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

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

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

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


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

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

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

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

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

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

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


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

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

instance Reify NamedClause A.Clause where
  reify :: NamedClause -> m Clause
reify (NamedClause f :: QName
f toDrop :: Bool
toDrop cl :: Clause
cl) = Tele (Dom Type) -> m Clause -> m Clause
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Tele (Dom Type)
clauseTel Clause
cl) (m Clause -> m Clause) -> m Clause -> m Clause
forall a b. (a -> b) -> a -> b
$ do
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.clause" 60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reifying NamedClause"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n  f      = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
f
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n  toDrop = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
toDrop
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n  cl     = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clause -> String
forall a. Show a => a -> String
show Clause
cl
    let ell :: ExpandedEllipsis
ell = Clause -> ExpandedEllipsis
clauseEllipsis Clause
cl
    Patterns
ps  <- [NamedArg DeBruijnPattern] -> m Patterns
forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns ([NamedArg DeBruijnPattern] -> m Patterns)
-> [NamedArg DeBruijnPattern] -> m Patterns
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
    SpineLHS
lhs <- (QName -> Patterns -> SpineLHS) -> (QName, Patterns) -> SpineLHS
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS (LHSInfo -> QName -> Patterns -> SpineLHS)
-> LHSInfo -> QName -> Patterns -> SpineLHS
forall a b. (a -> b) -> a -> b
$ LHSInfo
forall a. Null a => a
empty { lhsEllipsis :: ExpandedEllipsis
lhsEllipsis = ExpandedEllipsis
ell }) ((QName, Patterns) -> SpineLHS)
-> m (QName, Patterns) -> m SpineLHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Patterns -> Patterns -> m (QName, Patterns)
forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps []
    -- Unless @toDrop@ we have already dropped the module patterns from the clauses
    -- (e.g. for extended lambdas). We still get here with toDrop = True and
    -- pattern lambdas when doing make-case, so take care to drop the right
    -- number of parameters.
    (params :: Patterns
params , lhs :: SpineLHS
lhs) <- if Bool -> Bool
not Bool
toDrop then (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ([] , SpineLHS
lhs) else do
      Nat
nfv <- QName -> m (Either SigError ModuleName)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ModuleName)
getDefModule QName
f m (Either SigError ModuleName)
-> (Either SigError ModuleName -> m Nat) -> m Nat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left _  -> Nat -> m Nat
forall (m :: * -> *) a. Monad m => a -> m a
return 0
        Right m :: ModuleName
m -> Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size (Tele (Dom Type) -> Nat) -> m (Tele (Dom Type)) -> m Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
      (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Patterns, SpineLHS) -> m (Patterns, SpineLHS))
-> (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
forall a b. (a -> b) -> a -> b
$ Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams Nat
nfv SpineLHS
lhs
    SpineLHS
lhs <- Patterns -> SpineLHS -> m SpineLHS
forall (m :: * -> *).
MonadReify m =>
Patterns -> SpineLHS -> m SpineLHS
stripImps Patterns
params SpineLHS
lhs
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.clause" 60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reifying NamedClause, lhs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpineLHS -> String
forall a. Show a => a -> String
show SpineLHS
lhs
    RHS
rhs <- Maybe Term -> m RHS -> (Term -> m RHS) -> m RHS
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Clause -> Maybe Term
clauseBody Clause
cl) (RHS -> m RHS
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
AbsurdRHS) ((Term -> m RHS) -> m RHS) -> (Term -> m RHS) -> m RHS
forall a b. (a -> b) -> a -> b
$ \ e :: Term
e ->
      Expr -> Maybe Expr -> RHS
RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Expr -> m (Maybe Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
forall a. Maybe a
Nothing
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.clause" 60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reifying NamedClause, rhs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RHS -> String
forall a. Show a => a -> String
show RHS
rhs
    let result :: Clause
result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (SpineLHS -> LHS
forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls (Clause -> Bool
I.clauseCatchall Clause
cl)
    String -> Nat -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn "reify.clause" 60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "reified NamedClause, result = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clause -> String
forall a. Show a => a -> String
show Clause
result
    Clause -> m Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
result
    where
      splitParams :: Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams n :: Nat
n (SpineLHS i :: LHSInfo
i f :: QName
f ps :: Patterns
ps) =
        let (params :: Patterns
params , pats :: Patterns
pats) = Nat -> Patterns -> (Patterns, Patterns)
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Patterns
ps
        in  (Patterns
params , LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f Patterns
pats)
      stripImps :: MonadReify m => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
      stripImps :: Patterns -> SpineLHS -> m SpineLHS
stripImps params :: Patterns
params (SpineLHS i :: LHSInfo
i f :: QName
f ps :: Patterns
ps) =  LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f (Patterns -> SpineLHS) -> m Patterns -> m SpineLHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Patterns -> Patterns -> m Patterns
forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits Patterns
params Patterns
ps

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

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

instance Reify Type Expr where
    reifyWhen :: Bool -> Type -> m Expr
reifyWhen = Bool -> Type -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
    reify :: Type -> m Expr
reify (I.El _ t :: Term
t) = Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
t

instance Reify Sort Expr where
    reifyWhen :: Bool -> Sort -> m Expr
reifyWhen = Bool -> Sort -> m Expr
forall i (m :: * -> *).
(Reify i Expr, MonadReify m) =>
Bool -> i -> m Expr
reifyWhenE
    reify :: Sort -> m Expr
reify s :: Sort
s = do
      Sort
s <- Sort -> m Sort
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort
s
      case Sort
s of
        I.Type (I.ClosedLevel n :: Integer
n) -> Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Integer -> Expr
A.Set ExprInfo
noExprInfo Integer
n
        I.Type a :: Level
a -> do
          Expr
a <- Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Level
a
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Integer -> Expr
A.Set ExprInfo
noExprInfo 0) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        I.Prop (I.ClosedLevel n :: Integer
n) -> Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Integer -> Expr
A.Prop ExprInfo
noExprInfo Integer
n
        I.Prop a :: Level
a -> do
          Expr
a <- Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Level
a
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Integer -> Expr
A.Prop ExprInfo
noExprInfo 0) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
a)
        I.Inf       -> do
          I.Def inf :: QName
inf [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSetOmega
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
inf
        I.SizeUniv  -> do
          I.Def sizeU :: QName
sizeU [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSizeUniv
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
sizeU
        I.PiSort a :: Dom Type
a s :: Abs Sort
s -> do
          Name
pis <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ("piSort" :: String) -- TODO: hack
          (e1 :: Expr
e1,e2 :: Expr
e2) <- (Sort, Term) -> m (Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a, ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ (Sort -> Term) -> Abs Sort -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort Abs Sort
s)
          let app :: Expr -> Expr -> Expr
app x :: Expr
x y :: Expr
y = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
y)
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
pis Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
        I.FunSort s1 :: Sort
s1 s2 :: Sort
s2 -> do
          Name
funs <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ("funSort" :: String) -- TODO: hack
          (e1 :: Expr
e1,e2 :: Expr
e2) <- (Sort, Sort) -> m (Expr, Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Sort
s1 , Sort
s2)
          let app :: Expr -> Expr -> Expr
app x :: Expr
x y :: Expr
y = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
y)
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
funs Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
        I.UnivSort s :: Sort
s -> do
          Name
univs <- String -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ("univSort" :: String) -- TODO: hack
          Expr
e <- Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Sort
s
          Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (Name -> Expr
A.Var Name
univs) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg Expr
e
        I.MetaS x :: MetaId
x es :: Elims
es -> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> Term -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x Elims
es
        I.DefS d :: QName
d es :: Elims
es -> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> Term -> m Expr
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
d Elims
es
        I.DummyS s :: String
s -> Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ Literal -> Expr
A.Lit (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> String -> Literal
LitString Range
forall a. Range' a
noRange String
s

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

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

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

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

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

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

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

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

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

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

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