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 |           IDECommand -> Core IDEResult

139 | process (Interpret cmd)

140 |     = replWrap $ interpret cmd

141 | process (LoadFile fname_in _)

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

143 |                           Nothing => fname_in

144 |                           Just f' => f'

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

147 | process (NameAt name Nothing)

148 |     = do defs <- get Ctxt

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

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

151 |          pure (NameLocList dat)

152 | process (NameAt n (Just _))

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

154 |          pure $ REPL $ Edited $ DisplayEdit emptyDoc

155 | process (TypeOf n Nothing)

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

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

158 |     = replWrap $ Idris.REPL.process

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

160 | process (CaseSplit l c n)

161 |     = replWrap $ Idris.REPL.process

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

163 |     $ UN $ mkUserName n

164 | process (AddClause l n)

165 |     = replWrap $ Idris.REPL.process

166 |     $ Editing $ AddClause False (fromInteger l)

167 |     $ UN $ mkUserName n

168 | process (AddMissing l n)

169 |     = do todoCmd "add-missing"

170 |          pure $ REPL $ Edited $ DisplayEdit emptyDoc

171 | process (Intro l h) =

172 |    do replWrap $ Idris.REPL.process

173 |                $ Editing

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

175 | process (Refine l h expr) =

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

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

178 |       replWrap $ Idris.REPL.process

179 |                $ Editing

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

181 | process (ExprSearch l n hs all)

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

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

184 | process ExprSearchNext

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

186 | process (GenerateDef l n)

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

188 | process GenerateDefNext

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

190 | process (MakeLemma l n)

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

192 | process (MakeCase l n)

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

194 | process (MakeWith l n)

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

196 | process (DocsFor n modeOpt)

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

198 | process (Apropos n)

199 |     = do todoCmd "apropros"

200 |          pure $ REPL $ Printed emptyDoc

201 | process (Directive n)

202 |     = do todoCmd "directive"

203 |          pure $ REPL $ Printed emptyDoc

204 | process (WhoCalls n)

205 |     = do todoCmd "who-calls"

206 |          pure $ NameList []

207 | process (CallsWho n)

208 |     = do todoCmd "calls-who"

209 |          pure $ NameList []

210 | process (BrowseNamespace ns)

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

212 | process (NormaliseTerm tm)

213 |     = do todoCmd "normalise-term"

214 |          pure $ Term tm

215 | process (ShowTermImplicits tm)

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

217 |          pure $ Term tm

218 | process (HideTermImplicits tm)

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

220 |          pure $ Term tm

221 | process (ElaborateTerm tm)

222 |     = do todoCmd "elaborate-term"

223 |          pure $ TTTerm tm

224 | process (PrintDefinition n)

225 |     = do todoCmd "print-definition"

226 |          pure $ REPL $ Printed (pretty0 n)

227 | process (ReplCompletions line)

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

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

230 |          pure (CompletionList compl ctxt)

231 | process (EnableSyntax b)

232 |     = do setSynHighlightOn b

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

234 | process Version

235 |     = replWrap $ Idris.REPL.process ShowVersion

236 | process (Metavariables _)

237 |     = FoundHoles <$> getUserHolesData

238 | process GetOptions

239 |     = replWrap $ Idris.REPL.process GetOpts

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

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

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

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

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

246 |                IDECommand -> Core IDEResult

247 | processCatch cmd

248 |     = do c' <- branch

249 |          u' <- get UST

250 |          s' <- get Syn

251 |          o' <- get ROpts

252 |          catch (do res <- process cmd

253 |                    commit

254 |                    pure res)

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

256 |                            put UST u'

257 |                            put Syn s'

258 |                            put ROpts o'

259 |                            msg <- perror err

260 |                            pure $ REPL $ REPLError msg)

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

263 | idePutStrLn outf i msg

264 |     = send outf $ WriteString msg i

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

267 | returnFromIDE outf i payload

268 |     = do send outf (Immediate payload i)

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

271 | printIDEResult outf i result

272 |   = returnFromIDE outf i $ OK result []

274 | printIDEResultWithHighlight :

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

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

277 |   Core ()

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

280 |   returnFromIDE outf i

281 |     $ OK result spans

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

285 | printIDEError outf i msg = returnFromIDE outf i $

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

288 | Cast REPLEval String where

289 |   cast EvalTC = "typecheck"

290 |   cast NormaliseAll = "normalise"

291 |   cast Execute = "execute"

292 |   cast Scheme = "scheme"

294 | Cast REPLOpt REPLOption where

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

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

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

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

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

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

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

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

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

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

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

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

309 | displayIDEResult outf i  (REPL $ REPLError err)

310 |   = printIDEError outf i err

311 | displayIDEResult outf i  (REPL RequestedHelp  )

312 |   = printIDEResult outf i $ AString displayHelp

313 | displayIDEResult outf i  (REPL $ RequestedDetails details)

314 |   = printIDEResult outf i $ AString details

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

316 |   = printIDEResultWithHighlight outf i

317 |   $ mapFst AString

318 |    !(renderWithDecorations syntaxToProperties $ pretty x)

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

320 |   = printIDEResultWithHighlight outf i

321 |   $ mapFst AString

322 |    !(renderWithDecorations syntaxToProperties

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

324 | displayIDEResult outf i  (REPL $ Printed xs)

325 |   = printIDEResultWithHighlight outf i

326 |   $ mapFst AString

327 |   $ !(renderWithDecorations annToProperties xs)

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

329 |   = printIDEResultWithHighlight outf i

330 |   $ mapFst AString

331 |   $ !(renderWithDecorations docToProperties xs)

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

333 |   = printIDEResultWithHighlight outf i

334 |   $ mapFst AString

335 |    !(renderWithDecorations syntaxToProperties

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

337 | displayIDEResult outf i  (REPL $ FileLoaded x)

338 |   = printIDEResult outf i $ AUnit

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

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

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

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

343 | displayIDEResult outf i  (REPL $ NoFileLoaded)

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

345 | displayIDEResult outf i  (REPL $ CurrentDirectory dir)

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

347 | displayIDEResult outf i  (REPL CompilationFailed)

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

349 | displayIDEResult outf i  (REPL $ Compiled f)

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

351 | displayIDEResult outf i  (REPL $ ProofFound x)

352 |   = printIDEResult outf i $ AString $ show x

353 | displayIDEResult outf i  (REPL $ Missed cases)

354 |   = printIDEResult outf i

355 |   $ AString $ showSep "\n"

356 |   $ map handleMissing' cases

357 | displayIDEResult outf i  (REPL $ CheckedTotal xs)

358 |   = printIDEResult outf i

359 |   $ AString $ showSep "\n"

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

361 | displayIDEResult outf i  (REPL $ LogLevelSet k)

362 |   = printIDEResult outf i

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

364 | displayIDEResult outf i  (REPL $ OptionsSet opts)

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

366 | displayIDEResult outf i  (REPL $ VersionIs x)

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

368 |     in printIDEResult outf i $ AVersion $ MkIdrisVersion

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

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

371 |   = printIDEResultWithHighlight outf i

372 |   $ mapFst AString

373 |    !(renderWithDecorations annToProperties $ xs)

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

375 |   = printIDEError outf i x

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

377 |   = printIDEResult outf i $ AnIntroList is

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

379 |   = printIDEResult outf i $ AMetaVarLemma $ MkMetaVarLemma

380 |       { application = pappstr

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

382 |       }

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

384 |   = printIDEResult outf i

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

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

387 |   = printIDEResult outf i

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

389 | displayIDEResult outf i (FoundHoles holes)

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

391 | displayIDEResult outf i (CompletionList ns r)

392 |   = printIDEResult outf i $ ACompletionList ns r

393 | displayIDEResult outf i (NameList ns)

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

395 | displayIDEResult outf i (Term t)

396 |   = printIDEResult outf i $ AString t

397 | displayIDEResult outf i (TTTerm t)

398 |   = printIDEResult outf i $ AString t

399 | displayIDEResult outf i (REPL $ ConsoleWidthSet mn)

400 |   = let width = case mn of

401 |                     Just k  => show k

402 |                     Nothing => "auto"

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

404 | displayIDEResult outf i (NameLocList dat)

405 |   = printIDEResult outf i $ ANameLocList $

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

407 |   where

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

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

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

411 |     -- for the relevant source file.

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

413 |     sexpOriginDesc : OriginDesc -> Core String

414 |     sexpOriginDesc (PhysicalIdrSrc modIdent) = do

415 |       defs <- get Ctxt

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

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

418 |       let exts = listOfExtensionsStr

419 |       Just fname <- catch

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

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

422 |           (const $ firstAvailable $ do

423 |             pkg_dir <- pkg_dirs

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

425 |             ext <- exts

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

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

428 |       pure fname

429 |     sexpOriginDesc (PhysicalPkgSrc fname) = pure fname

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

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

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

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

435 |         (!(render $ pretty0 name)

436 |         , MkFileContext

437 |           { file  = !(sexpOriginDesc origin)

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

439 |           })

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

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

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

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

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

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

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

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

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

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

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

456 | handleIDEResult outf i other = displayIDEResult outf i other

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

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

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

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

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

463 |        Core ()

465 |     = do res <- getOutput

466 |          case res of

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

468 |               IDEMode idx inf outf => do

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

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

471 |                 end <- coreLift $ fEOF inf

472 |                 unless end $ do

473 |                   case parseSExp inp of

474 |                     Left err =>

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

476 |                          loop

477 |                     Right sexp =>

478 |                       case getMsg sexp of

479 |                         Just (cmd, i) =>

480 |                           do updateOutput i

481 |                              res <- processCatch cmd

482 |                              handleIDEResult outf i res

483 |                              loop

484 |                         Nothing =>

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

486 |                              loop

487 |   where

488 |     updateOutput : Integer -> Core ()

489 |     updateOutput idx

490 |         = do IDEMode _ i o <- getOutput

491 |                  | _ => pure ()

492 |              setOutput (IDEMode idx i o)

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

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

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

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

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

500 |           Core ()

502 |     = do res <- getOutput

503 |          case res of

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

505 |               IDEMode _ inf outf => do

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

507 |                 loop