9acf2c4 · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -66,6 +66,8 @@ Extra-source-files:

66

67 rts/*.c

68 rts/*.h

69+ rts/windows/*.c

70+ rts/windows/*.h

69 rts/Makefile

71 rts/Makefile

70

72

71 libs/Makefile

73 libs/Makefile

@@ -557,6 +559,7 @@ Library

557 , Idris.Transforms

559 , Idris.Transforms

558 , Idris.Unlit

560 , Idris.Unlit

559 , Idris.WhoCalls

561 , Idris.WhoCalls

562+ , Idris.CmdOptions

560

563

561 , IRTS.BCImp

564 , IRTS.BCImp

562 , IRTS.Bytecode

565 , IRTS.Bytecode

@@ -626,6 +629,7 @@ Library

626 , xml

629 , xml

627 , deepseq

630 , deepseq

628 , zlib

631 , zlib

632+ , optparse-applicative

629 Extensions: MultiParamTypeClasses

633 Extensions: MultiParamTypeClasses

630 , FunctionalDependencies

634 , FunctionalDependencies

631 , FlexibleContexts

635 , FlexibleContexts

libs/prelude/Prelude.idr+31−9

@@ -347,27 +347,38 @@ natRange n = List.reverse (go n)

347 where go Z = []

348 go (S n) = n :: go n

349

350+-- predifine Nat versions of Enum, so we can use them in the default impls

351+total natEnumFromThen : Nat -> Nat -> Stream Nat

352+natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc

353+total natEnumFromTo : Nat -> Nat -> List Nat

354+natEnumFromTo n m = map (plus n) (natRange ((S m) - n))

355+total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat

356+natEnumFromThenTo _ Z _ = []

357+natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))

358+

350class Enum a where

359class Enum a where

351 total pred : a -> a

360 total pred : a -> a

352 total succ : a -> a

361 total succ : a -> a

362+ succ e = fromNat (S (toNat e))

353 total toNat : a -> Nat

363 total toNat : a -> Nat

354 total fromNat : Nat -> a

364 total fromNat : Nat -> a

355 total enumFrom : a -> Stream a

365 total enumFrom : a -> Stream a

356 enumFrom n = n :: enumFrom (succ n)

366 enumFrom n = n :: enumFrom (succ n)

357 total enumFromThen : a -> a -> Stream a

367 total enumFromThen : a -> a -> Stream a

368+ enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))

358 total enumFromTo : a -> a -> List a

369 total enumFromTo : a -> a -> List a

370+ enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))

359 total enumFromThenTo : a -> a -> a -> List a

371 total enumFromThenTo : a -> a -> a -> List a

360−

372+ enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))

361

373

362instance Enum Nat where

374instance Enum Nat where

363− pred = Nat.pred

375+ pred n = Nat.pred n

364− succ = S

376+ succ n = S n

365− toNat = id

377+ toNat x = id x

366− fromNat = id

378+ fromNat x = id x

367− enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc

379+ enumFromThen x y = natEnumFromThen x y

368− enumFromThenTo _ Z _ = []

380+ enumFromThenTo x y z = natEnumFromThenTo x y z

369− enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))

381+ enumFromTo x y = natEnumFromTo x y

370− enumFromTo n m = map (plus n) (natRange ((S m) - n))

371

382

372instance Enum Integer where

383instance Enum Integer where

373 pred n = n - 1

384 pred n = n - 1

@@ -407,6 +418,17 @@ instance Enum Int where

407 go [] = []

418 go [] = []

408 go (x :: xs) = n + (cast x * inc) :: go xs

419 go (x :: xs) = n + (cast x * inc) :: go xs

409

420

421+instance Enum (Fin (S n)) where

422+ pred fZ = fZ

423+ pred (fS n) = weaken n

424+ succ n = case strengthen (fS n) of

425+ Left _ => last

426+ Right k => k

427+ toNat n = cast n

428+ fromNat {n=n} m = case natToFin m (S n) of

429+ Just k => k

430+ Nothing => last

431+

410syntax "[" [start] ".." [end] "]"

432syntax "[" [start] ".." [end] "]"

411 = enumFromTo start end

433 = enumFromTo start end

412syntax "[" [start] "," [next] ".." [end] "]"

434syntax "[" [start] "," [next] ".." [end] "]"

main/Main.hs+2−63

@@ -24,6 +24,7 @@ import Idris.ElabDecls

24import Idris.Primitives

25import Idris.Imports

26import Idris.Error

27+import Idris.CmdOptions

27

28

28import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )

29import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )

29

30

@@ -36,8 +37,7 @@ import Paths_idris

36-- Main program reads command line options, parses the main program, and gets

37-- Main program reads command line options, parses the main program, and gets

37-- on with the REPL.

38-- on with the REPL.

38

39

39−main = do xs <- getArgs

40+main = do opts <- runArgParser

40− let opts = parseArgs xs

41 result <- runErrorT $ execStateT (runIdris opts) idrisInit

42 case result of

43 Left err -> putStrLn $ "Uncaught error: " ++ show err

@@ -48,8 +48,6 @@ runIdris [Client c] = do setVerbose False

48 setQuiet True

49 runIO $ runClient c

50runIdris opts = do

51− when (Ver `elem` opts) $ runIO showver

52− when (Usage `elem` opts) $ runIO usage

53 when (ShowIncs `elem` opts) $ runIO showIncs

51 when (ShowIncs `elem` opts) $ runIO showIncs

54 when (ShowLibs `elem` opts) $ runIO showLibs

52 when (ShowLibs `elem` opts) $ runIO showLibs

55 when (ShowLibdir `elem` opts) $ runIO showLibdir

53 when (ShowLibdir `elem` opts) $ runIO showLibdir

@@ -72,9 +70,6 @@ runIdris opts = do

72 _ -> ifail "Too many packages"

70 _ -> ifail "Too many packages"

73 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

71 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

74

72

75−usage = do putStrLn usagemsg

76− exitWith ExitSuccess

77−

78showver = do putStrLn $ "Idris version " ++ ver

73showver = do putStrLn $ "Idris version " ++ ver

79 exitWith ExitSuccess

74 exitWith ExitSuccess

80

75

@@ -89,59 +84,3 @@ showLibdir = do dir <- getIdrisLibDir

89showIncs = do incFlags <- getIncFlags

84showIncs = do incFlags <- getIncFlags

90 putStrLn incFlags

85 putStrLn incFlags

91 exitWith ExitSuccess

86 exitWith ExitSuccess

92−

93−usagemsghdr = "Idris version " ++ ver ++ ", (C) The Idris Community 2014"

94−

95−usagemsg = usagemsghdr ++ "\n" ++

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

97− "idris [OPTIONS] [FILE]\n\n" ++

98− "Common flags:\n" ++

99− "\t --install IPKG Install package\n" ++

100− "\t --clean IPKG Clean package\n" ++

101− "\t --build IPKG Build package\n" ++

102− "\t --mkdoc IPKG Generate IdrisDoc for package\n" ++

103− "\t -e --eval EXPR Evaluate an expression without loading the REPL\n" ++

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

105− "\t --libdir Display library directory\n" ++

106− "\t --link Display link flags\n" ++

107− "\t --include Display the includes flags\n" ++

108− "\t --nobanner Suppress the banner\n" ++

109− "\t --color, --colour Force coloured output\n" ++

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

111− "\t --errorcontent Undocumented\n" ++

112− "\t --nocoverage Undocumented\n" ++

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

114− "\t --check Undocumented\n" ++

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

116− "\t --partial Undocumented\n" ++

117− "\t --warnreach Warn about reachable but inaccessible arguments\n" ++

118− "\t --warnpartial Warn about undeclared partial functions.\n" ++

119− "\t --warn Undocumented\n" ++

120− "\t --typecase Undocumented\n" ++

121− "\t --typeintype Undocumented\n" ++

122− "\t --nobasepkgs Undocumented\n" ++

123− "\t --noprelude Undocumented\n" ++

124− "\t --nobuiltins Undocumented\n" ++

125− "\t -O --level LEVEL Undocumented\n" ++

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

127− "\t --package ITEM Undocumented\n" ++

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

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

130− "\t javascript, node, or llvm\n" ++

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

132− "\t --cpu=CPU Select target CPU e.g. corei7 or cortex-m3\n" ++

133− "\t (for LLVM codegen)\n" ++

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

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

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

137− "\t -X --extension EXT Turn on langage extension (TypeProviders or ErrorReflection)\n" ++

138− "\t --dumpdefuns Undocumented\n" ++

139− "\t --dumpcases Undocumented\n" ++

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

141− "\t --ideslave Undocumented\n" ++

142− "\t --client Undocumented\n" ++

143− "\t -h --help Display help message\n" ++

144− "\t -v --version Print version information\n" ++

145− "\t -V --verbose Loud verbosity\n" ++

146− "\t -q --quiet Quiet verbosity\n"

147−

src/IRTS/CodegenC.hs+3−4

@@ -62,7 +62,6 @@ codegenC' defs out exec incs objs libs flags dbg

62 hPutStr tmph cout

63 hFlush tmph

64 hClose tmph

65− let useclang = False

66 comp <- getCC

65 comp <- getCC

67 libFlags <- getLibFlags

66 libFlags <- getLibFlags

68 incFlags <- getIncFlags

67 incFlags <- getIncFlags

@@ -175,15 +174,15 @@ bcc i (CASE True r code def)

175 | length code < 4 = showCase i def code

174 | length code < 4 = showCase i def code

176 where

175 where

177 showCode :: Int -> [BC] -> String

176 showCode :: Int -> [BC] -> String

178− showCode i bc = "{\n" ++ indent i ++ concatMap (bcc (i + 1)) bc ++

177+ showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++

179 indent i ++ "}\n"

178 indent i ++ "}\n"

180

179

181 showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String

180 showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String

182 showCase i Nothing [(t, c)] = showCode i c

181 showCase i Nothing [(t, c)] = showCode i c

183 showCase i (Just def) [] = showCode i def

182 showCase i (Just def) [] = showCode i def

184 showCase i def ((t, c) : cs)

183 showCase i def ((t, c) : cs)

185− = "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c

184+ = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c

186− ++ "else " ++ showCase i def cs

185+ ++ indent i ++ "else " ++ showCase i def cs

187

186

188bcc i (CASE safe r code def)

187bcc i (CASE safe r code def)

189 = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++

188 = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++

src/IRTS/CodegenJavaScript.hs+25−10

@@ -296,6 +296,8 @@ jsInstanceOf = JSBinOp "instanceof"

296jsEq :: JS -> JS -> JS

297jsEq = JSBinOp "=="

298

299+jsNotEq :: JS -> JS -> JS

300+jsNotEq = JSBinOp "!="

299

301

300jsAnd :: JS -> JS -> JS

302jsAnd :: JS -> JS -> JS

301jsAnd = JSBinOp "&&"

303jsAnd = JSBinOp "&&"

@@ -1601,23 +1603,36 @@ codegenJS_all target definitions includes filename outputType = do

1601

1603

1602 mainLoop :: JS

1604 mainLoop :: JS

1603 mainLoop =

1605 mainLoop =

1604− JSAlloc "main" $ Just $ JSFunction [] (

1606+ JSAlloc "main" $ Just $ JSFunction [] (

1605− case target of

1607+ case target of

1606− Node -> mainFun

1608+ Node -> mainFun

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

1609+ JavaScript -> JSCond [ (exists document `jsAnd` isReady, mainFun)

1608− JSString "DOMContentLoaded", JSFunction [] (

1610+ , (exists window, windowMainFun)

1609− mainFun

1611+ , (JSTrue, mainFun)

1610− ), JSFalse

1611− ])]

1612+ ]

1612 )

1613 )

1613 where

1614 where

1615+ exists :: JS -> JS

1616+ exists js = (JSPreOp "typeof " js) `jsNotEq` JSString "undefined"

1617+

1614 mainFun :: JS

1618 mainFun :: JS

1615 mainFun = jsTailcall $ jsCall runMain []

1619 mainFun = jsTailcall $ jsCall runMain []

1616

1620

1621+ window :: JS

1622+ window = JSIdent "window"

1617

1623

1618− isReady :: JS

1624+ document :: JS

1619− isReady = readyState `jsEq` JSString "complete" `jsOr` readyState `jsEq` JSString "loaded"

1625+ document = JSIdent "document"

1620

1626

1627+ windowMainFun :: JS

1628+ windowMainFun = jsMeth window "addEventListener" [

1629+ JSString "DOMContentLoaded"

1630+ , JSFunction [] ( mainFun )

1631+ , JSFalse

1632+ ]

1633+

1634+ isReady :: JS

1635+ isReady = JSParens $ readyState `jsEq` JSString "complete" `jsOr` readyState `jsEq` JSString "loaded"

1621

1636

1622 readyState :: JS

1637 readyState :: JS

1623 readyState = JSProj (JSIdent "document") "readyState"

1638 readyState = JSProj (JSIdent "document") "readyState"

src/Idris/AbsSyntaxTree.hs−2

@@ -340,8 +340,6 @@ data Command = Quit

340

341

342data Opt = Filename String

343− | Ver

344− | Usage

345 | Quiet

343 | Quiet

346 | NoBanner

344 | NoBanner

347 | ColourREPL Bool

345 | ColourREPL Bool

src/Idris/CmdOptions.hsnew file+108

@@ -0,0 +1,108 @@

1+{-# LANGUAGE Arrows #-}

2+module Idris.CmdOptions where

3+

4+import Idris.AbsSyntaxTree

5+import Idris.REPL

6+

7+import IRTS.CodegenCommon

8+

9+import Options.Applicative

10+import Options.Applicative.Arrows

11+import Data.Maybe

12+

13+runArgParser :: IO [Opt]

14+runArgParser = do opts <- execParser $ info parser $

15+ header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")

16+ return $ preProcOpts opts []

17+

18+pureArgParser :: [String] -> [Opt]

19+pureArgParser args = case execParserMaybe (info parser idm) args of

20+ Just opts -> preProcOpts opts []

21+ Nothing -> []

22+

23+parser :: Parser [Opt]

24+parser = runA $ proc () -> do

25+ flags <- asA parseFlags -< ()

26+ files <- asA (many $ argument ((fmap . fmap) Filename str) (metavar "FILES")) -< ()

27+ A parseVersion >>> A helper -< (flags ++ files)

28+

29+parseFlags :: Parser [Opt]

30+parseFlags = many $

31+ flag' NoBanner (long "nobanner" <> help "Suppress the banner")

32+ <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

33+ <|> flag' Ideslave (long "ideslave")

34+ <|> (Client <$> strOption (long "client"))

35+ <|> (OLogging <$> option (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

36+ <|> flag' NoBasePkgs (long "nobasepkgs")

37+ <|> flag' NoPrelude (long "noprelude")

38+ <|> flag' NoBuiltins (long "nobuiltins")

39+ <|> flag' NoREPL (long "check")

40+ <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

41+ <|> flag' TypeCase (long "typecase")

42+ <|> flag' TypeInType (long "typeintype")

43+ <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

44+ <|> flag' DefaultPartial (long "partial")

45+ <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")

46+ <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

47+ <|> flag' NoCoverage (long "nocoverage")

48+ <|> flag' ErrContext (long "errorcontext")

49+ <|> flag' ShowLibs (long "link" <> help "Display link flags")

50+ <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

51+ <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

52+ <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

53+ <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

54+ <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

55+ <|> flag' WarnOnly (long "warn")

56+ <|> (Pkg <$> strOption (short 'p' <> long "package"))

57+ -- Package commands

58+ <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

59+ <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

60+ <|> (PkgREPL <$> strOption (long "repl"))

61+ <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

62+ <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

63+ <|> (PkgCheck <$> strOption (long "check"))

64+ -- Misc options

65+ <|> (BCAsm <$> strOption (long "bytecode"))

66+ <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

67+ <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

68+ <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")

69+ <|> (DumpDefun <$> strOption (long "dumpdefuns"))

70+ <|> (DumpCases <$> strOption (long "dumpcases"))

71+ <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Java, bytecode"))

72+ <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

73+ <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

74+ <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

75+ <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension" <> short 'X' <> metavar "EXT" <> help "Turn on langage extension (TypeProviders or ErrorReflection)"))

76+ <|> flag' (OptLevel 3) (long "O3")

77+ <|> flag' (OptLevel 2) (long "O2")

78+ <|> flag' (OptLevel 1) (long "O1")

79+ <|> flag' (OptLevel 0) (long "O0")

80+ <|> (OptLevel <$> option (short 'O' <> long "level"))

81+ <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

82+ <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

83+ <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

84+ <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

85+ where

86+ getExt s = case maybeRead s of

87+ Just ext -> ext

88+ Nothing -> error ("Unknown extension " ++ s)

89+ maybeRead = fmap fst . listToMaybe . reads

90+

91+parseVersion :: Parser (a -> a)

92+parseVersion = infoOption ver (short 'v' <> long "version" <> help "Print version information")

93+

94+preProcOpts :: [Opt] -> [Opt] -> [Opt]

95+preProcOpts [] ys = ys

96+preProcOpts (NoBuiltins:xs) ys = NoBuiltins : NoPrelude : preProcOpts xs ys

97+preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys

98+preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys

99+preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

100+

101+parseCodegen :: String -> Codegen

102+parseCodegen "C" = ViaC

103+parseCodegen "Java" = ViaJava

104+parseCodegen "bytecode" = Bytecode

105+parseCodegen "javascript" = ViaJavaScript

106+parseCodegen "node" = ViaNode

107+parseCodegen "llvm" = ViaLLVM

108+parseCodegen _ = error "unknown codegen" -- FIXME: partial function

src/Idris/IdeSlave.hs+2

@@ -172,6 +172,7 @@ data IdeSlaveCommand = REPLCompletions String

172 | AddMissing Int String

173 | MakeWithBlock Int String

174 | ProofSearch Bool Int String [String]

175+ | MakeLemma Int String

175 | LoadFile String

176 | LoadFile String

176 | DocsFor String

177 | DocsFor String

177 | Apropos String

178 | Apropos String

@@ -199,6 +200,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

199 where getHints = mapM (\h -> case h of

200 where getHints = mapM (\h -> case h of

200 StringAtom s -> Just s

201 StringAtom s -> Just s

201 _ -> Nothing)

202 _ -> Nothing)

203+sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

202sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])

204sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])

203sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

205sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

204sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

206sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

src/Idris/Interactive.hs+22−5

@@ -15,6 +15,7 @@ import Idris.ElabDecls

15import Idris.Error

16import Idris.Delaborate

17import Idris.Output

18+import Idris.IdeSlave hiding (IdeSlaveCommand(..))

18

19

19import Util.Pretty

20import Util.Pretty

20import Util.System

21import Util.System

@@ -23,6 +24,7 @@ import System.FilePath

23import System.Directory

24import System.Directory

24import System.IO

25import System.IO

25import Data.Char

26import Data.Char

27+import Data.Maybe (fromMaybe)

26

28

27

29

28caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

30caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

@@ -254,15 +256,32 @@ makeLemma h fn updatefile l n

254 do let fb = fn ++ "~"

256 do let fb = fn ++ "~"

255 runIO $ writeFile fb (addLem before tyline lem lem_app later)

257 runIO $ writeFile fb (addLem before tyline lem lem_app later)

256 runIO $ copyFile fb fn

258 runIO $ copyFile fb fn

259+ else case idris_outputmode i of

257− else ihPrintResult h $ lem ++ "\n" ++ lem_app

260+ RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

261+ IdeSlave n ->

262+ let good = SexpList [SymbolAtom "ok",

263+ SexpList [SymbolAtom "metavariable-lemma",

264+ SexpList [SymbolAtom "replace-metavariable",

265+ StringAtom lem_app],

266+ SexpList [SymbolAtom "definition-type",

267+ StringAtom lem]]]

268+ in runIO . hPutStrLn h $ convSExp "return" good n

269+

258 else do -- provisional definition

270 else do -- provisional definition

259− let lem_app = show n ++ appArgs [] mty ++

271+ let lem_app = show n ++ appArgs [] mty ++

260 " = ?" ++ show n ++ "_rhs"

272 " = ?" ++ show n ++ "_rhs"

261 if updatefile then

273 if updatefile then

262 do let fb = fn ++ "~"

274 do let fb = fn ++ "~"

263 runIO $ writeFile fb (addProv before tyline lem_app later)

275 runIO $ writeFile fb (addProv before tyline lem_app later)

264 runIO $ copyFile fb fn

276 runIO $ copyFile fb fn

277+ else case idris_outputmode i of

265− else ihPrintResult h $ lem_app

278+ RawOutput -> ihPrintResult h $ lem_app

279+ IdeSlave n ->

280+ let good = SexpList [SymbolAtom "ok",

281+ SexpList [SymbolAtom "provisional-definition-lemma",

282+ SexpList [SymbolAtom "definition-clause",

283+ StringAtom lem_app]]]

284+ in runIO . hPutStrLn h $ convSExp "return" good n

266

285

267 where getIndent s = length (takeWhile isSpace s)

286 where getIndent s = length (takeWhile isSpace s)

268

287

@@ -318,5 +337,3 @@ makeLemma h fn updatefile l n

318 unlines $ before ++ tyline :

337 unlines $ before ++ tyline :

319 (later_bef ++ [blankline, lem_app, blankline] ++

338 (later_bef ++ [blankline, lem_app, blankline] ++

320 later_end)

339 later_end)

321−

322−

src/Idris/Primitives.hs+52−5

@@ -180,9 +180,9 @@ primitives =

180 Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

181 (2, LRegisterPtr) total,

182 -- Buffers

183− Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

183+ Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_allocate)

184 (1, LAllocate) total,

185− Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_cantreduce)

185+ Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_appendBuffer)

186 (6, LAppendBuffer) partial

187 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

188 ++ concatMap vecOps vecTypes

@@ -291,10 +291,10 @@ fixedOps ity@(ITFixed _) =

291 thisTy = AType $ ATInt ity

292 appendFun en = Prim (sUN $ "prim__append" ++ tyName ++ show en)

293 (ty [BufferType, b64, b64, thisTy] BufferType)

294− 4 (p_cantreduce) (4, LAppend ity en) partial

294+ 4 (p_append en) (4, LAppend ity en) partial

295 peekFun en = Prim (sUN $ "prim__peek" ++ tyName ++ show en)

296 (ty [BufferType, b64] thisTy)

297− 2 (p_cantreduce) (2, LPeek ity en) partial

297+ 2 (p_peek ity en) (2, LPeek ity en) partial

298

299mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b

300mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))

@@ -697,6 +697,53 @@ p_strCons _ = Nothing

697p_strRev [Str xs] = Just $ Str (reverse xs)

698p_strRev _ = Nothing

699

700+p_allocate, p_appendBuffer :: [Const] -> Maybe Const

701+p_allocate [B64 _] = Just $ B8V V.empty

702+p_allocate n = Nothing

703+p_appendBuffer [B8V vect1, B64 size1, B64 count, B64 size2, B64 off, B8V vect2] =

704+ Just $ B8V (foldl (V.++)

705+ (V.slice 0 (fromIntegral size1) vect1)

706+ (replicate (fromIntegral count) (V.slice (fromIntegral off) (fromIntegral size2) vect2)))

707+p_appendBuffer n = Nothing

708+p_append :: Endianness -> [Const] -> Maybe Const

709+p_append en [B8V vect, B64 size, B64 count, val] =

710+ let bytes = case val of

711+ B8 x -> [x]

712+ B16 x -> [fromIntegral x, fromIntegral (shiftR x 8)]

713+ B32 x -> map (fromIntegral . shiftR x) [0,8..24]

714+ B64 x -> map (fromIntegral . shiftR x) [0,8..56]

715+ in Just $ B8V (foldl V.snoc

716+ (V.slice 0 (fromIntegral size) vect)

717+ (concat (replicate (fromIntegral count)

718+ (case en of

719+ BE -> reverse bytes

720+ _ -> bytes))))

721+p_append _ _ = Nothing

722+

723+p_peek :: IntTy -> Endianness -> [Const] -> Maybe Const

724+p_peek (ITFixed IT8) _ [B8V vect, B64 offset] = Just $ B8 (vect V.! fromIntegral offset)

725+p_peek (ITFixed IT16) en [B8V vect, B64 offset] =

726+ let bytes = [0..1]

727+ in Just $ B16 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))

728+ 0

729+ (case en of

730+ BE -> bytes

731+ _ -> reverse bytes))

732+p_peek (ITFixed IT32) en [B8V vect, B64 offset] =

733+ let bytes = [0..1]

734+ in Just $ B32 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))

735+ 0

736+ (case en of

737+ BE -> bytes

738+ _ -> reverse bytes))

739+p_peek (ITFixed IT64) en [B8V vect, B64 offset] =

740+ let bytes = [0..1]

741+ in Just $ B64 (foldl (\full byte -> shiftL full 8 .|. fromIntegral (vect V.! (fromIntegral offset+byte)))

742+ 0

743+ (case en of

744+ BE -> bytes

745+ _ -> reverse bytes))

746+p_peek _ _ _ = Nothing

747+

700p_cantreduce :: a -> Maybe b

748p_cantreduce :: a -> Maybe b

701p_cantreduce _ = Nothing

749p_cantreduce _ = Nothing

702−

src/Idris/REPL.hs+4−77

@@ -295,6 +295,10 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

295 process stdout fn (MakeWith False line (sUN name))

296runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =

297 process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))

298+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

299+ case splitName name of

300+ Left err -> iPrintError err

301+ Right n -> process stdout fn (MakeLemma False line n)

298runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

302runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

299 process stdout fn (Apropos a)

303 process stdout fn (Apropos a)

300runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

304runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

@@ -965,83 +969,6 @@ displayHelp = let vstr = showVersion version in

965 l ++ take (c1 - length l) (repeat ' ') ++

969 l ++ take (c1 - length l) (repeat ' ') ++

966 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

970 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

967

971

968−parseCodegen :: String -> Codegen

969−parseCodegen "C" = ViaC

970−parseCodegen "Java" = ViaJava

971−parseCodegen "bytecode" = Bytecode

972−parseCodegen "javascript" = ViaJavaScript

973−parseCodegen "node" = ViaNode

974−parseCodegen "llvm" = ViaLLVM

975−parseCodegen _ = error "unknown codegen" -- FIXME: partial function

976−

977−parseArgs :: [String] -> [Opt]

978−parseArgs [] = []

979−parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)

980−parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

981−parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)

982−parseArgs ("--client":ns) = [Client (showSep " " ns)]

983−parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

984−parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)

985−parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

986−parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)

987−parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

988−parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

989−parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

990−parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

991−parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

992−parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

993−parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

994−parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)

995−parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

996−parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

997−parseArgs ("--help":ns) = Usage : (parseArgs ns)

998−parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

999−parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

1000−parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

1001−parseArgs ("--version":ns) = Ver : (parseArgs ns)

1002−parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

1003−parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

1004−parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

1005−parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

1006−-- Package Related options

1007−parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

1008−parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

1009−parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

1010−parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

1011−parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)

1012−parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

1013−parseArgs ("--mkdoc":n:ns) = PkgMkDoc n : (parseArgs ns) -- IdrisDoc

1014−parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)

1015−-- Misc Options

1016−parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

1017−parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

1018−parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

1019−parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

1020−parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

1021−parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

1022−parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

1023−parseArgs ("--eval":expr:ns) = EvalExpr expr : parseArgs ns

1024−parseArgs ("-e":expr:ns) = EvalExpr expr : parseArgs ns

1025−parseArgs ["--exec"] = InterpretScript "Main.main" : []

1026−parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

1027−parseArgs (('-':'X':extName):ns) = case maybeRead extName of

1028− Just ext -> Extension ext : parseArgs ns

1029− -- Not sure what to do for the Nothing case

1030− Nothing -> error ("Unknown extension " ++ extName)

1031− where maybeRead = fmap fst . listToMaybe . reads

1032−parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

1033−parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

1034−parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns

1035−parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

1036−parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

1037−parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

1038−parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

1039−parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns

1040−parseArgs ("--color":ns) = ColourREPL True : parseArgs ns

1041−parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns

1042−parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns

1043−parseArgs (n:ns) = Filename n : (parseArgs ns)

1044−

1045helphead =

972helphead =

1046 [ (["Command"], SpecialHeaderArg, "Purpose"),

973 [ (["Command"], SpecialHeaderArg, "Purpose"),

1047 ([""], NoArg, "")

974 ([""], NoArg, "")

src/Pkg/PParser.hs+2−1

@@ -8,6 +8,7 @@ import Idris.Core.TT

8import Idris.REPL

9import Idris.AbsSyntaxTree

10import Idris.ParseHelpers

11+import Idris.CmdOptions

11

12

12import Paths_idris

13import Paths_idris

13

14

@@ -66,7 +67,7 @@ pClause = do reserved "executable"; lchar '=';

66 <|> do reserved "opts"; lchar '=';

67 <|> do reserved "opts"; lchar '=';

67 opts <- stringLiteral

68 opts <- stringLiteral

68 st <- get

69 st <- get

69− let args = parseArgs (words opts)

70+ let args = pureArgParser (words opts)

70 put (st { idris_opts = args })

71 put (st { idris_opts = args })

71 <|> do reserved "modules"; lchar '=';

72 <|> do reserved "modules"; lchar '=';

72 ms <- sepBy1 (iName []) (lchar ',')

73 ms <- sepBy1 (iName []) (lchar ',')

test/reg029/run+1−1

@@ -3,5 +3,5 @@ idris $@ reg029.idr -o reg029

3unset IDRIS_REG029_NONEXISTENT_VAR

4export IDRIS_REG029_EXISTENT_VAR='exists!'

5./reg029

6−idris $@ reg029.idr --exec

6+idris $@ reg029.idr --execute

7rm -f reg029 *.ibc