42fb8bf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'repl'

42fb8bfraichoo12 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -7,6 +7,7 @@ New in 0.9.13:

7 REPL. This is useful for writing more portable tests.

8* Many more of the basic functions and datatypes are documented.

9* Removed javascript lib in favor of idris-hackers/iQuery

10+* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)

11Internal changes

12Internal changes

src/Idris/AbsSyntaxTree.hs+5−5

@@ -124,7 +124,7 @@ data IState = IState {

124 idris_calledgraph :: Ctxt [Name],

125 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),

126 idris_tyinfodata :: Ctxt TIData,

127− idris_totcheck :: [(FC, Name)], -- names to check totality on

127+ idris_totcheck :: [(FC, Name)], -- names to check totality on

128 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

129 idris_options :: IOption,

130 idris_name :: Int,

@@ -298,7 +298,7 @@ data Command = Quit

298 | AddMissing Bool Int Name

299 | MakeWith Bool Int Name

300 | DoProofSearch Bool -- ^ update

301− Bool -- ^ recursive (i.e. do arguments too)

301+ Bool -- ^ recursive (i.e. do arguments too)

302 Int Name [Name]

303 | SetOpt Opt

304 | UnsetOpt Opt

@@ -440,7 +440,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

440 | Implicit -- implicit coercion

441 | CExport String -- export, with a C name

442 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

443− | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

443+ | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

444 | Reflection -- a reflecting function, compile-time only

445 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

446 deriving (Show, Eq)

@@ -843,10 +843,10 @@ deriving instance NFData ClassInfo

843-- Type inference data

844

845data TIData = TIPartial -- ^ a function with a partially defined type

846− | TISolution [Term] -- ^ possible solutions to a metavariable in a type

846+ | TISolution [Term] -- ^ possible solutions to a metavariable in a type

847 deriving Show

848

849−data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting

849+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting

850 detaggable :: Bool }

851 deriving Show

852{-!

src/Idris/Help.hs+1−2

@@ -49,8 +49,7 @@ help =

49 ([":showproof"], NameArg, "Show proof"),

50 ([":proofs"], NoArg, "Show available proofs"),

51 ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),

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

52+ ([":c",":compile"], FileArg, "Compile to an executable [codegen] <filename>"),

53− ([":js", ":javascript"], FileArg, "Compile to JavaScript <filename>"),

54 ([":exec",":execute"], NoArg, "Compile to an executable and run"),

53 ([":exec",":execute"], NoArg, "Compile to an executable and run"),

55 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),

54 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),

56 ([":dynamic"], NoArg, "List dynamically loaded C libraries"),

55 ([":dynamic"], NoArg, "List dynamically loaded C libraries"),

src/Idris/REPLParser.hs+14−3

@@ -38,9 +38,12 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

38 return (ModImport (toPath f)))

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

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

41− <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))

41+ <|> try (do cmd ["c", "compile"]

42− <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))

42+ i <- get

43− <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))

43+ c <- option (opt_codegen $ idris_options i) codegenOption

44+ f <- P.identifier

45+ eof

46+ return (Compile c f))

44 <|> try (do cmd ["proofs"]; eof; return Proofs)

47 <|> try (do cmd ["proofs"]; eof; return Proofs)

45 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

48 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

46 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

49 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

@@ -118,6 +121,14 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext

118 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

121 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

119 <|> do discard (P.symbol "autosolve"); return AutoSolve

122 <|> do discard (P.symbol "autosolve"); return AutoSolve

120

123

124+codegenOption :: P.IdrisParser Codegen

125+codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

126+ <|> do discard (P.symbol "node"); return ViaNode

127+ <|> do discard (P.symbol "Java"); return ViaJava

128+ <|> do discard (P.symbol "llvm"); return ViaLLVM

129+ <|> do discard (P.symbol "bytecode"); return Bytecode

130+ <|> do discard (P.symbol "C"); return ViaC

131+

121pConsoleWidth :: P.IdrisParser ConsoleWidth

132pConsoleWidth :: P.IdrisParser ConsoleWidth

122pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

133pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

123 <|> do discard (P.symbol "infinite"); return InfinitelyWide

134 <|> do discard (P.symbol "infinite"); return InfinitelyWide