{-# LANGUAGE CPP #-}

module Agda.Compiler.MAlonzo.Misc where

import Control.Monad.Reader ( ask )
import Control.Monad.State ( modify )
import Control.Monad.Trans ( MonadTrans(lift) )
import Control.Monad.Trans.Except ( ExceptT )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Trans.Maybe ( MaybeT )
import Control.Monad.Trans.Reader ( ReaderT(runReaderT) )
import Control.Monad.Trans.State ( StateT(runStateT) )

import Data.Char
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup
#endif

import qualified Agda.Utils.Haskell.Syntax as HS

import Agda.Compiler.Common

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad

import Agda.Utils.Pretty

import Agda.Utils.Impossible

--------------------------------------------------
-- Setting up Interface before compile
--------------------------------------------------

data HsModuleEnv = HsModuleEnv
  { HsModuleEnv -> ModuleName
mazModuleName :: ModuleName
    -- ^ The name of the Agda module
  , HsModuleEnv -> Bool
mazIsMainModule :: Bool
  -- ^ Whether this is the compilation root and therefore should have the `main` function.
  --   This corresponds to the @IsMain@ flag provided to the backend,
  --   not necessarily whether the GHC module has a `main` function defined.
  }

-- | The options derived from
-- 'Agda.Compiler.MAlonzo.Compiler.GHCFlags' and other shared options.

data GHCOptions = GHCOptions
  { GHCOptions -> Bool
optGhcCallGhc    :: Bool
  , GHCOptions -> FilePath
optGhcBin        :: FilePath
    -- ^ Use the compiler at PATH instead of "ghc"
  , GHCOptions -> [FilePath]
optGhcFlags      :: [String]
  , GHCOptions -> FilePath
optGhcCompileDir :: FilePath
  , GHCOptions -> Bool
optGhcStrictData :: Bool
    -- ^ Make inductive constructors strict?
  , GHCOptions -> Bool
optGhcStrict :: Bool
    -- ^ Make functions strict?
  }

-- | A static part of the GHC backend's environment that does not
-- change from module to module.

data GHCEnv = GHCEnv
  { GHCEnv -> GHCOptions
ghcEnvOpts :: GHCOptions
  , GHCEnv -> Maybe QName
ghcEnvBool
  , GHCEnv -> Maybe QName
ghcEnvTrue
  , GHCEnv -> Maybe QName
ghcEnvFalse
  , GHCEnv -> Maybe QName
ghcEnvMaybe
  , GHCEnv -> Maybe QName
ghcEnvNothing
  , GHCEnv -> Maybe QName
ghcEnvJust
  , GHCEnv -> Maybe QName
ghcEnvList
  , GHCEnv -> Maybe QName
ghcEnvNil
  , GHCEnv -> Maybe QName
ghcEnvCons
  , GHCEnv -> Maybe QName
ghcEnvNat
  , GHCEnv -> Maybe QName
ghcEnvInteger
  , GHCEnv -> Maybe QName
ghcEnvWord64
  , GHCEnv -> Maybe QName
ghcEnvInf
  , GHCEnv -> Maybe QName
ghcEnvSharp
  , GHCEnv -> Maybe QName
ghcEnvFlat
  , GHCEnv -> Maybe QName
ghcEnvInterval
  , GHCEnv -> Maybe QName
ghcEnvIZero
  , GHCEnv -> Maybe QName
ghcEnvIOne
  , GHCEnv -> Maybe QName
ghcEnvIsOne
  , GHCEnv -> Maybe QName
ghcEnvItIsOne
  , GHCEnv -> Maybe QName
ghcEnvIsOne1
  , GHCEnv -> Maybe QName
ghcEnvIsOne2
  , GHCEnv -> Maybe QName
ghcEnvIsOneEmpty
  , GHCEnv -> Maybe QName
ghcEnvPathP
  , GHCEnv -> Maybe QName
ghcEnvSub
  , GHCEnv -> Maybe QName
ghcEnvSubIn
  , GHCEnv -> Maybe QName
ghcEnvId
  , GHCEnv -> Maybe QName
ghcEnvConId
    :: Maybe QName
    -- Various (possibly) builtin names.
  , GHCEnv -> QName -> Bool
ghcEnvIsTCBuiltin :: QName -> Bool
    -- ^ Is the given name a @TC@ builtin (except for @TC@ itself)?
  }

-- | Module compilation environment, bundling the overall
--   backend session options along with the module's basic
--   readable properties.
data GHCModuleEnv = GHCModuleEnv
  { GHCModuleEnv -> GHCEnv
ghcModEnv         :: GHCEnv
  , GHCModuleEnv -> HsModuleEnv
ghcModHsModuleEnv :: HsModuleEnv
  }

-- | Monads that can produce a 'GHCModuleEnv'.
class Monad m => ReadGHCModuleEnv m where
  askGHCModuleEnv :: m GHCModuleEnv

  default askGHCModuleEnv
    :: (MonadTrans t, Monad n, m ~ (t n), ReadGHCModuleEnv n)
    => m GHCModuleEnv
  askGHCModuleEnv = n GHCModuleEnv -> t n GHCModuleEnv
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv

  askHsModuleEnv :: m HsModuleEnv
  askHsModuleEnv = GHCModuleEnv -> HsModuleEnv
ghcModHsModuleEnv (GHCModuleEnv -> HsModuleEnv) -> m GHCModuleEnv -> m HsModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv

  askGHCEnv :: m GHCEnv
  askGHCEnv = GHCModuleEnv -> GHCEnv
ghcModEnv (GHCModuleEnv -> GHCEnv) -> m GHCModuleEnv -> m GHCEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
askGHCModuleEnv

instance Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) where
  askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv
askGHCModuleEnv = ReaderT GHCModuleEnv m GHCModuleEnv
forall r (m :: * -> *). MonadReader r m => m r
ask

instance ReadGHCModuleEnv m => ReadGHCModuleEnv (ExceptT e m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (IdentityT m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (MaybeT m)
instance ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m)

newtype HsCompileState = HsCompileState
  { HsCompileState -> Set ModuleName
mazAccumlatedImports :: Set ModuleName
  } deriving (HsCompileState -> HsCompileState -> Bool
(HsCompileState -> HsCompileState -> Bool)
-> (HsCompileState -> HsCompileState -> Bool) -> Eq HsCompileState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HsCompileState -> HsCompileState -> Bool
$c/= :: HsCompileState -> HsCompileState -> Bool
== :: HsCompileState -> HsCompileState -> Bool
$c== :: HsCompileState -> HsCompileState -> Bool
Eq, b -> HsCompileState -> HsCompileState
NonEmpty HsCompileState -> HsCompileState
HsCompileState -> HsCompileState -> HsCompileState
(HsCompileState -> HsCompileState -> HsCompileState)
-> (NonEmpty HsCompileState -> HsCompileState)
-> (forall b. Integral b => b -> HsCompileState -> HsCompileState)
-> Semigroup HsCompileState
forall b. Integral b => b -> HsCompileState -> HsCompileState
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> HsCompileState -> HsCompileState
$cstimes :: forall b. Integral b => b -> HsCompileState -> HsCompileState
sconcat :: NonEmpty HsCompileState -> HsCompileState
$csconcat :: NonEmpty HsCompileState -> HsCompileState
<> :: HsCompileState -> HsCompileState -> HsCompileState
$c<> :: HsCompileState -> HsCompileState -> HsCompileState
Semigroup, Semigroup HsCompileState
HsCompileState
Semigroup HsCompileState
-> HsCompileState
-> (HsCompileState -> HsCompileState -> HsCompileState)
-> ([HsCompileState] -> HsCompileState)
-> Monoid HsCompileState
[HsCompileState] -> HsCompileState
HsCompileState -> HsCompileState -> HsCompileState
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [HsCompileState] -> HsCompileState
$cmconcat :: [HsCompileState] -> HsCompileState
mappend :: HsCompileState -> HsCompileState -> HsCompileState
$cmappend :: HsCompileState -> HsCompileState -> HsCompileState
mempty :: HsCompileState
$cmempty :: HsCompileState
$cp1Monoid :: Semigroup HsCompileState
Monoid)

-- | Transformer adding read-only module info and a writable set of imported modules
type HsCompileT m = ReaderT GHCModuleEnv (StateT HsCompileState m)

-- | The default compilation monad is the entire TCM (☹️) enriched with our state and module info
type HsCompileM = HsCompileT TCM

runHsCompileT' :: HsCompileT m a -> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' :: HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' HsCompileT m a
t GHCModuleEnv
e HsCompileState
s = ((StateT HsCompileState m a
 -> HsCompileState -> m (a, HsCompileState))
-> HsCompileState
-> StateT HsCompileState m a
-> m (a, HsCompileState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT HsCompileState m a
-> HsCompileState -> m (a, HsCompileState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT HsCompileState
s) (StateT HsCompileState m a -> m (a, HsCompileState))
-> (HsCompileT m a -> StateT HsCompileState m a)
-> HsCompileT m a
-> m (a, HsCompileState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HsCompileT m a -> GHCModuleEnv -> StateT HsCompileState m a)
-> GHCModuleEnv -> HsCompileT m a -> StateT HsCompileState m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip HsCompileT m a -> GHCModuleEnv -> StateT HsCompileState m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT GHCModuleEnv
e) (HsCompileT m a -> m (a, HsCompileState))
-> HsCompileT m a -> m (a, HsCompileState)
forall a b. (a -> b) -> a -> b
$ HsCompileT m a
t

runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
runHsCompileT HsCompileT m a
t GHCModuleEnv
e = HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
forall (m :: * -> *) a.
HsCompileT m a
-> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
runHsCompileT' HsCompileT m a
t GHCModuleEnv
e HsCompileState
forall a. Monoid a => a
mempty

--------------------------------------------------
-- utilities for haskell names
--------------------------------------------------

-- | Whether the current module is expected to have the `main` function.
--   This corresponds to the @IsMain@ flag provided to the backend,
--   not necessarily whether the GHC module actually has a `main` function defined.
curIsMainModule :: ReadGHCModuleEnv m => m Bool
curIsMainModule :: m Bool
curIsMainModule = HsModuleEnv -> Bool
mazIsMainModule (HsModuleEnv -> Bool) -> m HsModuleEnv -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m HsModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m HsModuleEnv
askHsModuleEnv

-- | This is the same value as @curMName@, but does not rely on the TCM's state.
--   (@curMName@ and co. should be removed, but the current @Backend@ interface
--   is not sufficient yet to allow that)
curAgdaMod :: ReadGHCModuleEnv m => m ModuleName
curAgdaMod :: m ModuleName
curAgdaMod = HsModuleEnv -> ModuleName
mazModuleName (HsModuleEnv -> ModuleName) -> m HsModuleEnv -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m HsModuleEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m HsModuleEnv
askHsModuleEnv

-- | Get the Haskell module name of the currently-focused Agda module
curHsMod :: ReadGHCModuleEnv m => m HS.ModuleName
curHsMod :: m ModuleName
curHsMod = ModuleName -> ModuleName
mazMod (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ModuleName
forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
curAgdaMod

-- | There are two kinds of functions: those definitely without unused
-- arguments, and those that might have unused arguments.

data FunctionKind = NoUnused | PossiblyUnused

-- | Different kinds of variables: those starting with @a@, those
-- starting with @v@, and those starting with @x@.

data VariableKind = A | V | X

-- | Different kinds of names.

data NameKind
  = TypeK
    -- ^ Types.
  | ConK
    -- ^ Constructors.
  | VarK VariableKind
    -- ^ Variables.
  | CoverK
    -- ^ Used for coverage checking.
  | CheckK
    -- ^ Used for constructor type checking.
  | FunK FunctionKind
    -- ^ Other functions.

-- | Turns strings into valid Haskell identifiers.
--
-- In order to avoid clashes with names of regular Haskell definitions
-- (those not generated from Agda definitions), make sure that the
-- Haskell names are always used qualified, with the exception of
-- names from the prelude.

encodeString :: NameKind -> String -> String
encodeString :: NameKind -> FilePath -> FilePath
encodeString NameKind
k FilePath
s = FilePath
prefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Char -> FilePath) -> FilePath -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> FilePath
encode FilePath
s
  where
  encode :: Char -> FilePath
encode Char
'\'' = FilePath
"''"
  encode Char
c
    | Char -> Bool
isLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
||
      Char -> GeneralCategory
generalCategory Char
c GeneralCategory -> GeneralCategory -> Bool
forall a. Eq a => a -> a -> Bool
== GeneralCategory
DecimalNumber =
      [Char
c]
    | Bool
otherwise =
      FilePath
"'" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'"

  prefix :: FilePath
prefix = case NameKind
k of
    NameKind
TypeK               -> FilePath
"T"
    NameKind
ConK                -> FilePath
"C"
    VarK VariableKind
A              -> FilePath
"a"
    VarK VariableKind
V              -> FilePath
"v"
    VarK VariableKind
X              -> FilePath
"x"
    NameKind
CoverK              -> FilePath
"cover"
    NameKind
CheckK              -> FilePath
"check"
    FunK FunctionKind
NoUnused       -> FilePath
"du"
    FunK FunctionKind
PossiblyUnused -> FilePath
"d"

ihname :: VariableKind -> Nat -> HS.Name
ihname :: VariableKind -> Int -> Name
ihname VariableKind
k Int
i = FilePath -> Name
HS.Ident (FilePath -> Name) -> FilePath -> Name
forall a b. (a -> b) -> a -> b
$ NameKind -> FilePath -> FilePath
encodeString (VariableKind -> NameKind
VarK VariableKind
k) (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i)

unqhname :: NameKind -> QName -> HS.Name
unqhname :: NameKind -> QName -> Name
unqhname NameKind
k QName
q =
  FilePath -> Name
HS.Ident (FilePath -> Name) -> FilePath -> Name
forall a b. (a -> b) -> a -> b
$ NameKind -> FilePath -> FilePath
encodeString NameKind
k (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$
    FilePath
"_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow (Name -> Name
nameCanonical Name
n) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ NameId -> FilePath
idnum (Name -> NameId
nameId Name
n)
  where
  n :: Name
n = QName -> Name
qnameName QName
q

  idnum :: NameId -> FilePath
idnum (NameId Word64
x ModuleNameHash
_) = Integer -> FilePath
forall a. Show a => a -> FilePath
show (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x)

-- the toplevel module containing the given one
tlmodOf :: ReadTCState m => ModuleName -> m HS.ModuleName
tlmodOf :: ModuleName -> m ModuleName
tlmodOf = (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModuleName -> ModuleName
mazMod (m ModuleName -> m ModuleName)
-> (ModuleName -> m ModuleName) -> ModuleName -> m ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> m ModuleName
forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
topLevelModuleName


-- qualify HS.Name n by the module of QName q, if necessary;
-- accumulates the used module in stImportedModules at the same time.
xqual :: QName -> HS.Name -> HsCompileM HS.QName
xqual :: QName -> Name -> HsCompileM QName
xqual QName
q Name
n = do
  ModuleName
m1 <- ModuleName
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ModuleName
forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
topLevelModuleName (QName -> ModuleName
qnameModule QName
q)
  ModuleName
m2 <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) ModuleName
forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
curAgdaMod
  if ModuleName
m1 ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
m2
    then QName -> HsCompileM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> QName
HS.UnQual Name
n)
    else do
      (HsCompileState -> HsCompileState)
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Set ModuleName -> HsCompileState
HsCompileState (Set ModuleName -> HsCompileState)
-> (HsCompileState -> Set ModuleName)
-> HsCompileState
-> HsCompileState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => a -> Set a -> Set a
Set.insert ModuleName
m1 (Set ModuleName -> Set ModuleName)
-> (HsCompileState -> Set ModuleName)
-> HsCompileState
-> Set ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsCompileState -> Set ModuleName
mazAccumlatedImports)
      QName -> HsCompileM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> Name -> QName
HS.Qual (ModuleName -> ModuleName
mazMod ModuleName
m1) Name
n)

xhqn :: NameKind -> QName -> HsCompileM HS.QName
xhqn :: NameKind -> QName -> HsCompileM QName
xhqn NameKind
k QName
q = QName -> Name -> HsCompileM QName
xqual QName
q (NameKind -> QName -> Name
unqhname NameKind
k QName
q)

hsName :: String -> HS.QName
hsName :: FilePath -> QName
hsName FilePath
s = Name -> QName
HS.UnQual (FilePath -> Name
HS.Ident FilePath
s)

-- always use the original name for a constructor even when it's redefined.
conhqn :: QName -> HsCompileM HS.QName
conhqn :: QName -> HsCompileM QName
conhqn QName
q = NameKind -> QName -> HsCompileM QName
xhqn NameKind
ConK (QName -> HsCompileM QName)
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
-> HsCompileM QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
q

-- qualify name s by the module of builtin b
bltQual :: String -> String -> HsCompileM HS.QName
bltQual :: FilePath -> FilePath -> HsCompileM QName
bltQual FilePath
b FilePath
s = do
  Def QName
q Elims
_ <- FilePath -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
FilePath -> m Term
getBuiltin FilePath
b
  QName -> Name -> HsCompileM QName
xqual QName
q (FilePath -> Name
HS.Ident FilePath
s)

dname :: QName -> HS.Name
dname :: QName -> Name
dname QName
q = NameKind -> QName -> Name
unqhname (FunctionKind -> NameKind
FunK FunctionKind
PossiblyUnused) QName
q

-- | Name for definition stripped of unused arguments
duname :: QName -> HS.Name
duname :: QName -> Name
duname QName
q = NameKind -> QName -> Name
unqhname (FunctionKind -> NameKind
FunK FunctionKind
NoUnused) QName
q

hsPrimOp :: String -> HS.QOp
hsPrimOp :: FilePath -> QOp
hsPrimOp FilePath
s = QName -> QOp
HS.QVarOp (QName -> QOp) -> QName -> QOp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ FilePath -> Name
HS.Symbol FilePath
s

hsPrimOpApp :: String -> HS.Exp -> HS.Exp -> HS.Exp
hsPrimOpApp :: FilePath -> Exp -> Exp -> Exp
hsPrimOpApp FilePath
op Exp
e Exp
e1 = Exp -> QOp -> Exp -> Exp
HS.InfixApp Exp
e (FilePath -> QOp
hsPrimOp FilePath
op) Exp
e1

hsInt :: Integer -> HS.Exp
hsInt :: Integer -> Exp
hsInt Integer
n = Literal -> Exp
HS.Lit (Integer -> Literal
HS.Int Integer
n)

hsTypedInt :: Integral a => a -> HS.Exp
hsTypedInt :: a -> Exp
hsTypedInt a
n = Exp -> Type -> Exp
HS.ExpTypeSig (Literal -> Exp
HS.Lit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n)) (QName -> Type
HS.TyCon (FilePath -> QName
hsName FilePath
"Integer"))

hsTypedDouble :: Real a => a -> HS.Exp
hsTypedDouble :: a -> Exp
hsTypedDouble a
n = Exp -> Type -> Exp
HS.ExpTypeSig (Literal -> Exp
HS.Lit (Rational -> Literal
HS.Frac (Rational -> Literal) -> Rational -> Literal
forall a b. (a -> b) -> a -> b
$ a -> Rational
forall a. Real a => a -> Rational
toRational a
n)) (QName -> Type
HS.TyCon (FilePath -> QName
hsName FilePath
"Double"))

hsLet :: HS.Name -> HS.Exp -> HS.Exp -> HS.Exp
hsLet :: Name -> Exp -> Exp -> Exp
hsLet Name
x Exp
e Exp
b =
  Binds -> Exp -> Exp
HS.Let ([Decl] -> Binds
HS.BDecls [Strictness -> Name -> Rhs -> Decl
HS.LocalBind Strictness
HS.Lazy Name
x (Exp -> Rhs
HS.UnGuardedRhs Exp
e)]) Exp
b

hsVarUQ :: HS.Name -> HS.Exp
hsVarUQ :: Name -> Exp
hsVarUQ = QName -> Exp
HS.Var (QName -> Exp) -> (Name -> QName) -> Name -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
HS.UnQual

hsAppView :: HS.Exp -> [HS.Exp]
hsAppView :: Exp -> [Exp]
hsAppView = [Exp] -> [Exp]
forall a. [a] -> [a]
reverse ([Exp] -> [Exp]) -> (Exp -> [Exp]) -> Exp -> [Exp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> [Exp]
view
  where
    view :: Exp -> [Exp]
view (HS.App Exp
e Exp
e1) = Exp
e1 Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: Exp -> [Exp]
view Exp
e
    view (HS.InfixApp Exp
e1 QOp
op Exp
e2) = [Exp
e2, Exp
e1, QOp -> Exp
hsOpToExp QOp
op]
    view Exp
e = [Exp
e]

hsOpToExp :: HS.QOp -> HS.Exp
hsOpToExp :: QOp -> Exp
hsOpToExp (HS.QVarOp QName
x) = QName -> Exp
HS.Var QName
x

hsLambda :: [HS.Pat] -> HS.Exp -> HS.Exp
hsLambda :: [Pat] -> Exp -> Exp
hsLambda [Pat]
ps (HS.Lambda [Pat]
ps1 Exp
e) = [Pat] -> Exp -> Exp
HS.Lambda ([Pat]
ps [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ [Pat]
ps1) Exp
e
hsLambda [Pat]
ps Exp
e = [Pat] -> Exp -> Exp
HS.Lambda [Pat]
ps Exp
e

hsMapAlt :: (HS.Exp -> HS.Exp) -> HS.Alt -> HS.Alt
hsMapAlt :: (Exp -> Exp) -> Alt -> Alt
hsMapAlt Exp -> Exp
f (HS.Alt Pat
p Rhs
rhs Maybe Binds
wh) = Pat -> Rhs -> Maybe Binds -> Alt
HS.Alt Pat
p ((Exp -> Exp) -> Rhs -> Rhs
hsMapRHS Exp -> Exp
f Rhs
rhs) Maybe Binds
wh

hsMapRHS :: (HS.Exp -> HS.Exp) -> HS.Rhs -> HS.Rhs
hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs
hsMapRHS Exp -> Exp
f (HS.UnGuardedRhs Exp
def) = Exp -> Rhs
HS.UnGuardedRhs (Exp -> Exp
f Exp
def)
hsMapRHS Exp -> Exp
f (HS.GuardedRhss [GuardedRhs]
es)   = [GuardedRhs] -> Rhs
HS.GuardedRhss [ [Stmt] -> Exp -> GuardedRhs
HS.GuardedRhs [Stmt]
g (Exp -> Exp
f Exp
e) | HS.GuardedRhs [Stmt]
g Exp
e <- [GuardedRhs]
es ]

--------------------------------------------------
-- Hard coded module names
--------------------------------------------------

mazstr :: String
mazstr :: FilePath
mazstr = FilePath
"MAlonzo.Code"

mazName :: Name
mazName :: Name
mazName = NameId -> FilePath -> Name
forall a. MkName a => NameId -> a -> Name
mkName_ NameId
forall a. HasCallStack => a
__IMPOSSIBLE__ FilePath
mazstr

mazMod' :: String -> HS.ModuleName
mazMod' :: FilePath -> ModuleName
mazMod' FilePath
s = FilePath -> ModuleName
HS.ModuleName (FilePath -> ModuleName) -> FilePath -> ModuleName
forall a b. (a -> b) -> a -> b
$ FilePath
mazstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s

mazMod :: ModuleName -> HS.ModuleName
mazMod :: ModuleName -> ModuleName
mazMod = FilePath -> ModuleName
mazMod' (FilePath -> ModuleName)
-> (ModuleName -> FilePath) -> ModuleName -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow

mazCoerceName :: String
mazCoerceName :: FilePath
mazCoerceName = FilePath
"coe"

mazErasedName :: String
mazErasedName :: FilePath
mazErasedName = FilePath
"erased"

mazAnyTypeName :: String
mazAnyTypeName :: FilePath
mazAnyTypeName = FilePath
"AgdaAny"

mazCoerce :: HS.Exp
-- mazCoerce = HS.Var $ HS.Qual unsafeCoerceMod (HS.Ident "unsafeCoerce")
-- mazCoerce = HS.Var $ HS.Qual mazRTE $ HS.Ident mazCoerceName
mazCoerce :: Exp
mazCoerce = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ FilePath -> Name
HS.Ident FilePath
mazCoerceName

mazUnreachableError :: HS.Exp
mazUnreachableError :: Exp
mazUnreachableError = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ FilePath -> Name
HS.Ident FilePath
"mazUnreachableError"

rtmUnreachableError :: HS.Exp
rtmUnreachableError :: Exp
rtmUnreachableError = Exp
mazUnreachableError

mazHole :: HS.Exp
mazHole :: Exp
mazHole = QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ FilePath -> Name
HS.Ident FilePath
"mazHole"

rtmHole :: String -> HS.Exp
rtmHole :: FilePath -> Exp
rtmHole FilePath
s = Exp
mazHole Exp -> Exp -> Exp
`HS.App` Literal -> Exp
HS.Lit (Text -> Literal
HS.String (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
T.pack FilePath
s)

mazAnyType :: HS.Type
mazAnyType :: Type
mazAnyType = QName -> Type
HS.TyCon (FilePath -> QName
hsName FilePath
mazAnyTypeName)

mazRTE :: HS.ModuleName
mazRTE :: ModuleName
mazRTE = FilePath -> ModuleName
HS.ModuleName FilePath
"MAlonzo.RTE"

mazRTEFloat :: HS.ModuleName
mazRTEFloat :: ModuleName
mazRTEFloat = FilePath -> ModuleName
HS.ModuleName FilePath
"MAlonzo.RTE.Float"

rtmQual :: String -> HS.QName
rtmQual :: FilePath -> QName
rtmQual = Name -> QName
HS.UnQual (Name -> QName) -> (FilePath -> Name) -> FilePath -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Name
HS.Ident

rtmVar :: String -> HS.Exp
rtmVar :: FilePath -> Exp
rtmVar  = QName -> Exp
HS.Var (QName -> Exp) -> (FilePath -> QName) -> FilePath -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> QName
rtmQual

rtmError :: Text -> HS.Exp
rtmError :: Text -> Exp
rtmError Text
s = FilePath -> Exp
rtmVar FilePath
"error" Exp -> Exp -> Exp
`HS.App`
             Literal -> Exp
HS.Lit (Text -> Literal
HS.String (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"MAlonzo Runtime Error: " Text
s)

unsafeCoerceMod :: HS.ModuleName
unsafeCoerceMod :: ModuleName
unsafeCoerceMod = FilePath -> ModuleName
HS.ModuleName FilePath
"Unsafe.Coerce"

--------------------------------------------------
-- Sloppy ways to declare <name> = <string>
--------------------------------------------------

fakeD :: HS.Name -> String -> HS.Decl
fakeD :: Name -> FilePath -> Decl
fakeD Name
v FilePath
s = [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
v [] (Exp -> Rhs
HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
forall a b. (a -> b) -> a -> b
$ FilePath -> Exp
fakeExp FilePath
s) Maybe Binds
emptyBinds]

fakeDS :: String -> String -> HS.Decl
fakeDS :: FilePath -> FilePath -> Decl
fakeDS = Name -> FilePath -> Decl
fakeD (Name -> FilePath -> Decl)
-> (FilePath -> Name) -> FilePath -> FilePath -> Decl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Name
HS.Ident

fakeDQ :: QName -> String -> HS.Decl
fakeDQ :: QName -> FilePath -> Decl
fakeDQ = Name -> FilePath -> Decl
fakeD (Name -> FilePath -> Decl)
-> (QName -> Name) -> QName -> FilePath -> Decl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
dname

fakeType :: String -> HS.Type
fakeType :: FilePath -> Type
fakeType = FilePath -> Type
HS.FakeType

fakeExp :: String -> HS.Exp
fakeExp :: FilePath -> Exp
fakeExp = FilePath -> Exp
HS.FakeExp

fakeDecl :: String -> HS.Decl
fakeDecl :: FilePath -> Decl
fakeDecl = FilePath -> Decl
HS.FakeDecl

--------------------------------------------------
-- Auxiliary definitions
--------------------------------------------------

emptyBinds :: Maybe HS.Binds
emptyBinds :: Maybe Binds
emptyBinds = Maybe Binds
forall a. Maybe a
Nothing

--------------------------------------------------
-- Utilities for Haskell modules names
--------------------------------------------------

-- | Can the character be used in a Haskell module name part
-- (@conid@)? This function is more restrictive than what the Haskell
-- report allows.

isModChar :: Char -> Bool
isModChar :: Char -> Bool
isModChar Char
c =
  Char -> Bool
isLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\''