674c8b8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

IdeSlave mode improvements:

- introduce iResult and iFail to report success and failure of a REPLcommand - send warnings for occuring warnings during parsing / typechecking - introduce ideslaveProcess function, which guards process with iResult/iFail (and does not support all operations) - revert commit which removed IState from ideslaveStart/ideslave functions

commit674c8b8127b0094f3486d4e4a434fad2a65ba91e authorHannes Mehnert <hannes@mehnert.org> dateSat 11 May 2013, 20:59 (13 years ago) parent2253212

3 files changed+173−88

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+31−2 src/Idris/IdeSlave.hs+8−12 src/Idris/REPL.hs+134−74

src/Idris/AbsSyntax.hs+31−2

@@ -241,14 +241,43 @@ solveDeferred :: Name -> Idris ()

241241solveDeferred n = do i <- getIState

242242 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

243243

244+iResult :: String -> Idris ()

245+iResult s = do i <- getIState

246+ case idris_outputmode i of

247+ RawOutput -> case s of

248+ "" -> return ()

249+ s -> liftIO $ putStrLn s

250+ IdeSlave n ->

251+ let good = List [SymbolAtom "ok", toSExp s] in

252+ liftIO $ putStrLn $ convSExp "return" good n

253+

254+iFail :: String -> Idris ()

255+iFail s = do i <- getIState

256+ case idris_outputmode i of

257+ RawOutput -> case s of

258+ "" -> return ()

259+ s -> liftIO $ putStrLn s

260+ IdeSlave n ->

261+ let good = List [SymbolAtom "error", toSExp s] in

262+ liftIO $ putStrLn $ convSExp "return" good n

263+

244264iputStrLn :: String -> Idris ()

245265iputStrLn s = do i <- getIState

246266 case idris_outputmode i of

247267 RawOutput -> liftIO $ putStrLn s

248− IdeSlave n -> liftIO $ putStrLn $ convSExp "write-string" s n

268+ IdeSlave n ->

269+ case span (/=':') s of

270+ (fn, ':':rest) -> case span isDigit rest of

271+ ([], ':':msg) -> iWarn (FC fn 0) msg

272+ ([], msg) -> iWarn (FC fn 0) msg

273+ (num, ':':msg) -> iWarn (FC fn (read num)) msg

274+ _ -> liftIO $ putStrLn $ convSExp "write-string" s n

249275

250276iWarn :: FC -> String -> Idris ()

251−iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)

277+iWarn fc err = do i <- getIState

278+ case idris_outputmode i of

279+ RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)

280+ IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

252281

253282setLogLevel :: Int -> Idris ()

254283setLogLevel l = do i <- getIState

src/Idris/IdeSlave.hs+8−12

@@ -1,6 +1,6 @@

11{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

3−module Idris.IdeSlave(receiveMessage, sendMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, SExp(..)) where

3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..)) where

55import Text.Printf

66import Numeric

@@ -55,6 +55,9 @@ instance (SExpable a) => SExpable [a] where

5555instance (SExpable a, SExpable b) => SExpable (a, b) where

5656 toSExp (l, r) = List [toSExp l, toSExp r]

5757

58+instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

59+ toSExp (l, m, n) = List [toSExp l, toSExp m, toSExp n]

60+

5861escape :: String -> String

5962escape = concatMap escapeChar

6063 where

@@ -96,10 +99,10 @@ sexpToCommand (List [SymbolAtom "repl-completions", StringAtom prefix]) = Just (

9699sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

97100sexpToCommand _ = Nothing

98101

99−receiveMessage :: String -> (SExp, Integer)

100−receiveMessage x = case receiveString x of

101− (List [cmd, (IntegerAtom id)]) ->

102− (cmd, id)

102+parseMessage :: String -> (SExp, Integer)

103+parseMessage x = case receiveString x of

104+ (List [cmd, (IntegerAtom id)]) ->

105+ (cmd, id)

103106

104107receiveString :: String -> SExp

105108receiveString x =

@@ -119,12 +122,5 @@ convSExp pre s id =

119122 let str = sExpToString sex in

120123 (getHexLength str) ++ str

121124

122−sendMessage :: SExpable a => Integer -> Either a a -> String

123−sendMessage id s =

124− let sexp = case s of

125− Left err -> List [SymbolAtom "error", toSExp err]

126− Right succ -> List [SymbolAtom "ok", toSExp succ]

127− in convSExp "return" sexp id

128−

129125getHexLength :: String -> String

130126getHexLength s = printf "%06x" (1 + (length s))

src/Idris/REPL.hs+134−74

@@ -82,45 +82,102 @@ repl orig mods

8282 repl orig mods

8383

8484-- | Run the IdeSlave

85−ideslaveStart :: [FilePath] -> Idris ()

86−ideslaveStart mods

85+ideslaveStart :: IState -> [FilePath] -> Idris ()

86+ideslaveStart orig mods

8787 = do i <- getIState

8888 case idris_outputmode i of

8989 IdeSlave n ->

9090 when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)

91− ideslave mods

91+ ideslave orig mods

9292

9393

94−ideslave :: [FilePath] -> Idris ()

95−ideslave mods

94+ideslave :: IState -> [FilePath] -> Idris ()

95+ideslave orig mods

9696 = do idrisCatch

9797 (do l <- liftIO $ getLine

98− let (sexp, id) = receiveMessage l

98+ let (sexp, id) = parseMessage l

9999 i <- getIState

100100 putIState $ i { idris_outputmode = (IdeSlave id) }

101101 case sexpToCommand sexp of

102102 Just (Interpret cmd) ->

103− do i <- getIState

104− let fn = case mods of

105− (f:_) -> f

106− _ -> ""

103+ do let fn = case mods of

104+ (f:_) -> f

105+ _ -> ""

107106 case parseCmd i cmd of

108− Left err -> do liftIO $ putStrLn $ sendMessage id (Left (show err))

109− Right cmd -> do idrisCatch

110− (do xs <- process fn cmd

111− liftIO $ putStrLn $ sendMessage id (Right (xs, "no output")))

112− (\e -> do liftIO $ putStrLn $ sendMessage id (Left (show e)))

107+ Left err -> iFail $ show err

108+ Right cmd -> idrisCatch

109+ (do ideslaveProcess fn cmd)

110+ (\e -> do iFail $ show e)

113111 Just (REPLCompletions str) ->

114112 do (unused, compls) <- replCompletion (reverse str, "")

115− liftIO $ putStrLn $ sendMessage id (Right (map replacement compls, reverse unused))

116− Just (LoadFile filename) -> do clearErr

117− mod <- loadModule filename

118− liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id

119− liftIO $ putStrLn $ sendMessage id (Right (SymbolAtom "good"))

120− ideslave [filename]

121− Nothing -> do liftIO $ putStrLn $ sendMessage id (Left "did not understand"))

122− (\e -> do liftIO $ putStrLn $ sendMessage 0 (Left (show e)))

123− ideslave mods

113+ let good = List [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

114+ liftIO $ putStrLn $ convSExp "return" good id

115+ Just (LoadFile filename) ->

116+ do clearErr

117+ putIState (orig { idris_options = idris_options i,

118+ idris_outputmode = (IdeSlave id) })

119+ loadModule filename

120+ iucheck

121+ liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id

122+ -- report success! or failure!

123+ ideslave orig [filename]

124+ Nothing -> do iFail "did not understand")

125+ (\e -> do iFail $ show e)

126+ ideslave orig mods

127+

128+ideslaveProcess :: FilePath -> Command -> Idris ()

129+ideslaveProcess fn Help = process fn Help

130+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

131+ iResult "changed directory to"

132+ideslaveProcess fn (Eval t) = process fn (Eval t)

133+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

134+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

135+ideslaveProcess fn (Check t) = process fn (Check t)

136+ideslaveProcess fn (DocStr n) = process fn (DocStr n)

137+ideslaveProcess fn Universes = process fn Universes

138+ideslaveProcess fn (Defn n) = do process fn (Defn n)

139+ iResult ""

140+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

141+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

142+ iResult ""

143+ideslaveProcess fn (Info n) = process fn (Info n)

144+ideslaveProcess fn (Search t) = process fn (Search t)

145+ideslaveProcess fn (Spec t) = process fn (Spec t)

146+-- RmProof and AddProof not supported!

147+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

148+ideslaveProcess fn (Prove n') = process fn (Prove n')

149+ideslaveProcess fn (HNF t) = process fn (HNF t)

150+--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

151+

152+--that most likely does not work, since we need to wrap

153+--input/output of the executed binary...

154+ideslaveProcess fn Execute = do process fn Execute

155+ iResult ""

156+ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)

157+ iResult ""

158+ideslaveProcess fn (Compile target f) = do process fn (Compile target f)

159+ iResult ""

160+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

161+ iResult ""

162+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

163+ideslaveProcess fn (Missing n) = process fn (Missing n)

164+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

165+ iResult ""

166+ideslaveProcess fn ListDynamic = do process fn ListDynamic

167+ iResult ""

168+ideslaveProcess fn Metavars = process fn Metavars

169+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

170+ iResult ""

171+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

172+ iResult ""

173+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

174+ iResult ""

175+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

176+ iResult ""

177+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

178+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

179+ideslaveProcess fn _ = iFail "command not recognized or not supported"

180+

124181

125182-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

126183mkPrompt [] = "Idris"

@@ -215,25 +272,25 @@ proofs orig

215272

216273insertScript :: String -> [String] -> [String]

217274insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]

218−insertScript prf (p@"---------- Proofs ----------" : "" : xs)

275+insertScript prf (p@"---------- Proofs ----------" : "" : xs)

219276 = p : "" : prf : xs

220277insertScript prf (x : xs) = x : insertScript prf xs

221278

222279process :: FilePath -> Command -> Idris ()

223−process fn Help = iputStrLn displayHelp

280+process fn Help = iResult displayHelp

224281process fn (ChangeDirectory f)

225282 = do liftIO $ setCurrentDirectory f

226283 return ()

227−process fn (Eval t)

284+process fn (Eval t)

228285 = do (tm, ty) <- elabVal toplevel False t

229286 ctxt <- getContext

230− ist <- getIState

287+ ist <- getIState

231288 let tm' = normaliseAll ctxt [] tm

232289 let ty' = normaliseAll ctxt [] ty

233290 logLvl 3 $ "Raw: " ++ show (tm', ty')

234291 imp <- impShow

235− iputStrLn (showImp imp (delab ist tm') ++ " : " ++

236− showImp imp (delab ist ty'))

292+ iResult (showImp imp (delab ist tm') ++ " : " ++

293+ showImp imp (delab ist ty'))

237294process fn (ExecVal t)

238295 = do ctxt <- getContext

239296 ist <- getIState

@@ -242,30 +299,31 @@ process fn (ExecVal t)

242299 let ty' = normaliseAll ctxt [] ty

243300 res <- execute tm

244301 imp <- impShow

245− iputStrLn (showImp imp (delab ist res) ++ " : " ++

246− showImp imp (delab ist ty'))

247− return ()

302+ iResult (showImp imp (delab ist res) ++ " : " ++

303+ showImp imp (delab ist ty'))

248304process fn (Check (PRef _ n))

249305 = do ctxt <- getContext

250306 ist <- getIState

251307 imp <- impShow

252308 case lookupNames n ctxt of

253− ts@(_:_) -> mapM_ (\n -> iputStrLn $ show n ++ " : " ++

254− showImp imp (delabTy ist n)) ts

255− [] -> iputStrLn $ "No such variable " ++ show n

309+ ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++

310+ showImp imp (delabTy ist n)) ts

311+ iResult ""

312+ [] -> iFail $ "No such variable " ++ show n

256313process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

257314 ctxt <- getContext

258− ist <- getIState

315+ ist <- getIState

259316 imp <- impShow

260317 let ty' = normaliseC ctxt [] ty

261− iputStrLn (showImp imp (delab ist tm) ++ " : " ++

262− showImp imp (delab ist ty))

318+ iResult (showImp imp (delab ist tm) ++ " : " ++

319+ showImp imp (delab ist ty))

263320

264321process fn (DocStr n) = do i <- getIState

265322 case lookupCtxtName n (idris_docstrings i) of

266− [] -> iputStrLn $ "No documentation for " ++ show n

267− ns -> mapM_ showDoc ns

268− where showDoc (n, d)

323+ [] -> iFail $ "No documentation for " ++ show n

324+ ns -> do mapM_ showDoc ns

325+ iResult ""

326+ where showDoc (n, d)

269327 = do doc <- getDocs n

270328 iputStrLn $ show doc

271329process fn Universes = do i <- getIState

@@ -275,8 +333,8 @@ process fn Universes = do i <- getIState

275333 let n = length cs

276334 iputStrLn $ "(" ++ show n ++ " constraints)"

277335 case ucheck cs of

278− Error e -> iputStrLn $ pshow i e

279− OK _ -> iputStrLn "Universes OK"

336+ Error e -> iFail $ pshow i e

337+ OK _ -> iResult "Universes OK"

280338process fn (Defn n) = do i <- getIState

281339 iputStrLn "Compiled patterns:\n"

282340 liftIO $ print (lookupDef n (tt_ctxt i))

@@ -287,14 +345,15 @@ process fn (Defn n) = do i <- getIState

287345 case lookupTotal n (tt_ctxt i) of

288346 [t] -> iputStrLn (showTotal t i)

289347 _ -> return ()

290− where printCase i (_, lhs, rhs)

348+ where printCase i (_, lhs, rhs)

291349 = do iputStrLn (showImp True (delab i lhs) ++ " = " ++

292350 showImp True (delab i rhs))

293351process fn (TotCheck n) = do i <- getIState

294352 case lookupTotal n (tt_ctxt i) of

295− [t] -> iputStrLn (showTotal t i)

296− _ -> return ()

297−process fn (DebugInfo n)

353+ [t] -> iResult (showTotal t i)

354+ _ -> do iFail ""

355+ return ()

356+process fn (DebugInfo n)

298357 = do i <- getIState

299358 let oi = lookupCtxtName n (idris_optimisation i)

300359 when (not (null oi)) $ iputStrLn (show oi)

@@ -316,13 +375,13 @@ process fn (DebugInfo n)

316375process fn (Info n) = do i <- getIState

317376 case lookupCtxt n (idris_classes i) of

318377 [c] -> classInfo c

319− _ -> iputStrLn "Not a class"

320−process fn (Search t) = iputStrLn "Not implemented"

378+ _ -> iFail "Not a class"

379+process fn (Search t) = iFail "Not implemented"

321380process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

322381 ctxt <- getContext

323382 ist <- getIState

324383 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm

325− iputStrLn (show (delab ist tm'))

384+ iResult (show (delab ist tm'))

326385

327386process fn (RmProof n')

328387 = do i <- getIState

@@ -374,8 +433,8 @@ process fn (ShowProof n')

374433 n <- resolveProof n'

375434 let proofs = proof_list i

376435 case lookup n proofs of

377− Nothing -> iputStrLn "No proof to show"

378− Just p -> iputStrLn $ showProof False n p

436+ Nothing -> iFail "No proof to show"

437+ Just p -> iResult $ showProof False n p

379438

380439process fn (Prove n')

381440 = do ctxt <- getContext

@@ -395,13 +454,13 @@ process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

395454 ctxt <- getContext

396455 ist <- getIState

397456 let tm' = hnf ctxt [] tm

398− iputStrLn (show (delab ist tm'))

457+ iResult (show (delab ist tm'))

399458process fn TTShell = do ist <- getIState

400459 let shst = initState (tt_ctxt ist)

401460 runShell shst

402461 return ()

403−process fn Execute = do (m, _) <- elabVal toplevel False

404− (PApp fc

462+process fn Execute = do (m, _) <- elabVal toplevel False

463+ (PApp fc

405464 (PRef fc (UN "run__IO"))

406465 [pexp $ PRef fc (NS (UN "main") ["Main"])])

407466-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

@@ -411,37 +470,37 @@ process fn Execute = do (m, _) <- elabVal toplevel False

411470 compile t tmpn m

412471 liftIO $ system tmpn

413472 return ()

414− where fc = FC "main" 0

415−process fn (NewCompile f)

473+ where fc = FC "main" 0

474+process fn (NewCompile f)

416475 = do (m, _) <- elabVal toplevel False

417476 (PApp fc (PRef fc (UN "run__IO"))

418477 [pexp $ PRef fc (NS (UN "main") ["Main"])])

419478 compileEpic f m

420− where fc = FC "main" 0

421−process fn (Compile target f)

479+ where fc = FC "main" 0

480+process fn (Compile target f)

422481 = do (m, _) <- elabVal toplevel False

423482 (PApp fc (PRef fc (UN "run__IO"))

424483 [pexp $ PRef fc (NS (UN "main") ["Main"])])

425484 compile target f m

426− where fc = FC "main" 0

427−process fn (LogLvl i) = setLogLevel i

485+ where fc = FC "main" 0

486+process fn (LogLvl i) = setLogLevel i

428487-- Elaborate as if LHS of a pattern (debug command)

429−process fn (Pattelab t)

488+process fn (Pattelab t)

430489 = do (tm, ty) <- elabVal toplevel True t

431− iputStrLn $ show tm ++ "\n\n : " ++ show ty

490+ iResult $ show tm ++ "\n\n : " ++ show ty

432491

433−process fn (Missing n)

492+process fn (Missing n)

434493 = do i <- getIState

435494 case lookupCtxt n (idris_patdefs i) of

436495 [] -> return ()

437− [(_, tms)] ->

438− iputStrLn (showSep "\n" (map (showImp True) tms))

439− _ -> iputStrLn $ "Ambiguous name"

496+ [(_, tms)] ->

497+ iResult (showSep "\n" (map (showImp True) tms))

498+ _ -> iFail $ "Ambiguous name"

440499process fn (DynamicLink l) = do i <- getIState

441500 let lib = trim l

442501 handle <- lift $ tryLoadLib lib

443502 case handle of

444− Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""

503+ Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""

445504 Just x -> do let libs = idris_dynamic_libs i

446505 putIState $ i { idris_dynamic_libs = x:libs }

447506 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

@@ -454,8 +513,8 @@ process fn Metavars

454513 = do ist <- getIState

455514 let mvs = idris_metavars ist \\ primDefs

456515 case mvs of

457− [] -> iputStrLn "No global metavariables to solve"

458− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

516+ [] -> iFail "No global metavariables to solve"

517+ _ -> iResult $ "Global metavariables:\n\t" ++ show mvs

459518process fn NOP = return ()

460519

461520process fn (SetOpt ErrContext) = setErrContext True

@@ -463,8 +522,8 @@ process fn (UnsetOpt ErrContext) = setErrContext False

463522process fn (SetOpt ShowImpl) = setImpShow True

464523process fn (UnsetOpt ShowImpl) = setImpShow False

465524

466−process fn (SetOpt _) = iputStrLn "Not a valid option"

467−process fn (UnsetOpt _) = iputStrLn "Not a valid option"

525+process fn (SetOpt _) = iFail "Not a valid option"

526+process fn (UnsetOpt _) = iFail "Not a valid option"

468527

469528

470529classInfo :: ClassInfo -> Idris ()

@@ -473,6 +532,7 @@ classInfo ci = do iputStrLn "Methods:\n"

473532 iputStrLn ""

474533 iputStrLn "Instances:\n"

475534 mapM_ dumpInstance (class_instances ci)

535+ iResult ""

476536

477537dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

478538dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

@@ -622,7 +682,7 @@ idrisMain opts =

622682 [] -> return ()

623683 (o:_) -> process "" (NewCompile o)

624684 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs

625− when (idesl) $ ideslaveStart inputs

685+ when (idesl) $ ideslaveStart ist inputs

626686 ok <- noErrors

627687 when (not ok) $ liftIO (exitWith (ExitFailure 1))

628688 where