module Agda.Compiler.MAlonzo.Pragmas where

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

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

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

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

import Agda.Utils.Impossible

type HaskellCode = String
type HaskellType = String

-- | GHC backend translation pragmas.
data HaskellPragma
  = HsDefn Range HaskellCode
      --  ^ @COMPILE GHC x = <code>@
  | HsType Range HaskellType
      --  ^ @COMPILE GHC X = type <type>@
  | HsData Range HaskellType [HaskellCode]
      -- ^ @COMPILE GHC X = data D (c₁ | ... | cₙ)
  | HsExport Range HaskellCode
      -- ^ @COMPILE GHC x as f@
  deriving (Int -> HaskellPragma -> ShowS
[HaskellPragma] -> ShowS
HaskellPragma -> [Char]
(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
<+> [Char] -> Doc
text [Char]
hsCode
    HsType   Range
_r [Char]
hsType        -> Doc
equals Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
hsType
    HsData   Range
_r [Char]
hsType [[Char]]
hsCons -> [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
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
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
<+> [Char] -> Doc
text [Char]
hsCode

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

    notTypeOrData :: ReadP ()
notTypeOrData = do
      [Char]
s <- ReadP [Char]
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
$ ([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]
"type", [Char]
"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 :: (MonadTCError m, MonadTrace m) => CompilerPragma -> m HaskellPragma
parseHaskellPragma :: forall (m :: * -> *).
(MonadTCError m, MonadTrace m) =>
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 [Char] HaskellPragma
parsePragma CompilerPragma
p of
    Left [Char]
err -> [Char] -> m HaskellPragma
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
err
    Right HaskellPragma
p  -> HaskellPragma -> m HaskellPragma
forall a. a -> m a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe 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
=<< [Char] -> QName -> TCMT IO (Maybe CompilerPragma)
getUniqueCompilerPragma [Char]
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 a b. a -> TCMT IO b -> TCMT IO a
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 :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, MonadReduce m) =>
Definition -> Maybe HaskellPragma -> m ()
sanityCheckPragma Definition
_ Maybe HaskellPragma
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
sanityCheckPragma Definition
def (Just HsDefn{}) =
  case Definition -> Defn
theDef Definition
def of
    Axiom{}        -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Function{}     -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbstractDefn{} -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Datatype{}     -> [Char] -> m ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"data"
    Record{}       -> [Char] -> m ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
recOrDataErr [Char]
"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
$ [Char] -> TypeError
GenericError [Char]
"Haskell definitions can only be given for postulates and functions."
    where
      recOrDataErr :: [Char] -> m a
recOrDataErr [Char]
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 [ [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Bad COMPILE GHC pragma for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
which [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" type. Use"
              , Doc
"{-# COMPILE GHC <Name> = data <HsData> (<HsCon1> | .. | <HsConN>) #-}" ]
sanityCheckPragma Definition
def (Just HsData{}) =
  case Definition -> Defn
theDef Definition
def of
    Datatype{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Record{}   -> () -> m ()
forall a. a -> m a
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
$ [Char] -> TypeError
GenericError [Char]
"Haskell data types can only be given for data or record types."
sanityCheckPragma Definition
def (Just HsType{}) =
  case Definition -> Defn
theDef Definition
def of
    Axiom{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Datatype{} -> do
      -- We use HsType pragmas for Nat, Int and Bool
      Maybe QName
nat  <- [Char] -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinNat
      Maybe QName
int  <- [Char] -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinInteger
      Maybe QName
bool <- [Char] -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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 a. Eq a => a -> [a] -> 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
$ [Char] -> TypeError
GenericError [Char]
"Haskell types can only be given for postulates."
sanityCheckPragma Definition
def (Just HsExport{}) =
  case Definition -> Defn
theDef Definition
def of
    Function{} -> () -> m ()
forall a. a -> m a
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
$ [Char] -> TypeError
GenericError [Char]
"Only functions can be exported to Haskell using {-# COMPILE GHC <Name> as <HsName> #-}"



-- TODO: cache this to avoid parsing the pragma for every constructor
--       occurrence!
getHaskellConstructor :: QName -> HsCompileM (Maybe HaskellCode)
getHaskellConstructor :: QName -> HsCompileM (Maybe [Char])
getHaskellConstructor QName
c = do
  QName
c    <- QName
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
c
  Defn
cDef <- Definition -> Defn
theDef (Definition -> Defn)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
-> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Defn
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
c
  GHCEnv
env  <- ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) 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 [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
      Maybe HaskellPragma
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 Maybe HaskellPragma
mp of
        Just (HsData Range
_ [Char]
_ [[Char]]
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 (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
          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] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ QName -> [(QName, [Char])] -> Maybe [Char]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
c ([(QName, [Char])] -> Maybe [Char])
-> [(QName, [Char])] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [QName] -> [[Char]] -> [(QName, [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [QName]
cons [[Char]]
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] -> 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
. [Char] -> Map [Char] [ForeignCode] -> Maybe [ForeignCode]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
ghcBackendName (Map [Char] [ForeignCode] -> Maybe [ForeignCode])
-> (Interface -> Map [Char] [ForeignCode])
-> Interface
-> Maybe [ForeignCode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Map [Char] [ForeignCode]
iForeignCode
  where getCode :: ForeignCode -> [Char]
getCode (ForeignCode Range
_ [Char]
code) = [Char]
code

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

-- | Classify a @FOREIGN GHC@ declaration.
classifyForeign :: String -> KindOfForeignCode
classifyForeign :: [Char] -> KindOfForeignCode
classifyForeign [Char]
s0 = case ShowS
ltrim [Char]
s0 of
  [Char]
s | [Char]
"import " [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