{-# OPTIONS_GHC -Wunused-imports #-}

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

import Control.Monad.Except
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.TypeChecking.Warnings (warning)

import Agda.Syntax.Common.Pretty (prettyShow, render)

import Agda.Utils.Impossible

-- | Add display pragma if well-formed.
--   Otherwise, throw 'InvalidDisplayForm' warning and ignore it.
--
checkDisplayPragma :: QName -> [NamedArg A.Pattern] -> A.Expr -> TCM ()
checkDisplayPragma :: QName -> [NamedArg Pattern] -> Expr -> TCM ()
checkDisplayPragma QName
f [NamedArg Pattern]
ps Expr
e = do
  res <- TCMT IO (Either String DisplayForm)
-> TCMT IO (Either String DisplayForm)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO (Either String DisplayForm)
 -> TCMT IO (Either String DisplayForm))
-> TCMT IO (Either String DisplayForm)
-> TCMT IO (Either String DisplayForm)
forall a b. (a -> b) -> a -> b
$ ExceptT String TCM DisplayForm
-> TCMT IO (Either String DisplayForm)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT do
    QName
-> (Elims -> Elims)
-> [NamedArg Pattern]
-> (Nat -> Elims -> ExceptT String TCM DisplayForm)
-> ExceptT String TCM DisplayForm
forall b a.
QName
-> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
pappToTerm QName
f Elims -> Elims
forall a. a -> a
id [NamedArg Pattern]
ps \Nat
n Elims
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
args
      Nat -> Elims -> DisplayTerm -> DisplayForm
Display Nat
n Elims
lhs (DisplayTerm -> DisplayForm)
-> (Term -> DisplayTerm) -> Term -> DisplayForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> DisplayTerm
DTerm (Term -> DisplayForm)
-> ExceptT String TCM Term -> ExceptT String TCM DisplayForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ExceptT String TCM Term
exprToTerm Expr
e
  case res of
    Left String
reason -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> Warning
InvalidDisplayForm QName
f String
reason
    Right DisplayForm
df -> do
      String -> Nat -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"tc.display.pragma" Nat
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"Adding display form for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
f
      String -> Nat -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"tc.display.pragma" Nat
90 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
": \n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DisplayForm -> String
forall a. Show a => a -> String
show DisplayForm
df
      QName -> DisplayForm -> TCM ()
addDisplayForm QName
f DisplayForm
df

-- | The monad to check display forms.
--   The 'String' contains the reason to reject the display form.
--
type M = ExceptT String TCM

-- | Helper data type to record whether a pattern on the LHS contributed
-- a 'Proj' elimination or an 'Apply' elimination.
data ProjOrApp = IsProj QName | IsApp Term

patternsToTerms :: Telescope -> [NamedArg A.Pattern] -> (Int -> Elims -> M a) -> M a
patternsToTerms :: forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
patternsToTerms Telescope
_ [] Nat -> Elims -> M a
ret = Nat -> Elims -> M a
ret Nat
0 []
patternsToTerms Telescope
EmptyTel (NamedArg Pattern
p : [NamedArg Pattern]
ps) Nat -> Elims -> M a
ret =
  Pattern -> (Nat -> ProjOrApp -> M a) -> M a
forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) \Nat
n ProjOrApp
v ->
  Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
patternsToTerms Telescope
forall a. Tele a
EmptyTel [NamedArg Pattern]
ps \Nat
m Elims
vs -> Nat -> Elims -> M a
ret (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m) (NamedArg Pattern -> ProjOrApp -> Elim
forall a. LensHiding a => a -> ProjOrApp -> Elim
inheritHiding NamedArg Pattern
p ProjOrApp
v Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
vs)
patternsToTerms (ExtendTel Dom Type
a Abs Telescope
tel) (NamedArg Pattern
p : [NamedArg Pattern]
ps) Nat -> Elims -> M a
ret
  | 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 -> ProjOrApp -> M a) -> M a
forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
patternToTerm (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) \Nat
n ProjOrApp
v ->
      Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
patternsToTerms (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) [NamedArg Pattern]
ps \Nat
m Elims
vs -> Nat -> Elims -> M a
ret (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m) (NamedArg Pattern -> ProjOrApp -> Elim
forall a. LensHiding a => a -> ProjOrApp -> Elim
inheritHiding NamedArg Pattern
p ProjOrApp
v Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
vs)
  | Bool
otherwise =
      M a -> M a
forall a. M a -> M a
bindWild (M a -> M a) -> M a -> M a
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M 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
n Elims
vs ->
      Nat -> Elims -> M a
ret (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n) (Dom Type -> ProjOrApp -> Elim
forall a. LensHiding a => a -> ProjOrApp -> Elim
inheritHiding Dom Type
a (Term -> ProjOrApp
IsApp (Nat -> Elims -> Term
Var Nat
0 [])) Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
vs)

inheritHiding :: LensHiding a => a -> ProjOrApp -> Elim
inheritHiding :: forall a. LensHiding a => a -> ProjOrApp -> Elim
inheritHiding a
a (IsProj QName
q) = ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
q
inheritHiding a
a (IsApp Term
t) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding (a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding a
a) (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
t))

pappToTerm :: QName -> (Elims -> b) -> [NamedArg A.Pattern] -> (Int -> b -> M a) -> M a
pappToTerm :: forall b a.
QName
-> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
pappToTerm QName
x Elims -> b
f [NamedArg Pattern]
ps Nat -> b -> M a
ret = do
  def <- QName -> ExceptT String TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  TelV tel _ <- telView $ defType def
  let 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 (String, t)]
telToList
      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

  patternsToTerms (dropTel pars tel) ps $ \ Nat
n Elims
vs -> Nat -> b -> M a
ret Nat
n (Elims -> b
f Elims
vs)

patternToTerm :: A.Pattern -> (Nat -> ProjOrApp -> M a) -> M a
patternToTerm :: forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
patternToTerm Pattern
p Nat -> ProjOrApp -> M a
ret =
  case Pattern
p of
    A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}   -> Name -> M a -> M a
forall a. Name -> M a -> M a
bindVar Name
x (M a -> M a) -> M a -> M a
forall a b. (a -> b) -> a -> b
$ Nat -> ProjOrApp -> M a
ret Nat
1 (Term -> ProjOrApp
IsApp (Nat -> Elims -> Term
Var Nat
0 []))
    A.ConP ConPatInfo
_ AmbiguousQName
cs [NamedArg Pattern]
ps
      | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
cs -> QName
-> (Elims -> Term)
-> [NamedArg Pattern]
-> (Nat -> Term -> M a)
-> M a
forall b a.
QName
-> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
pappToTerm QName
c (ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
forall p. DataOrRecord' p
IsData Induction
Inductive []) ConInfo
ConOCon) [NamedArg Pattern]
ps \Nat
n Term
t -> Nat -> ProjOrApp -> M a
ret Nat
n (Term -> ProjOrApp
IsApp Term
t)
      | Bool
otherwise                   -> String -> AmbiguousQName -> M a
ambigErr String
"constructor" AmbiguousQName
cs
    A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
ds
      | Just QName
d <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ds -> Nat -> ProjOrApp -> M a
ret Nat
0 (ProjOrApp -> M a) -> ProjOrApp -> M a
forall a b. (a -> b) -> a -> b
$ QName -> ProjOrApp
IsProj QName
d
      | Bool
otherwise                   -> String -> AmbiguousQName -> M a
ambigErr String
"projection" AmbiguousQName
ds
    A.DefP PatInfo
_ AmbiguousQName
fs [NamedArg Pattern]
ps
      | Just QName
f <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
fs -> QName
-> (Elims -> Term)
-> [NamedArg Pattern]
-> (Nat -> Term -> M a)
-> M a
forall b a.
QName
-> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
pappToTerm QName
f (QName -> Elims -> Term
Def QName
f) [NamedArg Pattern]
ps \Nat
n Term
t -> Nat -> ProjOrApp -> M a
ret Nat
n (Term -> ProjOrApp
IsApp Term
t)
      | Bool
otherwise                   -> String -> AmbiguousQName -> M a
ambigErr String
"DefP" AmbiguousQName
fs
    A.LitP PatInfo
_ Literal
l                      -> Nat -> ProjOrApp -> M a
ret Nat
0 (ProjOrApp -> M a) -> ProjOrApp -> M a
forall a b. (a -> b) -> a -> b
$ Term -> ProjOrApp
IsApp (Term -> ProjOrApp) -> Term -> ProjOrApp
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    A.WildP PatInfo
_                       -> M a -> M a
forall a. M a -> M a
bindWild (M a -> M a) -> M a -> M a
forall a b. (a -> b) -> a -> b
$ Nat -> ProjOrApp -> M a
ret Nat
1 (ProjOrApp -> M a) -> ProjOrApp -> M a
forall a b. (a -> b) -> a -> b
$ Term -> ProjOrApp
IsApp (Nat -> Elims -> Term
Var Nat
0 [])
    A.AsP{}                         -> String -> M a
failP String
"an @-pattern"
    A.DotP{}                        -> String -> M a
failP String
"a dot pattern"
    A.AbsurdP{}                     -> String -> M a
failP String
"an absurd pattern"
    A.PatternSynP{}                 -> M a
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.RecP{}                        -> String -> M a
failP String
"a record pattern"
    A.EqualP{}                      -> String -> M a
failP String
"a system pattern"
    A.WithP{}                       -> M a
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    fail :: String -> ExceptT String TCM a
fail = String -> ExceptT String TCM a
forall a. String -> ExceptT String TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String TCM a)
-> (String -> String) -> String -> ExceptT String TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"its left-hand side contains " String -> String -> String
forall a. [a] -> [a] -> [a]
++)
    failP :: String -> M a
failP String
s = String -> M a
forall a. String -> ExceptT String TCM a
fail (String -> M a) -> (Doc -> String) -> Doc -> M a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Doc a -> String
render (Doc -> M a) -> ExceptT String TCM Doc -> M a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pattern -> ExceptT String TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
    ambigErr :: String -> AmbiguousQName -> M a
ambigErr String
thing (AmbQ List1 QName
xs) =
      String -> M a
forall a. String -> ExceptT String TCM a
fail (String -> M a) -> (Doc -> String) -> Doc -> M a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Doc a -> String
render (Doc -> M a) -> ExceptT String TCM Doc -> M a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        String -> ExceptT String TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
"an ambiguous " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thing String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") ExceptT String TCM Doc
-> ExceptT String TCM Doc -> ExceptT String TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
          [ExceptT String TCM Doc] -> ExceptT String TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (ExceptT String TCM Doc
-> NonEmpty (ExceptT String TCM Doc) -> [ExceptT String TCM Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate ExceptT String TCM Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((QName -> ExceptT String TCM Doc)
-> List1 QName -> NonEmpty (ExceptT String TCM Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> ExceptT String TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty List1 QName
xs))

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

bindVar :: Name -> M a -> M a
bindVar :: forall a. Name -> M a -> M a
bindVar Name
x M a
ret = Name -> M a -> M 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 M a
ret

exprToTerm :: A.Expr -> M Term
exprToTerm :: Expr -> ExceptT String 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)
-> ExceptT String TCM (Term, Dom Type) -> ExceptT String TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> ExceptT String TCM (Term, Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
    A.Def' QName
f Suffix
NoSuffix-> Term -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f []
    A.Def'{}         -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"suffix"
    A.Con AmbiguousQName
c          -> Term -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String 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
forall p. DataOrRecord' p
IsData Induction
Inductive []) ConInfo
ConOCon [] -- Don't care too much about ambiguity here
    A.Lit ExprInfo
_ Literal
l        -> Term -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String TCM Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    A.App AppInfo
_ Expr
e NamedArg Expr
arg    -> Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Term -> Elims -> Term)
-> ExceptT String TCM Term -> ExceptT String TCM (Elims -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ExceptT String TCM Term
exprToTerm Expr
e ExceptT String TCM (Elims -> Term)
-> ExceptT String TCM Elims -> ExceptT String TCM Term
forall a b.
ExceptT String TCM (a -> b)
-> ExceptT String TCM a -> ExceptT String TCM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Elim -> Elims -> Elims
forall a. a -> [a] -> [a]
:[]) (Elim -> Elims) -> (Term -> Elim) -> Term -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> ProjOrApp -> Elim
forall a. LensHiding a => a -> ProjOrApp -> Elim
inheritHiding NamedArg Expr
arg (ProjOrApp -> Elim) -> (Term -> ProjOrApp) -> Term -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ProjOrApp
IsApp (Term -> Elims)
-> ExceptT String TCM Term -> ExceptT String TCM Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ExceptT String TCM Term
exprToTerm (NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
arg))

    A.Proj ProjOrigin
_ AmbiguousQName
f       -> Term -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String 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 -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
f) []
    A.Macro QName
f        -> Term -> ExceptT String TCM Term
forall a. a -> ExceptT String TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ExceptT String TCM Term)
-> Term -> ExceptT String TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f []

    A.WithApp{}      -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"with application"
    A.QuestionMark{} -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"hole"
    A.Underscore{}   -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"metavariable"
    A.Dot{}          -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"dotted expression"
    A.Lam{}          -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"lambda"
    A.AbsurdLam{}    -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"lambda"
    A.ExtendedLam{}  -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"lambda"
    A.Fun{}          -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"function type"
    A.Pi{}           -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"function type"
    A.Generalized{}  -> ExceptT String TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Let{}          -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"let"
    A.Rec{}          -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"record"
    A.RecUpdate{}    -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"record update"
    A.ScopedExpr{}   -> ExceptT String TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.Quote{}        -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"quotation"
    A.QuoteTerm{}    -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"quotation"
    A.Unquote{}      -> String -> ExceptT String TCM Term
forall a. String -> ExceptT String TCM a
fail String
"unquote"
    A.DontCare{}     -> ExceptT String TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    fail :: String -> ExceptT String TCM a
fail = String -> ExceptT String TCM a
forall a. String -> ExceptT String TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String TCM a)
-> (String -> String) -> String -> ExceptT String TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"its right-hand side contains a " String -> String -> String
forall a. [a] -> [a] -> [a]
++)

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 i <- State Nat Nat
forall s (m :: * -> *). MonadState s m => m s
get; i <$ put (i - 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