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 | public export

 37 | CustomBackends : Type

 38 | CustomBackends = List (String, Codegen)

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

 41 | findInputs [] = Nothing

 42 | findInputs (InputFile f :: fs) =

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

 44 |   in  Just (f ::: rest)

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

 47 | splitPaths : String -> List1 String

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

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

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

 53 |             Core ()

 55 |     = do defs <- get Ctxt

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

 57 |          when noColor $ setColor False

 58 |          bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"

 59 |          setPrefix (fromMaybe yprefix bprefix)

 60 |          bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"

 61 |          whenJust bpath $ traverseList1_ addExtraDir . splitPaths

 62 |          bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"

 63 |          whenJust bdata $ traverseList1_ addDataDir . splitPaths

 64 |          blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"

 65 |          whenJust blibs $ traverseList1_ addLibDir . splitPaths

 66 |          pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"

 67 |          whenJust pdirs $ traverseList1_ addPackageSearchPath . splitPaths

 68 |          cg <- coreLift $ idrisGetEnv "IDRIS2_CG"

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

 70 |            Just cg => setCG cg

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

 72 |          inccgs <- coreLift $ idrisGetEnv "IDRIS2_INC_CGS"

 73 |          whenJust inccgs $ \ cgs =>

 74 |            traverseList1_ (setIncrementalCG False) $

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

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

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

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

 79 |          -- version

 80 |          defs <- get Ctxt

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

 82 |          -- added by the user with IDRIS2_PACKAGE_PATH)

 83 |          addPackageSearchPath !pkgGlobalDirectory

 84 |          -- These might fail while bootstrapping

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

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

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

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

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

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

 91 |          Just cwd <- coreLift $ currentDir

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

 93 |          addLibDir cwd

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

 96 |                  Core ()

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

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

103 | data Entrypoint

104 |   = Normal CustomBackends (List CLOpt)

105 |   | Yaffle String

106 |   | TTM String

108 | parameters (backends : CustomBackends) (allOpts : List CLOpt)

110 |   -- Yaffle and TTM are mutually incompatible so we parse the flags here and

111 |   -- report the error if it occurs. If neither flag is present we run in normal mode

113 |   parseCompilerMode' : List CLOpt -> Maybe Entrypoint -> Either String Entrypoint

114 |   parseCompilerMode' [] Nothing = pure $ Normal backends allOpts

115 |   parseCompilerMode' [] (Just m) = pure m

116 |   parseCompilerMode' (Yaffle f :: xs) Nothing = parseCompilerMode' xs (Just $ Yaffle f)

117 |   parseCompilerMode' (Metadata f :: xs) Nothing = parseCompilerMode' xs (Just $ TTM f)

118 |   parseCompilerMode' (Yaffle _ :: xs) (Just (TTM _)) = Left "Incompatible modes --ttm and --yaffle"

119 |   parseCompilerMode' (Metadata _ :: xs) (Just (Yaffle _)) = Left "Incompatible modes --ttm and --yaffle"

120 |   parseCompilerMode' (_ :: xs) m = parseCompilerMode' xs m

122 |   parseCompilerMode : Either String Entrypoint

123 |   parseCompilerMode = parseCompilerMode' allOpts Nothing

125 | ignoreMissingIpkg : List CLOpt -> Bool

126 | ignoreMissingIpkg [] = False

127 | ignoreMissingIpkg (IgnoreMissingIPKG :: _) = True

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

130 | banner : String

131 | banner = #"""

141 | checkVerbose : List CLOpt -> Bool

142 | checkVerbose [] = False

143 | checkVerbose (Verbose :: _) = True

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

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

147 | stMain cgs opts

148 |     = do defs <- initDefs

149 |          -- Add the manually added codegens to the option set

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

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

152 |          s <- newRef Syn initSyntax

153 |          -- If we give a custom codegen, set that as the default,

154 |          -- otherwise, use Chez

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

156 |          addPrimitives

158 |          setWorkingDir "."

159 |          when (ignoreMissingIpkg opts) $

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

162 |          let ide = ideMode opts

163 |          let ideSocket = ideModeSocket opts

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

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

166 |          updateEnv

167 |          fname <- case (findInputs opts) of

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

169 |                        Nothing => pure Nothing

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

171 |                          let suggestion = nearMatchOptSuggestion fname1

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

173 |                          quitWithError $

174 |                            UserError """

178 |          update ROpts { mainfile := fname }

180 |          s <- newRef PostS defaultPost

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

182 |          -- continue

183 |          Continue <- preOptions opts

184 |             | Abort => pure ()

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

187 |          Continue <- flip catch quitWithError $ processPackageOpts opts

188 |             | Abort => pure ()

190 |          flip catch quitWithError $

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

192 |                    setOutput (REPL InfoLvl)

193 |                u <- newRef UST initUState

194 |                origin <- maybe

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

196 |                    modIdent <- ctxtPathToNS fname

197 |                    pure (PhysicalIdrSrc modIdent)

198 |                    ) fname

199 |                m <- newRef MD (initMetadata origin)

200 |                updateREPLOpts

201 |                session <- getSession

202 |                when (not $ nobanner session) $ do

203 |                  iputStrLn $ pretty0 banner

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

205 |                fname <- if findipkg session

206 |                            then findIpkg fname

207 |                            else pure fname

208 |                setMainFile fname

209 |                result <- case fname of

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

211 |                                  when (not $ noprelude session) $

212 |                                    readPrelude True

213 |                                  pure Done

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

215 |                                 res <- loadMainFile f

216 |                                 displayStartupErrors res

217 |                                 pure res

219 |                post <- get PostS

220 |                Continue <- catch (postOptions result post)

221 |                                (\err => emitError err *> pure Abort)

222 |                 | Abort => do

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

224 |                     -- just exit

225 |                      ropts <- get ROpts

226 |                      showTimeRecord

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

228 |                        coreLift $ exitWith (ExitFailure 1)

229 |                if ide || ideSocket then

230 |                    if not ideSocket

231 |                     then do

232 |                      setOutput (IDEMode 0 stdin stdout)

233 |                      replIDE {c} {u} {m}

234 |                    else do

235 |                      let (host, port) = ideSocketModeAddress opts

236 |                      f <- coreLift $ initIDESocketFile host port

237 |                      case f of

238 |                        Left err => do

239 |                          coreLift $ putStrLn err

240 |                          coreLift $ exitWith (ExitFailure 1)

241 |                        Right file => do

242 |                          setOutput (IDEMode 0 file file)

243 |                          replIDE {c} {u} {m}

244 |                  else do

245 |                      repl {c} {u} {m}

246 |                      showTimeRecord

248 |   where

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

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

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

253 |                 Error -> Core a

254 |   quitWithError err = do

255 |     doc <- display err

256 |     msg <- render doc

257 |     coreLift (die msg)

259 | allMain : Entrypoint -> Core ()

260 | allMain (Normal cgs opts) = stMain cgs opts

261 | allMain (Yaffle f) = yaffleMain f []

262 | allMain (TTM f) = dumpTTM f

267 | quitOpts : List CLOpt -> IO ControlFlow

268 | quitOpts [] = pure Continue

269 | quitOpts (Version :: _)

270 |     = do putStrLn versionMsg

271 |          pure Abort

272 | quitOpts (TTCVersion :: _)

273 |     = do printLn ttcVersion

274 |          pure Abort

275 | quitOpts (Help Nothing :: _)

276 |     = do putStrLn usage

277 |          pure Abort

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

279 |     = do putStrLn helpTopics

280 |          pure Abort

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

282 |     = do putStrLn pragmaTopics

283 |          pure Abort

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

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

288 | mainWithCodegens cgs = do

289 |   Right opts <- getCmdOpts

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

291 |                      exitWith (ExitFailure 1)

292 |   Continue <- quitOpts opts

293 |     | Abort => pure ()

294 |   setupTerm

295 |   let Right cliMode = parseCompilerMode cgs opts

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

297 |                      exitWith (ExitFailure 1)

298 |   coreRun (allMain cliMode)

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

300 |                         exitWith (ExitFailure 1))

301 |     (\res => pure ())