{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.MAlonzo.Pragmas where

import Control.Monad.Trans.Maybe

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.Warnings
import Agda.TypeChecking.Primitive

import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.Treeless.Erase (isErasable)

import Agda.Syntax.Common.Pretty hiding (char)
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.String ( ltrim )
import Agda.Utils.Three

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

-- | Retrieve and parse a @COMPILE GHC@ pragma stored for a name.
--
getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)
getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q = MaybeT (TCMT IO) HaskellPragma -> TCM (Maybe HaskellPragma)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
  p <- TCMT IO (Maybe CompilerPragma) -> MaybeT (TCMT IO) CompilerPragma
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe CompilerPragma) -> MaybeT (TCMT IO) CompilerPragma)
-> TCMT IO (Maybe CompilerPragma)
-> MaybeT (TCMT IO) CompilerPragma
forall a b. (a -> b) -> a -> b
$ BackendName -> QName -> TCMT IO (Maybe CompilerPragma)
getUniqueCompilerPragma BackendName
ghcBackendName QName
q
  setCurrentRange p do
    pragma <- MaybeT $ parseHaskellPragma p
    MaybeT $ sanityCheckPragma q pragma

-- Syntax for Haskell pragmas:
--  HsDefn CODE       "= CODE"
--  HsType TYPE       "= type TYPE"
--  HsData NAME CONS  "= data NAME (CON₁ | .. | CONₙ)"
--  HsExport NAME     "as NAME"
parsePragma :: CompilerPragma -> Maybe HaskellPragma
parsePragma :: CompilerPragma -> Maybe 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
    []  -> Maybe HaskellPragma
forall a. Maybe a
Nothing
    [HaskellPragma
p] -> HaskellPragma -> Maybe HaskellPragma
forall a. a -> Maybe a
Just HaskellPragma
p
    [HaskellPragma]
ps  -> -- shouldn't happen
           -- trace ("Ambiguous parse of pragma '" ++ s ++ "':\n" ++ unlines (map show ps)) $
           Maybe HaskellPragma
forall a. HasCallStack => a
__IMPOSSIBLE__
  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
'|'

    -- quite liberal
    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 -- 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 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 :: CompilerPragma -> TCM (Maybe HaskellPragma)
parseHaskellPragma :: CompilerPragma -> TCM (Maybe HaskellPragma)
parseHaskellPragma p :: CompilerPragma
p@(CompilerPragma Range
_ [Char]
s) = do
  let p' :: Maybe HaskellPragma
p' = CompilerPragma -> Maybe HaskellPragma
parsePragma CompilerPragma
p
  () <- Maybe HaskellPragma -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> m () -> m ()
whenNothing Maybe HaskellPragma
p' (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Warning
PragmaCompileUnparsable [Char]
s
  return p'

-- | Check whether the parsed @COMPILE GHC@ pragma matches the kind of identifier it attaches to.
--
sanityCheckPragma :: QName -> HaskellPragma -> TCM (Maybe HaskellPragma)
sanityCheckPragma :: QName -> HaskellPragma -> TCM (Maybe HaskellPragma)
sanityCheckPragma QName
x HaskellPragma
pragma = do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"compile.haskell.pragma" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"sanityCheckPragma" , QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x]
  def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  case pragma of

    HsDefn{} -> case Definition -> Defn
theDef Definition
def of
      Axiom{}        -> TCM (Maybe HaskellPragma)
ok
      Function{}     -> TCM (Maybe HaskellPragma)
functionCheck
      AbstractDefn{} -> TCM (Maybe HaskellPragma)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Datatype{}     -> [Char] -> TCM (Maybe HaskellPragma)
recOrDataErr [Char]
"data"
      Record{}       -> [Char] -> TCM (Maybe HaskellPragma)
recOrDataErr [Char]
"record"
      Defn
_ -> [Char] -> TCM (Maybe HaskellPragma)
bad [Char]
"Haskell definitions can only be given for postulates and functions."

    HsData{} -> case Definition -> Defn
theDef Definition
def of
      Datatype{} -> TCM (Maybe HaskellPragma)
ok
      Record{}   -> TCM (Maybe HaskellPragma)
ok
      Defn
_ -> [Char] -> TCM (Maybe HaskellPragma)
bad [Char]
"Haskell data types can only be given for data or record types."

    HsType{} -> case Definition -> Defn
theDef Definition
def of
      Axiom{}    -> TCM (Maybe HaskellPragma)
ok
      Datatype{} -> do
        -- We use HsType pragmas for Nat, Int and Bool
        TCMT IO Bool
-> TCM (Maybe HaskellPragma)
-> TCM (Maybe HaskellPragma)
-> TCM (Maybe HaskellPragma)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((BuiltinId -> TCMT IO Bool) -> [BuiltinId] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
anyM ((QName -> Maybe QName
forall a. a -> Maybe a
Just (Definition -> QName
defName Definition
def) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool)
-> (BuiltinId -> TCMT IO (Maybe QName))
-> BuiltinId
-> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName) [BuiltinId
builtinNat, BuiltinId
builtinInteger, BuiltinId
builtinBool])
          {-then-} TCM (Maybe HaskellPragma)
ok
          {-else-} TCM (Maybe HaskellPragma)
notPostulate
      Defn
_ -> TCM (Maybe HaskellPragma)
notPostulate

    HsExport{} -> case Definition -> Defn
theDef Definition
def of
      Function{} -> TCM (Maybe HaskellPragma)
functionCheck
      Defn
_ -> [Char] -> TCM (Maybe HaskellPragma)
bad [Char]
"Only functions can be exported to Haskell using {-# COMPILE GHC <Name> as <HsName> #-}"

  where
    ok :: TCM (Maybe HaskellPragma)
ok  = Maybe HaskellPragma -> TCM (Maybe HaskellPragma)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe HaskellPragma -> TCM (Maybe HaskellPragma))
-> Maybe HaskellPragma -> TCM (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ HaskellPragma -> Maybe HaskellPragma
forall a. a -> Maybe a
Just HaskellPragma
pragma
    bad :: [Char] -> TCM (Maybe HaskellPragma)
bad = (Maybe HaskellPragma
forall a. Maybe a
Nothing Maybe HaskellPragma -> TCMT IO () -> TCM (Maybe HaskellPragma)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (TCMT IO () -> TCM (Maybe HaskellPragma))
-> ([Char] -> TCMT IO ()) -> [Char] -> TCM (Maybe HaskellPragma)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> ([Char] -> Warning) -> [Char] -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char] -> Warning
PragmaCompileWrong QName
x
    recOrDataErr :: [Char] -> TCM (Maybe HaskellPragma)
recOrDataErr [Char]
which = [Char] -> TCM (Maybe HaskellPragma)
bad ([Char] -> TCM (Maybe HaskellPragma))
-> [Char] -> TCM (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords
      [ [Char]
"Bad COMPILE GHC pragma for", [Char]
which, [Char]
"type. Use"
      , [Char]
"{-# COMPILE GHC <Name> = data <HsData> (<HsCon1> | .. | <HsConN>) #-}"
      ]
    notPostulate :: TCM (Maybe HaskellPragma)
notPostulate = [Char] -> TCM (Maybe HaskellPragma)
bad [Char]
"Haskell types can only be given for postulates."
    notBuiltinFlat :: TCM (Maybe HaskellPragma)
notBuiltinFlat = do
      mflat <- BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinFlat
      reportSLn "compile.haskell.pragma" 40 $ render $ vcat
        [ "Checking pragma for FLAT"
        , hsep [ "x     =", pretty x ]
        , hsep [ "mflat =", pretty mflat ]
        ]
      if Just x == mflat
        then bad "COMPILE GHC pragmas are not allowed for the FLAT builtin."
        else ok
    notErasable :: TCM (Maybe HaskellPragma)
notErasable = QName -> TCMT IO Bool
isErasable QName
x TCMT IO Bool
-> (Bool -> TCM (Maybe HaskellPragma)) -> TCM (Maybe HaskellPragma)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> Maybe HaskellPragma
forall a. Maybe a
Nothing Maybe HaskellPragma -> TCMT IO () -> TCM (Maybe HaskellPragma)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ BackendName -> QName -> Warning
PragmaCompileErased BackendName
ghcBackendName QName
x
      Bool
False -> TCM (Maybe HaskellPragma)
ok
    functionCheck :: TCM (Maybe HaskellPragma)
functionCheck = MaybeT (TCMT IO) HaskellPragma -> TCM (Maybe HaskellPragma)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
      _ <- TCM (Maybe HaskellPragma) -> MaybeT (TCMT IO) HaskellPragma
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT TCM (Maybe HaskellPragma)
notErasable
      MaybeT notBuiltinFlat

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

-- | 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 = ([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
. BackendName
-> Map BackendName ForeignCodeStack -> Maybe ForeignCodeStack
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BackendName
ghcBackendName (Map BackendName ForeignCodeStack -> Maybe ForeignCodeStack)
-> (Interface -> Map BackendName ForeignCodeStack)
-> Interface
-> Maybe ForeignCodeStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Map BackendName ForeignCodeStack
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 " [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

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

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