-- | Translating Agda types to Haskell types. Used to ensure that imported
--   Haskell functions have the right type.

module Agda.Compiler.MAlonzo.HaskellTypes
  ( haskellType
  , checkConstructorCount
  , hsTelApproximation, hsTelApproximation'
  ) where

import Control.Monad         ( zipWithM )
import Control.Monad.Except  ( ExceptT(ExceptT), runExceptT, mapExceptT, catchError, throwError )
import Control.Monad.Trans   ( lift )
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)
import Data.Maybe (fromMaybe)
import Data.List (intercalate)

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Telescope

import Agda.Compiler.MAlonzo.Pragmas
import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.MAlonzo.Pretty () --instance only

import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)

import Agda.Utils.Impossible

hsQCon :: String -> String -> HS.Type
hsQCon :: [Char] -> [Char] -> Type
hsQCon [Char]
m [Char]
f = QName -> Type
HS.TyCon forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
HS.Qual ([Char] -> ModuleName
HS.ModuleName [Char]
m) ([Char] -> Name
HS.Ident [Char]
f)

hsCon :: String -> HS.Type
hsCon :: [Char] -> Type
hsCon = QName -> Type
HS.TyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
HS.Ident

hsUnit :: HS.Type
hsUnit :: Type
hsUnit = [Char] -> Type
hsCon [Char]
"()"

hsVar :: HS.Name -> HS.Type
hsVar :: Name -> Type
hsVar = Name -> Type
HS.TyVar

hsApp :: HS.Type -> [HS.Type] -> HS.Type
hsApp :: Type -> [Type] -> Type
hsApp Type
d [Type]
ds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
HS.TyApp Type
d [Type]
ds

hsForall :: HS.Name -> HS.Type -> HS.Type
hsForall :: Name -> Type -> Type
hsForall Name
x = [TyVarBind] -> Type -> Type
HS.TyForall [Name -> TyVarBind
HS.UnkindedVar Name
x]

-- Issue #5207: From ghc-9.0 we have to be careful with nested foralls.
hsFun :: HS.Type -> HS.Type -> HS.Type
hsFun :: Type -> Type -> Type
hsFun Type
a (HS.TyForall [TyVarBind]
vs Type
b) = [TyVarBind] -> Type -> Type
HS.TyForall [TyVarBind]
vs forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
hsFun Type
a Type
b
hsFun Type
a Type
b = Type -> Type -> Type
HS.TyFun Type
a Type
b

data WhyNot = NoPragmaFor QName
            | WrongPragmaFor Range QName
            | BadLambda Term
            | BadMeta Term
            | BadDontCare Term
            | NotCompiled QName

type ToHs = ExceptT WhyNot HsCompileM

notAHaskellType :: Term -> WhyNot -> TCM a
notAHaskellType :: forall a. Term -> WhyNot -> TCM a
notAHaskellType Term
top WhyNot
offender = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The type" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
top] forall a. [a] -> [a] -> [a]
++
        forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot be translated to a corresponding Haskell type, because it contains" forall a. [a] -> [a] -> [a]
++
        forall {m :: * -> *}.
(Semigroup (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Null (m Doc)) =>
WhyNot -> [m Doc]
reason WhyNot
offender) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall {m :: * -> *}.
(Null (m Doc), IsString (m Doc), MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 Semigroup (m Doc)) =>
WhyNot -> m Doc
possibleFix WhyNot
offender
  where
    reason :: WhyNot -> [m Doc]
reason (BadLambda        Term
v) = forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"the lambda term" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadMeta          Term
v) = forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a meta variable" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadDontCare      Term
v) = forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"an erased term" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (NotCompiled      QName
x) = forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a name that is not compiled"
                                  forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x) forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (NoPragmaFor      QName
x) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which does not have a COMPILE pragma."
    reason (WrongPragmaFor Range
_ QName
x) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which has the wrong kind of COMPILE pragma."

    possibleFix :: WhyNot -> m Doc
possibleFix BadLambda{}     = forall a. Null a => a
empty
    possibleFix BadMeta{}       = forall a. Null a => a
empty
    possibleFix BadDontCare{}   = forall a. Null a => a
empty
    possibleFix NotCompiled{}   = forall a. Null a => a
empty
    possibleFix (NoPragmaFor QName
d) = forall {m :: * -> *}.
(IsString (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, Null (m Doc),
 Semigroup (m Doc)) =>
QName -> m Doc -> m Doc
suggestPragma QName
d forall a b. (a -> b) -> a -> b
$ m Doc
"add a pragma"
    possibleFix (WrongPragmaFor Range
r QName
d) = forall {m :: * -> *}.
(IsString (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, Null (m Doc),
 Semigroup (m Doc)) =>
QName -> m Doc -> m Doc
suggestPragma QName
d forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"replace the value-level pragma at", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Range
r, m Doc
"by" ]

    suggestPragma :: QName -> m Doc -> m Doc
suggestPragma QName
d m Doc
action = do
      Defn
def    <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      let dataPragma :: a -> (a, [Char])
dataPragma a
n = (a
"data type HsD", [Char]
"data HsD (" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" | " [ [Char]
"C" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i | a
i <- [a
1..a
n] ] forall a. [a] -> [a] -> [a]
++ [Char]
")")
          typePragma :: ([Char], [Char])
typePragma   = ([Char]
"type HsT", [Char]
"type HsT")
          ([Char]
hsThing, [Char]
pragma) =
            case Defn
def of
              Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> forall {a} {a}.
(IsString a, Num a, Enum a, Show a) =>
a -> (a, [Char])
dataPragma (forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs)
              Record{}                  -> forall {a} {a}.
(IsString a, Num a, Enum a, Show a) =>
a -> (a, [Char])
dataPragma Integer
1
              Defn
_                         -> ([Char], [Char])
typePragma
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [m Doc
"Possible fix:", m Doc
action]
           , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ m Doc
"{-# COMPILE GHC", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d, m Doc
"=", forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma, m Doc
"#-}" ]
           , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"for a suitable Haskell " forall a. [a] -> [a] -> [a]
++ [Char]
hsThing forall a. [a] -> [a] -> [a]
++ [Char]
".")
           ]

runToHs :: Term -> ToHs a -> HsCompileM a
runToHs :: forall a. Term -> ToHs a -> HsCompileM a
runToHs Term
top ToHs a
m = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Term -> WhyNot -> TCM a
notAHaskellType Term
top) forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ToHs a
m

liftE1' :: (forall b. (a -> m b) -> m b) -> (a -> ExceptT e m b) -> ExceptT e m b
liftE1' :: forall a (m :: * -> *) e b.
(forall b. (a -> m b) -> m b)
-> (a -> ExceptT e m b) -> ExceptT e m b
liftE1' forall b. (a -> m b) -> m b
f a -> ExceptT e m b
k = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (forall b. (a -> m b) -> m b
f (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ExceptT e m b
k))

-- Only used in hsTypeApproximation below, and in that case we catch the error.
getHsType' :: QName -> HsCompileM HS.Type
getHsType' :: QName -> HsCompileM Type
getHsType' QName
q = forall a. Term -> ToHs a -> HsCompileM a
runToHs (QName -> Elims -> Term
Def QName
q []) (QName -> ToHs Type
getHsType QName
q)

getHsType :: QName -> ToHs HS.Type
getHsType :: QName -> ToHs Type
getHsType QName
x = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isCompiled QName
x) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ QName -> WhyNot
NotCompiled QName
x

  Maybe HaskellPragma
d   <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
x
  GHCEnv
env <- forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
is QName
t GHCEnv -> Maybe QName
p = forall a. a -> Maybe a
Just QName
t forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env

      namedType :: ToHs Type
namedType = do
        -- For these builtin types, the type name (xhqn ...) refers to the
        -- generated, but unused, datatype and not the primitive type.
        if  | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNat Bool -> Bool -> Bool
||
              QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvInteger -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon [Char]
"Integer"
            | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvBool    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon [Char]
"Bool"
            | Bool
otherwise            ->
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind -> QName -> HsCompileM QName
xhqn NameKind
TypeK QName
x
  forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT (forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Maybe HaskellPragma
d) forall a b. (a -> b) -> a -> b
$ case Maybe HaskellPragma
d of
    Maybe HaskellPragma
_ | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvList ->
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind -> QName -> HsCompileM QName
xhqn NameKind
TypeK QName
x
        -- we ignore Haskell pragmas for List
    Maybe HaskellPragma
_ | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvMaybe ->
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind -> QName -> HsCompileM QName
xhqn NameKind
TypeK QName
x
        -- we ignore Haskell pragmas for Maybe
    Maybe HaskellPragma
_ | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvInf ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> Type
hsQCon [Char]
"MAlonzo.RTE" [Char]
"Infinity"
    Just HsDefn{}      -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Range -> QName -> WhyNot
WrongPragmaFor (forall a. HasRange a => a -> Range
getRange Maybe HaskellPragma
d) QName
x
    Just HsType{}      -> ToHs Type
namedType
    Just HsData{}      -> ToHs Type
namedType
    Maybe HaskellPragma
_                  -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ QName -> WhyNot
NoPragmaFor QName
x

-- | Is the given thing compiled?

isCompiled :: HasConstInfo m => QName -> m Bool
isCompiled :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isCompiled QName
q = forall a. LensModality a => a -> Bool
usableModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

-- | Does the name stand for a data or record type?

isData :: HasConstInfo m => QName -> m Bool
isData :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isData QName
q = do
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Defn
def of
    Datatype{} -> Bool
True
    Record{}   -> Bool
True
    Defn
_          -> Bool
False

getHsVar :: (MonadFail tcm, MonadTCM tcm) => Nat -> tcm HS.Name
getHsVar :: forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
i =
  [Char] -> Name
HS.Ident forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKind -> [Char] -> [Char]
encodeString (VariableKind -> NameKind
VarK VariableKind
X) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i

haskellType' :: Type -> HsCompileM HS.Type
haskellType' :: Type -> HsCompileM Type
haskellType' Type
t = forall a. Term -> ToHs a -> HsCompileM a
runToHs (forall t a. Type'' t a -> a
unEl Type
t) (Type -> ToHs Type
fromType Type
t)
  where
    fromArgs :: [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
fromArgs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term -> ToHs Type
fromTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg)
    fromType :: Type -> ToHs Type
fromType = Term -> ToHs Type
fromTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl
    fromTerm :: Term -> ToHs Type
fromTerm Term
v = do
      Term
v   <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Term -> Term
unSpine forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"compile.haskell.type" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"toHaskellType " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
v
      Maybe CoinductionKit
kit <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM (Maybe CoinductionKit)
coinductionKit
      case Term
v of
        Var Int
x Elims
es -> do
          let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type
hsVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
fromArgs [Arg Term]
args
        Def QName
d Elims
es -> do
          let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ToHs Type
getHsType QName
d forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
fromArgs [Arg Term]
args
        Pi Dom Type
a Abs Type
b ->
          if forall a. Free a => Abs a -> Bool
isBinderUsed Abs Type
b  -- Andreas, 2012-04-03.  Q: could we rely on Abs/NoAbs instead of again checking freeness of variable?
          then do
            Type
hsA <- Type -> ToHs Type
fromType (forall t e. Dom' t e -> e
unDom Dom Type
a)
            forall a (m :: * -> *) e b.
(forall b. (a -> m b) -> m b)
-> (a -> ExceptT e m b) -> ExceptT e m b
liftE1' (forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b) forall a b. (a -> b) -> a -> b
$ \ Type
b ->
              Name -> Type -> Type
hsForall forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> Type -> Type
hsFun Type
hsA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ToHs Type
fromType Type
b)
          else Type -> Type -> Type
hsFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ToHs Type
fromType (forall t e. Dom' t e -> e
unDom Dom Type
a) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ToHs Type
fromType (forall a. Subst a => Impossible -> Abs a -> a
noabsApp forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Type
b)
        Con ConHead
c ConInfo
ci Elims
es -> do
          let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ToHs Type
getHsType (ConHead -> QName
conName ConHead
c) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
fromArgs [Arg Term]
args
        Lam{}      -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadLambda Term
v)
        Level{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Lit{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Sort{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        MetaV{}    -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadMeta Term
v)
        DontCare{} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadDontCare Term
v)
        Dummy [Char]
s Elims
_  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

haskellType :: QName -> HsCompileM HS.Type
haskellType :: QName -> HsCompileM Type
haskellType QName
q = do
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let (Int
np, [Bool]
erased) =
        case Definition -> Defn
theDef Definition
def of
          Constructor{ Int
conPars :: Defn -> Int
conPars :: Int
conPars, Maybe [Bool]
conErased :: Defn -> Maybe [Bool]
conErased :: Maybe [Bool]
conErased }
            -> (Int
conPars, forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Bool]
conErased forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Bool
False)
          Defn
_ -> (Int
0, forall a. a -> [a]
repeat Bool
False)
      stripErased :: [Bool] -> Type -> Type
stripErased (Bool
True  : [Bool]
es) (HS.TyFun Type
_ Type
t)     = [Bool] -> Type -> Type
stripErased [Bool]
es Type
t
      stripErased (Bool
False : [Bool]
es) (HS.TyFun Type
s Type
t)     = Type -> Type -> Type
HS.TyFun Type
s forall a b. (a -> b) -> a -> b
$ [Bool] -> Type -> Type
stripErased [Bool]
es Type
t
      stripErased [Bool]
es           (HS.TyForall [TyVarBind]
xs Type
t) = [TyVarBind] -> Type -> Type
HS.TyForall [TyVarBind]
xs forall a b. (a -> b) -> a -> b
$ [Bool] -> Type -> Type
stripErased [Bool]
es Type
t
      stripErased [Bool]
_            Type
t                  = Type
t
      underPars :: Int -> Type -> HsCompileM Type
underPars Int
0 Type
a = [Bool] -> Type -> Type
stripErased [Bool]
erased forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> HsCompileM Type
haskellType' Type
a
      underPars Int
n Type
a = do
        Type
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        case forall t a. Type'' t a -> a
unEl Type
a of
          Pi Dom Type
a (NoAbs [Char]
_ Type
b) -> Int -> Type -> HsCompileM Type
underPars (Int
n forall a. Num a => a -> a -> a
- Int
1) Type
b
          Pi Dom Type
a Abs Type
b  -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ \Type
b -> Name -> Type -> Type
hsForall forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Type -> HsCompileM Type
underPars (Int
n forall a. Num a => a -> a -> a
- Int
1) Type
b
          Term
_       -> forall a. HasCallStack => a
__IMPOSSIBLE__
  Type
ty <- Int -> Type -> HsCompileM Type
underPars Int
np forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pragma.compile" Int
10 forall a b. (a -> b) -> a -> b
$ ((TCMT IO Doc
"Haskell type for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

checkConstructorCount :: QName -> [QName] -> [HaskellCode] -> TCM ()
checkConstructorCount :: QName -> [QName] -> [[Char]] -> TCM ()
checkConstructorCount QName
d [QName]
cs [[Char]]
hsCons
  | Int
n forall a. Eq a => a -> a -> Bool
== Int
hn   = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = do
    let n_forms_are :: [Char]
n_forms_are = case Int
hn of
          Int
1 -> [Char]
"1 Haskell constructor is"
          Int
n -> forall a. Show a => a -> [Char]
show Int
n forall a. [a] -> [a] -> [a]
++ [Char]
" Haskell constructors are"
        only :: [Char]
only | Int
hn forall a. Eq a => a -> a -> Bool
== Int
0   = [Char]
""
             | Int
hn forall a. Ord a => a -> a -> Bool
< Int
n    = [Char]
"only "
             | Bool
otherwise = [Char]
""

    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
fsep (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d forall a. a -> [a] -> [a]
: forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"has " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n forall a. [a] -> [a] -> [a]
++
            [Char]
" constructors, but " forall a. [a] -> [a] -> [a]
++ [Char]
only forall a. [a] -> [a] -> [a]
++ [Char]
n_forms_are forall a. [a] -> [a] -> [a]
++ [Char]
" given [" forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords [[Char]]
hsCons forall a. [a] -> [a] -> [a]
++ [Char]
"]"))
  where
    n :: Int
n  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs
    hn :: Int
hn = forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
hsCons

-- Type approximations ----------------------------------------------------

data PolyApprox = PolyApprox | NoPolyApprox
  deriving (PolyApprox -> PolyApprox -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PolyApprox -> PolyApprox -> Bool
$c/= :: PolyApprox -> PolyApprox -> Bool
== :: PolyApprox -> PolyApprox -> Bool
$c== :: PolyApprox -> PolyApprox -> Bool
Eq)

hsTypeApproximation :: PolyApprox -> Int -> Type -> HsCompileM HS.Type
hsTypeApproximation :: PolyApprox -> Int -> Type -> HsCompileM Type
hsTypeApproximation PolyApprox
poly Int
fv Type
t = do
  GHCEnv
env <- forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
is QName
q GHCEnv -> Maybe QName
b = forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
b GHCEnv
env
      tyCon :: [Char] -> Type
tyCon  = QName -> Type
HS.TyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
HS.Ident
      rteCon :: [Char] -> Type
rteCon = QName -> Type
HS.TyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
HS.Ident
      tyVar :: a -> a -> Type
tyVar a
n a
i = Name -> Type
HS.TyVar forall a b. (a -> b) -> a -> b
$ [Char] -> Name
HS.Ident forall a b. (a -> b) -> a -> b
$ [Char]
"a" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (a
n forall a. Num a => a -> a -> a
- a
i)
  let go :: Int -> Term -> HsCompileM Type
go Int
n Term
t = do
        Term
t <- Term -> Term
unSpine forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t
        case Term
t of
          Var Int
i Elims
_ | PolyApprox
poly forall a. Eq a => a -> a -> Bool
== PolyApprox
PolyApprox -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {a}. (Show a, Num a) => a -> a -> Type
tyVar Int
n Int
i
          Pi Dom Type
a Abs Type
b -> Type -> Type -> Type
hsFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Term -> HsCompileM Type
go (Int
n forall a. Num a => a -> a -> a
+ Int
k) (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Type
b)
            where k :: Int
k = case Abs Type
b of Abs{} -> Int
1; NoAbs{} -> Int
0
          Def QName
q Elims
els
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvList
            , Apply Arg Term
t <- forall a. a -> [a] -> a
last1 (forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
els ->
              Type -> Type -> Type
HS.TyApp ([Char] -> Type
tyCon [Char]
"[]") forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (forall e. Arg e -> e
unArg Arg Term
t)
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvMaybe
            , Apply Arg Term
t <- forall a. a -> [a] -> a
last1 (forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
els ->
              Type -> Type -> Type
HS.TyApp ([Char] -> Type
tyCon [Char]
"Maybe") forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (forall e. Arg e -> e
unArg Arg Term
t)
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvBool    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Bool"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvInteger -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Integer"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNat     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Integer"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvWord64  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
rteCon [Char]
"Word64"
            | Bool
otherwise -> do
                let args :: [Arg Term]
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
els
                forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
HS.TyApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HsCompileM Type
getHsType' QName
q forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Term -> HsCompileM Type
go Int
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term]
args
              forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> -- Not a Haskell type
                forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isCompiled QName
q) (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isData QName
q))
                  (QName -> Type
HS.TyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind -> QName -> HsCompileM QName
xhqn NameKind
TypeK QName
q)
                  (forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType)
          Sort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Type
HS.FakeType [Char]
"()"
          Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType
  Int -> Term -> HsCompileM Type
go Int
fv (forall t a. Type'' t a -> a
unEl Type
t)

-- Approximating polymorphic types is not actually a good idea unless we
-- actually keep track of type applications in recursive functions, and
-- generate parameterised datatypes. Otherwise we'll just coerce all type
-- variables to `Any` at the first `unsafeCoerce`.
hsTelApproximation :: Type -> HsCompileM ([HS.Type], HS.Type)
hsTelApproximation :: Type -> HsCompileM ([Type], Type)
hsTelApproximation = PolyApprox -> Type -> HsCompileM ([Type], Type)
hsTelApproximation' PolyApprox
NoPolyApprox

hsTelApproximation' :: PolyApprox -> Type -> HsCompileM ([HS.Type], HS.Type)
hsTelApproximation' :: PolyApprox -> Type -> HsCompileM ([Type], Type)
hsTelApproximation' PolyApprox
poly Type
t = do
  TelV Tele (Dom Type)
tel Type
res <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  let args :: [Type]
args = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel)
  (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (PolyApprox -> Int -> Type -> HsCompileM Type
hsTypeApproximation PolyApprox
poly) [Int
0..] [Type]
args forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PolyApprox -> Int -> Type -> HsCompileM Type
hsTypeApproximation PolyApprox
poly (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args) Type
res