9875894 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merged upstream changes

9875894David Christiansen14 years ago

CHANGELOG+14

compare with master

unifiedsplit

@@ -1,3 +1,17 @@

1+New in 0.9.8:

2+-------------

4+User visible changes:

6+* Renamed EFF to EFFECT in Effect package

7+* Experimental Java backend

8+* Tab completion in REPL

10+Internal changes:

11+

12+* Improved name disambiguation

13+* Various unification and totality checking bug fixes

14+

1New in 0.9.7:

15New in 0.9.7:

2-------------

16-------------

Makefile+6−6

@@ -1,17 +1,17 @@

1include config.mk

3install: .PHONY

4− $(CABAL) install

4+ $(CABAL) install $(CABALFLAGS)

6pinstall: .PHONY

7− $(CABAL) configure --enable-executable-profiling

7+ $(CABAL) configure --enable-executable-profiling $(CABALFLAGS)

8− $(CABAL) install --enable-executable-profiling

8+ $(CABAL) install --enable-executable-profiling $(CABALFLAGS)

10build: .PHONY

11− $(CABAL) build

11+ $(CABAL) build $(CABALFLAGS)

13configure: .PHONY

14− $(CABAL) configure

14+ $(CABAL) configure $(CABALFLAGS)

16test : .PHONY

17 make -C test

@@ -19,7 +19,7 @@ test : .PHONY

19relib: .PHONY

20 make -C lib IDRIS=../dist/build/idris/idris clean

21 make -C effects IDRIS=../dist/build/idris/idris clean

22− $(CABAL) install

22+ $(CABAL) install $(CABALFLAGS)

24linecount : .PHONY

25 wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

Setup.hs+69−6

@@ -1,24 +1,32 @@

1{-# LANGUAGE CPP #-}

2+import Control.Monad

3+import Data.IORef

2import Distribution.Simple

5import Distribution.Simple

3import Distribution.Simple.InstallDirs as I

6import Distribution.Simple.InstallDirs as I

4import Distribution.Simple.LocalBuildInfo as L

7import Distribution.Simple.LocalBuildInfo as L

5import qualified Distribution.Simple.Setup as S

8import qualified Distribution.Simple.Setup as S

6import qualified Distribution.Simple.Program as P

9import qualified Distribution.Simple.Program as P

7import Distribution.PackageDescription

10import Distribution.PackageDescription

11+import Distribution.Text

9import System.Exit

13import System.Exit

10import System.FilePath ((</>), splitDirectories)

14import System.FilePath ((</>), splitDirectories)

15+import System.Directory

11import qualified System.FilePath.Posix as Px

16import qualified System.FilePath.Posix as Px

12import System.Process

17import System.Process

18+import qualified Data.Text as T

19+import qualified Data.Text.IO as TIO

14-- After Idris is built, we need to check and install the prelude and other libs

21-- After Idris is built, we need to check and install the prelude and other libs

16make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"

23make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"

24+mvn verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "mvn"

18#ifdef mingw32_HOST_OS

26#ifdef mingw32_HOST_OS

19-- make on mingw32 exepects unix style separators

27-- make on mingw32 exepects unix style separators

20(<//>) = (Px.</>)

28(<//>) = (Px.</>)

21−idrisCmd local = Px.joinPath $ splitDirectories $

29+idrisCmd local = Px.joinPath $ splitDirectories $

22 ".." <//> buildDir local <//> "idris" <//> "idris"

30 ".." <//> buildDir local <//> "idris" <//> "idris"

23#else

31#else

24idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

32idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

@@ -28,6 +36,14 @@ cleanStdLib verbosity

28 = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ]

36 = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ]

29 make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ]

37 make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ]

39+cleanJavaLib verbosity

40+ = do dirty <- doesDirectoryExist ("java" </> "target")

41+ when dirty $ mvn verbosity [ "-f", "java/pom.xml", "clean" ]

42+ pomExists <- doesFileExist ("java" </> "pom.xml")

43+ when pomExists $ removeFile ("java" </> "pom.xml")

44+ execPomExists <- doesFileExist ("java" </> "executable_pom.xml")

45+ when pomExists $ removeFile ("java" </> "executable_pom.xml")

46+

31installStdLib pkg local verbosity copy

47installStdLib pkg local verbosity copy

32 = do let dirs = L.absoluteInstallDirs pkg local copy

48 = do let dirs = L.absoluteInstallDirs pkg local copy

33 let idir = datadir dirs

49 let idir = datadir dirs

@@ -51,6 +67,20 @@ installStdLib pkg local verbosity copy

51 , "IDRIS=" ++ icmd

67 , "IDRIS=" ++ icmd

52 ]

68 ]

70+installJavaLib pkg local verbosity copy version = do

71+ let rtsFile = "idris-" ++ display version ++ ".jar"

72+ putStrLn $ "Installing java libraries"

73+ mvn verbosity [ "install:install-file"

74+ , "-Dfile=" ++ ("java" </> "target" </> rtsFile)

75+ , "-DgroupId=org.idris-lang"

76+ , "-DartifactId=idris"

77+ , "-Dversion=" ++ display version

78+ , "-Dpackaging=jar"

79+ , "-DgeneratePom=True"

80+ ]

81+ let dir = datadir $ L.absoluteInstallDirs pkg local copy

82+ copyFile ("java" </> "executable_pom.xml") (dir </> "executable_pom.xml")

83+

54-- This is a hack. I don't know how to tell cabal that a data file needs

84-- This is a hack. I don't know how to tell cabal that a data file needs

55-- installing but shouldn't be in the distribution. And it won't make the

85-- installing but shouldn't be in the distribution. And it won't make the

56-- distribution if it's not there, so instead I just delete

86-- distribution if it's not there, so instead I just delete

@@ -79,19 +109,52 @@ checkStdLib local verbosity

79 , "IDRIS=" ++ icmd

109 , "IDRIS=" ++ icmd

80 ]

110 ]

111

112+checkJavaLib verbosity = mvn verbosity [ "-f", "java" </> "pom.xml", "package" ]

113+

114+javaFlag flags =

115+ case lookup (FlagName "java") (S.configConfigurationsFlags flags) of

116+ Just True -> True

117+ Just False -> False

118+ Nothing -> False

119+

120+preparePoms version

121+ = do pomTemplate <- TIO.readFile ("java" </> "pom_template.xml")

122+ TIO.writeFile ("java" </> "pom.xml") (insertVersion pomTemplate)

123+ execPomTemplate <- TIO.readFile ("java" </> "executable_pom_template.xml")

124+ TIO.writeFile ("java" </> "executable_pom.xml") (insertVersion execPomTemplate)

125+ where

126+ insertVersion template =

127+ T.replace (T.pack "$RTS-VERSION$") (T.pack $ display version) template

128+

82-- Install libraries during both copy and install

129-- Install libraries during both copy and install

83-- See http://hackage.haskell.org/trac/hackage/ticket/718

130-- See http://hackage.haskell.org/trac/hackage/ticket/718

131+main = do

84−main = defaultMainWithHooks $ simpleUserHooks

132+ defaultMainWithHooks $ simpleUserHooks

85 { postCopy = \ _ flags pkg lbi -> do

133 { postCopy = \ _ flags pkg lbi -> do

86− installStdLib pkg lbi (S.fromFlag $ S.copyVerbosity flags)

134+ let verb = S.fromFlag $ S.copyVerbosity flags

135+ installStdLib pkg lbi verb

87 (S.fromFlag $ S.copyDest flags)

136 (S.fromFlag $ S.copyDest flags)

88 , postInst = \ _ flags pkg lbi -> do

137 , postInst = \ _ flags pkg lbi -> do

89− installStdLib pkg lbi (S.fromFlag $ S.installVerbosity flags)

138+ let verb = (S.fromFlag $ S.installVerbosity flags)

139+ installStdLib pkg lbi verb

90 NoCopyDest

140 NoCopyDest

141+ when (javaFlag $ configFlags lbi)

142+ (installJavaLib pkg

143+ lbi

144+ verb

145+ NoCopyDest

146+ (pkgVersion . package $ localPkgDescr lbi)

147+ )

91 , postConf = \ _ flags _ lbi -> do

148 , postConf = \ _ flags _ lbi -> do

92 removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags)

149 removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags)

150+ when (javaFlag $ configFlags lbi)

151+ (preparePoms . pkgVersion . package $ localPkgDescr lbi)

93 , postClean = \ _ flags _ _ -> do

152 , postClean = \ _ flags _ _ -> do

94− cleanStdLib (S.fromFlag $ S.cleanVerbosity flags)

153+ let verb = S.fromFlag $ S.cleanVerbosity flags

154+ cleanStdLib verb

155+ cleanJavaLib verb

95 , postBuild = \ _ flags _ lbi -> do

156 , postBuild = \ _ flags _ lbi -> do

96− checkStdLib lbi (S.fromFlag $ S.buildVerbosity flags)

157+ let verb = S.fromFlag $ S.buildVerbosity flags

158+ checkStdLib lbi verb

159+ when (javaFlag $ configFlags lbi) (checkJavaLib verb)

97 }

160 }

config.mk+3

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

1GMP_INCLUDE_DIR :=

2CC :=gcc

3CABAL :=cabal

4+CABALFLAGS :=

5+## Enable Java RTS:

6+#CABALFLAGS :=-f Java

contribs/lib/._simpleparser.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._Makefiledeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlexpr.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3.idrdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3api.cdeleted

Binary file not shown.

contribs/lib/SQLite3/._sqlite3api.hdeleted

Binary file not shown.

contribs/lib/SQLite3/._testunit.idrdeleted

Binary file not shown.

effects/Effect/Exception.idr+1−1

@@ -17,7 +17,7 @@ instance Show a => Handler (Exception a) IO where

17instance Handler (Exception a) (IOExcept a) where

18 handle _ (Raise e) k = ioM (return (Left e))

20−EXCEPTION : Type -> EFF

20+EXCEPTION : Type -> EFFECT

21EXCEPTION t = MkEff () (Exception t)

23raise : a -> Eff m [EXCEPTION a] b

effects/Effect/File.idr+1−1

@@ -40,7 +40,7 @@ instance Handler FileIO (IOExcept String) where

40 handle (FH h) EOF k = do e <- ioe_lift (feof h)

41 k (FH h) e

43−FILE_IO : Type -> EFF

43+FILE_IO : Type -> EFFECT

44FILE_IO t = MkEff t FileIO

46open : Handler FileIO e =>

effects/Effect/Random.idr+1−1

@@ -11,7 +11,7 @@ using (m : Type -> Type)

11 = let seed' = 1664525 * seed + 1013904223 in

12 k seed' seed'

14−RND : EFF

14+RND : EFFECT

15RND = MkEff Int Random

17rndInt : Int -> Int -> Eff m [RND] Int

effects/Effect/Select.idr+1−1

@@ -15,7 +15,7 @@ instance Handler Selection Maybe where

15instance Handler Selection List where

16 handle r (Select xs) k = concatMap (k r) xs

18−SELECT : EFF

18+SELECT : EFFECT

19SELECT = MkEff () Selection

21select : List a -> Eff m [SELECT] a

effects/Effect/State.idr+6−1

@@ -13,7 +13,7 @@ using (m : Type -> Type)

13 handle st Get k = k st st

14 handle st (Put n) k = k n ()

16−STATE : Type -> EFF

16+STATE : Type -> EFFECT

17STATE t = MkEff t State

19get : Eff m [STATE x] x

@@ -29,3 +29,8 @@ update : (x -> x) -> Eff m [STATE x] ()

29update f = do val <- get

30 put (f val)

32+updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()

33+updateM f = do val <- get

34+ putM (f val)

35+

36+

effects/Effect/StdIO.idr+1−1

@@ -38,7 +38,7 @@ instance Handler StdIO IOStream where

39--- The Effect and associated functions

41−STDIO : EFF

41+STDIO : EFFECT

42STDIO = MkEff () StdIO

44putStr : Handler StdIO e => String -> Eff e [STDIO] ()

effects/Effects.idr+10−10

@@ -10,8 +10,8 @@ import Control.Catchable

10Effect : Type

11Effect = Type -> Type -> Type -> Type

13−data EFF : Type where

13+data EFFECT : Type where

14− MkEff : Type -> Effect -> EFF

14+ MkEff : Type -> Effect -> EFFECT

16class Handler (e : Effect) (m : Type -> Type) where

17 handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a

@@ -28,12 +28,12 @@ using (xs : List a, ys : List a)

28 subListId {xs = Nil} = SubNil

29 subListId {xs = x :: xs} = Keep subListId

31−data Env : (m : Type -> Type) -> List EFF -> Type where

31+data Env : (m : Type -> Type) -> List EFFECT -> Type where

32 Nil : Env m Nil

33 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

35data EffElem : (Type -> Type -> Type -> Type) -> Type ->

36− List EFF -> Type where

36+ List EFFECT -> Type where

37 Here : EffElem x a (MkEff a x :: xs)

38 There : EffElem x a xs -> EffElem x a (y :: xs)

@@ -73,8 +73,8 @@ findSubList (S n)

73 ((Try (Refine "Keep" `Seq` Solve)

74 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))

76−updateResTy : (xs : List EFF) -> EffElem e a xs -> e a b t ->

76+updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

77− List EFF

77+ List EFFECT

78updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs

79updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

@@ -83,7 +83,7 @@ infix 5 :::, :-, :=

83data LRes : lbl -> Type -> Type where

84 (:=) : (x : lbl) -> res -> LRes x res

86−(:::) : lbl -> EFF -> EFF

86+(:::) : lbl -> EFFECT -> EFFECT

87(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff

89private

@@ -97,7 +97,7 @@ relabel {x = MkEff a eff} l [v] = [l := v]

97-- the language of Effects

99data EffM : (m : Type -> Type) ->

100− List EFF -> List EFF -> Type -> Type where

100+ List EFFECT -> List EFFECT -> Type -> Type where

101 value : a -> EffM m xs xs a

102 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

103 effect : {a, b: _} -> {e : Effect} ->

@@ -114,7 +114,7 @@ data EffM : (m : Type -> Type) ->

114 EffM m xs xs' a

115 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

116

117−-- Eff : List (EFF m) -> Type -> Type

117+-- Eff : List (EFFECT m) -> Type -> Type

118

119implicit

120lift' : {default tactics { reflect findSubList 10; solve; }

@@ -192,7 +192,7 @@ runPure env prog = eff env prog (\env, r => r)

192runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

193runWith inj env prog = eff env prog (\env, r => inj r)

194

195−Eff : (Type -> Type) -> List EFF -> Type -> Type

195+Eff : (Type -> Type) -> List EFFECT -> Type -> Type

196Eff m xs t = EffM m xs xs t

197

198-- some higher order things

git-credential-osxkeychaindeleted

Binary file not shown.

idris.cabal+9−1

@@ -42,8 +42,11 @@ Description: Idris is a general purpose language with full dependent types.

42 * Hugs style interactive environment

44Cabal-Version: >= 1.6

45+

46+

45Build-type: Custom

47Build-type: Custom

49+

47Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

50Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

48 rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h

51 rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h

49 rts/libtest.c

52 rts/libtest.c

@@ -62,11 +65,16 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

62 config.mk

65 config.mk

63 rts/*.c rts/*.h rts/Makefile

66 rts/*.c rts/*.h rts/Makefile

64 js/*.js

67 js/*.js

68+ java/org/idris/rts/*.java

66source-repository head

70source-repository head

67 type: git

71 type: git

68 location: git://github.com/edwinb/Idris-dev.git

72 location: git://github.com/edwinb/Idris-dev.git

74+Flag Java

75+ Description: Build the Java RTS

76+ Default: False

77+

71Executable idris

79Executable idris

72 Main-is: Main.hs

80 Main-is: Main.hs

@@ -99,7 +107,7 @@ Executable idris

99 Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal,

107 Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal,

100 haskeline>=0.7, split, directory,

108 haskeline>=0.7, split, directory,

101 containers, process, transformers, filepath,

109 containers, process, transformers, filepath,

102− directory, binary, bytestring, pretty,

110+ directory, binary, bytestring, text, pretty,

103 language-java>=0.2.2, libffi, unix

111 language-java>=0.2.2, libffi, unix

104

112

105 Extensions: MultiParamTypeClasses, FunctionalDependencies,

113 Extensions: MultiParamTypeClasses, FunctionalDependencies,

java/executable_pom_template.xmlnew file+65

@@ -0,0 +1,65 @@

1+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"

2+ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">

3+ <modelVersion>4.0.0</modelVersion>

4+ <groupId>org.idris-lang</groupId>

5+ <artifactId>$ARTIFACT-NAME$</artifactId>

6+ <packaging>jar</packaging>

7+ <version>1.0</version>

8+ <name>$ARTIFACT-NAME$</name>

10+ <properties>

11+ <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

12+ <skipTests>true</skipTests>

13+ </properties>

14+ <dependencies>

15+ <dependency>

16+ <groupId>org.idris-lang</groupId>

17+ <artifactId>idris</artifactId>

18+ <version>$RTS-VERSION$</version>

19+ </dependency>

20+ </dependencies>

21+

22+

23+ <build>

24+ <finalName>$ARTIFACT-NAME$</finalName>

25+ <plugins>

26+ <plugin>

27+ <groupId>org.apache.maven.plugins</groupId>

28+ <artifactId>maven-compiler-plugin</artifactId>

29+ <version>3.0</version>

30+ <configuration>

31+ <source>1.7</source>

32+ <target>1.7</target>

33+ </configuration>

34+ </plugin>

35+ <plugin>

36+ <groupId>org.apache.maven.plugins</groupId>

37+ <artifactId>maven-surefire-plugin</artifactId>

38+ <version>2.14</version>

39+ <configuration>

40+ <skipTests>${skipTests}</skipTests>

41+ </configuration>

42+ </plugin>

43+ <plugin>

44+ <groupId>org.apache.maven.plugins</groupId>

45+ <artifactId>maven-shade-plugin</artifactId>

46+ <version>2.0</version>

47+ <executions>

48+ <execution>

49+ <phase>package</phase>

50+ <goals>

51+ <goal>shade</goal>

52+ </goals>

53+ <configuration>

54+ <transformers>

55+ <transformer implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">

56+ <mainClass>$MAIN-CLASS$</mainClass>

57+ </transformer>

58+ </transformers>

59+ </configuration>

60+ </execution>

61+ </executions>

62+ </plugin>

63+ </plugins>

64+ </build>

65+</project>

java/idris.jardeleted

Binary file not shown.

java/pom_template.xmlnew file+39

@@ -0,0 +1,39 @@

1+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"

2+ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">

3+ <modelVersion>4.0.0</modelVersion>

5+ <groupId>org.idris-lang</groupId>

6+ <artifactId>idris</artifactId>

7+ <version>$RTS-VERSION$</version>

8+ <packaging>jar</packaging>

10+ <name>Runtime System for the Idris Java Backend</name>

11+ <url>http://www.irdis-lang.org</url>

12+

13+ <properties>

14+ <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

15+ <skipTests>true</skipTests>

16+ </properties>

17+

18+ <build>

19+ <plugins>

20+ <plugin>

21+ <groupId>org.apache.maven.plugins</groupId>

22+ <artifactId>maven-compiler-plugin</artifactId>

23+ <version>3.0</version>

24+ <configuration>

25+ <source>1.7</source>

26+ <target>1.7</target>

27+ </configuration>

28+ </plugin>

29+ <plugin>

30+ <groupId>org.apache.maven.plugins</groupId>

31+ <artifactId>maven-surefire-plugin</artifactId>

32+ <version>2.14</version>

33+ <configuration>

34+ <skipTests>${skipTests}</skipTests>

35+ </configuration>

36+ </plugin>

37+ </plugins>

38+ </build>

39+</project>

java/org/idris/rts/Closure.java → java/src/main/java/org/idris/rts/Closure.javarenamed

The content is the same.

java/org/idris/rts/ForeignPrimitives.java → java/src/main/java/org/idris/rts/ForeignPrimitives.javarenamed+16

@@ -195,4 +195,20 @@ public class ForeignPrimitives {

195 public static int isNull(Object o) {

196 return (o == null ? 1 : 0);

197 }

198+

199+ public final static Object idris_K(final Object result, final Object drop) {

200+ return result;

201+ }

202+

203+ public final static Object idris_flipK(final Object drop, final Object result) {

204+ return result;

205+ }

206+

207+ public final static Object idris_assignStack(final Object [] context, final int start, final Object ... vars) {

208+ int i = start;

209+ for (Object var : vars) {

210+ context[i] = var;

211+ }

212+ return context;

213+ }

198}

214}

java/org/idris/rts/IdrisObject.java → java/src/main/java/org/idris/rts/IdrisObject.javarenamed

The content is the same.

java/org/idris/rts/TailCallClosure.java → java/src/main/java/org/idris/rts/TailCallClosure.javarenamed

The content is the same.

lib/Prelude/Strings.idr+3

@@ -115,3 +115,6 @@ unwords' ws = (foldr1 addSpace ws)

115unwords : List String -> String

116unwords = pack . unwords' . map unpack

117

118+length : String -> Nat

119+length = fromInteger . prim_lenString

120+

rts/Makefile+3−2

@@ -1,8 +1,9 @@

1include ../config.mk

3−OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o

3+OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o idris_opts.o idris_stats.o

4−HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h

4+HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h idris_opts.h idris_stats.h

5CFLAGS = -O2 -Wall

6ifneq ($(GMP_INCLUDE_DIR),)

7ifneq ($(GMP_INCLUDE_DIR),)

7 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8endif

9endif

rts/idris_gc.c+21−21

@@ -55,9 +55,9 @@ VAL copy(VM* vm, VAL x) {

55void cheney(VM *vm) {

56 int i;

57 int ar;

58− char* scan = vm->heap;

58+ char* scan = vm->heap.heap;

60− while(scan < vm->heap_next) {

60+ while(scan < vm->heap.next) {

61 size_t inc = *((size_t*)scan);

62 VAL heap_item = (VAL)(scan+sizeof(size_t));

63 // If it's a CON, copy its arguments

@@ -76,21 +76,22 @@ void cheney(VM *vm) {

76 }

77 scan += inc;

78 }

79− assert(scan == vm->heap_next);

79+ assert(scan == vm->heap.next);

80}

82void idris_gc(VM* vm) {

83+ HEAP_CHECK(vm)

84+ STATS_ENTER_GC(vm->stats, vm->heap.size)

83 // printf("Collecting\n");

85 // printf("Collecting\n");

85− char* newheap = malloc(vm -> heap_size);

87+ char* newheap = malloc(vm->heap.size);

86− char* oldheap = vm -> heap;

88+ char* oldheap = vm->heap.heap;

87− if (vm->oldheap != NULL) free(vm->oldheap);

89+ if (vm->heap.old != NULL)

90+ free(vm->heap.old);

89− vm->heap = newheap;

92+ vm->heap.heap = newheap;

90− vm->heap_next = newheap;

93+ vm->heap.next = newheap;

91− vm->heap_end = newheap + vm->heap_size;

94+ vm->heap.end = newheap + vm->heap.size;

92−

93− vm->collections++;

95 VAL* root;

96 VAL* root;

@@ -111,20 +112,19 @@ void idris_gc(VM* vm) {

111 // After reallocation, if we've still more than half filled the new heap, grow the heap

112 // After reallocation, if we've still more than half filled the new heap, grow the heap

112 // for next time.

113 // for next time.

113

114

114− if ((vm->heap_next - vm->heap) > vm->heap_size >> 1) {

115+ if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {

115− vm->heap_size += vm->heap_growth;

116+ vm->heap.size += vm->heap.growth;

116 }

117 }

117− vm->oldheap = oldheap;

118+ vm->heap.old = oldheap;

118

119

119− // gcInfo(vm, 0);

120+ STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)

121+ HEAP_CHECK(vm)

120}

122}

121

123

122void idris_gcInfo(VM* vm, int doGC) {

124void idris_gcInfo(VM* vm, int doGC) {

123− printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

125+ printf("Stack: <BOT %p> <TOP %p>\n", vm->valstack, vm->valstack_top);

124− printf("Total allocations: %d\n", vm->allocations);

125− printf("GCs: %d\n", vm->collections);

126− printf("Final heap size %d\n", (int)(vm->heap_size));

126+ printf("Final heap size %d\n", (int)(vm->heap.size));

127− printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));

127+ printf("Final heap use %d\n", (int)(vm->heap.next - vm->heap.heap));

128 if (doGC) { idris_gc(vm); }

129− printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));

129+ printf("Final heap use after GC %d\n", (int)(vm->heap.next - vm->heap.heap));

130}

rts/idris_heap.cnew file+125

@@ -0,0 +1,125 @@

1+#include "idris_heap.h"

2+#include "idris_rts.h"

4+#include <stdlib.h>

5+#include <stddef.h>

6+#include <stdio.h>

8+void alloc_heap(Heap * h, size_t heap_size)

9+{

10+ char * mem = malloc(heap_size);

11+ if (mem == NULL) {

12+ fprintf(stderr,

13+ "RTS ERROR: Unable to allocate heap. Requested %d bytes.\n",

14+ (int)heap_size);

15+ exit(EXIT_FAILURE);

16+ }

17+

18+ h->heap = mem;

19+ h->next = h->heap;

20+ h->end = h->heap + heap_size;

21+

22+ h->size = heap_size;

23+ h->growth = heap_size;

24+

25+ h->old = NULL;

26+}

27+

28+void free_heap(Heap * h) {

29+ free(h->heap);

30+

31+ if (h->old != NULL) {

32+ free(h->old);

33+ }

34+}

35+

36+// TODO: more testing

37+/******************** Heap testing ********************************************/

38+void heap_check_underflow(Heap * heap) {

39+ if (!(heap->heap <= heap->next)) {

40+ fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n",

41+ heap->heap, heap->next);

42+ exit(EXIT_FAILURE);

43+ }

44+}

45+

46+void heap_check_overflow(Heap * heap) {

47+ if (!(heap->next <= heap->end)) {

48+ fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n",

49+ heap->next, heap->end);

50+ exit(EXIT_FAILURE);

51+ }

52+}

53+

54+int is_valid_ref(VAL v) {

55+ return (v != NULL) && !(ISINT(v));

56+}

57+

58+int ref_in_heap(Heap * heap, VAL v) {

59+ return ((VAL)heap->heap <= v) && (v < (VAL)heap->next);

60+}

61+

62+// Checks three important properties:

63+// 1. Closure.

64+// Check if all pointers in the _heap_ points only to heap.

65+// 2. Unidirectionality. (if compact gc)

66+// All references in the heap should be are unidirectional. In other words,

67+// more recently allocated closure can point only to earlier allocated one.

68+// 3. After gc there should be no forward references.

69+//

70+void heap_check_pointers(Heap * heap) {

71+ char* scan = NULL;

72+

73+ size_t item_size = 0;

74+ for(scan = heap->heap; scan < heap->next; scan += item_size) {

75+ item_size = *((size_t*)scan);

76+ VAL heap_item = (VAL)(scan + sizeof(size_t));

77+

78+ switch(GETTY(heap_item)) {

79+ case CON:

80+ {

81+ int ar = ARITY(heap_item);

82+ int i = 0;

83+ for(i = 0; i < ar; ++i) {

84+ VAL ptr = heap_item->info.c.args[i];

85+

86+ if (is_valid_ref(ptr)) {

87+ // Check for closure.

88+ if (!ref_in_heap(heap, ptr)) {

89+ fprintf(stderr,

90+ "RTS ERROR: heap closure broken. "\

91+ "<HEAP %p %p %p> <REF %p>\n",

92+ heap->heap, heap->next, heap->end, ptr);

93+ exit(EXIT_FAILURE);

94+ }

95+#if 0 // TODO macro

96+ // Check for unidirectionality.

97+ if (!(ptr < heap_item)) {

98+ fprintf(stderr,

99+ "RTS ERROR: heap unidirectionality broken:" \

100+ "<CON %p> <FIELD %p>\n",

101+ heap_item, ptr);

102+ exit(EXIT_FAILURE);

103+ }

104+#endif

105+ }

106+ }

107+ break;

108+ }

109+ case FWD:

110+ // Check for artifacts after cheney gc.

111+ fprintf(stderr, "RTS ERROR: FWD in working heap.\n");

112+ exit(EXIT_FAILURE);

113+ break;

114+ default:

115+ break;

116+ }

117+ }

118+}

119+

120+void heap_check_all(Heap * heap)

121+{

122+ heap_check_underflow(heap);

123+ heap_check_overflow(heap);

124+ heap_check_pointers(heap);

125+}

rts/idris_heap.hnew file+29

@@ -0,0 +1,29 @@

1+#ifndef _IDRIS_HEAP_H

2+#define _IDRIS_HEAP_H

4+#include <stddef.h>

6+typedef struct {

7+ char* next; // Next allocated chunk. Should always (heap <= next < end).

8+ char* heap; // Point to bottom of heap

9+ char* end; // Point to top of heap

10+ size_t size; // Size of _next_ heap. Size of current heap is /end - heap/.

11+ size_t growth; // Quantity of heap growth in bytes.

12+

13+ char* old;

14+} Heap;

15+

16+

17+void alloc_heap(Heap * heap, size_t heap_size);

18+void free_heap(Heap * heap);

19+

20+

21+#ifdef IDRIS_DEBUG

22+void heap_check_all(Heap * heap);

23+// Should be used _between_ gc's.

24+#define HEAP_CHECK(vm) heap_check_all(&(vm->heap));

25+#else

26+#define HEAP_CHECK(vm)

27+#endif // IDRIS_DEBUG

28+

29+#endif // _IDRIS_HEAP_H

rts/idris_main.c+26−5

@@ -1,9 +1,30 @@

1+#include "idris_opts.h"

2+#include "idris_stats.h"

3+#include "idris_rts.h"

4+// The default options should give satisfactory results under many circumstances.

5+RTSOpts opts = {

6+ .init_heap_size = 4096000,

7+ .max_stack_size = 4096000,

8+ .show_summary = 0

9+};

10+

1int main(int argc, char* argv[]) {

11int main(int argc, char* argv[]) {

12+ parse_shift_args(&opts, &argc, &argv);

13+

2− VM* vm = init_vm(4096000, 4096000, 1, argc, argv); // 1024000);

14+ VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1, argc, argv);

3 _idris__123_runMain0_125_(vm, NULL);

15 _idris__123_runMain0_125_(vm, NULL);

4− //_idris_main(vm, NULL);

16+

5−#ifdef IDRIS_TRACE

17+#ifdef IDRIS_DEBUG

18+ if (opts.show_summary) {

6− idris_gcInfo(vm, 1);

19+ idris_gcInfo(vm, 1);

20+ }

7#endif

21#endif

22+

8− terminate(vm);

23+ Stats stats = terminate(vm);

24+

25+ if (opts.show_summary) {

26+ print_stats(&stats);

27+ }

28+

29+ return EXIT_SUCCESS;

30}

rts/idris_opts.cnew file+110

@@ -0,0 +1,110 @@

1+#include "idris_opts.h"

3+#include <stdlib.h>

4+#include <stddef.h>

5+#include <stdio.h>

6+#include <string.h>

9+char usage[] =

10+ "\n" \

11+ "Usage: <prog> [+RTS <rtsopts> -RTS] <args>\n\n" \

12+ "Options:\n\n" \

13+ " -? Print this message and exits.\n" \

14+ " -s Summary GC statistics.\n" \

15+ " -H Initial heap size. Egs: -H4M, -H500K, -H1G\n" \

16+ " -K Sets the maximum stack size. Egs: -K8M\n" \

17+ "\n";

18+

19+void print_usage(FILE * s) {

20+ fprintf(s, usage);

21+}

22+

23+int read_size(char * str) {

24+ int size = 0;

25+ char mult = ' ';

26+

27+ int r = sscanf(str, "%u%c", &size, &mult);

28+

29+ if (r == 1)

30+ return size;

31+

32+ if (r == 2) {

33+ switch (mult) {

34+ case 'K': size = size << 10; break;

35+ case 'M': size = size << 20; break;

36+ case 'G': size = size << 30; break;

37+ default:

38+ fprintf(stderr,

39+ "RTS Opts: Unable to recognize size suffix `%c'.\n" \

40+ " Possible suffixes are K or M or G.\n",

41+ mult);

42+ print_usage(stderr);

43+ exit(EXIT_FAILURE);

44+ }

45+ return size;

46+ }

47+

48+ fprintf(stderr, "RTS Opts: Unable to parse size. Egs: 1K, 10M, 2G.\n");

49+ print_usage(stderr);

50+ exit(EXIT_FAILURE);

51+}

52+

53+

54+int parse_args(RTSOpts * opts, int argc, char *argv[])

55+{

56+ if (argc == 0)

57+ return 0;

58+

59+ if (strcmp(argv[0], "+RTS") != 0)

60+ return 0;

61+

62+ int i;

63+ for (i = 1; i < argc; i++) {

64+ if (strcmp(argv[i], "-RTS") == 0) {

65+ return i + 1;

66+ }

67+

68+ if (argv[i][0] != '-') {

69+ fprintf(stderr, "RTS options should start with '-'.\n");

70+ print_usage(stderr);

71+ exit(EXIT_FAILURE);

72+ }

73+

74+ switch (argv[i][1])

75+ {

76+ case '?':

77+ print_usage(stdout);

78+ exit(EXIT_SUCCESS);

79+ break;

80+

81+ case 's':

82+ opts->show_summary = 1;

83+ break;

84+

85+ case 'H':

86+ opts->init_heap_size = read_size(argv[i] + 2);

87+ break;

88+

89+ case 'K':

90+ opts->max_stack_size = read_size(argv[i] + 2);

91+ break;

92+

93+ default:

94+ printf("RTS opts: Wrong argument: %s\n", argv[i]);

95+ print_usage(stderr);

96+ exit(EXIT_FAILURE);

97+ }

98+ }

99+

100+ return argc;

101+}

102+

103+void parse_shift_args(RTSOpts * opts, int * argc, char ** argv[]) {

104+ size_t shift = parse_args(opts, (*argc) - 1, (*argv) + 1);

105+

106+ char *prg = (*argv)[0];

107+ *argc = *argc - shift;

108+ *argv = *argv + shift;

109+ (*argv)[0] = prg;

110+}

rts/idris_opts.hnew file+19

@@ -0,0 +1,19 @@

1+#ifndef _IDRIS_OPTS_H

2+#define _IDRIS_OPTS_H

4+#include <stddef.h>

5+#include <stdio.h>

7+typedef struct {

8+ size_t init_heap_size;

9+ size_t max_stack_size;

10+ int show_summary;

11+} RTSOpts;

12+

13+void print_usage(FILE * s);

14+

15+// Parse rts options and shift arguments such that rts options becomes invisible

16+// for main program.

17+void parse_shift_args(RTSOpts * opts, int * argc, char ** argv[]);

18+

19+#endif

rts/idris_rts.c+41−25

@@ -10,14 +10,19 @@

10#include "idris_gc.h"

11#include "idris_bitstring.h"

13+

13VM* init_vm(int stack_size, size_t heap_size,

14VM* init_vm(int stack_size, size_t heap_size,

14 int max_threads, // not implemented yet

15 int max_threads, // not implemented yet

15 int argc, char* argv[]) {

16 int argc, char* argv[]) {

16− VAL* valstack = malloc(stack_size*sizeof(VAL));

17− int* intstack = malloc(stack_size*sizeof(int));

18− double* floatstack = malloc(stack_size*sizeof(double));

20 VM* vm = malloc(sizeof(VM));

18 VM* vm = malloc(sizeof(VM));

19+ STATS_INIT_STATS(vm->stats)

20+ STATS_ENTER_INIT(vm->stats)

21+

22+ VAL* valstack = malloc(stack_size * sizeof(VAL));

23+ int* intstack = malloc(stack_size * sizeof(int));

24+ double* floatstack = malloc(stack_size*sizeof(double));

25+

21 vm->valstack = valstack;

26 vm->valstack = valstack;

22 vm->valstack_top = valstack;

27 vm->valstack_top = valstack;

23 vm->valstack_base = valstack;

28 vm->valstack_base = valstack;

@@ -26,14 +31,9 @@ VM* init_vm(int stack_size, size_t heap_size,

26 vm->floatstack = floatstack;

31 vm->floatstack = floatstack;

27 vm->floatstack_ptr = floatstack;

32 vm->floatstack_ptr = floatstack;

28 vm->stack_max = valstack + stack_size;

33 vm->stack_max = valstack + stack_size;

34+

29− vm->heap = malloc(heap_size);

35+ alloc_heap(&(vm->heap), heap_size);

30− vm->oldheap = NULL;

36+

31− vm->heap_next = vm->heap;

32− vm->heap_end = vm->heap + heap_size;

33− vm->heap_size = heap_size;

34− vm->collections = 0;

35− vm->allocations = 0;

36− vm->heap_growth = heap_size;

37 vm->ret = NULL;

38 vm->reg1 = NULL;

@@ -60,25 +60,32 @@ VM* init_vm(int stack_size, size_t heap_size,

60 vm->argv[i] = MKSTR(vm, argv[i]);

61 }

63+ STATS_LEAVE_INIT(vm->stats)

63 return vm;

64 return vm;

64}

65}

66−void terminate(VM* vm) {

67+Stats terminate(VM* vm) {

68+ Stats stats = vm->stats;

69+ STATS_ENTER_EXIT(stats)

70+

67 free(vm->inbox);

71 free(vm->inbox);

68 free(vm->valstack);

72 free(vm->valstack);

69 free(vm->intstack);

73 free(vm->intstack);

70 free(vm->floatstack);

74 free(vm->floatstack);

71− free(vm->heap);

75+ free_heap(&(vm->heap));

72 free(vm->argv);

76 free(vm->argv);

73− if (vm->oldheap != NULL) { free(vm->oldheap); }

77+

74 pthread_mutex_destroy(&(vm -> inbox_lock));

78 pthread_mutex_destroy(&(vm -> inbox_lock));

75 pthread_mutex_destroy(&(vm -> inbox_block));

79 pthread_mutex_destroy(&(vm -> inbox_block));

76 pthread_cond_destroy(&(vm -> inbox_waiting));

80 pthread_cond_destroy(&(vm -> inbox_waiting));

77 free(vm);

81 free(vm);

82+

83+ STATS_LEAVE_EXIT(stats)

84+ return stats;

78}

85}

80void idris_requireAlloc(VM* vm, size_t size) {

87void idris_requireAlloc(VM* vm, size_t size) {

81− if (!(vm -> heap_next + size < vm -> heap_end)) {

88+ if (!(vm->heap.next + size < vm->heap.end)) {

82 idris_gc(vm);

89 idris_gc(vm);

83 }

90 }

@@ -106,12 +113,19 @@ void* allocate(VM* vm, size_t size, int outerlock) {

106 if ((size & 7)!=0) {

113 if ((size & 7)!=0) {

107 size = 8 + ((size >> 3) << 3);

114 size = 8 + ((size >> 3) << 3);

108 }

115 }

109− if (vm -> heap_next + size < vm -> heap_end) {

116+

110− vm->allocations += size + sizeof(size_t);

117+ size_t chunk_size = size + sizeof(size_t);

118+

119+ if (vm->heap.next + chunk_size < vm->heap.end) {

120+ STATS_ALLOC(vm->stats, chunk_size)

111− void* ptr = (void*)(vm->heap_next + sizeof(size_t));

121+ void* ptr = (void*)(vm->heap.next + sizeof(size_t));

112− *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

122+ *((size_t*)(vm->heap.next)) = chunk_size;

113− vm -> heap_next += size + sizeof(size_t);

123+ vm->heap.next += chunk_size;

124+

125+ assert(vm->heap.next <= vm->heap.end);

126+

114 memset(ptr, 0, size);

127 memset(ptr, 0, size);

128+

115 if (lock) { // not message passing

129 if (lock) { // not message passing

116 pthread_mutex_unlock(&vm->alloc_lock);

130 pthread_mutex_unlock(&vm->alloc_lock);

117 }

131 }

@@ -208,7 +222,7 @@ void dumpStack(VM* vm) {

208 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {

222 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {

209 printf("%d: ", i);

223 printf("%d: ", i);

210 dumpVal(*root);

224 dumpVal(*root);

211− if (*root >= (VAL)(vm->heap) && *root < (VAL)(vm->heap_end)) { printf("OK"); }

225+ if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf("OK"); }

212 printf("\n");

226 printf("\n");

213 }

227 }

214 printf("RET: ");

228 printf("RET: ");

@@ -401,12 +415,14 @@ void* runThread(void* arg) {

401 callvm->processes--;

415 callvm->processes--;

402

416

403 free(td);

417 free(td);

418+

404− terminate(vm);

419+ Stats stats = terminate(vm);

420+ // aggregate_stats(&(td->vm->stats), &stats);

405 return NULL;

421 return NULL;

406}

422}

407

423

408void* vmThread(VM* callvm, func f, VAL arg) {

424void* vmThread(VM* callvm, func f, VAL arg) {

409− VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size,

425+ VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap.size,

410 callvm->max_threads,

426 callvm->max_threads,

411 0, NULL);

427 0, NULL);

412 vm->processes=1; // since it can send and receive messages

428 vm->processes=1; // since it can send and receive messages

@@ -493,12 +509,12 @@ void idris_sendMessage(VM* sender, VM* dest, VAL msg) {

493 // So: we try to copy, if a collection happens, we do the copy again

509 // So: we try to copy, if a collection happens, we do the copy again

494 // under the assumption there's enough space this time.

510 // under the assumption there's enough space this time.

495

511

496− int gcs = dest->collections;

512+ int gcs = dest->stats.collections;

497 pthread_mutex_lock(&dest->alloc_lock);

513 pthread_mutex_lock(&dest->alloc_lock);

498 VAL dmsg = copyTo(dest, msg);

514 VAL dmsg = copyTo(dest, msg);

499 pthread_mutex_unlock(&dest->alloc_lock);

515 pthread_mutex_unlock(&dest->alloc_lock);

500

516

501− if (dest->collections>gcs) {

517+ if (dest->stats.collections > gcs) {

502 // a collection will have invalidated the copy

518 // a collection will have invalidated the copy

503 pthread_mutex_lock(&dest->alloc_lock);

519 pthread_mutex_lock(&dest->alloc_lock);

504 dmsg = copyTo(dest, msg); // try again now there's room...

520 dmsg = copyTo(dest, msg); // try again now there's room...

rts/idris_rts.h+9−10

@@ -9,6 +9,9 @@

9#include <pthread.h>

10#include <stdint.h>

12+#include "idris_heap.h"

13+#include "idris_stats.h"

14+

12// Closures

15// Closures

14typedef enum {

17typedef enum {

@@ -47,12 +50,10 @@ typedef struct {

47 VAL* valstack_base;

50 VAL* valstack_base;

48 int* intstack_ptr;

51 int* intstack_ptr;

49 double* floatstack_ptr;

52 double* floatstack_ptr;

50− char* heap;

51− char* oldheap;

52− char* heap_next;

53− char* heap_end;

54 VAL* stack_max;

53 VAL* stack_max;

55−

54+

55+ Heap heap;

56+

56 pthread_mutex_t inbox_lock;

57 pthread_mutex_t inbox_lock;

57 pthread_mutex_t inbox_block;

58 pthread_mutex_t inbox_block;

58 pthread_mutex_t alloc_lock;

59 pthread_mutex_t alloc_lock;

@@ -66,14 +67,12 @@ typedef struct {

67 int processes; // Number of child processes

68 int processes; // Number of child processes

68 int max_threads; // maximum number of threads to run in parallel

69 int max_threads; // maximum number of threads to run in parallel

70+

71+ Stats stats;

70 int argc;

73 int argc;

71 VAL* argv; // command line arguments

74 VAL* argv; // command line arguments

73− size_t heap_size;

74− size_t heap_growth;

75− int allocations;

76− int collections;

77 VAL ret;

76 VAL ret;

78 VAL reg1;

77 VAL reg1;

79} VM;

78} VM;

@@ -83,7 +82,7 @@ VM* init_vm(int stack_size, size_t heap_size,

83 int max_threads,

82 int max_threads,

84 int argc, char* argv[]);

83 int argc, char* argv[]);

85// Clean up a VM once it's no longer needed

84// Clean up a VM once it's no longer needed

86−void terminate(VM* vm);

85+Stats terminate(VM* vm);

88// Functions all take a pointer to their VM, and previous stack base,

87// Functions all take a pointer to their VM, and previous stack base,

89// and return nothing.

88// and return nothing.

rts/idris_stats.cnew file+53

@@ -0,0 +1,53 @@

1+#include "idris_stats.h"

3+#include <stdio.h>

4+#include <locale.h>

6+#ifdef IDRIS_ENABLE_STATS

8+void print_stats(const Stats * stats) {

9+ clock_t total = clock() - stats->start_time;

10+ clock_t mut = total - stats->init_time - stats->gc_time - stats->exit_time;

11+ double mut_sec = (double)mut / CLOCKS_PER_SEC;

12+ int avg_chunk = (int)((double)stats->allocations / (double)stats->alloc_count);

13+ int alloc_rate = (int)((double)(stats->allocations) / mut_sec);

14+

15+ setlocale(LC_NUMERIC, "");

16+ printf("\n");

17+ printf("%'20d bytes allocated in the heap\n", stats->allocations);

18+ printf("%'20d bytes copied during GC\n", stats->copied);

19+ printf("%'20d maximum heap size\n", stats->max_heap_size);

20+ printf("%'20d chunks allocated in the heap\n", stats->alloc_count);

21+ printf("%'20d average chunk size\n\n", avg_chunk);

22+

23+ printf("GC called %d times\n\n", stats->collections);

24+

25+ printf("INIT time: %8.3fs\n", (double)stats->init_time / CLOCKS_PER_SEC);

26+ printf("MUT time: %8.3fs\n", mut_sec);

27+ printf("GC time: %8.3fs\n", (double)stats->gc_time / CLOCKS_PER_SEC);

28+ printf("EXIT time: %8.3fs\n", (double)stats->exit_time / CLOCKS_PER_SEC);

29+ printf("TOTAL time: %8.3fs\n\n", (double)total / CLOCKS_PER_SEC);

30+

31+ printf("%%GC time: %.2f%%\n\n", 100 * (double)stats->gc_time / (double)total);

32+

33+ printf("Alloc rate %'d bytes per MUT sec\n\n", alloc_rate);

34+

35+ printf("Productivity %.2f%%\n", 100 * ((double)mut / (double)total));

36+}

37+

38+void aggregate_stats(Stats * stats1, const Stats * stats2) {

39+ fprintf(stderr, "RTS error: aggregate_stats not implemented");

40+}

41+

42+#else

43+

44+void print_stats(const Stats * stats) {

45+ fprintf(stderr, "RTS ERROR: Stats are disabled.\n" \

46+ "By the way GC called %d times.\n", stats->collections);

47+}

48+

49+void aggregate_stats(Stats * stats1, const Stats * stats2) {

50+ stats1->collections += stats2->collections;

51+}

52+

53+#endif // IDRIS_ENABLE_STATS

rts/idris_stats.hnew file+73

@@ -0,0 +1,73 @@

1+#ifndef _IDRIS_STATS_H

2+#define _IDRIS_STATS_H

4+#include <time.h>

6+// Should not be defined in release.

7+#define IDRIS_ENABLE_STATS

9+// TODO: measure user time, exclusive/inclusive stats

10+typedef struct {

11+#ifdef IDRIS_ENABLE_STATS

12+ int allocations; // Size of allocated space in bytes for all execution time.

13+ int alloc_count; // How many times alloc is called.

14+ int copied; // Size of space copied during GC.

15+ int max_heap_size; // Maximum heap size achieved.

16+

17+ clock_t init_time; // Time spent for vm initialization.

18+ clock_t exit_time; // Time spent for vm termination.

19+ clock_t gc_time; // Time spent for gc for all execution time.

20+ clock_t max_gc_pause; // Time spent for longest gc.

21+ clock_t start_time; // Time of rts entry point.

22+#endif // IDRIS_ENABLE_STATS

23+ int collections; // How many times gc called.

24+} Stats; // without start time it's a monoid, can we remove start_time it somehow?

25+

26+void print_stats(const Stats * stats);

27+void aggregate_stats(Stats * stats1, const Stats * stats2);

28+

29+

30+#ifdef IDRIS_ENABLE_STATS

31+

32+#ifndef MAX

33+#define MAX(a, b) ((a) > (b) ? (a) : (b))

34+#endif

35+

36+#define STATS_INIT_STATS(stats) \

37+ memset(&stats, 0, sizeof(Stats)); \

38+ stats.start_time = clock();

39+

40+#define STATS_ALLOC(stats, size) \

41+ stats.allocations += size; \

42+ stats.alloc_count = stats.alloc_count + 1;

43+

44+#define STATS_ENTER_INIT(stats) clock_t _start_time = clock();

45+#define STATS_LEAVE_INIT(stats) stats.init_time = clock() - _start_time;

46+

47+#define STATS_ENTER_EXIT(stats) clock_t _start_time = clock();

48+#define STATS_LEAVE_EXIT(stats) stats.exit_time = clock() - _start_time;

49+

50+#define STATS_ENTER_GC(stats, heap_size) \

51+ clock_t _start_time = clock(); \

52+ stats.max_heap_size = MAX(stats.max_heap_size, heap_size);

53+#define STATS_LEAVE_GC(stats, heap_size, heap_occuped) \

54+ clock_t _pause = clock() - _start_time; \

55+ stats.gc_time += _pause; \

56+ stats.max_gc_pause = MAX(_pause, stats.max_gc_pause); \

57+ stats.max_heap_size = MAX(stats.max_heap_size, heap_size); \

58+ stats.copied += heap_occuped; \

59+ stats.collections = stats.collections + 1;

60+

61+#else

62+#define STATS_INIT_STATS(stats) memset(&stats, 0, sizeof(Stats));

63+#define STATS_ENTER_INIT(stats)

64+#define STATS_LEAVE_INIT(stats)

65+#define STATS_ENTER_EXIT(stats)

66+#define STATS_LEAVE_EXIT(stats)

67+#define STATS_ALLOC(stats, size)

68+#define STATS_ENTER_GC(stats, heap_size)

69+#define STATS_LEAVE_GC(stats, heap_size, heap_occuped) \

70+ stats.collections = stats.collections + 1;

71+#endif // IDRIS_ENABLE_STATS

72+

73+#endif // _IDRIS_STATS_H

src/Core/CaseTree.hs+8−2

@@ -167,9 +167,15 @@ data Phase = CompileTime | RunTime

167

168simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->

169 TC CaseDef

170−simpleCase tc cover phase fc []

170+simpleCase tc cover phase fc cs

171+ = sc' tc cover phase fc (filter (\(_, _, r) ->

172+ case r of

173+ Impossible -> False

174+ _ -> True) cs)

175+ where

176+ sc' tc cover phase fc []

171 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

177 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

172−simpleCase tc cover phase fc cs

178+ sc' tc cover phase fc cs

173 = let proj = phase == RunTime

179 = let proj = phase == RunTime

174 pats = map (\ (avs, l, r) ->

180 pats = map (\ (avs, l, r) ->

175 (avs, toPats tc l, (l, r))) cs

181 (avs, toPats tc l, (l, r))) cs

src/Core/Elaborate.hs+27−18

@@ -471,8 +471,8 @@ apply_elab n args =

471

472simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

473simple_app fun arg =

474− do a <- unique_hole (MN 0 "a")

474+ do a <- unique_hole (MN 0 "argTy")

475− b <- unique_hole (MN 0 "b")

475+ b <- unique_hole (MN 0 "retTy")

476 f <- unique_hole (MN 0 "f")

477 s <- unique_hole (MN 0 "s")

478 claim a RType

@@ -516,9 +516,9 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

516try' t1 t2 proofSearch

517 = do s <- get

518 ps <- get_probs

519− case prunStateT ps t1 s of

519+ case prunStateT 999999 False ps t1 s of

520− OK (v, s') -> do put s'

520+ OK ((v, _), s') -> do put s'

521− return v

521+ return v

522 Error e1 -> if recoverableErr e1 then

523 do case runStateT t2 s of

524 OK (v, s') -> do put s'; return v

@@ -539,42 +539,51 @@ tryWhen False a b = a

539

540-- Try a selection of tactics. Exactly one must work, all others must fail

541tryAll :: [(Elab' aux a, String)] -> Elab' aux a

542−tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

542+tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)

543 where

544 cantResolve :: Elab' aux a

545 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

546

547 tryAll' :: [Elab' aux a] -> -- successes

548+ Int -> -- most problems

548 (Elab' aux a, Int) -> -- smallest failure

549 (Elab' aux a, Int) -> -- smallest failure

549 [Elab' aux a] -> -- still to try

550 [Elab' aux a] -> -- still to try

550 Elab' aux a

551 Elab' aux a

551− tryAll' [res] _ [] = res

552+ tryAll' [res] pmax _ [] = res

552− tryAll' (_:_) _ [] = cantResolve

553+ tryAll' (_:_) pmax _ [] = cantResolve

553− tryAll' [] (f, _) [] = f

554+ tryAll' [] pmax (f, _) [] = f

554− tryAll' cs f (x:xs)

555+ tryAll' cs pmax f (x:xs)

555 = do s <- get

556 = do s <- get

556 ps <- get_probs

557 ps <- get_probs

557− case prunStateT ps x s of

558+ case prunStateT pmax True ps x s of

558− OK (v, s') -> tryAll' ((do put s'

559+ OK ((v, newps), s') ->

559− return v):cs) f xs

560+ do let cs' = if (newps < pmax)

561+ then [do put s'; return v]

562+ else (do put s'; return v) : cs

563+ tryAll' cs' newps f xs

560 Error err -> do put s

564 Error err -> do put s

561 if (score err) < 100

565 if (score err) < 100

562− then tryAll' cs (better err f) xs

566+ then tryAll' cs pmax (better err f) xs

563− else tryAll' [] (better err f) xs -- give up

567+ else tryAll' [] pmax (better err f) xs -- give up

564

568

565

569

566 better err (f, i) = let s = score err in

570 better err (f, i) = let s = score err in

567 if (s >= i) then (lift (tfail err), s)

571 if (s >= i) then (lift (tfail err), s)

568 else (f, i)

572 else (f, i)

569

573

570−prunStateT ps x s

574+prunStateT pmax zok ps x s

571 = case runStateT x s of

575 = case runStateT x s of

572 OK (v, s'@(ES (p, _) _ _)) ->

576 OK (v, s'@(ES (p, _) _ _)) ->

573− if (length (problems p) > length ps)

577+ let newps = length (problems p) - length ps

578+ newpmax = if newps < 0 then 0 else newps in

579+ if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

574 then case reverse (problems p) of

580 then case reverse (problems p) of

575 ((_,_,_,e):_) -> Error e

581 ((_,_,_,e):_) -> Error e

576− else OK (v, s')

582+ else OK ((v, newpmax), s')

577 Error e -> Error e

583 Error e -> Error e

578

584

585+qshow :: Fails -> String

586+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

587+

579dumpprobs [] = ""

588dumpprobs [] = ""

580dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

589dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Core/ProofState.hs+12−7

@@ -155,10 +155,15 @@ qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

155unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

156unify' ctxt env topx topy =

157 do ps <- get

158+ let dont = dontunify ps

159+ (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

158− (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)

160+ lift $ unify ctxt env topx topy dont (holes ps)

159−-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++

161+-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

162+-- -- " in " ++ show env ++

160−-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

163+-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

161−-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $

164+-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

165+-- -- ++ show (pterm ps)

166+-- ++ "\n----------") $

162 case fails of

167 case fails of

163-- [] -> return u

168-- [] -> return u

164 err ->

169 err ->

@@ -396,9 +401,9 @@ solve ctxt env (Bind x (Guess ty val) sc)

396 instances = instances ps \\ [x] })

401 instances = instances ps \\ [x] })

397 return $ {- Bind x (Let ty val) sc -}

402 return $ {- Bind x (Let ty val) sc -}

398 instantiate val (pToV x sc)

403 instantiate val (pToV x sc)

399− | otherwise = do ps <- get

400− lift $ tfail $ IncompleteTerm val

404+ | otherwise = lift $ tfail $ IncompleteTerm val

405+solve _ _ h@(Bind x t sc)

401−solve _ _ h = do ps <- get

406+ = do ps <- get

402 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

407 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

403

408

404introTy :: Raw -> Maybe Name -> RunTactic

409introTy :: Raw -> Maybe Name -> RunTactic

src/Core/Unify.hs+64−11

@@ -29,7 +29,7 @@ data UResult a = UOK a

30unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

31 TC ([(Name, TT Name)], Fails)

32−unify ctxt env topx topy injtc holes =

32+unify ctxt env topx topy dont holes =

33-- trace ("Unifying " ++ show (topx, topy)) $

34 -- don't bother if topx and topy are different at the head

35 case runStateT (un False [] topx topy) (UI 0 []) of

@@ -54,8 +54,9 @@ unify ctxt env topx topy injtc holes =

55 injective (P (DCon _ _) _ _) = True

56 injective (P (TCon _ _) _ _) = True

57− injective (P _ n _) = n `elem` injtc

57+ injective (App f (P _ _ _)) = injective f

58+ injective (App f (Constant _)) = injective f

58− injective (App f a) = injective f

59+ injective (App f a) = injective f && injective a

59 injective _ = False

60 injective _ = False

61 notP (P _ _ _) = False

62 notP (P _ _ _) = False

@@ -94,12 +95,16 @@ unify ctxt env topx topy injtc holes =

94 = unifyFail topx topy

95 = unifyFail topx topy

95 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

96 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

96 = unifyFail topx topy

97 = unifyFail topx topy

98+ un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

99+ = unifyFail topx topy

100+ un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)

101+ = unifyFail topx topy

97 un' fn bnames tx@(P _ x _) ty@(P _ y _)

102 un' fn bnames tx@(P _ x _) ty@(P _ y _)

98 | (x,y) `elem` bnames || x == y = do sc 1; return []

103 | (x,y) `elem` bnames || x == y = do sc 1; return []

99 | injective tx && not (holeIn env y || y `elem` holes)

104 | injective tx && not (holeIn env y || y `elem` holes)

100− = unifyFail tx ty

105+ = unifyTmpFail tx ty

101 | injective ty && not (holeIn env x || x `elem` holes)

106 | injective ty && not (holeIn env x || x `elem` holes)

102− = unifyFail tx ty

107+ = unifyTmpFail tx ty

103 un' fn bnames xtm@(P _ x _) tm

108 un' fn bnames xtm@(P _ x _) tm

104 | holeIn env x || x `elem` holes

109 | holeIn env x || x `elem` holes

105 = do UI s f <- get

110 = do UI s f <- get

@@ -128,8 +133,8 @@ unify ctxt env topx topy injtc holes =

128 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

129

134

130 un' fn bnames appx@(App fx ax) appy@(App fy ay)

135 un' fn bnames appx@(App fx ax) appy@(App fy ay)

131− | injective fx && metavarApp appy

136+ | injective fx && sameArgStruct appx appy && metavarApp appy

132− || injective fy && metavarApp appx

137+ || injective fy && sameArgStruct appx appy && metavarApp appx

133 || injective fx && injective fy

138 || injective fx && injective fy

134 || fx == fy

139 || fx == fy

135 = do let (headx, _) = unApply fx

140 = do let (headx, _) = unApply fx

@@ -158,12 +163,14 @@ unify ctxt env topx topy injtc holes =

158 let (heady, argsy) = unApply appy

163 let (heady, argsy) = unApply appy

159 if (length argsx == length argsy &&

164 if (length argsx == length argsy &&

160 ((headx == heady) || (argsx == argsy) ||

165 ((headx == heady) || (argsx == argsy) ||

166+ (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

167+ then

161− (notFn headx && notFn heady))) then

168+-- (notFn headx && notFn heady))) then

162 do uf <- un' True bnames headx heady

169 do uf <- un' True bnames headx heady

163 unArgs uf argsx argsy

170 unArgs uf argsx argsy

164 else unifyTmpFail appx appy

171 else unifyTmpFail appx appy

165 where hnormalise [] _ _ t = t

172 where hnormalise [] _ _ t = t

166− hnormalise ns ctxt env t = hnf ctxt env t

173+ hnormalise ns ctxt env t = normalise ctxt env t

167 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

174 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

168 | x /= y = unifyFail appx appy

175 | x /= y = unifyFail appx appy

169 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

176 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

@@ -183,10 +190,39 @@ unify ctxt env topx topy injtc holes =

183 unArgs vs xs ys

190 unArgs vs xs ys

184

191

185 metavarApp tm = let (f, args) = unApply tm in

192 metavarApp tm = let (f, args) = unApply tm in

186− all (\x -> metavar x || notFn x) (f : args)

193+ all (\x -> metavar x || inenv x) (f : args)

194+ metavarArgs tm = let (f, args) = unApply tm in

195+ all (\x -> metavar x || inenv x) args

196+ metavarApp' tm = let (f, args) = unApply tm in

197+ all (\x -> pat x || metavar x) (f : args)

198+

199+ sameArgStruct appx appy = let (_, ax) = unApply appx

200+ (_, ay) = unApply appy in

201+ and (zipWith sameStruct ax ay)

202+

203+ sameStruct fapp@(App f x) gapp@(App g y)

204+ = let (f',a') = unApply fapp

205+ (g',b') = unApply gapp in

206+ (f' == g' && length a' == length b' &&

207+ (injective f' || injective g'))

208+ || (sameStruct f g && sameStruct x y)

209+ sameStruct (P _ x _) (P _ y _) = True

210+ sameStruct (V i) (V j) = i == j

211+ sameStruct (Constant x) (Constant y) = True

212+ sameStruct (P _ _ _) (Constant y) = True

213+ sameStruct (Constant x) (P _ _ _) = True

214+ sameStruct (Bind n t sc) (P _ _ _) = True

215+ sameStruct (P _ _ _) (Bind n t sc) = True

216+ sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'

217+ sameStruct _ _ = False

218+

187 metavar t = case t of

219 metavar t = case t of

188− P _ x _ -> x `elem` holes || holeIn env x

220+ P _ x _ -> (x `elem` holes || holeIn env x) &&

221+ not (x `elem` dont)

189 _ -> False

222 _ -> False

223+ pat t = case t of

224+ P _ x _ -> x `elem` holes || patIn env x

225+ _ -> False

190 inenv t = case t of

226 inenv t = case t of

191 P _ x _ -> x `elem` (map fst env)

227 P _ x _ -> x `elem` (map fst env)

192 _ -> False

228 _ -> False

@@ -197,6 +233,10 @@ unify ctxt env topx topy injtc holes =

197 | n == n' = un' False bnames x y

233 | n == n' = un' False bnames x y

198 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

234 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

199 | n == n' = un' False bnames x y

235 | n == n' = un' False bnames x y

236+ un' fn bnames x (Bind n (Lam t) (App y (V 0)))

237+ = un' False bnames x y

238+ un' fn bnames (Bind n (Lam t) (App x (V 0))) y

239+ = un' False bnames x y

200-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

240-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

201-- = un' False ((x,y):bnames) sx sy

241-- = un' False ((x,y):bnames) sx sy

202-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

242-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

@@ -285,8 +325,14 @@ unify ctxt env topx topy injtc holes =

285 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

325 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

286 | x == y = True

326 | x == y = True

287 | otherwise = False

327 | otherwise = False

328+ recoverable (Constant _) (P (DCon _ _) y _) = False

329+ recoverable (P (DCon _ _) x _) (Constant _) = False

330+ recoverable (Constant _) (P (TCon _ _) y _) = False

331+ recoverable (P (TCon _ _) x _) (Constant _) = False

288 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

332 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

289 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

333 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

334+ recoverable p@(Constant _) (App f a) = recoverable p f

335+ recoverable (App f a) p@(Constant _) = recoverable f p

290 recoverable p@(P _ n _) (App f a) = recoverable p f

336 recoverable p@(P _ n _) (App f a) = recoverable p f

291-- recoverable (App f a) p@(P _ _ _) = recoverable f p

337-- recoverable (App f a) p@(P _ _ _) = recoverable f p

292 recoverable (App f a) (App f' a')

338 recoverable (App f a) (App f' a')

@@ -298,5 +344,12 @@ errEnv = map (\(x, b) -> (x, binderTy b))

298holeIn :: Env -> Name -> Bool

344holeIn :: Env -> Name -> Bool

299holeIn env n = case lookup n env of

345holeIn env n = case lookup n env of

300 Just (Hole _) -> True

346 Just (Hole _) -> True

347+ Just (Guess _ _) -> True

348+ _ -> False

349+

350+patIn :: Env -> Name -> Bool

351+patIn env n = case lookup n env of

352+ Just (PVar _) -> True

353+ Just (PVTy _) -> True

301 _ -> False

354 _ -> False

302

355

src/IRTS/CodegenJava.hs+755−591

@@ -11,8 +11,13 @@ import Util.System

11import Control.Applicative

12import Control.Arrow

13import Control.Monad

14+import qualified Control.Monad.Trans as T

15+import Control.Monad.Trans.State

14import Data.Char

16import Data.Char

15import Data.Maybe (fromJust)

17import Data.Maybe (fromJust)

18+import Data.List (isPrefixOf, intercalate)

19+import qualified Data.Text as T

20+import qualified Data.Text.IO as TIO

16import Language.Java.Parser

21import Language.Java.Parser

17import Language.Java.Pretty

22import Language.Java.Pretty

18import Language.Java.Syntax hiding (Name)

23import Language.Java.Syntax hiding (Name)

@@ -23,19 +28,83 @@ import System.FilePath

23import System.IO

28import System.IO

24import System.Process

29import System.Process

31+data CodeGenerationEnv = CodeGenerationEnv { globalVariablePositions :: [(Name, Integer)] }

32+

33+type CodeGeneration = StateT (CodeGenerationEnv) (Either String)

34+

26−codegenJava :: [(Name, SDecl)] ->

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

36+ [(Name, SDecl)] ->

27 FilePath -> -- output file name

37 FilePath -> -- output file name

28 OutputType ->

38 OutputType ->

29 IO ()

39 IO ()

30−codegenJava defs out exec =

40+codegenJava globalInit defs out exec = do

31− either (error)

41+ withTempdir (takeBaseName out) $ \ tmpDir -> do

42+ let srcdir = tmpDir </> "src" </> "main" </> "java"

43+ createDirectoryIfMissing True srcdir

44+ let (Ident clsName) =

45+ either error id (evalStateT (mkClassName out) (mkCodeGenEnv globalInit))

46+ let outjava = srcdir </> clsName <.> "java"

47+ let jout = either error

32− (writeFile out . flatIndent . prettyPrint)

48+ (flatIndent . prettyPrint)

33− (mkCompilationUnit defs out)

49+ (evalStateT (mkCompilationUnit globalInit defs out) (mkCodeGenEnv globalInit))

34−

50+ writeFile outjava jout

51+ if (exec == Raw)

52+ then copyFile outjava (takeDirectory out </> clsName <.> "java")

53+ else do

54+ execPom <- getExecutablePom

55+ execPomTemplate <- TIO.readFile execPom

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

57+ (T.pack clsName)

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

59+ (T.pack $ takeBaseName out)

60+ execPomTemplate)

61+ TIO.writeFile (tmpDir </> "pom.xml") execPom

62+ mvnCmd <- getMvn

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

64+ (exit, _, err) <- readProcessWithExitCode mvnCmd (args ++ ["compile"]) ""

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

66+ if (exec == Object)

67+ then do

68+ classFiles <-

69+ map (\ clsFile -> tmpDir </> "target" </> "classes" </> clsFile)

70+ . filter ((".class" ==) . takeExtension)

71+ <$> getDirectoryContents (tmpDir </> "target" </> "classes")

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

73+ classFiles

74+ else do

75+ (exit, _, err) <- readProcessWithExitCode mvnCmd (args ++ ["package"]) ""

76+ when (exit /= ExitSuccess) (error ("FAILURE: " ++ mvnCmd ++ " package\n" ++ err))

77+ copyFile (tmpDir </> "target" </> (takeBaseName out) <.> "jar") out

78+ handle <- openBinaryFile out ReadMode

79+ contents <- TIO.hGetContents handle

80+ hClose handle

81+ handle <- openBinaryFile out WriteMode

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

83+ hFlush handle

84+ hClose handle

85+ perms <- getPermissions out

86+ setPermissions out (setOwnerExecutable True perms)

87+ readProcess mvnCmd (args ++ ["clean"]) ""

88+ removeFile (tmpDir </> "pom.xml")

89+

90+jarHeader :: String

91+jarHeader =

92+ "#!/bin/sh\n"

93+ ++ "MYSELF=`which \"$0\" 2>/dev/null`\n"

94+ ++ "[ $? -gt 0 -a -f \"$0\" ] && MYSELF=\"./$0\"\n"

95+ ++ "java=java\n"

96+ ++ "if test -n \"$JAVA_HOME\"; then\n"

97+ ++ " java=\"$JAVA_HOME/bin/java\"\n"

98+ ++ "fi\n"

99+ ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""

100+ ++ "exit 1\n"

101+

102+mkCodeGenEnv :: [(Name, SExp)] -> CodeGenerationEnv

103+mkCodeGenEnv globalInit =

104+ CodeGenerationEnv $ zipWith (\ (name, _) pos -> (name, pos)) globalInit [0..]

105+

35−mkCompilationUnit :: [(Name, SDecl)] ->

106+mkCompilationUnit :: [(Name, SExp)] -> [(Name, SDecl)] -> FilePath -> CodeGeneration CompilationUnit

36− FilePath ->

37− Either String CompilationUnit

38−mkCompilationUnit defs out =

107+mkCompilationUnit globalInit defs out =

39 CompilationUnit Nothing [ ImportDecl False idrisRts True

108 CompilationUnit Nothing [ ImportDecl False idrisRts True

40 , ImportDecl True idrisForeign True

109 , ImportDecl True idrisForeign True

41 , ImportDecl False bigInteger False

110 , ImportDecl False bigInteger False

@@ -44,7 +113,7 @@ mkCompilationUnit defs out =

44 , ImportDecl False scanner False

113 , ImportDecl False scanner False

45 , ImportDecl False arrays False

114 , ImportDecl False arrays False

46 ] <$>

115 ] <$>

47− mkTypeDecl defs out

116+ mkTypeDecl globalInit defs out

48 where

117 where

49 idrisRts = J.Name $ map Ident ["org", "idris", "rts"]

118 idrisRts = J.Name $ map Ident ["org", "idris", "rts"]

50 idrisForeign = J.Name $ map Ident ["org", "idris", "rts", "ForeignPrimitives"]

119 idrisForeign = J.Name $ map Ident ["org", "idris", "rts", "ForeignPrimitives"]

@@ -75,10 +144,8 @@ prefixCallNamespacesCase name (SDefaultCase e) = SDefaultCase (prefixCallNamespa

75prefixCallNamespacesDecl :: Ident -> SDecl -> SDecl

144prefixCallNamespacesDecl :: Ident -> SDecl -> SDecl

76prefixCallNamespacesDecl name (SFun fname args i e) = SFun fname args i (prefixCallNamespaces name e)

145prefixCallNamespacesDecl name (SFun fname args i e) = SFun fname args i (prefixCallNamespaces name e)

146

78−mkTypeDecl :: [(Name, SDecl)] ->

147+mkTypeDecl :: [(Name, SExp)] -> [(Name, SDecl)] -> FilePath -> CodeGeneration [TypeDecl]

79− FilePath ->

80− Either String [TypeDecl]

81−mkTypeDecl defs out =

148+mkTypeDecl globalInit defs out =

82 (\ name body -> [ClassTypeDecl $ ClassDecl [ Public

149 (\ name body -> [ClassTypeDecl $ ClassDecl [ Public

83 , Annotation $ SingleElementAnnotation

150 , Annotation $ SingleElementAnnotation

84 (J.Name [Ident "SuppressWarnings"])

151 (J.Name [Ident "SuppressWarnings"])

@@ -91,18 +158,33 @@ mkTypeDecl defs out =

91 body])

158 body])

92 <$> mkClassName out

159 <$> mkClassName out

93 <*> ( mkClassName out

160 <*> ( mkClassName out

94− >>= (\ ident -> mkClassBody (map (second (prefixCallNamespacesDecl ident)) defs))

161+ >>= (\ ident -> mkClassBody globalInit (map (second (prefixCallNamespacesDecl ident)) defs))

95 )

162 )

163

97−mkClassName :: FilePath -> Either String Ident

164+mkClassName :: FilePath -> CodeGeneration Ident

98mkClassName path =

165mkClassName path =

99− left (\ err -> "Parser error in \"" ++ path ++ "\": " ++ (show err))

166+ T.lift $ left (\ err -> "Parser error in \"" ++ path ++ "\": " ++ (show err))

100− (parser ident . takeBaseName $ takeFileName path)

167+ (parser ident . takeBaseName $ takeFileName path)

168+

169+mkClassBody :: [(Name, SExp)] -> [(Name, SDecl)] -> CodeGeneration ClassBody

170+mkClassBody globalInit defs =

171+ (\ globals defs -> ClassBody . (globals++) . addMainMethod . mergeInnerClasses $ defs)

172+ <$> mkGlobalContext globalInit

173+ <*> mapM mkDecl defs

174+

175+mkGlobalContext :: [(Name, SExp)] -> CodeGeneration [Decl]

176+mkGlobalContext [] = return []

177+mkGlobalContext initExps =

178+ (\ exps -> [ MemberDecl $ FieldDecl [Private, Static, Final]

179+ objectArrayType

180+ [VarDecl (VarId $ Ident "globalContext")

181+ (Just . InitArray $ ArrayInit exps)

182+ ]

183+ ]

184+ )

185+ <$> mapM (\ (_, exp) -> InitExp <$> mkExp exp) initExps

101

186

102−mkClassBody :: [(Name, SDecl)] ->

187+

103− Either String ClassBody

104−mkClassBody defs = (ClassBody . addMainMethod . mergeInnerClasses)

105− <$> mapM mkDecl defs

106

188

107addMainMethod :: [Decl] -> [Decl]

189addMainMethod :: [Decl] -> [Decl]

108addMainMethod decls

190addMainMethod decls

@@ -160,17 +242,17 @@ mergeInnerClasses = foldl mergeInner []

160 mergeInner [] decl' = [decl']

242 mergeInner [] decl' = [decl']

161

243

162

244

163−mkIdentifier :: Name -> Either String Ident

245+mkIdentifier :: Name -> CodeGeneration Ident

164mkIdentifier (NS name _) = mkIdentifier name

246mkIdentifier (NS name _) = mkIdentifier name

165mkIdentifier (MN i name) = (\ (Ident x) -> Ident $ x ++ ('_' : show i))

247mkIdentifier (MN i name) = (\ (Ident x) -> Ident $ x ++ ('_' : show i))

166 <$> mkIdentifier (UN name)

248 <$> mkIdentifier (UN name)

167mkIdentifier (UN name) =

249mkIdentifier (UN name) =

168− left (\ err -> "Parser error in \"" ++ name ++ "\": " ++ (show err))

250+ T.lift $ left (\ err -> "Parser error in \"" ++ name ++ "\": " ++ (show err))

169− ( parser ident

251+ ( parser ident

170− . cleanReserved

252+ . cleanReserved

171− . cleanNonLetter

253+ . cleanNonLetter

172− . cleanStart

254+ . cleanStart

173− $ cleanWs False name)

255+ $ cleanWs False name)

174 where

256 where

175 cleanStart (x:xs)

257 cleanStart (x:xs)

176 | isNumber x = '_' : (x:xs)

258 | isNumber x = '_' : (x:xs)

@@ -207,6 +289,7 @@ mkIdentifier (UN name) =

207

289

208

290

209 cleanReserved "param" = "_param"

291 cleanReserved "param" = "_param"

292+ cleanReserved "globalContext" = "_globalContext"

210 cleanReserved "context" = "_context"

293 cleanReserved "context" = "_context"

211 cleanReserved "newcontext" = "_newcontext"

294 cleanReserved "newcontext" = "_newcontext"

212

295

@@ -300,10 +383,13 @@ mkIdentifier (UN name) =

300 cleanReserved "fputStr" = "_fputStr"

383 cleanReserved "fputStr" = "_fputStr"

301 cleanReserved "fileEOF" = "_fileEOF"

384 cleanReserved "fileEOF" = "_fileEOF"

302 cleanReserved "isNull" = "_isNull"

385 cleanReserved "isNull" = "_isNull"

386+ cleanReserved "idris_K" = "_idris_K"

387+ cleanReserved "idris_flipK" = "_idris_flipK"

388+ cleanReserved "idris_assignStack" = "_idris_assignStack"

303

389

304 cleanReserved x = x

390 cleanReserved x = x

305

391

306−mkName :: Name -> Either String J.Name

392+mkName :: Name -> CodeGeneration J.Name

307mkName (NS name nss) = (\ n ns -> J.Name (n:ns))

393mkName (NS name nss) = (\ n ns -> J.Name (n:ns))

308 <$> mkIdentifier name

394 <$> mkIdentifier name

309 <*> mapM (mkIdentifier . UN) nss

395 <*> mapM (mkIdentifier . UN) nss

@@ -330,8 +416,9 @@ idrisTailCallClosureType = ClassType [(Ident "TailCallClosure", [])]

330idrisObjectType :: ClassType

416idrisObjectType :: ClassType

331idrisObjectType = ClassType [(Ident "IdrisObject", [])]

417idrisObjectType = ClassType [(Ident "IdrisObject", [])]

332

418

333−contextArray :: Exp

419+contextArray :: LVar -> Exp

334−contextArray = ExpName $ J.Name [Ident "context"]

420+contextArray (Loc _) = ExpName $ J.Name [Ident "context"]

421+contextArray (Glob _) = ExpName $ J.Name [Ident "globalContext"]

335

422

336charType :: ClassType

423charType :: ClassType

337charType = ClassType [(Ident "Character", [])]

424charType = ClassType [(Ident "Character", [])]

@@ -369,29 +456,38 @@ runtimeExceptionType = ClassType [(Ident "RuntimeException", [])]

369comparableType :: ClassType

456comparableType :: ClassType

370comparableType = ClassType [(Ident "Comparable", [])]

457comparableType = ClassType [(Ident "Comparable", [])]

371

458

372−mkDecl :: (Name, SDecl) ->

459+mkDecl :: (Name, SDecl) -> CodeGeneration Decl

373− Either String Decl

374mkDecl ((NS n (ns:nss)), decl) =

460mkDecl ((NS n (ns:nss)), decl) =

375 (\ name body -> MemberDecl $ MemberClassDecl $ ClassDecl [Public, Static] name [] Nothing [] body)

461 (\ name body -> MemberDecl $ MemberClassDecl $ ClassDecl [Public, Static] name [] Nothing [] body)

376 <$> mkIdentifier (UN ns)

462 <$> mkIdentifier (UN ns)

377− <*> mkClassBody [(NS n nss, decl)]

463+ <*> mkClassBody [] [(NS n nss, decl)]

378mkDecl (_, SFun name params stackSize body) =

464mkDecl (_, SFun name params stackSize body) =

379− (\ name params cont ->

465+ (\ name params paramNames methodBody ->

380 MemberDecl $ MethodDecl [Public, Static]

466 MemberDecl $ MethodDecl [Public, Static]

381 []

467 []

382 (Just . RefType $ ClassRefType objectType)

468 (Just . RefType $ ClassRefType objectType)

383 name

469 name

384 params

470 params

385 []

471 []

386− (MethodBody . Just $ Block [ BlockStmt . Return . Just . MethodInv $

472+ (MethodBody . Just $ Block

387− PrimaryMethodCall cont [] (Ident "call") []])

473+ [ LocalVars [Final]

474+ objectArrayType

475+ [ VarDecl (VarDeclArray . VarId $ Ident "context")

476+ (Just . InitArray . ArrayInit $

477+ paramNames

478+ ++ replicate stackSize (InitExp . Lit $ Null))

479+ ]

480+ , BlockStmt . Return $ Just methodBody

481+ ]

482+ )

388 )

483 )

389 <$> mkIdentifier name

484 <$> mkIdentifier name

390 <*> mapM mkFormalParam params

485 <*> mapM mkFormalParam params

391− <*> mkClosure params stackSize body

486+ <*> mapM (\ p -> (InitExp . ExpName) <$> mkName p) params

487+ <*> mkExp body

392

488

393

489

394−mkClosure :: [Name] -> Int -> SExp -> Either String Exp

490+mkClosure :: [Name] -> Int -> SExp -> CodeGeneration Exp

395mkClosure params stackSize body =

491mkClosure params stackSize body =

396 (\ paramArray body ->

492 (\ paramArray body ->

397 InstanceCreation []

493 InstanceCreation []

@@ -402,126 +498,55 @@ mkClosure params stackSize body =

402 <$> mkStackInit params stackSize

498 <$> mkStackInit params stackSize

403 <*> mkClosureCall body

499 <*> mkClosureCall body

404

500

405−mkFormalParam :: Name -> Either String FormalParam

501+mkFormalParam :: Name -> CodeGeneration FormalParam

406mkFormalParam name =

502mkFormalParam name =

407 (\ name -> FormalParam [Final] (RefType . ClassRefType $ objectType) False (VarId name))

503 (\ name -> FormalParam [Final] (RefType . ClassRefType $ objectType) False (VarId name))

408 <$> mkIdentifier name

504 <$> mkIdentifier name

409

505

410−mkClosureCall :: SExp -> Either String Decl

506+mkClosureCall :: SExp -> CodeGeneration Decl

411mkClosureCall body =

507mkClosureCall body =

412 (\ body -> MemberDecl $ MethodDecl [Public] [] (Just . RefType $ ClassRefType objectType) (Ident "call") [] [] body)

508 (\ body -> MemberDecl $ MethodDecl [Public] [] (Just . RefType $ ClassRefType objectType) (Ident "call") [] [] body)

413 <$> mkMethodBody body

509 <$> mkMethodBody body

414

510

415−mkMethodBody :: SExp -> Either String MethodBody

511+mkMethodBody :: SExp -> CodeGeneration MethodBody

416mkMethodBody exp =

512mkMethodBody exp =

417 (\ exp -> MethodBody . Just . Block $ [BlockStmt . Return . Just $ exp])

513 (\ exp -> MethodBody . Just . Block $ [BlockStmt . Return . Just $ exp])

418 <$> mkExp exp

514 <$> mkExp exp

419

515

420−mkStackInit :: [Name] -> Int -> Either String Exp

516+mkStackInit :: [Name] -> Int -> CodeGeneration Exp

421mkStackInit params stackSize =

517mkStackInit params stackSize =

422 (\ localVars -> ArrayCreateInit objectArrayType 0 . ArrayInit $

518 (\ localVars -> ArrayCreateInit objectArrayType 0 . ArrayInit $

423 (map (InitExp . ExpName) localVars)

519 (map (InitExp . ExpName) localVars)

424 ++ (replicate (stackSize) (InitExp $ Lit Null)))

520 ++ (replicate (stackSize) (InitExp $ Lit Null)))

425 <$> mapM mkName params

521 <$> mapM mkName params

426

522

427−mkAnonymousLetBinding :: LVar -> SExp -> SExp -> Either String Exp

523+mkK :: Exp -> Exp -> Exp

428−mkAnonymousLetBinding var oldExp newExp =

524+mkK result drop =

429− (\ bindingMethod newExp ->

525+ MethodInv $ MethodCall (J.Name [Ident "idris_K"]) [ result, drop ]

430− MethodInv $ PrimaryMethodCall

526+

431− ( MethodInv $ PrimaryMethodCall ( InstanceCreation []

527+mkFlipK :: Exp -> Exp -> Exp

432− objectType

528+mkFlipK drop result =

433− []

529+ MethodInv $ MethodCall (J.Name [Ident "idris_flipK"]) [ drop, result ]

434− (Just $ ClassBody [MemberDecl $ bindingMethod])

530+

435− )

531+mkLet :: LVar -> SExp -> SExp -> CodeGeneration Exp

436− []

532+mkLet (Loc pos) oldExp newExp =

437− (Ident "apply")

533+ (\ oldExp newExp ->

438− [ contextArray

439− , newExp]

440− )

441− []

442− (Ident "call")

443− []

444− )

445− <$> mkLetBindingMethod var oldExp

446− <*> mkExp newExp

447−

448−

449−mkContextParam :: FormalParam

450−mkContextParam =

451− FormalParam [Final] (objectArrayType) False (VarId (Ident "context"))

452−

453−mkLetBindingMethod :: LVar -> SExp -> Either String MemberDecl

454−mkLetBindingMethod (Loc i) oldExp =

455− (\ param bindingStack oldCont ->

456− MethodDecl [Final, Public]

457− []

458− (Just . RefType $ ClassRefType idrisClosureType)

459− (Ident "apply")

460− [mkContextParam, param]

461− []

462− (MethodBody . Just . Block $

463− bindingStack ++ [BlockStmt . Return $ Just oldCont]

464− )

465− )

466− <$> mkFormalParam (UN "param")

467− <*> mkBindingStack True i [UN "param"]

468− <*> mkBindingClosure oldExp

469−

470−mkBindingClosure :: SExp -> Either String Exp

471−mkBindingClosure oldExp =

472− (\ oldCall ->

473− InstanceCreation []

474− idrisClosureType

475− [ ExpName $ J.Name [Ident "new_context"] ]

534+ mkFlipK ( Assign ( ArrayLhs $ ArrayIndex (ExpName $ J.Name [Ident "context"])

476− (Just $ ClassBody [oldCall])

535+ (Lit $ Int (toInteger pos)))

536+ EqualA

537+ newExp

538+ )

539+ oldExp

477 )

540 )

478− <$> mkClosureCall oldExp

541+ <$> mkExp oldExp

479−

542+ <*> mkExp newExp

480−

543+mkLet (Glob _) _ _ = T.lift $ Left "Cannot let bind to global variable"

481−mkBindingStack :: Bool -> Int -> [Name] -> Either String [BlockStmt]

482−mkBindingStack checked parentStackStart params =

483− (\ paramNames ->

484− ( LocalVars [Final]

485− objectArrayType

486− [ VarDecl (VarDeclArray . VarId $ Ident "new_context")

487− (Just . InitExp $ mkContextCopy checked parentStackStart params)

488− ])

489− : ( map (\ (param, pos) ->

490− BlockStmt . ExpStmt $

491− Assign (ArrayLhs $ ArrayIndex (ExpName $ J.Name [Ident "new_context"])

492− (Lit $ Int (toInteger pos)))

493− EqualA

494− (ExpName param)) $ zip paramNames [parentStackStart..]

495− )

496− )

497− <$> mapM mkName params

498

544

499−mkContextCopy :: Bool -> Int -> [Name] -> Exp

500−mkContextCopy True parentStackStart params =

501− MethodInv $ PrimaryMethodCall (ExpName $ J.Name [Ident "context"])

502− []

503− (Ident "clone")

504− []

505−mkContextCopy False parentStackStart params =

506− MethodInv $ TypeMethodCall (J.Name [Ident "Arrays"])

507− []

508− (Ident "copyOf")

509− [ ExpName $ J.Name [Ident "context"]

510− , MethodInv

511− $ TypeMethodCall (J.Name [Ident "Math"])

512− []

513− (Ident "max")

514− [ FieldAccess $ PrimaryFieldAccess (ExpName $ J.Name [Ident "context"])

515− (Ident "length")

516− , Lit . Int $ toInteger (parentStackStart + length params)

517− ]

518− ]

519−

520reverseNameSpace :: J.Name -> J.Name

545reverseNameSpace :: J.Name -> J.Name

521reverseNameSpace (J.Name ids) =

546reverseNameSpace (J.Name ids) =

522 J.Name ((tail ids) ++ [head ids])

547 J.Name ((tail ids) ++ [head ids])

523

548

524−mkCase :: Bool -> LVar -> [SAlt] -> Either String Exp

549+mkCase :: Bool -> LVar -> [SAlt] -> CodeGeneration Exp

525mkCase checked var ((SConCase parentStackPos consIndex _ params branchExpression):cases) =

550mkCase checked var ((SConCase parentStackPos consIndex _ params branchExpression):cases) =

526 mkConsCase checked

551 mkConsCase checked

527 var

552 var

@@ -531,11 +556,11 @@ mkCase checked var ((SConCase parentStackPos consIndex _ params branchExpression

531 branchExpression

556 branchExpression

532 (SCase var cases)

557 (SCase var cases)

533mkCase checked var (c@(SConstCase constant branchExpression):cases) =

558mkCase checked var (c@(SConstCase constant branchExpression):cases) =

534− (\ constant branchExpression alternative ->

559+ (\ constant branchExpression alternative var->

535 Cond ( MethodInv $ PrimaryMethodCall (constant)

560 Cond ( MethodInv $ PrimaryMethodCall (constant)

536 []

561 []

537 (Ident "equals")

562 (Ident "equals")

538− [mkVarAccess Nothing var]

563+ [var]

539 )

564 )

540 branchExpression

565 branchExpression

541 alternative

566 alternative

@@ -543,10 +568,11 @@ mkCase checked var (c@(SConstCase constant branchExpression):cases) =

543 <$> mkExp (SConst constant)

568 <$> mkExp (SConst constant)

544 <*> mkExp branchExpression

569 <*> mkExp branchExpression

545 <*> mkCase checked var cases

570 <*> mkCase checked var cases

571+ <*> mkVarAccess Nothing var

546mkCase checked var (SDefaultCase exp:cases) = mkExp exp

572mkCase checked var (SDefaultCase exp:cases) = mkExp exp

547mkCase checked _ [] = mkExp (SError "Non-exhaustive pattern")

573mkCase checked _ [] = mkExp (SError "Non-exhaustive pattern")

548

574

549−mkConsCase :: Bool -> LVar -> Int -> Int -> [Name] -> SExp -> SExp -> Either String Exp

575+mkConsCase :: Bool -> LVar -> Int -> Int -> [Name] -> SExp -> SExp -> CodeGeneration Exp

550mkConsCase checked

576mkConsCase checked

551 toDeconstruct

577 toDeconstruct

552 parentStackStart

578 parentStackStart

@@ -554,13 +580,13 @@ mkConsCase checked

554 params

580 params

555 branchExpression

581 branchExpression

556 alternative =

582 alternative =

557− (\ caseBinding alternative->

583+ (\ caseBinding alternative var varCasted->

558− Cond (BinOp (InstanceOf (mkVarAccess Nothing toDeconstruct)

584+ Cond (BinOp (InstanceOf (var)

559 (ClassRefType idrisObjectType)

585 (ClassRefType idrisObjectType)

560 )

586 )

561 CAnd

587 CAnd

562 ( BinOp

588 ( BinOp

563− ( MethodInv $ PrimaryMethodCall (mkVarAccess (Just idrisObjectType) toDeconstruct)

589+ ( MethodInv $ PrimaryMethodCall (varCasted)

564 []

590 []

565 (Ident "getConstructorId")

591 (Ident "getConstructorId")

566 []

592 []

@@ -574,11 +600,24 @@ mkConsCase checked

574 )

600 )

575 <$> mkCaseBinding checked toDeconstruct parentStackStart params branchExpression

601 <$> mkCaseBinding checked toDeconstruct parentStackStart params branchExpression

576 <*> mkExp alternative

602 <*> mkExp alternative

577−

603+ <*> mkVarAccess (Nothing) toDeconstruct

578−

604+ <*> mkVarAccess (Just idrisObjectType) toDeconstruct

605+

606+

579−mkCaseBinding :: Bool -> LVar -> Int -> [Name] -> SExp -> Either String Exp

607+mkCaseBinding :: Bool -> LVar -> Int -> [Name] -> SExp -> CodeGeneration Exp

608+mkCaseBinding True var parentStackStart params branchExpression =

609+ (\ branchExpression deconstruction ->

610+ mkFlipK (MethodInv $ MethodCall (J.Name [Ident "idris_assignStack"])

611+ ( (ExpName $ J.Name [Ident "context"])

612+ : (Lit $ Int (toInteger parentStackStart))

613+ : deconstruction

614+ ))

615+ (branchExpression)

616+ )

617+ <$> mkExp branchExpression

618+ <*> mkCaseBindingDeconstruction var params

580−mkCaseBinding checked var parentStackStart params branchExpression =

619+mkCaseBinding False var parentStackStart params branchExpression =

581− (\ bindingMethod ->

620+ (\ bindingMethod deconstruction ->

582 MethodInv $ PrimaryMethodCall

621 MethodInv $ PrimaryMethodCall

583 ( MethodInv $ PrimaryMethodCall (InstanceCreation []

622 ( MethodInv $ PrimaryMethodCall (InstanceCreation []

584 (ClassType [(Ident "Object", [])])

623 (ClassType [(Ident "Object", [])])

@@ -587,20 +626,21 @@ mkCaseBinding checked var parentStackStart params branchExpression =

587 )

626 )

588 []

627 []

589 (Ident "apply")

628 (Ident "apply")

590− ( contextArray

629+ ( contextArray (Loc undefined) : deconstruction )

591− : (mkCaseBindingDeconstruction var params)

592− )

593 )

630 )

594 []

631 []

595 (Ident "call")

632 (Ident "call")

596 []

633 []

597 )

634 )

598− <$> mkCaseBindingMethod checked parentStackStart params branchExpression

635+ <$> mkCaseBindingMethod parentStackStart params branchExpression

599−

636+ <*> mkCaseBindingDeconstruction var params

600

637

638+mkCaseBindingDeconstruction :: LVar -> [Name] -> CodeGeneration [Exp]

639+mkCaseBindingDeconstruction var members =

640+ mapM (mkProjection var) ([0..(length members - 1)])

601

641

602−mkCaseBindingMethod :: Bool -> Int -> [Name] -> SExp -> Either String MemberDecl

642+mkCaseBindingMethod :: Int -> [Name] -> SExp -> CodeGeneration MemberDecl

603−mkCaseBindingMethod checked parentStackStart params branchExpression =

643+mkCaseBindingMethod parentStackStart params branchExpression =

604 (\ formalParams caseBindingStack branchExpression ->

644 (\ formalParams caseBindingStack branchExpression ->

605 MethodDecl [Final, Public]

645 MethodDecl [Final, Public]

606 []

646 []

@@ -612,22 +652,74 @@ mkCaseBindingMethod checked parentStackStart params branchExpression =

612 caseBindingStack ++

652 caseBindingStack ++

613 [BlockStmt . Return $ Just branchExpression]))

653 [BlockStmt . Return $ Just branchExpression]))

614 <$> mapM mkFormalParam params

654 <$> mapM mkFormalParam params

615− <*> mkBindingStack checked parentStackStart params

655+ <*> mkBindingStack False parentStackStart params

616 <*> mkBindingClosure branchExpression

656 <*> mkBindingClosure branchExpression

617

657

618−mkCaseBindingDeconstruction :: LVar -> [Name] -> [Exp]

658+mkContextParam :: FormalParam

619−mkCaseBindingDeconstruction var members =

659+mkContextParam =

620− map (mkProjection var) ([0..(length members - 1)])

660+ FormalParam [Final] (objectArrayType) False (VarId (Ident "context"))

661+

662+mkBindingClosure :: SExp -> CodeGeneration Exp

663+mkBindingClosure oldExp =

664+ (\ oldCall ->

665+ InstanceCreation []

666+ idrisClosureType

667+ [ ExpName $ J.Name [Ident "new_context"] ]

668+ (Just $ ClassBody [oldCall])

669+ )

670+ <$> mkClosureCall oldExp

671+

672+

673+mkBindingStack :: Bool -> Int -> [Name] -> CodeGeneration [BlockStmt]

674+mkBindingStack checked parentStackStart params =

675+ (\ paramNames ->

676+ ( LocalVars [Final]

677+ objectArrayType

678+ [ VarDecl (VarDeclArray . VarId $ Ident "new_context")

679+ (Just . InitExp $ mkContextCopy checked parentStackStart params)

680+ ])

681+ : ( map (\ (param, pos) ->

682+ BlockStmt . ExpStmt $

683+ Assign (ArrayLhs $ ArrayIndex (ExpName $ J.Name [Ident "new_context"])

684+ (Lit $ Int (toInteger pos)))

685+ EqualA

686+ (ExpName param)) $ zip paramNames [parentStackStart..]

687+ )

688+ )

689+ <$> mapM mkName params

621

690

691+mkContextCopy :: Bool -> Int -> [Name] -> Exp

692+mkContextCopy True parentStackStart params =

693+ MethodInv $ PrimaryMethodCall (ExpName $ J.Name [Ident "context"])

694+ []

695+ (Ident "clone")

696+ []

697+mkContextCopy False parentStackStart params =

698+ MethodInv $ TypeMethodCall (J.Name [Ident "Arrays"])

699+ []

700+ (Ident "copyOf")

701+ [ ExpName $ J.Name [Ident "context"]

702+ , MethodInv

703+ $ TypeMethodCall (J.Name [Ident "Math"])

704+ []

705+ (Ident "max")

706+ [ FieldAccess $ PrimaryFieldAccess (ExpName $ J.Name [Ident "context"])

707+ (Ident "length")

708+ , Lit . Int $ toInteger (parentStackStart + length params)

709+ ]

710+ ]

711+

622−mkProjection :: LVar -> Int -> Exp

712+mkProjection :: LVar -> Int -> CodeGeneration Exp

623mkProjection var memberNr =

713mkProjection var memberNr =

624− ArrayAccess $ ArrayIndex ( MethodInv $ PrimaryMethodCall

714+ (\ var -> ArrayAccess $ ArrayIndex ( MethodInv $ PrimaryMethodCall

625− (mkVarAccess (Just idrisObjectType) var)

715+ (var)

626− []

716+ []

627− (Ident "getData")

717+ (Ident "getData")

628− []

718+ []

629− )

719+ )

630− (Lit $ Int (toInteger memberNr))

720+ (Lit $ Int (toInteger memberNr))

721+ )

722+ <$> mkVarAccess (Just idrisObjectType) var

631

723

632type ClassName = String

724type ClassName = String

633

725

@@ -642,22 +734,22 @@ mkClass :: ClassType -> Exp

642mkClass classType =

734mkClass classType =

643 ClassLit . Just . RefType .ClassRefType $ classType

735 ClassLit . Just . RefType .ClassRefType $ classType

644

736

645−mkBinOpExp :: ClassType -> Op -> [LVar] -> Exp

737+mkBinOpExp :: ClassType -> Op -> [LVar] -> CodeGeneration Exp

646−mkBinOpExp castTo op (var:vars) =

738+mkBinOpExp castTo op (var:vars) = do

739+ start <- mkVarAccess (Just castTo) var

740+ foldM (\ exp var -> BinOp exp op <$> mkVarAccess (Just castTo) var) start vars

741+

742+mkBinOpExpTrans :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> Op -> [LVar] -> CodeGeneration Exp

743+mkBinOpExpTrans opTransformation resultTransformation castTo op (var:vars) = do

744+ start <- (mkVarAccess (Just castTo) var)

745+ foldM (\ exp var -> resultTransformation

746+ . BinOp (opTransformation exp) op

747+ . opTransformation

647− foldl (\ exp -> BinOp exp op . mkVarAccess (Just castTo))

748+ <$> mkVarAccess (Just castTo) var)

648− (mkVarAccess (Just castTo) var)

749+ start

649 vars

750 vars

650

751

651−mkBinOpExpTrans :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> Op -> [LVar] -> Exp

652−mkBinOpExpTrans opTransformation resultTransformation castTo op (var:vars) =

653− foldl (\ exp -> resultTransformation

654− . BinOp (opTransformation exp) op

655− . opTransformation

656− . mkVarAccess (Just castTo))

657− (mkVarAccess (Just castTo) var)

658− vars

659−

660−mkBinOpExpConv :: String -> PrimType -> ClassType -> Op -> [LVar] -> Exp

752+mkBinOpExpConv :: String -> PrimType -> ClassType -> Op -> [LVar] -> CodeGeneration Exp

661mkBinOpExpConv fromMethodName toType fromType@(ClassType [(cls@(Ident _), [])]) op args =

753mkBinOpExpConv fromMethodName toType fromType@(ClassType [(cls@(Ident _), [])]) op args =

662 mkBinOpExpTrans (\ exp -> MethodInv $ TypeMethodCall (J.Name [cls])

754 mkBinOpExpTrans (\ exp -> MethodInv $ TypeMethodCall (J.Name [cls])

663 []

755 []

@@ -673,59 +765,70 @@ mkBinOpExpConv fromMethodName toType fromType@(ClassType [(cls@(Ident _), [])])

673 op

765 op

674 args

766 args

675

767

676−mkLogicalBinOpExp :: ClassType -> Op -> [LVar] -> Exp

768+mkLogicalBinOpExp :: ClassType -> Op -> [LVar] -> CodeGeneration Exp

677−mkLogicalBinOpExp castTo op (var:vars) =

769+mkLogicalBinOpExp castTo op (var:vars) = do

770+ start <- mkVarAccess (Just castTo) var

678− foldl (\ exp -> mkBoolToNumber castTo . BinOp exp op . mkVarAccess (Just castTo))

771+ foldM (\ exp var -> mkBoolToNumber castTo . BinOp exp op <$> mkVarAccess (Just castTo) var)

679− (mkVarAccess (Just castTo) var)

772+ start

680 vars

773 vars

681

774

682−mkMethodOpChain1 :: (Exp -> Exp) -> ClassType -> String -> [LVar] -> Exp

775+mkMethodOpChain1 :: (Exp -> Exp) -> ClassType -> String -> [LVar] -> CodeGeneration Exp

683mkMethodOpChain1 = mkMethodOpChain id

776mkMethodOpChain1 = mkMethodOpChain id

684

777

685−mkMethodOpChain :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> String -> [LVar] -> Exp

778+mkMethodOpChain :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> String -> [LVar] -> CodeGeneration Exp

686−mkMethodOpChain initialTransformation resultTransformation castTo method (arg:args) =

779+mkMethodOpChain initialTransformation resultTransformation castTo method (arg:args) = do

780+ start <- initialTransformation <$> mkVarAccess (Just $ castTo) arg

687− foldl (\ exp arg' ->

781+ foldM (\ exp arg' ->

688− resultTransformation . MethodInv $ PrimaryMethodCall exp

782+ resultTransformation

689− []

783+ . MethodInv

690− (Ident method)

784+ . PrimaryMethodCall exp [] (Ident method)

785+ . (:[])

691− [mkVarAccess (Just $ castTo) arg']

786+ <$> mkVarAccess (Just $ castTo) arg'

692 )

787 )

693− (initialTransformation (mkVarAccess (Just $ castTo) arg))

788+ start

694 args

789 args

695

790

696mkBoolToNumber :: ClassType -> Exp -> Exp

791mkBoolToNumber :: ClassType -> Exp -> Exp

697mkBoolToNumber (ClassType [(Ident name, [])]) boolExp =

792mkBoolToNumber (ClassType [(Ident name, [])]) boolExp =

698 Cond boolExp (mkPrimitive name (Int 1)) (mkPrimitive name (Int 0))

793 Cond boolExp (mkPrimitive name (Int 1)) (mkPrimitive name (Int 0))

699

794

700−mkZeroExt :: String -> Int -> ClassType -> ClassType -> LVar -> Exp

795+mkZeroExt :: String -> Int -> ClassType -> ClassType -> LVar -> CodeGeneration Exp

701−mkZeroExt toMethod bits fromType toType@(ClassType [(toTypeName, [])]) var =

796+mkZeroExt toMethod bits fromType toType@(ClassType [(toTypeName, [])]) var = do

797+ (\ var sext ->

702− MethodInv $ TypeMethodCall (J.Name [toTypeName])

798+ MethodInv $ TypeMethodCall (J.Name [toTypeName])

703− []

799+ []

704− (Ident "valueOf")

800+ (Ident "valueOf")

705− [ Cond ( BinOp (mkVarAccess (Just $ fromType) var)

801+ [ Cond ( BinOp (var)

706− LThan

802+ LThan

707− (Lit $ Int 0)

803+ (Lit $ Int 0)

708− )

804+ )

709− ( BinOp (Lit $ Int (2^bits))

805+ ( BinOp (Lit $ Int (2^bits))

710− Add

806+ Add

711− (mkSignedExt' toMethod fromType var)

807+ (sext)

712− )

808+ )

809+ sext

810+ ]

811+ )

812+ <$> mkVarAccess (Just $ fromType) var

713− (mkSignedExt' toMethod fromType var)

813+ <*> mkSignedExt' toMethod fromType var

714− ]

715

814

716−mkSignedExt :: String -> ClassType -> ClassType -> LVar -> Exp

815+mkSignedExt :: String -> ClassType -> ClassType -> LVar -> CodeGeneration Exp

717mkSignedExt toMethod fromType (ClassType [(toTypeName, [])]) var =

816mkSignedExt toMethod fromType (ClassType [(toTypeName, [])]) var =

718− MethodInv $ TypeMethodCall (J.Name [toTypeName])

817+ (\ sext -> MethodInv $ TypeMethodCall (J.Name [toTypeName])

719− []

818+ []

720− (Ident "valueOf")

819+ (Ident "valueOf")

820+ [ sext ]

821+ )

721− [ mkSignedExt' toMethod fromType var ]

822+ <$> mkSignedExt' toMethod fromType var

722

823

723−mkSignedExt' :: String -> ClassType -> LVar -> Exp

824+mkSignedExt' :: String -> ClassType -> LVar -> CodeGeneration Exp

724mkSignedExt' toMethod fromType var =

825mkSignedExt' toMethod fromType var =

826+ (\ var -> MethodInv $ PrimaryMethodCall (var)

827+ []

828+ (Ident toMethod)

829+ []

830+ )

725− MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ fromType) var)

831+ <$> mkVarAccess (Just $ fromType) var

726− []

727− (Ident toMethod)

728− []

729

832

730data SPartialOrder

833data SPartialOrder

731 = SLt

834 = SLt

@@ -747,26 +850,39 @@ mkPartialOrder SGe x =

747 (BinOp (Lit $ Int 0) Equal x)

850 (BinOp (Lit $ Int 0) Equal x)

748mkPartialOrder SGt x = (BinOp (Lit $ Int 1) Equal x)

851mkPartialOrder SGt x = (BinOp (Lit $ Int 1) Equal x)

749

852

853+varPos :: LVar -> CodeGeneration Integer

854+varPos (Loc i) = return (toInteger i)

855+varPos (Glob name) = do

856+ positions <- globalVariablePositions <$> get

857+ case lookup name positions of

858+ (Just pos) -> return pos

859+ Nothing -> T.lift . Left $ "Invalid global variable id: " ++ show name

860+

750−mkVarAccess :: Maybe ClassType -> LVar -> Exp

861+mkVarAccess :: Maybe ClassType -> LVar -> CodeGeneration Exp

751−mkVarAccess Nothing (Loc i) =

862+mkVarAccess Nothing var =

752− ArrayAccess $ ArrayIndex contextArray (Lit $ Int (toInteger i))

863+ (\ pos -> ArrayAccess $ ArrayIndex (contextArray var) (Lit $ Int pos))

864+ <$> varPos var

753mkVarAccess (Just castTo) var =

865mkVarAccess (Just castTo) var =

754− Cast (RefType . ClassRefType $ castTo) (mkVarAccess Nothing var)

866+ Cast (RefType . ClassRefType $ castTo) <$> (mkVarAccess Nothing var)

755

867

756−mkPrimitiveCast :: ClassType -> ClassType -> LVar -> Exp

868+mkPrimitiveCast :: ClassType -> ClassType -> LVar -> CodeGeneration Exp

757mkPrimitiveCast fromType (ClassType [(toType, [])]) var =

869mkPrimitiveCast fromType (ClassType [(toType, [])]) var =

870+ (\ var ->

758− MethodInv $ TypeMethodCall (J.Name [toType])

871+ MethodInv $ TypeMethodCall (J.Name [toType])

759− []

760− (Ident "valueOf")

761− [mkVarAccess (Just fromType) var]

762−

763−mkToString :: ClassType -> LVar -> Exp

764−mkToString castTo var =

765− MethodInv $ PrimaryMethodCall (mkVarAccess (Just castTo) var)

766− []

767− (Ident "toString")

768 []

872 []

873+ (Ident "valueOf")

874+ [var]

875+ )

876+ <$> mkVarAccess (Just fromType) var

769

877

878+mkToString :: ClassType -> LVar -> CodeGeneration Exp

879+mkToString castTo var =

880+ (\ var -> MethodInv $ PrimaryMethodCall (var)

881+ []

882+ (Ident "toString")

883+ []

884+ )

885+ <$> mkVarAccess (Just castTo) var

770data Std = In | Out | Err

886data Std = In | Out | Err

771

887

772instance Show Std where

888instance Show Std where

@@ -784,49 +900,57 @@ mkSystemOutPrint value =

784 (Ident "print")

900 (Ident "print")

785 [value]

901 [value]

786

902

787−mkMathFun :: String -> LVar -> Exp

903+mkMathFun :: String -> LVar -> CodeGeneration Exp

788mkMathFun funName var =

904mkMathFun funName var =

789− MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

905+ (\ var -> MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

790− []

906+ []

791− (Ident "valueOf")

907+ (Ident "valueOf")

792− [ MethodInv $ TypeMethodCall (J.Name [Ident "Math"])

908+ [ MethodInv $ TypeMethodCall (J.Name [Ident "Math"])

793− []

909+ []

794− (Ident funName)

910+ (Ident funName)

911+ [var]

912+ ]

913+ )

795− [mkVarAccess (Just doubleType) var]

914+ <$> mkVarAccess (Just doubleType) var

796− ]

797

915

798−mkStringAtIndex :: LVar -> Exp -> Exp

916+mkStringAtIndex :: LVar -> Exp -> CodeGeneration Exp

799mkStringAtIndex var indexExp =

917mkStringAtIndex var indexExp =

800− MethodInv $ TypeMethodCall (J.Name [Ident "Integer"])

918+ (\ var -> MethodInv $ TypeMethodCall (J.Name [Ident "Integer"])

801− []

919+ []

802− (Ident "valueOf")

920+ (Ident "valueOf")

921+ [ MethodInv $ PrimaryMethodCall (var)

922+ []

923+ (Ident "charAt")

924+ [indexExp]

925+ ]

926+ )

803− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) var)

927+ <$> mkVarAccess (Just stringType) var

804− []

805− (Ident "charAt")

806− [indexExp]

807− ]

808

928

809mkForeignType :: FType -> Maybe ClassType

929mkForeignType :: FType -> Maybe ClassType

810−mkForeignType FInt = return $ integerType

930+mkForeignType FInt = return integerType

811−mkForeignType FChar = return $ integerType

931+mkForeignType FChar = return integerType

812−mkForeignType FString = return $ stringType

932+mkForeignType FString = return stringType

813−mkForeignType FPtr = return $ objectType

933+mkForeignType FPtr = return objectType

814−mkForeignType FDouble = return $ doubleType

934+mkForeignType FDouble = return doubleType

815−mkForeignType FAny = return $ objectType

935+mkForeignType FAny = return objectType

816mkForeignType FUnit = Nothing

936mkForeignType FUnit = Nothing

817

937

818−mkForeignVarAccess :: FType -> LVar -> Exp

938+mkForeignVarAccess :: FType -> LVar -> CodeGeneration Exp

819mkForeignVarAccess FInt var =

939mkForeignVarAccess FInt var =

940+ (\ var -> MethodInv $ PrimaryMethodCall (var)

941+ []

942+ (Ident "intValue")

943+ []

944+ )

820− MethodInv $ PrimaryMethodCall (mkVarAccess (Just integerType) var)

945+ <$> mkVarAccess (Just integerType) var

821− []

822− (Ident "intValue")

823− []

824−mkForeignVarAccess FChar var = Cast (PrimType CharT) (mkForeignVarAccess FInt var)

946+mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess FInt var

825mkForeignVarAccess FDouble var =

947mkForeignVarAccess FDouble var =

948+ (\ var -> MethodInv $ PrimaryMethodCall (var)

949+ []

950+ (Ident "doubleValue")

951+ []

952+ )

826− MethodInv $ PrimaryMethodCall (mkVarAccess (Just doubleType) var)

953+ <$> mkVarAccess (Just doubleType) var

827− []

828− (Ident "doubleValue")

829− []

830mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

954mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

831

955

832mkFromForeignType :: FType -> Exp -> Exp

956mkFromForeignType :: FType -> Exp -> Exp

@@ -843,7 +967,7 @@ mkFromForeignType FDouble from =

843 [from]

967 [from]

844mkFromForeignType _ from = from

968mkFromForeignType _ from = from

845

969

846−mkForeignInvoke :: FType -> String -> [(FType, LVar)] -> Either String Exp

970+mkForeignInvoke :: FType -> String -> [(FType, LVar)] -> CodeGeneration Exp

847mkForeignInvoke fType method args =

971mkForeignInvoke fType method args =

848 (\ foreignInvokeMeth ->

972 (\ foreignInvokeMeth ->

849 MethodInv $ PrimaryMethodCall (InstanceCreation []

973 MethodInv $ PrimaryMethodCall (InstanceCreation []

@@ -858,7 +982,7 @@ mkForeignInvoke fType method args =

858 <$> mkForeignInvokeMethod fType method args

982 <$> mkForeignInvokeMethod fType method args

859

983

860

984

861−mkForeignInvokeMethod :: FType -> String -> [(FType, LVar)] -> Either String MemberDecl

985+mkForeignInvokeMethod :: FType -> String -> [(FType, LVar)] -> CodeGeneration MemberDecl

862mkForeignInvokeMethod fType method args =

986mkForeignInvokeMethod fType method args =

863 (\ tryBlock ->

987 (\ tryBlock ->

864 MethodDecl [Public, Final]

988 MethodDecl [Public, Final]

@@ -867,111 +991,124 @@ mkForeignInvokeMethod fType method args =

867 (Ident "foreignInvoke")

991 (Ident "foreignInvoke")

868 []

992 []

869 []

993 []

870− (MethodBody . Just $ Block [ BlockStmt $

994+ (MethodBody . Just $ Block

995+ [ BlockStmt

871− Try tryBlock

996+ $ Try tryBlock

872− [ Catch (FormalParam []

997+ [ Catch (FormalParam []

873− (RefType $ ClassRefType exceptionType)

998+ (RefType $ ClassRefType exceptionType)

874− False

999+ False

875− (VarId $ Ident "ex")

1000+ (VarId $ Ident "ex")

876− )

1001+ )

877− (Block [ BlockStmt . Throw $

1002+ (Block [ BlockStmt

1003+ . Throw

878− InstanceCreation []

1004+ $ InstanceCreation []

879− runtimeExceptionType

1005+ runtimeExceptionType

880− [ExpName $ J.Name [Ident "ex"]]

1006+ [ExpName $ J.Name [Ident "ex"]]

881− Nothing

1007+ Nothing

882− ]

1008+ ]

883− )

1009+ )

884− ]

1010+ ]

885− Nothing

1011+ Nothing

886− ]

1012+ ]

887 )

1013 )

888− )

1014+ )

889 <$> mkForeignInvokeTryBlock fType method args

1015 <$> mkForeignInvokeTryBlock fType method args

890

1016

891

1017

892−mkForeignInvokeTryBlock :: FType -> String -> [(FType, LVar)] -> Either String Block

1018+mkForeignInvokeTryBlock :: FType -> String -> [(FType, LVar)] -> CodeGeneration Block

893mkForeignInvokeTryBlock FUnit method args =

1019mkForeignInvokeTryBlock FUnit method args =

894− (\ method -> Block [ BlockStmt . ExpStmt . MethodInv $

1020+ (\ method args -> Block [ BlockStmt . ExpStmt . MethodInv $ MethodCall method args

895− MethodCall method

896− (map (uncurry mkForeignVarAccess) args)

897− , BlockStmt $ Return (Just $ Lit Null)

1021+ , BlockStmt $ Return (Just $ Lit Null)

898− ]

1022+ ]

899 )

1023 )

900− <$> ( left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

1024+ <$> ( T.lift $ left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

901− (parser name method)

1025+ (parser name method)

902 )

1026 )

1027+ <*> mapM (uncurry mkForeignVarAccess) args

903mkForeignInvokeTryBlock fType method args =

1028mkForeignInvokeTryBlock fType method args =

904− (\ method -> Block [ BlockStmt . Return

1029+ (\ method args -> Block [ BlockStmt . Return

905 . Just

1030 . Just

906 . mkFromForeignType fType

1031 . mkFromForeignType fType

907− . MethodInv $

1032+ . MethodInv

908− MethodCall method

1033+ $ MethodCall method args

909− (map (uncurry mkForeignVarAccess) args)

910− ]

1034+ ]

911 )

1035 )

912− <$> ( left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

1036+ <$> ( T.lift $ left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

913− (parser name method)

1037+ (parser name method)

914 )

1038 )

1039+ <*> mapM (uncurry mkForeignVarAccess) args

915

1040

916−mkMethodClosure :: Name -> [LVar] -> Either String Exp

1041+mkMethodClosure :: Name -> [LVar] -> CodeGeneration Exp

917mkMethodClosure name args =

1042mkMethodClosure name args =

918 (\ name args ->

1043 (\ name args ->

919 InstanceCreation []

1044 InstanceCreation []

920 idrisClosureType

1045 idrisClosureType

921 [ (ExpName $ J.Name [Ident "context"]) ]

1046 [ (ExpName $ J.Name [Ident "context"]) ]

1047+ ( Just

922− ( Just $ ClassBody

1048+ $ ClassBody

923− [ MemberDecl $

1049+ [ MemberDecl

924− MethodDecl [Public, Final]

1050+ $ MethodDecl [Public, Final]

925− []

1051+ []

926− (Just . RefType $ ClassRefType objectType)

1052+ (Just . RefType $ ClassRefType objectType)

927− (Ident "call")

1053+ (Ident "call")

928− []

1054+ []

929− []

1055+ []

930− ( MethodBody . Just $

1056+ ( MethodBody

1057+ . Just

931− Block [ BlockStmt . Return . Just . MethodInv $

1058+ $ Block [ BlockStmt

1059+ . Return

1060+ . Just

1061+ . MethodInv

932− MethodCall (reverseNameSpace name)

1062+ $ MethodCall (reverseNameSpace name)

933− args

1063+ args

934− ]

1064+ ]

935− )

1065+ )

936− ]

1066+ ]

937− )

1067+ )

938 )

1068 )

939 <$> mkName name

1069 <$> mkName name

940 <*> mapM (mkExp . SV) args

1070 <*> mapM (mkExp . SV) args

941

1071

942−mkThread :: LVar -> Either String Exp

1072+mkThread :: LVar -> CodeGeneration Exp

943mkThread arg =

1073mkThread arg =

1074+ (\ eval ->

944− (\ eval -> MethodInv $

1075+ MethodInv

945− PrimaryMethodCall (InstanceCreation []

1076+ $ PrimaryMethodCall (InstanceCreation []

946− (ClassType [(Ident "Thread", [])])

1077+ (ClassType [(Ident "Thread", [])])

947− [ eval ]

1078+ [ eval ]

1079+ ( Just

948− ( Just $ ClassBody

1080+ $ ClassBody [ MemberDecl

949− [ MemberDecl $ MethodDecl

950− [Public, Final]

1081+ $ MethodDecl [Public, Final]

951− []

1082+ []

952− (Just . RefType $ ClassRefType objectType)

1083+ (Just . RefType $ ClassRefType objectType)

953− (Ident "_start")

1084+ (Ident "_start")

954− []

1085+ []

955− []

1086+ []

956− ( MethodBody . Just $ Block

1087+ ( MethodBody

1088+ . Just

1089+ $ Block [ BlockStmt

1090+ . ExpStmt

957− [ BlockStmt . ExpStmt . MethodInv $ MethodCall

1091+ . MethodInv

958− (J.Name [Ident "start"])

1092+ $ MethodCall (J.Name [Ident "start"])

959− []

1093+ []

960− , BlockStmt . Return . Just $ This

1094+ , BlockStmt

1095+ . Return

1096+ . Just

1097+ $ This

961 ]

1098 ]

962− )

1099+ )

963− ]

1100+ ]

964− )

1101+ )

965− )

1102+ )

966− []

1103+ []

967− (Ident "_start")

1104+ (Ident "_start")

968− []

1105+ []

969 )

1106 )

970 <$> mkThreadBinding arg

1107 <$> mkThreadBinding arg

971

1108

972−mkThreadBinding :: LVar -> Either String Exp

1109+mkThreadBinding :: LVar -> CodeGeneration Exp

973mkThreadBinding var =

1110mkThreadBinding var =

974− (\ bindingMethod ->

1111+ (\ bindingMethod var ->

975 MethodInv $ PrimaryMethodCall ( InstanceCreation []

1112 MethodInv $ PrimaryMethodCall ( InstanceCreation []

976 objectType

1113 objectType

977 []

1114 []

@@ -979,12 +1116,13 @@ mkThreadBinding var =

979 )

1116 )

980 []

1117 []

981 (Ident "apply")

1118 (Ident "apply")

982− [ mkVarAccess Nothing var ]

1119+ [ var ]

983− )

1120+ )

984 <$> mkThreadBindingMethod

1121 <$> mkThreadBindingMethod

1122+ <*> mkVarAccess Nothing var

985

1123

986

1124

987−mkThreadBindingMethod :: Either String MemberDecl

1125+mkThreadBindingMethod :: CodeGeneration MemberDecl

988mkThreadBindingMethod =

1126mkThreadBindingMethod =

989 (\ compute ->

1127 (\ compute ->

990 MethodDecl [Final, Public]

1128 MethodDecl [Final, Public]

@@ -1011,9 +1149,8 @@ mkThreadBindingStack =

1011 ]

1149 ]

1012

1150

1013

1151

1014−mkExp :: SExp -> Either String Exp

1152+mkExp :: SExp -> CodeGeneration Exp

1015−mkExp (SV var) =

1016− return $ mkVarAccess Nothing var

1153+mkExp (SV var) = mkVarAccess Nothing var

1017mkExp (SApp False name args) =

1154mkExp (SApp False name args) =

1018 (\ methClosure ->

1155 (\ methClosure ->

1019 MethodInv $ PrimaryMethodCall ( InstanceCreation []

1156 MethodInv $ PrimaryMethodCall ( InstanceCreation []

@@ -1036,12 +1173,14 @@ mkExp (SApp True name args) =

1036 )

1173 )

1037 <$> mkMethodClosure name args

1174 <$> mkMethodClosure name args

1038mkExp (SLet var new old) =

1175mkExp (SLet var new old) =

1039− mkAnonymousLetBinding var old new

1176+ mkLet var old new

1040−mkExp (SUpdate (Loc i) exp) =

1177+mkExp (SUpdate var exp) =

1041− (\ rhs -> Assign (ArrayLhs $ ArrayIndex (contextArray) (Lit $ Int (toInteger i)))

1178+ (\ rhs varPos -> Assign (ArrayLhs $ ArrayIndex (contextArray var) (Lit $ Int varPos))

1042− EqualA

1179+ EqualA

1043− rhs)

1180+ rhs

1181+ )

1044 <$> mkExp exp

1182 <$> mkExp exp

1183+ <*> varPos var

1045mkExp (SCon conId name args) =

1184mkExp (SCon conId name args) =

1046 (\ args -> InstanceCreation []

1185 (\ args -> InstanceCreation []

1047 idrisObjectType

1186 idrisObjectType

@@ -1050,7 +1189,7 @@ mkExp (SCon conId name args) =

1050 <$> mapM (mkExp .SV) args

1189 <$> mapM (mkExp .SV) args

1051mkExp (SCase var alts) = mkCase False var alts

1190mkExp (SCase var alts) = mkCase False var alts

1052mkExp (SChkCase var alts) = mkCase True var alts

1191mkExp (SChkCase var alts) = mkCase True var alts

1053−mkExp (SProj var i) = return $ mkProjection var i

1192+mkExp (SProj var i) = mkProjection var i

1054mkExp (SConst (I x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1193mkExp (SConst (I x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1055mkExp (SConst (BI x)) =

1194mkExp (SConst (BI x)) =

1056 return $ InstanceCreation []

1195 return $ InstanceCreation []

@@ -1077,226 +1216,235 @@ mkExp (SConst (PtrType)) = return $ mkClass objectType

1077mkExp (SConst (VoidType)) = return $ mkClass voidType

1216mkExp (SConst (VoidType)) = return $ mkClass voidType

1078mkExp (SConst (Forgot)) = return $ mkClass objectType

1217mkExp (SConst (Forgot)) = return $ mkClass objectType

1079mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1218mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1080−mkExp (SOp LPlus args) = return $ mkBinOpExp integerType Add args

1219+mkExp (SOp LPlus args) = mkBinOpExp integerType Add args

1081−mkExp (SOp LMinus args) = return $ mkBinOpExp integerType Sub args

1220+mkExp (SOp LMinus args) = mkBinOpExp integerType Sub args

1082−mkExp (SOp LTimes args) = return $ mkBinOpExp integerType Mult args

1221+mkExp (SOp LTimes args) = mkBinOpExp integerType Mult args

1083−mkExp (SOp LDiv args) = return $ mkBinOpExp integerType Div args

1222+mkExp (SOp LDiv args) = mkBinOpExp integerType Div args

1084−mkExp (SOp LMod args) = return $ mkBinOpExp integerType Rem args

1223+mkExp (SOp LMod args) = mkBinOpExp integerType Rem args

1085−mkExp (SOp LAnd args) = return $ mkBinOpExp integerType And args

1224+mkExp (SOp LAnd args) = mkBinOpExp integerType And args

1086−mkExp (SOp LOr args) = return $ mkBinOpExp integerType Or args

1225+mkExp (SOp LOr args) = mkBinOpExp integerType Or args

1087−mkExp (SOp LXOr args) = return $ mkBinOpExp integerType Xor args

1226+mkExp (SOp LXOr args) = mkBinOpExp integerType Xor args

1088mkExp (SOp LCompl [var]) =

1227mkExp (SOp LCompl [var]) =

1089− return $ PreBitCompl (mkVarAccess (Just $ integerType) var)

1228+ PreBitCompl <$> mkVarAccess (Just $ integerType) var

1090−mkExp (SOp LSHL args) = return $ mkBinOpExp integerType LShift args

1229+mkExp (SOp LSHL args) = mkBinOpExp integerType LShift args

1091−mkExp (SOp LSHR args) = return $ mkBinOpExp integerType RShift args

1230+mkExp (SOp LSHR args) = mkBinOpExp integerType RShift args

1092mkExp (SOp LEq args) =

1231mkExp (SOp LEq args) =

1093− return $ mkMethodOpChain1 (mkBoolToNumber integerType) objectType "equals" args

1232+ mkMethodOpChain1 (mkBoolToNumber integerType) objectType "equals" args

1094−mkExp (SOp LLt args) = return $ mkLogicalBinOpExp integerType LThan args

1233+mkExp (SOp LLt args) = mkLogicalBinOpExp integerType LThan args

1095−mkExp (SOp LLe args) = return $ mkLogicalBinOpExp integerType LThanE args

1234+mkExp (SOp LLe args) = mkLogicalBinOpExp integerType LThanE args

1096−mkExp (SOp LGt args) = return $ mkLogicalBinOpExp integerType GThan args

1235+mkExp (SOp LGt args) = mkLogicalBinOpExp integerType GThan args

1097−mkExp (SOp LGe args) = return $ mkLogicalBinOpExp integerType GThanE args

1236+mkExp (SOp LGe args) = mkLogicalBinOpExp integerType GThanE args

1098−mkExp (SOp LFPlus args) = return $ mkBinOpExp doubleType Add args

1237+mkExp (SOp LFPlus args) = mkBinOpExp doubleType Add args

1099−mkExp (SOp LFMinus args) = return $ mkBinOpExp doubleType Sub args

1238+mkExp (SOp LFMinus args) = mkBinOpExp doubleType Sub args

1100−mkExp (SOp LFTimes args) = return $ mkBinOpExp doubleType Mult args

1239+mkExp (SOp LFTimes args) = mkBinOpExp doubleType Mult args

1101−mkExp (SOp LFDiv args) = return $ mkBinOpExp doubleType Div args

1240+mkExp (SOp LFDiv args) = mkBinOpExp doubleType Div args

1102mkExp (SOp LFEq args) =

1241mkExp (SOp LFEq args) =

1103− return $ mkMethodOpChain1 (mkBoolToNumber doubleType) doubleType "equals" args

1242+ mkMethodOpChain1 (mkBoolToNumber doubleType) doubleType "equals" args

1104−mkExp (SOp LFLt args) = return $ mkLogicalBinOpExp integerType LThan args

1243+mkExp (SOp LFLt args) = mkLogicalBinOpExp integerType LThan args

1105−mkExp (SOp LFLe args) = return $ mkLogicalBinOpExp integerType LThanE args

1244+mkExp (SOp LFLe args) = mkLogicalBinOpExp integerType LThanE args

1106−mkExp (SOp LFGt args) = return $ mkLogicalBinOpExp integerType GThan args

1245+mkExp (SOp LFGt args) = mkLogicalBinOpExp integerType GThan args

1107−mkExp (SOp LFGe args) = return $ mkLogicalBinOpExp integerType GThanE args

1246+mkExp (SOp LFGe args) = mkLogicalBinOpExp integerType GThanE args

1108−mkExp (SOp LBPlus args) = return $ mkMethodOpChain1 id bigIntegerType "add" args

1247+mkExp (SOp LBPlus args) = mkMethodOpChain1 id bigIntegerType "add" args

1109−mkExp (SOp LBMinus args) = return $ mkMethodOpChain1 id bigIntegerType "subtract" args

1248+mkExp (SOp LBMinus args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1110−mkExp (SOp LBTimes args) = return $ mkMethodOpChain1 id bigIntegerType "multiply" args

1249+mkExp (SOp LBTimes args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1111−mkExp (SOp LBDiv args) = return $ mkMethodOpChain1 id bigIntegerType "divide" args

1250+mkExp (SOp LBDiv args) = mkMethodOpChain1 id bigIntegerType "divide" args

1112−mkExp (SOp LBMod args) = return $ mkMethodOpChain1 id bigIntegerType "mod" args

1251+mkExp (SOp LBMod args) = mkMethodOpChain1 id bigIntegerType "mod" args

1113mkExp (SOp LBEq args) =

1252mkExp (SOp LBEq args) =

1114− return $ mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1253+ mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1115mkExp (SOp LBLt args) =

1254mkExp (SOp LBLt args) =

1116− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1255+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1117− . mkPartialOrder SLt

1256+ . mkPartialOrder SLt

1118− )

1257+ )

1119− bigIntegerType

1258+ bigIntegerType

1120− "compare"

1259+ "compare"

1121− args

1260+ args

1122mkExp (SOp LBLe args) =

1261mkExp (SOp LBLe args) =

1123− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1262+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1124− . mkPartialOrder SLe

1263+ . mkPartialOrder SLe

1125− )

1264+ )

1126− bigIntegerType

1265+ bigIntegerType

1127− "compare"

1266+ "compare"

1128− args

1267+ args

1129mkExp (SOp LBGt args) =

1268mkExp (SOp LBGt args) =

1130− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1269+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1131− . mkPartialOrder SGt

1270+ . mkPartialOrder SGt

1132− )

1271+ )

1133− bigIntegerType

1272+ bigIntegerType

1134− "compare"

1273+ "compare"

1135− args

1274+ args

1136mkExp (SOp LBGe args) =

1275mkExp (SOp LBGe args) =

1137− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1276+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1138− . mkPartialOrder SGe

1277+ . mkPartialOrder SGe

1139− )

1278+ )

1140− bigIntegerType

1279+ bigIntegerType

1141− "compare"

1280+ "compare"

1142− args

1281+ args

1143mkExp (SOp LStrConcat args) =

1282mkExp (SOp LStrConcat args) =

1144− return $ mkMethodOpChain (\ exp ->

1145− InstanceCreation []

1283+ mkMethodOpChain (\ exp -> InstanceCreation []

1146− (ClassType [(Ident "StringBuilder", [])])

1284+ (ClassType [(Ident "StringBuilder", [])])

1147− [exp]

1285+ [exp]

1148− Nothing

1286+ Nothing

1149− )

1287+ )

1150− (\ exp -> MethodInv $ PrimaryMethodCall exp [] (Ident "toString") [])

1288+ (\ exp -> MethodInv $ PrimaryMethodCall exp [] (Ident "toString") [])

1151− stringType

1289+ stringType

1152− "append"

1290+ "append"

1153− args

1291+ args

1154mkExp (SOp LStrLt args@[_, _]) =

1292mkExp (SOp LStrLt args@[_, _]) =

1155− return $ mkMethodOpChain1 ( mkBoolToNumber integerType

1293+ mkMethodOpChain1 ( mkBoolToNumber integerType

1156− . mkPartialOrder SLt

1294+ . mkPartialOrder SLt

1157− )

1295+ )

1158− stringType

1296+ stringType

1159− "compare"

1297+ "compare"

1160− args

1298+ args

1161mkExp (SOp LStrEq args@[_, _]) =

1299mkExp (SOp LStrEq args@[_, _]) =

1162− return $ mkMethodOpChain1 ( mkBoolToNumber integerType)

1300+ mkMethodOpChain1 ( mkBoolToNumber integerType)

1163− stringType

1301+ stringType

1164− "equals"

1302+ "equals"

1165− args

1303+ args

1166mkExp (SOp LStrLen [arg]) =

1304mkExp (SOp LStrLen [arg]) =

1305+ (\ var -> MethodInv $ PrimaryMethodCall var [] (Ident "length") [])

1167− return . MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) arg) [] (Ident "length") []

1306+ <$> mkVarAccess (Just stringType) arg

1168mkExp (SOp LIntFloat [arg]) =

1307mkExp (SOp LIntFloat [arg]) =

1169− return $ mkPrimitiveCast integerType doubleType arg

1308+ mkPrimitiveCast integerType doubleType arg

1170mkExp (SOp LFloatInt [arg]) =

1309mkExp (SOp LFloatInt [arg]) =

1171− return $ mkPrimitiveCast doubleType integerType arg

1310+ mkPrimitiveCast doubleType integerType arg

1172mkExp (SOp LIntStr [arg]) =

1311mkExp (SOp LIntStr [arg]) =

1173− return $ mkToString integerType arg

1312+ mkToString integerType arg

1174mkExp (SOp LStrInt [arg]) =

1313mkExp (SOp LStrInt [arg]) =

1175− return $ mkPrimitiveCast stringType integerType arg

1314+ mkPrimitiveCast stringType integerType arg

1176mkExp (SOp LFloatStr [arg]) =

1315mkExp (SOp LFloatStr [arg]) =

1177− return $ mkToString doubleType arg

1316+ mkToString doubleType arg

1178mkExp (SOp LStrFloat [arg]) =

1317mkExp (SOp LStrFloat [arg]) =

1179− return $ mkPrimitiveCast doubleType stringType arg

1318+ mkPrimitiveCast doubleType stringType arg

1180mkExp (SOp LIntBig [arg]) =

1319mkExp (SOp LIntBig [arg]) =

1181− return $ mkPrimitiveCast integerType bigIntegerType arg

1320+ mkPrimitiveCast integerType bigIntegerType arg

1182mkExp (SOp LBigInt [arg]) =

1321mkExp (SOp LBigInt [arg]) =

1183− return $ mkPrimitiveCast bigIntegerType integerType arg

1322+ mkPrimitiveCast bigIntegerType integerType arg

1184mkExp (SOp LStrBig [arg]) =

1323mkExp (SOp LStrBig [arg]) =

1324+ (\ var -> InstanceCreation [] bigIntegerType [var] Nothing)

1185− return $ InstanceCreation [] bigIntegerType [mkVarAccess (Just stringType) arg] Nothing

1325+ <$> mkVarAccess (Just stringType) arg

1186mkExp (SOp LBigStr [arg]) =

1326mkExp (SOp LBigStr [arg]) =

1187− return $ mkToString bigIntegerType arg

1327+ mkToString bigIntegerType arg

1188mkExp (SOp LChInt [arg]) =

1328mkExp (SOp LChInt [arg]) =

1189− return $ mkVarAccess (Just integerType) arg

1329+ mkVarAccess (Just integerType) arg

1190mkExp (SOp LIntCh [arg]) =

1330mkExp (SOp LIntCh [arg]) =

1191− return $ mkVarAccess (Just integerType) arg

1331+ mkVarAccess (Just integerType) arg

1192mkExp (SOp LPrintNum [arg]) =

1332mkExp (SOp LPrintNum [arg]) =

1193− return $ mkSystemOutPrint (mkVarAccess Nothing arg)

1333+ mkSystemOutPrint <$> (mkVarAccess Nothing arg)

1194mkExp (SOp LPrintStr [arg]) =

1334mkExp (SOp LPrintStr [arg]) =

1195− return $ mkSystemOutPrint (mkVarAccess (Just stringType) arg)

1335+ mkSystemOutPrint <$> (mkVarAccess (Just stringType) arg)

1196mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1336mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1197−mkExp (SOp LB8Lt args) = return $ mkLogicalBinOpExp byteType LThan args

1337+mkExp (SOp LB8Lt args) = mkLogicalBinOpExp byteType LThan args

1198−mkExp (SOp LB8Lte args) = return $ mkLogicalBinOpExp byteType LThanE args

1338+mkExp (SOp LB8Lte args) = mkLogicalBinOpExp byteType LThanE args

1199mkExp (SOp LB8Eq args) =

1339mkExp (SOp LB8Eq args) =

1200− return $ mkMethodOpChain1 (mkBoolToNumber byteType) byteType "equals" args

1340+ mkMethodOpChain1 (mkBoolToNumber byteType) byteType "equals" args

1201−mkExp (SOp LB8Gt args) = return $ mkLogicalBinOpExp byteType GThan args

1341+mkExp (SOp LB8Gt args) = mkLogicalBinOpExp byteType GThan args

1202−mkExp (SOp LB8Gte args) = return $ mkLogicalBinOpExp byteType GThanE args

1342+mkExp (SOp LB8Gte args) = mkLogicalBinOpExp byteType GThanE args

1203−mkExp (SOp LB8Plus args) = return $ mkBinOpExp byteType Add args

1343+mkExp (SOp LB8Plus args) = mkBinOpExp byteType Add args

1204−mkExp (SOp LB8Minus args) = return $ mkBinOpExp byteType Sub args

1344+mkExp (SOp LB8Minus args) = mkBinOpExp byteType Sub args

1205−mkExp (SOp LB8Times args) = return $ mkBinOpExp byteType Mult args

1345+mkExp (SOp LB8Times args) = mkBinOpExp byteType Mult args

1206−mkExp (SOp LB8UDiv args) = return $ mkBinOpExpConv "shortValue" ShortT byteType Div args

1346+mkExp (SOp LB8UDiv args) = mkBinOpExpConv "shortValue" ShortT byteType Div args

1207−mkExp (SOp LB8SDiv args) = return $ mkBinOpExp byteType Div args

1347+mkExp (SOp LB8SDiv args) = mkBinOpExp byteType Div args

1208−mkExp (SOp LB8URem args) = return $ mkBinOpExpConv "shortValue" ShortT byteType Rem args

1348+mkExp (SOp LB8URem args) = mkBinOpExpConv "shortValue" ShortT byteType Rem args

1209−mkExp (SOp LB8SRem args) = return $ mkBinOpExp byteType Rem args

1349+mkExp (SOp LB8SRem args) = mkBinOpExp byteType Rem args

1210−mkExp (SOp LB8Shl args) = return $ mkBinOpExp byteType LShift args

1350+mkExp (SOp LB8Shl args) = mkBinOpExp byteType LShift args

1211−mkExp (SOp LB8LShr args) = return $ mkBinOpExp byteType RRShift args

1351+mkExp (SOp LB8LShr args) = mkBinOpExp byteType RRShift args

1212−mkExp (SOp LB8AShr args) = return $ mkBinOpExp byteType RShift args

1352+mkExp (SOp LB8AShr args) = mkBinOpExp byteType RShift args

1213−mkExp (SOp LB8And args) = return $ mkBinOpExp byteType And args

1353+mkExp (SOp LB8And args) = mkBinOpExp byteType And args

1214−mkExp (SOp LB8Or args) = return $ mkBinOpExp byteType Or args

1354+mkExp (SOp LB8Or args) = mkBinOpExp byteType Or args

1215−mkExp (SOp LB8Xor args) = return $ mkBinOpExp byteType Xor args

1355+mkExp (SOp LB8Xor args) = mkBinOpExp byteType Xor args

1216mkExp (SOp LB8Compl [var]) =

1356mkExp (SOp LB8Compl [var]) =

1217− return $ PreBitCompl (mkVarAccess (Just $ byteType) var)

1357+ PreBitCompl <$> mkVarAccess (Just $ byteType) var

1218−mkExp (SOp LB8Z16 [var]) = return $ mkZeroExt "shortValue" 8 byteType shortType var

1358+mkExp (SOp LB8Z16 [var]) = mkZeroExt "shortValue" 8 byteType shortType var

1219−mkExp (SOp LB8Z32 [var]) = return $ mkZeroExt "intValue" 8 byteType integerType var

1359+mkExp (SOp LB8Z32 [var]) = mkZeroExt "intValue" 8 byteType integerType var

1220−mkExp (SOp LB8Z64 [var]) = return $ mkZeroExt "longValue" 8 byteType longType var

1360+mkExp (SOp LB8Z64 [var]) = mkZeroExt "longValue" 8 byteType longType var

1221−mkExp (SOp LB8S16 [var]) = return $ mkSignedExt "shortValue" byteType shortType var

1361+mkExp (SOp LB8S16 [var]) = mkSignedExt "shortValue" byteType shortType var

1222−mkExp (SOp LB8S32 [var]) = return $ mkSignedExt "intValue" byteType integerType var

1362+mkExp (SOp LB8S32 [var]) = mkSignedExt "intValue" byteType integerType var

1223−mkExp (SOp LB8S64 [var]) = return $ mkSignedExt "longValue" byteType longType var

1363+mkExp (SOp LB8S64 [var]) = mkSignedExt "longValue" byteType longType var

1224−mkExp (SOp LB16Lt args) = return $ mkLogicalBinOpExp shortType LThan args

1364+mkExp (SOp LB16Lt args) = mkLogicalBinOpExp shortType LThan args

1225−mkExp (SOp LB16Lte args) = return $ mkLogicalBinOpExp shortType LThanE args

1365+mkExp (SOp LB16Lte args) = mkLogicalBinOpExp shortType LThanE args

1226mkExp (SOp LB16Eq args) =

1366mkExp (SOp LB16Eq args) =

1227− return $ mkMethodOpChain1 (mkBoolToNumber shortType) shortType "equals" args

1367+ mkMethodOpChain1 (mkBoolToNumber shortType) shortType "equals" args

1228−mkExp (SOp LB16Gt args) = return $ mkLogicalBinOpExp shortType GThan args

1368+mkExp (SOp LB16Gt args) = mkLogicalBinOpExp shortType GThan args

1229−mkExp (SOp LB16Gte args) = return $ mkLogicalBinOpExp shortType GThanE args

1369+mkExp (SOp LB16Gte args) = mkLogicalBinOpExp shortType GThanE args

1230−mkExp (SOp LB16Plus args) = return $ mkBinOpExp shortType Add args

1370+mkExp (SOp LB16Plus args) = mkBinOpExp shortType Add args

1231−mkExp (SOp LB16Minus args) = return $ mkBinOpExp shortType Sub args

1371+mkExp (SOp LB16Minus args) = mkBinOpExp shortType Sub args

1232−mkExp (SOp LB16Times args) = return $ mkBinOpExp shortType Mult args

1372+mkExp (SOp LB16Times args) = mkBinOpExp shortType Mult args

1233−mkExp (SOp LB16UDiv args) = return $ mkBinOpExpConv "intValue" IntT shortType Div args

1373+mkExp (SOp LB16UDiv args) = mkBinOpExpConv "intValue" IntT shortType Div args

1234−mkExp (SOp LB16SDiv args) = return $ mkBinOpExp shortType Div args

1374+mkExp (SOp LB16SDiv args) = mkBinOpExp shortType Div args

1235−mkExp (SOp LB16URem args) = return $ mkBinOpExpConv "intValue" IntT shortType Rem args

1375+mkExp (SOp LB16URem args) = mkBinOpExpConv "intValue" IntT shortType Rem args

1236−mkExp (SOp LB16SRem args) = return $ mkBinOpExp shortType Rem args

1376+mkExp (SOp LB16SRem args) = mkBinOpExp shortType Rem args

1237−mkExp (SOp LB16Shl args) = return $ mkBinOpExp shortType LShift args

1377+mkExp (SOp LB16Shl args) = mkBinOpExp shortType LShift args

1238−mkExp (SOp LB16LShr args) = return $ mkBinOpExp shortType RRShift args

1378+mkExp (SOp LB16LShr args) = mkBinOpExp shortType RRShift args

1239−mkExp (SOp LB16AShr args) = return $ mkBinOpExp shortType RShift args

1379+mkExp (SOp LB16AShr args) = mkBinOpExp shortType RShift args

1240−mkExp (SOp LB16And args) = return $ mkBinOpExp shortType And args

1380+mkExp (SOp LB16And args) = mkBinOpExp shortType And args

1241−mkExp (SOp LB16Or args) = return $ mkBinOpExp shortType Or args

1381+mkExp (SOp LB16Or args) = mkBinOpExp shortType Or args

1242−mkExp (SOp LB16Xor args) = return $ mkBinOpExp shortType Xor args

1382+mkExp (SOp LB16Xor args) = mkBinOpExp shortType Xor args

1243mkExp (SOp LB16Compl [var]) =

1383mkExp (SOp LB16Compl [var]) =

1244− return $ PreBitCompl (mkVarAccess (Just $ shortType) var)

1384+ PreBitCompl <$> mkVarAccess (Just $ shortType) var

1245−mkExp (SOp LB16Z32 [var]) = return $ mkZeroExt "intValue" 16 shortType integerType var

1385+mkExp (SOp LB16Z32 [var]) = mkZeroExt "intValue" 16 shortType integerType var

1246−mkExp (SOp LB16Z64 [var]) = return $ mkZeroExt "longValue" 16 shortType longType var

1386+mkExp (SOp LB16Z64 [var]) = mkZeroExt "longValue" 16 shortType longType var

1247−mkExp (SOp LB16S32 [var]) = return $ mkSignedExt "intValue" shortType integerType var

1387+mkExp (SOp LB16S32 [var]) = mkSignedExt "intValue" shortType integerType var

1248−mkExp (SOp LB16S64 [var]) = return $ mkSignedExt "longValue" shortType longType var

1388+mkExp (SOp LB16S64 [var]) = mkSignedExt "longValue" shortType longType var

1249mkExp (SOp LB16T8 [var]) =

1389mkExp (SOp LB16T8 [var]) =

1250− return . MethodInv $

1390+ (\ var -> MethodInv $

1251− TypeMethodCall (J.Name [Ident "Byte"])

1391+ TypeMethodCall (J.Name [Ident "Byte"])

1252− []

1392+ []

1253− (Ident "valueOf")

1393+ (Ident "valueOf")

1394+ [ MethodInv

1395+ $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1396+ )

1254− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ shortType) var) [] (Ident "byteValue") [] ]

1397+ <$> mkVarAccess (Just $ shortType) var

1255−mkExp (SOp LB32Lt args) = return $ mkLogicalBinOpExp integerType LThan args

1398+mkExp (SOp LB32Lt args) = mkLogicalBinOpExp integerType LThan args

1256−mkExp (SOp LB32Lte args) = return $ mkLogicalBinOpExp integerType LThanE args

1399+mkExp (SOp LB32Lte args) = mkLogicalBinOpExp integerType LThanE args

1257mkExp (SOp LB32Eq args) =

1400mkExp (SOp LB32Eq args) =

1258− return $ mkMethodOpChain1 (mkBoolToNumber integerType) integerType "equals" args

1401+ mkMethodOpChain1 (mkBoolToNumber integerType) integerType "equals" args

1259−mkExp (SOp LB32Gt args) = return $ mkLogicalBinOpExp integerType GThan args

1402+mkExp (SOp LB32Gt args) = mkLogicalBinOpExp integerType GThan args

1260−mkExp (SOp LB32Gte args) = return $ mkLogicalBinOpExp integerType GThanE args

1403+mkExp (SOp LB32Gte args) = mkLogicalBinOpExp integerType GThanE args

1261−mkExp (SOp LB32Plus args) = return $ mkBinOpExp integerType Add args

1404+mkExp (SOp LB32Plus args) = mkBinOpExp integerType Add args

1262−mkExp (SOp LB32Minus args) = return $ mkBinOpExp integerType Sub args

1405+mkExp (SOp LB32Minus args) = mkBinOpExp integerType Sub args

1263−mkExp (SOp LB32Times args) = return $ mkBinOpExp integerType Mult args

1406+mkExp (SOp LB32Times args) = mkBinOpExp integerType Mult args

1264−mkExp (SOp LB32UDiv args) = return $ mkBinOpExpConv "longValue" LongT integerType Div args

1407+mkExp (SOp LB32UDiv args) = mkBinOpExpConv "longValue" LongT integerType Div args

1265−mkExp (SOp LB32SDiv args) = return $ mkBinOpExp integerType Div args

1408+mkExp (SOp LB32SDiv args) = mkBinOpExp integerType Div args

1266−mkExp (SOp LB32URem args) = return $ mkBinOpExpConv "longValue" LongT integerType Rem args

1409+mkExp (SOp LB32URem args) = mkBinOpExpConv "longValue" LongT integerType Rem args

1267−mkExp (SOp LB32SRem args) = return $ mkBinOpExp integerType Rem args

1410+mkExp (SOp LB32SRem args) = mkBinOpExp integerType Rem args

1268−mkExp (SOp LB32Shl args) = return $ mkBinOpExp integerType LShift args

1411+mkExp (SOp LB32Shl args) = mkBinOpExp integerType LShift args

1269−mkExp (SOp LB32LShr args) = return $ mkBinOpExp integerType RRShift args

1412+mkExp (SOp LB32LShr args) = mkBinOpExp integerType RRShift args

1270−mkExp (SOp LB32AShr args) = return $ mkBinOpExp integerType RShift args

1413+mkExp (SOp LB32AShr args) = mkBinOpExp integerType RShift args

1271−mkExp (SOp LB32And args) = return $ mkBinOpExp integerType And args

1414+mkExp (SOp LB32And args) = mkBinOpExp integerType And args

1272−mkExp (SOp LB32Or args) = return $ mkBinOpExp integerType Or args

1415+mkExp (SOp LB32Or args) = mkBinOpExp integerType Or args

1273−mkExp (SOp LB32Xor args) = return $ mkBinOpExp integerType Xor args

1416+mkExp (SOp LB32Xor args) = mkBinOpExp integerType Xor args

1274mkExp (SOp LB32Compl [var]) =

1417mkExp (SOp LB32Compl [var]) =

1275− return $ PreBitCompl (mkVarAccess (Just $ integerType) var)

1418+ PreBitCompl <$> mkVarAccess (Just $ integerType) var

1276−mkExp (SOp LB32Z64 [var]) = return $ mkZeroExt "longValue" 32 integerType longType var

1419+mkExp (SOp LB32Z64 [var]) = mkZeroExt "longValue" 32 integerType longType var

1277−mkExp (SOp LB32S64 [var]) = return $ mkSignedExt "longValue" integerType longType var

1420+mkExp (SOp LB32S64 [var]) = mkSignedExt "longValue" integerType longType var

1278mkExp (SOp LB32T8 [var]) =

1421mkExp (SOp LB32T8 [var]) =

1279− return . MethodInv $

1422+ (\ var -> MethodInv

1280− TypeMethodCall (J.Name [Ident "Byte"])

1423+ $ TypeMethodCall (J.Name [Ident "Byte"])

1281− []

1424+ []

1282− (Ident "valueOf")

1425+ (Ident "valueOf")

1426+ [ MethodInv $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1427+ )

1283− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ integerType) var) [] (Ident "byteValue") [] ]

1428+ <$> mkVarAccess (Just $ integerType) var

1284mkExp (SOp LB32T16 [var]) =

1429mkExp (SOp LB32T16 [var]) =

1285− return . MethodInv $

1430+ (\ var -> MethodInv

1286− TypeMethodCall (J.Name [Ident "Short"])

1431+ $ TypeMethodCall (J.Name [Ident "Short"])

1287− []

1432+ []

1288− (Ident "valueOf")

1433+ (Ident "valueOf")

1434+ [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1435+ )

1289− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ integerType) var) [] (Ident "shortValue") [] ]

1436+ <$> mkVarAccess (Just $ integerType) var

1290−mkExp (SOp LB64Lt args) = return $ mkLogicalBinOpExp longType LThan args

1437+mkExp (SOp LB64Lt args) = mkLogicalBinOpExp longType LThan args

1291−mkExp (SOp LB64Lte args) = return $ mkLogicalBinOpExp longType LThanE args

1438+mkExp (SOp LB64Lte args) = mkLogicalBinOpExp longType LThanE args

1292mkExp (SOp LB64Eq args) =

1439mkExp (SOp LB64Eq args) =

1293− return $ mkMethodOpChain1 (mkBoolToNumber longType) longType "equals" args

1440+ mkMethodOpChain1 (mkBoolToNumber longType) longType "equals" args

1294−mkExp (SOp LB64Gt args) = return $ mkLogicalBinOpExp longType GThan args

1441+mkExp (SOp LB64Gt args) = mkLogicalBinOpExp longType GThan args

1295−mkExp (SOp LB64Gte args) = return $ mkLogicalBinOpExp longType GThanE args

1442+mkExp (SOp LB64Gte args) = mkLogicalBinOpExp longType GThanE args

1296−mkExp (SOp LB64Plus args) = return $ mkBinOpExp longType Add args

1443+mkExp (SOp LB64Plus args) = mkBinOpExp longType Add args

1297−mkExp (SOp LB64Minus args) = return $ mkBinOpExp longType Sub args

1444+mkExp (SOp LB64Minus args) = mkBinOpExp longType Sub args

1298−mkExp (SOp LB64Times args) = return $ mkBinOpExp longType Mult args

1445+mkExp (SOp LB64Times args) = mkBinOpExp longType Mult args

1299−mkExp (SOp LB64UDiv (arg:args)) =

1446+mkExp (SOp LB64UDiv (arg:args)) = do

1447+ (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1300 return $ foldl (\ exp arg ->

1448 return $ foldl (\ exp arg ->

1301 MethodInv $ PrimaryMethodCall

1449 MethodInv $ PrimaryMethodCall

1302 ( MethodInv $ PrimaryMethodCall

1450 ( MethodInv $ PrimaryMethodCall

@@ -1310,17 +1458,18 @@ mkExp (SOp LB64UDiv (arg:args)) =

1310 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1458 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1311 []

1459 []

1312 (Ident "valueOf")

1460 (Ident "valueOf")

1313− [ (mkVarAccess (Just longType) arg) ]

1461+ [ arg ]

1314 ]

1462 ]

1315 )

1463 )

1316 []

1464 []

1317 (Ident "longValue")

1465 (Ident "longValue")

1318 []

1466 []

1319 )

1467 )

1320− (mkVarAccess (Just longType) arg)

1468+ arg

1321 args

1469 args

1322−mkExp (SOp LB64SDiv args) = return $ mkBinOpExp longType Div args

1470+mkExp (SOp LB64SDiv args) = mkBinOpExp longType Div args

1323−mkExp (SOp LB64URem (arg:args)) =

1471+mkExp (SOp LB64URem (arg:args)) = do

1472+ (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1324 return $ foldl (\ exp arg ->

1473 return $ foldl (\ exp arg ->

1325 MethodInv $ PrimaryMethodCall

1474 MethodInv $ PrimaryMethodCall

1326 ( MethodInv $ PrimaryMethodCall

1475 ( MethodInv $ PrimaryMethodCall

@@ -1334,69 +1483,79 @@ mkExp (SOp LB64URem (arg:args)) =

1334 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1483 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1335 []

1484 []

1336 (Ident "valueOf")

1485 (Ident "valueOf")

1337− [ (mkVarAccess (Just longType) arg) ]

1486+ [ arg ]

1338 ]

1487 ]

1339 )

1488 )

1340 []

1489 []

1341 (Ident "longValue")

1490 (Ident "longValue")

1342 []

1491 []

1343 )

1492 )

1344− (mkVarAccess (Just longType) arg)

1493+ arg

1345 args

1494 args

1346−mkExp (SOp LB64SRem args) = return $ mkBinOpExp longType Rem args

1495+mkExp (SOp LB64SRem args) = mkBinOpExp longType Rem args

1347−mkExp (SOp LB64Shl args) = return $ mkBinOpExp longType LShift args

1496+mkExp (SOp LB64Shl args) = mkBinOpExp longType LShift args

1348−mkExp (SOp LB64LShr args) = return $ mkBinOpExp longType RRShift args

1497+mkExp (SOp LB64LShr args) = mkBinOpExp longType RRShift args

1349−mkExp (SOp LB64AShr args) = return $ mkBinOpExp longType RShift args

1498+mkExp (SOp LB64AShr args) = mkBinOpExp longType RShift args

1350−mkExp (SOp LB64And args) = return $ mkBinOpExp longType And args

1499+mkExp (SOp LB64And args) = mkBinOpExp longType And args

1351−mkExp (SOp LB64Or args) = return $ mkBinOpExp longType Or args

1500+mkExp (SOp LB64Or args) = mkBinOpExp longType Or args

1352−mkExp (SOp LB64Xor args) = return $ mkBinOpExp longType Xor args

1501+mkExp (SOp LB64Xor args) = mkBinOpExp longType Xor args

1353mkExp (SOp LB64Compl [var]) =

1502mkExp (SOp LB64Compl [var]) =

1354− return $ PreBitCompl (mkVarAccess (Just $ longType) var)

1503+ PreBitCompl <$> mkVarAccess (Just $ longType) var

1355mkExp (SOp LB64T8 [var]) =

1504mkExp (SOp LB64T8 [var]) =

1356− return . MethodInv $

1505+ (\ var -> MethodInv

1357− TypeMethodCall (J.Name [Ident "Byte"])

1506+ $ TypeMethodCall (J.Name [Ident "Byte"])

1358− []

1507+ []

1359− (Ident "valueOf")

1508+ (Ident "valueOf")

1509+ [ MethodInv

1510+ $ PrimaryMethodCall var [] (Ident "byteValue") []

1511+ ]

1512+ )

1360− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "byteValue") [] ]

1513+ <$> mkVarAccess (Just $ longType) var

1361mkExp (SOp LB64T16 [var]) =

1514mkExp (SOp LB64T16 [var]) =

1362− return . MethodInv $

1515+ (\ var -> MethodInv

1363− TypeMethodCall (J.Name [Ident "Short"])

1516+ $ TypeMethodCall (J.Name [Ident "Short"])

1364− []

1517+ []

1365− (Ident "valueOf")

1518+ (Ident "valueOf")

1519+ [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1520+ )

1366− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "shortValue") [] ]

1521+ <$> mkVarAccess (Just $ longType) var

1367mkExp (SOp LB64T32 [var]) =

1522mkExp (SOp LB64T32 [var]) =

1368− return . MethodInv $

1523+ (\ var -> MethodInv

1369− TypeMethodCall (J.Name [Ident "Integer"])

1524+ $ TypeMethodCall (J.Name [Ident "Integer"])

1370− []

1525+ []

1371− (Ident "valueOf")

1526+ (Ident "valueOf")

1527+ [ MethodInv $ PrimaryMethodCall var [] (Ident "intValue") [] ]

1528+ )

1372− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "intValue") [] ]

1529+ <$> mkVarAccess (Just $ longType) var

1373mkExp (SOp LIntB8 [arg]) = mkExp (SOp LB32T8 [arg])

1530mkExp (SOp LIntB8 [arg]) = mkExp (SOp LB32T8 [arg])

1374mkExp (SOp LIntB16 [arg]) = mkExp (SOp LB32T16 [arg])

1531mkExp (SOp LIntB16 [arg]) = mkExp (SOp LB32T16 [arg])

1375mkExp (SOp LIntB32 [arg]) = mkExp (SV arg)

1532mkExp (SOp LIntB32 [arg]) = mkExp (SV arg)

1376mkExp (SOp LIntB64 [arg]) = mkExp (SOp LB32S64 [arg])

1533mkExp (SOp LIntB64 [arg]) = mkExp (SOp LB32S64 [arg])

1377mkExp (SOp LB32Int [arg]) = mkExp (SV arg)

1534mkExp (SOp LB32Int [arg]) = mkExp (SV arg)

1378−mkExp (SOp LFExp [arg]) = return $ mkMathFun "exp" arg

1535+mkExp (SOp LFExp [arg]) = mkMathFun "exp" arg

1379−mkExp (SOp LFLog [arg]) = return $ mkMathFun "log" arg

1536+mkExp (SOp LFLog [arg]) = mkMathFun "log" arg

1380−mkExp (SOp LFSin [arg]) = return $ mkMathFun "sin" arg

1537+mkExp (SOp LFSin [arg]) = mkMathFun "sin" arg

1381−mkExp (SOp LFCos [arg]) = return $ mkMathFun "cos" arg

1538+mkExp (SOp LFCos [arg]) = mkMathFun "cos" arg

1382−mkExp (SOp LFTan [arg]) = return $ mkMathFun "tan" arg

1539+mkExp (SOp LFTan [arg]) = mkMathFun "tan" arg

1383−mkExp (SOp LFASin [arg]) = return $ mkMathFun "asin" arg

1540+mkExp (SOp LFASin [arg]) = mkMathFun "asin" arg

1384−mkExp (SOp LFACos [arg]) = return $ mkMathFun "acos" arg

1541+mkExp (SOp LFACos [arg]) = mkMathFun "acos" arg

1385−mkExp (SOp LFATan [arg]) = return $ mkMathFun "atan" arg

1542+mkExp (SOp LFATan [arg]) = mkMathFun "atan" arg

1386−mkExp (SOp LFSqrt [arg]) = return $ mkMathFun "sqrt" arg

1543+mkExp (SOp LFSqrt [arg]) = mkMathFun "sqrt" arg

1387−mkExp (SOp LFFloor [arg]) = return $ mkMathFun "floor" arg

1544+mkExp (SOp LFFloor [arg]) = mkMathFun "floor" arg

1388−mkExp (SOp LFCeil [arg]) = return $ mkMathFun "ceil" arg

1545+mkExp (SOp LFCeil [arg]) = mkMathFun "ceil" arg

1389−mkExp (SOp LStrHead [arg]) = return $ mkStringAtIndex arg (Lit $ Int 0)

1546+mkExp (SOp LStrHead [arg]) = mkStringAtIndex arg (Lit $ Int 0)

1390mkExp (SOp LStrTail [arg]) =

1547mkExp (SOp LStrTail [arg]) =

1391− return . MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) arg)

1548+ (\ var -> MethodInv $ PrimaryMethodCall (var)

1392 []

1549 []

1393 (Ident "substring")

1550 (Ident "substring")

1394 [Lit $ Int 1]

1551 [Lit $ Int 1]

1552+ )

1553+ <$> mkVarAccess (Just stringType) arg

1395mkExp (SOp LStrCons [c, cs]) =

1554mkExp (SOp LStrCons [c, cs]) =

1396− return . MethodInv $

1555+ (\ cVar csVar -> MethodInv $

1397 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

1556 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

1398 (ClassType [(Ident "StringBuilder", [])])

1557 (ClassType [(Ident "StringBuilder", [])])

1399− [mkVarAccess (Just stringType) cs]

1558+ [csVar]

1400 Nothing

1559 Nothing

1401 )

1560 )

1402 []

1561 []

@@ -1404,7 +1563,7 @@ mkExp (SOp LStrCons [c, cs]) =

1404 [ Lit $ Int 0,

1563 [ Lit $ Int 0,

1405 Cast (PrimType CharT)

1564 Cast (PrimType CharT)

1406 (MethodInv $ PrimaryMethodCall

1565 (MethodInv $ PrimaryMethodCall

1407− (mkVarAccess (Just integerType) c)

1566+ (cVar)

1408 []

1567 []

1409 (Ident "intValue")

1568 (Ident "intValue")

1410 []

1569 []

@@ -1414,12 +1573,15 @@ mkExp (SOp LStrCons [c, cs]) =

1414 []

1573 []

1415 (Ident "toString")

1574 (Ident "toString")

1416 []

1575 []

1576+ )

1577+ <$> mkVarAccess (Just integerType) c

1578+ <*> mkVarAccess (Just stringType) cs

1417−mkExp (SOp LStrIndex [str, i]) = return $ mkStringAtIndex str (mkVarAccess (Just integerType) i)

1579+mkExp (SOp LStrIndex [str, i]) = mkVarAccess (Just integerType) i >>= mkStringAtIndex str

1418mkExp (SOp LStrRev [str]) =

1580mkExp (SOp LStrRev [str]) =

1419− return . MethodInv $

1581+ (\ var -> MethodInv $

1420 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

1582 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

1421 (ClassType [(Ident "StringBuffer", [])])

1583 (ClassType [(Ident "StringBuffer", [])])

1422− [mkVarAccess (Just stringType) str]

1584+ [var]

1423 Nothing

1585 Nothing

1424 )

1586 )

1425 []

1587 []

@@ -1429,13 +1591,15 @@ mkExp (SOp LStrRev [str]) =

1429 []

1591 []

1430 (Ident "toString")

1592 (Ident "toString")

1431 []

1593 []

1594+ )

1595+ <$> mkVarAccess (Just stringType) str

1432mkExp (SOp LStdIn []) = return $ mkSystemStd In

1596mkExp (SOp LStdIn []) = return $ mkSystemStd In

1433mkExp (SOp LStdOut []) = return $ mkSystemStd Out

1597mkExp (SOp LStdOut []) = return $ mkSystemStd Out

1434mkExp (SOp LStdErr []) = return $ mkSystemStd Err

1598mkExp (SOp LStdErr []) = return $ mkSystemStd Err

1435mkExp (SOp LFork [arg]) = mkThread arg

1599mkExp (SOp LFork [arg]) = mkThread arg

1436mkExp (SOp LPar [arg]) = mkExp (SV arg)

1600mkExp (SOp LPar [arg]) = mkExp (SV arg)

1437mkExp (SOp LVMPtr []) =

1601mkExp (SOp LVMPtr []) =

1438− return . MethodInv $ TypeMethodCall (J.Name [Ident "Thread"]) [] (Ident "currentThread") []

1602+ return $ MethodInv $ TypeMethodCall (J.Name [Ident "Thread"]) [] (Ident "currentThread") []

1439mkExp (SOp LNoOp args) = mkExp . SV $ last args

1603mkExp (SOp LNoOp args) = mkExp . SV $ last args

1440mkExp (SNothing) = return $ Lit Null

1604mkExp (SNothing) = return $ Lit Null

1441mkExp (SError err) =

1605mkExp (SError err) =

src/IRTS/Compiler.hs+1−1

@@ -71,7 +71,7 @@ compile target f tm

71 (concatMap mkObj objs)

72 (concatMap mkLib libs) NONE

73 ViaJava ->

74− codegenJava c f outty

74+ codegenJava [] c f outty

75 ViaJavaScript ->

76 codegenJavaScript JavaScript c f outty

77 ViaNode ->

src/IRTS/LParser.hs+1−1

@@ -61,7 +61,7 @@ fovm tgt outty f

61 case checked of

62 OK c -> case tgt of

63 ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

64− ViaJava -> codegenJava c "a.out" outty

64+ ViaJava -> codegenJava [] c "a.out" outty

65 Error e -> fail $ show e

67parseFOVM :: FilePath -> IO [(Name, LDecl)]

src/Idris/AbsSyntax.hs+1−1

@@ -940,7 +940,7 @@ stripLinear i tm = evalState (sl tm) [] where

940 if (f `elem` ns)

941 then return Placeholder

942 else do put (f : ns)

943− return (PRef fc f)

943+ return (PPatvar fc f)

944 sl (PApp fc fn args) = do fn' <- sl fn

945 args' <- mapM slA args

946 return $ PApp fc fn' args'

src/Idris/ElabTerm.hs+14−6

@@ -57,6 +57,7 @@ build ist info pattern fn tm

57 resolveTC 7 fn ist) ivs

58 probs <- get_probs

59 tm <- get_term

60+ ctxt <- get_context

60 case probs of

61 case probs of

61 [] -> return ()

62 [] -> return ()

62 ((_,_,_,e):es) -> lift (Error e)

63 ((_,_,_,e):es) -> lift (Error e)

@@ -122,6 +123,15 @@ elab ist info pattern tcgen fn tm

122 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

123 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

123 $ -}

124 $ -}

124 do t' <- insertCoerce ina t

125 do t' <- insertCoerce ina t

126+ g <- goal

127+ tm <- get_term

128+ ps <- get_probs

129+ hs <- get_holes

130+-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

131+-- -- ++ "\n" ++ show tm

132+-- ++ "\nholes " ++ show hs

133+-- ++ "\nproblems " ++ show ps

134+-- ++ "\n-----------\n") $

125 elab' ina t'

135 elab' ina t'

126

136

127 local f = do e <- get_env

137 local f = do e <- get_env

@@ -198,13 +208,8 @@ elab ist info pattern tcgen fn tm

198 trySeq' deferr (x : xs)

208 trySeq' deferr (x : xs)

199 = try' (elab' ina x) (trySeq' deferr xs) True

209 = try' (elab' ina x) (trySeq' deferr xs) True

200 elab' ina (PPatvar fc n) | pattern = patvar n

210 elab' ina (PPatvar fc n) | pattern = patvar n

201−-- = do env <- get_env

202−-- case lookup n env of

203−-- Just (PVar _) -> elab' ina Placeholder

204−-- _ -> patvar n

205 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

211 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

206 = do ctxt <- get_context

212 = do ctxt <- get_context

207− env <- get_env

208 let defined = case lookupTy Nothing n ctxt of

213 let defined = case lookupTy Nothing n ctxt of

209 [] -> False

214 [] -> False

210 _ -> True

215 _ -> True

@@ -421,6 +426,8 @@ elab ist info pattern tcgen fn tm

421 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

426 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

422 -- elaborate case

427 -- elaborate case

423 updateAux (newdef : )

428 updateAux (newdef : )

429+ -- if we haven't got the type yet, hopefully we'll get it later!

430+ movelast tyn

424 solve

431 solve

425 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

432 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

426 mkCaseName (UN x) = UN (x ++ "_case")

433 mkCaseName (UN x) = UN (x ++ "_case")

@@ -537,7 +544,8 @@ pruneByType (P _ n _) c as

537

544

538 typeHead var f f'

545 typeHead var f f'

539 = case lookupTy Nothing f' c of

546 = case lookupTy Nothing f' c of

547+ [ty] -> let ty' = normalise c [] ty in

540− [ty] -> case unApply (getRetTy ty) of

548+ case unApply (getRetTy ty') of

541 (P _ ftyn _, _) -> ftyn == f

549 (P _ ftyn _, _) -> ftyn == f

542 (V _, _) -> var -- keep, variable

550 (V _, _) -> var -- keep, variable

543 _ -> False

551 _ -> False

src/Idris/Primitives.hs+3

@@ -332,6 +332,8 @@ primitives =

332 (2, LStrEq) total,

333 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

334 (2, LStrLt) total,

335+ Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

336+ (1, LStrLen) total,

335 -- Conversions

337 -- Conversions

336 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

338 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

337 (1, LStrInt) total,

339 (1, LStrInt) total,

@@ -622,6 +624,7 @@ p_floatSqrt = p_fPrim sqrt

622p_floatFloor = p_fPrim (fromInteger . floor)

624p_floatFloor = p_fPrim (fromInteger . floor)

623p_floatCeil = p_fPrim (fromInteger . ceiling)

625p_floatCeil = p_fPrim (fromInteger . ceiling)

624

626

627+p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

625p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

628p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

626p_strHead _ = Nothing

629p_strHead _ = Nothing

627p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

630p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

src/Util/System.hs+38−4

@@ -1,13 +1,20 @@

1{-# LANGUAGE CPP #-}

2−module Util.System(tempfile,environment,getCC,

2+module Util.System(tempfile,withTempdir,environment,getCC,

3− getLibFlags,getIdrisLibDir,getIncFlags,rmFile) where

3+ getLibFlags,getIdrisLibDir,getIncFlags,rmFile,

4+ getMvn,getExecutablePom) where

5-- System helper functions.

6-- System helper functions.

6−

7+import Control.Monad (when)

8+import Distribution.Text (display)

7−import System.Directory (getTemporaryDirectory, removeFile)

9+import System.Directory (getTemporaryDirectory

10+ , removeFile

11+ , removeDirectoryRecursive

12+ , createDirectoryIfMissing

13+ )

8import System.FilePath ((</>), addTrailingPathSeparator, normalise)

14import System.FilePath ((</>), addTrailingPathSeparator, normalise)

9import System.Environment

15import System.Environment

10import System.IO

16import System.IO

17+import System.IO.Error

11#if MIN_VERSION_base(4,0,0)

18#if MIN_VERSION_base(4,0,0)

12import Control.Exception as CE

19import Control.Exception as CE

13#endif

20#endif

@@ -17,20 +24,44 @@ import Paths_idris

17#if MIN_VERSION_base(4,0,0)

24#if MIN_VERSION_base(4,0,0)

18catchIO :: IO a -> (IOError -> IO a) -> IO a

25catchIO :: IO a -> (IOError -> IO a) -> IO a

19catchIO = CE.catch

26catchIO = CE.catch

27+

28+throwIO :: IOError -> IO a

29+throwIO = CE.throw

20#else

30#else

21catchIO = catch

31catchIO = catch

32+throwIO = throw

22#endif

33#endif

35+

36+

24getCC :: IO String

37getCC :: IO String

25getCC = do env <- environment "IDRIS_CC"

38getCC = do env <- environment "IDRIS_CC"

26 case env of

39 case env of

27 Nothing -> return "gcc"

40 Nothing -> return "gcc"

28 Just cc -> return cc

41 Just cc -> return cc

43+getMvn :: IO String

44+getMvn = do env <- environment "IDRIS_MVN"

45+ case env of

46+ Nothing -> return "mvn"

47+ Just mvn -> return mvn

48+

30tempfile :: IO (FilePath, Handle)

49tempfile :: IO (FilePath, Handle)

31tempfile = do dir <- getTemporaryDirectory

50tempfile = do dir <- getTemporaryDirectory

32 openTempFile (normalise dir) "idris"

51 openTempFile (normalise dir) "idris"

53+withTempdir :: String -> (FilePath -> IO a) -> IO a

54+withTempdir subdir callback

55+ = do dir <- getTemporaryDirectory

56+ let tmpDir = (normalise dir) </> subdir

57+ removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)

58+ (\ ioError -> if isAlreadyExistsError ioError then return False

59+ else throw ioError

60+ )

61+ result <- callback tmpDir

62+ when removeLater $ removeDirectoryRecursive tmpDir

63+ return result

64+

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

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

35environment x = catchIO (do e <- getEnv x

66environment x = catchIO (do e <- getEnv x

36 return (Just e))

67 return (Just e))

@@ -51,3 +82,6 @@ getIdrisLibDir = do dir <- getDataDir

52getIncFlags = do dir <- getDataDir

83getIncFlags = do dir <- getDataDir

53 return $ "-I" ++ dir </> "rts"

84 return $ "-I" ++ dir </> "rts"

85+

86+getExecutablePom = do dir <- getDataDir

87+ return $ dir </> "executable_pom.xml"

test/Makefile+1−1

@@ -2,7 +2,7 @@ test:

2 perl ./runtest.pl all

4test_java:

5− perl ./runtest.pl all --java

5+ perl ./runtest.pl all --target Java

7update:

8 perl ./runtest.pl all -u

test/mkjavatest.pldeleted−24

@@ -1,24 +0,0 @@

1−#!/usr/bin/perl

2−

3−if ($#ARGV>=0) {

4− $test=shift(@ARGV);

5−} else {

6− print "What's its name?\n";

7− exit;

8−}

9−

10−mkdir($test);

11−

12−chdir($test);

13−open(FOO,">run_java");

14−

15−print FOO "#!/bin/bash\n";

16−print FOO "idris \$@ $test.idr -o $test.java --target Java\n";

17−print FOO "export CLASSPATH=../../java/idris.jar:\$CLASSPATH\n";

18−print FOO "javac $test.java\n";

19−print FOO "java $test\n";

20−print FOO "rm -f $test.java *.class\n";

21−

22−close(FOO);

23−

24−system("chmod +x run_java");

test/reg002/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ reg002.idr -o reg002.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac reg002.java

5−java reg002

6−rm -f reg002.java *.class

test/reg004/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ reg004.idr -o reg004.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac reg004.java

5−java reg004

6−rm -f reg004.java *.class

test/reg005/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ reg005.idr -o reg005.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac reg005.java

5−java reg005

6−rm -f reg005.java *.class

test/reg006/run_javadeleted−3

@@ -1,3 +0,0 @@

1−#!/bin/bash

2−idris $@ reg006.idr -o reg006.java --target Java

3−rm -f reg006.java *.class

test/reg011/expectednew file

No changes to the content.

test/reg011/reg011.idrnew file+10

@@ -0,0 +1,10 @@

1+vfoldl : (P : Nat -> Type) ->

2+ ((x : Nat) -> P x -> a -> P (S x)) -> P O

3+ -> Vect a m -> P m

4+-- vfoldl P cons nil []

5+-- = nil

6+vfoldl P cons nil (x :: xs)

7+ = vfoldl (\n => P (S n)) (\ n => cons (S n)) (cons O nil x) xs

8+%logging 0

9+-- vfoldl P cons nil (x :: xs)

10+-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

test/reg011/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg011.idr --check

3+rm -f *.ibc

test/reg012/expectednew file

No changes to the content.

test/reg012/reg012.lidrnew file+32

@@ -0,0 +1,32 @@

1+> total soElim : (C : (b : Bool) -> so b -> Type) ->

2+> C True oh ->

3+> (b : Bool) -> (s : so b) -> (C b s)

4+> soElim C coh .True .oh = coh

6+> soFalseElim : so False -> a

7+> soFalseElim x = FalseElim (soElim C () False x)

8+> where

9+> C : (b : Bool) -> so b -> Type

10+> C True s = ()

11+> C False s = _|_

12+

13+> soTrue : so b -> b = True

14+> soTrue {b = False} x = soFalseElim x

15+> soTrue {b = True} x = refl

16+

17+> class Eq alpha => ReflEqEq alpha where

18+> reflexive_eqeq : (a : alpha) -> so (a == a)

19+

20+> modifyFun : (Eq alpha) =>

21+> (alpha -> beta) ->

22+> (alpha, beta) ->

23+> (alpha -> beta)

24+> modifyFun f (a, b) a' = if a' == a then b else f a'

25+

26+> modifyFunLemma : (ReflEqEq alpha) =>

27+> (f : alpha -> beta) ->

28+> (ab : (alpha, beta)) ->

29+> modifyFun f ab (fst ab) = snd ab

30+> modifyFunLemma f (a,b) =

31+> replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

32+> (soTrue (reflexive_eqeq a)) refl

test/reg012/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg012.lidr --check

3+rm -f *.ibc

test/reg013/expectednew file+3

@@ -0,0 +1,3 @@

1+5

2+1

3+0

test/reg013/reg013.idrnew file+8

@@ -0,0 +1,8 @@

1+module Main

3+main : IO ()

4+main = do

5+ print $ prim_lenString "hallo"

6+ print $ prim_lenString "1"

7+ print $ prim_lenString ""

test/reg013/runnew file+4

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

1+#!/bin/bash

2+idris $@ reg013.idr -o reg013

3+./reg013

4+rm -f reg013 *.ibc

test/reg014/expectednew file

No changes to the content.

test/reg014/reg014.idrnew file+12

@@ -0,0 +1,12 @@

1+module reg014

3+Matrix : Type -> Nat -> Nat -> Type

4+Matrix a n m = Vect (Vect a m) n

6+transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

7+transpose ((x:: []) :: []) = [[x]]

8+transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])

9+transpose (x :: y :: xs)

10+ = let tx = transpose [x] in

11+ let ux = transpose (y :: xs) in zipWith (++) tx ux

12+

test/reg014/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg014.idr --check

3+rm -f *.ibc

test/runtest.pl+6−14

@@ -3,16 +3,12 @@

3my $exitstatus = 0;

5sub runtest {

6− my ($test, $update, $usejava) = @_;

6+ my ($test, $update) = @_;

8 chdir($test);

10 print "Running $test...";

11− if ($usejava == 1) {

12− $got = `sh ./run_java @idrOpts`;

13− } else {

14− $got = `sh ./run @idrOpts`;

11+ $got = `sh ./run @idrOpts`;

15− }

16 $exp = `cat expected`;

12 $exp = `cat expected`;

18 open(OUT,">output");

14 open(OUT,">output");

@@ -78,19 +74,15 @@ $usejava = 0;

79while ($opt=shift(@opts)) {

75while ($opt=shift(@opts)) {

80 if ($opt eq "-u") { $update = 1; }

76 if ($opt eq "-u") { $update = 1; }

81− if ($opt eq "-d") { $diff = 1; }

77+ elsif ($opt eq "-d") { $diff = 1; }

82− if ($opt eq "-s") { $show = 1; }

78+ elsif ($opt eq "-s") { $show = 1; }

83− if ($opt eq "--java") { $usejava = 1; }

79+ else { push(@idrOpts, $opt); }

84}

80}

86foreach $test (@tests) {

82foreach $test (@tests) {

88− if ($usejava == 1 && !(-e "$test/run_java")) {

89− next;

90− }

91−

92 if ($diff == 0 && $show == 0) {

84 if ($diff == 0 && $show == 0) {

93− runtest($test,$update, $usejava);

85+ runtest($test,$update);

94 }

86 }

95 else {

87 else {

96 chdir($test);

88 chdir($test);

test/test001/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test001.idr -o test001.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test001.java

5−java test001

6−rm -f test001.java *.class

test/test003/run_javadeleted−7

@@ -1,7 +0,0 @@

1−#!/bin/bash

2−idris $@ test003a.lidr -o test003a.java --target Java

3−idris $@ test003.lidr -o test003.java --target Java

4−export CLASSPATH=../../java/idris.jar:$CLASSPATH

5−javac test003.java

6−java test003

7−rm -f test003.java *.class

test/test004/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test004.idr -o test004.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test004.java

5−java test004

6−rm -f test004.java *.class

test/test005/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test005.idr -o test005.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test005.java

5−java test005

6−rm -f test005.java *.class

test/test006/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test006.idr -o test006.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test006.java

5−java test006

6−rm -f test006.java *.class

test/test007/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test007.idr -o test007.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test007.java

5−java test007

6−rm -f test007.java *.class

test/test008/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test008.idr -o test008.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test008.java

5−java test008

6−rm -f test008.java *.class

test/test009/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test009.idr -o test009.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test009.java

5−java test009

6−rm -f test009.java *.class

test/test010/run_javadeleted−5

@@ -1,5 +0,0 @@

1−#!/bin/bash

2−idris $@ test010.idr -o test010.java --target Java

3−idris $@ test010a.idr -o test010a.java --target Java

4−idris $@ test010b.idr -o test010b.java --target Java

5−rm -f test010.java *.class

test/test011/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test011.idr -o test011.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test011.java

5−java test011

6−rm -f test011.java *.class

test/test012/run_javadeleted−3

@@ -1,3 +0,0 @@

1−#!/bin/bash

2−idris $@ test012a.idr -o test012a.java --target Java

3−rm -f test012a.java *.class

test/test013/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test013.idr -o test013.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test013.java

5−java test013

6−rm -f test013.java *.class

test/test014/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test014.idr -o test014.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test014.java

5−java test014

6−rm -f test014.java *.class

test/test015/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test015.idr -o test015.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test015.java

5−java test015

6−rm -f test015.java *.class

test/test016/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test016.idr -o test016.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test016.java

5−java test016

6−rm -f test016.java *.class

test/test017/run_javadeleted−4

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

1−#!/bin/bash

2−idris $@ test017a.idr -o test017a.java --target Java

3−idris $@ test017b.idr -o test017b.java --target Java

4−rm -f *.class

test/test018/run_javadeleted−7

@@ -1,7 +0,0 @@

1−#!/bin/bash

2−idris $@ test018.idr -o test018.java --target Java

3−idris $@ test018a.idr -o test018a.java --target Java

4−export CLASSPATH=../../java/idris.jar:$CLASSPATH

5−javac test018.java

6−java test018

7−rm -f test018.java test018a.java *.class

test/test019/run_javadeleted−6

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

1−#!/bin/bash

2−idris $@ test019.lidr -o test019.java --target Java

3−export CLASSPATH=../../java/idris.jar:$CLASSPATH

4−javac test019.java

5−java test019

6−rm -f test019.java *.class

test/test020/run_javadeleted−7

@@ -1,7 +0,0 @@

1−#!/bin/bash

2−idris $@ test020.idr -o test020.java --target Java

3−idris $@ test020a.idr -o test020a.java --target Java

4−export CLASSPATH=../../java/idris.jar:$CLASSPATH

5−javac test020.java

6−java test020

7−rm -f test020.java *.class

test/test020/test020a.idr−1

@@ -16,4 +16,3 @@ foo xs = reverse xs

16main : IO ()

17main = print (foo [1,2,3])

19−

test/test021/run_javadeleted−9

@@ -1,9 +0,0 @@

1−#!/bin/bash

2−idris -p effects $@ test021.idr -o test021.java --target Java

3−idris -p effects $@ test021a.idr -o test021a.java --target Java

4−export CLASSPATH=../../java/idris.jar:$CLASSPATH

5−javac test021.java

6−java test021

7−javac test021a.java

8−java test021a

9−rm -f test021.java test021a.java *.class

tutorial/idris-tutorial.pdf

Binary file not shown.