a5a63fc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1578 from jfdm/tidyup/lift-todos-1

a5a63fcDavid Christiansen12 years ago

src/Idris/Docs.hs+3−3

compare with master

unifiedsplit

@@ -15,7 +15,9 @@ import Data.List

15import qualified Data.Text as T

17-- TODO: Only include names with public/abstract accessibility

18−

18+--

19+-- Issue #1573 on the Issue tracker.

20+-- https://github.com/idris-lang/Idris-dev/issues/1573

19data FunDoc = FD Name (Docstring (Maybe Term))

21data FunDoc = FD Name (Docstring (Maybe Term))

20 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs

22 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs

21 PTerm -- function type

23 PTerm -- function type

@@ -203,5 +205,3 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty

203 t (Str _) = PConstant StrType

205 t (Str _) = PConstant StrType

204 t (Ch c) = PConstant $ AType (ATInt ITChar)

206 t (Ch c) = PConstant $ AType (ATInt ITChar)

205 t _ = PType

207 t _ = PType

206−

207−

src/Idris/Parser.hs+7−2

@@ -399,6 +399,9 @@ NameTimesList ::=

399@

400-}

401-- FIXME: Check compatability for function options (i.e. partal/total)

402+--

403+-- Issue #1574 on the issue tracker.

404+-- https://github.com/idris-lang/Idris-dev/issues/1574

402fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

405fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

403fnOpts opts

406fnOpts opts

404 = do reserved "total"; fnOpts (TotalFn : opts)

407 = do reserved "total"; fnOpts (TotalFn : opts)

@@ -914,7 +917,7 @@ clause syn

914

917

915{-| Parses with pattern

918{-| Parses with pattern

916

919

917−@

920+@

918WExpr ::= '|' Expr';

921WExpr ::= '|' Expr';

919@

922@

920-}

923-}

@@ -1161,6 +1164,8 @@ parseProg syn fname input mrk

1161 case runparser mainProg i fname input of

1164 case runparser mainProg i fname input of

1162 Failure doc -> do -- FIXME: Get error location from trifecta

1165 Failure doc -> do -- FIXME: Get error location from trifecta

1163 -- this can't be the solution!

1166 -- this can't be the solution!

1167+ -- Issue #1575 on the issue tracker.

1168+ -- https://github.com/idris-lang/Idris-dev/issues/1575

1164 let (fc, msg) = findFC doc

1169 let (fc, msg) = findFC doc

1165 i <- getIState

1170 i <- getIState

1166 case idris_outputmode i of

1171 case idris_outputmode i of

@@ -1272,7 +1277,7 @@ loadSource lidr f toline

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

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

1273 clearIBC -- start a new .ibc file

1278 clearIBC -- start a new .ibc file

1274 -- record package info in .ibc

1279 -- record package info in .ibc

1275− imps <- allImportDirs

1280+ imps <- allImportDirs

1276 mapM_ addIBC (map IBCImportDir imps)

1281 mapM_ addIBC (map IBCImportDir imps)

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

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

1278 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1283 let syntax = defaultSyntax{ syn_namespace = reverse mname,

src/Idris/REPL.hs+11−6

@@ -727,7 +727,7 @@ process fn (NewDefn decls) = do

727 getClauseName (PClause fc name whole with rhs whereBlock) = name

728 getClauseName (PWith fc name whole with rhs whereBlock) = name

729 defineName :: [PDecl] -> Idris ()

730− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

730+ defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

731 elabDecl EAll recinfo tyDecl

732 elabClauses recinfo fc opts name (concatMap getClauses decls)

733 setReplDefined (Just name)

@@ -767,7 +767,7 @@ process fn (NewDefn decls) = do

767 fixClauses :: PDecl' t -> PDecl' t

768 fixClauses (PClauses fc opts _ css@(clause:cs)) =

769 PClauses fc opts (getClauseName clause) css

770− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

770+ fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

771 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

772 fixClauses decl = decl

773

@@ -777,10 +777,10 @@ process fn (Undefine names) = undefine names

777 undefine [] = do

778 allDefined <- idris_repl_defs `fmap` get

779 undefine' allDefined []

780− -- Keep track of which names you've removed so you can

780+ -- Keep track of which names you've removed so you can

781 -- print them out to the user afterward

782 undefine names = undefine' names []

783− undefine' [] list = do iRenderOutput $ printUndefinedNames list

783+ undefine' [] list = do iRenderOutput $ printUndefinedNames list

784 return ()

785 undefine' (n:names) already = do

786 allDefined <- idris_repl_defs `fmap` get

@@ -794,12 +794,12 @@ process fn (Undefine names) = undefine names

794 -- smart detection of exactly what kind of name we're undefining.

795 fputState (ctxt_lookup n . known_classes) Nothing

796 fmodifyState repl_definitions (delete n)

797− undefClosure n =

797+ undefClosure n =

798 do replDefs <- idris_repl_defs `fmap` get

799 callGraph <- whoCalls n

800 let users = case lookup n callGraph of

801 Just ns -> nub ns

802− Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)

802+ Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)

803 undefinedJustNow <- concat `fmap` mapM undefClosure users

804 undefOne n

805 return (nub (n : undefinedJustNow))

@@ -1341,6 +1341,8 @@ loadInputs inputs toline -- furthest line to read in input source files

1341 iWarn f $ pprintErr i e'

1342 ProgramLineComment -> return () -- fail elsewhere

1343 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1344+ -- Issue #1576 on the issue tracker.

1345+ -- https://github.com/idris-lang/Idris-dev/issues/1576

1344 iWarn emptyFC $ pprintErr i e)

1346 iWarn emptyFC $ pprintErr i e)

1345 where -- load all files, stop if any fail

1347 where -- load all files, stop if any fail

1346 tryLoad :: Bool -> [IFileType] -> Idris ()

1348 tryLoad :: Bool -> [IFileType] -> Idris ()

@@ -1362,6 +1364,9 @@ loadInputs inputs toline -- furthest line to read in input source files

1362 inew <- getIState

1364 inew <- getIState

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

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

1364 -- preserve it all from source inputs

1366 -- preserve it all from source inputs

1367+ --

1368+ -- Issue #1577 on the issue tracker.

1369+ -- https://github.com/idris-lang/Idris-dev/issues/1577

1365 let tidata = idris_tyinfodata inew

1370 let tidata = idris_tyinfodata inew

1366 let patdefs = idris_patdefs inew

1371 let patdefs = idris_patdefs inew

1367 ok <- noErrors

1372 ok <- noErrors

src/Pkg/Package.hs+7−4

@@ -63,10 +63,10 @@ buildPkg warnonly (install, fp)

63 -- Also give up if there are metavariables to solve

64 case (map fst (idris_metavars ist) \\ primDefs) of

65 _ -> when install $ installPkg pkgdesc

66−-- ms -> do if install

66+-- ms -> do if install

67-- then putStrLn "Can't install: there are undefined metavariables:"

68-- else putStrLn "There are undefined metavariables:"

69−-- putStrLn $ "\t" ++ show ms

69+-- putStrLn $ "\t" ++ show ms

70-- exitWith (ExitFailure 1)

72-- | Type check packages only

@@ -107,7 +107,7 @@ replPkg fp = do orig <- getIState

107 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

108

109 if (f /= "")

110− then idrisMain ((Filename f) : opts)

110+ then idrisMain ((Filename f) : opts)

111 else iputStrLn "Can't start REPL: no main module given"

112 runIO $ setCurrentDirectory dir

113

@@ -129,6 +129,9 @@ cleanPkg fp

129-- | Generate IdrisDoc for package

130-- TODO: Handle case where module does not contain a matching namespace

131-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins

132+--

133+-- Issue number #1572 on the issue tracker

134+-- https://github.com/idris-lang/Idris-dev/issues/1572

132documentPkg :: FilePath -- ^ Path to .ipkg file.

135documentPkg :: FilePath -- ^ Path to .ipkg file.

133 -> IO ()

136 -> IO ()

134documentPkg fp =

137documentPkg fp =

@@ -143,7 +146,7 @@ documentPkg fp =

143 make (makefile pkgdesc)

146 make (makefile pkgdesc)

144 setCurrentDirectory $ pkgDir

147 setCurrentDirectory $ pkgDir

145 let run l = runErrorT . (execStateT l)

148 let run l = runErrorT . (execStateT l)

146− load [] = return ()

149+ load [] = return ()

147 load (f:fs) = do loadModule f; load fs

150 load (f:fs) = do loadModule f; load fs

148 loader = do idrisMain opts; load fs

151 loader = do idrisMain opts; load fs

149 idrisInstance <- run loader idrisInit

152 idrisInstance <- run loader idrisInit