module Agda.TypeChecking.Rules.Display (checkDisplayPragma) where

import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Internal as I
import Agda.Syntax.Common

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty

import Agda.Utils.Impossible

checkDisplayPragma :: QName -> [NamedArg A.Pattern] -> A.Expr -> TCM ()
checkDisplayPragma :: QName -> [NamedArg Pattern] -> Expr -> TCM ()
checkDisplayPragma QName
f [NamedArg Pattern]
ps Expr
e = do
  DisplayForm
df <- TCMT IO DisplayForm -> TCMT IO DisplayForm
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO DisplayForm -> TCMT IO DisplayForm)
-> TCMT IO DisplayForm -> TCMT IO DisplayForm
forall a b. (a -> b) -> a -> b
$ do
          QName
-> (Args -> Args)
-> [NamedArg Pattern]
-> (Int -> Args -> TCMT IO DisplayForm)
-> TCMT IO DisplayForm
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Int -> b -> TCM a)
-> TCM a
pappToTerm QName
f Args -> Args
forall a. a -> a
id [NamedArg Pattern]
ps ((Int -> Args -> TCMT IO DisplayForm) -> TCMT IO DisplayForm)
-> (Int -> Args -> TCMT IO DisplayForm) -> TCMT IO DisplayForm
forall a b. (a -> b) -> a -> b
$ \Int
n Args
args -> do
            let lhs :: [Elim' Term]
lhs = (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Args
args
            Term
v <- Expr -> TCM Term
exprToTerm Expr
e
            DisplayForm -> TCMT IO DisplayForm
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForm -> TCMT IO DisplayForm)
-> DisplayForm -> TCMT IO DisplayForm
forall a b. (a -> b) -> a -> b
$ Int -> [Elim' Term] -> DisplayTerm -> DisplayForm
Display Int
n [Elim' Term]
lhs (Term -> DisplayTerm
DTerm Term
v)
  VerboseKey -> Int -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.display.pragma" Int
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Adding display form for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Show a => a -> VerboseKey
show QName
f VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ DisplayForm -> VerboseKey
forall a. Show a => a -> VerboseKey
show DisplayForm
df
  QName -> DisplayForm -> TCM ()
addDisplayForm QName
f DisplayForm
df

--UNUSED Liang-Ting 2019-07-16
---- Compute a left-hand side for a display form. Inserts implicits, but no type
---- checking so does the wrong thing if implicitness is computed. Binds variables.
--displayLHS :: Telescope -> [NamedArg A.Pattern] -> (Int -> [Term] -> TCM a) -> TCM a
--displayLHS tel ps ret = patternsToTerms tel ps $ \n vs -> ret n (map unArg vs)

patternsToTerms :: Telescope -> [NamedArg A.Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms :: Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms Telescope
_ [] Int -> Args -> TCM a
ret = Int -> Args -> TCM a
ret Int
0 []
patternsToTerms Telescope
EmptyTel (NamedArg Pattern
p : [NamedArg Pattern]
ps) Int -> Args -> TCM a
ret =
  Pattern -> (Int -> Term -> TCM a) -> TCM a
forall a. Pattern -> (Int -> Term -> TCM a) -> TCM a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) ((Int -> Term -> TCM a) -> TCM a)
-> (Int -> Term -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
n Term
v ->
  Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms Telescope
forall a. Tele a
EmptyTel [NamedArg Pattern]
ps     ((Int -> Args -> TCM a) -> TCM a)
-> (Int -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
m Args
vs -> Int -> Args -> TCM a
ret (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (NamedArg Pattern -> Term -> Arg Term
forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Pattern
p Term
v Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
: Args
vs)
patternsToTerms (ExtendTel Dom Type
a Abs Telescope
tel) (NamedArg Pattern
p : [NamedArg Pattern]
ps) Int -> Args -> TCM a
ret
  -- Andreas, 2019-07-22, while #3353: we should use domName, not absName !!
  -- WAS: -- | sameHiding p a, visible p || maybe True (absName tel ==) (bareNameOf p) =  -- no ArgName or same as p
  | Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern -> Dom Type -> Maybe Bool
forall arg dom.
(LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom,
 LensHiding dom) =>
arg -> dom -> Maybe Bool
fittingNamedArg NamedArg Pattern
p Dom Type
a =
      Pattern -> (Int -> Term -> TCM a) -> TCM a
forall a. Pattern -> (Int -> Term -> TCM a) -> TCM a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) ((Int -> Term -> TCM a) -> TCM a)
-> (Int -> Term -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
n Term
v ->
      Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) [NamedArg Pattern]
ps  ((Int -> Args -> TCM a) -> TCM a)
-> (Int -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
m Args
vs -> Int -> Args -> TCM a
ret (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (NamedArg Pattern -> Term -> Arg Term
forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Pattern
p Term
v Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
: Args
vs)
  | Bool
otherwise =
      TCM a -> TCM a
forall a. TCM a -> TCM a
bindWild (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) (NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps) ((Int -> Args -> TCM a) -> TCM a)
-> (Int -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
n Args
vs ->
      Int -> Args -> TCM a
ret (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (Dom Type -> Term -> Arg Term
forall a b. LensHiding a => a -> b -> Arg b
inheritHiding Dom Type
a (Int -> [Elim' Term] -> Term
Var Int
0 []) Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
: Args
vs)

inheritHiding :: LensHiding a => a -> b -> Arg b
inheritHiding :: a -> b -> Arg b
inheritHiding a
a b
b = Hiding -> Arg b -> Arg b
forall a. LensHiding a => Hiding -> a -> a
setHiding (a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding a
a) (b -> Arg b
forall a. a -> Arg a
defaultArg b
b)

pappToTerm :: QName -> (Args -> b) -> [NamedArg A.Pattern] -> (Int -> b -> TCM a) -> TCM a
pappToTerm :: QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Int -> b -> TCM a)
-> TCM a
pappToTerm QName
x Args -> b
f [NamedArg Pattern]
ps Int -> b -> TCM a
ret = do
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  TelV Telescope
tel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  let dropTel :: Int -> Telescope -> Telescope
dropTel Int
n = ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> (Telescope -> ListTel) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop Int
n (ListTel -> ListTel)
-> (Telescope -> ListTel) -> Telescope -> ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList
      pars :: Int
pars =
        case Definition -> Defn
theDef Definition
def of
          Constructor { conPars :: Defn -> Int
conPars = Int
p } -> Int
p
          Function { funProjection :: Defn -> Maybe Projection
funProjection = Just Projection{projIndex :: Projection -> Int
projIndex = Int
i} }
            | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
          Defn
_ -> Int
0

  Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms (Int -> Telescope -> Telescope
dropTel Int
pars Telescope
tel) [NamedArg Pattern]
ps ((Int -> Args -> TCM a) -> TCM a)
-> (Int -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Int
n Args
vs -> Int -> b -> TCM a
ret Int
n (Args -> b
f Args
vs)

patternToTerm :: A.Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm :: Pattern -> (Int -> Term -> TCM a) -> TCM a
patternToTerm Pattern
p Int -> Term -> TCM a
ret =
  case Pattern
p of
    A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}   -> Name -> TCM a -> TCM a
forall a. Name -> TCM a -> TCM a
bindVar Name
x (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Int -> Term -> TCM a
ret Int
1 (Int -> [Elim' Term] -> Term
Var Int
0 [])
    A.ConP ConPatInfo
_ AmbiguousQName
cs [NamedArg Pattern]
ps
      | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
cs -> QName
-> (Args -> Term)
-> [NamedArg Pattern]
-> (Int -> Term -> TCM a)
-> TCM a
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Int -> b -> TCM a)
-> TCM a
pappToTerm QName
c (ConHead -> ConInfo -> [Elim' Term] -> Term
Con (QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
c Induction
Inductive []) ConInfo
ConOCon ([Elim' Term] -> Term) -> (Args -> [Elim' Term]) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Int -> Term -> TCM a
ret
      | Bool
otherwise                   -> VerboseKey -> AmbiguousQName -> TCM a
forall (m :: * -> *) b.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
VerboseKey -> AmbiguousQName -> m b
ambigErr VerboseKey
"constructor" AmbiguousQName
cs
    A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
ds
      | Just QName
d <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ds -> Int -> Term -> TCM a
ret Int
0 (QName -> [Elim' Term] -> Term
Def QName
d [])
      | Bool
otherwise                   -> VerboseKey -> AmbiguousQName -> TCM a
forall (m :: * -> *) b.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
VerboseKey -> AmbiguousQName -> m b
ambigErr VerboseKey
"projection" AmbiguousQName
ds
    A.DefP PatInfo
_ AmbiguousQName
fs [NamedArg Pattern]
ps
      | Just QName
f <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
fs -> QName
-> (Args -> Term)
-> [NamedArg Pattern]
-> (Int -> Term -> TCM a)
-> TCM a
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Int -> b -> TCM a)
-> TCM a
pappToTerm QName
f (QName -> [Elim' Term] -> Term
Def QName
f ([Elim' Term] -> Term) -> (Args -> [Elim' Term]) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Int -> Term -> TCM a
ret
      | Bool
otherwise                   -> VerboseKey -> AmbiguousQName -> TCM a
forall (m :: * -> *) b.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
VerboseKey -> AmbiguousQName -> m b
ambigErr VerboseKey
"DefP" AmbiguousQName
fs
    A.LitP Literal
l                        -> Int -> Term -> TCM a
ret Int
0 (Literal -> Term
Lit Literal
l)
    A.WildP PatInfo
_                       -> TCM a -> TCM a
forall a. TCM a -> TCM a
bindWild (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Int -> Term -> TCM a
ret Int
1 (Int -> [Elim' Term] -> Term
Var Int
0 [])
    Pattern
_                               -> do
      Doc
doc <- Pattern -> TCMT IO Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
      TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Pattern not allowed in DISPLAY pragma:\n" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Doc -> VerboseKey
forall a. Show a => a -> VerboseKey
show Doc
doc
  where
    ambigErr :: VerboseKey -> AmbiguousQName -> m b
ambigErr VerboseKey
thing (AmbQ NonEmpty QName
xs) =
      Doc -> m b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> m b) -> m Doc -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey
"Ambiguous " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
thing VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
          [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Monad m => m Doc
comma ((QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow ([QName] -> [m Doc]) -> [QName] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
xs))

bindWild :: TCM a -> TCM a
bindWild :: TCM a -> TCM a
bindWild TCM a
ret = do
  Name
x <- TCMT IO Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_
  Name -> TCM a -> TCM a
forall a. Name -> TCM a -> TCM a
bindVar Name
x TCM a
ret

bindVar :: Name -> TCM a -> TCM a
bindVar :: Name -> TCM a -> TCM a
bindVar Name
x TCM a
ret = Name -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Name
x TCM a
ret

exprToTerm :: A.Expr -> TCM Term
exprToTerm :: Expr -> TCM Term
exprToTerm Expr
e =
  case Expr -> Expr
unScope Expr
e of
    A.Var Name
x  -> (Term, Dom Type) -> Term
forall a b. (a, b) -> a
fst ((Term, Dom Type) -> Term) -> TCMT IO (Term, Dom Type) -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TCMT IO (Term, Dom Type)
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
    A.Def QName
f  -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def QName
f []
    A.Con AmbiguousQName
c  -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim' Term] -> Term
Con (QName -> Induction -> [Arg QName] -> ConHead
ConHead (AmbiguousQName -> QName
headAmbQ AmbiguousQName
c) Induction
Inductive []) ConInfo
ConOCon [] -- Don't care too much about ambiguity here
    A.Lit Literal
l  -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    A.App AppInfo
_ Expr
e NamedArg Expr
arg  -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply (Term -> Args -> Term) -> TCM Term -> TCMT IO (Args -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Term
exprToTerm Expr
e TCMT IO (Args -> Term) -> TCMT IO Args -> TCM Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
:[]) (Arg Term -> Args) -> (Term -> Arg Term) -> Term -> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Term -> Arg Term
forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Expr
arg (Term -> Args) -> TCM Term -> TCMT IO Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Term
exprToTerm (NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
arg))

    A.Proj ProjOrigin
_ AmbiguousQName
f -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
f) []   -- only for printing so we don't have to worry too much here
    A.PatternSyn AmbiguousQName
f -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
f) []
    A.Macro QName
f      -> Term -> TCM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def QName
f []

    A.WithApp{}      -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"with application"
    A.QuestionMark{} -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"holes"
    A.Underscore{}   -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"metavariables"
    A.Lam{}          -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"lambdas"
    A.AbsurdLam{}    -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"lambdas"
    A.ExtendedLam{}  -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
notAllowed VerboseKey
"lambdas"
    Expr
_                -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"TODO: exprToTerm " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Expr -> VerboseKey
forall a. Show a => a -> VerboseKey
show Expr
e
  where
    notAllowed :: VerboseKey -> m a
notAllowed VerboseKey
s = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Not allowed in DISPLAY pragma right-hand side: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
s