ec86b47 · Idris-dev · git.iko.soy

libs/prelude/Prelude/Vect.idr+5−1

@@ -49,9 +49,13 @@ deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

4949deleteAt _ [] impossible

5050

5151replaceAt : Fin n -> t -> Vect n t -> Vect n t

52−replaceAt fZ y (x::xs) = y::xs

52+replaceAt fZ y (x::xs) = y :: xs

5353replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

5454

55+updateAt : Fin n -> (t -> t) -> Vect n t -> Vect n t

56+updateAt fZ f (x::xs) = f x :: xs

57+updateAt (fS k) f (x::xs) = x :: updateAt k f xs

58+

5559--------------------------------------------------------------------------------

5660-- Subvectors

5761--------------------------------------------------------------------------------

main/Main.hs+12−12

@@ -92,10 +92,10 @@ usagemsg = usagemsghdr ++ "\n" ++

9292 map (\x -> '-') usagemsghdr ++ "\n" ++

9393 "idris [OPTIONS] [FILE]\n\n" ++

9494 "Common flags:\n" ++

95− "\t --install=IPKG Install package\n" ++

96− "\t --clean=IPKG Clean package\n" ++

97− "\t --build=IPKG Build package\n" ++

98− "\t --exec=EXPR Execute as idris\n" ++

95+ "\t --install IPKG Install package\n" ++

96+ "\t --clean IPKG Clean package\n" ++

97+ "\t --build IPKG Build package\n" ++

98+ "\t --exec EXPR Execute as idris\n" ++

9999 "\t --libdir Display library directory\n" ++

100100 "\t --link Display link directory\n" ++

101101 "\t --include Display the includes directory\n" ++

@@ -104,7 +104,7 @@ usagemsg = usagemsghdr ++ "\n" ++

104104 "\t --nocolor, --nocolour Disable coloured output\n" ++

105105 "\t --errorcontent Undocumented\n" ++

106106 "\t --nocoverage Undocumented\n" ++

107− "\t -o --output=FILE Specify output file\n" ++

107+ "\t -o --output FILE Specify output file\n" ++

108108 "\t --check Undocumented\n" ++

109109 "\t --total Require functions to be total by default\n" ++

110110 "\t --partial Undocumented\n" ++

@@ -115,11 +115,11 @@ usagemsg = usagemsghdr ++ "\n" ++

115115 "\t --nobasepkgs Undocumented\n" ++

116116 "\t --noprelude Undocumented\n" ++

117117 "\t --nobuiltins Undocumented\n" ++

118− "\t -O --level=LEVEL Undocumented\n" ++

119− "\t -i --idrispath=DIR Add directory to the list of import paths\n" ++

120− "\t --package=ITEM Undocumented\n" ++

121− "\t --ibcsubdir=FILE Write IBC files into sub directory\n" ++

122− "\t --codegen=TARGET Select code generator: C, Java, bytecode,\n" ++

118+ "\t -O --level LEVEL Undocumented\n" ++

119+ "\t -i --idrispath DIR Add directory to the list of import paths\n" ++

120+ "\t --package ITEM Undocumented\n" ++

121+ "\t --ibcsubdir FILE Write IBC files into sub directory\n" ++

122+ "\t --codegen TARGET Select code generator: C, Java, bytecode,\n" ++

123123 "\t javascript, node, or llvm\n" ++

124124 "\t --mvn Create a maven project (for Java codegen)\n" ++

125125 "\t --cpu=CPU Select tartget CPU e.g. corei7 or cortex-m3\n" ++

@@ -127,10 +127,10 @@ usagemsg = usagemsghdr ++ "\n" ++

127127 "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

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

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

130− "\t -X --extension=ITEM Undocumented\n" ++

130+ "\t -X --extension ITEM Undocumented\n" ++

131131 "\t --dumpdefuns Undocumented\n" ++

132132 "\t --dumpcases Undocumented\n" ++

133− "\t --log=LEVEL --loglevel Debugging log level\n" ++

133+ "\t --log LEVEL --loglevel Debugging log level\n" ++

134134 "\t --ideslave Undocumented\n" ++

135135 "\t --client Undocumented\n" ++

136136 "\t -h --help Display help message\n" ++

src/IRTS/CodegenJavaScript.hs+33−3

@@ -231,6 +231,10 @@ jsAnd :: JS -> JS -> JS

231231jsAnd = JSBinOp "&&"

232232

233233

234+jsOr :: JS -> JS -> JS

235+jsOr = JSBinOp "||"

236+

237+

234238jsType :: JS

235239jsType = JSIdent $ idrRTNamespace ++ "Type"

236240

@@ -1027,7 +1031,7 @@ extractLocalConstructors js =

10271031

10281032 extractLocalConstructors' :: JS -> [JS]

10291033 extractLocalConstructors' js@(JSAlloc fun (Just (JSFunction args body))) =

1030− map allocCon cons ++ [foldr (uncurry jsSubst) js (reverse cons)]

1034+ addCons cons [foldr (uncurry jsSubst) js (reverse cons)]

10311035 where

10321036 cons :: [(JS, JS)]

10331037 cons = zipWith genName (foldJS match (++) [] body) [1..]

@@ -1043,6 +1047,24 @@ extractLocalConstructors js =

10431047 | otherwise = []

10441048

10451049

1050+ addCons :: [(JS, JS)] -> [JS] -> [JS]

1051+ addCons [] js = js

1052+ addCons (con@(_, name):cons) js

1053+ | sum (map (countOccur name) js) > 0 =

1054+ addCons cons ((allocCon con) : js)

1055+ | otherwise =

1056+ addCons cons js

1057+

1058+

1059+ countOccur :: JS -> JS -> Int

1060+ countOccur ident js = foldJS match (+) 0 js

1061+ where

1062+ match :: JS -> Int

1063+ match js

1064+ | js == ident = 1

1065+ | otherwise = 0

1066+

1067+

10461068 allocCon :: (JS, JS) -> JS

10471069 allocCon (js, JSIdent name) =

10481070 JSAlloc name (Just js)

@@ -1247,17 +1269,25 @@ codegenJavaScript target definitions filename outputType = do

12471269 JSAlloc "main" $ Just $ JSFunction [] (

12481270 case target of

12491271 Node -> mainFun

1250− JavaScript -> jsMeth (JSIdent "window") "addEventListener" [

1272+ JavaScript -> JSCond [(isReady, mainFun), (JSTrue, jsMeth (JSIdent "window") "addEventListener" [

12511273 JSString "DOMContentLoaded", JSFunction [] (

12521274 mainFun

12531275 ), JSFalse

1254− ]

1276+ ])]

12551277 )

12561278 where

12571279 mainFun :: JS

12581280 mainFun = jsTailcall $ jsCall runMain []

12591281

12601282

1283+ isReady :: JS

1284+ isReady = readyState `jsEq` JSString "complete" `jsOr` readyState `jsEq` JSString "loaded"

1285+

1286+

1287+ readyState :: JS

1288+ readyState = JSProj (JSIdent "document") "readyState"

1289+

1290+

12611291 runMain :: String

12621292 runMain = idrNamespace ++ translateName (sMN 0 "runMain")

12631293

src/Idris/AbsSyntax.hs+22−3

@@ -579,6 +579,19 @@ fancifyAnnots _ annot = annot

579579type1Doc :: Doc OutputAnnotation

580580type1Doc = (annotate AnnConstType $ text "Type 1")

581581

582+-- | Show an error with semantic highlighting

583+ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

584+ihRenderError h e = do ist <- getIState

585+ case idris_outputmode ist of

586+ RawOutput -> consoleDisplayAnnotated h e

587+ IdeSlave n -> do

588+ (str, spans) <- fmap displaySpans .

589+ iRender .

590+ fmap (fancifyAnnots ist) $

591+ e

592+ let good = [SymbolAtom "error", toSExp str, toSExp spans]

593+ runIO . hPutStrLn h $ convSExp "return" good n

594+

582595ihPrintError :: Handle -> String -> Idris ()

583596ihPrintError h s = do i <- getIState

584597 case idris_outputmode i of

@@ -619,11 +632,17 @@ isetPrompt p = do i <- getIState

619632 case idris_outputmode i of

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

621634

622−ihWarn :: Handle -> FC -> String -> Idris ()

635+ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

623636ihWarn h fc err = do i <- getIState

637+ err' <- iRender . fmap (fancifyAnnots i) $ err

624638 case idris_outputmode i of

625− RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)

626− IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n

639+ RawOutput ->

640+ runIO $

641+ hPutStrLn h (show fc ++ ":" ++ displayDecorated (consoleDecorate i) err')

642+ IdeSlave n ->

643+ do let (str, spans) = displaySpans err'

644+ runIO . hPutStrLn h $

645+ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, str, spans) n

627646

628647setLogLevel :: Int -> Idris ()

629648setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+2−2

@@ -38,7 +38,7 @@ import qualified Data.Text as T

3838import Data.Char(isLetter, toLower)

3939import Data.List.Split (splitOn)

4040

41−import Util.Pretty(pretty)

41+import Util.Pretty(pretty, text)

4242

4343recheckC fc env t

4444 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -2008,7 +2008,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20082008

20092009 warnMissing decls ns iname meth

20102010 | null $ filter (clauseFor meth iname ns) decls

2011− = iWarn fc $ "method " ++ show meth ++ " not defined"

2011+ = iWarn fc . text $ "method " ++ show meth ++ " not defined"

20122012 | otherwise = return ()

20132013

20142014 checkInClass ns meth

src/Idris/Error.hs+1−1

@@ -44,7 +44,7 @@ setAndReport e = do ist <- getIState

4444 let h = idris_outh ist

4545 case e of

4646 At fc@(FC f l c) e -> do setErrLine l

47− ihWarn h fc $ pshow ist e

47+ ihWarn h fc $ pprintErr ist e

4848 _ -> do setErrLine (getErrLine e)

4949 ihputStrLn h $ pshow ist e

5050

src/Idris/IdeSlave.hs+4

@@ -69,6 +69,10 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

6969instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where

7070 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]

7171

72+instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>

73+ SExpable (a, b, c, d, e) where

74+ toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

75+

7276instance SExpable NameOutput where

7377 toSExp TypeOutput = SymbolAtom "type"

7478 toSExp FunOutput = SymbolAtom "function"

src/Idris/Parser.hs+4−3

@@ -38,6 +38,7 @@ import Idris.ParseData

3838import Paths_idris

3939

4040import Util.DynamicLinker

41+import qualified Util.Pretty as P

4142

4243import Idris.Core.TT

4344import Idris.Core.Evaluate

@@ -1119,7 +1120,7 @@ parseProg syn fname input mrk

11191120 i <- getIState

11201121 case idris_outputmode i of

11211122 RawOutput -> ihputStrLn (idris_outh i) (show doc)

1122− IdeSlave n -> ihWarn (idris_outh i) fc msg

1123+ IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

11231124 putIState (i { errLine = Just (fc_line fc) }) -- Just errl })

11241125 return []

11251126 Success (x, i) -> do putIState i

@@ -1186,8 +1187,8 @@ loadSource' :: Handle -> Bool -> FilePath -> Idris ()

11861187loadSource' h lidr r

11871188 = idrisCatch (loadSource h lidr r)

11881189 (\e -> do setErrLine (getErrLine e)

1189− msg <- showErr e

1190− ihputStrLn h msg)

1190+ ist <- getIState

1191+ ihRenderError h (pprintErr ist e))

11911192

11921193{- | Load Idris source code-}

11931194loadSource :: Handle -> Bool -> FilePath -> Idris ()

src/Idris/REPL.hs+4−3

@@ -227,11 +227,11 @@ ideslave orig mods

227227 Success (Prove n') -> do iPrintResult ""

228228 idrisCatch

229229 (process stdout fn (Prove n'))

230− (\e -> getIState >>= iPrintError . flip pshow e)

230+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

231231 isetPrompt (mkPrompt mods)

232232 Success cmd -> idrisCatch

233233 (ideslaveProcess fn cmd)

234− (\e -> getIState >>= iPrintError . flip pshow e)

234+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

235235 Just (IdeSlave.REPLCompletions str) ->

236236 do (unused, compls) <- replCompletion (reverse str, "")

237237 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

@@ -1126,7 +1126,7 @@ loadInputs h inputs

11261126 (\e -> do i <- getIState

11271127 case e of

11281128 At f _ -> do setErrLine (fc_line f)

1129− iputStrLn (show e)

1129+ ihRenderError stdout $ pprintErr i e

11301130 ProgramLineComment -> return () -- fail elsewhere

11311131 _ -> do setErrLine 3 -- FIXME! Propagate it

11321132 iputStrLn (pshow i e))

@@ -1184,6 +1184,7 @@ idrisMain opts =

11841184 when (DefaultTotal `elem` opts) $ do i <- getIState

11851185 putIState (i { default_total = True })

11861186 setColourise $ not quiet && last (True : opt getColour opts)

1187+ when (not runrepl) $ setWidth InfinitelyWide

11871188 mapM_ addLangExt (opt getLanguageExt opts)

11881189 setREPL runrepl

11891190 setQuiet (quiet || isJust script)