f17a517 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

f17a517Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+12

compare with master

unifiedsplit

@@ -538,6 +538,18 @@ isetPrompt p = do i <- getIState

538 case idris_outputmode i of

539 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

540

541+-- | Tell clients how much was parsed and loaded

542+isetLoadedRegion :: Idris ()

543+isetLoadedRegion = do i <- getIState

544+ let span = idris_parsedSpan i

545+ case span of

546+ Just fc ->

547+ case idris_outputmode i of

548+ IdeSlave n ->

549+ runIO . putStrLn $

550+ convSExp "set-loaded-region" fc n

551+ Nothing -> return ()

552+

541setLogLevel :: Int -> Idris ()

553setLogLevel :: Int -> Idris ()

542setLogLevel l = do i <- getIState

554setLogLevel l = do i <- getIState

543 let opts = idris_options i

555 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+3−1

@@ -174,6 +174,7 @@ data IState = IState {

174 indent_stack :: [Int],

175 brace_stack :: [Maybe Int],

176 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

177+ idris_parsedSpan :: Maybe FC,

177 hide_list :: [(Name, Maybe Accessibility)],

178 hide_list :: [(Name, Maybe Accessibility)],

178 default_access :: Accessibility,

179 default_access :: Accessibility,

179 default_total :: Bool,

180 default_total :: Bool,

@@ -255,6 +256,7 @@ data IBCWrite = IBCFix FixDecl

255 | IBCFunctionErrorHandler Name Name Name

256 | IBCFunctionErrorHandler Name Name Name

256 | IBCPostulate Name

257 | IBCPostulate Name

257 | IBCTotCheckErr FC String

258 | IBCTotCheckErr FC String

259+ | IBCParsedRegion FC

258 deriving Show

260 deriving Show

259

261

260-- | The initial state for the compiler

262-- | The initial state for the compiler

@@ -264,7 +266,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

264 emptyContext emptyContext emptyContext emptyContext

266 emptyContext emptyContext emptyContext emptyContext

265 emptyContext emptyContext

267 emptyContext emptyContext

266 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

268 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

267− [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

269+ [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

268 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

270 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

269 AutomaticWidth S.empty Nothing Nothing

271 AutomaticWidth S.empty Nothing Nothing

270

272

src/Idris/IBC.hs+14−5

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

32ibcVersion :: Word8

33−ibcVersion = 72

33+ibcVersion = 73

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -68,7 +68,8 @@ data IBCFile = IBCFile { ver :: Word8,

68 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

69 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

70 ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],

71− ibc_postulates :: [Name]

71+ ibc_postulates :: [Name],

72+ ibc_parsedSpan :: Maybe FC

72 }

73 }

73 deriving Show

74 deriving Show

74{-!

75{-!

@@ -76,7 +77,7 @@ deriving instance Binary IBCFile

76!-}

77!-}

78initIBC :: IBCFile

79initIBC :: IBCFile

79−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

80+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

81loadIBC :: FilePath -> Idris ()

82loadIBC :: FilePath -> Idris ()

82loadIBC fp = do imps <- getImported

83loadIBC fp = do imps <- getImported

@@ -241,6 +242,7 @@ ibc i (IBCMetavar n) f =

241 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

242 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

242ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

243ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

243ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

244ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

245+ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

244

246

245process :: IBCFile -> FilePath -> Idris ()

247process :: IBCFile -> FilePath -> Idris ()

246process i fn

248process i fn

@@ -285,6 +287,7 @@ process i fn

285 pFunctionErrorHandlers (ibc_function_errorhandlers i)

287 pFunctionErrorHandlers (ibc_function_errorhandlers i)

286 pMetavars (ibc_metavars i)

288 pMetavars (ibc_metavars i)

287 pPostulates (ibc_postulates i)

289 pPostulates (ibc_postulates i)

290+ pParsedSpan (ibc_parsedSpan i)

288

291

289timestampOlder :: FilePath -> FilePath -> Idris ()

292timestampOlder :: FilePath -> FilePath -> Idris ()

290timestampOlder src ibc = do srct <- runIO $ getModificationTime src

293timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -298,6 +301,10 @@ pPostulates ns = do

298 i <- getIState

301 i <- getIState

299 putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

302 putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

300

303

304+pParsedSpan :: Maybe FC -> Idris ()

305+pParsedSpan fc = do ist <- getIState

306+ putIState ist { idris_parsedSpan = fc }

307+

301pImports :: [FilePath] -> Idris ()

308pImports :: [FilePath] -> Idris ()

302pImports fs

309pImports fs

303 = do mapM_ (\f -> do i <- getIState

310 = do mapM_ (\f -> do i <- getIState

@@ -1168,7 +1175,7 @@ instance Binary MetaInformation where

1168 return (DataMI x1)

1175 return (DataMI x1)

1169

1176

1170instance Binary IBCFile where

1177instance Binary IBCFile where

1171− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1178+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38)

1172 = {-# SCC "putIBCFile" #-}

1179 = {-# SCC "putIBCFile" #-}

1173 do put x1

1180 do put x1

1174 put x2

1181 put x2

@@ -1207,6 +1214,7 @@ instance Binary IBCFile where

1207 put x35

1214 put x35

1208 put x36

1215 put x36

1209 put x37

1216 put x37

1217+ put x38

1210

1218

1211 get

1219 get

1212 = do x1 <- get

1220 = do x1 <- get

@@ -1247,7 +1255,8 @@ instance Binary IBCFile where

1247 x35 <- get

1255 x35 <- get

1248 x36 <- get

1256 x36 <- get

1249 x37 <- get

1257 x37 <- get

1258+ x38 <- get

1250− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1259+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38)

1251 else return (initIBC { ver = x1 })

1260 else return (initIBC { ver = x1 })

1252

1261

1253instance Binary DataOpt where

1262instance Binary DataOpt where

src/Idris/IdeSlave.hs+21−12

@@ -121,16 +121,19 @@ instance SExpable OutputAnnotation where

121 (SymbolAtom "doc-overview", StringAtom doc)] ++

122 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []

123 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

124− toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

124+ toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]

125− ((SymbolAtom "filename", StringAtom f),

126− (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

127− (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]

128 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]

125 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]

129 where format = case fmt of

126 where format = case fmt of

130 BoldText -> "bold"

127 BoldText -> "bold"

131 ItalicText -> "italic"

128 ItalicText -> "italic"

132 UnderlineText -> "underline"

129 UnderlineText -> "underline"

133

130

131+instance SExpable FC where

132+ toSExp (FC f (sl, sc) (el, ec)) =

133+ toSExp ((SymbolAtom "filename", StringAtom f),

134+ (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

135+ (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))

136+

134escape :: String -> String

137escape :: String -> String

135escape = concatMap escapeChar

138escape = concatMap escapeChar

136 where

139 where

@@ -171,9 +174,9 @@ data IdeSlaveCommand = REPLCompletions String

171 | AddProofClause Int String

174 | AddProofClause Int String

172 | AddMissing Int String

175 | AddMissing Int String

173 | MakeWithBlock Int String

176 | MakeWithBlock Int String

174− | ProofSearch Bool Int String [String]

177+ | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

175 | MakeLemma Int String

178 | MakeLemma Int String

176− | LoadFile String

179+ | LoadFile String (Maybe Int)

177 | DocsFor String

180 | DocsFor String

178 | Apropos String

181 | Apropos String

179 | GetOpts

182 | GetOpts

@@ -186,7 +189,8 @@ sexpToCommand :: SExp -> Maybe IdeSlaveCommand

186sexpToCommand (SexpList (x:[])) = sexpToCommand x

189sexpToCommand (SexpList (x:[])) = sexpToCommand x

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

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

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

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

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

192+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))

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

190sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

194sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

191sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

195sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

192sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

196sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

@@ -196,12 +200,17 @@ sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom na

196-- The Boolean in ProofSearch means "search recursively"

200-- The Boolean in ProofSearch means "search recursively"

197-- If it's False, that means "refine", i.e. apply the name and fill in any

201-- If it's False, that means "refine", i.e. apply the name and fill in any

198-- arguments which can be done by unification.

202-- arguments which can be done by unification.

199−sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)

203+sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))

204+ | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)

205+ | [SexpList hintexp] <- rest

206+ , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)

207+ | [SexpList hintexp, IntegerAtom depth] <- rest

208+ , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))

200− where getHints = mapM (\h -> case h of

209+ where getHints = mapM (\h -> case h of

201− StringAtom s -> Just s

210+ StringAtom s -> Just s

202− _ -> Nothing)

211+ _ -> Nothing)

203sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

212sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

204−sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])

213+sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

205sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

214sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

206sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

215sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

207sexpToCommand (SymbolAtom "get-options") = Just GetOpts

216sexpToCommand (SymbolAtom "get-options") = Just GetOpts

src/Idris/Interactive.hs+6−4

@@ -152,8 +152,10 @@ makeWith h fn updatefile l n

152

153

154doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

155− Int -> Name -> [Name] -> Idris ()

155+ Int -> Name -> [Name] -> Maybe Int -> Idris ()

156−doProofSearch h fn updatefile rec l n hints

156+doProofSearch h fn updatefile rec l n hints Nothing

157+ = doProofSearch h fn updatefile rec l n hints (Just 10)

158+doProofSearch h fn updatefile rec l n hints (Just depth)

157 = do src <- runIO $ readFile fn

159 = do src <- runIO $ readFile fn

158 let (before, tyline : later) = splitAt (l-1) (lines src)

160 let (before, tyline : later) = splitAt (l-1) (lines src)

159 ctxt <- getContext

161 ctxt <- getContext

@@ -166,8 +168,8 @@ doProofSearch h fn updatefile rec l n hints

166 Just (t, e, False) -> (t, e, False)

168 Just (t, e, False) -> (t, e, False)

167 _ -> (Nothing, 0, True)

169 _ -> (Nothing, 0, True)

168 let fc = fileFC fn

170 let fc = fileFC fn

169− let body t = PProof [Try (TSeq Intros (ProofSearch rec False 10 t hints))

171+ let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

170− (ProofSearch rec False 10 t hints)]

172+ (ProofSearch rec False depth t hints)]

171 let def = PClause fc mn (PRef fc mn) [] (body top) []

173 let def = PClause fc mn (PRef fc mn) [] (body top) []

172 newmv <- idrisCatch

174 newmv <- idrisCatch

173 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

175 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

src/Idris/Parser.hs+6−2

@@ -132,6 +132,10 @@ prog syn = do whiteSpace

132 case maxline syn of

133 Nothing -> do notOpenBraces; eof

134 _ -> return ()

135+ ist <- get

136+ fc <- getFC

137+ put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),

138+ ibc_write = IBCParsedRegion fc : ibc_write ist }

135 return c

139 return c

136

140

137{-| Parses a top-level declaration

141{-| Parses a top-level declaration

@@ -158,12 +162,12 @@ decl syn = do fc <- getFC

158 -- if we're after maxline, stop here

162 -- if we're after maxline, stop here

159 let continue = case maxline syn of

163 let continue = case maxline syn of

160 Nothing -> True

164 Nothing -> True

161− Just l -> if fst (fc_end fc) > l

165+ Just l -> if fst (fc_end fc) > l

162 then False

166 then False

163 else True

167 else True

164 if continue then do notEndBlock

168 if continue then do notEndBlock

165 declBody

169 declBody

166− else fail "End of readable input"

170+ else fail "End of readable input"

167 where declBody :: IdrisParser [PDecl]

171 where declBody :: IdrisParser [PDecl]

168 declBody = declBody'

172 declBody = declBody'

169 <|> using_ syn

173 <|> using_ syn

src/Idris/REPL.hs+12−7

@@ -253,17 +253,22 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

253 IdeSlave.toSExp (map replacement compls,

254 reverse unused)]

255 runIO $ putStrLn $ IdeSlave.convSExp "return" good id

256−runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

256+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

257 do i <- getIState

258 clearErr

259 putIState (orig { idris_options = idris_options i,

260 idris_outputmode = (IdeSlave id) })

261− loadInputs stdout [filename] Nothing

261+ loadInputs stdout [filename] toline

262 isetPrompt (mkPrompt [filename])

263 -- Report either success or failure

264 i <- getIState

265 case (errSpan i) of

266− Nothing -> iPrintResult $ "loaded " ++ filename

266+ Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

267+ IdeSlave.SexpList []])

268+ (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

269+ IdeSlave.toSExp fc])

270+ (idris_parsedSpan i)

271+ in runIO . putStrLn $ IdeSlave.convSExp "return" msg id

267 Just x -> iPrintError $ "didn't load " ++ filename

272 Just x -> iPrintError $ "didn't load " ++ filename

268 ideslave orig [filename]

273 ideslave orig [filename]

269runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

274runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

@@ -293,8 +298,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

293 process stdout fn (AddMissing False line (sUN name))

298 process stdout fn (AddMissing False line (sUN name))

294runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

299runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

295 process stdout fn (MakeWith False line (sUN name))

300 process stdout fn (MakeWith False line (sUN name))

296−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =

301+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

297− process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))

302+ doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth

298runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

303runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

299 case splitName name of

304 case splitName name of

300 Left err -> iPrintError err

305 Left err -> iPrintError err

@@ -716,7 +721,7 @@ process h fn (MakeWith updatefile l n)

716process h fn (MakeLemma updatefile l n)

721process h fn (MakeLemma updatefile l n)

717 = makeLemma h fn updatefile l n

722 = makeLemma h fn updatefile l n

718process h fn (DoProofSearch updatefile rec l n hints)

723process h fn (DoProofSearch updatefile rec l n hints)

719− = doProofSearch h fn updatefile rec l n hints

724+ = doProofSearch h fn updatefile rec l n hints Nothing

720process h fn (Spec t)

725process h fn (Spec t)

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

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

722 ctxt <- getContext

727 ctxt <- getContext

@@ -1056,7 +1061,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

1056 tryLoad keepstate [] = warnTotality >> return ()

1061 tryLoad keepstate [] = warnTotality >> return ()

1057 tryLoad keepstate (f : fs)

1062 tryLoad keepstate (f : fs)

1058 = do ist <- getIState

1063 = do ist <- getIState

1059− let maxline

1064+ let maxline

1060 = case toline of

1065 = case toline of

1061 Nothing -> Nothing

1066 Nothing -> Nothing

1062 Just l -> case f of

1067 Just l -> case f of