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 )
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 ()
import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.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]
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
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
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]
"type HsT", [Char]
"type HsT")
(hsThing, pragma) =
case 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
vcat [ sep ["Possible fix:", action]
, nest 2 $ hsep [ "{-# COMPILE GHC", prettyTCM d, "=", text pragma, "#-}" ]
, text ("for a suitable Haskell " ++ hsThing ++ ".")
]
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))
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
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
env <- askGHCEnv
let 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 = do
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
mapExceptT (setCurrentRange d) $ case 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
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
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
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
isData :: HasConstInfo m => QName -> m Bool
isData :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isData QName
q = do
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
return $ case 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
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
reportSDoc "compile.haskell.type" 25 $ "toHaskellType " <+> prettyTCM v
reportSDoc "compile.haskell.type" 50 $ "toHaskellType " <+> pretty v
kit <- liftTCM coinductionKit
case 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
then do
hsA <- Type -> ToHs Type
fromType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
liftE1' (underAbstraction 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
def <- QName
-> ReaderT
GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
let (np, erased) =
case theDef 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
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
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
a <- Type -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a
case unEl 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__
ty <- underPars np $ defType def
reportSDoc "tc.pragma.compile" 10 $ (("Haskell type for" <+> prettyTCM q) <> ":") <?> pretty ty
return 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
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
env <- ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) GHCEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
let 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 = 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 = 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
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
n Term
t = do
[Char]
-> Int
-> TCMT IO Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"compile.haskell.type" Int
25 (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
"hsTypeApproximation " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
[Char]
-> Int
-> TCMT IO Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"compile.haskell.type" Int
50 (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
"hsTypeApproximation " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
t
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 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
, Just Int
k <- GHCEnv -> Maybe Int
ghcEnvListArity GHCEnv
env
, [Apply Arg Term
t] <- Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) 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
, Just Int
k <- GHCEnv -> Maybe Int
ghcEnvMaybeArity GHCEnv
env
, [Apply Arg Term
t] <- Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) 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
_ ->
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
go fv (unEl t)
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 tel res <- Type
-> ReaderT
GHCModuleEnv (StateT HsCompileState (TCMT IO)) (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
let 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)
(,) <$> zipWithM (hsTypeApproximation poly) [0..] args <*> hsTypeApproximation poly (length args) res