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