d676ca6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added -o option, and :exec and :t at the REPL

d676ca6Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+8−2

compare with master

unifiedsplit

@@ -128,6 +128,12 @@ logLvl l str = do i <- get

128iLOG :: String -> Idris ()

129iLOG = logLvl 1

130

131+noErrors :: Idris Bool

132+noErrors = do i <- get

133+ case errLine i of

134+ Nothing -> return True

135+ _ -> return False

136+

131setTypeCase :: Bool -> Idris ()

137setTypeCase :: Bool -> Idris ()

132setTypeCase t = do i <- get

138setTypeCase t = do i <- get

133 let opts = idris_options i

139 let opts = idris_options i

@@ -136,8 +142,8 @@ setTypeCase t = do i <- get

136

142

137-- Commands in the REPL

143-- Commands in the REPL

138

144

139−data Command = Quit | Help | Eval PTerm | Reload | Edit

140− | Compile String

146+ | Compile String | Execute String

141 | Metavars | Prove Name

147 | Metavars | Prove Name

142 | TTShell

148 | TTShell

143 | LogLvl Int | Spec PTerm | HNF PTerm

149 | LogLvl Int | Spec PTerm | HNF PTerm

src/Idris/REPL.hs+12−1

@@ -86,6 +86,12 @@ process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t

86 logLvl 3 $ "Raw: " ++ show (tm', ty')

87 iputStrLn (show (delab ist tm') ++ " : " ++

88 show (delab ist ty'))

89+process _ (Check t) = do (tm, ty) <- elabVal toplevel False t

90+ ctxt <- getContext

91+ ist <- get

92+ let ty' = normaliseC ctxt [] ty

93+ iputStrLn (show (delab ist tm) ++ " : " ++

94+ show (delab ist ty'))

89process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t

95process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t

90 ctxt <- getContext

96 ctxt <- getContext

91 ist <- get

97 ist <- get

@@ -101,6 +107,9 @@ process _ TTShell = do ist <- get

101 let shst = initState (tt_ctxt ist)

107 let shst = initState (tt_ctxt ist)

102 shst' <- lift $ runShell shst

108 shst' <- lift $ runShell shst

103 return ()

109 return ()

110+process _ (Execute f) = do compile f

111+ lift $ system ("./" ++ f)

112+ return ()

104process _ (Compile f) = do compile f

113process _ (Compile f) = do compile f

105process _ (LogLvl i) = setLogLevel i

114process _ (LogLvl i) = setLogLevel i

106process _ Metavars = do ist <- get

115process _ Metavars = do ist <- get

@@ -114,7 +123,7 @@ displayHelp = let vstr = showVersion version in

114 "\nIdris version " ++ vstr ++ "\n" ++

123 "\nIdris version " ++ vstr ++ "\n" ++

115 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

124 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

116 concatMap cmdInfo help

125 concatMap cmdInfo help

117− where cmdInfo (cmds, args, text) = " " ++ col 14 14 (showSep " " cmds) args text

126+ where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text

118 col c1 c2 l m r =

127 col c1 c2 l m r =

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

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

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

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

@@ -123,11 +132,13 @@ help =

123 [ (["Command"], "Arguments", "Purpose"),

132 [ (["Command"], "Arguments", "Purpose"),

124 ([""], "", ""),

133 ([""], "", ""),

125 (["<expression>"], "", "Evaluate an expression"),

134 (["<expression>"], "", "Evaluate an expression"),

135+ ([":t"], "<expression>", "Check the type of an expression"),

126 ([":r",":reload"], "", "Reload current file"),

136 ([":r",":reload"], "", "Reload current file"),

127 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

137 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

128 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

138 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

129 ([":p",":prove"], "<name>", "Prove a metavariable"),

139 ([":p",":prove"], "<name>", "Prove a metavariable"),

130 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

140 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

141+ ([":exec",":execute"], "<filename>", "Compile to an executable <filename> and run"),

131 ([":?",":h",":help"], "", "Display this help text"),

142 ([":?",":h",":help"], "", "Display this help text"),

132 ([":q",":quit"], "", "Exit the Idris system")

143 ([":q",":quit"], "", "Exit the Idris system")

133 ]

144 ]

src/Idris/REPLParser.hs+2

@@ -24,6 +24,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

24 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

25 <|> try (do cmd ["r", "reload"]; eof; return Reload)

26 <|> try (do cmd ["e", "edit"]; eof; return Edit)

27+ <|> try (do cmd ["exec", "execute"]; f <- identifier; eof; return (Execute f))

27 <|> try (do cmd ["ttshell"]; eof; return TTShell)

28 <|> try (do cmd ["ttshell"]; eof; return TTShell)

28 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

29 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

29 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

30 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

@@ -31,6 +32,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

31 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

32 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

32 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

33 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

33 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

34 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

35+ <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

34 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

36 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

35 <|> do eof; return NOP

37 <|> do eof; return NOP

src/Main.hs+12−1

@@ -32,6 +32,7 @@ data Opt = Filename String

32 | NoPrelude

33 | NoREPL

34 | OLogging Int

35+ | Output String

35 | TypeCase

36 | TypeCase

36 deriving Eq

37 deriving Eq

@@ -43,13 +44,18 @@ runIdris :: [Opt] -> Idris ()

43runIdris opts =

44runIdris opts =

44 do let inputs = opt getFile opts

45 do let inputs = opt getFile opts

45 let runrepl = not (NoREPL `elem` opts)

46 let runrepl = not (NoREPL `elem` opts)

47+ let output = opt getOutput opts

46 mapM_ makeOption opts

48 mapM_ makeOption opts

47 elabPrims

49 elabPrims

48 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

50 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

49 return ()

51 return ()

50 when runrepl $ iputStrLn banner

52 when runrepl $ iputStrLn banner

51 ist <- get

53 ist <- get

52− mods <- mapM loadModule inputs

54+ mods <- mapM loadModule inputs

55+ ok <- noErrors

56+ when ok $ case output of

57+ [] -> return ()

58+ (o:_) -> process "" (Compile o)

53 when runrepl $ repl ist inputs

59 when runrepl $ repl ist inputs

54 where

60 where

55 makeOption (OLogging i) = setLogLevel i

61 makeOption (OLogging i) = setLogLevel i

@@ -60,6 +66,10 @@ getFile :: Opt -> Maybe String

60getFile (Filename str) = Just str

66getFile (Filename str) = Just str

61getFile _ = Nothing

67getFile _ = Nothing

69+getOutput :: Opt -> Maybe String

70+getOutput (Output str) = Just str

71+getOutput _ = Nothing

72+

63opt :: (Opt -> Maybe a) -> [Opt] -> [a]

73opt :: (Opt -> Maybe a) -> [Opt] -> [a]

64opt = mapMaybe

74opt = mapMaybe

@@ -71,6 +81,7 @@ parseArgs [] = return []

71parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

81parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

72parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

82parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

73parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

83parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

84+parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

74parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

85parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

75parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

86parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)