{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Compiler.MAlonzo.Pragmas where
import Control.Monad
import Data.Maybe
import Data.Char
import qualified Data.List as List
import qualified Data.Map as Map
import Text.ParserCombinators.ReadP
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.Syntax.Common.Pretty hiding (char)
import Agda.Utils.String ( ltrim )
import Agda.Utils.Three
import Agda.Compiler.MAlonzo.Misc
import Agda.Utils.Impossible
type HaskellCode = String
type HaskellType = String
data HaskellPragma
= HsDefn Range HaskellCode
| HsType Range HaskellType
| HsData Range HaskellType [HaskellCode]
| HsExport Range HaskellCode
deriving (Int -> HaskellPragma -> ShowS
[HaskellPragma] -> ShowS
HaskellPragma -> [Char]
(Int -> HaskellPragma -> ShowS)
-> (HaskellPragma -> [Char])
-> ([HaskellPragma] -> ShowS)
-> Show HaskellPragma
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HaskellPragma -> ShowS
showsPrec :: Int -> HaskellPragma -> ShowS
$cshow :: HaskellPragma -> [Char]
show :: HaskellPragma -> [Char]
$cshowList :: [HaskellPragma] -> ShowS
showList :: [HaskellPragma] -> ShowS
Show, HaskellPragma -> HaskellPragma -> Bool
(HaskellPragma -> HaskellPragma -> Bool)
-> (HaskellPragma -> HaskellPragma -> Bool) -> Eq HaskellPragma
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HaskellPragma -> HaskellPragma -> Bool
== :: HaskellPragma -> HaskellPragma -> Bool
$c/= :: HaskellPragma -> HaskellPragma -> Bool
/= :: HaskellPragma -> HaskellPragma -> Bool
Eq)
instance HasRange HaskellPragma where
getRange :: HaskellPragma -> Range
getRange (HsDefn Range
r [Char]
_) = Range
r
getRange (HsType Range
r [Char]
_) = Range
r
getRange (HsData Range
r [Char]
_ [[Char]]
_) = Range
r
getRange (HsExport Range
r [Char]
_) = Range
r
instance Pretty HaskellPragma where
pretty :: HaskellPragma -> Doc
pretty = \case
HsDefn Range
_r [Char]
hsCode -> Doc
equals Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
hsCode
HsType Range
_r [Char]
hsType -> Doc
equals Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
hsType
HsData Range
_r [Char]
hsType [[Char]]
hsCons -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
[ Doc
equals, Doc
"data", [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
hsType
, Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc
forall a. [Char] -> Doc a
text ([[Char]] -> [Doc]) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
List.intersperse [Char]
"|" [[Char]]
hsCons
]
HsExport Range
_r [Char]
hsCode -> Doc
"as" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
hsCode
parsePragma :: CompilerPragma -> Either String HaskellPragma
parsePragma :: CompilerPragma -> Either [Char] HaskellPragma
parsePragma (CompilerPragma Range
r [Char]
s) =
case [ HaskellPragma
p | (HaskellPragma
p, [Char]
"") <- ReadP HaskellPragma -> ReadS HaskellPragma
forall a. ReadP a -> ReadS a
readP_to_S ReadP HaskellPragma
pragmaP [Char]
s ] of
[] -> [Char] -> Either [Char] HaskellPragma
forall a b. a -> Either a b
Left ([Char] -> Either [Char] HaskellPragma)
-> [Char] -> Either [Char] HaskellPragma
forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to parse GHC pragma '" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"'"
[HaskellPragma
p] -> HaskellPragma -> Either [Char] HaskellPragma
forall a b. b -> Either a b
Right HaskellPragma
p
[HaskellPragma]
ps -> [Char] -> Either [Char] HaskellPragma
forall a b. a -> Either a b
Left ([Char] -> Either [Char] HaskellPragma)
-> [Char] -> Either [Char] HaskellPragma
forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous parse of pragma '" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"':\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines ((HaskellPragma -> [Char]) -> [HaskellPragma] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map HaskellPragma -> [Char]
forall a. Show a => a -> [Char]
show [HaskellPragma]
ps)
where
pragmaP :: ReadP HaskellPragma
pragmaP :: ReadP HaskellPragma
pragmaP = [ReadP HaskellPragma] -> ReadP HaskellPragma
forall a. [ReadP a] -> ReadP a
choice [ ReadP HaskellPragma
exportP, ReadP HaskellPragma
typeP, ReadP HaskellPragma
dataP, ReadP HaskellPragma
defnP ]
whitespace :: ReadP [Char]
whitespace = ReadP Char -> ReadP [Char]
forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isSpace)
wordsP :: [[Char]] -> ReadP ()
wordsP [] = () -> ReadP ()
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
wordsP ([Char]
w:[[Char]]
ws) = ReadP ()
skipSpaces ReadP () -> ReadP [Char] -> ReadP [Char]
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Char] -> ReadP [Char]
string [Char]
w ReadP [Char] -> ReadP () -> ReadP ()
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [[Char]] -> ReadP ()
wordsP [[Char]]
ws
barP :: ReadP Char
barP = ReadP ()
skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
'|'
isIdent :: Char -> Bool
isIdent Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c ([Char]
"_.':[]" :: String)
isOp :: Char -> Bool
isOp Char
c = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c ([Char]
"()" :: String)
hsIdent :: ReadP [Char]
hsIdent = ([Char], [Char]) -> [Char]
forall a b. (a, b) -> a
fst (([Char], [Char]) -> [Char])
-> ReadP ([Char], [Char]) -> ReadP [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP [Char] -> ReadP ([Char], [Char])
forall a. ReadP a -> ReadP ([Char], a)
gather ([ReadP [Char]] -> ReadP [Char]
forall a. [ReadP a] -> ReadP a
choice
[ [Char] -> ReadP [Char]
string [Char]
"()"
, ReadP Char -> ReadP [Char]
forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isIdent)
, ReadP Char -> ReadP Char -> ReadP [Char] -> ReadP [Char]
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
between (Char -> ReadP Char
char Char
'(') (Char -> ReadP Char
char Char
')') (ReadP Char -> ReadP [Char]
forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isOp))
])
hsCode :: ReadP [Char]
hsCode = ReadP Char -> ReadP [Char]
forall a. ReadP a -> ReadP [a]
many1 ReadP Char
get
paren :: ReadP a -> ReadP a
paren = ReadP Char -> ReadP Char -> ReadP a -> ReadP a
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
between (ReadP ()
skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
'(') (ReadP ()
skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
')')
isPrefixSpaceOf :: [Char] -> [Char] -> Bool
isPrefixSpaceOf [Char]
pre [Char]
s = case [Char] -> [Char] -> Maybe [Char]
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix [Char]
pre [Char]
s of
Just (Char
x:[Char]
_) -> Char -> Bool
isSpace Char
x
Maybe [Char]
_ -> Bool
False
notTypeOrData :: ReadP ()
notTypeOrData = do
s <- ReadP [Char]
look
guard $ not $ any (`isPrefixSpaceOf` s) ["type", "data"]
exportP :: ReadP HaskellPragma
exportP = Range -> [Char] -> HaskellPragma
HsExport Range
r ([Char] -> HaskellPragma)
-> ReadP () -> ReadP ([Char] -> HaskellPragma)
forall a b. a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"as"] ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP ([Char] -> HaskellPragma)
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP HaskellPragma
forall a b. ReadP (a -> b) -> ReadP a -> ReadP b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsIdent ReadP HaskellPragma -> ReadP () -> ReadP HaskellPragma
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
typeP :: ReadP HaskellPragma
typeP = Range -> [Char] -> HaskellPragma
HsType Range
r ([Char] -> HaskellPragma)
-> ReadP () -> ReadP ([Char] -> HaskellPragma)
forall a b. a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"=", [Char]
"type"] ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP ([Char] -> HaskellPragma)
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP HaskellPragma
forall a b. ReadP (a -> b) -> ReadP a -> ReadP b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsCode
dataP :: ReadP HaskellPragma
dataP = Range -> [Char] -> [[Char]] -> HaskellPragma
HsData Range
r ([Char] -> [[Char]] -> HaskellPragma)
-> ReadP () -> ReadP ([Char] -> [[Char]] -> HaskellPragma)
forall a b. a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"=", [Char]
"data"] ReadP ([Char] -> [[Char]] -> HaskellPragma)
-> ReadP [Char] -> ReadP ([Char] -> [[Char]] -> HaskellPragma)
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace ReadP ([Char] -> [[Char]] -> HaskellPragma)
-> ReadP [Char] -> ReadP ([[Char]] -> HaskellPragma)
forall a b. ReadP (a -> b) -> ReadP a -> ReadP b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsIdent ReadP ([[Char]] -> HaskellPragma)
-> ReadP [[Char]] -> ReadP HaskellPragma
forall a b. ReadP (a -> b) -> ReadP a -> ReadP b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
ReadP [[Char]] -> ReadP [[Char]]
forall {a}. ReadP a -> ReadP a
paren (ReadP [Char] -> ReadP Char -> ReadP [[Char]]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy (ReadP ()
skipSpaces ReadP () -> ReadP [Char] -> ReadP [Char]
forall a b. ReadP a -> ReadP b -> ReadP b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP [Char]
hsIdent) ReadP Char
barP) ReadP HaskellPragma -> ReadP () -> ReadP HaskellPragma
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
defnP :: ReadP HaskellPragma
defnP = Range -> [Char] -> HaskellPragma
HsDefn Range
r ([Char] -> HaskellPragma)
-> ReadP () -> ReadP ([Char] -> HaskellPragma)
forall a b. a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"="] ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP ([Char] -> HaskellPragma)
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace ReadP ([Char] -> HaskellPragma)
-> ReadP () -> ReadP ([Char] -> HaskellPragma)
forall a b. ReadP a -> ReadP b -> ReadP a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
notTypeOrData ReadP ([Char] -> HaskellPragma)
-> ReadP [Char] -> ReadP HaskellPragma
forall a b. ReadP (a -> b) -> ReadP a -> ReadP b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsCode
parseHaskellPragma :: (MonadTCError m, MonadTrace m) => CompilerPragma -> m HaskellPragma
parseHaskellPragma :: forall (m :: * -> *).
(MonadTCError m, MonadTrace m) =>
CompilerPragma -> m HaskellPragma
parseHaskellPragma CompilerPragma
p = CompilerPragma -> m HaskellPragma -> m HaskellPragma
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange CompilerPragma
p (m HaskellPragma -> m HaskellPragma)
-> m HaskellPragma -> m HaskellPragma
forall a b. (a -> b) -> a -> b
$
case CompilerPragma -> Either [Char] HaskellPragma
parsePragma CompilerPragma
p of
Left [Char]
err -> [Char] -> m HaskellPragma
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
err
Right HaskellPragma
p -> HaskellPragma -> m HaskellPragma
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return HaskellPragma
p
getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)
getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q = do
pragma <- (CompilerPragma -> TCMT IO HaskellPragma)
-> Maybe CompilerPragma -> TCM (Maybe HaskellPragma)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse CompilerPragma -> TCMT IO HaskellPragma
forall (m :: * -> *).
(MonadTCError m, MonadTrace m) =>
CompilerPragma -> m HaskellPragma
parseHaskellPragma (Maybe CompilerPragma -> TCM (Maybe HaskellPragma))
-> TCMT IO (Maybe CompilerPragma) -> TCM (Maybe HaskellPragma)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Char] -> QName -> TCMT IO (Maybe CompilerPragma)
getUniqueCompilerPragma [Char]
ghcBackendName QName
q
def <- getConstInfo q
setCurrentRange pragma $ pragma <$ sanityCheckPragma def pragma
sanityCheckPragma :: (HasBuiltins m, MonadTCError m, MonadReduce m) => Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, MonadReduce m) =>
Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma Definition
_ Maybe HaskellPragma
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
sanityCheckPragma Definition
def (Just HsDefn{}) =
case Definition -> Defn
theDef Definition
def of
Axiom{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Function{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
AbstractDefn{} -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Datatype{} -> [Char] -> m ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"data"
Record{} -> [Char] -> m ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"record"
Defn
_ -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Haskell definitions can only be given for postulates and functions."
where
recOrDataErr :: [Char] -> m a
recOrDataErr [Char]
which =
TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> TypeError
GenericDocError (Doc -> TypeError) -> Doc -> TypeError
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad COMPILE GHC pragma for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
which [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" type. Use"
, Doc
"{-# COMPILE GHC <Name> = data <HsData> (<HsCon1> | .. | <HsConN>) #-}" ]
sanityCheckPragma Definition
def (Just HsData{}) =
case Definition -> Defn
theDef Definition
def of
Datatype{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Record{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Defn
_ -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Haskell data types can only be given for data or record types."
sanityCheckPragma Definition
def (Just HsType{}) =
case Definition -> Defn
theDef Definition
def of
Axiom{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Datatype{} -> do
nat <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNat
int <- getBuiltinName builtinInteger
bool <- getBuiltinName builtinBool
unless (Just (defName def) `elem` [nat, int, bool]) err
Defn
_ -> m ()
forall {a}. m a
err
where
err :: m a
err = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Haskell types can only be given for postulates."
sanityCheckPragma Definition
def (Just HsExport{}) =
case Definition -> Defn
theDef Definition
def of
Function{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Defn
_ -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Only functions can be exported to Haskell using {-# COMPILE GHC <Name> as <HsName> #-}"
getHaskellConstructor :: QName -> HsCompileM (Maybe HaskellCode)
getHaskellConstructor :: QName -> HsCompileM (Maybe [Char])
getHaskellConstructor QName
c = do
c <- QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
cDef <- theDef <$> getConstInfo c
env <- askGHCEnv
let is QName
c GHCEnv -> Maybe QName
p = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env
case cDef of
Defn
_ | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvTrue -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"True"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvFalse -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"False"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNil -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"[]"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvCons -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"(:)"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNothing -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"Nothing"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvJust -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"Just"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvSharp -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"MAlonzo.RTE.Sharp"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIZero -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"False"
| QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIOne -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> HsCompileM (Maybe [Char]))
-> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"True"
Constructor{conData :: Defn -> QName
conData = QName
d} -> do
mp <- TCM (Maybe HaskellPragma)
-> ReaderT
GHCModuleEnv
(StateT HsCompileState (TCMT IO))
(Maybe HaskellPragma)
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
-> ReaderT
GHCModuleEnv
(StateT HsCompileState (TCMT IO))
(Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ReaderT
GHCModuleEnv
(StateT HsCompileState (TCMT IO))
(Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
d
case mp of
Just (HsData Range
_ [Char]
_ [[Char]]
hsCons) -> do
cons <- Defn -> [QName]
defConstructors (Defn -> [QName]) -> (Definition -> Defn) -> Definition -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> [QName])
-> ReaderT
GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT
GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
return $ Just $ fromMaybe __IMPOSSIBLE__ $ lookup c $ zip cons hsCons
Maybe HaskellPragma
_ -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Char]
forall a. Maybe a
Nothing
Defn
_ -> Maybe [Char] -> HsCompileM (Maybe [Char])
forall a.
a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Char]
forall a. Maybe a
Nothing
foreignHaskell :: Interface -> ([String], [String], [String])
foreignHaskell :: Interface -> ([[Char]], [[Char]], [[Char]])
foreignHaskell = ([Char] -> KindOfForeignCode)
-> [[Char]] -> ([[Char]], [[Char]], [[Char]])
forall a. (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode [Char] -> KindOfForeignCode
classifyForeign
([[Char]] -> ([[Char]], [[Char]], [[Char]]))
-> (Interface -> [[Char]])
-> Interface
-> ([[Char]], [[Char]], [[Char]])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ForeignCode -> [Char]) -> [ForeignCode] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ForeignCode -> [Char]
getCode ([ForeignCode] -> [[Char]])
-> (Interface -> [ForeignCode]) -> Interface -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ForeignCode]
-> (ForeignCodeStack -> [ForeignCode])
-> Maybe ForeignCodeStack
-> [ForeignCode]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ([ForeignCode] -> [ForeignCode]
forall a. [a] -> [a]
reverse ([ForeignCode] -> [ForeignCode])
-> (ForeignCodeStack -> [ForeignCode])
-> ForeignCodeStack
-> [ForeignCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ForeignCodeStack -> [ForeignCode]
getForeignCodeStack) (Maybe ForeignCodeStack -> [ForeignCode])
-> (Interface -> Maybe ForeignCodeStack)
-> Interface
-> [ForeignCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Map [Char] ForeignCodeStack -> Maybe ForeignCodeStack
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
ghcBackendName (Map [Char] ForeignCodeStack -> Maybe ForeignCodeStack)
-> (Interface -> Map [Char] ForeignCodeStack)
-> Interface
-> Maybe ForeignCodeStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Map [Char] ForeignCodeStack
iForeignCode
where getCode :: ForeignCode -> [Char]
getCode (ForeignCode Range
_ [Char]
code) = [Char]
code
data KindOfForeignCode
=
| ForeignImport
| ForeignOther
classifyForeign :: String -> KindOfForeignCode
classifyForeign :: [Char] -> KindOfForeignCode
classifyForeign [Char]
s0 = case ShowS
ltrim [Char]
s0 of
[Char]
s | [Char]
"import " [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s -> KindOfForeignCode
ForeignImport
[Char]
s | [Char]
"{-#" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s -> [Char] -> KindOfForeignCode
classifyPragma ([Char] -> KindOfForeignCode) -> [Char] -> KindOfForeignCode
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 [Char]
s
[Char]
_ -> KindOfForeignCode
ForeignOther
classifyPragma :: String -> KindOfForeignCode
classifyPragma :: [Char] -> KindOfForeignCode
classifyPragma [Char]
s0 = case ShowS
ltrim [Char]
s0 of
[Char]
s | ([Char] -> Bool) -> [[Char]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s) [[Char]]
fileHeaderPragmas -> KindOfForeignCode
ForeignFileHeaderPragma
[Char]
_ -> KindOfForeignCode
ForeignOther
where
fileHeaderPragmas :: [[Char]]
fileHeaderPragmas =
[ [Char]
"LANGUAGE"
, [Char]
"OPTIONS_GHC"
, [Char]
"INCLUDE"
]
partitionByKindOfForeignCode :: (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode :: forall a. (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode a -> KindOfForeignCode
f = (a -> Three) -> [a] -> ([a], [a], [a])
forall a. (a -> Three) -> [a] -> ([a], [a], [a])
partition3 ((a -> Three) -> [a] -> ([a], [a], [a]))
-> (a -> Three) -> [a] -> ([a], [a], [a])
forall a b. (a -> b) -> a -> b
$ KindOfForeignCode -> Three
toThree (KindOfForeignCode -> Three)
-> (a -> KindOfForeignCode) -> a -> Three
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> KindOfForeignCode
f
where
toThree :: KindOfForeignCode -> Three
toThree = \case
KindOfForeignCode
ForeignFileHeaderPragma -> Three
One
KindOfForeignCode
ForeignImport -> Three
Two
KindOfForeignCode
ForeignOther -> Three
Three