a5a63fc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

First lift of TODOs and FIXMEs from source to Issue Tracker.

commita5a63fc6924bac32ca2bc5e303df8a8963e619ca authorDavid Christiansen <david@davidchristiansen.dk> dateFri 3 Oct 2014, 17:34 (12 years ago) parenta4faccb bc74c4f

4 files changed+28−15

compare with master

unifiedsplit

src/Idris/Docs.hs+3−3 src/Idris/Parser.hs+7−2 src/Idris/REPL.hs+11−6 src/Pkg/Package.hs+7−4

src/Idris/Docs.hs+3−3

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

1515import qualified Data.Text as T

1616

1717-- 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

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

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

2123 PTerm -- function type

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

203205 t (Str _) = PConstant StrType

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

205207 t _ = PType

206−

207−

src/Idris/Parser.hs+7−2

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

399399@

400400-}

401401-- 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

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

403406fnOpts opts

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

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

914917

915918{-| Parses with pattern

916919

917−@

920+@

918921WExpr ::= '|' Expr';

919922@

920923-}

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

11611164 case runparser mainProg i fname input of

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

11631166 -- this can't be the solution!

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

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

11641169 let (fc, msg) = findFC doc

11651170 i <- getIState

11661171 case idris_outputmode i of

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

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

12731278 clearIBC -- start a new .ibc file

12741279 -- record package info in .ibc

1275− imps <- allImportDirs

1280+ imps <- allImportDirs

12761281 mapM_ addIBC (map IBCImportDir imps)

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

12781283 let syntax = defaultSyntax{ syn_namespace = reverse mname,

src/Idris/REPL.hs+11−6

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

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

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

729729 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

731731 elabDecl EAll recinfo tyDecl

732732 elabClauses recinfo fc opts name (concatMap getClauses decls)

733733 setReplDefined (Just name)

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

767767 fixClauses :: PDecl' t -> PDecl' t

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

769769 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) =

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

772772 fixClauses decl = decl

773773

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

777777 undefine [] = do

778778 allDefined <- idris_repl_defs `fmap` get

779779 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

781781 -- print them out to the user afterward

782782 undefine names = undefine' names []

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

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

784784 return ()

785785 undefine' (n:names) already = do

786786 allDefined <- idris_repl_defs `fmap` get

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

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

795795 fputState (ctxt_lookup n . known_classes) Nothing

796796 fmodifyState repl_definitions (delete n)

797− undefClosure n =

797+ undefClosure n =

798798 do replDefs <- idris_repl_defs `fmap` get

799799 callGraph <- whoCalls n

800800 let users = case lookup n callGraph of

801801 Just ns -> nub ns

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

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

803803 undefinedJustNow <- concat `fmap` mapM undefClosure users

804804 undefOne n

805805 return (nub (n : undefinedJustNow))

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

13411341 iWarn f $ pprintErr i e'

13421342 ProgramLineComment -> return () -- fail elsewhere

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

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

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

13441346 iWarn emptyFC $ pprintErr i e)

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

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

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

13621364 inew <- getIState

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

13641366 -- preserve it all from source inputs

1367+ --

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

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

13651370 let tidata = idris_tyinfodata inew

13661371 let patdefs = idris_patdefs inew

13671372 ok <- noErrors

src/Pkg/Package.hs+7−4

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

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

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

6565 _ -> when install $ installPkg pkgdesc

66−-- ms -> do if install

66+-- ms -> do if install

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

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

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

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

7070-- exitWith (ExitFailure 1)

7171

7272-- | Type check packages only

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

107107 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

108108

109109 if (f /= "")

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

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

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

112112 runIO $ setCurrentDirectory dir

113113

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

129129-- | Generate IdrisDoc for package

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

131131-- 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

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

133136 -> IO ()

134137documentPkg fp =

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

143146 make (makefile pkgdesc)

144147 setCurrentDirectory $ pkgDir

145148 let run l = runErrorT . (execStateT l)

146− load [] = return ()

149+ load [] = return ()

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

148151 loader = do idrisMain opts; load fs

149152 idrisInstance <- run loader idrisInit