0b5bd21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #398 from hannesm/ideslave-prover

0b5bd21Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+21−3

compare with master

unifiedsplit

@@ -264,7 +264,7 @@ iFail s = do i <- getIState

264 s -> liftIO $ putStrLn s

265 IdeSlave n ->

266 let good = SexpList [SymbolAtom "error", toSExp s] in

267− liftIO $ putStrLn $ convSExp "return" good n

267+ liftIO . putStrLn $ convSExp "return" good n

268

269iputStrLn :: String -> Idris ()

270iputStrLn s = do i <- getIState

@@ -277,13 +277,31 @@ iputStrLn s = do i <- getIState

277 ([], msg) -> write

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

279 _ -> write

280− where write = liftIO $ putStrLn $ convSExp "write-string" s n

280+ where write = liftIO . putStrLn $ convSExp "write-string" s n

281+

282+ideslavePutSExp :: SExpable a => String -> a -> Idris ()

283+ideslavePutSExp cmd info = do i <- getIState

284+ case idris_outputmode i of

285+ IdeSlave n -> liftIO . putStrLn $ convSExp cmd info n

286+ _ -> return ()

287+

288+-- this needs some typing magic and more structured output towards emacs

289+iputGoal :: String -> Idris ()

290+iputGoal s = do i <- getIState

291+ case idris_outputmode i of

292+ RawOutput -> liftIO $ putStrLn s

293+ IdeSlave n -> liftIO . putStrLn $ convSExp "write-goal" s n

294+

295+isetPrompt :: String -> Idris ()

296+isetPrompt p = do i <- getIState

297+ case idris_outputmode i of

298+ IdeSlave n -> liftIO . putStrLn $ convSExp "set-prompt" p n

281

299

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

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

283iWarn fc err = do i <- getIState

301iWarn fc err = do i <- getIState

284 case idris_outputmode i of

302 case idris_outputmode i of

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

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

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

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

287

305

288setLogLevel :: Int -> Idris ()

306setLogLevel :: Int -> Idris ()

289setLogLevel l = do i <- getIState

307setLogLevel l = do i <- getIState

src/Idris/Completion.hs+2−3

@@ -28,8 +28,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

29-- | A list of available tactics and their argument requirements

30tacticArgs :: [(String, Maybe TacticArg)]

31−tacticArgs = [ ("intro", Nothing)

31+tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

32− , ("intros", Nothing)

33 , ("refine", Just ExprTArg)

32 , ("refine", Just ExprTArg)

34 , ("mrefine", Just ExprTArg)

33 , ("mrefine", Just ExprTArg)

35 , ("rewrite", Just ExprTArg)

34 , ("rewrite", Just ExprTArg)

@@ -41,7 +40,7 @@ tacticArgs = [ ("intro", Nothing)

41 , ("fill", Just ExprTArg)

40 , ("fill", Just ExprTArg)

42 , ("try", Just AltsTArg)

41 , ("try", Just AltsTArg)

43 ] ++ map (\x -> (x, Nothing)) [

42 ] ++ map (\x -> (x, Nothing)) [

44− "intro", "intros", "compute", "trivial", "solve", "attack",

43+ "intros", "compute", "trivial", "solve", "attack",

45 "state", "term", "undo", "qed", "abandon", ":q"

44 "state", "term", "undo", "qed", "abandon", ":q"

46 ]

45 ]

47tactics = map fst tacticArgs

46tactics = map fst tacticArgs

src/Idris/IdeSlave.hs+9−2

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

1{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

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

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

5import Text.Printf

6import Numeric

@@ -8,6 +8,8 @@ import Data.List

8-- import qualified Data.Text as T

9import Text.Parsec

11+import Core.TT

12+

11data SExp = SexpList [SExp]

13data SExp = SexpList [SExp]

12 | StringAtom String

14 | StringAtom String

13 | BoolAtom Bool

15 | BoolAtom Bool

@@ -42,6 +44,11 @@ instance SExpable Integer where

42instance SExpable Int where

44instance SExpable Int where

43 toSExp n = IntegerAtom (toInteger n)

45 toSExp n = IntegerAtom (toInteger n)

47+

48+instance SExpable Name where

49+ toSExp s = StringAtom (show s)

50+

51+

45instance (SExpable a) => SExpable (Maybe a) where

52instance (SExpable a) => SExpable (Maybe a) where

46 toSExp Nothing = SexpList [SymbolAtom "Nothing"]

53 toSExp Nothing = SexpList [SymbolAtom "Nothing"]

47 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]

54 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]

@@ -94,7 +101,7 @@ sexpToCommand (SexpList (x:[])) = se

94sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

101sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

95sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

102sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

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

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

97−sexpToCommand _ = Nothing

104+sexpToCommand _ = Nothing

105

99parseMessage :: String -> (SExp, Integer)

106parseMessage :: String -> (SExp, Integer)

100parseMessage x = case receiveString x of

107parseMessage x = case receiveString x of

src/Idris/Prover.hs+64−35

@@ -14,6 +14,7 @@ import Idris.Parser

14import Idris.Error

15import Idris.DataOpts

16import Idris.Completion

17+import Idris.IdeSlave

18import System.Console.Haskeline

19import System.Console.Haskeline

19import System.Console.Haskeline.History

20import System.Console.Haskeline.History

@@ -41,26 +42,31 @@ showProof lit n ps

41 break = "\n" ++ bird

42 break = "\n" ++ bird

43proverSettings :: ElabState [PDecl] -> Settings Idris

44proverSettings :: ElabState [PDecl] -> Settings Idris

44−proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings

45+proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings

46+

47+assumptionNames :: ElabState [PDecl] -> [String]

48+assumptionNames e

45− where assumptionNames = case envAtFocus (proof e) of

49+ = case envAtFocus (proof e) of

46− OK env -> names env

50+ OK env -> names env

47− names [] = []

51+ where names [] = []

48− names ((MN _ _, _) : bs) = names bs

52+ names ((MN _ _, _) : bs) = names bs

49− names ((n, _) : bs) = show n : names bs

53+ names ((n, _) : bs) = show n : names bs

51prove :: Context -> Bool -> Name -> Type -> Idris ()

55prove :: Context -> Bool -> Name -> Type -> Idris ()

52−prove ctxt lit n ty

56+prove ctxt lit n ty

53 = do let ps = initElaborator n ctxt ty

57 = do let ps = initElaborator n ctxt ty

58+ ideslavePutSExp "start-proof-mode" n

54 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

59 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

55 iLOG $ "Adding " ++ show tm

60 iLOG $ "Adding " ++ show tm

56 iputStrLn $ showProof lit n prf

61 iputStrLn $ showProof lit n prf

57 i <- getIState

62 i <- getIState

63+ ideslavePutSExp "end-proof-mode" n

58 let proofs = proof_list i

64 let proofs = proof_list i

59 putIState (i { proof_list = (n, prf) : proofs })

65 putIState (i { proof_list = (n, prf) : proofs })

60 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

66 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

61 logLvl 3 (show tree)

67 logLvl 3 (show tree)

62 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

68 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

63− logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

69+ logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

64 "Expected type:" ++ show ty)

70 "Expected type:" ++ show ty)

65 case converts ctxt [] ty pty of

71 case converts ctxt [] ty pty of

66 OK _ -> return ()

72 OK _ -> return ()

@@ -68,7 +74,7 @@ prove ctxt lit n ty

68 ptm' <- applyOpts ptm

74 ptm' <- applyOpts ptm

69 updateContext (addCasedef n True False True False

75 updateContext (addCasedef n True False True False

70 [Right (P Ref n ty, ptm)]

76 [Right (P Ref n ty, ptm)]

71− [([], P Ref n ty, ptm)]

77+ [([], P Ref n ty, ptm)]

72 [([], P Ref n ty, ptm')] ty)

78 [([], P Ref n ty, ptm')] ty)

73 solveDeferred n

79 solveDeferred n

74elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

80elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

@@ -77,13 +83,13 @@ elabStep st e = do case runStateT e st of

77 Error a -> do i <- getIState

83 Error a -> do i <- getIState

78 fail (pshow i a)

84 fail (pshow i a)

80−dumpState :: IState -> ProofState -> IO ()

86+dumpState :: IState -> ProofState -> Idris ()

81dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

87dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

82− putStrLn . render $ pretty nm <> colon <+> text "No more goals."

88+ iputGoal . render $ pretty nm <> colon <+> text "No more goals."

83dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

89dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

84 let OK ty = goalAtFocus ps

90 let OK ty = goalAtFocus ps

85 let OK env = envAtFocus ps

91 let OK env = envAtFocus ps

86− putStrLn . render $

92+ iputGoal . render $

87 prettyOtherGoals hs $$

93 prettyOtherGoals hs $$

88 prettyAssumptions env $$

94 prettyAssumptions env $$

89 prettyGoal ty

95 prettyGoal ty

@@ -124,46 +130,69 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a

124lifte st e = do (v, _) <- elabStep st e

130lifte st e = do (v, _) <- elabStep st e

125 return v

131 return v

126

132

133+receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

134+receiveInput e =

135+ do i <- getIState

136+ l <- liftIO $ getLine

137+ let (sexp, id) = parseMessage l

138+ putIState $ i { idris_outputmode = (IdeSlave id) }

139+ case sexpToCommand sexp of

140+ Just (REPLCompletions prefix) ->

141+ do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

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

143+ ideslavePutSExp "return" good

144+ receiveInput e

145+ Just (Interpret cmd) -> return (Just cmd)

146+ Nothing -> return Nothing

147+

127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

148ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

128ploop d prompt prf e h

149ploop d prompt prf e h

129 = do i <- getIState

150 = do i <- getIState

130− when d $ liftIO $ dumpState i (proof e)

151+ when d $ dumpState i (proof e)

152+ (x, h') <-

153+ case idris_outputmode i of

131− (x, h') <- runInputT (proverSettings e) $

154+ RawOutput -> runInputT (proverSettings e) $

132− -- Manually track the history so that we can use the proof state

155+ -- Manually track the history so that we can use the proof state

133− do _ <- case h of

156+ do _ <- case h of

134− Just history -> putHistory history

157+ Just history -> putHistory history

135− Nothing -> return ()

158+ Nothing -> return ()

136− l <- getInputLine (prompt ++ "> ")

159+ l <- getInputLine (prompt ++ "> ")

137− h' <- getHistory

160+ h' <- getHistory

138− return (l, Just h')

161+ return (l, Just h')

162+ IdeSlave n ->

163+ do isetPrompt prompt

164+ i <- receiveInput e

165+ return (i, h)

139 (cmd, step) <- case x of

166 (cmd, step) <- case x of

140− Nothing -> fail "Abandoned"

167+ Nothing -> do iFail ""; fail "Abandoned"

141 Just input -> do return (parseTac i input, input)

168 Just input -> do return (parseTac i input, input)

142 case cmd of

169 case cmd of

143− Right Abandon -> fail "Abandoned"

170+ Right Abandon -> do iFail ""; fail "Abandoned"

144 _ -> return ()

171 _ -> return ()

145 (d, st, done, prf') <- idrisCatch

172 (d, st, done, prf') <- idrisCatch

146 (case cmd of

173 (case cmd of

147− Left err -> do iputStrLn (show err)

174+ Left err -> do iFail (show err)

148 return (False, e, False, prf)

175 return (False, e, False, prf)

149− Right Undo ->

150− do (_, st) <- elabStep e loadState

176+ Right Undo -> do (_, st) <- elabStep e loadState

177+ iResult ""

151− return (True, st, False, init prf)

178+ return (True, st, False, init prf)

152− Right ProofState ->

179+ Right ProofState -> do iResult ""

153− return (True, e, False, prf)

180+ return (True, e, False, prf)

154− Right ProofTerm ->

155− do tm <- lifte e get_term

181+ Right ProofTerm -> do tm <- lifte e get_term

156− iputStrLn $ "TT: " ++ show tm ++ "\n"

182+ iResult $ "TT: " ++ show tm ++ "\n"

157− return (False, e, False, prf)

183+ return (False, e, False, prf)

158 Right Qed -> do hs <- lifte e get_holes

184 Right Qed -> do hs <- lifte e get_holes

159 when (not (null hs)) $ fail "Incomplete proof"

185 when (not (null hs)) $ fail "Incomplete proof"

186+ iResult "Proof completed!"

160 return (False, e, True, prf)

187 return (False, e, True, prf)

161 Right tac -> do (_, e) <- elabStep e saveState

188 Right tac -> do (_, e) <- elabStep e saveState

162 (_, st) <- elabStep e (runTac True i tac)

189 (_, st) <- elabStep e (runTac True i tac)

163−-- trace (show (problems (proof st))) $

190+-- trace (show (problems (proof st))) $

191+ iResult ""

164 return (True, st, False, prf ++ [step]))

192 return (True, st, False, prf ++ [step]))

165− (\err -> do iputStrLn (show err)

193+ (\err -> do iFail (show err)

166 return (False, e, False, prf))

194 return (False, e, False, prf))

195+ ideslavePutSExp "write-proof-state" (prf', length prf')

167 if done then do (tm, _) <- elabStep st get_term

196 if done then do (tm, _) <- elabStep st get_term

168 return (tm, prf')

197 return (tm, prf')

169 else ploop d prompt prf' st h'

198 else ploop d prompt prf' st h'

src/Idris/REPL.hs+13−4

@@ -91,7 +91,7 @@ ideslaveStart orig mods

91 = do i <- getIState

92 case idris_outputmode i of

93 IdeSlave n ->

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

94+ when (mods /= []) (do isetPrompt (mkPrompt mods))

95 ideslave orig mods

@@ -109,6 +109,11 @@ ideslave orig mods

109 _ -> ""

110 case parseCmd i cmd of

111 Left err -> iFail $ show err

112+ Right (Prove n') -> do iResult ""

113+ idrisCatch

114+ (do process fn (Prove n'))

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

116+ isetPrompt (mkPrompt mods)

112 Right cmd -> idrisCatch

117 Right cmd -> idrisCatch

113 (do ideslaveProcess fn cmd)

118 (do ideslaveProcess fn cmd)

114 (\e -> do iFail $ show e)

119 (\e -> do iFail $ show e)

@@ -122,8 +127,13 @@ ideslave orig mods

122 idris_outputmode = (IdeSlave id) })

127 idris_outputmode = (IdeSlave id) })

123 loadModule filename

128 loadModule filename

124 iucheck

129 iucheck

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

130+ isetPrompt (mkPrompt [filename])

131+

126− -- report success! or failure!

132+ -- Report either success or failure

133+ i <- getIState

134+ case (errLine i) of

135+ Nothing -> iResult $ "loaded " ++ filename

136+ Just x -> iFail $ "didn't load " ++ filename

127 ideslave orig [filename]

137 ideslave orig [filename]

128 Nothing -> do iFail "did not understand")

138 Nothing -> do iFail "did not understand")

129 (\e -> do iFail $ show e)

139 (\e -> do iFail $ show e)

@@ -149,7 +159,6 @@ ideslaveProcess fn (Search t) = process fn (Search t)

149ideslaveProcess fn (Spec t) = process fn (Spec t)

159ideslaveProcess fn (Spec t) = process fn (Spec t)

150-- RmProof and AddProof not supported!

160-- RmProof and AddProof not supported!

151ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

161ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

152−ideslaveProcess fn (Prove n') = process fn (Prove n')

153ideslaveProcess fn (HNF t) = process fn (HNF t)

162ideslaveProcess fn (HNF t) = process fn (HNF t)

154--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

163--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

155

164