git.iko.soy/Idris-dev
on master help sign in
Merge branch 'repl'

Conflicts: CHANGELOG src/Idris/AbsSyntaxTree.hs

commit42fb8bf19f554d7f4a9b8529a5dcef1a4996dcb1 authorraichoo <raichoo@googlemail.com> dateWed 30 Apr 2014, 22:02 (12 years ago) parent34e25c28522683
4 files changed+21−10
compare with master
unifiedsplit
CHANGELOG+1 src/Idris/AbsSyntaxTree.hs+5−5 src/Idris/Help.hs+1−2 src/Idris/REPLParser.hs+14−3
CHANGELOG+1
@@ -7,6 +7,7 @@ New in 0.9.13:
77 REPL. This is useful for writing more portable tests.
88* Many more of the basic functions and datatypes are documented.
99* Removed javascript lib in favor of idris-hackers/iQuery
10+* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
1011
1112Internal changes
1213
src/Idris/AbsSyntaxTree.hs+5−5
@@ -124,7 +124,7 @@ data IState = IState {
124124 idris_calledgraph :: Ctxt [Name],
125125 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
126126 idris_tyinfodata :: Ctxt TIData,
127− idris_totcheck :: [(FC, Name)], -- names to check totality on
127+ idris_totcheck :: [(FC, Name)], -- names to check totality on
128128 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
129129 idris_options :: IOption,
130130 idris_name :: Int,
@@ -298,7 +298,7 @@ data Command = Quit
298298 | AddMissing Bool Int Name
299299 | MakeWith Bool Int Name
300300 | DoProofSearch Bool -- ^ update
301− Bool -- ^ recursive (i.e. do arguments too)
301+ Bool -- ^ recursive (i.e. do arguments too)
302302 Int Name [Name]
303303 | SetOpt Opt
304304 | UnsetOpt Opt
@@ -440,7 +440,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
440440 | Implicit -- implicit coercion
441441 | CExport String -- export, with a C name
442442 | 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
444444 | Reflection -- a reflecting function, compile-time only
445445 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
446446 deriving (Show, Eq)
@@ -843,10 +843,10 @@ deriving instance NFData ClassInfo
843843-- Type inference data
844844
845845data 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
847847 deriving Show
848848
849−data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
849+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
850850 detaggable :: Bool }
851851 deriving Show
852852{-!
src/Idris/Help.hs+1−2
@@ -49,8 +49,7 @@ help =
4949 ([":showproof"], NameArg, "Show proof"),
5050 ([":proofs"], NoArg, "Show available proofs"),
5151 ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),
52− ([":c",":compile"], FileArg, "Compile to an executable <filename>"),
53− ([":js", ":javascript"], FileArg, "Compile to JavaScript <filename>"),
52+ ([":c",":compile"], FileArg, "Compile to an executable [codegen] <filename>"),
5453 ([":exec",":execute"], NoArg, "Compile to an executable and run"),
5554 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),
5655 ([":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)
3838 return (ModImport (toPath f)))
3939 <|> try (do cmd ["e", "edit"]; eof; return Edit)
4040 <|> try (do cmd ["exec", "execute"]; eof; return Execute)
41− <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))
42− <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))
43− <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))
41+ <|> try (do cmd ["c", "compile"]
42+ i <- get
43+ c <- option (opt_codegen $ idris_options i) codegenOption
44+ f <- P.identifier
45+ eof
46+ return (Compile c f))
4447 <|> try (do cmd ["proofs"]; eof; return Proofs)
4548 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))
4649 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))
@@ -118,6 +121,14 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext
118121 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
119122 <|> do discard (P.symbol "autosolve"); return AutoSolve
120123
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+
121132pConsoleWidth :: P.IdrisParser ConsoleWidth
122133pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
123134 <|> do discard (P.symbol "infinite"); return InfinitelyWide