content: {-|
  Module      : IRTS.Compiler
  Description : Coordinates the compilation process.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,
               TypeSynonymInstances #-}
  
  module IRTS.Compiler(compile, generate) where
  
  import Idris.AbsSyntax
  import Idris.ASTUtils
  import Idris.Core.CaseTree
  import Idris.Core.Evaluate
  import Idris.Core.TT
  import Idris.Erasure
  import Idris.Error
  import Idris.Options
  import Idris.Output
  import IRTS.CodegenC
  import IRTS.CodegenCommon
  import IRTS.Defunctionalise
  import IRTS.DumpBC
  import IRTS.Exports
  import IRTS.Inliner
  import IRTS.LangOpts
  import IRTS.Portable
  import IRTS.Simplified
  
  import Prelude hiding (id, (.))
  
  import Control.Category
  import Control.Monad
  import Control.Monad.State
  import Data.List
  import qualified Data.Map as M
  import Data.Ord
  import qualified Data.Set as S
  import System.Directory
  import System.Exit
  import System.IO
  import System.Process
  
  -- |  Compile to simplified forms and return CodegenInfo
  compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
  compile codegen f mtm = do
          logCodeGen 1 "Compiling Output."
          iReport 2 "Compiling Output."
          checkMVs  -- check for undefined metavariables
          checkTotality -- refuse to compile if there are totality problems
          exports <- findExports
          let rootNames = case mtm of
                               Nothing -> []
                               Just t -> freeNames t
  
          logCodeGen 1 "Running Erasure Analysis"
          iReport 3 "Running Erasure Analysis"
          reachableNames <- performUsageAnalysis
                                (rootNames ++ getExpNames exports)
          maindef <- case mtm of
                          Nothing -> return []
                          Just tm -> do md <- irMain tm
                                        logCodeGen 1 $ "MAIN: " ++ show md
                                        return [(sMN 0 "runMain", md)]
          objs <- getObjectFiles codegen
          libs <- getLibs codegen
          flags <- getFlags codegen
          hdrs <- getHdrs codegen
          impdirs <- rankedImportDirs f
          ttDeclarations <- getDeclarations reachableNames
          defsIn <- mkDecls reachableNames
          -- if no 'main term' given, generate interface files
          let iface = case mtm of
                           Nothing -> True
                           Just _ -> False
  
          let defs = defsIn ++ maindef
  
          -- Inlined top level LDecl made here
          let defsInlined = inlineAll defs
          let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
                             defsInlined
  
          logCodeGen 1 "Inlining"
  
          dumpCases <- getDumpCases
          case dumpCases of
              Nothing -> return ()
              Just f -> runIO $ writeFile f (showCaseTrees defsUniq)
  
          let (nexttag, tagged) = addTags 65536 (liftAll defsInlined)
          let ctxtIn = addAlist tagged emptyContext
  
          logCodeGen 1 "Defunctionalising"
          iReport 3 "Defunctionalising"
          let defuns_in = defunctionalise nexttag ctxtIn
          logCodeGen 5 $ show defuns_in
          logCodeGen 1 "Inlining"
          iReport 3 "Inlining"
          let defuns = inline defuns_in
          logCodeGen 5 $ show defuns
          logCodeGen 1 "Resolving variables for CG"
  
          let checked = simplifyDefs defuns (toAlist defuns)
          outty <- outputTy
          dumpDefun <- getDumpDefun
          case dumpDefun of
              Nothing -> return ()
              Just f -> runIO $ writeFile f (dumpDefuns defuns)
          triple <- Idris.AbsSyntax.targetTriple
          cpu <- Idris.AbsSyntax.targetCPU
          logCodeGen 1 "Generating Code."
          iReport 2 "Generating Code."
          case checked of
              OK c -> do return $ CodegenInfo f outty triple cpu
                                              hdrs impdirs objs libs flags
                                              NONE c (toAlist defuns)
                                              tagged iface exports
                                              ttDeclarations
              Error e -> ierror e
    where checkMVs = do i <- getIState
                        case map fst (idris_metavars i) \\ primDefs of
                              [] -> return ()
                              ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
                                       iputStrLn "\nEvaluation of any of these will crash at run time."
                                       return ()
          checkTotality = do i <- getIState
                             case idris_totcheckfail i of
                               [] -> return ()
                               ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n  " ++ msg
  
  generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
  generate codegen mainmod ir
    = case codegen of
         -- Built-in code generators (FIXME: lift these out!)
         Via _ "c" -> codegenC ir
         -- Any external code generator
         Via fm cg -> do input <- case fm of
                                      IBCFormat -> return mainmod
                                      JSONFormat -> do
                                          tempdir <- getTemporaryDirectory
                                          (fn, h) <- openTempFile tempdir "idris-cg.json"
                                          writePortable h ir
                                          hClose h
                                          return fn
                         let cmd = "idris-codegen-" ++ cg
                             args = [input, "-o", outputFile ir] ++ compilerFlags ir
                         exit <- rawSystem cmd (if interfaces ir then "--interface" : args else args)
                         when (exit /= ExitSuccess) $
                              putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
         Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
  
  irMain :: TT Name -> Idris LDecl
  irMain tm = do
      i <- irTerm (sMN 0 "runMain") M.empty [] tm
      return $ LFun [] (sMN 0 "runMain") [] (LForce i)
  
  mkDecls :: [Name] -> Idris [(Name, LDecl)]
  mkDecls used
      = do i <- getIState
           let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
           decls <- mapM build ds
           return decls
  
  getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
  getDeclarations used
      = do i <- getIState
           let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
           return ds
  
  showCaseTrees :: [(Name, LDecl)] -> String
  showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
    where
      showCT (n, LFun opts f args lexp)
         = showOpts ++
           show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
              ++ show lexp
        where
          showOpts | Inline `elem` opts = "%inline "
                   | otherwise = ""
      showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
  
      defnRank :: (Name, LDecl) -> String
      defnRank (n, LFun _ _ _ _)       = "1" ++ nameRank n
      defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
  
      nameRank :: Name -> String
      nameRank (UN s)   = "1" ++ show s
      nameRank (MN i s) = "2" ++ show s ++ show i
      nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
      nameRank (SN sn) = "4" ++ snRank sn
      nameRank n = "5" ++ show n
  
      snRank :: SpecialName -> String
      snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
      snRank (ImplementationN n args) = "2" ++ nameRank n ++ concatMap show args
      snRank (ParentN n s) = "3" ++ nameRank n ++ show s
      snRank (MethodN n) = "4" ++ nameRank n
      snRank (CaseN _ n) = "5" ++ nameRank n
      snRank (ImplementationCtorN n) = "7" ++ nameRank n
      snRank (WithN i n) = "8" ++ nameRank n ++ show i
  
  isCon (TyDecl _ _) = True
  isCon _ = False
  
  build :: (Name, Def) -> Idris (Name, LDecl)
  build (n, d)
      = do i <- getIState
           case getPrim n i of
                Just (ar, op) ->
                    let args = map (\x -> sMN x "op") [0..] in
                        return (n, (LFun [] n (take ar args)
                                           (LOp op (map LV (take ar args)))))
                _ -> do def <- mkLDecl n d
                        logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
                        return (n, def)
     where getPrim n i
               | Just (ar, op) <- lookup n (idris_scprims i)
                    = Just (ar, op)
               | Just ar <- lookup n (S.toList (idris_externs i))
                    = Just (ar, LExternal n)
           getPrim n i = Nothing
  
  declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
  declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
  
  mkLDecl n (Function tm _)
      = declArgs [] True n <$> irTerm n M.empty [] tm
  
  mkLDecl n (CaseOp ci _ _ _ pats cd)
      = declArgs [] (case_inlinable ci || caseName n) n <$> irTree n args sc
    where
      (args, sc) = cases_runtime cd
  
      -- Always attempt to inline functions arising from 'case' expressions
      caseName (SN (CaseN _ _)) = True
      caseName (SN (WithN _ _)) = True
      caseName (NS n _) = caseName n
      caseName _ = False
  
  mkLDecl n (TyDecl (DCon tag arity _) _) =
      LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
  
  mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
  mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
  
  data VarInfo = VI
      { viMethod :: Maybe Name
      }
      deriving Show
  
  type Vars = M.Map Name VarInfo
  
  irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
  irTerm top vs env tm@(App _ f a) = do
    ist <- getIState
    case unApply tm of
      (P _ n _, args)
          | n `elem` map fst (idris_metavars ist) \\ primDefs
          -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
      (P _ (UN m) _, args)
          | m == txt "mkForeignPrim"
          -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
  
      (P _ (UN u) _, [_, arg])
          | u == txt "unsafePerformPrimIO"
          -> irTerm top vs env arg
  
      (P _ (UN u) _, _)
          | u == txt "assert_unreachable"
          -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top
  
      (P _ (UN u) _, [_, msg])
          | u == txt "idris_crash"
          -> do msg' <- irTerm top vs env msg
                return $ LOp LCrash [msg']
  
      -- TMP HACK - until we get inlining.
      (P _ (UN r) _, [_, _, _, _, _, arg])
          | r == txt "replace"
          -> irTerm top vs env arg
  
      -- 'void' doesn't have any pattern clauses and only gets called on
      -- erased things in higher order contexts (also a TMP HACK...)
      (P _ (UN r) _, _)
          | r == txt "void"
          -> return LNothing
  
      -- Laziness, the old way
      (P _ (UN l) _, [_, arg])
          | l == txt "lazy"
          -> error "lazy has crept in somehow"
  
      (P _ (UN l) _, [_, arg])
          | l == txt "force"
          -> LForce <$> irTerm top vs env arg
  
      -- Laziness, the new way
      (P _ (UN l) _, [_, _, arg])
          | l == txt "Delay"
          -> LLazyExp <$> irTerm top vs env arg
  
      (P _ (UN l) _, [_, _, arg])
          | l == txt "Force"
          -> LForce <$> irTerm top vs env arg
  
      (P _ (UN a) _, [_, _, _, arg])
          | a == txt "assert_smaller"
          -> irTerm top vs env arg
  
      (P _ (UN a) _, [_, arg])
          | a == txt "assert_total"
          -> irTerm top vs env arg
  
      (P _ (UN p) _, [_, arg])
          | p == txt "par"
          -> do arg' <- irTerm top vs env arg
                return $ LOp LPar [LLazyExp arg']
  
      (P _ (UN pf) _, [arg])
          | pf == txt "prim_fork"
          -> do arg' <- irTerm top vs env arg
                return $ LOp LFork [LLazyExp arg']
  
      (P _ (UN m) _, [_,size,t])
          | m == txt "malloc"
          -> irTerm top vs env t
  
      (P _ (UN tm) _, [_,t])
          | tm == txt "trace_malloc"
          -> irTerm top vs env t -- TODO
  
      -- This case is here until we get more general inlining. It's just
      -- a really common case, and the laziness hurts...
      (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
                                      (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
          | be == txt "ifThenElse"
          , d  == txt "Delay"
          , d' == txt "Delay"
          , b  == txt "Bool"
          , p  == txt "Prelude"
          -> do
              x' <- irTerm top vs env x
              t' <- irTerm top vs env t
              e' <- irTerm top vs env e
              return (LCase Shared x'
                               [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
                               ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
                               ])
  
      -- data constructor
      (P (DCon t arity _) n _, args) -> do
          detag <- fgetState (opt_detaggable . ist_optimisation n)
          used  <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
  
          let isNewtype = length used == 1 && detag
          let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
  
          -- The following code removes fields from data constructors
          -- and performs the newtype optimisation.
          --
          -- The general rule here is:
          -- Everything we get as input is not touched by erasure,
          -- so it conforms to the official arities and types
          -- and we can reason about it like it's plain TT.
          --
          -- It's only the data that leaves this point that's erased
          -- and possibly no longer typed as the original TT version.
          --
          -- Especially, underapplied constructors must yield functions
          -- even if all the remaining arguments are erased
          -- (the resulting function *will* be applied, to NULLs).
          --
          -- This will probably need rethinking when we get erasure from functions.
  
          -- "padLams" will wrap our term in LLam-bdas and give us
          -- the "list of future unerased args" coming from these lambdas.
          --
          -- We can do whatever we like with the list of unerased args,
          -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
          let padLams = padLambdas used (length args) arity
  
          case compare (length args) arity of
  
              -- overapplied
              GT  -> ifail ("overapplied data constructor: " ++ show tm ++
                            "\nDEBUG INFO:\n" ++
                            "Arity: " ++ show arity ++ "\n" ++
                            "Arguments: " ++ show args ++ "\n" ++
                            "Pruned arguments: " ++ show argsPruned)
  
              -- exactly saturated
              EQ  | isNewtype
                  -> irTerm top vs env (head argsPruned)
  
                  -- compile Nat-likes as bigints
                  | Just LikeZ <- isLikeNat ist n
                  -> irTerm top vs env $ Constant (BI 0)
  
                  -- compile Nat-likes as bigints
                  | Just LikeS <- isLikeNat ist n
                  -> irTerm top vs env $ mkApp
                      (P Ref (sUN "prim__addBigInt") Erased)
                      (Constant (BI 1) : argsPruned)
  
                  | otherwise  -- not newtype, plain data ctor
                  -> buildApp (LV n) argsPruned
  
              -- not saturated, underapplied
              LT  | isNewtype               -- newtype
                  , length argsPruned == 1  -- and we already have the value
                  -> padLams . (\tm [] -> tm)  -- the [] asserts there are no unerased args
                      <$> irTerm top vs env (head argsPruned)
  
                  | isNewtype  -- newtype but the value is not among args yet
                  -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
  
                  -- compile Nat-likes as bigints
                  -- it seems that prim applications needn't be saturated
                  | Just LikeS <- isLikeNat ist n
                  -> irTerm top vs env $
                      App Complete
                          (P Ref (sUN "prim__addBigInt") Erased)
                          (Constant $ BI 1)
  
                  -- not a newtype, just apply to a constructor
                  | otherwise
                  -> padLams . applyToNames <$> buildApp (LV n) argsPruned
  
      -- type constructor
      (P (TCon t a) n _, args) -> return LNothing
  
      -- an external name applied to arguments
      (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
          LOp (LExternal n) <$> mapM (irTerm top vs env) args
  
      -- a name applied to arguments
      (P _ n _, args) -> do
          case lookup n (idris_scprims ist) of
              -- if it's a primitive that is already saturated,
              -- compile to the corresponding op here already to save work
              Just (arity, op) | length args == arity
                  -> LOp op <$> mapM (irTerm top vs env) args
  
              -- otherwise, just apply the name
              _   -> applyName n ist args
  
      -- turn de bruijn vars into regular named references and try again
      (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args
  
      (f, args)
          -> LApp False
              <$> irTerm top vs env f
              <*> mapM (irTerm top vs env) args
  
    where
      buildApp :: LExp -> [Term] -> Idris LExp
      buildApp e [] = return e
      buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs
  
      applyToNames :: LExp -> [Name] -> LExp
      applyToNames tm [] = tm
      applyToNames tm ns = LApp False tm $ map LV ns
  
      padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
      padLambdas used startIdx endSIdx mkTerm
          = LLam allNames $ mkTerm nonerasedNames
        where
          allNames       = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
          nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
  
      applyName :: Name -> IState -> [Term] -> Idris LExp
      applyName n ist args =
          LApp False (LV n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)
        where
          erase (i, x)
              | i >= arity || i `elem` used = x
              | otherwise = Erased
  
          arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
              Just (CaseOp ci ty tys def tot cdefs) -> length tys
              Just (TyDecl (DCon tag ar _) _)       -> ar
              Just (TyDecl Ref ty)                  -> length $ getArgTys ty
              Just (Operator ty ar op)              -> ar
              Just def -> error $ "unknown arity: " ++ show (n, def)
              Nothing  -> 0  -- no definition, probably local name => can't erase anything
  
          -- name for purposes of usage info lookup
          uName
              | Just n' <- viMethod =<< M.lookup n vs = n'
              | otherwise = n
  
          used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
          fst4 (x,_,_,_,_,_) = x
  
  irTerm top vs env (P _ n _) = return $ LV n
  irTerm top vs env (V i)
      | i >= 0 && i < length env = return $ LV (env!!i)
      | otherwise = ifail $ "bad de bruijn index: " ++ show i
  
  irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
    where
      n' = uniqueName n env
  
  irTerm top vs env (Bind n (Let _ _ v) sc)
      = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc
  
  irTerm top vs env (Bind _ _ _) = return $ LNothing
  
  irTerm top vs env (Proj t (-1)) = do
      t' <- irTerm top vs env t
      return $ LOp (LMinus (ATInt ITBig))
                   [t', LConst (BI 1)]
  
  irTerm top vs env (Proj t i)   = LProj <$> irTerm top vs env t <*> pure i
  irTerm top vs env (Constant TheWorld) = return LNothing
  irTerm top vs env (Constant c)        = return (LConst c)
  irTerm top vs env (TType _)           = return LNothing
  irTerm top vs env Erased              = return LNothing
  irTerm top vs env Impossible          = return LNothing
  
  data LikeNat = LikeZ | LikeS
  
  isLikeNat :: IState -> Name -> Maybe LikeNat
  isLikeNat ist cn
      -- Nat itself is special-cased in Idris/DataOpts.hs,
      -- which will have already happened at this point.
  
      -- If the optimisation is disabled then nothing looks like Nat.
      | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)
      = Nothing
  
      | Just cTy <- lookupTyExact cn $ tt_ctxt ist
      , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
      , Just (z, s) <- natLikeCtors tyN
      = if | cn == z -> Just LikeZ
           | cn == s -> Just LikeS
           | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
  
      | otherwise = Nothing
    where
      natLikeCtors :: Name -> Maybe (Name, Name)
      natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of
          Just TI{con_names = [z, s]}
              | 0 <- getUsedCount z
              , looksLikeS s
              -> Just (z, s)
  
          Just TI{con_names = [s, z]}
              | 0 <- getUsedCount z
              , looksLikeS s
              -> Just (z, s)
  
          _ -> Nothing
  
      getUsedCount :: Name -> Int
      getUsedCount n =
          maybe 0 (length . usedpos)
          $ lookupCtxtExact n
          $ idris_callgraph ist
  
      looksLikeS :: Name -> Bool
      looksLikeS cn
          | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist
          , Just cTy <- lookupTyExact cn $ tt_ctxt ist
          , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]
          , (P TCon{} recTyN _, _) <- unApply recTy
          , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
          , recTyN == tyN
          = True
  
          | otherwise = False
  
  doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
  doForeign vs env (ret : fname : world : args)
       = do args' <- mapM splitArg args
            let fname' = toFDesc fname
            let ret' = toFDesc ret
            return $ LForeign ret' fname' args'
    where
      splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
          = do let l' = toFDesc l
               r' <- irTerm (sMN 0 "__foreignCall") vs env r
               return (l', r')
      splitArg _ = ifail $ "Badly formed foreign function call: " ++
                           show (ret : fname : world : args)
  
  
      toFDesc (Constant (Str str)) = FStr str
      toFDesc tm
         | (P _ n _, []) <- unApply tm = FCon (deNS n)
         | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
      toFDesc _ = FUnknown
  
      deNS (NS n _) = n
      deNS n = n
  doForeign vs env xs = ifail "Badly formed foreign function call"
  
  irTree :: Name -> [Name] -> SC -> Idris LExp
  irTree top args tree = do
      logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
      LLam args <$> irSC top M.empty tree
  
  irSC :: Name -> Vars -> SC -> Idris LExp
  irSC top vs (STerm t) = irTerm top vs [] t
  irSC top vs (UnmatchedCase str) = return $ LError str
  
  irSC top vs (ProjCase tm alts) = do
      tm'   <- irTerm top vs [] tm
      alts' <- mapM (irAlt top vs tm') alts
      return $ LCase Shared tm' alts'
  
  -- Transform matching on Delay to applications of Force.
  irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
      | delay == txt "Delay"
      = do sc' <- irSC top vs sc -- mkForce n' n sc
           return $ lsubst n' (LForce (LV n)) sc'
  
  -- There are two transformations in this case:
  --
  --  1. Newtype-case elimination:
  --      case {e0} of
  --          wrap({e1}) -> P({e1})   ==>   P({e0})
  --
  -- This is important because newtyped constructors are compiled away entirely
  -- and we need to do that everywhere.
  --
  --  2. Unused-case elimination (only valid for singleton branches):
  --      case {e0} of                                ==>     P
  --          C(x,y) -> P[... x,y not used ...]
  --
  -- This is important for runtime because sometimes we case on irrelevant data:
  --
  -- In the example above, {e0} will most probably have been erased
  -- so this vain projection would make the resulting program segfault
  -- because the code generator still emits a PROJECT(...) G-machine instruction.
  --
  -- Hence, we check whether the variables are used at all
  -- and erase the casesplit if they are not.
  --
  irSC top vs (Case up n [alt]) = do
      replacement <- case alt of
          ConCase cn a ns sc -> do
              detag <- fgetState (opt_detaggable . ist_optimisation cn)
              used  <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
              if detag && length used == 1
                  then return . Just $ substSC (ns !! head used) n sc
                  else return Nothing
          _ -> return Nothing
  
      case replacement of
          Just sc -> irSC top vs sc
          _ -> do
              alt' <- irAlt top vs (LV n) alt
              return $ case namesBoundIn alt' `usedIn` subexpr alt' of
                  [] -> subexpr alt'  -- strip the unused top-most case
                  _  -> LCase up (LV n) [alt']
    where
      namesBoundIn :: LAlt -> [Name]
      namesBoundIn (LConCase cn i ns sc) = ns
      namesBoundIn (LConstCase c sc)     = []
      namesBoundIn (LDefaultCase sc)     = []
  
      subexpr :: LAlt -> LExp
      subexpr (LConCase _ _ _ e) = e
      subexpr (LConstCase _   e) = e
      subexpr (LDefaultCase   e) = e
  
  -- FIXME: When we have a non-singleton case-tree of the form
  --
  --     case {e0} of
  --         C(x) => ...
  --         ...  => ...
  --
  -- and C is detaggable (the only constructor of the family), we can be sure
  -- that the first branch will be always taken -- so we add special handling
  -- to remove the dead default branch.
  --
  -- If we don't do so and C is newtype-optimisable, we will miss this newtype
  -- transformation and the resulting code will probably segfault.
  --
  -- This work-around is not entirely optimal; the best approach would be
  -- to ensure that such case trees don't arise in the first place.
  --
  irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
      detag <- fgetState (opt_detaggable . ist_optimisation cn)
      if detag
          then irSC top vs (Case up n [ConCase cn a ns sc])
          else do
              likeNat <- isLikeNat <$> getIState <*> pure cn
              case likeNat of
                  -- the annoying case: LikeS is translated into a default case
                  -- so we need to change the original DefaultCase to Z-case
                  -- and reorder it before this one
                  Just LikeS -> do
                      zCase <- LConstCase (BI 0) <$> irSC top vs sc'
                      sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)
                      return $ LCase up (LV n) [zCase, sCase]
  
                  -- the usual case
                  _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
  
  irSC top vs sc@(Case up n alts) = getIState >>= rhs
    where
      rhs ist
          | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts
          , Just LikeS <- isLikeNat ist cns
          = do
              -- reorder to make the Z case come first
              zCase <- LConstCase (BI 0) <$> irSC top vs scz
              sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)
              return $ LCase up (LV n) [zCase, sCase]
  
          | otherwise = do
              -- check that neither alternative needs the newtype optimisation,
              -- see comment above
              goneWrong <- or <$> mapM isDetaggable alts
              when goneWrong
                  $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
  
              -- everything okay
              LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
  
      isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
      isDetaggable  _                 = return False
  
  irSC top vs ImpossibleCase = return LNothing
  
  irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt
  
  -- this leaves out all unused arguments of the constructor
  irAlt top vs tm (ConCase n t args sc) = do
      likeNat <- isLikeNat <$> getIState <*> pure n
      used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
      let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
  
      case likeNat of
          -- like S
          Just LikeS -> do
              sc' <- irSC top vs sc
              case usedArgs of
                  [pv] -> return $ LDefaultCase $ LLet pv
                          ( LOp
                              (LMinus (ATInt ITBig))
                              [ tm
                              , LConst (BI 1)
                              ]
                          )
                          sc'
  
                  _ -> ifail $ "irAlt/LikeS: multiple used args: " ++ show usedArgs
  
          -- like Z
          Just LikeZ -> LConstCase (BI 0) <$> irSC top vs sc
  
          -- not like Nat
          Nothing -> LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc
    where
      methodVars = case n of
          SN (ImplementationCtorN interfaceName)
              -> M.fromList [(v, VI
                  { viMethod = Just $ mkFieldName n i
                  }) | (v,i) <- zip args [0..]]
          _
              -> M.empty -- not an implementation constructor
  
  irAlt top vs _ (ConstCase x rhs)
      | matchable   x = LConstCase x <$> irSC top vs rhs
      | matchableTy x = LDefaultCase <$> irSC top vs rhs
    where
      matchable (I _) = True
      matchable (BI _) = True
      matchable (Ch _) = True
      matchable (Str _) = True
      matchable (B8 _) = True
      matchable (B16 _) = True
      matchable (B32 _) = True
      matchable (B64 _) = True
      matchable _ = False
  
      matchableTy (AType (ATInt ITNative)) = True
      matchableTy (AType (ATInt ITBig)) = True
      matchableTy (AType (ATInt ITChar)) = True
      matchableTy StrType = True
  
      matchableTy (AType (ATInt (ITFixed IT8)))  = True
      matchableTy (AType (ATInt (ITFixed IT16))) = True
      matchableTy (AType (ATInt (ITFixed IT32))) = True
      matchableTy (AType (ATInt (ITFixed IT64))) = True
  
      matchableTy _ = False
  
  irAlt top vs tm (SucCase n rhs) = do
      rhs' <- irSC top vs rhs
      return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
                                              [tm,
                                              LConst (BI 1)]) rhs')
  
  irAlt top vs _ (ConstCase c rhs)
      = ifail $ "Can't match on (" ++ show c ++ ")"
  
  irAlt top vs _ (DefaultCase rhs)
      = LDefaultCase <$> irSC top vs rhs
  