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

import qualified Data.List.NonEmpty as NonEmpty
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]
-> (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
            -- 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 = Int -> Elims -> Elims
renumberElims (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
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 -> Elims -> DisplayTerm -> DisplayForm
Display Int
n Elims
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. Pretty a => a -> VerboseKey
prettyShow 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)

type ToTm = StateT Nat TCM

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 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 -> (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 -> Elims -> 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 -> Elims -> 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 -> 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' Term) -> Args -> Elims
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 -> Elims -> 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 -> Elims -> Term
Def QName
f (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
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 PatInfo
_ Literal
l                      -> Int -> Term -> TCM a
ret Int
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
$ Int -> Term -> TCM a
ret Int
1 (Int -> Elims -> Term
Var Int
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 :: VerboseKey -> AmbiguousQName -> m b
ambigErr VerboseKey
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
        VerboseKey -> m Doc
forall (m :: * -> *). Applicative 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 :: * -> *) (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 (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 :: 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 -> Elims -> 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 -> 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 (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 -> 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 (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 (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{}      -> 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.
(HasCallStack, MonadTCError 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.
(HasCallStack, MonadTCError 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

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

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

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