665676b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added :l and :m commands to REPL

commit665676b620865e2f636d557cd745ac625106e22d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 29 Oct 2012, 09:46 (14 years ago) parent3f6fd87

8 files changed+43−20

compare with master

unifiedsplit

CHANGELOG+3 src/Idris/AbsSyntaxTree.hs+2 src/Idris/REPL.hs+27−15 src/Idris/REPLParser.hs+6 tutorial/examples/binary.idr+2−2 tutorial/examples/bmain.idr+1−1 tutorial/examples/hello.idr+1−1 tutorial/examples/interp.idr+1−1

CHANGELOG+3

@@ -13,6 +13,9 @@ User visible changes:

1313 as allowed to be partial. Also "--total" and "--partial" added as command

1414 line options.

1515* New termination checker supporting mutually recursive definitions.

16+* Added ':load' command to REPL, for loading a new file

17+* Added ':module' command to REPL, for adding modules

18+* Renamed library modules (now have initial capital)

1619

1720Internal changes:

1821

src/Idris/AbsSyntaxTree.hs+2

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

143143 | Check PTerm

144144 | TotCheck Name

145145 | Reload

146+ | Load FilePath

147+ | ModImport String

146148 | Edit

147149 | Compile Target String

148150 | Execute

src/Idris/REPL.hs+27−15

@@ -81,21 +81,31 @@ processInput cmd orig inputs

8181 (f:_) -> f

8282 _ -> ""

8383 case parseCmd i cmd of

84− Left err -> do liftIO $ print err

85− return (Just inputs)

86− Right Reload -> do put (orig { idris_options = idris_options i })

87− clearErr

88− mods <- mapM loadModule inputs

89− return (Just inputs)

90− Right Edit -> do edit fn orig

91− return (Just inputs)

92− Right Proofs -> do proofs orig

93− return (Just inputs)

94− Right Quit -> do iputStrLn "Bye bye"

95− return Nothing

96− Right cmd -> do idrisCatch (process fn cmd)

97− (\e -> iputStrLn (show e))

98− return (Just inputs)

84+ Left err -> do liftIO $ print err

85+ return (Just inputs)

86+ Right Reload ->

87+ do put (orig { idris_options = idris_options i })

88+ clearErr

89+ mods <- mapM loadModule inputs

90+ return (Just inputs)

91+ Right (Load f) ->

92+ do put (orig { idris_options = idris_options i })

93+ clearErr

94+ mod <- loadModule f

95+ return (Just [f])

96+ Right (ModImport f) ->

97+ do clearErr

98+ fmod <- loadModule f

99+ return (Just (inputs ++ [fmod]))

100+ Right Edit -> do edit fn orig

101+ return (Just inputs)

102+ Right Proofs -> do proofs orig

103+ return (Just inputs)

104+ Right Quit -> do iputStrLn "Bye bye"

105+ return Nothing

106+ Right cmd -> do idrisCatch (process fn cmd)

107+ (\e -> iputStrLn (show e))

108+ return (Just inputs)

99109

100110resolveProof :: Name -> Idris Name

101111resolveProof n'

@@ -438,6 +448,8 @@ help =

438448 ([":i", ":info"], "<name>", "Display information about a type class"),

439449 ([":total"], "<name>", "Check the totality of a name"),

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

451+ ([":l",":load"], "<filename>", "Load a new file"),

452+ ([":m",":module"], "<module>", "Import an extra module"),

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

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

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

src/Idris/REPLParser.hs+6

@@ -23,6 +23,9 @@ pCmd :: IParser Command

2323pCmd = 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)

26+ <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

27+ <|> try (do cmd ["m", "module"]; f <- identifier; eof;

28+ return (ModImport (map dot f)))

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

2730 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

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

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

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

5659 <|> do eof; return NOP

5760

61+ where dot '.' = '/'

62+ dot c = c

63+

5864pOption :: IParser Opt

5965pOption = do discard (symbol "errorcontext"); return ErrContext

6066 <|> do discard (symbol "showimplicits"); return ShowImpl

tutorial/examples/binary.idr+2−2

@@ -1,4 +1,4 @@

1−module main

1+module Main

33data Binary : Nat -> Set where

44 bEnd : Binary O

@@ -40,7 +40,7 @@ main = do putStr "Enter a number: "

4040

4141---------- Proofs ----------

4242

43−main.parity_lemma_1 = proof {

43+parity_lemma_1 = proof {

4444 intros;

4545 rewrite sym (plusSuccRightSucc j j);

4646 trivial;

tutorial/examples/bmain.idr+1−1

@@ -1,4 +1,4 @@

1−module main

1+module Main

33import btree

tutorial/examples/hello.idr+1−1

@@ -1,4 +1,4 @@

1−module main

1+module Main

33main : IO ()

44main = putStrLn "Hello world"

tutorial/examples/interp.idr+1−1

@@ -1,4 +1,4 @@

1−module main

1+module Main

33data Ty = TyInt | TyBool| TyFun Ty Ty