d676ca6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitd676ca6c52f47835af14e79a131687716ff7fc22 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 9 Nov 2011, 18:00 (15 years ago) parenta4a77bf

4 files changed+34−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+8−2 src/Idris/REPL.hs+12−1 src/Idris/REPLParser.hs+2 src/Main.hs+12−1

src/Idris/AbsSyntax.hs+8−2

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

128128iLOG :: String -> Idris ()

129129iLOG = logLvl 1

130130

131+noErrors :: Idris Bool

132+noErrors = do i <- get

133+ case errLine i of

134+ Nothing -> return True

135+ _ -> return False

136+

131137setTypeCase :: Bool -> Idris ()

132138setTypeCase t = do i <- get

133139 let opts = idris_options i

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

136142

137143-- Commands in the REPL

138144

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

140− | Compile String

146+ | Compile String | Execute String

141147 | Metavars | Prove Name

142148 | TTShell

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

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

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

8888 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'))

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

9096 ctxt <- getContext

9197 ist <- get

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

101107 let shst = initState (tt_ctxt ist)

102108 shst' <- lift $ runShell shst

103109 return ()

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

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

112+ return ()

104113process _ (Compile f) = do compile f

105114process _ (LogLvl i) = setLogLevel i

106115process _ Metavars = do ist <- get

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

114123 "\nIdris version " ++ vstr ++ "\n" ++

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

116125 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

118127 col c1 c2 l m r =

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

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

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

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

124133 ([""], "", ""),

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

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

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

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

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

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

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

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

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

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

133144 ]

src/Idris/REPLParser.hs+2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3537 <|> do eof; return NOP

3638

src/Main.hs+12−1

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

3232 | NoPrelude

3333 | NoREPL

3434 | OLogging Int

35+ | Output String

3536 | TypeCase

3637 deriving Eq

3738

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

4344runIdris opts =

4445 do let inputs = opt getFile opts

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

47+ let output = opt getOutput opts

4648 mapM_ makeOption opts

4749 elabPrims

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

4951 return ()

5052 when runrepl $ iputStrLn banner

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

5359 when runrepl $ repl ist inputs

5460 where

5561 makeOption (OLogging i) = setLogLevel i

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

6066getFile (Filename str) = Just str

6167getFile _ = Nothing

6268

69+getOutput :: Opt -> Maybe String

70+getOutput (Output str) = Just str

71+getOutput _ = Nothing

72+

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

6474opt = mapMaybe

6575

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

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

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

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

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

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

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

7687