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 <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
          forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
f forall a. a -> a
id [NamedArg Pattern]
ps 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 forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
I.Apply Args
args
            Term
v <- Expr -> TCM Term
exprToTerm Expr
e
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Nat -> Elims -> DisplayTerm -> DisplayForm
Display Nat
n Elims
lhs (Term -> DisplayTerm
DTerm Term
v)
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.display.pragma" Nat
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Adding display form for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ [Char]
"\n  " forall a. [a] -> [a] -> [a]
++ 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 =
  forall a. Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm (forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) forall a b. (a -> b) -> a -> b
$ \Nat
n Term
v ->
  forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms forall a. Tele a
EmptyTel [NamedArg Pattern]
ps     forall a b. (a -> b) -> a -> b
$ \Nat
m Args
vs -> Nat -> Args -> TCM a
ret (Nat
n forall a. Num a => a -> a -> a
+ Nat
m) (forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Pattern
p Term
v 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
  | forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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 =
      forall a. Pattern -> (Nat -> Term -> TCM a) -> TCM a
patternToTerm (forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) forall a b. (a -> b) -> a -> b
$ \Nat
n Term
v ->
      forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms (forall a. Abs a -> a
unAbs Abs Telescope
tel) [NamedArg Pattern]
ps  forall a b. (a -> b) -> a -> b
$ \Nat
m Args
vs -> Nat -> Args -> TCM a
ret (Nat
n forall a. Num a => a -> a -> a
+ Nat
m) (forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Pattern
p Term
v forall a. a -> [a] -> [a]
: Args
vs)
  | Bool
otherwise =
      forall a. TCM a -> TCM a
bindWild forall a b. (a -> b) -> a -> b
$ forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms (forall a. Abs a -> a
unAbs Abs Telescope
tel) (NamedArg Pattern
p forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps) forall a b. (a -> b) -> a -> b
$ \Nat
n Args
vs ->
      Nat -> Args -> TCM a
ret (Nat
1 forall a. Num a => a -> a -> a
+ Nat
n) (forall a b. LensHiding a => a -> b -> Arg b
inheritHiding Dom Type
a (Nat -> Elims -> Term
Var Nat
0 []) 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 = forall a. LensHiding a => Hiding -> a -> a
setHiding (forall a. LensHiding a => a -> Hiding
getHiding a
a) (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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  TelV Telescope
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  let dropTel :: Nat -> Telescope -> Telescope
dropTel Nat
n = ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Nat -> [a] -> [a]
drop Nat
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Nat
0 -> Nat
i forall a. Num a => a -> a -> a
- Nat
1
          Defn
_ -> Nat
0

  forall a.
Telescope -> [NamedArg Pattern] -> (Nat -> Args -> TCM a) -> TCM a
patternsToTerms (Nat -> Telescope -> Telescope
dropTel Nat
pars Telescope
tel) [NamedArg Pattern]
ps 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}   -> forall a. Name -> TCM a -> TCM a
bindVar Name
x 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 -> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Nat -> Term -> TCM a
ret
      | Bool
otherwise                   -> 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                   -> 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 -> forall b a.
QName
-> (Args -> b)
-> [NamedArg Pattern]
-> (Nat -> b -> TCM a)
-> TCM a
pappToTerm QName
f (QName -> Elims -> Term
Def QName
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply) [NamedArg Pattern]
ps Nat -> Term -> TCM a
ret
      | Bool
otherwise                   -> 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 forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    A.WildP PatInfo
_                       -> forall a. TCM a -> TCM a
bindWild forall a b. (a -> b) -> a -> b
$ Nat -> Term -> TCM a
ret Nat
1 (Nat -> Elims -> Term
Var Nat
0 [])
    Pattern
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Pattern not allowed in DISPLAY pragma:", 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) =
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Ambiguous " forall a. [a] -> [a] -> [a]
++ [Char]
thing forall a. [a] -> [a] -> [a]
++ [Char]
":") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 <- forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_
  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 = 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  -> forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
    A.Def QName
f  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f []
    A.Con AmbiguousQName
c  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    A.App AppInfo
_ Expr
e NamedArg Expr
arg  -> forall t. Apply t => t -> Args -> t
apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Term
exprToTerm Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. LensHiding a => a -> b -> Arg b
inheritHiding NamedArg Expr
arg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Term
exprToTerm (forall a. NamedArg a -> a
namedArg NamedArg Expr
arg))

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

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

renumberElims :: Nat -> Elims -> Elims
renumberElims :: Nat -> Elims -> Elims
renumberElims Nat
n Elims
es = 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 <- forall s (m :: * -> *). MonadState s m => m s
get; Nat
i forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall s (m :: * -> *). MonadState s m => s -> m ()
put (Nat
i forall a. Num a => a -> a -> a
- Nat
1)

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

    renumber :: Term -> State Nat Term
    renumber :: Term -> State Nat Term
renumber (Var Nat
0 [])   = Nat -> Term
var 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> State Nat Elims
renumbers Elims
es
    renumber (Lit Literal
l)      = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
    renumber Term
_            = forall a. HasCallStack => a
__IMPOSSIBLE__ -- We need only handle the result of patternToTerm here