5b10b97 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit5b10b97c216126d75957e2a367a11d87da8c9898 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 30 Oct 2013, 08:16 (13 years ago) parent4a63609 6bcb9c7

9 files changed+174−80

compare with master

unifiedsplit

idris.cabal+1 src/IRTS/CodegenC.hs+1 src/IRTS/CodegenCommon.hs+1−1 src/IRTS/CodegenJava.hs+117−51 src/IRTS/CodegenLLVM.hs+1 src/Idris/CaseSplit.hs+24−26 src/Idris/REPL.hs+6−2 src/Main.hs+1 src/Util/Net.hs+22

idris.cabal+1

@@ -357,6 +357,7 @@ Executable idris

357357 , Util.Pretty

358358 , Util.System

359359 , Util.DynamicLinker

360+ , Util.Net

360361

361362 , Pkg.Package

362363 , Pkg.PParser

src/IRTS/CodegenC.hs+1

@@ -37,6 +37,7 @@ codegenC defs out exec incs objs libs flags dbg

3737 let cout = headers incs ++ debug dbg ++ h ++ cc ++

3838 (if (exec == Executable) then mprog else "")

3939 case exec of

40+ MavenProject -> putStrLn ("FAILURE: output type not supported")

4041 Raw -> writeFile out cout

4142 _ -> do

4243 (tmpn, tmph) <- tempfile

src/IRTS/CodegenCommon.hs+1−1

@@ -7,7 +7,7 @@ import Control.Exception

77import System.Environment

99data 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)

1111

1212environment :: String -> IO (Maybe String)

1313environment x = Control.Exception.catch (do e <- getEnv x

src/IRTS/CodegenJava.hs+117−51

@@ -37,66 +37,132 @@ import System.Process

3737

3838-----------------------------------------------------------------------

3939-- Main function

40−

4140codegenJava :: [(Name, SExp)] -> -- initialization of globals

42− [(Name, SDecl)] ->

41+ [(Name, SDecl)] -> -- decls

4342 FilePath -> -- output file name

4443 [String] -> -- headers

4544 [String] -> -- libs

4645 OutputType ->

4746 IO ()

48−codegenJava globalInit defs out hdrs libs exec = do

49− withTempdir (takeBaseName out) $ \ tmpDir -> do

50− let srcdir = tmpDir </> "src" </> "main" </> "java"

51− createDirectoryIfMissing True srcdir

52− let (Ident clsName) = either error id (mkClassName out)

53− let outjava = srcdir </> clsName <.> "java"

54− let jout = either error

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

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

80+ let srcDir = (tgtDir </> "src" </> "main" </> "java")

81+ createDirectoryIfMissing True srcDir

82+ return srcDir

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

95+ let code = either error

5596 (prettyPrint)-- flatIndent . prettyPrint)

5697 (evalStateT (mkCompilationUnit globalInit defs hdrs out) mkCodeGenEnv)

57− writeFile outjava jout

58− if (exec == Raw)

59− then copyFile outjava (takeDirectory out </> clsName <.> "java")

60− else do

61− execPom <- getExecutablePom

62− execPomTemplate <- TIO.readFile execPom

63− let execPom = T.replace (T.pack "$MAIN-CLASS$")

64− (T.pack clsName)

65− (T.replace (T.pack "$ARTIFACT-NAME$")

66− (T.pack $ takeBaseName out)

67− (T.replace (T.pack "$DEPENDENCIES$")

68− (mkPomDependencies libs)

69− execPomTemplate

70− )

71− )

72− TIO.writeFile (tmpDir </> "pom.xml") execPom

73− mvnCmd <- getMvn

74− let args = ["-f", (tmpDir </> "pom.xml")]

75− (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ ["compile"]) ""

76− when (exit /= ExitSuccess) $ error ("FAILURE: " ++ mvnCmd ++ " compile\n" ++ err ++ mvout)

77− if (exec == Object)

78− then do

79− classFiles <-

80− map (\ clsFile -> tmpDir </> "target" </> "classes" </> clsFile)

98+ writeFile (javaFileName srcDir out) code

99+

100+pomFileName :: FilePath -> FilePath

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

108+ execPom <- getExecutablePom

109+ execPomTemplate <- TIO.readFile execPom

110+ let (Ident clsName) = either error id (mkClassName out)

111+ let execPom = T.replace (T.pack "$MAIN-CLASS$")

112+ (T.pack clsName)

113+ (T.replace (T.pack "$ARTIFACT-NAME$")

114+ (T.pack $ takeBaseName out)

115+ (T.replace (T.pack "$DEPENDENCIES$")

116+ (mkPomDependencies libs)

117+ execPomTemplate

118+ )

119+ )

120+ TIO.writeFile (pomFileName tgtDir) execPom

121+

122+invokeMvn :: FilePath -> String -> IO ()

123+invokeMvn tgtDir command = do

124+ mvnCmd <- getMvn

125+ let args = ["-f", pomFileName tgtDir]

126+ (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ [command]) ""

127+ when (exit /= ExitSuccess) $

128+ error ("FAILURE: " ++ mvnCmd ++ " " ++ command ++ "\n" ++ err ++ mvout)

129+

130+classFileDir :: FilePath -> FilePath

131+classFileDir tgtDir = tgtDir </> "target" </> "classes"

132+

133+copyClassFiles :: FilePath -> FilePath -> IO ()

134+copyClassFiles tgtDir out = do

135+ classFiles <- map (\ clsFile -> classFileDir tgtDir </> clsFile)

81136 . filter ((".class" ==) . takeExtension)

82− <$> getDirectoryContents (tmpDir </> "target" </> "classes")

83− mapM_ (\ clsFile -> copyFile clsFile (takeDirectory out </> takeFileName clsFile))

84− classFiles

85− else do

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

89− handle <- openBinaryFile out ReadMode

90− contents <- TIO.hGetContents handle

91− hClose handle

92− handle <- openBinaryFile out WriteMode

93− TIO.hPutStr handle (T.append (T.pack jarHeader) contents)

94− hFlush handle

95− hClose handle

96− perms <- getPermissions out

97− setPermissions out (setOwnerExecutable True perms)

98− readProcess mvnCmd (args ++ ["clean"]) ""

99− removeFile (tmpDir </> "pom.xml")

137+ <$> getDirectoryContents (classFileDir tgtDir)

138+ mapM_ (\ clsFile -> copyFile clsFile (takeDirectory out </> takeFileName clsFile)) classFiles

139+

140+jarFileName :: FilePath -> FilePath -> FilePath

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

149+ handle <- openBinaryFile out ReadMode

150+ contents <- TIO.hGetContents handle

151+ hClose handle

152+ handle <- openBinaryFile out WriteMode

153+ TIO.hPutStr handle (T.append (T.pack jarHeader) contents)

154+ hFlush handle

155+ hClose handle

156+ perms <- getPermissions out

157+ setPermissions out (setOwnerExecutable True perms)

158+

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

100166

101167-----------------------------------------------------------------------

102168-- Jar and Pom infrastructure

src/IRTS/CodegenLLVM.hs+1

@@ -94,6 +94,7 @@ outputModule tm file Executable m = withTmpFile $ \obj -> do

9494 defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir

9595 exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]

9696 when (exit /= ExitSuccess) $ ierror "FAILURE: Linking"

97+outputModule _ _ MavenProject _ = ierror "FAILURE: unsupported output type"

9798

9899withTmpFile :: (FilePath -> IO a) -> IO a

99100withTmpFile f = do

src/Idris/CaseSplit.hs+24−26

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split, splitOnLine, replaceSplits,

3+module Idris.CaseSplit(split, splitOnLine, replaceSplits,

44 getClause,

55 mkWith) where

@@ -30,9 +30,9 @@ import qualified Data.ByteString.UTF8 as UTF8

3030

3131import Debug.Trace

3232

33−{-

33+{-

3434

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

3636type of 'n'.

3737

3838Make new pattern clauses by replacing 'n' with all the possibly constructors

@@ -47,7 +47,7 @@ names over '_', patterns over names, etc.

4747-- Given a variable to split, and a term application, return a list of

4848-- variable updates

4949split :: Name -> PTerm -> Idris [[(Name, PTerm)]]

50−split n t'

50+split n t'

5151 = do (tm, ty, pats) <- elabValBind toplevel True t'

5252 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

5353 ist <- getIState

@@ -57,7 +57,7 @@ split n t'

5757 let ctxt = tt_ctxt ist

5858 case lookup n pats of

5959 Nothing -> fail $ show n ++ " is not a pattern variable"

60− Just ty ->

60+ Just ty ->

6161 do let splits = findPats ist ty

6262 iLOG ("New patterns " ++ show splits)

6363 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

@@ -65,7 +65,7 @@ split n t'

6565 logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))

6666 newPats <- mapM elabNewPat newPats_in

6767 logLvl 3 ("Original:\n" ++ show t)

68− logLvl 3 ("Split:\n" ++

68+ logLvl 3 ("Split:\n" ++

6969 (showSep "\n" (map show (mapMaybe id newPats))))

7070 logLvl 3 "----"

7171 let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)

@@ -75,17 +75,17 @@ split n t'

7575

7676data MergeState = MS { namemap :: [(Name, Name)],

7777 updates :: [(Name, PTerm)] }

78−

78+

7979addUpdate n tm = do ms <- get

8080 put (ms { updates = ((n, stripNS tm) : updates ms) } )

8181

82−stripNS tm = mapPT dens tm where

82+stripNS tm = mapPT dens tm where

8383 dens (PRef fc n) = PRef fc (nsroot n)

8484 dens t = t

8585

8686mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

8787mergeAllPats ctxt t [] = []

88−mergeAllPats ctxt t (p : ps)

88+mergeAllPats ctxt t (p : ps)

8989 = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])

9090 ps' = mergeAllPats ctxt t ps in

9191 ((p, u) : ps')

@@ -97,7 +97,7 @@ mergePat ctxt (PPatvar fc n) new

9797 = mergePat ctxt (PRef fc n) new

9898mergePat ctxt old (PPatvar fc n)

9999 = 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')

101101 | isDConName n' ctxt = do addUpdate n new;

102102 return new

103103 | otherwise

@@ -107,7 +107,7 @@ mergePat ctxt orig@(PRef fc n) new@(PRef _ n')

107107 return (PRef fc x)

108108 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })

109109 return (PRef fc n)

110−mergePat ctxt (PApp _ _ args) (PApp fc f args')

110+mergePat ctxt (PApp _ _ args) (PApp fc f args')

111111 = do newArgs <- zipWithM mergeArg args args'

112112 return (PApp fc f newArgs)

113113 where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)

@@ -124,7 +124,7 @@ mergePat ctxt x y = return y

124124mergeUserImpl :: PTerm -> PTerm -> PTerm

125125mergeUserImpl x y = x

126126

127−tidy orig@(PRef fc n)

127+tidy orig@(PRef fc n)

128128 = do ms <- get

129129 case lookup n (namemap ms) of

130130 Just x -> return (PRef fc x)

@@ -181,10 +181,10 @@ splitOnLine :: Int -- ^ line number

181181 -> Name -- ^ variable

182182 -> FilePath -- ^ name of file

183183 -> Idris [[(Name, PTerm)]]

184−splitOnLine l n fn = do

184+splitOnLine l n fn = do

185185-- let (before, later) = splitAt (l-1) (lines inp)

186186-- i <- getIState

187− cl <- getInternalApp fn l

187+ cl <- getInternalApp fn l

188188 logLvl 3 ("Working with " ++ showImp Nothing True False cl)

189189 tms <- split n cl

190190-- iputStrLn (showSep "\n" (map show tms))

@@ -210,7 +210,7 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

210210 return (x : xs', i')

211211 updateRHS i [] = return ("", i)

212212

213− getUniq nm i

213+ getUniq nm i

214214 = do ist <- getIState

215215 let n = nameRoot [] nm ++ "_" ++ show i

216216 case lookupTy (UN n) (tt_ctxt ist) of

@@ -218,15 +218,15 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

218218 _ -> getUniq nm (i+1)

219219

220220 nameRoot acc nm | all isDigit nm = showSep "_" acc

221− nameRoot acc nm =

221+ nameRoot acc nm =

222222 case span (/='_') nm of

223223 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

224224 _ -> showSep "_" (acc ++ [nm])

225225

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

227227 -- this isn't supported in a pattern, so special case here

228228 nshow brack (PRef _ (UN "Z")) = "Z"

229− nshow brack (PApp _ (PRef _ (UN "S")) [x]) =

229+ nshow brack (PApp _ (PRef _ (UN "S")) [x]) =

230230 if brack then "(S " else "S " ++ nshow True (getTm x) ++

231231 if brack then ")" else ""

232232 nshow _ t = show t

@@ -235,14 +235,14 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

235235 expandBraces ('{' : xs)

236236 = let (brace, (_:rest)) = span (/= '}') xs in

237237 if (not ('=' `elem` brace))

238− then ('{' : brace ++ " = " ++ brace ++ "}") ++

238+ then ('{' : brace ++ " = " ++ brace ++ "}") ++

239239 expandBraces rest

240240 else ('{' : brace ++ "}") ++ expandBraces rest

241241 expandBraces (x : xs) = x : expandBraces xs

242242 expandBraces [] = []

243243

244244 updatePat start n tm [] = []

245− updatePat start n tm ('{':rest) =

245+ updatePat start n tm ('{':rest) =

246246 let (space, rest') = span isSpace rest in

247247 '{' : space ++ updatePat False n tm rest'

248248 updatePat True n tm xs@(c:rest) | length xs > length n

@@ -261,7 +261,7 @@ getClause :: Int -> -- ^ Line type is declared on

261261 Idris String

262262getClause l fn fp = do ty <- getInternalApp fp l

263263 let ap = mkApp ty [1..]

264− return (show fn ++ " " ++ ap ++

264+ return (show fn ++ " " ++ ap ++

265265 "= ?" ++ show fn ++ "_rhs")

266266 where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)

267267 = "x" ++ show n ++ " " ++ mkApp sc ns

@@ -275,17 +275,15 @@ getClause l fn fp = do ty <- getInternalApp fp l

275275

276276mkWith :: String -> Name -> String

277277mkWith str n = let ind = getIndent str

278− str' = replicate ind ' ' ++

278+ str' = replicate ind ' ' ++

279279 replaceRHS str "with (_)"

280− newpat = replicate (ind + 2) ' ' ++

280+ newpat = replicate (ind + 2) ' ' ++

281281 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in

282282 str' ++ "\n" ++ newpat

283−

283+

284284 where getIndent s = length (takeWhile isSpace s)

285285

286286 replaceRHS [] str = str

287287 replaceRHS ('?':'=': rest) str = str

288288 replaceRHS ('=': rest) str = str

289289 replaceRHS (x : rest) str = x : replaceRHS rest str

290−

291−

src/Idris/REPL.hs+6−2

@@ -27,6 +27,7 @@ import Idris.CaseSplit

2727import Paths_idris

2828import Util.System

2929import Util.DynamicLinker

30+import Util.Net (listenOnLocalhost)

3031

3132import Core.Evaluate

3233import Core.Execute (execute)

@@ -111,7 +112,7 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

111112 where serverLoop :: IO ()

112113 -- TODO: option for port number

113114 serverLoop = withSocketsDo $

114− do sock <- listenOn $ PortNumber 4294

115+ do sock <- listenOnLocalhost $ PortNumber 4294

115116 i <- readMVar stvar

116117 loop fn i sock

117118

@@ -121,7 +122,9 @@ startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

121122

122123 loop fn ist sock

123124 = do (h,host,_) <- accept sock

124− if (host == "localhost" ||

125+ -- just use the local part of the hostname

126+ -- for the "localhost.localdomain" case

127+ if ((takeWhile (/= '.') host) == "localhost" ||

125128 host == "127.0.0.1")

126129 then do

127130 cmd <- hGetLine h

@@ -872,6 +875,7 @@ parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

872875parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

873876parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

874877parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

878+parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

875879parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

876880parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

877881parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

src/Main.hs+1

@@ -98,6 +98,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

9898 "\t--log [level] Type debugging log level\n" ++

9999 "\t-S Do no further compilation of code generator output\n" ++

100100 "\t-c Compile to object files rather than an executable\n" ++

101+ "\t--mvn Create a maven project (for Java codegen)\n" ++

101102 "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++

102103 "\t defaulting to Main.main if none provided, and exit.\n" ++

103104 "\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

3+import Network

4+import Network.Socket hiding (sClose, PortNumber)

5+import Network.BSD (getProtocolNumber)

6+import Control.Exception (bracketOnError)

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+