module Agda.Compiler.MAlonzo.Pragmas where

import Control.Monad
import Data.Maybe
import Data.Char
import qualified Data.List as List
import Data.Traversable (traverse)
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.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 -> String
(Int -> HaskellPragma -> ShowS)
-> (HaskellPragma -> String)
-> ([HaskellPragma] -> ShowS)
-> Show HaskellPragma
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HaskellPragma] -> ShowS
$cshowList :: [HaskellPragma] -> ShowS
show :: HaskellPragma -> String
$cshow :: HaskellPragma -> String
showsPrec :: Int -> HaskellPragma -> ShowS
$cshowsPrec :: Int -> HaskellPragma -> ShowS
Show, HaskellPragma -> HaskellPragma -> Bool
(HaskellPragma -> HaskellPragma -> Bool)
-> (HaskellPragma -> HaskellPragma -> Bool) -> Eq HaskellPragma
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 String
_)   = Range
r
  getRange (HsType   Range
r String
_)   = Range
r
  getRange (HsData   Range
r String
_ [String]
_) = Range
r
  getRange (HsExport Range
r String
_)   = Range
r

instance Pretty HaskellPragma where
  pretty :: HaskellPragma -> Doc
pretty = \case
    HsDefn   Range
_r String
hsCode        -> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text String
hsCode
    HsType   Range
_r String
hsType        -> Doc
equals Doc -> Doc -> Doc
<+> String -> Doc
text String
hsType
    HsData   Range
_r String
hsType [String]
hsCons -> [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ Doc
equals, Doc
"data", String -> Doc
text String
hsType
      , Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
List.intersperse String
"|" [String]
hsCons
      ]
    HsExport Range
_r String
hsCode        -> Doc
"as" Doc -> Doc -> Doc
<+> String -> Doc
text String
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 String HaskellPragma
parsePragma (CompilerPragma Range
r String
s) =
  case [ HaskellPragma
p | (HaskellPragma
p, String
"") <- ReadP HaskellPragma -> ReadS HaskellPragma
forall a. ReadP a -> ReadS a
readP_to_S ReadP HaskellPragma
pragmaP String
s ] of
    []  -> String -> Either String HaskellPragma
forall a b. a -> Either a b
Left (String -> Either String HaskellPragma)
-> String -> Either String HaskellPragma
forall a b. (a -> b) -> a -> b
$ String
"Failed to parse GHC pragma '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
    [HaskellPragma
p] -> HaskellPragma -> Either String HaskellPragma
forall a b. b -> Either a b
Right HaskellPragma
p
    [HaskellPragma]
ps  -> String -> Either String HaskellPragma
forall a b. a -> Either a b
Left (String -> Either String HaskellPragma)
-> String -> Either String HaskellPragma
forall a b. (a -> b) -> a -> b
$ String
"Ambiguous parse of pragma '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"':\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((HaskellPragma -> String) -> [HaskellPragma] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map HaskellPragma -> String
forall a. Show a => a -> String
show [HaskellPragma]
ps)  -- shouldn't happen
  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 String
whitespace = ReadP Char -> ReadP String
forall a. ReadP a -> ReadP [a]
many1 ((Char -> Bool) -> ReadP Char
satisfy Char -> Bool
isSpace)

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

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

    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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
'(') (ReadP ()
skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
char Char
')')

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

    exportP :: ReadP HaskellPragma
exportP = Range -> String -> HaskellPragma
HsExport Range
r (String -> HaskellPragma)
-> ReadP () -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [String] -> ReadP ()
wordsP [String
"as"]        ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP String
whitespace ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP String
hsIdent ReadP HaskellPragma -> ReadP () -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
    typeP :: ReadP HaskellPragma
typeP   = Range -> String -> HaskellPragma
HsType   Range
r (String -> HaskellPragma)
-> ReadP () -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [String] -> ReadP ()
wordsP [String
"=", String
"type"] ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP String
whitespace ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP String
hsCode
    dataP :: ReadP HaskellPragma
dataP   = Range -> String -> [String] -> HaskellPragma
HsData   Range
r (String -> [String] -> HaskellPragma)
-> ReadP () -> ReadP (String -> [String] -> HaskellPragma)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [String] -> ReadP ()
wordsP [String
"=", String
"data"] ReadP (String -> [String] -> HaskellPragma)
-> ReadP String -> ReadP (String -> [String] -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP String
whitespace ReadP (String -> [String] -> HaskellPragma)
-> ReadP String -> ReadP ([String] -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP String
hsIdent ReadP ([String] -> HaskellPragma)
-> ReadP [String] -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                                    ReadP [String] -> ReadP [String]
forall a. ReadP a -> ReadP a
paren (ReadP String -> ReadP Char -> ReadP [String]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy (ReadP ()
skipSpaces ReadP () -> ReadP String -> ReadP String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP String
hsIdent) ReadP Char
barP) ReadP HaskellPragma -> ReadP () -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces
    defnP :: ReadP HaskellPragma
defnP   = Range -> String -> HaskellPragma
HsDefn   Range
r (String -> HaskellPragma)
-> ReadP () -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [String] -> ReadP ()
wordsP [String
"="]         ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP String
whitespace ReadP (String -> HaskellPragma)
-> ReadP () -> ReadP (String -> HaskellPragma)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*  ReadP ()
notTypeOrData ReadP (String -> HaskellPragma)
-> ReadP String -> ReadP HaskellPragma
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP String
hsCode

parseHaskellPragma :: CompilerPragma -> TCM HaskellPragma
parseHaskellPragma :: CompilerPragma -> TCM HaskellPragma
parseHaskellPragma CompilerPragma
p = CompilerPragma -> TCM HaskellPragma -> TCM HaskellPragma
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange CompilerPragma
p (TCM HaskellPragma -> TCM HaskellPragma)
-> TCM HaskellPragma -> TCM HaskellPragma
forall a b. (a -> b) -> a -> b
$
  case CompilerPragma -> Either String HaskellPragma
parsePragma CompilerPragma
p of
    Left String
err -> String -> TCM HaskellPragma
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
err
    Right HaskellPragma
p  -> HaskellPragma -> TCM HaskellPragma
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 <- (CompilerPragma -> TCM HaskellPragma)
-> Maybe CompilerPragma -> TCM (Maybe HaskellPragma)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompilerPragma -> TCM 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
=<< String -> QName -> TCMT IO (Maybe CompilerPragma)
getUniqueCompilerPragma String
ghcBackendName QName
q
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  Maybe HaskellPragma
-> TCM (Maybe HaskellPragma) -> TCM (Maybe HaskellPragma)
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Maybe HaskellPragma
pragma (TCM (Maybe HaskellPragma) -> TCM (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma) -> TCM (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ Maybe HaskellPragma
pragma Maybe HaskellPragma -> TCMT IO () -> TCM (Maybe HaskellPragma)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Definition -> Maybe HaskellPragma -> TCMT IO ()
sanityCheckPragma Definition
def Maybe HaskellPragma
pragma

sanityCheckPragma :: Definition -> Maybe HaskellPragma -> TCM ()
sanityCheckPragma :: Definition -> Maybe HaskellPragma -> TCMT IO ()
sanityCheckPragma Definition
_ Maybe HaskellPragma
Nothing = () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
sanityCheckPragma Definition
def (Just HsDefn{}) =
  case Definition -> Defn
theDef Definition
def of
    Axiom{}        -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Function{}     -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbstractDefn{} -> TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Datatype{}     -> String -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
recOrDataErr String
"data"
    Record{}       -> String -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
recOrDataErr String
"record"
    Defn
_              -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Haskell definitions can only be given for postulates and functions."
    where
      recOrDataErr :: String -> m a
recOrDataErr String
which =
        TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
sep [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Bad COMPILE GHC pragma for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
which String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" type. Use"
              , Doc
"{-# COMPILE GHC <Name> = data <HsData> (<HsCon1> | .. | <HsConN>) #-}" ]
sanityCheckPragma Definition
def (Just HsData{}) =
  case Definition -> Defn
theDef Definition
def of
    Datatype{} -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Record{}   -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_          -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"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{} -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Datatype{} -> do
      -- We use HsType pragmas for Nat, Int and Bool
      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
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (QName -> Maybe QName
forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
nat, Maybe QName
int, Maybe QName
bool]) TCMT IO ()
forall a. TCMT IO a
err
    Defn
_ -> TCMT IO ()
forall a. TCMT IO a
err
  where
    err :: TCMT IO a
err = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Haskell types can only be given for postulates."
sanityCheckPragma Definition
def (Just HsExport{}) =
  case Definition -> Defn
theDef Definition
def of
    Function{} -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_ -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"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 -> TCM (Maybe HaskellCode)
getHaskellConstructor :: QName -> TCM (Maybe String)
getHaskellConstructor QName
c = do
  QName
c     <- QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  Defn
cDef  <- 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
c
  Maybe QName
true  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinTrue
  Maybe QName
false <- String -> TCM (Maybe QName)
getBuiltinName String
builtinFalse
  Maybe QName
nil   <- String -> TCM (Maybe QName)
getBuiltinName String
builtinNil
  Maybe QName
cons  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinCons
  Maybe QName
sharp <- String -> TCM (Maybe QName)
getBuiltinName String
builtinSharp
  case Defn
cDef of
    Defn
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
true  -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"True"
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
false -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"False"
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
nil   -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"[]"
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
cons  -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"(:)"
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
sharp -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"MAlonzo.RTE.Sharp"
    Constructor{conData :: Defn -> QName
conData = QName
d} -> do
      Maybe HaskellPragma
mp <- QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
d
      case Maybe HaskellPragma
mp of
        Just (HsData Range
_ String
_ [String]
hsCons) -> do
          [QName]
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]) -> TCMT IO Definition -> TCMT IO [QName]
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
d
          Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> TCM (Maybe String))
-> Maybe String -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ QName -> [(QName, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
c ([(QName, String)] -> Maybe String)
-> [(QName, String)] -> Maybe String
forall a b. (a -> b) -> a -> b
$ [QName] -> [String] -> [(QName, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [QName]
cons [String]
hsCons
        Maybe HaskellPragma
_ -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
    Defn
_ -> Maybe String -> TCM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing

-- | Get content of @FOREIGN GHC@ pragmas, sorted by 'KindOfForeignCode':
--   file header pragmas, import statements, rest.
foreignHaskell :: TCM ([String], [String], [String])
foreignHaskell :: TCM ([String], [String], [String])
foreignHaskell = (String -> KindOfForeignCode)
-> [String] -> ([String], [String], [String])
forall a. (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode String -> KindOfForeignCode
classifyForeign
    ([String] -> ([String], [String], [String]))
-> (Interface -> [String])
-> Interface
-> ([String], [String], [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ForeignCode -> String) -> [ForeignCode] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ForeignCode -> String
getCode ([ForeignCode] -> [String])
-> (Interface -> [ForeignCode]) -> Interface -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ForeignCode] -> Maybe [ForeignCode] -> [ForeignCode]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [ForeignCode] -> [ForeignCode])
-> (Interface -> Maybe [ForeignCode]) -> Interface -> [ForeignCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map String [ForeignCode] -> Maybe [ForeignCode]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
ghcBackendName (Map String [ForeignCode] -> Maybe [ForeignCode])
-> (Interface -> Map String [ForeignCode])
-> Interface
-> Maybe [ForeignCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Map String [ForeignCode]
iForeignCode (Interface -> ([String], [String], [String]))
-> TCMT IO Interface -> TCM ([String], [String], [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
curIF
  where getCode :: ForeignCode -> String
getCode (ForeignCode Range
_ String
code) = String
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 :: String -> KindOfForeignCode
classifyForeign String
s0 = case ShowS
ltrim String
s0 of
  String
s | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"import " String
s -> KindOfForeignCode
ForeignImport
  String
s | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
"{-#" String
s -> String -> KindOfForeignCode
classifyPragma (String -> KindOfForeignCode) -> String -> KindOfForeignCode
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 String
s
  String
_ -> KindOfForeignCode
ForeignOther

-- | Classify a Haskell pragma into whether it is a file header pragma or not.
classifyPragma :: String -> KindOfForeignCode
classifyPragma :: String -> KindOfForeignCode
classifyPragma String
s0 = case ShowS
ltrim String
s0 of
  String
s | (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` String
s) [String]
fileHeaderPragmas -> KindOfForeignCode
ForeignFileHeaderPragma
  String
_ -> KindOfForeignCode
ForeignOther
  where
  fileHeaderPragmas :: [String]
fileHeaderPragmas =
    [ String
"LANGUAGE"
    , String
"OPTIONS_GHC"
    , String
"INCLUDE"
    ]

-- | Partition a list by 'KindOfForeignCode' attribute.
partitionByKindOfForeignCode :: (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])
partitionByKindOfForeignCode :: (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