{-# LANGUAGE CPP                 #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE PatternGuards       #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Agda.Compiler.MAlonzo.Compiler where

#if __GLASGOW_HASKELL__ <= 708
import Prelude hiding (mapM_, mapM, sequence, concat)
#endif

import Control.Applicative
import Control.Monad.Reader hiding (mapM_, forM_, mapM, forM, sequence)
import Control.Monad.State  hiding (mapM_, forM_, mapM, forM, sequence)

import Data.Generics.Geniplate
import Data.Foldable
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable hiding (for)

import qualified Language.Haskell.Exts.Extension as HS
import qualified Language.Haskell.Exts.Parser as HS
import qualified Language.Haskell.Exts.Pretty as HS
import qualified Language.Haskell.Exts.Syntax as HS

import System.Directory (createDirectoryIfMissing)
import System.FilePath hiding (normalise)

import Agda.Compiler.CallCompiler
import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.MAlonzo.Pretty
import Agda.Compiler.MAlonzo.Primitives

import Agda.Interaction.FindFile
import Agda.Interaction.Imports
import Agda.Interaction.Options

import Agda.Syntax.Common
import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Level (reallyUnLevelView)

import Agda.TypeChecking.CompiledClause

import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.IO.UTF8 as UTF8
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Singleton
import Agda.Utils.Tuple

#include "undefined.h"
import Agda.Utils.Impossible

compilerMain :: Bool -> Interface -> TCM ()
compilerMain modIsMain mainI =
  -- Preserve the state (the compiler modifies the state).
  -- Andreas, 2014-03-23 But we might want to collect Benchmark info,
  -- so use localTCState.
  localTCState $ do

    -- Compute the output directory.
    opts <- commandLineOptions
    compileDir <- case optCompileDir opts of
      Just dir -> return dir
      Nothing  -> do
        -- The default output directory is the project root.
        let tm = toTopLevelModuleName $ iModuleName mainI
        f <- findFile tm
        return $ filePath $ C.projectRoot f tm
    setCommandLineOptions $
      opts { optCompileDir = Just compileDir }

    ignoreAbstractMode $ do
      mapM_ (compile . miInterface) =<< (Map.elems <$> getVisitedModules)
      writeModule rteModule
      callGHC modIsMain mainI

compile :: Interface -> TCM ()
compile i = do
  setInterface i
  ifM uptodate noComp $ {- else -} do
    yesComp
    writeModule =<< decl <$> curHsMod <*> (definitions =<< curDefs) <*> imports
  where
  decl mn ds imp = HS.Module dummy mn [] Nothing Nothing imp ds
  uptodate = liftIO =<< (isNewerThan <$> outFile_ <*> ifile)
  ifile    = maybe __IMPOSSIBLE__ filePath <$>
               (findInterfaceFile . toTopLevelModuleName =<< curMName)
  noComp   = reportSLn "" 1 . (++ " : no compilation is needed.") . show . A.mnameToConcrete =<< curMName
  yesComp  = reportSLn "" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
             sequence [show . A.mnameToConcrete <$> curMName, ifile, outFile_] :: TCM ()

--------------------------------------------------
-- imported modules
--   I use stImportedModules in a non-standard way,
--   accumulating in it what are acutally used in Misc.xqual
--------------------------------------------------

imports :: TCM [HS.ImportDecl]
imports = (++) <$> hsImps <*> imps where
  hsImps :: TCM [HS.ImportDecl]
  hsImps = (List.map decl . Set.toList .
            Set.insert mazRTE . Set.map HS.ModuleName) <$>
             getHaskellImports

  imps :: TCM [HS.ImportDecl]
  imps = List.map decl . uniq <$>
           ((++) <$> importsForPrim <*> (List.map mazMod <$> mnames))

  decl :: HS.ModuleName -> HS.ImportDecl
  decl m = HS.ImportDecl dummy m True False False Nothing Nothing Nothing

  mnames :: TCM [ModuleName]
  mnames = (++) <$> (Set.elems <$> use stImportedModules)
                <*> (List.map fst . iImportedModules <$> curIF)

  uniq :: [HS.ModuleName] -> [HS.ModuleName]
  uniq = List.map head . List.group . List.sort

--------------------------------------------------
-- Main compiling clauses
--------------------------------------------------

definitions :: Definitions -> TCM [HS.Decl]
definitions defs = do
  kit <- coinductionKit
  HMap.foldr (liftM2 (++) . (definition kit <=< instantiateFull))
             declsForPrim defs

-- | Note that the INFINITY, SHARP and FLAT builtins are translated as
-- follows (if a 'CoinductionKit' is given):
--
-- @
--   type Infinity a b = b
--
--   sharp :: a -> a
--   sharp x = x
--
--   flat :: a -> a
--   flat x = x
-- @

definition :: Maybe CoinductionKit -> Definition -> TCM [HS.Decl]
-- ignore irrelevant definitions
{- Andreas, 2012-10-02: Invariant no longer holds
definition kit (Defn Forced{}  _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
definition kit (Defn UnusedArg _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
definition kit (Defn NonStrict _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
-}
definition kit Defn{defArgInfo = info, defName = q} | isIrrelevant info = do
  reportSDoc "malonzo.definition" 10 $
    text "Not compiling" <+> prettyTCM q <> text "."
  return []
definition kit Defn{defName = q, defType = ty, defCompiledRep = compiled, theDef = d} = do
  reportSDoc "malonzo.definition" 10 $ vcat
    [ text "Compiling" <+> prettyTCM q <> text ":"
    , nest 2 $ text (show d)
    ]
  checkTypeOfMain q ty $ do
    (infodecl q :) <$> case d of

      _ | Just (HsDefn ty hs) <- compiledHaskell compiled ->
        return $ fbWithType ty (fakeExp hs)

      -- Special treatment of coinductive builtins.
      Datatype{} | Just q == (nameOfInf <$> kit) -> do
        let infT = unqhname "T" q
            infV = unqhname "d" q
            a    = ihname "a" 0
            b    = ihname "a" 1
            vars = [a, b]
        return [ HS.TypeDecl dummy infT
                             (List.map HS.UnkindedVar vars)
                             (HS.TyVar b)
               , HS.FunBind [HS.Match dummy infV
                                      (List.map HS.PVar vars) Nothing
                                      (HS.UnGuardedRhs HS.unit_con)
                                      emptyBinds]
               ]
      Constructor{} | Just q == (nameOfSharp <$> kit) -> do
        let sharp = unqhname "d" q
            x     = ihname "x" 0
        return $
          [ HS.TypeSig dummy [sharp] $ fakeType $
              "forall a. a -> a"
          , HS.FunBind [HS.Match dummy sharp
                                 [HS.PVar x]
                                 Nothing
                                 (HS.UnGuardedRhs (HS.Var (HS.UnQual x)))
                                 emptyBinds]
          ]
      Function{} | Just q == (nameOfFlat <$> kit) -> do
        let flat = unqhname "d" q
            x    = ihname "x" 0
        return $
          [ HS.TypeSig dummy [flat] $ fakeType $
              "forall a. a -> a"
          , HS.FunBind [HS.Match dummy flat
                                 [HS.PVar x]
                                 Nothing
                                 (HS.UnGuardedRhs (HS.Var (HS.UnQual x)))
                                 emptyBinds]
          ]

      Axiom{} -> return $ fb axiomErr
      Primitive{ primClauses = [], primName = s } -> fb <$> primBody s
      Primitive{ primClauses = cls } -> function Nothing $
        functionFromClauses cls

      -- Currently, catchAllBranches cannot be handled properly by casetree
      Function{ funCompiled = Just cc } | not (hasCatchAll cc) ->
        function (exportHaskell compiled) $ functionFromCaseTree q cc
      Function{ funClauses = cls } ->
        function (exportHaskell compiled) $ functionFromClauses cls

      Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs }
        | Just (HsType ty) <- compiledHaskell compiled -> do
        ccs <- List.concat <$> mapM checkConstructorType cs
        cov <- checkCover q ty np cs
        return $ tvaldecl q (dataInduction d) 0 (np + ni) [] (Just __IMPOSSIBLE__) ++ ccs ++ cov
      Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs } -> do
        (ars, cds) <- unzip <$> mapM condecl cs
        return $ tvaldecl q (dataInduction d) (List.maximum (np:ars) - np) (np + ni) cds cl
      Constructor{} -> return []
      Record{ recClause = cl, recConHead = con, recFields = flds } -> do
        let c = conName con
        let noFields = length flds
        let ar = I.arity ty
        cd <- snd <$> condecl c
  --       cd <- case c of
  --         Nothing -> return $ cdecl q noFields
  --         Just c  -> snd <$> condecl c
        return $ tvaldecl q Inductive noFields ar [cd] cl
  where
  function :: Maybe HaskellExport -> TCM [HS.Decl] -> TCM [HS.Decl]
  function mhe fun = do
    ccls <- mkwhere <$> fun
    case mhe of
      Nothing -> return ccls
      Just (HsExport t name) -> do
        let tsig :: HS.Decl
            tsig = HS.TypeSig dummy [HS.Ident name] (fakeType t)

            def :: HS.Decl
            def = HS.FunBind [HS.Match dummy (HS.Ident name) [] Nothing (HS.UnGuardedRhs (hsVarUQ $ dsubname q 0)) emptyBinds]
        return ([tsig,def] ++ ccls)

  functionFromClauses :: [Clause] -> TCM [HS.Decl]
  functionFromClauses cls = mapM (clause q Nothing) (tag 0 cls)

  functionFromCaseTree :: QName -> CompiledClauses -> TCM [HS.Decl]
  functionFromCaseTree q cc = do
    e <- casetree cc `runReaderT` initCCEnv (Just q)
    return $ [HS.FunBind [HS.Match dummy (dsubname q 0) [] Nothing (HS.UnGuardedRhs e) emptyBinds]]

  tag :: Nat -> [Clause] -> [(Nat, Bool, Clause)]
  tag _ []       = []
  tag i [cl]     = (i, True , cl) : []
  tag i (cl:cls) = (i, False, cl) : tag (i + 1) cls

  mkwhere :: [HS.Decl] -> [HS.Decl]
  mkwhere (HS.FunBind [m0, HS.Match _     dn ps mt rhs emptyBinds] :
           fbs@(_:_)) =
          [HS.FunBind [m0, HS.Match dummy dn ps mt rhs bindsAux]]
    where
#if MIN_VERSION_haskell_src_exts(1,17,0)
    bindsAux :: Maybe HS.Binds
    bindsAux = Just $ HS.BDecls fbs
#else
    bindsAux :: HS.Binds
    bindsAux = HS.BDecls fbs
#endif
  mkwhere fbs = fbs

  fbWithType :: HaskellType -> HS.Exp -> [HS.Decl]
  fbWithType ty e =
    [ HS.TypeSig dummy [unqhname "d" q] $ fakeType ty ] ++ fb e

  fb :: HS.Exp -> [HS.Decl]
  fb e  = [HS.FunBind [HS.Match dummy (unqhname "d" q) [] Nothing
                                (HS.UnGuardedRhs $ e) emptyBinds]]

  axiomErr :: HS.Exp
  axiomErr = rtmError $ "postulate evaluated: " ++ show (A.qnameToConcrete q)

-- | Environment for naming of local variables.
--   Invariant: @reverse ccCxt ++ ccNameSupply@
data CCEnv = CCEnv
  { ccFunName    :: Maybe QName -- ^ Agda function we are currently compiling.
  , ccNameSupply :: NameSupply  -- ^ Supply of fresh names
  , ccCxt        :: CCContext   -- ^ Names currently in scope
  , ccCatchAll   :: Maybe CompiledClauses  -- ^ Naive catch-all implementation.
      -- If an inner case has no catch-all clause, we use the one from its parent.
  }

type NameSupply = [HS.Name]
type CCContext  = [HS.Name]

mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv
mapNameSupply f e = e { ccNameSupply = f (ccNameSupply e) }

mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv
mapContext f e = e { ccCxt = f (ccCxt e) }

-- | Initial environment for expression generation.
initCCEnv :: Maybe QName -> CCEnv
initCCEnv q = CCEnv
  { ccFunName    = q
  , ccNameSupply = map (ihname "v") [0..]  -- DON'T CHANGE THESE NAMES!
  , ccCxt        = []
  , ccCatchAll   = Nothing
  }

-- | Term variables are de Bruijn indices.
lookupIndex :: Int -> CCContext -> HS.Name
lookupIndex i xs = fromMaybe __IMPOSSIBLE__ $ xs !!! i

-- | Case variables are de Bruijn levels.
lookupLevel :: Int -> CCContext -> HS.Name
lookupLevel l xs = fromMaybe __IMPOSSIBLE__ $ xs !!! (length xs - 1 - l)

type CC = ReaderT CCEnv TCM

-- | Compile a case tree into nested case and record expressions.
casetree :: CompiledClauses -> CC HS.Exp
casetree cc = do
  case cc of
    Fail -> return $ rtmError $ "Impossible Clause Body"
    Done xs v -> lambdasUpTo (length xs) $ hsCast <$> term v
    Case n (Branches True conBrs _ _) -> lambdasUpTo n $ do
      mkRecord =<< mapM casetree (content <$> conBrs)
    Case n (Branches False conBrs litBrs catchAll) -> lambdasUpTo (n + 1) $ do
      x <- lookupLevel n <$> asks ccCxt
      HS.Case (hsCast $ hsVarUQ x) <$> do
        updateCatchAll catchAll $ do
          br1 <- conAlts n conBrs
          br2 <- litAlts litBrs
          br3 <- catchAllAlts =<< asks ccCatchAll
          return (br1 ++ br2 ++ br3)

-- | Replace the current catch-all clause with a new one, if given.
updateCatchAll :: Maybe CompiledClauses -> CC a -> CC a
updateCatchAll Nothing   = id
updateCatchAll (Just cc) = local $ \ e -> e { ccCatchAll = Just cc }

-- -- | Replace de Bruijn index by term in catch-all tree.
-- substCatchAll :: Int -> I.Term -> CC a -> CC a
-- substCatchAll i t = local $ \ e -> e { ccCatchAll = subst i t $ ccCatchAll e }

conAlts :: Int -> Map QName (WithArity CompiledClauses) -> CC [HS.Alt]
conAlts x br = forM (Map.toList br) $ \ (c, WithArity n cc) -> do
  c <- lift $ conhqn c
  -- TODO: substitute in ccCatchAll somehow
  replaceVar x n $ \ xs -> do
    branch (HS.PApp c $ map HS.PVar xs) cc

litAlts :: Map Literal CompiledClauses -> CC [HS.Alt]
litAlts br = forM (Map.toList br) $ \ (l, cc) ->
  -- TODO: substitute in ccCatchAll somehow
  branch (HS.PLit HS.Signless $ hslit l) cc

catchAllAlts :: Maybe CompiledClauses -> CC [HS.Alt]
catchAllAlts (Just cc) = mapM (branch HS.PWildCard) [cc]
catchAllAlts Nothing   = do
  q <- fromMaybe __IMPOSSIBLE__ <$> asks ccFunName
  return [ HS.Alt dummy HS.PWildCard (HS.UnGuardedRhs $ rtmIncompleteMatch q) emptyBinds ]

branch :: HS.Pat -> CompiledClauses -> CC HS.Alt
branch pat cc = do
  e <- casetree cc
  return $ HS.Alt dummy pat (HS.UnGuardedRhs e) emptyBinds

-- | Replace de Bruijn Level @x@ by @n@ new variables.
replaceVar :: Int -> Int -> ([HS.Name] -> CC a) -> CC a
replaceVar x n cont = do
  (xs, rest) <- splitAt n <$> asks ccNameSupply
  let upd cxt = ys ++ reverse xs ++ zs -- We reverse xs to get nicer names.
       where
         -- compute the de Bruijn index
         i = length cxt - 1 - x
         -- discard index i
         (ys, _:zs) = splitAt i cxt
  local (mapNameSupply (const rest) . mapContext upd) $
    cont xs

-- | Precondition: Map not empty.
mkRecord :: Map QName HS.Exp -> CC HS.Exp
mkRecord fs = lift $ do
  -- Get the name of the first field
  let p1 = fst $ fromMaybe __IMPOSSIBLE__ $ headMaybe $ Map.toList fs
  -- Use the field name to get the record constructor and the field names.
  ConHead c _ind xs <- recConFromProj p1
  -- Convert the constructor to a Haskell name
  c <- conhqn c
  let (args :: [HS.Exp]) = for xs $ \ x -> fromMaybe __IMPOSSIBLE__ $ Map.lookup x fs
  return $ hsCast $ List.foldl HS.App (HS.Con c) args

-- -- | Precondition: Map not empty.
-- MAlonzo does not translate field names in data decls.
-- mkRecord :: Map QName HS.Exp -> CC HS.Exp
-- mkRecord fs = lift $ do
--   -- Get the list of (field name, expression pairs)
--   let l = Map.toList fs
--   -- Get the name of the first field
--   let p1 = fst $ fromMaybe __IMPOSSIBLE__ $ headMaybe l
--   -- Use the field name to get the record constructor
--   c <- I.conName <$> recConFromProj p1
--   -- Convert it to a Haskell name
--   c <- conhqn c
--   -- Convert the field names into Haskell names
--   fs <- mapM (mapFstM (xhqn "d")) l
--   return $ hsCast $ HS.RecConstr c $ map (uncurry HS.FieldUpdate) fs

recConFromProj :: QName -> TCM I.ConHead
recConFromProj q = do
  caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do
    let d = projFromType proj
    getRecordConstructor d

-- | Introduce lambdas such that @n@ variables are in scope.
lambdasUpTo :: Int -> CC HS.Exp -> CC HS.Exp
lambdasUpTo n cont = do
  diff <- (n -) . length <$> asks ccCxt
  lambdas diff cont

-- | Introduce n lambdas.
lambdas :: Int -> CC HS.Exp -> CC HS.Exp
lambdas diff cont = intros diff $ \ xs -> mkLams xs <$> cont

-- -- | Introduce variables such that @n@ are in scope.
-- introsUpTo :: Int -> ([HS.Name] -> CC HS.Exp) -> CC HS.Exp
-- introsUpTo n cont = do
--   diff <- (n -) . length <$> asks ccCxt
--   intros diff cont

-- | Introduce n variables into the context.
intros :: Int -> ([HS.Name] -> CC HS.Exp) -> CC HS.Exp
intros diff cont = do
  if diff <= 0 then cont [] else do
    -- Need diff lambdas to continue.
    (xs, rest) <- splitAt diff <$> asks ccNameSupply
    local (mapNameSupply (const rest) . mapContext (reverse xs ++)) $
      cont xs

-- | Prefix a Haskell expression with lambda abstractions.
mkLams :: [HS.Name] -> HS.Exp -> HS.Exp
mkLams [] e = e
mkLams xs e = HS.Lambda dummy (map HS.PVar xs) e

checkConstructorType :: QName -> TCM [HS.Decl]
checkConstructorType q = do
  Just (HsDefn ty hs) <- compiledHaskell . defCompiledRep <$> getConstInfo q
  return [ HS.TypeSig dummy [unqhname "check" q] $ fakeType ty
         , HS.FunBind [HS.Match dummy (unqhname "check" q) [] Nothing
                                (HS.UnGuardedRhs $ fakeExp hs) emptyBinds]
         ]

checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HS.Decl]
checkCover q ty n cs = do
  let tvs = [ "a" ++ show i | i <- [1..n] ]
      makeClause c = do
        (a, _) <- conArityAndPars c
        Just (HsDefn _ hsc) <- compiledHaskell . defCompiledRep <$> getConstInfo c
        let pat = HS.PApp (HS.UnQual $ HS.Ident hsc) $ replicate a HS.PWildCard
        return $ HS.Alt dummy pat (HS.UnGuardedRhs $ HS.unit_con) emptyBinds

  cs <- mapM makeClause cs
  let rhs = case cs of
              [] -> fakeExp "()" -- There is no empty case statement in Haskell
              _  -> HS.Case (HS.Var $ HS.UnQual $ HS.Ident "x") cs

  return [ HS.TypeSig dummy [unqhname "cover" q] $ fakeType $ unwords (ty : tvs) ++ " -> ()"
         , HS.FunBind [HS.Match dummy (unqhname "cover" q) [HS.PVar $ HS.Ident "x"]
                                Nothing (HS.UnGuardedRhs rhs) emptyBinds]
         ]

-- | Move somewhere else!
conArityAndPars :: QName -> TCM (Nat, Nat)
conArityAndPars q = do
  def <- getConstInfo q
  TelV tel _ <- telView $ defType def
  let Constructor{ conPars = np } = theDef def
      n = length (telToList tel)
  return (n - np, np)

clause :: QName -> Maybe String -> (Nat, Bool, Clause) -> TCM HS.Decl
clause q maybeName (i, isLast, Clause{ namedClausePats = ps, clauseBody = b }) =
  HS.FunBind . (: cont) <$> main where
  main = match <$> argpatts ps (bvars b (0::Nat)) <*> clausebody b
  cont | isLast && List.any isCon ps = [match (List.map HS.PVar cvs) failrhs]
       | isLast                      = []
       | otherwise                   = [match (List.map HS.PVar cvs) crhs]
  cvs  = List.map (ihname "v") [0 .. length ps - 1]
  crhs = hsCast$ List.foldl HS.App (hsVarUQ $ dsubname q (i + 1)) (List.map hsVarUQ cvs)
  failrhs = rtmIncompleteMatch q  -- Andreas, 2011-11-16 call to RTE instead of inlined error
--  failrhs = rtmError $ "incomplete pattern matching: " ++ show q
  match hps rhs = HS.Match dummy (maybe (dsubname q i) HS.Ident maybeName) hps Nothing
                           (HS.UnGuardedRhs rhs) emptyBinds
  bvars (Body _)           _ = []
  bvars (Bind (Abs _ b'))  n = HS.PVar (ihname "v" n) : bvars b' (n + 1)
  bvars (Bind (NoAbs _ b)) n = HS.PWildCard : bvars b n
  bvars NoBody             _ = repeat HS.PWildCard -- ?

  isCon (Arg _ (Named _ ConP{})) = True
  isCon _                        = False

-- argpatts aps xs = hps
-- xs is alist of haskell *variables* in form of patterns (because of wildcard)
argpatts :: [I.NamedArg Pattern] -> [HS.Pat] -> TCM [HS.Pat]
argpatts ps0 bvs = evalStateT (List.concat <$> mapM pat' ps0) bvs
  where
  pat :: Pattern -> StateT [HS.Pat] TCM [HS.Pat]
  pat   (ProjP p  ) = do
    kit <- lift coinductionKit
    -- Sharps and flats are erased from compiled code
    if Just p == fmap nameOfFlat kit then return [] else
      lift $ typeError $ NotImplemented $ "Compilation of copatterns"
  pat   (VarP _   ) = do v <- gets head; modify tail; return [v]
  pat   (DotP _   ) = pat (VarP dummy) -- WHY NOT: return HS.PWildCard -- SEE ABOVE
  pat   (LitP (LitQName _ x)) = return [ litqnamepat x ]
  pat   (LitP l   ) = return [ HS.PLit HS.Signless $ hslit l ]

  pat p@(ConP c _ ps) = do
    -- Note that irr is applied once for every subpattern, so in the
    -- worst case it is quadratic in the size of the pattern. I
    -- suspect that this will not be a problem in practice, though.
    irrefutable <- lift $ irr p
    let tilde :: HS.Pat -> HS.Pat
        tilde = if tildesEnabled && irrefutable
                then HS.PParen . HS.PIrrPat
                else id
    ((:[]) . tilde . HS.PParen) <$>
      (HS.PApp <$> lift (conhqn $ conName c) <*> (List.concat <$> mapM pat' ps))

  {- Andreas, 2013-02-15 this triggers Issue 794,
     because it fails to count the variables bound in p,
     thus, the following variables bound by patterns do
     not correspond to the according rhs-variables.

  -- Andreas, 2010-09-29
  -- do not match against irrelevant stuff
  pat' a | isIrrelevant a = return $ HS.PWildCard
-}
  pat' :: I.NamedArg Pattern -> StateT [HS.Pat] TCM [HS.Pat]
  pat' a = pat $ namedArg a

  tildesEnabled = False

  -- | Is the pattern irrefutable?
  irr :: Pattern -> TCM Bool
  irr (ProjP {})  = __IMPOSSIBLE__
  irr (VarP {})   = return True
  irr (DotP {})   = return True
  irr (LitP {})   = return False
  irr (ConP c _ ps) =
    (&&) <$> singleConstructorType (conName c)
         <*> (andM $ List.map irr' ps)

  -- | Irrelevant patterns are naturally irrefutable.
  irr' :: I.NamedArg Pattern -> TCM Bool
  irr' a | isIrrelevant a = return $ True
  irr' a = irr $ namedArg a

clausebody :: ClauseBody -> TCM HS.Exp
clausebody b0 = go 0 b0 where
  go n (Body tm       )   = hsCast <$> do
    runReaderT (intros n $ const $ term tm) (initCCEnv Nothing)
  go n (Bind (Abs _ b))   = go (n+1) b
  go n (Bind (NoAbs _ b)) = go n b
  go n NoBody             = return $ rtmError $ "Impossible Clause Body"


closedTerm :: Term -> TCM HS.Exp
closedTerm v = term v `runReaderT` initCCEnv Nothing

-- | Extract Agda term to Haskell expression.
--   Irrelevant arguments are extracted as @()@.
--   Types are extracted as @()@.
--   @DontCare@ outside of irrelevant arguments is extracted as @error@.
term :: Term -> CC HS.Exp
term tm0 = case unSpine $ ignoreSharing tm0 of
  Var   i es -> do
    x <- lookupIndex i <$> asks ccCxt
    apps (hsVarUQ x) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
  Lam   _ at -> lambdas 1 $ term $ absBody at
  Lit   l    -> lift $ literal l
  Def   q es -> do
    let Just as = allApplyElims es
    q <- lift $ xhqn "d" q
    HS.Var q `apps` as
  Con   c as -> do
    let q = conName c
    kit <- lift coinductionKit
    if Just q == (nameOfSharp <$> kit)
      then (`apps` as) . HS.Var =<< lift (xhqn "d" q)
      else (`apps` as) . HS.Con =<< lift (conhqn q)
  Level l    -> term =<< lift (reallyUnLevelView l)
  Pi    _ _  -> return HS.unit_con
  Sort  _    -> return HS.unit_con
  MetaV _ _  -> mazerror "hit MetaV"
  DontCare _ -> return $ rtmError $ "hit DontCare"
  Shared{}   -> __IMPOSSIBLE__
  ExtLam{}   -> __IMPOSSIBLE__
  where apps =  foldM (\ h a -> HS.App h <$> term' a)

-- | Irrelevant arguments are replaced by Haskells' ().
term' :: I.Arg Term -> CC HS.Exp
term' a | isIrrelevant a = return HS.unit_con
term' a = term $ unArg a

literal :: Literal -> TCM HS.Exp
literal l = case l of
  LitInt    _ _   -> do toN <- bltQual "NATURAL" mazIntegerToNat
                        return $ HS.Var toN `HS.App` typed "Integer"
  LitFloat  _ _   -> return $ typed "Double"
  LitQName  _ x   -> return $ litqname x
  _               -> return $ l'
  where l'    = HS.Lit $ hslit l
        typed = HS.ExpTypeSig dummy l' . HS.TyCon . rtmQual

hslit :: Literal -> HS.Literal
hslit l = case l of LitInt    _ x -> HS.Int    x
                    LitFloat  _ x -> HS.Frac   (toRational x)
                    LitString _ x -> HS.String x
                    LitChar   _ x -> HS.Char   x
                    LitQName  _ x -> __IMPOSSIBLE__

litqname :: QName -> HS.Exp
litqname x =
  HS.Con (HS.Qual mazRTE $ HS.Ident "QName") `HS.App`
  HS.Lit (HS.Int n) `HS.App`
  HS.Lit (HS.Int m) `HS.App`
  (rtmError "primQNameType: not implemented") `HS.App`
  (rtmError "primQNameDefinition: not implemented") `HS.App`
  HS.Lit (HS.String $ show x )
  where
    NameId n m = nameId $ qnameName x

litqnamepat :: QName -> HS.Pat
litqnamepat x =
  HS.PApp (HS.Qual mazRTE $ HS.Ident "QName")
          [ HS.PLit HS.Signless (HS.Int n)
          , HS.PLit HS.Signless (HS.Int m)
          , HS.PWildCard
          , HS.PWildCard
          , HS.PWildCard]
  where
    NameId n m = nameId $ qnameName x

condecl :: QName -> TCM (Nat, HS.ConDecl)
condecl q = do
  (ar, np) <- conArityAndPars q
  return $ (ar + np, cdecl q ar)

cdecl :: QName -> Nat -> HS.ConDecl
cdecl q n = HS.ConDecl (unqhname "C" q)
            [ HS.TyVar $ ihname "a" i | i <- [0 .. n - 1] ]

tvaldecl :: QName
         -> Induction
            -- ^ Is the type inductive or coinductive?
         -> Nat -> Nat -> [HS.ConDecl] -> Maybe Clause -> [HS.Decl]
tvaldecl q ind ntv npar cds cl =
  HS.FunBind [HS.Match dummy vn pvs Nothing
                       (HS.UnGuardedRhs HS.unit_con) emptyBinds] :
  maybe [HS.DataDecl dummy kind [] tn tvs
                     (List.map (HS.QualConDecl dummy [] []) cds) []]
        (const []) cl
  where
  (tn, vn) = (unqhname "T" q, unqhname "d" q)
  tvs = [ HS.UnkindedVar $ ihname "a" i | i <- [0 .. ntv  - 1]]
  pvs = [ HS.PVar        $ ihname "a" i | i <- [0 .. npar - 1]]

  -- Inductive data types consisting of a single constructor with a
  -- single argument are translated into newtypes.
  kind = case (ind, cds) of
    (Inductive, [HS.ConDecl _ [_]]) -> HS.NewType
    (Inductive, [HS.RecDecl _ [_]]) -> HS.NewType
    _                               -> HS.DataType

infodecl :: QName -> HS.Decl
infodecl q = fakeD (unqhname "name" q) $ show $ prettyShow q

--------------------------------------------------
-- Inserting unsafeCoerce
--------------------------------------------------

hsCast :: HS.Exp -> HS.Exp
{-
hsCast = addcast . go where
  addcast [e@(HS.Var(HS.UnQual(HS.Ident(c:ns))))] | c == 'v' && all isDigit ns = e
  addcast es = foldl HS.App mazCoerce es
  -- this need to be extended if you generate other kinds of exps.
  go (HS.App e1 e2    ) = go e1 ++ [hsCast e2]
  go (HS.Lambda _ ps e) = [ HS.Lambda dummy ps (hsCast e) ]
  go e = [e]
-}

hsCast e = mazCoerce `HS.App` hsCast' e

hsCast' :: HS.Exp -> HS.Exp
hsCast' (HS.App e1 e2)     = hsCast' e1 `HS.App` (hsCoerce $ hsCast' e2)
hsCast' (HS.Lambda _ ps e) = HS.Lambda dummy ps $ hsCast' e
hsCast' e = e

-- No coercion for literal integers
hsCoerce :: HS.Exp -> HS.Exp
hsCoerce e@(HS.ExpTypeSig _ (HS.Lit (HS.Int{})) _) = e
hsCoerce e = HS.App mazCoerce e

--------------------------------------------------
-- Writing out a haskell module
--------------------------------------------------

writeModule :: HS.Module -> TCM ()
writeModule (HS.Module l m ps w ex imp ds) = do
  -- Note that GHC assumes that sources use ASCII or UTF-8.
  out <- outFile m
  liftIO $ UTF8.writeFile out $ prettyPrint $
    HS.Module l m (p : ps) w ex imp ds
  where
  p = HS.LanguagePragma dummy $ List.map HS.Ident $
        [ "EmptyDataDecls"
        , "ExistentialQuantification"
        , "ScopedTypeVariables"
        , "NoMonomorphismRestriction"
        , "Rank2Types"
        ]

rteModule :: HS.Module
rteModule = ok $ parse $ unlines
  [ "module " ++ prettyPrint mazRTE ++ " where"
  , "import Unsafe.Coerce"
  , ""
  , "-- Special version of coerce that plays well with rules."
  , "{-# INLINE [1] mazCoerce #-}"
  , "mazCoerce = Unsafe.Coerce.unsafeCoerce"
  , "{-# RULES \"coerce-id\" forall (x :: a) . mazCoerce x = x #-}"
  , ""
  , "-- Builtin QNames, the third field is for the type."
  , "data QName a b = QName { nameId, moduleId :: Integer, qnameType :: a, qnameDefinition :: b, qnameString :: String}"
  , "instance Eq (QName a b) where"
  , "  QName a b _ _ _ == QName c d _ _ _ = (a, b) == (c, d)"
  , ""
  , "mazIncompleteMatch :: String -> a"
  , "mazIncompleteMatch s = error (\"MAlonzo Runtime Error: incomplete pattern matching: \" ++ s)"
  ]
  where
    parse :: String -> HS.ParseResult HS.Module
    parse = HS.parseModuleWithMode
              HS.defaultParseMode
                { HS.extensions = [ HS.EnableExtension HS.ExplicitForAll ] }

    ok :: HS.ParseResult HS.Module -> HS.Module
    ok (HS.ParseOk d)   = d
    ok HS.ParseFailed{} = __IMPOSSIBLE__

compileDir :: TCM FilePath
compileDir = do
  mdir <- optCompileDir <$> commandLineOptions
  case mdir of
    Just dir -> return dir
    Nothing  -> __IMPOSSIBLE__

outFile' :: (HS.Pretty a, TransformBi HS.ModuleName (Wrap a)) =>
            a -> TCM (FilePath, FilePath)
outFile' m = do
  mdir <- compileDir
  let (fdir, fn) = splitFileName $ repldot pathSeparator $
                   prettyPrint m
  let dir = mdir </> fdir
      fp  = dir </> replaceExtension fn "hs"
  liftIO $ createDirectoryIfMissing True dir
  return (mdir, fp)
  where
  repldot c = List.map $ \ c' -> if c' == '.' then c else c'

outFile :: HS.ModuleName -> TCM FilePath
outFile m = snd <$> outFile' m

outFile_ :: TCM FilePath
outFile_ = outFile =<< curHsMod

callGHC :: Bool -> Interface -> TCM ()
callGHC modIsMain i = do
  setInterface i
  mdir          <- compileDir
  hsmod         <- prettyPrint <$> curHsMod
  MName agdaMod <- curMName
  let outputName = case agdaMod of
        [] -> __IMPOSSIBLE__
        ms -> last ms
  (mdir, fp) <- outFile' =<< curHsMod
  opts       <- optGhcFlags <$> commandLineOptions

  let overridableArgs =
        [ "-O"] ++
        (if modIsMain then ["-o", mdir </> show (nameConcrete outputName)] else []) ++
        [ "-Werror"]
      otherArgs       =
        [ "-i" ++ mdir] ++
        (if modIsMain then ["-main-is", hsmod] else []) ++
        [ fp
        , "--make"
        , "-fwarn-incomplete-patterns"
        , "-fno-warn-overlapping-patterns"
        ]
      args     = overridableArgs ++ opts ++ otherArgs
      compiler = "ghc"

  -- Note: Some versions of GHC use stderr for progress reports. For
  -- those versions of GHC we don't print any progress information
  -- unless an error is encountered.
  callCompiler compiler args