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

CHANGELOG+3

compare with master

unifiedsplit

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

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

14 line options.

15* 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)

16

19

17Internal changes:

20Internal changes:

18

21

src/Idris/AbsSyntaxTree.hs+2

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

143 | Check PTerm

144 | TotCheck Name

145 | Reload

146+ | Load FilePath

147+ | ModImport String

146 | Edit

148 | Edit

147 | Compile Target String

149 | Compile Target String

148 | Execute

150 | Execute

src/Idris/REPL.hs+27−15

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

81 (f:_) -> f

82 _ -> ""

83 case parseCmd i cmd of

84− Left err -> do liftIO $ print err

84+ Left err -> do liftIO $ print err

85− return (Just inputs)

85+ return (Just inputs)

86+ Right Reload ->

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

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

87− clearErr

88+ clearErr

88− mods <- mapM loadModule inputs

89+ mods <- mapM loadModule inputs

89− return (Just 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]))

90− Right Edit -> do edit fn orig

100+ Right Edit -> do edit fn orig

91− return (Just inputs)

101+ return (Just inputs)

92− Right Proofs -> do proofs orig

102+ Right Proofs -> do proofs orig

93− return (Just inputs)

103+ return (Just inputs)

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

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

95− return Nothing

105+ return Nothing

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

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

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

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

98− return (Just inputs)

108+ return (Just inputs)

99

109

100resolveProof :: Name -> Idris Name

110resolveProof :: Name -> Idris Name

101resolveProof n'

111resolveProof n'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/REPLParser.hs+6

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

23pCmd = 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 ["l", "load"]; f <- getInput; return (Load f))

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

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

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

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

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

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

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

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

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

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

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

56 <|> do eof; return NOP

59 <|> do eof; return NOP

57

60

61+ where dot '.' = '/'

62+ dot c = c

63+

58pOption :: IParser Opt

64pOption :: IParser Opt

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

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

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

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

tutorial/examples/binary.idr+2−2

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

1−module main

1+module Main

2

3data Binary : Nat -> Set where

4 bEnd : Binary O

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

40

41---------- Proofs ----------

42

43−main.parity_lemma_1 = proof {

43+parity_lemma_1 = proof {

44 intros;

45 rewrite sym (plusSuccRightSucc j j);

46 trivial;

tutorial/examples/bmain.idr+1−1

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

1−module main

1+module Main

2

3import btree

4

tutorial/examples/hello.idr+1−1

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

1−module main

1+module Main

2

3main : IO ()

4main = putStrLn "Hello world"

tutorial/examples/interp.idr+1−1

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

1−module main

1+module Main

2

3data Ty = TyInt | TyBool| TyFun Ty Ty

4