module Idris.SetOptions import Core.Contextimport Core.Directoryimport Core.Metadataimport Core.Optionsimport Core.Unify import Idris.CommandLineimport Idris.REPLimport Idris.Syntaximport Idris.Version import YafflePaths import System -- TODO: Version numbers on dependenciesexportaddPkgDir : {auto c : Ref Ctxt Defs} ->            String -> Core ()addPkgDir p    = do defs <- get Ctxt         addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++                             "idris2-" ++ showVersion False version ++ dirSep ++ p) dirOption : Dirs -> DirCommand -> Core ()dirOption dirs LibDir    = coreLift $ putStrLn         (dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion False version ++ dirSep) -- Options to be processed before type checking. Return whether to continue.exportpreOptions : {auto c : Ref Ctxt Defs} ->             {auto o : Ref ROpts REPLOpts} ->             List CLOpt -> Core BoolpreOptions [] = pure TruepreOptions (NoBanner :: opts)    = do setSession (record { nobanner = True } !getSession)         preOptions opts-- These things are processed later, but imply nobanner toopreOptions (OutputFile _ :: opts)    = do setSession (record { nobanner = True } !getSession)         preOptions optspreOptions (ExecFn _ :: opts)    = do setSession (record { nobanner = True } !getSession)         preOptions optspreOptions (IdeMode :: opts)    = do setSession (record { nobanner = True } !getSession)         preOptions optspreOptions (CheckOnly :: opts)    = do setSession (record { nobanner = True } !getSession)         preOptions optspreOptions (Quiet :: opts)    = do setOutput (REPL True)         preOptions optspreOptions (NoPrelude :: opts)    = do setSession (record { noprelude = True } !getSession)         preOptions optspreOptions (SetCG e :: opts)    = case getCG e of           Just cg => do setCG cg                         preOptions opts           Nothing =>              do coreLift $ putStrLn "No such code generator"                 coreLift $ putStrLn $ "Code generators available: " ++                                 showSep ", " (map fst availableCGs)                 coreLift $ exit 1preOptions (PkgPath p :: opts)    = do addPkgDir p         preOptions optspreOptions (Directory d :: opts)    = do defs <- get Ctxt         dirOption (dirs (options defs)) d         pure FalsepreOptions (Timing :: opts)    = do setLogTimings True         preOptions optspreOptions (DebugElabCheck :: opts)    = do setDebugElabCheck True         preOptions optspreOptions (RunREPL _ :: opts)    = do setOutput (REPL True)         setSession (record { nobanner = True } !getSession)         preOptions optspreOptions (FindIPKG :: opts)    = do setSession (record { findipkg = True } !getSession)         preOptions optspreOptions (DumpCases f :: opts)    = do setSession (record { dumpcases = Just f } !getSession)         preOptions optspreOptions (DumpLifted f :: opts)    = do setSession (record { dumplifted = Just f } !getSession)         preOptions optspreOptions (_ :: opts) = preOptions opts -- Options to be processed after type checking. Returns whether execution-- should continue (i.e., whether to start a REPL)exportpostOptions : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->              {auto s : Ref Syn SyntaxInfo} ->              {auto m : Ref MD Metadata} ->              {auto o : Ref ROpts REPLOpts} ->              List CLOpt -> Core BoolpostOptions [] = pure TruepostOptions (OutputFile outfile :: rest)    = do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile         postOptions rest         pure FalsepostOptions (ExecFn str :: rest)    = do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))         postOptions rest         pure FalsepostOptions (CheckOnly :: rest)    = do postOptions rest         pure FalsepostOptions (RunREPL str :: rest)    = do replCmd str         pure FalsepostOptions (_ :: rest) = postOptions rest exportideMode : List CLOpt -> BoolideMode [] = FalseideMode (IdeMode :: _) = TrueideMode (_ :: xs) = ideMode xs exportideModeSocket : List CLOpt -> BoolideModeSocket [] = FalseideModeSocket (IdeModeSocket _ :: _) = TrueideModeSocket (_ :: xs) = ideModeSocket xs