ec86b47 · 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 into typed-laziness

ec86b47Edwin Brady13 years ago

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

compare with master

unifiedsplit

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

49deleteAt _ [] impossible

51replaceAt : 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

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

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+

55--------------------------------------------------------------------------------

59--------------------------------------------------------------------------------

56-- Subvectors

60-- Subvectors

57--------------------------------------------------------------------------------

61--------------------------------------------------------------------------------

main/Main.hs+12−12

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

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

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

94 "Common flags:\n" ++

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

129 "\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" ++

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

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

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

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

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

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

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

src/IRTS/CodegenJavaScript.hs+33−3

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

231jsAnd = JSBinOp "&&"

232

233

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

235+jsOr = JSBinOp "||"

236+

237+

234jsType :: JS

238jsType :: JS

235jsType = JSIdent $ idrRTNamespace ++ "Type"

239jsType = JSIdent $ idrRTNamespace ++ "Type"

236

240

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

1027

1031

1028 extractLocalConstructors' :: JS -> [JS]

1032 extractLocalConstructors' :: JS -> [JS]

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

1033 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)]

1031 where

1035 where

1032 cons :: [(JS, JS)]

1036 cons :: [(JS, JS)]

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

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

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

1043 | otherwise = []

1047 | otherwise = []

1044

1048

1045

1049

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+

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

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

1047 allocCon (js, JSIdent name) =

1069 allocCon (js, JSIdent name) =

1048 JSAlloc name (Just js)

1070 JSAlloc name (Just js)

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

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

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

1248 case target of

1270 case target of

1249 Node -> mainFun

1271 Node -> mainFun

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

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

1251 JSString "DOMContentLoaded", JSFunction [] (

1273 JSString "DOMContentLoaded", JSFunction [] (

1252 mainFun

1274 mainFun

1253 ), JSFalse

1275 ), JSFalse

1254− ]

1276+ ])]

1255 )

1277 )

1256 where

1278 where

1257 mainFun :: JS

1279 mainFun :: JS

1258 mainFun = jsTailcall $ jsCall runMain []

1280 mainFun = jsTailcall $ jsCall runMain []

1259

1281

1260

1282

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+

1261 runMain :: String

1291 runMain :: String

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

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

1263

1293

src/Idris/AbsSyntax.hs+22−3

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

579type1Doc :: Doc OutputAnnotation

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

581

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+

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

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

583ihPrintError h s = do i <- getIState

596ihPrintError h s = do i <- getIState

584 case idris_outputmode i of

597 case idris_outputmode i of

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

619 case idris_outputmode i of

632 case idris_outputmode i of

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

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

621

634

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

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

623ihWarn h fc err = do i <- getIState

636ihWarn h fc err = do i <- getIState

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

624 case idris_outputmode i of

638 case idris_outputmode i of

639+ RawOutput ->

640+ runIO $

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

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

642+ IdeSlave n ->

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

644+ runIO . hPutStrLn h $

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

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

627

646

628setLogLevel :: Int -> Idris ()

647setLogLevel :: Int -> Idris ()

629setLogLevel l = do i <- getIState

648setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+2−2

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

38import Data.Char(isLetter, toLower)

39import Data.List.Split (splitOn)

41−import Util.Pretty(pretty)

41+import Util.Pretty(pretty, text)

43recheckC fc env t

44 = 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

2008

2009 warnMissing decls ns iname meth

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

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

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

2012 | otherwise = return ()

2013

2014 checkInClass ns meth

src/Idris/Error.hs+1−1

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

44 let h = idris_outh ist

45 case e of

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

47− ihWarn h fc $ pshow ist e

47+ ihWarn h fc $ pprintErr ist e

48 _ -> do setErrLine (getErrLine e)

49 ihputStrLn h $ pshow ist e

src/Idris/IdeSlave.hs+4

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

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

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

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+

72instance SExpable NameOutput where

76instance SExpable NameOutput where

73 toSExp TypeOutput = SymbolAtom "type"

77 toSExp TypeOutput = SymbolAtom "type"

74 toSExp FunOutput = SymbolAtom "function"

78 toSExp FunOutput = SymbolAtom "function"

src/Idris/Parser.hs+4−3

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

38import Paths_idris

40import Util.DynamicLinker

41+import qualified Util.Pretty as P

42import Idris.Core.TT

43import Idris.Core.TT

43import Idris.Core.Evaluate

44import Idris.Core.Evaluate

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

1119 i <- getIState

1120 i <- getIState

1120 case idris_outputmode i of

1121 case idris_outputmode i of

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

1122 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)

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

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

1124 return []

1125 return []

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

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

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

1186loadSource' h lidr r

1187loadSource' h lidr r

1187 = idrisCatch (loadSource h lidr r)

1188 = idrisCatch (loadSource h lidr r)

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

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

1189− msg <- showErr e

1190+ ist <- getIState

1190− ihputStrLn h msg)

1191+ ihRenderError h (pprintErr ist e))

1191

1192

1192{- | Load Idris source code-}

1193{- | Load Idris source code-}

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

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

src/Idris/REPL.hs+4−3

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

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

228 idrisCatch

229 (process stdout fn (Prove n'))

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

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

231 isetPrompt (mkPrompt mods)

232 Success cmd -> idrisCatch

233 (ideslaveProcess fn cmd)

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

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

235 Just (IdeSlave.REPLCompletions str) ->

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

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

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

1126 (\e -> do i <- getIState

1127 case e of

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

1129− iputStrLn (show e)

1129+ ihRenderError stdout $ pprintErr i e

1130 ProgramLineComment -> return () -- fail elsewhere

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

1132 iputStrLn (pshow i e))

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

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

1185 putIState (i { default_total = True })

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

1187+ when (not runrepl) $ setWidth InfinitelyWide

1187 mapM_ addLangExt (opt getLanguageExt opts)

1188 mapM_ addLangExt (opt getLanguageExt opts)

1188 setREPL runrepl

1189 setREPL runrepl

1189 setQuiet (quiet || isJust script)

1190 setQuiet (quiet || isJust script)