git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
5b10b97Edwin Brady
idris.cabal+1
compare with master
unifiedsplit
@@ -357,6 +357,7 @@ Executable idris
357 , Util.Pretty
357 , Util.Pretty
358 , Util.System
358 , Util.System
359 , Util.DynamicLinker
359 , Util.DynamicLinker
360+ , Util.Net
360
361
361 , Pkg.Package
362 , Pkg.Package
362 , Pkg.PParser
363 , Pkg.PParser
src/IRTS/CodegenC.hs+1
@@ -37,6 +37,7 @@ codegenC defs out exec incs objs libs flags dbg
37 let cout = headers incs ++ debug dbg ++ h ++ cc ++
37 let cout = headers incs ++ debug dbg ++ h ++ cc ++
38 (if (exec == Executable) then mprog else "")
38 (if (exec == Executable) then mprog else "")
39 case exec of
39 case exec of
40+ MavenProject -> putStrLn ("FAILURE: output type not supported")
40 Raw -> writeFile out cout
41 Raw -> writeFile out cout
41 _ -> do
42 _ -> do
42 (tmpn, tmph) <- tempfile
43 (tmpn, tmph) <- tempfile
src/IRTS/CodegenCommon.hs+1−1
@@ -7,7 +7,7 @@ import Control.Exception
7import System.Environment
7import System.Environment
8
8
9data DbgLevel = NONE | DEBUG | TRACE deriving Eq
9data DbgLevel = NONE | DEBUG | TRACE deriving Eq
10−data OutputType = Raw | Object | Executable deriving (Eq, Show)
10+data OutputType = Raw | Object | Executable | MavenProject deriving (Eq, Show)
11
11
12environment :: String -> IO (Maybe String)
12environment :: String -> IO (Maybe String)
13environment x = Control.Exception.catch (do e <- getEnv x
13environment x = Control.Exception.catch (do e <- getEnv x
src/IRTS/CodegenJava.hs+117−51
@@ -37,66 +37,132 @@ import System.Process
37
37
38-----------------------------------------------------------------------
38-----------------------------------------------------------------------
39-- Main function
39-- Main function
40−
41codegenJava :: [(Name, SExp)] -> -- initialization of globals
40codegenJava :: [(Name, SExp)] -> -- initialization of globals
42− [(Name, SDecl)] ->
41+ [(Name, SDecl)] -> -- decls
43 FilePath -> -- output file name
42 FilePath -> -- output file name
44 [String] -> -- headers
43 [String] -> -- headers
45 [String] -> -- libs
44 [String] -> -- libs
46 OutputType ->
45 OutputType ->
47 IO ()
46 IO ()
48−codegenJava globalInit defs out hdrs libs exec = do
47+codegenJava globalInit defs out hdrs libs exec =
48+ withTgtDir exec out (codegenJava' exec)
49+ where
50+ codegenJava' :: OutputType -> FilePath -> IO ()
51+ codegenJava' Raw tgtDir = do
52+ srcDir <- prepareSrcDir exec tgtDir
53+ generateJavaFile globalInit defs hdrs srcDir out
54+ codegenJava' MavenProject tgtDir = do
55+ codegenJava' Raw tgtDir
56+ generatePom tgtDir out libs
57+ codegenJava' Object tgtDir = do
58+ codegenJava' MavenProject tgtDir
59+ invokeMvn tgtDir "compile"
60+ copyClassFiles tgtDir out
61+ cleanUpTmp tgtDir
62+ codegenJava' _ tgtDir = do
63+ codegenJava' MavenProject tgtDir
64+ invokeMvn tgtDir "package";
65+ copyJar tgtDir out
66+ makeJarExecutable out
67+ cleanUpTmp tgtDir
68+
69+-----------------------------------------------------------------------
70+-- Compiler IO
71+
72+withTgtDir :: OutputType -> FilePath -> (FilePath -> IO ()) -> IO ()
73+withTgtDir Raw out action = action (dropFileName out)
74+withTgtDir MavenProject out action = createDirectoryIfMissing False out >> action out
49− withTempdir (takeBaseName out) $ \ tmpDir -> do
75+withTgtDir _ out action = withTempdir (takeBaseName out) action
76+
77+prepareSrcDir :: OutputType -> FilePath -> IO FilePath
78+prepareSrcDir Raw tgtDir = return tgtDir
79+prepareSrcDir _ tgtDir = do
50− let srcdir = tmpDir </> "src" </> "main" </> "java"
80+ let srcDir = (tgtDir </> "src" </> "main" </> "java")
51− createDirectoryIfMissing True srcdir
81+ createDirectoryIfMissing True srcDir
52− let (Ident clsName) = either error id (mkClassName out)
82+ return srcDir
53− let outjava = srcdir </> clsName <.> "java"
83+
84+javaFileName :: FilePath -> FilePath -> FilePath
85+javaFileName srcDir out =
86+ either error (\ (Ident clsName) -> srcDir </> clsName <.> "java") (mkClassName out)
87+
88+generateJavaFile :: [(Name, SExp)] -> -- initialization of globals
89+ [(Name, SDecl)] -> -- definitions
90+ [String] -> -- headers
91+ FilePath -> -- Source dir
92+ FilePath -> -- output target
93+ IO ()
94+generateJavaFile globalInit defs hdrs srcDir out = do
54− let jout = either error
95+ let code = either error
55 (prettyPrint)-- flatIndent . prettyPrint)
96 (prettyPrint)-- flatIndent . prettyPrint)
56 (evalStateT (mkCompilationUnit globalInit defs hdrs out) mkCodeGenEnv)
97 (evalStateT (mkCompilationUnit globalInit defs hdrs out) mkCodeGenEnv)
57− writeFile outjava jout
98+ writeFile (javaFileName srcDir out) code
58− if (exec == Raw)
99+
59− then copyFile outjava (takeDirectory out </> clsName <.> "java")
100+pomFileName :: FilePath -> FilePath
60− else do
101+pomFileName tgtDir = tgtDir </> "pom.xml"
102+
103+generatePom :: FilePath -> -- tgt dir
104+ FilePath -> -- output target
105+ [String] -> -- libs
106+ IO ()
107+generatePom tgtDir out libs = do
61− execPom <- getExecutablePom
108+ execPom <- getExecutablePom
62− execPomTemplate <- TIO.readFile execPom
109+ execPomTemplate <- TIO.readFile execPom
110+ let (Ident clsName) = either error id (mkClassName out)
63− let execPom = T.replace (T.pack "$MAIN-CLASS$")
111+ let execPom = T.replace (T.pack "$MAIN-CLASS$")
64− (T.pack clsName)
112+ (T.pack clsName)
65− (T.replace (T.pack "$ARTIFACT-NAME$")
113+ (T.replace (T.pack "$ARTIFACT-NAME$")
66− (T.pack $ takeBaseName out)
114+ (T.pack $ takeBaseName out)
67− (T.replace (T.pack "$DEPENDENCIES$")
115+ (T.replace (T.pack "$DEPENDENCIES$")
68− (mkPomDependencies libs)
116+ (mkPomDependencies libs)
69− execPomTemplate
117+ execPomTemplate
70− )
118+ )
71− )
119+ )
72− TIO.writeFile (tmpDir </> "pom.xml") execPom
120+ TIO.writeFile (pomFileName tgtDir) execPom
121+
122+invokeMvn :: FilePath -> String -> IO ()
123+invokeMvn tgtDir command = do
73− mvnCmd <- getMvn
124+ mvnCmd <- getMvn
74− let args = ["-f", (tmpDir </> "pom.xml")]
125+ let args = ["-f", pomFileName tgtDir]
75− (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ ["compile"]) ""
126+ (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ [command]) ""
127+ when (exit /= ExitSuccess) $
76− when (exit /= ExitSuccess) $ error ("FAILURE: " ++ mvnCmd ++ " compile\n" ++ err ++ mvout)
128+ error ("FAILURE: " ++ mvnCmd ++ " " ++ command ++ "\n" ++ err ++ mvout)
77− if (exec == Object)
129+
78− then do
130+classFileDir :: FilePath -> FilePath
79− classFiles <-
131+classFileDir tgtDir = tgtDir </> "target" </> "classes"
132+
133+copyClassFiles :: FilePath -> FilePath -> IO ()
134+copyClassFiles tgtDir out = do
80− map (\ clsFile -> tmpDir </> "target" </> "classes" </> clsFile)
135+ classFiles <- map (\ clsFile -> classFileDir tgtDir </> clsFile)
81 . filter ((".class" ==) . takeExtension)
136 . filter ((".class" ==) . takeExtension)
82− <$> getDirectoryContents (tmpDir </> "target" </> "classes")
137+ <$> getDirectoryContents (classFileDir tgtDir)
83− mapM_ (\ clsFile -> copyFile clsFile (takeDirectory out </> takeFileName clsFile))
138+ mapM_ (\ clsFile -> copyFile clsFile (takeDirectory out </> takeFileName clsFile)) classFiles
84− classFiles
139+
85− else do
140+jarFileName :: FilePath -> FilePath -> FilePath
86− (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ ["package"]) ""
87− when (exit /= ExitSuccess) (error ("FAILURE: " ++ mvnCmd ++ " package\n" ++ err ++ mvout))
88− copyFile (tmpDir </> "target" </> (takeBaseName out) <.> "jar") out
141+jarFileName tgtDir out = tgtDir </> "target" </> (takeBaseName out) <.> "jar"
142+
143+copyJar :: FilePath -> FilePath -> IO ()
144+copyJar tgtDir out =
145+ copyFile (jarFileName tgtDir out) out
146+
147+makeJarExecutable :: FilePath -> IO ()
148+makeJarExecutable out = do
89− handle <- openBinaryFile out ReadMode
149+ handle <- openBinaryFile out ReadMode
90− contents <- TIO.hGetContents handle
150+ contents <- TIO.hGetContents handle
91− hClose handle
151+ hClose handle
92− handle <- openBinaryFile out WriteMode
152+ handle <- openBinaryFile out WriteMode
93− TIO.hPutStr handle (T.append (T.pack jarHeader) contents)
153+ TIO.hPutStr handle (T.append (T.pack jarHeader) contents)
94− hFlush handle
154+ hFlush handle
95− hClose handle
155+ hClose handle
96− perms <- getPermissions out
156+ perms <- getPermissions out
97− setPermissions out (setOwnerExecutable True perms)
157+ setPermissions out (setOwnerExecutable True perms)
98− readProcess mvnCmd (args ++ ["clean"]) ""
158+
99− removeFile (tmpDir </> "pom.xml")
159+removePom :: FilePath -> IO ()
160+removePom tgtDir = removeFile (pomFileName tgtDir)
161+
162+cleanUpTmp :: FilePath -> IO ()
163+cleanUpTmp tgtDir = do
164+ invokeMvn tgtDir "clean"
165+ removePom tgtDir
100
166
101-----------------------------------------------------------------------
167-----------------------------------------------------------------------
102-- Jar and Pom infrastructure
168-- Jar and Pom infrastructure
src/IRTS/CodegenLLVM.hs+1
@@ -94,6 +94,7 @@ outputModule tm file Executable m = withTmpFile $ \obj -> do
94 defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir
94 defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir
95 exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]
95 exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]
96 when (exit /= ExitSuccess) $ ierror "FAILURE: Linking"
96 when (exit /= ExitSuccess) $ ierror "FAILURE: Linking"
97+outputModule _ _ MavenProject _ = ierror "FAILURE: unsupported output type"
97
98
98withTmpFile :: (FilePath -> IO a) -> IO a
99withTmpFile :: (FilePath -> IO a) -> IO a
99withTmpFile f = do
100withTmpFile f = do
src/Idris/CaseSplit.hs+24−26
@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Idris.CaseSplit(split, splitOnLine, replaceSplits,
3+module Idris.CaseSplit(split, splitOnLine, replaceSplits,
4 getClause,
4 getClause,
5 mkWith) where
5 mkWith) where
6
6
@@ -30,9 +30,9 @@ import qualified Data.ByteString.UTF8 as UTF8
30
30
31import Debug.Trace
31import Debug.Trace
32
32
33−{-
33+{-
34
34
35−Given a pattern clause and a variable 'n', elaborate the cluse and find the
35+Given a pattern clause and a variable 'n', elaborate the clause and find the
36type of 'n'.
36type of 'n'.
37
37
38Make new pattern clauses by replacing 'n' with all the possibly constructors
38Make new pattern clauses by replacing 'n' with all the possibly constructors
@@ -47,7 +47,7 @@ names over '_', patterns over names, etc.
47-- Given a variable to split, and a term application, return a list of
47-- Given a variable to split, and a term application, return a list of
48-- variable updates
48-- variable updates
49split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
49split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
50−split n t'
50+split n t'
51 = do (tm, ty, pats) <- elabValBind toplevel True t'
51 = do (tm, ty, pats) <- elabValBind toplevel True t'
52 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
52 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
53 ist <- getIState
53 ist <- getIState
@@ -57,7 +57,7 @@ split n t'
57 let ctxt = tt_ctxt ist
57 let ctxt = tt_ctxt ist
58 case lookup n pats of
58 case lookup n pats of
59 Nothing -> fail $ show n ++ " is not a pattern variable"
59 Nothing -> fail $ show n ++ " is not a pattern variable"
60− Just ty ->
60+ Just ty ->
61 do let splits = findPats ist ty
61 do let splits = findPats ist ty
62 iLOG ("New patterns " ++ show splits)
62 iLOG ("New patterns " ++ show splits)
63 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
63 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
@@ -65,7 +65,7 @@ split n t'
65 logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))
65 logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))
66 newPats <- mapM elabNewPat newPats_in
66 newPats <- mapM elabNewPat newPats_in
67 logLvl 3 ("Original:\n" ++ show t)
67 logLvl 3 ("Original:\n" ++ show t)
68− logLvl 3 ("Split:\n" ++
68+ logLvl 3 ("Split:\n" ++
69 (showSep "\n" (map show (mapMaybe id newPats))))
69 (showSep "\n" (map show (mapMaybe id newPats))))
70 logLvl 3 "----"
70 logLvl 3 "----"
71 let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
71 let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
@@ -75,17 +75,17 @@ split n t'
75
75
76data MergeState = MS { namemap :: [(Name, Name)],
76data MergeState = MS { namemap :: [(Name, Name)],
77 updates :: [(Name, PTerm)] }
77 updates :: [(Name, PTerm)] }
78−
78+
79addUpdate n tm = do ms <- get
79addUpdate n tm = do ms <- get
80 put (ms { updates = ((n, stripNS tm) : updates ms) } )
80 put (ms { updates = ((n, stripNS tm) : updates ms) } )
81
81
82−stripNS tm = mapPT dens tm where
82+stripNS tm = mapPT dens tm where
83 dens (PRef fc n) = PRef fc (nsroot n)
83 dens (PRef fc n) = PRef fc (nsroot n)
84 dens t = t
84 dens t = t
85
85
86mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
86mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
87mergeAllPats ctxt t [] = []
87mergeAllPats ctxt t [] = []
88−mergeAllPats ctxt t (p : ps)
88+mergeAllPats ctxt t (p : ps)
89 = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])
89 = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])
90 ps' = mergeAllPats ctxt t ps in
90 ps' = mergeAllPats ctxt t ps in
91 ((p, u) : ps')
91 ((p, u) : ps')
@@ -97,7 +97,7 @@ mergePat ctxt (PPatvar fc n) new
97 = mergePat ctxt (PRef fc n) new
97 = mergePat ctxt (PRef fc n) new
98mergePat ctxt old (PPatvar fc n)
98mergePat ctxt old (PPatvar fc n)
99 = mergePat ctxt old (PRef fc n)
99 = mergePat ctxt old (PRef fc n)
100−mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
100+mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
101 | isDConName n' ctxt = do addUpdate n new;
101 | isDConName n' ctxt = do addUpdate n new;
102 return new
102 return new
103 | otherwise
103 | otherwise
@@ -107,7 +107,7 @@ mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
107 return (PRef fc x)
107 return (PRef fc x)
108 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
108 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
109 return (PRef fc n)
109 return (PRef fc n)
110−mergePat ctxt (PApp _ _ args) (PApp fc f args')
110+mergePat ctxt (PApp _ _ args) (PApp fc f args')
111 = do newArgs <- zipWithM mergeArg args args'
111 = do newArgs <- zipWithM mergeArg args args'
112 return (PApp fc f newArgs)
112 return (PApp fc f newArgs)
113 where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
113 where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
@@ -124,7 +124,7 @@ mergePat ctxt x y = return y
124mergeUserImpl :: PTerm -> PTerm -> PTerm
124mergeUserImpl :: PTerm -> PTerm -> PTerm
125mergeUserImpl x y = x
125mergeUserImpl x y = x
126
126
127−tidy orig@(PRef fc n)
127+tidy orig@(PRef fc n)
128 = do ms <- get
128 = do ms <- get
129 case lookup n (namemap ms) of
129 case lookup n (namemap ms) of
130 Just x -> return (PRef fc x)
130 Just x -> return (PRef fc x)
@@ -181,10 +181,10 @@ splitOnLine :: Int -- ^ line number
181 -> Name -- ^ variable
181 -> Name -- ^ variable
182 -> FilePath -- ^ name of file
182 -> FilePath -- ^ name of file
183 -> Idris [[(Name, PTerm)]]
183 -> Idris [[(Name, PTerm)]]
184−splitOnLine l n fn = do
184+splitOnLine l n fn = do
185-- let (before, later) = splitAt (l-1) (lines inp)
185-- let (before, later) = splitAt (l-1) (lines inp)
186-- i <- getIState
186-- i <- getIState
187− cl <- getInternalApp fn l
187+ cl <- getInternalApp fn l
188 logLvl 3 ("Working with " ++ showImp Nothing True False cl)
188 logLvl 3 ("Working with " ++ showImp Nothing True False cl)
189 tms <- split n cl
189 tms <- split n cl
190-- iputStrLn (showSep "\n" (map show tms))
190-- iputStrLn (showSep "\n" (map show tms))
@@ -210,7 +210,7 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
210 return (x : xs', i')
210 return (x : xs', i')
211 updateRHS i [] = return ("", i)
211 updateRHS i [] = return ("", i)
212
212
213− getUniq nm i
213+ getUniq nm i
214 = do ist <- getIState
214 = do ist <- getIState
215 let n = nameRoot [] nm ++ "_" ++ show i
215 let n = nameRoot [] nm ++ "_" ++ show i
216 case lookupTy (UN n) (tt_ctxt ist) of
216 case lookupTy (UN n) (tt_ctxt ist) of
@@ -218,15 +218,15 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
218 _ -> getUniq nm (i+1)
218 _ -> getUniq nm (i+1)
219
219
220 nameRoot acc nm | all isDigit nm = showSep "_" acc
220 nameRoot acc nm | all isDigit nm = showSep "_" acc
221− nameRoot acc nm =
221+ nameRoot acc nm =
222 case span (/='_') nm of
222 case span (/='_') nm of
223 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
223 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
224 _ -> showSep "_" (acc ++ [nm])
224 _ -> showSep "_" (acc ++ [nm])
225
225
226− -- TMP HACK: If there are Nats, we don't want to show as numerals since
226+ -- TMP HACK: If there are Nats, we don't want to show as numerals since
227 -- this isn't supported in a pattern, so special case here
227 -- this isn't supported in a pattern, so special case here
228 nshow brack (PRef _ (UN "Z")) = "Z"
228 nshow brack (PRef _ (UN "Z")) = "Z"
229− nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
229+ nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
230 if brack then "(S " else "S " ++ nshow True (getTm x) ++
230 if brack then "(S " else "S " ++ nshow True (getTm x) ++
231 if brack then ")" else ""
231 if brack then ")" else ""
232 nshow _ t = show t
232 nshow _ t = show t
@@ -235,14 +235,14 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
235 expandBraces ('{' : xs)
235 expandBraces ('{' : xs)
236 = let (brace, (_:rest)) = span (/= '}') xs in
236 = let (brace, (_:rest)) = span (/= '}') xs in
237 if (not ('=' `elem` brace))
237 if (not ('=' `elem` brace))
238− then ('{' : brace ++ " = " ++ brace ++ "}") ++
238+ then ('{' : brace ++ " = " ++ brace ++ "}") ++
239 expandBraces rest
239 expandBraces rest
240 else ('{' : brace ++ "}") ++ expandBraces rest
240 else ('{' : brace ++ "}") ++ expandBraces rest
241 expandBraces (x : xs) = x : expandBraces xs
241 expandBraces (x : xs) = x : expandBraces xs
242 expandBraces [] = []
242 expandBraces [] = []
243
243
244 updatePat start n tm [] = []
244 updatePat start n tm [] = []
245− updatePat start n tm ('{':rest) =
245+ updatePat start n tm ('{':rest) =
246 let (space, rest') = span isSpace rest in
246 let (space, rest') = span isSpace rest in
247 '{' : space ++ updatePat False n tm rest'
247 '{' : space ++ updatePat False n tm rest'
248 updatePat True n tm xs@(c:rest) | length xs > length n
248 updatePat True n tm xs@(c:rest) | length xs > length n
@@ -261,7 +261,7 @@ getClause :: Int -> -- ^ Line type is declared on
261 Idris String
261 Idris String
262getClause l fn fp = do ty <- getInternalApp fp l
262getClause l fn fp = do ty <- getInternalApp fp l
263 let ap = mkApp ty [1..]
263 let ap = mkApp ty [1..]
264− return (show fn ++ " " ++ ap ++
264+ return (show fn ++ " " ++ ap ++
265 "= ?" ++ show fn ++ "_rhs")
265 "= ?" ++ show fn ++ "_rhs")
266 where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
266 where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
267 = "x" ++ show n ++ " " ++ mkApp sc ns
267 = "x" ++ show n ++ " " ++ mkApp sc ns
@@ -275,17 +275,15 @@ getClause l fn fp = do ty <- getInternalApp fp l
275
275
276mkWith :: String -> Name -> String
276mkWith :: String -> Name -> String
277mkWith str n = let ind = getIndent str
277mkWith str n = let ind = getIndent str
278− str' = replicate ind ' ' ++
278+ str' = replicate ind ' ' ++
279 replaceRHS str "with (_)"
279 replaceRHS str "with (_)"
280− newpat = replicate (ind + 2) ' ' ++
280+ newpat = replicate (ind + 2) ' ' ++
281 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
281 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
282 str' ++ "\n" ++ newpat
282 str' ++ "\n" ++ newpat
283−
283+
284 where getIndent s = length (takeWhile isSpace s)
284 where getIndent s = length (takeWhile isSpace s)
285
285
286 replaceRHS [] str = str
286 replaceRHS [] str = str
287 replaceRHS ('?':'=': rest) str = str
287 replaceRHS ('?':'=': rest) str = str
288 replaceRHS ('=': rest) str = str
288 replaceRHS ('=': rest) str = str
289 replaceRHS (x : rest) str = x : replaceRHS rest str
289 replaceRHS (x : rest) str = x : replaceRHS rest str
290−
291−
src/Idris/REPL.hs+6−2
@@ -27,6 +27,7 @@ import Idris.CaseSplit
27import Paths_idris
27import Paths_idris
28import Util.System
28import Util.System
29import Util.DynamicLinker
29import Util.DynamicLinker
30+import Util.Net (listenOnLocalhost)
30
31
31import Core.Evaluate
32import Core.Evaluate
32import Core.Execute (execute)
33import Core.Execute (execute)
@@ -111,7 +112,7 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
111 where serverLoop :: IO ()
112 where serverLoop :: IO ()
112 -- TODO: option for port number
113 -- TODO: option for port number
113 serverLoop = withSocketsDo $
114 serverLoop = withSocketsDo $
114− do sock <- listenOn $ PortNumber 4294
115+ do sock <- listenOnLocalhost $ PortNumber 4294
115 i <- readMVar stvar
116 i <- readMVar stvar
116 loop fn i sock
117 loop fn i sock
117
118
@@ -121,7 +122,9 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
121
122
122 loop fn ist sock
123 loop fn ist sock
123 = do (h,host,_) <- accept sock
124 = do (h,host,_) <- accept sock
125+ -- just use the local part of the hostname
126+ -- for the "localhost.localdomain" case
124− if (host == "localhost" ||
127+ if ((takeWhile (/= '.') host) == "localhost" ||
125 host == "127.0.0.1")
128 host == "127.0.0.1")
126 then do
129 then do
127 cmd <- hGetLine h
130 cmd <- hGetLine h
@@ -872,6 +875,7 @@ parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
872parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)
875parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)
873parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
876parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
874parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
877parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
878+parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)
875parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
879parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
876parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
880parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
877parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
881parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
src/Main.hs+1
@@ -98,6 +98,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++
98 "\t--log [level] Type debugging log level\n" ++
98 "\t--log [level] Type debugging log level\n" ++
99 "\t-S Do no further compilation of code generator output\n" ++
99 "\t-S Do no further compilation of code generator output\n" ++
100 "\t-c Compile to object files rather than an executable\n" ++
100 "\t-c Compile to object files rather than an executable\n" ++
101+ "\t--mvn Create a maven project (for Java codegen)\n" ++
101 "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++
102 "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++
102 "\t defaulting to Main.main if none provided, and exit.\n" ++
103 "\t defaulting to Main.main if none provided, and exit.\n" ++
103 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++
104 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++
src/Util/Net.hsnew file+22
@@ -0,0 +1,22 @@
1+module Util.Net (listenOnLocalhost) where
2+
3+import Network
4+import Network.Socket hiding (sClose, PortNumber)
5+import Network.BSD (getProtocolNumber)
6+import Control.Exception (bracketOnError)
7+
8+-- Copied from upstream impl of listenOn
9+-- bound to localhost interface instead of iNADDR_ANY
10+listenOnLocalhost (PortNumber port) = do
11+ proto <- getProtocolNumber "tcp"
12+ localhost <- inet_addr "127.0.0.1"
13+ bracketOnError
14+ (socket AF_INET Stream proto)
15+ (sClose)
16+ (\sock -> do
17+ setSocketOption sock ReuseAddr 1
18+ bindSocket sock (SockAddrInet port localhost)
19+ listen sock maxListenQueue
20+ return sock
21+ )
22+