module Main import Core.Binaryimport Core.Contextimport Core.Coreimport Core.Directoryimport Core.InitPrimitivesimport Core.Metadataimport Core.Optionsimport Core.Unify import Idris.CommandLineimport Idris.Desugarimport Idris.IDEMode.REPLimport Idris.ModTreeimport Idris.Packageimport Idris.Parserimport Idris.ProcessIdrimport Idris.REPLimport Idris.SetOptionsimport Idris.Syntaximport Idris.Version import Data.Vectimport System import Yaffle.Mainimport YafflePaths %default covering%flag C "-g" yprefix : Stringyprefix = unsafePerformIO (foreign FFI_C "getIdris2_prefix" (IO String)) findInput : List CLOpt -> Maybe StringfindInput [] = NothingfindInput (InputFile f :: fs) = Just ffindInput (_ :: fs) = findInput fs -- Add extra library directories from the "BLODWEN_PATH"-- environment variableupdatePaths : {auto c : Ref Ctxt Defs} ->              Core ()updatePaths    = do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"         case bprefix of              Just p => setPrefix p              Nothing => setPrefix yprefix         bpath <- coreLift $ getEnv "IDRIS2_PATH"         case bpath of              Just path => do traverse addExtraDir (map trim (split (==pathSep) path))                              pure ()              Nothing => pure ()         bdata <- coreLift $ getEnv "IDRIS2_DATA"         case bdata of              Just path => do traverse addDataDir (map trim (split (==pathSep) path))                              pure ()              Nothing => pure ()         blibs <- coreLift $ getEnv "IDRIS2_LIBS"         case blibs of              Just path => do traverse addLibDir (map trim (split (==pathSep) path))                              pure ()              Nothing => pure ()         -- IDRIS2_PATH goes first so that it overrides this if there's         -- any conflicts. In particular, that means that setting IDRIS2_PATH         -- for the tests means they test the local version not the installed         -- version         defs <- get Ctxt         addPkgDir "prelude"         addPkgDir "base"         addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++                        "idris2-" ++ showVersion False version ++ dirSep ++ "support")         addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++                        "idris2-" ++ showVersion False version ++ dirSep ++ "lib")         cwd <- coreLift $ currentDir         addLibDir cwd updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->                 Core ()updateREPLOpts    = do opts <- get ROpts         ed <- coreLift $ getEnv "EDITOR"         case ed of              Just e => put ROpts (record { editor = e } opts)              Nothing => pure () showInfo : {auto c : Ref Ctxt Defs}        -> {auto o : Ref ROpts REPLOpts}        -> List CLOpt        -> Core BoolshowInfo Nil = pure FalseshowInfo (BlodwenPaths :: _)    = do defs <- get Ctxt         iputStrLn (toString (dirs (options defs)))         pure TrueshowInfo (_::rest) = showInfo rest tryYaffle : List CLOpt -> Core BooltryYaffle [] = pure FalsetryYaffle (Yaffle f :: _) = do yaffleMain f []                               pure TruetryYaffle (c :: cs) = tryYaffle cs tryTTM : List CLOpt -> Core BooltryTTM [] = pure FalsetryTTM (Metadata f :: _) = do dumpTTM f                              pure TruetryTTM (c :: cs) = tryTTM cs  banner : Stringbanner = "     ____    __     _         ___                                           \n" ++         "    /  _/___/ /____(_)____   |__ \\                                          \n" ++         "    / // __  / ___/ / ___/   __/ /     Version " ++ showVersion True version ++ "\n" ++         "  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           \n" ++         " /___/\\__,_/_/  /_/____/   /____/      Type :? for help                     \n" ++         "\n" ++         "Welcome to Idris 2.  Enjoy yourself!"  stMain : List CLOpt -> Core ()stMain opts    = do False <- tryYaffle opts            | True => pure ()         False <- tryTTM opts            | True => pure ()         defs <- initDefs         c <- newRef Ctxt defs         s <- newRef Syn initSyntax         m <- newRef MD initMetadata         addPrimitives          setWorkingDir "."         updatePaths         let ide = ideMode opts         let ideSocket = ideModeSocket opts         let outmode = if ide then IDEMode 0 stdin stdout else REPL False         let fname = findInput opts         o <- newRef ROpts (REPLOpts.defaultOpts fname outmode)          finish <- showInfo opts         if finish         then pure ()         else do            -- If there's a --build or --install, just do that then quit           done <- processPackageOpts opts            when (not done) $              do True <- preOptions opts                     | False => pure ()                  u <- newRef UST initUState                 updateREPLOpts                 session <- getSession                 when (not $ nobanner session) $                   iputStrLn banner                 fname <- if findipkg session                             then findIpkg fname                             else pure fname                 case fname of                      Nothing => logTime "Loading prelude" $                                   when (not $ noprelude session) $                                     readPrelude                      Just f => logTime "Loading main file" $                                   (loadMainFile f >>= displayErrors)                  doRepl <- postOptions opts                 if doRepl                 then                   if ide || ideSocket                   then                     if not ideSocket                     then do                       setOutput (IDEMode 0 stdin stdout)                       replIDE {c} {u} {m}                     else do                       let (host, port) = ideSocketModeHostPort opts                       f <- coreLift $ initIDESocketFile host port                       case f of                         Left err => do                           coreLift $ putStrLn err                           coreLift $ exit 1                         Right file => do                           setOutput (IDEMode 0 file file)                           replIDE {c} {u} {m}                   else do                       repl {c} {u} {m}                       showTimeRecord                 else                      -- exit with an error code if there was an error, otherwise                      -- just exit                    do ropts <- get ROpts                       showTimeRecord                       case errorLine ropts of                         Nothing => pure ()                         Just _ => coreLift $ exit 1 -- Run any options (such as --version or --help) which imply printing a-- message then exiting. Returns wheter the program should continuequitOpts : List CLOpt -> IO BoolquitOpts [] = pure TruequitOpts (Version :: _)    = do putStrLn versionMsg         pure FalsequitOpts (Help :: _)    = do putStrLn usage         pure FalsequitOpts (ShowPrefix :: _)    = do putStrLn yprefix         pure FalsequitOpts (_ :: opts) = quitOpts opts main : IO ()main = do Right opts <- getCmdOpts             | Left err =>                    do putStrLn err                       putStrLn usage          continue <- quitOpts opts          if continue             then                coreRun (stMain opts)                     (\err : Error =>                             do putStrLn ("Uncaught error: " ++ show err)                                exit 1)                     (\res => pure ())             else pure ()