602552e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :loadto command

Loads an input file up to the declaration beginning at the given line, discarding any declaration after that. This only really makes sense when developing interactively: it means you can work on something at the top of a file without worrying about how it affects what happens later (this also potentially makes it a lot quicker!) Latest idris-vim uses this.

commit602552ebdbec73dc8ccb9fd58c9c809be5091167 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 22 May 2014, 01:10 (12 years ago) parent094be98

6 files changed+69−38

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/DeepSeq.hs+2−2 src/Idris/IBC.hs+2−2 src/Idris/Parser.hs+28−18 src/Idris/REPL.hs+28−13 src/Idris/REPLParser.hs+6−1

src/Idris/AbsSyntaxTree.hs+3−2

@@ -291,7 +291,7 @@ data Command = Quit

291291 | DocStr (Either Name Const)

292292 | TotCheck Name

293293 | Reload

294− | Load FilePath

294+ | Load FilePath (Maybe Int) -- up to maximum line number

295295 | ChangeDirectory FilePath

296296 | ModImport String

297297 | Edit

@@ -960,6 +960,7 @@ data SyntaxInfo = Syn { using :: [Using],

960960 decoration :: Name -> Name,

961961 inPattern :: Bool,

962962 implicitAllowed :: Bool,

963+ maxline :: Maybe Int,

963964 dsl_info :: DSL }

964965 deriving Show

965966{-!

@@ -967,7 +968,7 @@ deriving instance NFData SyntaxInfo

967968deriving instance Binary SyntaxInfo

968969!-}

969970

970−defaultSyntax = Syn [] [] [] [] id False False initDSL

971+defaultSyntax = Syn [] [] [] [] id False False Nothing initDSL

971972

972973expandNS :: SyntaxInfo -> Name -> Name

973974expandNS syn n@(NS _ _) = n

src/Idris/DeepSeq.hs+2−2

@@ -321,11 +321,11 @@ instance NFData Using where

321321

322322

323323instance NFData SyntaxInfo where

324− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9)

325325 = rnf x1 `seq`

326326 rnf x2 `seq`

327327 rnf x3 `seq`

328− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

328+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

329329

330330

331331

src/Idris/IBC.hs+2−2

@@ -1573,7 +1573,7 @@ instance Binary Using where

15731573 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

15741574

15751575instance Binary SyntaxInfo where

1576− put (Syn x1 x2 x3 x4 _ x5 x6 x7)

1576+ put (Syn x1 x2 x3 x4 _ x5 x6 _ x7)

15771577 = do put x1

15781578 put x2

15791579 put x3

@@ -1589,7 +1589,7 @@ instance Binary SyntaxInfo where

15891589 x5 <- get

15901590 x6 <- get

15911591 x7 <- get

1592− return (Syn x1 x2 x3 x4 id x5 x6 x7)

1592+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing x7)

15931593

15941594instance (Binary t) => Binary (PClause' t) where

15951595 put x

src/Idris/Parser.hs+28−18

@@ -128,9 +128,10 @@ import_ = do fc <- getFC

128128prog :: SyntaxInfo -> IdrisParser [PDecl]

129129prog syn = do whiteSpace

130130 decls <- many (decl syn)

131− notOpenBraces

132− eof

133131 let c = (concat decls)

132+ case maxline syn of

133+ Nothing -> do notOpenBraces; eof

134+ _ -> return ()

134135 return c

135136

136137{-| Parses a top-level declaration

@@ -153,8 +154,16 @@ Decl ::=

153154@

154155-}

155156decl :: SyntaxInfo -> IdrisParser [PDecl]

156−decl syn = do notEndBlock

157− declBody

157+decl syn = do fc <- getFC

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

159+ let continue = case maxline syn of

160+ Nothing -> True

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

162+ then False

163+ else True

164+ if continue then do notEndBlock

165+ declBody

166+ else fail "End of readable input"

158167 where declBody :: IdrisParser [PDecl]

159168 declBody = declBody'

160169 <|> using_ syn

@@ -1177,21 +1186,21 @@ loadModule' outh f

11771186 then iLOG $ "Already read " ++ file

11781187 else do putIState (i { imported = file : imported i })

11791188 case fp of

1180− IDR fn -> loadSource outh False fn

1181− LIDR fn -> loadSource outh True fn

1189+ IDR fn -> loadSource outh False fn Nothing

1190+ LIDR fn -> loadSource outh True fn Nothing

11821191 IBC fn src ->

11831192 idrisCatch (loadIBC fn)

11841193 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

11851194 case src of

1186− IDR sfn -> loadSource outh False sfn

1187− LIDR sfn -> loadSource outh True sfn)

1195+ IDR sfn -> loadSource outh False sfn Nothing

1196+ LIDR sfn -> loadSource outh True sfn Nothing)

11881197 let (dir, fh) = splitFileName file

11891198 return (dropExtension fh)

11901199

11911200

11921201{- | Load idris code from file -}

1193−loadFromIFile :: Handle -> IFileType -> Idris ()

1194−loadFromIFile h i@(IBC fn src)

1202+loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()

1203+loadFromIFile h i@(IBC fn src) maxline

11951204 = do iLOG $ "Skipping " ++ getSrcFile i

11961205 idrisCatch (loadIBC fn)

11971206 (\err -> ierror $ LoadingFailed fn err)

@@ -1200,13 +1209,13 @@ loadFromIFile h i@(IBC fn src)

12001209 getSrcFile (LIDR fn) = fn

12011210 getSrcFile (IBC f src) = getSrcFile src

12021211

1203−loadFromIFile h (IDR fn) = loadSource' h False fn

1204−loadFromIFile h (LIDR fn) = loadSource' h True fn

1212+loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline

1213+loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline

12051214

12061215{-| Load idris source code and show error if something wrong happens -}

1207−loadSource' :: Handle -> Bool -> FilePath -> Idris ()

1208−loadSource' h lidr r

1209− = idrisCatch (loadSource h lidr r)

1216+loadSource' :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1217+loadSource' h lidr r maxline

1218+ = idrisCatch (loadSource h lidr r maxline)

12101219 (\e -> do setErrSpan (getErrSpan e)

12111220 ist <- getIState

12121221 case e of

@@ -1214,8 +1223,8 @@ loadSource' h lidr r

12141223 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

12151224

12161225{- | Load Idris source code-}

1217−loadSource :: Handle -> Bool -> FilePath -> Idris ()

1218−loadSource h lidr f

1226+loadSource :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1227+loadSource h lidr f toline

12191228 = do iLOG ("Reading " ++ f)

12201229 i <- getIState

12211230 let def_total = default_total i

@@ -1246,7 +1255,8 @@ loadSource h lidr f

12461255 putIState (i { default_access = Hidden, module_aliases = modAliases })

12471256 clearIBC -- start a new .ibc file

12481257 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1249− let syntax = defaultSyntax{ syn_namespace = reverse mname }

1258+ let syntax = defaultSyntax{ syn_namespace = reverse mname,

1259+ maxline = toline }

12501260 ds' <- parseProg syntax f file pos

12511261

12521262 -- Parsing done, now process declarations

src/Idris/REPL.hs+28−13

@@ -166,8 +166,8 @@ processNetCmd orig i h fn cmd

166166 Left err -> do hPutStrLn h (show err)

167167 return (i, fn)

168168 where

169− processNet fn Reload = processNet fn (Load fn)

170− processNet fn (Load f) =

169+ processNet fn Reload = processNet fn (Load fn Nothing)

170+ processNet fn (Load f toline) =

171171 do let ist = orig { idris_options = idris_options i

172172 , idris_colourTheme = idris_colourTheme i

173173 , idris_colourRepl = False

@@ -177,7 +177,7 @@ processNetCmd orig i h fn cmd

177177 setOutH h

178178 setQuiet True

179179 setVerbose False

180− mods <- loadInputs h [f]

180+ mods <- loadInputs h [f] toline

181181 ist <- getIState

182182 return (ist, f)

183183 processNet fn c = do process h fn c

@@ -258,7 +258,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

258258 clearErr

259259 putIState (orig { idris_options = idris_options i,

260260 idris_outputmode = (IdeSlave id) })

261− loadInputs stdout [filename]

261+ loadInputs stdout [filename] Nothing

262262 isetPrompt (mkPrompt [filename])

263263 -- Report either success or failure

264264 i <- getIState

@@ -474,14 +474,14 @@ processInput cmd orig inputs

474474 , idris_colourTheme = idris_colourTheme i

475475 }

476476 clearErr

477− mods <- loadInputs stdout inputs

477+ mods <- loadInputs stdout inputs Nothing

478478 return (Just inputs)

479− Success (Load f) ->

479+ Success (Load f toline) ->

480480 do putIState orig { idris_options = idris_options i

481481 , idris_colourTheme = idris_colourTheme i

482482 }

483483 clearErr

484− mod <- loadInputs stdout [f]

484+ mod <- loadInputs stdout [f] toline

485485 return (Just [f])

486486 Success (ModImport f) ->

487487 do clearErr

@@ -530,7 +530,7 @@ edit f orig

530530 putIState $ orig { idris_options = idris_options i

531531 , idris_colourTheme = idris_colourTheme i

532532 }

533− loadInputs stdout [f]

533+ loadInputs stdout [f] Nothing

534534-- clearOrigPats

535535 iucheck

536536 return ()

@@ -994,8 +994,8 @@ idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

994994 [] -> return ()

995995

996996

997−loadInputs :: Handle -> [FilePath] -> Idris ()

998−loadInputs h inputs

997+loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()

998+loadInputs h inputs toline -- furthest line to read in input source files

999999 = idrisCatch

10001000 (do ist <- getIState

10011001 -- if we're in --check and not outputting anything, don't bother

@@ -1056,7 +1056,18 @@ loadInputs h inputs

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

10571057 tryLoad keepstate (f : fs)

10581058 = do ist <- getIState

1059− loadFromIFile h f

1059+ let maxline

1060+ = case toline of

1061+ Nothing -> Nothing

1062+ Just l -> case f of

1063+ IDR fn -> if any (fmatch fn) inputs

1064+ then Just l

1065+ else Nothing

1066+ LIDR fn -> if any (fmatch fn) inputs

1067+ then Just l

1068+ else Nothing

1069+ _ -> Nothing

1070+ loadFromIFile h f maxline

10601071 inew <- getIState

10611072 -- FIXME: Save these in IBC to avoid this hack! Need to

10621073 -- preserve it all from source inputs

@@ -1072,6 +1083,10 @@ loadInputs h inputs

10721083 ibc (IBC _ _) = True

10731084 ibc _ = False

10741085

1086+ fmatch ('.':'/':xs) ys = fmatch xs ys

1087+ fmatch xs ('.':'/':ys) = fmatch xs ys

1088+ fmatch xs ys = xs == ys

1089+

10751090 findNewIBC :: IFileType -> Idris (Maybe IFileType)

10761091 findNewIBC i@(IBC _ _) = return (Just i)

10771092 findNewIBC s@(IDR f) = do ist <- get

@@ -1181,7 +1196,7 @@ idrisMain opts =

11811196 iputStrLn banner

11821197

11831198 orig <- getIState

1184− loadInputs stdout inputs

1199+ loadInputs stdout inputs Nothing

11851200

11861201 runIO $ hSetBuffering stdout LineBuffering

11871202

@@ -1278,7 +1293,7 @@ initScript = do script <- getInitScript

12781293 case parseCmd i input cmd of

12791294 Failure err -> runIO $ print (fixColour clr err)

12801295 Success Reload -> iPrintError "Init scripts cannot reload the file"

1281− Success (Load f) -> iPrintError "Init scripts cannot load files"

1296+ Success (Load f _) -> iPrintError "Init scripts cannot load files"

12821297 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

12831298 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

12841299 Success Proofs -> proofs i

src/Idris/REPLParser.hs+6−1

@@ -48,7 +48,12 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

4848 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

4949 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

5050 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51− <|> try (do cmd ["l", "load"]; f <- many anyChar; return (Load f))

51+ <|> try (do cmd ["lto", "loadto"];

52+ toline <- P.natural

53+ f <- many anyChar;

54+ return (Load f (Just (fromInteger toline))))

55+ <|> try (do cmd ["l", "load"]; f <- many anyChar;

56+ return (Load f Nothing))

5257 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

5358 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

5459 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))