0 | module Idris.Driver

  2 | import Compiler.Common

  4 | import Core.Binary

  5 | import Core.Directory

  6 | import Core.InitPrimitives

  7 | import Core.Metadata

  8 | import Core.UnifyState

 10 | import Idris.CommandLine

 11 | import Idris.Env

 12 | import Idris.IDEMode.REPL

 13 | import Idris.Package

 14 | import Idris.ProcessIdr

 15 | import Idris.REPL

 16 | import Idris.SetOptions

 17 | import Idris.Syntax

 18 | import Idris.Version

 19 | import Idris.Pretty

 20 | import Idris.Error

 22 | import IdrisPaths

 24 | import Data.String

 25 | import System

 26 | import System.Directory

 27 | import System.File.Meta

 28 | import System.File.Virtual

 29 | import Libraries.Utils.Path

 30 | import System.Term

 32 | import Yaffle.Main

 34 | %default covering

 36 | findInputs : List CLOpt -> Maybe (List1 String)

 37 | findInputs [] = Nothing

 38 | findInputs (InputFile f :: fs) =

 39 |   let rest = maybe [] toList (findInputs fs)

 40 |   in  Just (f ::: rest)

 41 | findInputs (_ :: fs) = findInputs fs

 43 | splitPaths : String -> List1 String

 44 | splitPaths = map trim . split (==pathSeparator)

 47 | updateEnv : {auto c : Ref Ctxt Defs} ->

 48 |             {auto o : Ref ROpts REPLOpts} ->

 49 |             Core ()

 51 |     = do defs <- get Ctxt

 52 |          noColor <- coreLift [ isJust noc || not tty | noc <- idrisGetEnv "NO_COLOR", tty <- isTTY stdout ]

 53 |          when noColor $ setColor False

 54 |          bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"

 55 |          setPrefix (fromMaybe yprefix bprefix)

 56 |          bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"

 57 |          whenJust bpath $ traverseList1_ addExtraDir . splitPaths

 58 |          bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"

 59 |          whenJust bdata $ traverseList1_ addDataDir . splitPaths

 60 |          blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"

 61 |          whenJust blibs $ traverseList1_ addLibDir . splitPaths

 62 |          pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"

 63 |          whenJust pdirs $ traverseList1_ addPackageSearchPath . splitPaths

 64 |          cg <- coreLift $ idrisGetEnv "IDRIS2_CG"

 65 |          whenJust cg $ \ e => case getCG (options defs) e of

 66 |            Just cg => setCG cg

 67 |            Nothing => throw (InternalError ("Unknown code generator " ++ show e))

 68 |          inccgs <- coreLift $ idrisGetEnv "IDRIS2_INC_CGS"

 69 |          whenJust inccgs $ \ cgs =>

 70 |            traverseList1_ (setIncrementalCG False) $

 71 |              map trim (split (==',') cgs)

 72 |          -- IDRIS2_PATH goes first so that it overrides this if there's

 73 |          -- any conflicts. In particular, that means that setting IDRIS2_PATH

 74 |          -- for the tests means they test the local version not the installed

 75 |          -- version

 76 |          defs <- get Ctxt

 77 |          -- add global package path to the package search paths (after those

 78 |          -- added by the user with IDRIS2_PACKAGE_PATH)

 79 |          addPackageSearchPath !pkgGlobalDirectory

 80 |          -- These might fail while bootstrapping

 81 |          catch (addPkgDir "prelude" anyBounds) (const (pure ()))

 82 |          catch (addPkgDir "base" anyBounds) (const (pure ()))

 83 |          addDataDir (prefix_dir (dirs (options defs)) </>

 84 |                         ("idris2-" ++ showVersion False version) </> "support")

 85 |          addLibDir (prefix_dir (dirs (options defs)) </>

 86 |                         ("idris2-" ++ showVersion False version) </> "lib")

 87 |          Just cwd <- coreLift $ currentDir

 88 |               | Nothing => throw (InternalError "Can't get current directory")

 89 |          addLibDir cwd

 91 | updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->

 92 |                  Core ()

 94 |     = do ed <- coreLift $ idrisGetEnv "EDITOR"

 95 |          whenJust ed $ \ e => update ROpts { editor := e }

 97 | tryYaffle : List CLOpt -> Core Bool

 98 | tryYaffle [] = pure False

 99 | tryYaffle (Yaffle f :: _) = do yaffleMain f []

100 |                                pure True

101 | tryYaffle (c :: cs) = tryYaffle cs

103 | ignoreMissingIpkg : List CLOpt -> Bool

104 | ignoreMissingIpkg [] = False

105 | ignoreMissingIpkg (IgnoreMissingIPKG :: _) = True

106 | ignoreMissingIpkg (c :: cs) = ignoreMissingIpkg cs

108 | tryTTM : List CLOpt -> Core Bool

109 | tryTTM [] = pure False

110 | tryTTM (Metadata f :: _) = do dumpTTM f

111 |                               pure True

112 | tryTTM (c :: cs) = tryTTM cs

115 | banner : String

116 | banner = #"""

126 | checkVerbose : List CLOpt -> Bool

127 | checkVerbose [] = False

128 | checkVerbose (Verbose :: _) = True

129 | checkVerbose (_ :: xs) = checkVerbose xs

131 | stMain : List (String, Codegen) -> List CLOpt -> Core ()

132 | stMain cgs opts

133 |     = do False <- tryYaffle opts

134 |             | True => pure ()

135 |          False <- tryTTM opts

136 |             | True => pure ()

137 |          defs <- initDefs

138 |          let updated = foldl (\o, (s, _) => addCG (s, Other s) o) (options defs) cgs

139 |          c <- newRef Ctxt ({ options := updated } defs)

140 |          s <- newRef Syn initSyntax

141 |          setCG {c} $ maybe Chez (Other . fst) (head' cgs)

142 |          addPrimitives

144 |          setWorkingDir "."

145 |          when (ignoreMissingIpkg opts) $

146 |             setSession ({ ignoreMissingPkg := True } !getSession)

148 |          let ide = ideMode opts

149 |          let ideSocket = ideModeSocket opts

150 |          let outmode = if ide then IDEMode 0 stdin stdout else REPL InfoLvl

151 |          o <- newRef ROpts (REPL.Opts.defaultOpts Nothing outmode cgs)

152 |          updateEnv

153 |          fname <- case (findInputs opts) of

154 |                        Just (fname ::: Nil) => pure $ Just fname

155 |                        Nothing => pure Nothing

156 |                        Just (fname1 ::: fnames) => do

157 |                          let suggestion = nearMatchOptSuggestion fname1

158 |                          renderedSuggestion <- maybe (pure "") render suggestion

159 |                          quitWithError $

160 |                            UserError """

164 |          update ROpts { mainfile := fname }

166 |          -- start by going over the pre-options, and stop if we do not need to

167 |          -- continue

168 |          True <- preOptions opts

169 |             | False => pure ()

171 |          -- If there's a --build or --install, just do that then quit

172 |          done <- flip catch quitWithError $ processPackageOpts opts

174 |          when (not done) $ flip catch quitWithError $

175 |             do when (checkVerbose opts) $ -- override Quiet if implicitly set

176 |                    setOutput (REPL InfoLvl)

177 |                u <- newRef UST initUState

178 |                origin <- maybe

179 |                  (pure $ Virtual Interactive) (\fname => do

180 |                    modIdent <- ctxtPathToNS fname

181 |                    pure (PhysicalIdrSrc modIdent)

182 |                    ) fname

183 |                m <- newRef MD (initMetadata origin)

184 |                updateREPLOpts

185 |                session <- getSession

186 |                when (not $ nobanner session) $ do

187 |                  iputStrLn $ pretty0 banner

188 |                  when (isCons cgs) $ iputStrLn (reflow "With codegen for:" <++> hsep (pretty0 . fst <$> cgs))

189 |                fname <- if findipkg session

190 |                            then findIpkg fname

191 |                            else pure fname

192 |                setMainFile fname

193 |                result <- case fname of

194 |                     Nothing => logTime 1 "Loading prelude" $ do

195 |                                  when (not $ noprelude session) $

196 |                                    readPrelude True

197 |                                  pure Done

198 |                     Just f => logTime 1 "Loading main file" $ do

199 |                                 res <- loadMainFile f

200 |                                 displayStartupErrors res

201 |                                 pure res

203 |                doRepl <- catch (postOptions result opts)

204 |                                (\err => emitError err *> pure False)

205 |                if doRepl then

206 |                  if ide || ideSocket then

207 |                    if not ideSocket

208 |                     then do

209 |                      setOutput (IDEMode 0 stdin stdout)

210 |                      replIDE {c} {u} {m}

211 |                    else do

212 |                      let (host, port) = ideSocketModeAddress opts

213 |                      f <- coreLift $ initIDESocketFile host port

214 |                      case f of

215 |                        Left err => do

216 |                          coreLift $ putStrLn err

217 |                          coreLift $ exitWith (ExitFailure 1)

218 |                        Right file => do

219 |                          setOutput (IDEMode 0 file file)

220 |                          replIDE {c} {u} {m}

221 |                  else do

222 |                      repl {c} {u} {m}

223 |                      showTimeRecord

224 |                 else

225 |                     -- exit with an error code if there was an error, otherwise

226 |                     -- just exit

227 |                   do ropts <- get ROpts

228 |                      showTimeRecord

229 |                      whenJust (errorLine ropts) $ \ _ =>

230 |                        coreLift $ exitWith (ExitFailure 1)

232 |   where

234 |   quitWithError : {auto c : Ref Ctxt Defs} ->

235 |                 {auto s : Ref Syn SyntaxInfo} ->

236 |                 {auto o : Ref ROpts REPLOpts} ->

237 |                 Error -> Core a

238 |   quitWithError err = do

239 |     doc <- display err

240 |     msg <- render doc

241 |     coreLift (die msg)

246 | quitOpts : List CLOpt -> IO Bool

247 | quitOpts [] = pure True

248 | quitOpts (Version :: _)

249 |     = do putStrLn versionMsg

250 |          pure False

251 | quitOpts (TTCVersion :: _)

252 |     = do printLn ttcVersion

253 |          pure False

254 | quitOpts (Help Nothing :: _)

255 |     = do putStrLn usage

256 |          pure False

257 | quitOpts (Help (Just HelpLogging) :: _)

258 |     = do putStrLn helpTopics

259 |          pure False

260 | quitOpts (Help (Just HelpPragma) :: _)

261 |     = do putStrLn pragmaTopics

262 |          pure False

263 | quitOpts (_ :: opts) = quitOpts opts

266 | mainWithCodegens : List (String, Codegen) -> IO ()

267 | mainWithCodegens cgs = do

268 |   Right opts <- getCmdOpts

269 |     | Left err => do ignore $ fPutStrLn stderr $ "Error: " ++ err

270 |                      exitWith (ExitFailure 1)

271 |   continue <- quitOpts opts

272 |   when continue $ do

273 |     setupTerm

274 |     coreRun (stMain cgs opts)

275 |       (\err : Error => do ignore $ fPutStrLn stderr $ "Uncaught error: " ++ show err

276 |                           exitWith (ExitFailure 1))

277 |       (\res => pure ())