-- | 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.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.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive (getBuiltinName)
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.Except
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Null

import Agda.Utils.Impossible

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

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

hsUnit :: HS.Type
hsUnit :: Type
hsUnit = String -> Type
hsCon String
"()"

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 (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]

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

type ToHs = ExceptT WhyNot TCM

notAHaskellType :: Term -> WhyNot -> TCM a
notAHaskellType :: Term -> WhyNot -> TCM a
notAHaskellType Term
top WhyNot
offender = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep (String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM Term
top] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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), MonadReduce m, MonadAddContext m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames 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), HasConstInfo m, IsString (m Doc), MonadReduce m,
 MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m,
 HasBuiltins m, MonadStConcreteNames m, Semigroup (m Doc)) =>
WhyNot -> m Doc
possibleFix WhyNot
offender
  where
    reason :: WhyNot -> [m Doc]
reason (BadLambda        Term
v) = String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadMeta          Term
v) = String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
    reason (BadDontCare      Term
v) = String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM Term
v 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
prettyTCM QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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
prettyTCM QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ String -> [m Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords String
"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 (NoPragmaFor QName
d) = QName -> m Doc -> m Doc
forall (m :: * -> *).
(HasConstInfo m, IsString (m Doc), MonadReduce m,
 MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m,
 HasBuiltins m, MonadStConcreteNames 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 :: * -> *).
(HasConstInfo m, IsString (m Doc), MonadReduce m,
 MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m,
 HasBuiltins m, MonadStConcreteNames 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 :: * -> *). Monad m => [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. (Monad 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, String)
dataPragma a
n = (a
"data type HsD", String
"data HsD (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" | " [ String
"C" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i | a
i <- [a
1..a
n] ] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")
          typePragma :: (String, String)
typePragma   = (String
"type HsT", String
"type HsT")
          (String
hsThing, String
pragma) =
            case Defn
def of
              Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> Int -> (String, String)
forall a a. (IsString a, Num a, Enum a, Show a) => a -> (a, String)
dataPragma ([QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs)
              Record{}                  -> Integer -> (String, String)
forall a a. (IsString a, Num a, Enum a, Show a) => a -> (a, String)
dataPragma Integer
1
              Defn
_                         -> (String, String)
typePragma
      [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ [m Doc] -> m Doc
forall (m :: * -> *). Monad m => [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 :: * -> *). Monad m => [m Doc] -> m Doc
hsep [ m Doc
"{-# COMPILE GHC", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d, m Doc
"=", String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
pragma, m Doc
"#-}" ]
           , String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String
"for a suitable Haskell " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hsThing String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".")
           ]

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

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

liftE1' :: (forall b. (a -> m b) -> m b) -> (a -> ExceptT e m b) -> ExceptT e m b
liftE1' :: (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 (m :: * -> *) e a. m (Either e a) -> ExceptT e m a
mkExceptT ((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 -> TCM HS.Type
getHsType' :: QName -> TCM Type
getHsType' QName
q = Term -> ToHs Type -> TCM Type
forall a. Term -> ToHs a -> TCM 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
  Maybe HaskellPragma
d <- TCM (Maybe HaskellPragma)
-> ExceptT WhyNot TCM (Maybe HaskellPragma)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ExceptT WhyNot TCM (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ExceptT WhyNot TCM (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
x
  Maybe QName
list <- TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName))
-> TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinList
  Maybe QName
inf  <- TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName))
-> TCM (Maybe QName) -> ExceptT WhyNot TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinInf
  let namedType :: ToHs Type
namedType = TCM Type -> ToHs Type
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Type -> ToHs Type) -> TCM Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ do
        -- For these builtin types, the type name (xhqn ...) refers to the
        -- generated, but unused, datatype and not the primitive type.
        Maybe QName
nat  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinNat
        Maybe QName
int  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinInteger
        Maybe QName
bool <- String -> TCM (Maybe QName)
getBuiltinName String
builtinBool
        if  | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
nat, Maybe QName
int] -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
hsCon String
"Integer"
            | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
bool           -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
hsCon String
"Bool"
            | Bool
otherwise                -> String -> Type
hsCon (String -> Type) -> (QName -> String) -> QName -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Pretty a => a -> String
prettyShow (QName -> Type) -> TCMT IO QName -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> QName -> TCMT IO QName
xhqn String
"T" QName
x
  (forall a. TCM a -> TCM a) -> ToHs Type -> ToHs Type
forall (m :: * -> *) e a.
(forall a. m a -> m a) -> ExceptT e m a -> ExceptT e m a
liftE1 (Maybe HaskellPragma -> TCM a -> TCM a
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm 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 -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
list -> TCM Type -> ToHs Type
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Type -> ToHs Type) -> TCM Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ String -> Type
hsCon (String -> Type) -> (QName -> String) -> QName -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Pretty a => a -> String
prettyShow (QName -> Type) -> TCMT IO QName -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> QName -> TCMT IO QName
xhqn String
"T" QName
x -- we ignore Haskell pragmas for List
    Maybe HaskellPragma
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
inf  -> Type -> ToHs Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> ToHs Type) -> Type -> ToHs Type
forall a b. (a -> b) -> a -> b
$ String -> String -> Type
hsQCon String
"MAlonzo.RTE" String
"Infinity"
    Just HsDefn{}      -> WhyNot -> ToHs Type
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 t. HasRange t => t -> Range
getRange Maybe HaskellPragma
d) QName
x
    Just HsType{}      -> ToHs Type
namedType
    Just HsData{}      -> ToHs Type
namedType
    Maybe HaskellPragma
_                  -> WhyNot -> ToHs Type
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

getHsVar :: (MonadFail tcm, MonadTCM tcm) => Nat -> tcm HS.Name
getHsVar :: Int -> tcm Name
getHsVar Int
i = String -> Name
HS.Ident (String -> Name) -> (Name -> String) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Pretty a => a -> String
encodeName (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
  where
    encodeName :: a -> String
encodeName a
x = String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
encode (a -> String
forall a. Pretty a => a -> String
prettyShow a
x)
    okChars :: String
okChars = [Char
'a'..Char
'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Y'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_'"
    encode :: Char -> String
encode Char
'Z' = String
"ZZ"
    encode Char
c
      | Char
c Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
okChars = [Char
c]
      | Bool
otherwise        = String
"Z" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c)

haskellType' :: Type -> TCM HS.Type
haskellType' :: Type -> TCM Type
haskellType' Type
t = Term -> ToHs Type -> TCM Type
forall a. Term -> ToHs a -> TCM 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 TCM [Type]
fromArgs = (Arg Term -> ToHs Type) -> [Arg Term] -> ExceptT WhyNot TCM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 TCM Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> ExceptT WhyNot TCM Term)
-> TCM Term -> ExceptT WhyNot TCM 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
      String -> Int -> String -> ExceptT WhyNot TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.haskell.type" Int
50 (String -> ExceptT WhyNot TCM ())
-> String -> ExceptT WhyNot TCM ()
forall a b. (a -> b) -> a -> b
$ String
"toHaskellType " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
v
      Maybe CoinductionKit
kit <- TCM (Maybe CoinductionKit)
-> ExceptT WhyNot TCM (Maybe CoinductionKit)
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 TCM Name -> ExceptT WhyNot TCM ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ExceptT WhyNot TCM Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
x ExceptT WhyNot TCM ([Type] -> Type)
-> ExceptT WhyNot TCM [Type] -> ToHs Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot TCM [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 TCM ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ToHs Type
getHsType QName
d ExceptT WhyNot TCM ([Type] -> Type)
-> ExceptT WhyNot TCM [Type] -> ToHs Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot TCM [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 -> TCM b) -> TCM 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 -> TCM b) -> TCM b
forall t a (m :: * -> *) b.
(Subst t 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 TCM Name -> ExceptT WhyNot TCM (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ExceptT WhyNot TCM Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 ExceptT WhyNot TCM (Type -> Type) -> ToHs Type -> ToHs Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> Type -> Type
HS.TyFun 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
HS.TyFun (Type -> Type -> Type)
-> ToHs Type -> ExceptT WhyNot TCM (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 TCM (Type -> Type) -> ToHs Type -> ToHs Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ToHs Type
fromType (Empty -> Abs Type -> Type
forall t a. Subst t a => Empty -> Abs a -> a
noabsApp Empty
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 TCM ([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 TCM ([Type] -> Type)
-> ExceptT WhyNot TCM [Type] -> ToHs Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Arg Term] -> ExceptT WhyNot TCM [Type]
fromArgs [Arg Term]
args
        Lam{}      -> WhyNot -> ToHs Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadLambda Term
v)
        Level{}    -> Type -> ToHs Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Lit{}      -> Type -> ToHs Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        Sort{}     -> Type -> ToHs Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
hsUnit
        MetaV{}    -> WhyNot -> ToHs Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadMeta Term
v)
        DontCare{} -> WhyNot -> ToHs Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> WhyNot
BadDontCare Term
v)
        Dummy String
s Elims
_  -> String -> ToHs Type
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

haskellType :: QName -> TCM HS.Type
haskellType :: QName -> TCM Type
haskellType QName
q = do
  Definition
def <- QName -> 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 :: Defn -> Int
conPars :: Int
conPars, Maybe [Bool]
conErased :: Defn -> Maybe [Bool]
conErased :: 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 :: a -> Type -> TCM Type
underPars a
0 Type
a = [Bool] -> Type -> Type
stripErased [Bool]
erased (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
haskellType' Type
a
      underPars a
n Type
a = do
        Type
a <- Type -> 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 String
_ Type
b) -> a -> Type -> TCM Type
underPars (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) Type
b
          Pi Dom Type
a Abs Type
b  -> Dom Type -> Abs Type -> (Type -> TCM Type) -> TCM Type
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b ((Type -> TCM Type) -> TCM Type) -> (Type -> TCM Type) -> TCM Type
forall a b. (a -> b) -> a -> b
$ \Type
b -> Name -> Type -> Type
hsForall (Name -> Type -> Type) -> TCMT IO Name -> TCMT IO (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Name
forall (tcm :: * -> *).
(MonadFail tcm, MonadTCM tcm) =>
Int -> tcm Name
getHsVar Int
0 TCMT IO (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> Type -> TCM Type
underPars (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) Type
b
          Term
_       -> TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
  Type
ty <- Int -> Type -> TCM Type
forall a. (Num a, Eq a) => a -> Type -> TCM Type
underPars Int
np (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.pragma.compile" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> 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
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. (Monad m, Pretty a) => a -> m Doc
pretty Type
ty
  Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

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

    Doc -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ([QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ String -> [TCMT IO Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords (String
"has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String
" constructors, but " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
only String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n_forms_are String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" given [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
hsCons String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"))
  where
    n :: Int
n  = [QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs
    hn :: Int
hn = [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
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
/= :: PolyApprox -> PolyApprox -> Bool
$c/= :: PolyApprox -> PolyApprox -> Bool
== :: PolyApprox -> PolyApprox -> Bool
$c== :: PolyApprox -> PolyApprox -> Bool
Eq)

hsTypeApproximation :: PolyApprox -> Int -> Type -> TCM HS.Type
hsTypeApproximation :: PolyApprox -> Int -> Type -> TCM Type
hsTypeApproximation PolyApprox
poly Int
fv Type
t = do
  Maybe QName
list <- String -> TCM (Maybe QName)
getBuiltinName String
builtinList
  Maybe QName
bool <- String -> TCM (Maybe QName)
getBuiltinName String
builtinBool
  Maybe QName
int  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinInteger
  Maybe QName
nat  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinNat
  Maybe QName
word <- String -> TCM (Maybe QName)
getBuiltinName String
builtinWord64
  let is :: a -> Maybe a -> Bool
is a
q Maybe a
b = a -> Maybe a
forall a. a -> Maybe a
Just a
q Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe a
b
      tyCon :: String -> Type
tyCon  = QName -> Type
HS.TyCon (QName -> Type) -> (String -> QName) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual (Name -> QName) -> (String -> Name) -> String -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident
      rteCon :: String -> Type
rteCon = QName -> Type
HS.TyCon (QName -> Type) -> (String -> QName) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> (String -> Name) -> String -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> 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
$ String -> Name
HS.Ident (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
i)
  let go :: Int -> Term -> TCM Type
go Int
n Term
t = do
        Term
t <- 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
t
        case Term
t of
          Var Int
i Elims
_ | PolyApprox
poly PolyApprox -> PolyApprox -> Bool
forall a. Eq a => a -> a -> Bool
== PolyApprox
PolyApprox -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM 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
HS.TyFun (Type -> Type -> Type) -> TCM Type -> TCMT IO (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> TCM 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) TCMT IO (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Term -> TCM 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 -> Maybe QName -> Bool
forall a. Eq a => a -> Maybe a -> Bool
`is` Maybe QName
list, Apply Arg Term
t <- Elims -> Elim' Term
forall a. [a] -> a
last ([ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
forall a. HasCallStack => a
__IMPOSSIBLE__] Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
els)
                        -> Type -> Type -> Type
HS.TyApp (String -> Type
tyCon String
"[]") (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> TCM Type
go Int
n (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t)
            | QName
q QName -> Maybe QName -> Bool
forall a. Eq a => a -> Maybe a -> Bool
`is` Maybe QName
bool -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
tyCon String
"Bool"
            | QName
q QName -> Maybe QName -> Bool
forall a. Eq a => a -> Maybe a -> Bool
`is` Maybe QName
int  -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
tyCon String
"Integer"
            | QName
q QName -> Maybe QName -> Bool
forall a. Eq a => a -> Maybe a -> Bool
`is` Maybe QName
nat  -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
tyCon String
"Integer"
            | QName
q QName -> Maybe QName -> Bool
forall a. Eq a => a -> Maybe a -> Bool
`is` Maybe QName
word -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
rteCon String
"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 (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
HS.TyApp (Type -> [Type] -> Type) -> TCM Type -> TCMT IO ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Type
getHsType' QName
q TCMT IO ([Type] -> Type) -> TCMT IO [Type] -> TCM Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Arg Term -> TCM Type) -> [Arg Term] -> TCMT IO [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Term -> TCM Type
go Int
n (Term -> TCM Type) -> (Arg Term -> Term) -> Arg Term -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
args
              TCM Type -> (TCErr -> TCM Type) -> TCM Type
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> do -- Not a Haskell type
                Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
                let isData :: Bool
isData | Datatype{} <- Defn
def = Bool
True
                           | Record{}   <- Defn
def = Bool
True
                           | Bool
otherwise         = Bool
False
                if Bool
isData then QName -> Type
HS.TyCon (QName -> Type) -> TCMT IO QName -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> QName -> TCMT IO QName
xhqn String
"T" QName
q
                          else Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType
          Sort{} -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> Type
HS.FakeType String
"()"
          Term
_ -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
mazAnyType
  Int -> Term -> TCM 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 -> TCM ([HS.Type], HS.Type)
hsTelApproximation :: Type -> TCM ([Type], Type)
hsTelApproximation = PolyApprox -> Type -> TCM ([Type], Type)
hsTelApproximation' PolyApprox
NoPolyApprox

hsTelApproximation' :: PolyApprox -> Type -> TCM ([HS.Type], HS.Type)
hsTelApproximation' :: PolyApprox -> Type -> TCM ([Type], Type)
hsTelApproximation' PolyApprox
poly Type
t = do
  TelV Tele (Dom Type)
tel Type
res <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let args :: [Type]
args = (Dom' Term (String, Type) -> Type)
-> [Dom' Term (String, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> (Dom' Term (String, Type) -> (String, Type))
-> Dom' Term (String, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom) (Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel)
  (,) ([Type] -> Type -> ([Type], Type))
-> TCMT IO [Type] -> TCMT IO (Type -> ([Type], Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Type -> TCM Type) -> [Int] -> [Type] -> TCMT IO [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (PolyApprox -> Int -> Type -> TCM Type
hsTypeApproximation PolyApprox
poly) [Int
0..] [Type]
args TCMT IO (Type -> ([Type], Type)) -> TCM Type -> TCM ([Type], Type)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PolyApprox -> Int -> Type -> TCM Type
hsTypeApproximation PolyApprox
poly ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args) Type
res