-- | 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 (QName -> Type) -> QName -> Type
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 (QName -> Type) -> ([Char] -> QName) -> [Char] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual (Name -> QName) -> ([Char] -> Name) -> [Char] -> QName
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 = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
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 (Type -> Type) -> Type -> Type
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 = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The type" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
top] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
        [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot be translated to a corresponding Haskell type, because it contains" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
        WhyNot -> [TCMT IO Doc]
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) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ WhyNot -> TCMT IO 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) = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"the lambda term" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadMeta          Term
v) = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a meta variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadDontCare      Term
v) = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"an erased term" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (NotCompiled      QName
x) = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a name that is not compiled"
                                  [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (NoPragmaFor      QName
x) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which does not have a COMPILE pragma."
    reason (WrongPragmaFor Range
_ QName
x) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which has the wrong kind of COMPILE pragma."

    possibleFix :: WhyNot -> m Doc
possibleFix BadLambda{}     = m Doc
forall a. Null a => a
empty
    possibleFix BadMeta{}       = m Doc
forall a. Null a => a
empty
    possibleFix BadDontCare{}   = m Doc
forall a. Null a => a
empty
    possibleFix NotCompiled{}   = m Doc
forall a. Null a => a
empty
    possibleFix (NoPragmaFor QName
d) = QName -> m Doc -> m Doc
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 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"add a pragma"
    possibleFix (WrongPragmaFor Range
r QName
d) = QName -> m Doc -> m Doc
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 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"replace the value-level pragma at", Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> m Doc
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 (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
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 (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" | " [ [Char]
"C" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i | a
i <- [a
1..a
n] ] [Char] -> [Char] -> [Char]
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 } -> Int -> ([Char], [Char])
forall {a} {a}.
(IsString a, Num a, Enum a, Show a) =>
a -> (a, [Char])
dataPragma ([QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs)
              Record{}                  -> Integer -> ([Char], [Char])
forall {a} {a}.
(IsString a, Num a, Enum a, Show a) =>
a -> (a, [Char])
dataPragma Integer
1
              Defn
_                         -> ([Char], [Char])
typePragma
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [m Doc
"Possible fix:", m Doc
action]
           , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ m Doc
"{-# COMPILE GHC", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d, m Doc
"=", [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
pragma, m Doc
"#-}" ]
           , [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"for a suitable Haskell " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
hsThing [Char] -> [Char] -> [Char]
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 = (WhyNot
 -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
-> (a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
-> Either WhyNot a
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
-> (WhyNot -> TCM a)
-> WhyNot
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> WhyNot -> TCM a
forall a. Term -> WhyNot -> TCM a
notAHaskellType Term
top) a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either WhyNot a
 -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Either WhyNot a)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ToHs a
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Either WhyNot a)
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 = m (Either e b) -> ExceptT e m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT ((a -> m (Either e b)) -> m (Either e b)
forall b. (a -> m b) -> m b
f (ExceptT e m b -> m (Either e b)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT e m b -> m (Either e b))
-> (a -> ExceptT e m b) -> a -> m (Either e b)
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 = Term -> ToHs Type -> HsCompileM Type
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
  ExceptT WhyNot HsCompileM Bool
-> ExceptT WhyNot HsCompileM () -> ExceptT WhyNot HsCompileM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (QName -> ExceptT WhyNot HsCompileM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isCompiled QName
x) (ExceptT WhyNot HsCompileM () -> ExceptT WhyNot HsCompileM ())
-> ExceptT WhyNot HsCompileM () -> ExceptT WhyNot HsCompileM ()
forall a b. (a -> b) -> a -> b
$ WhyNot -> ExceptT WhyNot HsCompileM ()
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (WhyNot -> ExceptT WhyNot HsCompileM ())
-> WhyNot -> ExceptT WhyNot HsCompileM ()
forall a b. (a -> b) -> a -> b
$ QName -> WhyNot
NotCompiled QName
x

  Maybe HaskellPragma
d   <- TCM (Maybe HaskellPragma)
-> ExceptT WhyNot HsCompileM (Maybe HaskellPragma)
forall a. TCM a -> ExceptT WhyNot HsCompileM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ExceptT WhyNot HsCompileM (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ExceptT WhyNot HsCompileM (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
x
  GHCEnv
env <- ExceptT WhyNot HsCompileM GHCEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
is QName
t GHCEnv -> Maybe QName
p = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
t Maybe QName -> Maybe QName -> Bool
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 -> Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> ToHs Type) -> Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon [Char]
"Integer"
            | QName
x QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvBool    -> Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> ToHs Type) -> Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon [Char]
"Bool"
            | Bool
otherwise            ->
              HsCompileM Type -> ToHs Type
forall (m :: * -> *) a. Monad m => m a -> ExceptT WhyNot m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon ([Char] -> Type) -> (QName -> [Char]) -> QName -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
-> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind
-> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
xhqn NameKind
TypeK QName
x
  (ReaderT
   GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Either WhyNot Type)
 -> ReaderT
      GHCModuleEnv
      (StateT HsCompileState (TCMT IO))
      (Either WhyNot Type))
-> ToHs Type -> ToHs Type
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT (Maybe HaskellPragma
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Either WhyNot Type)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Either WhyNot Type)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Maybe HaskellPragma
d) (ToHs Type -> ToHs Type) -> ToHs Type -> ToHs Type
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 ->
        HsCompileM Type -> ToHs Type
forall (m :: * -> *) a. Monad m => m a -> ExceptT WhyNot m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon ([Char] -> Type) -> (QName -> [Char]) -> QName -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
-> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind
-> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) 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 ->
        HsCompileM Type -> ToHs Type
forall (m :: * -> *) a. Monad m => m a -> ExceptT WhyNot m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
hsCon ([Char] -> Type) -> (QName -> [Char]) -> QName -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
-> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind
-> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) 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 ->
        Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> ToHs Type) -> Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> Type
hsQCon [Char]
"MAlonzo.RTE" [Char]
"Infinity"
    Just HsDefn{}      -> WhyNot -> ToHs Type
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (WhyNot -> ToHs Type) -> WhyNot -> ToHs Type
forall a b. (a -> b) -> a -> b
$ Range -> QName -> WhyNot
WrongPragmaFor (Maybe HaskellPragma -> Range
forall a. HasRange a => a -> Range
getRange Maybe HaskellPragma
d) QName
x
    Just HsType{}      -> ToHs Type
namedType
    Just HsData{}      -> ToHs Type
namedType
    Maybe HaskellPragma
_                  -> WhyNot -> ToHs Type
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (WhyNot -> ToHs Type) -> WhyNot -> ToHs Type
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 = Definition -> Bool
forall a. LensModality a => a -> Bool
usableModality (Definition -> Bool) -> m Definition -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
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 (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
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 ([Char] -> Name) -> (Name -> [Char]) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKind -> [Char] -> [Char]
encodeString (VariableKind -> NameKind
VarK VariableKind
X) ([Char] -> [Char]) -> (Name -> [Char]) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> Name) -> tcm Name -> tcm Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> tcm Name
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 = Term -> ToHs Type -> HsCompileM Type
forall a. Term -> ToHs a -> HsCompileM a
runToHs (Type -> Term
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 = (Arg Term -> ToHs Type)
-> [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> ToHs Type
fromTerm (Term -> ToHs Type) -> (Arg Term -> Term) -> Arg Term -> ToHs Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg)
    fromType :: Type -> ToHs Type
fromType = Term -> ToHs Type
fromTerm (Term -> ToHs Type) -> (Type -> Term) -> Type -> ToHs Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl
    fromTerm :: Term -> ToHs Type
fromTerm Term
v = do
      Term
v   <- TCM Term -> ExceptT WhyNot HsCompileM Term
forall a. TCM a -> ExceptT WhyNot HsCompileM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> ExceptT WhyNot HsCompileM Term)
-> TCM Term -> ExceptT WhyNot HsCompileM Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
unSpine (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      [Char] -> Int -> [Char] -> ExceptT WhyNot HsCompileM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"compile.haskell.type" Int
50 ([Char] -> ExceptT WhyNot HsCompileM ())
-> [Char] -> ExceptT WhyNot HsCompileM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"toHaskellType " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
v
      Maybe CoinductionKit
kit <- TCM (Maybe CoinductionKit)
-> ExceptT WhyNot HsCompileM (Maybe CoinductionKit)
forall a. TCM a -> ExceptT WhyNot HsCompileM a
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 = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp (Type -> [Type] -> Type)
-> (Name -> Type) -> Name -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type
hsVar (Name -> [Type] -> Type)
-> ExceptT WhyNot HsCompileM Name
-> ExceptT WhyNot HsCompileM ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ExceptT WhyNot HsCompileM Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
x ExceptT WhyNot HsCompileM ([Type] -> Type)
-> ExceptT WhyNot HsCompileM [Type] -> ToHs Type
forall a b.
ExceptT WhyNot HsCompileM (a -> b)
-> ExceptT WhyNot HsCompileM a -> ExceptT WhyNot HsCompileM b
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 = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp (Type -> [Type] -> Type)
-> ToHs Type -> ExceptT WhyNot HsCompileM ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ToHs Type
getHsType QName
d ExceptT WhyNot HsCompileM ([Type] -> Type)
-> ExceptT WhyNot HsCompileM [Type] -> ToHs Type
forall a b.
ExceptT WhyNot HsCompileM (a -> b)
-> ExceptT WhyNot HsCompileM a -> ExceptT WhyNot HsCompileM b
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 Abs Type -> Bool
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 (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
            (forall b. (Type -> HsCompileM b) -> HsCompileM b)
-> (Type -> ToHs Type) -> ToHs Type
forall a (m :: * -> *) e b.
(forall b. (a -> m b) -> m b)
-> (a -> ExceptT e m b) -> ExceptT e m b
liftE1' (Dom Type
-> Abs Type
-> (Type
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) 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) ((Type -> ToHs Type) -> ToHs Type)
-> (Type -> ToHs Type) -> ToHs Type
forall a b. (a -> b) -> a -> b
$ \ Type
b ->
              Name -> Type -> Type
hsForall (Name -> Type -> Type)
-> ExceptT WhyNot HsCompileM Name
-> ExceptT WhyNot HsCompileM (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ExceptT WhyNot HsCompileM Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 ExceptT WhyNot HsCompileM (Type -> Type) -> ToHs Type -> ToHs Type
forall a b.
ExceptT WhyNot HsCompileM (a -> b)
-> ExceptT WhyNot HsCompileM a -> ExceptT WhyNot HsCompileM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> Type -> Type
hsFun Type
hsA (Type -> Type) -> ToHs Type -> ToHs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ToHs Type
fromType Type
b)
          else Type -> Type -> Type
hsFun (Type -> Type -> Type)
-> ToHs Type -> ExceptT WhyNot HsCompileM (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ToHs Type
fromType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) ExceptT WhyNot HsCompileM (Type -> Type) -> ToHs Type -> ToHs Type
forall a b.
ExceptT WhyNot HsCompileM (a -> b)
-> ExceptT WhyNot HsCompileM a -> ExceptT WhyNot HsCompileM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ToHs Type
fromType (Impossible -> Abs Type -> Type
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Type
b)
        Con ConHead
c ConInfo
ci Elims
es -> do
          let args :: [Arg Term]
args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          Type -> [Type] -> Type
hsApp (Type -> [Type] -> Type)
-> ToHs Type -> ExceptT WhyNot HsCompileM ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ToHs Type
getHsType (ConHead -> QName
conName ConHead
c) ExceptT WhyNot HsCompileM ([Type] -> Type)
-> ExceptT WhyNot HsCompileM [Type] -> ToHs Type
forall a b.
ExceptT WhyNot HsCompileM (a -> b)
-> ExceptT WhyNot HsCompileM a -> ExceptT WhyNot HsCompileM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot HsCompileM [Type]
fromArgs [Arg Term]
args
        Lam{}      -> WhyNot -> ToHs Type
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadLambda Term
v)
        Level{}    -> Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Lit{}      -> Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Sort{}     -> Type -> ToHs Type
forall a. a -> ExceptT WhyNot HsCompileM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        MetaV{}    -> WhyNot -> ToHs Type
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadMeta Term
v)
        DontCare{} -> WhyNot -> ToHs Type
forall a. WhyNot -> ExceptT WhyNot HsCompileM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadDontCare Term
v)
        Dummy [Char]
s Elims
_  -> [Char] -> ToHs Type
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 <- QName
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
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 :: Int
conPars :: Defn -> Int
conPars, Maybe [Bool]
conErased :: Maybe [Bool]
conErased :: Defn -> Maybe [Bool]
conErased }
            -> (Int
conPars, [Bool] -> Maybe [Bool] -> [Bool]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Bool]
conErased [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
          Defn
_ -> (Int
0, Bool -> [Bool]
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 (Type -> Type) -> Type -> Type
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 (Type -> Type) -> Type -> Type
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 (Type -> Type) -> HsCompileM Type -> HsCompileM Type
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 <- Type -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
        case Type -> Term
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
b
          Pi Dom Type
a Abs Type
b  -> Dom Type
-> Abs Type -> (Type -> HsCompileM Type) -> HsCompileM Type
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b ((Type -> HsCompileM Type) -> HsCompileM Type)
-> (Type -> HsCompileM Type) -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ \Type
b -> Name -> Type -> Type
hsForall (Name -> Type -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Name
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 ReaderT
  GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
-> HsCompileM Type -> HsCompileM Type
forall a b.
ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Type -> HsCompileM Type
underPars (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
b
          Term
_       -> HsCompileM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
  Type
ty <- Int -> Type -> HsCompileM Type
underPars Int
np (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  [Char]
-> Int
-> TCMT IO Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.pragma.compile" Int
10 (TCMT IO Doc
 -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ())
-> TCMT IO Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
forall a b. (a -> b) -> a -> b
$ ((TCMT IO Doc
"Haskell type for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
  Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
hn   = () -> TCM ()
forall a. a -> TCMT IO a
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 -> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" Haskell constructors are"
        only :: [Char]
only | Int
hn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0   = [Char]
""
             | Int
hn Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n    = [Char]
"only "
             | Bool
otherwise = [Char]
""

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

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

data PolyApprox = PolyApprox | NoPolyApprox
  deriving (PolyApprox -> PolyApprox -> Bool
(PolyApprox -> PolyApprox -> Bool)
-> (PolyApprox -> PolyApprox -> Bool) -> Eq PolyApprox
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PolyApprox -> PolyApprox -> Bool
== :: PolyApprox -> PolyApprox -> Bool
$c/= :: PolyApprox -> PolyApprox -> Bool
/= :: 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 <- ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) GHCEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
is QName
q GHCEnv -> Maybe QName
b = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
b GHCEnv
env
      tyCon :: [Char] -> Type
tyCon  = QName -> Type
HS.TyCon (QName -> Type) -> ([Char] -> QName) -> [Char] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual (Name -> QName) -> ([Char] -> Name) -> [Char] -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
HS.Ident
      rteCon :: [Char] -> Type
rteCon = QName -> Type
HS.TyCon (QName -> Type) -> ([Char] -> QName) -> [Char] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> ([Char] -> Name) -> [Char] -> QName
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 (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Name
HS.Ident ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ [Char]
"a" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show (a
n a -> a -> a
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 (Term -> Term)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t
        case Term
t of
          Var Int
i Elims
_ | PolyApprox
poly PolyApprox -> PolyApprox -> Bool
forall a. Eq a => a -> a -> Bool
== PolyApprox
PolyApprox -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Type
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 (Type -> Type -> Type)
-> HsCompileM Type
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) ReaderT
  GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
-> HsCompileM Type -> HsCompileM Type
forall a b.
ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Term -> HsCompileM Type
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
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 <- Elim' Term -> Elims -> Elim' Term
forall a. a -> [a] -> a
last1 (ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
els ->
              Type -> Type -> Type
HS.TyApp ([Char] -> Type
tyCon [Char]
"[]") (Type -> Type) -> HsCompileM Type -> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (Arg Term -> Term
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 <- Elim' Term -> Elims -> Elim' Term
forall a. a -> [a] -> a
last1 (ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
els ->
              Type -> Type -> Type
HS.TyApp ([Char] -> Type
tyCon [Char]
"Maybe") (Type -> Type) -> HsCompileM Type -> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> HsCompileM Type
go Int
n (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t)
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvBool    -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Bool"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvInteger -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Integer"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNat     -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
tyCon [Char]
"Integer"
            | QName
q QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvWord64  -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
rteCon [Char]
"Word64"
            | Bool
otherwise -> do
                let args :: [Arg Term]
args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
els
                (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
HS.TyApp (Type -> [Type] -> Type)
-> HsCompileM Type
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HsCompileM Type
getHsType' QName
q ReaderT
  GHCModuleEnv (StateT HsCompileState (TCMT IO)) ([Type] -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
-> HsCompileM Type
forall a b.
ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Arg Term -> HsCompileM Type)
-> [Arg Term]
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int -> Term -> HsCompileM Type
go Int
n (Term -> HsCompileM Type)
-> (Arg Term -> Term) -> Arg Term -> HsCompileM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
args
              HsCompileM Type -> (TCErr -> HsCompileM Type) -> HsCompileM Type
forall a.
ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
-> (TCErr
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> -- Not a Haskell type
                ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
-> HsCompileM Type -> HsCompileM Type -> HsCompileM Type
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isCompiled QName
q) (QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isData QName
q))
                  (QName -> Type
HS.TyCon (QName -> Type)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
-> HsCompileM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameKind
-> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
xhqn NameKind
TypeK QName
q)
                  (Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType)
          Sort{} -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Type
HS.FakeType [Char]
"()"
          Term
_ -> Type -> HsCompileM Type
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType
  Int -> Term -> HsCompileM Type
go Int
fv (Type -> Term
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 <- Type
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  let args :: [Type]
args = (Dom' Term ([Char], Type) -> Type)
-> [Dom' Term ([Char], Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type)
-> (Dom' Term ([Char], Type) -> ([Char], Type))
-> Dom' Term ([Char], Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom) (Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel)
  (,) ([Type] -> Type -> ([Type], Type))
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
-> ReaderT
     GHCModuleEnv
     (StateT HsCompileState (TCMT IO))
     (Type -> ([Type], Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Type -> HsCompileM Type)
-> [Int]
-> [Type]
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
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 ReaderT
  GHCModuleEnv
  (StateT HsCompileState (TCMT IO))
  (Type -> ([Type], Type))
-> HsCompileM Type -> HsCompileM ([Type], Type)
forall a b.
ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PolyApprox -> Int -> Type -> HsCompileM Type
hsTypeApproximation PolyApprox
poly ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args) Type
res