0 | module Idris.IDEMode.REPL

  2 | import Core.Directory

  3 | import Core.Metadata

  4 | import Core.Unify

  6 | import Idris.Error

  7 | import Idris.Package

  8 | import Idris.Parser

  9 | import Idris.Pretty

 10 | import Idris.REPL

 11 | import Idris.Syntax

 12 | import Idris.Version

 13 | import Idris.Doc.String

 15 | import Idris.IDEMode.Commands

 16 | import Idris.IDEMode.Holes

 17 | import Idris.IDEMode.Parser

 18 | import Idris.IDEMode.SyntaxHighlight

 19 | import Idris.IDEMode.Pretty

 21 | import Protocol.Hex

 22 | import Libraries.Utils.Path

 24 | import Data.String

 25 | import System

 26 | import System.File

 28 | import Network.FFI

 29 | import Network.Socket

 30 | import Network.Socket.Data

 31 | import Network.Socket.Raw

 33 | import TTImp.Interactive.Completion

 35 | %default covering

 38 | socketToFile : Socket -> IO (Either String File)

 39 | socketToFile (MkSocket f _ _ _) = do

 40 |   file <- FHandle <$> primIO (prim__idrnet_fdopen f "r+")

 41 |   if !(fileError file)

 42 |     then pure (Left "Failed to fdopen socket file descriptor")

 43 |     else pure (Right file)

 46 | initIDESocketFile : String -> Int -> IO (Either String File)

 47 | initIDESocketFile h p = do

 48 |   osock <- socket AF_INET Stream 0

 49 |   case osock of

 50 |     Left fail => do

 51 |       putStrLn (show fail)

 52 |       putStrLn "Failed to open socket"

 53 |       exitWith (ExitFailure 1)

 54 |     Right sock => do

 55 |       res <- bind sock (Just (Hostname h)) p

 56 |       if res /= 0

 57 |         then pure (Left ("Failed to bind socket with error: " ++ show res))

 58 |         else

 59 |           do res <- listen sock

 60 |              if res /= 0

 61 |                 then

 62 |                   pure (Left ("Failed to listen on socket with error: " ++ show res))

 63 |                else

 64 |                  do p <- getSockPort sock

 65 |                     putStrLn (show p)

 66 |                     fflush stdout

 67 |                     res <- accept sock

 68 |                     case res of

 69 |                       Left err =>

 70 |                          pure (Left ("Failed to accept on socket with error: " ++ show err))

 71 |                       Right (s, _) =>

 72 |                          socketToFile s

 74 | getChar : File -> IO Char

 75 | getChar h = do

 76 |   if !(fEOF h)

 77 |      then do

 78 |        putStrLn "Alas the file is done, aborting"

 79 |        exitWith (ExitFailure 1)

 80 |      else do

 81 |        Right chr <- fGetChar h

 82 |            | Left err => do putStrLn "Failed to read a character"

 83 |                             exitWith (ExitFailure 1)

 84 |        pure chr

 86 | getFLine : File -> IO String

 87 | getFLine h

 88 |     = do Right str <- fGetLine h

 89 |                | Left err =>

 90 |                    do putStrLn "Failed to read a line"

 91 |                       exitWith (ExitFailure 1)

 92 |          pure str

 94 | getNChars : File -> Nat -> IO (List Char)

 95 | getNChars i Z = pure []

 96 | getNChars i (S k)

 97 |     = do x <- getChar i

 98 |          xs <- getNChars i k

 99 |          pure (x :: xs)

103 | getInput : File -> IO (Maybe String, String)

104 | getInput f

105 |     = do x <- getNChars f 6

106 |          case fromHexChars (reverse x) of

107 |               Nothing =>

108 |                 do rest <- getFLine f

109 |                    pure (Nothing, pack x ++ rest)

110 |               Just num =>

111 |                 do inp <- getNChars f (integerToNat num)

112 |                    pure (Just (pack x), pack inp)

115 | todoCmd : {auto c : Ref Ctxt Defs} ->

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

117 |           String -> Core ()

118 | todoCmd cmdName = iputStrLn $ reflow $ cmdName ++ ": command not yet implemented. Hopefully soon!"

121 | data IDEResult

122 |   = REPL REPLResult

123 |   | CompletionList (List String) String

124 |   | NameList (List Name)

125 |   | FoundHoles (List Holes.Data)

126 |   | Term String   -- should be a PTerm + metadata, or SExp.

127 |   | TTTerm String -- should be a TT Term + metadata, or perhaps SExp

128 |   | NameLocList (List (Name, FC))

130 | replWrap : Core REPLResult -> Core IDEResult

131 | replWrap m = pure $ REPL !m

133 | process : {auto c : Ref Ctxt Defs} ->

134 |           {auto u : Ref UST UState} ->

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

136 |           {auto m : Ref MD Metadata} ->

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

138 |           {auto _ : Ref PostS PostSession} ->

139 |           IDECommand -> Core IDEResult

140 | process (Interpret cmd)

141 |     = replWrap $ interpret cmd

142 | process (LoadFile fname_in _)

143 |     = do let fname = case !(findIpkg (Just fname_in)) of

144 |                           Nothing => fname_in

145 |                           Just f' => f'

146 |          replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname

148 | process (NameAt name Nothing)

149 |     = do defs <- get Ctxt

150 |          glob <- lookupCtxtName (UN (mkUserName name)) (gamma defs)

151 |          let dat = map (\(name, _, gdef) => (name, gdef.location)) glob

152 |          pure (NameLocList dat)

153 | process (NameAt n (Just _))

154 |     = do todoCmd "name-at <name> <line> <column>"

155 |          pure $ REPL $ Edited $ DisplayEdit emptyDoc

156 | process (TypeOf n Nothing)

157 |     = replWrap $ Idris.REPL.process (Check (PRef replFC (UN $ mkUserName n)))

158 | process (TypeOf n (Just (l, c)))

159 |     = replWrap $ Idris.REPL.process

160 |                $ Editing (TypeAt (fromInteger l) (fromInteger c) (UN $ mkUserName n))

161 | process (CaseSplit l c n)

162 |     = replWrap $ Idris.REPL.process

163 |     $ Editing $ CaseSplit False (fromInteger l) (fromInteger c)

164 |     $ UN $ mkUserName n

165 | process (AddClause l n)

166 |     = replWrap $ Idris.REPL.process

167 |     $ Editing $ AddClause False (fromInteger l)

168 |     $ UN $ mkUserName n

169 | process (AddMissing l n)

170 |     = do todoCmd "add-missing"

171 |          pure $ REPL $ Edited $ DisplayEdit emptyDoc

172 | process (Intro l h) =

173 |    do replWrap $ Idris.REPL.process

174 |                $ Editing

175 |                $ Intro False (fromInteger l) (UN $ Basic h) {- hole name -}

176 | process (Refine l h expr) =

177 |    do let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr aPTerm

178 |         | Left err => pure $ REPL $ REPLError (pretty0 $ show err)

179 |       replWrap $ Idris.REPL.process

180 |                $ Editing

181 |                $ Refine False (fromInteger l) (UN $ Basic h) {- hole name -} e

182 | process (ExprSearch l n hs all)

183 |     = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l)

184 |                      (UN $ Basic n) (map (UN . Basic) hs.list)))

185 | process ExprSearchNext

186 |     = replWrap $ Idris.REPL.process (Editing ExprSearchNext)

187 | process (GenerateDef l n)

188 |     = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN $ Basic n) 0))

189 | process GenerateDefNext

190 |     = replWrap $ Idris.REPL.process (Editing GenerateDefNext)

191 | process (MakeLemma l n)

192 |     = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN $ mkUserName n)))

193 | process (MakeCase l n)

194 |     = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN $ mkUserName n)))

195 | process (MakeWith l n)

196 |     = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN $ mkUserName n)))

197 | process (DocsFor n modeOpt)

198 |     = replWrap $ Idris.REPL.process (Doc $ APTerm (PRef EmptyFC (UN $ mkUserName n)))

199 | process (Apropos n)

200 |     = do todoCmd "apropros"

201 |          pure $ REPL $ Printed emptyDoc

202 | process (Directive n)

203 |     = do todoCmd "directive"

204 |          pure $ REPL $ Printed emptyDoc

205 | process (WhoCalls n)

206 |     = do todoCmd "who-calls"

207 |          pure $ NameList []

208 | process (CallsWho n)

209 |     = do todoCmd "calls-who"

210 |          pure $ NameList []

211 | process (BrowseNamespace ns)

212 |     = replWrap $ Idris.REPL.process (Browse (mkNamespace ns))

213 | process (NormaliseTerm tm)

214 |     = do todoCmd "normalise-term"

215 |          pure $ Term tm

216 | process (ShowTermImplicits tm)

217 |     = do todoCmd "show-term-implicits"

218 |          pure $ Term tm

219 | process (HideTermImplicits tm)

220 |     = do todoCmd "hide-term-implicits"

221 |          pure $ Term tm

222 | process (ElaborateTerm tm)

223 |     = do todoCmd "elaborate-term"

224 |          pure $ TTTerm tm

225 | process (PrintDefinition n)

226 |     = do todoCmd "print-definition"

227 |          pure $ REPL $ Printed (pretty0 n)

228 | process (ReplCompletions line)

229 |     = do Just (ctxt, compl) <- completion line

230 |            | Nothing => pure (REPL $ REPLError $ vcat [ "I can't make sense of the completion task:", pretty0 line])

231 |          pure (CompletionList compl ctxt)

232 | process (EnableSyntax b)

233 |     = do setSynHighlightOn b

234 |          pure $ REPL $ Printed (reflow "Syntax highlight option changed to" <++> byShow b)

235 | process Version

236 |     = replWrap $ Idris.REPL.process ShowVersion

237 | process (Metavariables _)

238 |     = FoundHoles <$> getUserHolesData

239 | process GetOptions

240 |     = replWrap $ Idris.REPL.process GetOpts

242 | processCatch : {auto c : Ref Ctxt Defs} ->

243 |                {auto u : Ref UST UState} ->

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

245 |                {auto m : Ref MD Metadata} ->

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

247 |                {auto p : Ref PostS PostSession} ->

248 |                IDECommand -> Core IDEResult

249 | processCatch cmd

250 |     = do c' <- branch

251 |          u' <- get UST

252 |          s' <- get Syn

253 |          o' <- get ROpts

254 |          catch (do res <- process cmd

255 |                    commit

256 |                    pure res)

257 |                (\err => do put Ctxt c'

258 |                            put UST u'

259 |                            put Syn s'

260 |                            put ROpts o'

261 |                            msg <- perror err

262 |                            pure $ REPL $ REPLError msg)

264 | idePutStrLn : {auto c : Ref Ctxt Defs} -> File -> Integer -> String -> Core ()

265 | idePutStrLn outf i msg

266 |     = send outf $ WriteString msg i

268 | returnFromIDE : {auto c : Ref Ctxt Defs} -> File -> Integer -> IDE.ReplyPayload -> Core ()

269 | returnFromIDE outf i payload

270 |     = do send outf (Immediate payload i)

272 | printIDEResult : {auto c : Ref Ctxt Defs} -> File -> Integer -> IDE.Result -> Core ()

273 | printIDEResult outf i result

274 |   = returnFromIDE outf i $ OK result []

276 | printIDEResultWithHighlight :

277 |   {auto c : Ref Ctxt Defs} ->

278 |   File -> Integer -> (Result, List (Span Properties)) ->

279 |   Core ()

280 | printIDEResultWithHighlight outf i (result, spans) = do

282 |   returnFromIDE outf i

283 |     $ OK result spans

286 | printIDEError : Ref ROpts REPLOpts => {auto c : Ref Ctxt Defs} -> File -> Integer -> Doc IdrisAnn -> Core ()

287 | printIDEError outf i msg = returnFromIDE outf i $

288 |   uncurry IDE.Error !(renderWithDecorations annToProperties msg)

290 | Cast REPLEval String where

291 |   cast EvalTC = "typecheck"

292 |   cast NormaliseAll = "normalise"

293 |   cast Execute = "execute"

294 |   cast Scheme = "scheme"

296 | Cast REPLOpt REPLOption where

297 |   cast (ShowImplicits impl)  = MkOption "show-implicits" BOOL impl

298 |   cast (ShowNamespace ns)    = MkOption "show-namespace" BOOL ns

299 |   cast (ShowMachineNames ns) = MkOption "show-machinenames" BOOL ns

300 |   cast (ShowTypes typs)      = MkOption "show-types"     BOOL typs

301 |   cast (EvalMode mod)        = MkOption "eval"           ATOM $ cast mod

302 |   cast (Editor editor)       = MkOption "editor"         STRING editor

303 |   cast (CG str)              = MkOption "cg"             STRING str

304 |   cast (Profile p)           = MkOption "profile"        BOOL p

305 |   cast (EvalTiming p)        = MkOption "evaltiming"     BOOL p

308 | displayIDEResult : {auto c : Ref Ctxt Defs} ->

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

310 |        File -> Integer -> IDEResult -> Core ()

311 | displayIDEResult outf i  (REPL $ REPLError err)

312 |   = printIDEError outf i err

313 | displayIDEResult outf i  (REPL RequestedHelp  )

314 |   = printIDEResult outf i $ AString displayHelp

315 | displayIDEResult outf i  (REPL $ RequestedDetails details)

316 |   = printIDEResult outf i $ AString details

317 | displayIDEResult outf i  (REPL $ Evaluated x Nothing)

318 |   = printIDEResultWithHighlight outf i

319 |   $ mapFst AString

320 |    !(renderWithDecorations syntaxToProperties $ pretty x)

321 | displayIDEResult outf i  (REPL $ Evaluated x (Just y))

322 |   = printIDEResultWithHighlight outf i

323 |   $ mapFst AString

324 |    !(renderWithDecorations syntaxToProperties

325 |      $ pretty x <++> ":" <++> pretty y)

326 | displayIDEResult outf i  (REPL $ Printed xs)

327 |   = printIDEResultWithHighlight outf i

328 |   $ mapFst AString

329 |   $ !(renderWithDecorations annToProperties xs)

330 | displayIDEResult outf i (REPL (PrintedDoc xs))

331 |   = printIDEResultWithHighlight outf i

332 |   $ mapFst AString

333 |   $ !(renderWithDecorations docToProperties xs)

334 | displayIDEResult outf i  (REPL $ TermChecked x y)

335 |   = printIDEResultWithHighlight outf i

336 |   $ mapFst AString

337 |    !(renderWithDecorations syntaxToProperties

338 |      $ pretty x <++> ":" <++> pretty y)

339 | displayIDEResult outf i  (REPL $ FileLoaded x)

340 |   = printIDEResult outf i $ AUnit

341 | displayIDEResult outf i  (REPL $ ErrorLoadingFile x err)

342 |   = printIDEError outf i $ reflow "Error loading file" <++> pretty0 x <+> colon <++> pretty0 (show err)

343 | displayIDEResult outf i  (REPL $ ErrorsBuildingFile x errs)

344 |   = printIDEError outf i $ reflow "Error(s) building file" <++> pretty0 x -- messages already displayed while building

345 | displayIDEResult outf i  (REPL $ NoFileLoaded)

346 |   = printIDEError outf i $ reflow "No file can be reloaded"

347 | displayIDEResult outf i  (REPL $ CurrentDirectory dir)

348 |   = printIDEResult outf i $ AString $ "Current working directory is \"\{dir}\""

349 | displayIDEResult outf i  (REPL CompilationFailed)

350 |   = printIDEError outf i $ reflow "Compilation failed"

351 | displayIDEResult outf i  (REPL $ Compiled f)

352 |   = printIDEResult outf i $ AString "File \{f} written"

353 | displayIDEResult outf i  (REPL $ ProofFound x)

354 |   = printIDEResult outf i $ AString $ show x

355 | displayIDEResult outf i  (REPL $ Missed cases)

356 |   = printIDEResult outf i

357 |   $ AString $ showSep "\n"

358 |   $ map handleMissing' cases

359 | displayIDEResult outf i  (REPL $ CheckedTotal xs)

360 |   = printIDEResult outf i

361 |   $ AString $ showSep "\n"

362 |   $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs

363 | displayIDEResult outf i  (REPL $ LogLevelSet k)

364 |   = printIDEResult outf i

365 |   $ AString $ "Set loglevel to " ++ show k

366 | displayIDEResult outf i  (REPL $ OptionsSet opts)

367 |   = printIDEResult outf i $ AnOptionList $ map cast opts

368 | displayIDEResult outf i  (REPL $ VersionIs x)

369 |   = let (major, minor, patch) = semVer x

370 |     in printIDEResult outf i $ AVersion $ MkIdrisVersion

371 |       {major, minor, patch, tag = versionTag x}

372 | displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))

373 |   = printIDEResultWithHighlight outf i

374 |   $ mapFst AString

375 |    !(renderWithDecorations annToProperties $ xs)

376 | displayIDEResult outf i (REPL $ Edited (EditError x))

377 |   = printIDEError outf i x

378 | displayIDEResult outf i (REPL $ Edited (MadeIntro is))

379 |   = printIDEResult outf i $ AnIntroList is

380 | displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))

381 |   = printIDEResult outf i $ AMetaVarLemma $ MkMetaVarLemma

382 |       { application = pappstr

383 |       , lemma = relit lit $ show name ++ " : " ++ show pty

384 |       }

385 | displayIDEResult outf i (REPL $ Edited (MadeWith lit wapp))

386 |   = printIDEResult outf i

387 |   $ AString $ showSep "\n" (map (relit lit) wapp)

388 | displayIDEResult outf i (REPL $ (Edited (MadeCase lit cstr)))

389 |   = printIDEResult outf i

390 |   $ AString $ showSep "\n" (map (relit lit) cstr)

391 | displayIDEResult outf i (FoundHoles holes)

392 |   = printIDEResult outf i $ AHoleList $ map holeIDE holes

393 | displayIDEResult outf i (CompletionList ns r)

394 |   = printIDEResult outf i $ ACompletionList ns r

395 | displayIDEResult outf i (NameList ns)

396 |   = printIDEResult outf i $ ANameList (map show ns)

397 | displayIDEResult outf i (Term t)

398 |   = printIDEResult outf i $ AString t

399 | displayIDEResult outf i (TTTerm t)

400 |   = printIDEResult outf i $ AString t

401 | displayIDEResult outf i (REPL $ ConsoleWidthSet mn)

402 |   = let width = case mn of

403 |                     Just k  => show k

404 |                     Nothing => "auto"

405 |     in printIDEResult outf i $ AString $ "Set consolewidth to " ++ width

406 | displayIDEResult outf i (NameLocList dat)

407 |   = printIDEResult outf i $ ANameLocList $

408 |        !(traverse (constructFileContext . map toNonEmptyFC) dat)

409 |   where

410 |     -- In order to recover the full path to the module referenced by FC,

411 |     -- which stores a module identifier as opposed to a full path,

412 |     -- we need to check the project's source folder and all the library directories

413 |     -- for the relevant source file.

414 |     -- (!) Always returns the *absolute* path.

415 |     sexpOriginDesc : OriginDesc -> Core String

416 |     sexpOriginDesc (PhysicalIdrSrc modIdent) = do

417 |       defs <- get Ctxt

418 |       let wdir = defs.options.dirs.working_dir

419 |       let pkg_dirs = filter (/= ".") (defs.options.dirs.extra_dirs ++ defs.options.dirs.package_dirs)

420 |       let exts = listOfExtensionsStr

421 |       Just fname <- catch

422 |           (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first

423 |           -- if not found, try looking for the file amongst the loaded packages.

424 |           (const $ firstAvailable $ do

425 |             pkg_dir <- pkg_dirs

426 |             let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir

427 |             ext <- exts

428 |             pure (pkg_dir_abs </> ModuleIdent.toPath modIdent <.> ext))

429 |         | _ => pure "(File-Not-Found)"

430 |       pure fname

431 |     sexpOriginDesc (PhysicalPkgSrc fname) = pure fname

432 |     sexpOriginDesc (Virtual Interactive) = pure "(Interactive)"

434 |     constructFileContext : (Name, NonEmptyFC) -> Core (String, FileContext)

435 |     constructFileContext (name, origin, (startLine, startCol), (endLine, endCol)) = pure $

436 |         -- TODO: fix the emacs mode to use the more structured SExpr representation

437 |         (!(render $ pretty0 name)

438 |         , MkFileContext

439 |           { file  = !(sexpOriginDesc origin)

440 |           , range = MkBounds {startCol, startLine, endCol, endLine}

441 |           })

445 | displayIDEResult outf i (REPL Done) = printIDEResult outf i (AString "")

446 | displayIDEResult outf i (REPL (Executed {})) = printIDEResult outf i (AString "")

447 | displayIDEResult outf i (REPL (ModuleLoaded {})) = printIDEResult outf i (AString "")

448 | displayIDEResult outf i (REPL (ErrorLoadingModule {})) = printIDEResult outf i (AString "")

449 | displayIDEResult outf i (REPL (ColorSet {})) = printIDEResult outf i (AString "")

450 | displayIDEResult outf i (REPL DefDeclared) = printIDEResult outf i (AString "")

451 | displayIDEResult outf i (REPL Exited) = printIDEResult outf i (AString "")

454 | handleIDEResult : {auto c : Ref Ctxt Defs} ->

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

456 |        File -> Integer -> IDEResult -> Core ()

457 | handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!"

458 | handleIDEResult outf i other = displayIDEResult outf i other

460 | loop : {auto c : Ref Ctxt Defs} ->

461 |        {auto u : Ref UST UState} ->

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

463 |        {auto m : Ref MD Metadata} ->

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

465 |        {auto p : Ref PostS PostSession} ->

466 |        Core ()

468 |     = do res <- getOutput

469 |          case res of

470 |               REPL _ => printError $ reflow "Running idemode but output isn't"

471 |               IDEMode idx inf outf => do

472 |                 (pref, inp) <- coreLift $ getInput inf

473 |                 log "ide-mode.recv" 50 $ "Received: \{fromMaybe "" pref}\{inp}"

474 |                 end <- coreLift $ fEOF inf

475 |                 unless end $ do

476 |                   case parseSExp inp of

477 |                     Left err =>

478 |                       do printIDEError outf idx (reflow "Parse error:" <++> !(perror err))

479 |                          loop

480 |                     Right sexp =>

481 |                       case getMsg sexp of

482 |                         Just (cmd, i) =>

483 |                           do updateOutput i

484 |                              res <- processCatch cmd

485 |                              handleIDEResult outf i res

486 |                              loop

487 |                         Nothing =>

488 |                           do printIDEError outf idx (reflow "Unrecognised command:" <++> pretty0 (show sexp))

489 |                              loop

490 |   where

491 |     updateOutput : Integer -> Core ()

492 |     updateOutput idx

493 |         = do IDEMode _ i o <- getOutput

494 |                  | _ => pure ()

495 |              setOutput (IDEMode idx i o)

498 | replIDE : {auto c : Ref Ctxt Defs} ->

499 |           {auto u : Ref UST UState} ->

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

501 |           {auto m : Ref MD Metadata} ->

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

503 |           {auto p : Ref PostS PostSession} ->

504 |           Core ()

506 |     = do res <- getOutput

507 |          case res of

508 |               REPL _ => printError $ reflow "Running idemode but output isn't"

509 |               IDEMode _ inf outf => do

510 |                 send outf (ProtocolVersion 2 1) -- TODO: Move this info somewhere more central

511 |                 loop