f7c7a81 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commitf7c7a81e38f284597aac788438e56952c7354ea8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 16 Jul 2013, 15:15 (13 years ago) parent86b4541 0b5bd21

7 files changed+118−52

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+21−3 src/Idris/Completion.hs+2−3 src/Idris/IdeSlave.hs+9−2 src/Idris/Prover.hs+64−35 src/Idris/REPL.hs+13−4 src/Main.hs+8−4 src/Util/LLVMStubs.hs+1−1

src/Idris/AbsSyntax.hs+21−3

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

264264 s -> liftIO $ putStrLn s

265265 IdeSlave n ->

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

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

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

268268

269269iputStrLn :: String -> Idris ()

270270iputStrLn s = do i <- getIState

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

277277 ([], msg) -> write

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

279279 _ -> 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

281299

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

283301iWarn fc err = do i <- getIState

284302 case idris_outputmode i of

285303 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

287305

288306setLogLevel :: Int -> Idris ()

289307setLogLevel l = do i <- getIState

src/Idris/Completion.hs+2−3

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

2828

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

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

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

32− , ("intros", Nothing)

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

3332 , ("refine", Just ExprTArg)

3433 , ("mrefine", Just ExprTArg)

3534 , ("rewrite", Just ExprTArg)

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

4140 , ("fill", Just ExprTArg)

4241 , ("try", Just AltsTArg)

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

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

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

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

4645 ]

4746tactics = map fst tacticArgs

src/Idris/IdeSlave.hs+9−2

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

11{-# 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

55import Text.Printf

66import Numeric

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

88-- import qualified Data.Text as T

99import Text.Parsec

1010

11+import Core.TT

12+

1113data SExp = SexpList [SExp]

1214 | StringAtom String

1315 | BoolAtom Bool

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

4244instance SExpable Int where

4345 toSExp n = IntegerAtom (toInteger n)

4446

47+

48+instance SExpable Name where

49+ toSExp s = StringAtom (show s)

50+

51+

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

4653 toSExp Nothing = SexpList [SymbolAtom "Nothing"]

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

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

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

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

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

97−sexpToCommand _ = Nothing

104+sexpToCommand _ = Nothing

98105

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

100107parseMessage x = case receiveString x of

src/Idris/Prover.hs+64−35

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

1414import Idris.Error

1515import Idris.DataOpts

1616import Idris.Completion

17+import Idris.IdeSlave

1718

1819import System.Console.Haskeline

1920import System.Console.Haskeline.History

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

4142 break = "\n" ++ bird

4243

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

44−proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings

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

46− OK env -> names env

47− names [] = []

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

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

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

46+

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

48+assumptionNames e

49+ = case envAtFocus (proof e) of

50+ OK env -> names env

51+ where names [] = []

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

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

5054

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

52−prove ctxt lit n ty

56+prove ctxt lit n ty

5357 = do let ps = initElaborator n ctxt ty

58+ ideslavePutSExp "start-proof-mode" n

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

5560 iLOG $ "Adding " ++ show tm

5661 iputStrLn $ showProof lit n prf

5762 i <- getIState

63+ ideslavePutSExp "end-proof-mode" n

5864 let proofs = proof_list i

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

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

6167 logLvl 3 (show tree)

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

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

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

6470 "Expected type:" ++ show ty)

6571 case converts ctxt [] ty pty of

6672 OK _ -> return ()

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

6874 ptm' <- applyOpts ptm

6975 updateContext (addCasedef n True False True False

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

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

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

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

7379 solveDeferred n

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

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

7783 Error a -> do i <- getIState

7884 fail (pshow i a)

7985

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

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

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

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

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

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

8490 let OK ty = goalAtFocus ps

8591 let OK env = envAtFocus ps

86− putStrLn . render $

92+ iputGoal . render $

8793 prettyOtherGoals hs $$

8894 prettyAssumptions env $$

8995 prettyGoal ty

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

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

125131 return v

126132

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+

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

128149ploop d prompt prf e h

129150 = do i <- getIState

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

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

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

133− do _ <- case h of

134− Just history -> putHistory history

135− Nothing -> return ()

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

137− h' <- getHistory

138− return (l, Just h')

151+ when d $ dumpState i (proof e)

152+ (x, h') <-

153+ case idris_outputmode i of

154+ RawOutput -> runInputT (proverSettings e) $

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

156+ do _ <- case h of

157+ Just history -> putHistory history

158+ Nothing -> return ()

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

160+ h' <- getHistory

161+ return (l, Just h')

162+ IdeSlave n ->

163+ do isetPrompt prompt

164+ i <- receiveInput e

165+ return (i, h)

139166 (cmd, step) <- case x of

140− Nothing -> fail "Abandoned"

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

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

142169 case cmd of

143− Right Abandon -> fail "Abandoned"

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

144171 _ -> return ()

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

146173 (case cmd of

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

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

148175 return (False, e, False, prf)

149− Right Undo ->

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

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

152− Right ProofState ->

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

154− Right ProofTerm ->

155− do tm <- lifte e get_term

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

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

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

177+ iResult ""

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

179+ Right ProofState -> do iResult ""

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

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

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

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

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

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

186+ iResult "Proof completed!"

160187 return (False, e, True, prf)

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

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

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

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

191+ iResult ""

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

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

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

166194 return (False, e, False, prf))

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

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

168197 return (tm, prf')

169198 else ploop d prompt prf' st h'

src/Idris/REPL.hs+13−4

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

9191 = do i <- getIState

9292 case idris_outputmode i of

9393 IdeSlave n ->

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

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

9595 ideslave orig mods

9696

9797

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

109109 _ -> ""

110110 case parseCmd i cmd of

111111 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)

112117 Right cmd -> idrisCatch

113118 (do ideslaveProcess fn cmd)

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

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

122127 idris_outputmode = (IdeSlave id) })

123128 loadModule filename

124129 iucheck

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

126− -- report success! or failure!

130+ isetPrompt (mkPrompt [filename])

131+

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

127137 ideslave orig [filename]

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

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

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

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

150160-- RmProof and AddProof not supported!

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

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

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

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

155164

src/Main.hs+8−4

@@ -91,12 +91,16 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

9191 "\t--log [level] Type debugging log level\n" ++

9292 "\t-S Do no further compilation of code generator output\n" ++

9393 "\t-c Compile to object files rather than an executable\n" ++

94− "\t--exec [expr] Execute the expression expr in the interpreter, defaulting to\n" ++

95− "\t Main.main if none provided, and exit.\n" ++

96− "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in s-expressions)\n" ++

94+ "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++

95+ "\t defaulting to Main.main if none provided, and exit.\n" ++

96+ "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++

97+ "\t s-expressions)\n" ++

9798 "\t--libdir Show library install directory and exit\n" ++

9899 "\t--link Show C library directories and exit (for C linking)\n" ++

99100 "\t--include Show C include directories and exit (for C linking)\n" ++

100− "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"

101+ "\t--codegen [cg] Select code generator: C, Java, bytecode, javascript,\n" ++

102+ "\t node or llvm\n" ++

103+ "\t--target [triple] Select target triple (for LLVM codegen)\n" ++

104+ "\t--cpu [cpu] Select target architecture (for LLVM codegen)\n"

101105

102106

src/Util/LLVMStubs.hs+1−1

@@ -27,4 +27,4 @@ codegenLLVM :: [(TT.Name, SDecl)] ->

2727 OutputType ->

2828 IO ()

2929

30−codegenLLVM _ _ _ _ _ _ = print "Error: This Idris was compiled without the LLVM backend."

30+codegenLLVM _ _ _ _ _ _ = fail "This Idris was compiled without the LLVM backend."