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.Utils.Pretty hiding (char)
import Agda.Utils.String ( ltrim )
import Agda.Utils.Three

import Agda.Compiler.Common
import Agda.Compiler.MAlonzo.Misc

import Agda.Utils.Impossible

type HaskellCode = String
type HaskellType = String

-- | GHC backend translation pragmas.
data HaskellPragma
  = HsDefn Range HaskellCode
      --  ^ @COMPILE GHC x = <code>@
  | HsType Range HaskellType
      --  ^ @COMPILE GHC X = type <type>@
  | HsData Range HaskellType [HaskellCode]
      -- ^ @COMPILE GHC X = data D (c₁ | ... | cₙ)
  | HsExport Range HaskellCode
      -- ^ @COMPILE GHC x as f@
  deriving (Int -> HaskellPragma -> ShowS
[HaskellPragma] -> ShowS
HaskellPragma -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [HaskellPragma] -> ShowS
$cshowList :: [HaskellPragma] -> ShowS
show :: HaskellPragma -> [Char]
$cshow :: HaskellPragma -> [Char]
showsPrec :: Int -> HaskellPragma -> ShowS
$cshowsPrec :: Int -> HaskellPragma -> ShowS
Show, HaskellPragma -> HaskellPragma -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HaskellPragma -> HaskellPragma -> Bool
$c/= :: HaskellPragma -> HaskellPragma -> Bool
== :: HaskellPragma -> HaskellPragma -> Bool
$c== :: 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
<+> [Char] -> Doc
text [Char]
hsCode
    HsType   Range
_r [Char]
hsType        -> Doc
equals Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
hsType
    HsData   Range
_r [Char]
hsType [[Char]]
hsCons -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$
      [ Doc
equals, Doc
"data", [Char] -> Doc
text [Char]
hsType
      , Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
List.intersperse [Char]
"|" [[Char]]
hsCons
      ]
    HsExport Range
_r [Char]
hsCode        -> Doc
"as" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
hsCode

-- Syntax for Haskell pragmas:
--  HsDefn CODE       "= CODE"
--  HsType TYPE       "= type TYPE"
--  HsData NAME CONS  "= data NAME (CON₁ | .. | CONₙ)"
--  HsExport NAME     "as NAME"
parsePragma :: CompilerPragma -> Either String HaskellPragma
parsePragma :: CompilerPragma -> Either [Char] HaskellPragma
parsePragma (CompilerPragma Range
r [Char]
s) =
  case [ HaskellPragma
p | (HaskellPragma
p, [Char]
"") <- forall a. ReadP a -> ReadS a
readP_to_S ReadP HaskellPragma
pragmaP [Char]
s ] of
    []  -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to parse GHC pragma '" forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
"'"
    [HaskellPragma
p] -> forall a b. b -> Either a b
Right HaskellPragma
p
    [HaskellPragma]
ps  -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous parse of pragma '" forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
"':\n" forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [HaskellPragma]
ps)  -- shouldn't happen
  where
    pragmaP :: ReadP HaskellPragma
    pragmaP :: ReadP HaskellPragma
pragmaP = forall a. [ReadP a] -> ReadP a
choice [ ReadP HaskellPragma
exportP, ReadP HaskellPragma
typeP, ReadP HaskellPragma
dataP, ReadP HaskellPragma
defnP ]

    whitespace :: ReadP [Char]
whitespace = forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isSpace)

    wordsP :: [[Char]] -> ReadP ()
wordsP []     = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    wordsP ([Char]
w:[[Char]]
ws) = ReadP ()
skipSpaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Char] -> ReadP [Char]
string [Char]
w forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [[Char]] -> ReadP ()
wordsP [[Char]]
ws

    barP :: ReadP Char
barP = ReadP ()
skipSpaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
'|'

    -- quite liberal
    isIdent :: Char -> Bool
isIdent Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> 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 forall a b. (a -> b) -> a -> b
$ Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c ([Char]
"()" :: String)
    hsIdent :: ReadP [Char]
hsIdent = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ReadP a -> ReadP ([Char], a)
gather (forall a. [ReadP a] -> ReadP a
choice
                [ [Char] -> ReadP [Char]
string [Char]
"()"
                , forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isIdent)
                , forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
between (Char -> ReadP Char
char Char
'(') (Char -> ReadP Char
char Char
')') (forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isOp))
                ])
    hsCode :: ReadP [Char]
hsCode  = forall a. ReadP a -> ReadP [a]
many1 ReadP Char
get -- very liberal

    paren :: ReadP a -> ReadP a
paren = forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
between (ReadP ()
skipSpaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
'(') (ReadP ()
skipSpaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
')')

    notTypeOrData :: ReadP ()
notTypeOrData = do
      [Char]
s <- ReadP [Char]
look
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s) [[Char]
"type", [Char]
"data"]

    exportP :: ReadP HaskellPragma
exportP = Range -> [Char] -> HaskellPragma
HsExport Range
r forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"as"]        forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsIdent forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
    typeP :: ReadP HaskellPragma
typeP   = Range -> [Char] -> HaskellPragma
HsType   Range
r forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"=", [Char]
"type"] forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"=", [Char]
"data"] forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP [Char]
hsIdent forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                                    forall {a}. ReadP a -> ReadP a
paren (forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy (ReadP ()
skipSpaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP [Char]
hsIdent) ReadP Char
barP) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
    defnP :: ReadP HaskellPragma
defnP   = Range -> [Char] -> HaskellPragma
HsDefn   Range
r forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [[Char]] -> ReadP ()
wordsP [[Char]
"="]         forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP [Char]
whitespace forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*  ReadP ()
notTypeOrData 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 = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange CompilerPragma
p forall a b. (a -> b) -> a -> b
$
  case CompilerPragma -> Either [Char] HaskellPragma
parsePragma CompilerPragma
p of
    Left [Char]
err -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
err
    Right HaskellPragma
p  -> 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
  Maybe HaskellPragma
pragma <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadTCError m, MonadTrace m) =>
CompilerPragma -> m HaskellPragma
parseHaskellPragma forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Char] -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma [Char]
ghcBackendName QName
q
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Maybe HaskellPragma
pragma forall a b. (a -> b) -> a -> b
$ Maybe HaskellPragma
pragma forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, MonadReduce m) =>
Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma Definition
def Maybe HaskellPragma
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 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
sanityCheckPragma Definition
def (Just HsDefn{}) =
  case Definition -> Defn
theDef Definition
def of
    Axiom{}        -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Function{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbstractDefn{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Datatype{}     -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"data"
    Record{}       -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"record"
    Defn
_              -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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 =
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Doc -> TypeError
GenericDocError forall a b. (a -> b) -> a -> b
$
          forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Bad COMPILE GHC pragma for " forall a. [a] -> [a] -> [a]
++ [Char]
which 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Record{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_          -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Datatype{} -> do
      -- We use HsType pragmas for Nat, Int and Bool
      Maybe QName
nat  <- forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinNat
      Maybe QName
int  <- forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinInteger
      Maybe QName
bool <- forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinBool
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
nat, Maybe QName
int, Maybe QName
bool]) forall {a}. m a
err
    Defn
_ -> forall {a}. m a
err
  where
    err :: m a
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Only functions can be exported to Haskell using {-# COMPILE GHC <Name> as <HsName> #-}"



-- TODO: cache this to avoid parsing the pragma for every constructor
--       occurrence!
getHaskellConstructor :: QName -> HsCompileM (Maybe HaskellCode)
getHaskellConstructor :: QName -> HsCompileM (Maybe [Char])
getHaskellConstructor QName
c = do
  QName
c    <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  Defn
cDef <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  GHCEnv
env  <- forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
is QName
c GHCEnv -> Maybe QName
p = forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env
  case Defn
cDef of
    Defn
_ | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvTrue    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"True"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvFalse   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"False"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNil     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"[]"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvCons    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"(:)"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"Nothing"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvJust    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"Just"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvSharp   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"MAlonzo.RTE.Sharp"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIZero   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"False"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIOne    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"True"
    Constructor{conData :: Defn -> QName
conData = QName
d} -> do
      Maybe HaskellPragma
mp <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
d
      case Maybe HaskellPragma
mp of
        Just (HsData Range
_ [Char]
_ [[Char]]
hsCons) -> do
          [QName]
cons <- Defn -> [QName]
defConstructors forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
c forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [QName]
cons [[Char]]
hsCons
        Maybe HaskellPragma
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- | Get content of @FOREIGN GHC@ pragmas, sorted by 'KindOfForeignCode':
--   file header pragmas, import statements, rest.
foreignHaskell :: Interface -> ([String], [String], [String])
foreignHaskell :: Interface -> ([[Char]], [[Char]], [[Char]])
foreignHaskell = forall a. (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode [Char] -> KindOfForeignCode
classifyForeign
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ForeignCode -> [Char]
getCode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
ghcBackendName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Map [Char] [ForeignCode]
iForeignCode
  where getCode :: ForeignCode -> [Char]
getCode (ForeignCode Range
_ [Char]
code) = [Char]
code

-- | Classify @FOREIGN@ Haskell code.
data KindOfForeignCode
  = ForeignFileHeaderPragma
      -- ^ A pragma that must appear before the module header.
  | ForeignImport
      -- ^ An import statement.  Must appear right after the module header.
  | ForeignOther
      -- ^ The rest.  To appear after the import statements.

-- | Classify a @FOREIGN GHC@ declaration.
classifyForeign :: String -> KindOfForeignCode
classifyForeign :: [Char] -> KindOfForeignCode
classifyForeign [Char]
s0 = case ShowS
ltrim [Char]
s0 of
  [Char]
s | [Char]
"import " forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s -> KindOfForeignCode
ForeignImport
  [Char]
s | [Char]
"{-#" forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` [Char]
s -> [Char] -> KindOfForeignCode
classifyPragma forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
3 [Char]
s
  [Char]
_ -> KindOfForeignCode
ForeignOther

-- | Classify a Haskell pragma into whether it is a file header pragma or not.
classifyPragma :: String -> KindOfForeignCode
classifyPragma :: [Char] -> KindOfForeignCode
classifyPragma [Char]
s0 = case ShowS
ltrim [Char]
s0 of
  [Char]
s | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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"
    ]

-- | Partition a list by 'KindOfForeignCode' attribute.
partitionByKindOfForeignCode :: (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode :: forall a. (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode a -> KindOfForeignCode
f = forall a. (a -> Three) -> [a] -> ([a], [a], [a])
partition3 forall a b. (a -> b) -> a -> b
$ KindOfForeignCode -> Three
toThree 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