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

import Control.Monad.State
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.Pretty (prettyShow)

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]
-> (Nat -> Args -> TCMT IO DisplayForm)
-> TCMT IO DisplayForm
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
f Args -> Args
forall a. a -> a
id [NamedArg Pattern]
ps ((Nat -> Args -> TCMT IO DisplayForm) -> TCMT IO DisplayForm)
-> (Nat -> Args -> TCMT IO DisplayForm) -> TCMT IO DisplayForm
forall a b. (a -> b) -> a -> b
$ \ Nat
n Args
args -> do
            -- pappToTerm puts Var 0 for every variable. We get to know how many there were (n) so
            -- now we can renumber them with decreasing deBruijn indices.
            let lhs :: Elims
lhs = Nat -> Elims -> Elims
renumberElims (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply Args
args
            Term
v <- Expr -> TCM Term
exprToTerm Expr
e
            DisplayForm -> TCMT IO DisplayForm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForm -> TCMT IO DisplayForm)
-> DisplayForm -> TCMT IO DisplayForm
forall a b. (a -> b) -> a -> b
$ Nat -> Elims -> DisplayTerm -> DisplayForm
Display Nat
n Elims
lhs (Term -> DisplayTerm
DTerm Term
v)
  [Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.display.pragma" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Adding display form for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DisplayForm -> [Char]
forall a. Show a => a -> [Char]
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)

type ToTm = StateT Nat TCM

patternsToTerms :: Telescope -> [NamedArg A.Pattern] -> (Int -> Args -> TCM a) -> TCM a
patternsToTerms :: forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms Telescope
_ [] Nat -> Args -> TCM a
ret = Nat -> Args -> TCM a
ret Nat
0 []
patternsToTerms Telescope
EmptyTel (NamedArg Pattern
p : [NamedArg Pattern]
ps) Nat -> Args -> TCM a
ret =
  Pattern -> (Nat -> Term -> TCM a) -> TCM a
forall a. Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) ((Nat -> Term -> TCM a) -> TCM a)
-> (Nat -> Term -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Nat
n Term
v ->
  Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms Telescope
forall a. Tele a
EmptyTel [NamedArg Pattern]
ps     ((Nat -> Args -> TCM a) -> TCM a)
-> (Nat -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Nat
m Args
vs -> Nat -> Args -> TCM a
ret (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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) Nat -> 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 arg, NameOf arg ~ NamedName, LensHiding arg,
 LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) =>
arg -> dom -> Maybe Bool
fittingNamedArg NamedArg Pattern
p Dom Type
a =
      Pattern -> (Nat -> Term -> TCM a) -> TCM a
forall a. Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) ((Nat -> Term -> TCM a) -> TCM a)
-> (Nat -> Term -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Nat
n Term
v ->
      Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) [NamedArg Pattern]
ps  ((Nat -> Args -> TCM a) -> TCM a)
-> (Nat -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Nat
m Args
vs -> Nat -> Args -> TCM a
ret (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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] -> (Nat -> Args -> TCM a) -> TCM a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> 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) ((Nat -> Args -> TCM a) -> TCM a)
-> (Nat -> Args -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Nat
n Args
vs ->
      Nat -> Args -> TCM a
ret (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n) (Dom Type -> Term -> Arg Term
forall a b. LensHiding a => a -> b -> Arg b
inheritHiding Dom Type
a (Nat -> Elims -> Term
Var Nat
0 []) Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
: Args
vs)

inheritHiding :: LensHiding a => a -> b -> Arg b
inheritHiding :: forall a b. LensHiding a => 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 :: forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
x Args -> b
f [NamedArg Pattern]
ps Nat -> 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 :: Nat -> Telescope -> Telescope
dropTel Nat
n = ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> (Telescope -> ListTel) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> ListTel -> ListTel
forall a. Nat -> [a] -> [a]
drop Nat
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 ([Char], t)]
telToList
      pars :: Nat
pars =
        case Definition -> Defn
theDef Definition
def of
          Constructor { conPars :: Defn -> Nat
conPars = Nat
p } -> Nat
p
          Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{projIndex :: Projection -> Nat
projIndex = Nat
i} }
            | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 -> Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
          Defn
_ -> Nat
0

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

patternToTerm :: A.Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm :: forall a. Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm Pattern
p Nat -> 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
$ Nat -> Term -> TCM a
ret Nat
1 (Nat -> Elims -> Term
Var Nat
0 [])
    A.ConP ConPatInfo
_ AmbiguousQName
cs [NamedArg Pattern]
ps
      | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
cs -> QName
-> (Args -> Term)
-> [NamedArg Pattern]
-> (Nat -> Term -> TCM a)
-> TCM a
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
c (ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
IsData Induction
Inductive []) ConInfo
ConOCon (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Nat -> Term -> TCM a
ret
      | Bool
otherwise                   -> [Char] -> AmbiguousQName -> TCM a
forall {m :: * -> *} {b}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
[Char] -> AmbiguousQName -> m b
ambigErr [Char]
"constructor" AmbiguousQName
cs
    A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
ds
      | Just QName
d <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ds -> Nat -> Term -> TCM a
ret Nat
0 (QName -> Elims -> Term
Def QName
d [])
      | Bool
otherwise                   -> [Char] -> AmbiguousQName -> TCM a
forall {m :: * -> *} {b}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
[Char] -> AmbiguousQName -> m b
ambigErr [Char]
"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]
-> (Nat -> Term -> TCM a)
-> TCM a
forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
f (QName -> Elims -> Term
Def QName
f (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Nat -> Term -> TCM a
ret
      | Bool
otherwise                   -> [Char] -> AmbiguousQName -> TCM a
forall {m :: * -> *} {b}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 Semigroup (m Doc)) =>
[Char] -> AmbiguousQName -> m b
ambigErr [Char]
"DefP" AmbiguousQName
fs
    A.LitP PatInfo
_ Literal
l                      -> Nat -> Term -> TCM a
ret Nat
0 (Term -> TCM a) -> Term -> TCM a
forall a b. (a -> b) -> a -> b
$ 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
$ Nat -> Term -> TCM a
ret Nat
1 (Nat -> Elims -> Term
Var Nat
0 [])
    Pattern
_ -> Doc -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Pattern not allowed in DISPLAY pragma:", Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p ]
  where
    ambigErr :: [Char] -> AmbiguousQName -> m b
ambigErr [Char]
thing (AmbQ List1 QName
xs) =
      Doc -> m b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError 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
        [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Ambiguous " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
thing [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
          [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (m Doc -> NonEmpty (m Doc) -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((QName -> m Doc) -> List1 QName -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 QName
xs))

bindWild :: TCM a -> TCM a
bindWild :: forall a. 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 :: forall a. 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
forall (m :: * -> *) a. MonadAddContext m => Name -> 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 a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f []
    A.Con AmbiguousQName
c  -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead (AmbiguousQName -> QName
headAmbQ AmbiguousQName
c) DataOrRecord
IsData Induction
Inductive []) ConInfo
ConOCon [] -- Don't care too much about ambiguity here
    A.Lit ExprInfo
_ Literal
l  -> Term -> TCM Term
forall a. a -> TCMT IO a
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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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 a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> 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 a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
f) []
    A.Macro QName
f      -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f []

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

renumberElims :: Nat -> Elims -> Elims
renumberElims :: Nat -> Elims -> Elims
renumberElims Nat
n Elims
es = State Nat Elims -> Nat -> Elims
forall s a. State s a -> s -> a
evalState (Elims -> State Nat Elims
renumbers Elims
es) Nat
n
  where
    next :: State Nat Nat
    next :: State Nat Nat
next = do Nat
i <- State Nat Nat
forall s (m :: * -> *). MonadState s m => m s
get; Nat
i Nat -> StateT Nat Identity () -> State Nat Nat
forall a b. a -> StateT Nat Identity b -> StateT Nat Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Nat -> StateT Nat Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)

    renumbers :: Elims -> State Nat Elims
    renumbers :: Elims -> State Nat Elims
renumbers = ((Elim -> StateT Nat Identity Elim) -> Elims -> State Nat Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Elim -> StateT Nat Identity Elim) -> Elims -> State Nat Elims)
-> ((Term -> StateT Nat Identity Term)
    -> Elim -> StateT Nat Identity Elim)
-> (Term -> StateT Nat Identity Term)
-> Elims
-> State Nat Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> StateT Nat Identity Term)
-> Elim -> StateT Nat Identity Elim
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse) Term -> StateT Nat Identity Term
renumber

    renumber :: Term -> State Nat Term
    renumber :: Term -> StateT Nat Identity Term
renumber (Var Nat
0 [])   = Nat -> Term
var (Nat -> Term) -> State Nat Nat -> StateT Nat Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State Nat Nat
next
    renumber (Def QName
f Elims
es)   = QName -> Elims -> Term
Def QName
f (Elims -> Term) -> State Nat Elims -> StateT Nat Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> State Nat Elims
renumbers Elims
es
    renumber (Con ConHead
c ConInfo
h Elims
es) = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
h (Elims -> Term) -> State Nat Elims -> StateT Nat Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> State Nat Elims
renumbers Elims
es
    renumber (Lit Literal
l)      = Term -> StateT Nat Identity Term
forall a. a -> StateT Nat Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> StateT Nat Identity Term)
-> Term -> StateT Nat Identity Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    renumber Term
_            = StateT Nat Identity Term
forall a. HasCallStack => a
__IMPOSSIBLE__ -- We need only handle the result of patternToTerm here