module Agda.Compiler.MAlonzo.Pragmas where

import Control.Monad
import Data.Maybe
import Data.Char
import qualified Data.List as List
import qualified Data.Map as Map
import Text.ParserCombinators.ReadP

import Agda.Syntax.Position
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive

import Agda.Utils.Pretty hiding (char)
import Agda.Utils.String ( ltrim )
import Agda.Utils.Three

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

import Agda.Utils.Impossible

type HaskellCode = String
type HaskellType = String

-- | GHC backend translation pragmas.
data HaskellPragma
  = HsDefn Range HaskellCode
      --  ^ @COMPILE GHC x = <code>@
  | HsType Range HaskellType
      --  ^ @COMPILE GHC X = type <type>@
  | HsData Range HaskellType [HaskellCode]
      -- ^ @COMPILE GHC X = data D (c₁ | ... | cₙ)
  | HsExport Range HaskellCode
      -- ^ @COMPILE GHC x as f@
  deriving (Int -> HaskellPragma -> ShowS
[HaskellPragma] -> ShowS
HaskellPragma -> 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
forall (t :: * -> *). Foldable t => t 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
forall (t :: * -> *). Foldable t => t 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 :: (MonadTCError m, MonadTrace m) => CompilerPragma -> m HaskellPragma
parseHaskellPragma :: CompilerPragma -> m HaskellPragma
parseHaskellPragma CompilerPragma
p = CompilerPragma -> m HaskellPragma -> m HaskellPragma
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange CompilerPragma
p (m HaskellPragma -> m HaskellPragma)
-> m HaskellPragma -> m HaskellPragma
forall a b. (a -> b) -> a -> b
$
  case CompilerPragma -> Either String HaskellPragma
parsePragma CompilerPragma
p of
    Left String
err -> String -> m HaskellPragma
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError String
err
    Right HaskellPragma
p  -> HaskellPragma -> m 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 -> TCMT IO HaskellPragma)
-> Maybe CompilerPragma -> TCM (Maybe HaskellPragma)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompilerPragma -> TCMT IO HaskellPragma
forall (m :: * -> *).
(MonadTCError m, MonadTrace m) =>
CompilerPragma -> m HaskellPragma
parseHaskellPragma (Maybe CompilerPragma -> TCM (Maybe HaskellPragma))
-> TCMT IO (Maybe CompilerPragma) -> TCM (Maybe HaskellPragma)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m 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 ()
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, MonadReduce m) =>
Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma Definition
def Maybe HaskellPragma
pragma

sanityCheckPragma :: (HasBuiltins m, MonadTCError m, MonadReduce m) => Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma :: Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma Definition
_ Maybe HaskellPragma
Nothing = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
sanityCheckPragma Definition
def (Just HsDefn{}) =
  case Definition -> Defn
theDef Definition
def of
    Axiom{}        -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Function{}     -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbstractDefn{} -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Datatype{}     -> String -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
recOrDataErr String
"data"
    Record{}       -> String -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
recOrDataErr String
"record"
    Defn
_              -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ 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.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> TypeError
GenericDocError (Doc -> TypeError) -> Doc -> TypeError
forall a b. (a -> b) -> a -> b
$
          [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ 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{} -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Record{}   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_          -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ 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{} -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Datatype{} -> do
      -- We use HsType pragmas for Nat, Int and Bool
      Maybe QName
nat  <- String -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
builtinNat
      Maybe QName
int  <- String -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
builtinInteger
      Maybe QName
bool <- String -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
builtinBool
      Bool -> m () -> m ()
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]) m ()
forall a. m a
err
    Defn
_ -> m ()
forall a. m a
err
  where
    err :: m a
err = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ 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{} -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Defn
_ -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ 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 -> HsCompileM (Maybe HaskellCode)
getHaskellConstructor :: QName -> HsCompileM (Maybe String)
getHaskellConstructor QName
c = do
  QName
c    <- QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  Defn
cDef <- Definition -> Defn
theDef (Definition -> Defn)
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  GHCEnv
env  <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: QName -> (GHCEnv -> Maybe QName) -> Bool
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 Defn
cDef of
    Defn
_ | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvTrue    -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"True"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvFalse   -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"False"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNil     -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"[]"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvCons    -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"(:)"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvNothing -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"Nothing"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvJust    -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"Just"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvSharp   -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"MAlonzo.RTE.Sharp"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIZero   -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"False"
      | QName
c QName -> (GHCEnv -> Maybe QName) -> Bool
`is` GHCEnv -> Maybe QName
ghcEnvIOne    -> Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"True"
    Constructor{conData :: Defn -> QName
conData = QName
d} -> do
      Maybe HaskellPragma
mp <- TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ 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])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          Maybe String -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> HsCompileM (Maybe String))
-> Maybe String -> HsCompileM (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 -> HsCompileM (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
    Defn
_ -> Maybe String -> HsCompileM (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 :: Interface -> ([String], [String], [String])
foreignHaskell :: Interface -> ([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
  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
"import " String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` String
s -> KindOfForeignCode
ForeignImport
  String
s | String
"{-#" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` 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