9875894 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merged upstream changes

commit9875894dde2e2af91d27c4463219d969e348778d authorDavid Christiansen <david@davidchristiansen.dk> dateThu 21 Mar 2013, 16:19 (14 years ago) parent879769a 93819ed

91 files changed+1763−915

compare with master

unifiedsplit

CHANGELOG+14

@@ -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+

115New in 0.9.7:

216-------------

317

Makefile+6−6

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

11include config.mk

33install: .PHONY

4− $(CABAL) install

4+ $(CABAL) install $(CABALFLAGS)

66pinstall: .PHONY

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

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

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

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

1010build: .PHONY

11− $(CABAL) build

11+ $(CABAL) build $(CABALFLAGS)

1212

1313configure: .PHONY

14− $(CABAL) configure

14+ $(CABAL) configure $(CABALFLAGS)

1515

1616test : .PHONY

1717 make -C test

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

1919relib: .PHONY

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

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

22− $(CABAL) install

22+ $(CABAL) install $(CABALFLAGS)

2323

2424linecount : .PHONY

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

Setup.hs+69−6

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

11{-# LANGUAGE CPP #-}

2+import Control.Monad

3+import Data.IORef

25import Distribution.Simple

36import Distribution.Simple.InstallDirs as I

47import Distribution.Simple.LocalBuildInfo as L

58import qualified Distribution.Simple.Setup as S

69import qualified Distribution.Simple.Program as P

710import Distribution.PackageDescription

11+import Distribution.Text

812

913import System.Exit

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

15+import System.Directory

1116import qualified System.FilePath.Posix as Px

1217import System.Process

18+import qualified Data.Text as T

19+import qualified Data.Text.IO as TIO

1320

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

1522

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

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

1725

1826#ifdef mingw32_HOST_OS

1927-- make on mingw32 exepects unix style separators

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

21−idrisCmd local = Px.joinPath $ splitDirectories $

29+idrisCmd local = Px.joinPath $ splitDirectories $

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

2331#else

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

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

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

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

3038

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+

3147installStdLib pkg local verbosity copy

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

3349 let idir = datadir dirs

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

5167 , "IDRIS=" ++ icmd

5268 ]

5369

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+

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

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

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

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

79109 , "IDRIS=" ++ icmd

80110 ]

81111

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+

82129-- Install libraries during both copy and install

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

84−main = defaultMainWithHooks $ simpleUserHooks

131+main = do

132+ defaultMainWithHooks $ simpleUserHooks

85133 { 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

87136 (S.fromFlag $ S.copyDest flags)

88137 , 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

90140 NoCopyDest

141+ when (javaFlag $ configFlags lbi)

142+ (installJavaLib pkg

143+ lbi

144+ verb

145+ NoCopyDest

146+ (pkgVersion . package $ localPkgDescr lbi)

147+ )

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

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

150+ when (javaFlag $ configFlags lbi)

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

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

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

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

154+ cleanStdLib verb

155+ cleanJavaLib verb

95156 , 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)

97160 }

config.mk+3

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

11GMP_INCLUDE_DIR :=

22CC :=gcc

33CABAL :=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

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

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

1919

20−EXCEPTION : Type -> EFF

20+EXCEPTION : Type -> EFFECT

2121EXCEPTION t = MkEff () (Exception t)

2222

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

effects/Effect/File.idr+1−1

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

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

4141 k (FH h) e

4242

43−FILE_IO : Type -> EFF

43+FILE_IO : Type -> EFFECT

4444FILE_IO t = MkEff t FileIO

4545

4646open : Handler FileIO e =>

effects/Effect/Random.idr+1−1

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

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

1212 k seed' seed'

1313

14−RND : EFF

14+RND : EFFECT

1515RND = MkEff Int Random

1616

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

effects/Effect/Select.idr+1−1

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

1515instance Handler Selection List where

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

1717

18−SELECT : EFF

18+SELECT : EFFECT

1919SELECT = MkEff () Selection

2020

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

effects/Effect/State.idr+6−1

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

1313 handle st Get k = k st st

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

1515

16−STATE : Type -> EFF

16+STATE : Type -> EFFECT

1717STATE t = MkEff t State

1818

1919get : Eff m [STATE x] x

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

2929update f = do val <- get

3030 put (f val)

3131

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

3838

3939--- The Effect and associated functions

4040

41−STDIO : EFF

41+STDIO : EFFECT

4242STDIO = MkEff () StdIO

4343

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

effects/Effects.idr+10−10

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

1010Effect : Type

1111Effect = Type -> Type -> Type -> Type

1212

13−data EFF : Type where

14− MkEff : Type -> Effect -> EFF

13+data EFFECT : Type where

14+ MkEff : Type -> Effect -> EFFECT

1515

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

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

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

2828 subListId {xs = Nil} = SubNil

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

3030

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

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

3232 Nil : Env m Nil

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

3434

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

36− List EFF -> Type where

36+ List EFFECT -> Type where

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

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

3939

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

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

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

7575

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

77− List EFF

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

77+ List EFFECT

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

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

8080

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

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

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

8585

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

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

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

8888

8989private

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

9797-- the language of Effects

9898

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

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

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

101101 value : a -> EffM m xs xs a

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

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

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

114114 EffM m xs xs' a

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

116116

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

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

118118

119119implicit

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

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

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

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

194194

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

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

196196Eff m xs t = EffM m xs xs t

197197

198198-- 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.

4242 * Hugs style interactive environment

4343

4444Cabal-Version: >= 1.6

45+

46+

4547Build-type: Custom

4648

49+

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

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

4952 rts/libtest.c

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

6265 config.mk

6366 rts/*.c rts/*.h rts/Makefile

6467 js/*.js

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

6569

6670source-repository head

6771 type: git

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

6973

74+Flag Java

75+ Description: Build the Java RTS

76+ Default: False

77+

7078

7179Executable idris

7280 Main-is: Main.hs

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

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

100108 haskeline>=0.7, split, directory,

101109 containers, process, transformers, filepath,

102− directory, binary, bytestring, pretty,

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

103111 language-java>=0.2.2, libffi, unix

104112

105113 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 {

195195 public static int isNull(Object o) {

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

197197 }

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+ }

198214}

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)

115115unwords : List String -> String

116116unwords = pack . unwords' . map unpack

117117

118+length : String -> Nat

119+length = fromInteger . prim_lenString

120+

rts/Makefile+3−2

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

11include ../config.mk

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

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

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_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h idris_opts.h idris_stats.h

55CFLAGS = -O2 -Wall

67ifneq ($(GMP_INCLUDE_DIR),)

78 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

89endif

rts/idris_gc.c+21−21

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

5555void cheney(VM *vm) {

5656 int i;

5757 int ar;

58− char* scan = vm->heap;

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

5959

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

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

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

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

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

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

7676 }

7777 scan += inc;

7878 }

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

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

8080}

8181

8282void idris_gc(VM* vm) {

83+ HEAP_CHECK(vm)

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

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

8486

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

86− char* oldheap = vm -> heap;

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

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

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

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

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

8891

89− vm->heap = newheap;

90− vm->heap_next = newheap;

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

92−

93− vm->collections++;

92+ vm->heap.heap = newheap;

93+ vm->heap.next = newheap;

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

9495

9596 VAL* root;

9697

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

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

112113 // for next time.

113114

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

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

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

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

116117 }

117− vm->oldheap = oldheap;

118+ vm->heap.old = oldheap;

118119

119− // gcInfo(vm, 0);

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

121+ HEAP_CHECK(vm)

120122}

121123

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

123− printf("\nStack: %p %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));

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

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

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

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

128128 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));

130130}

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+

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

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

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

13+

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

315 _idris__123_runMain0_125_(vm, NULL);

4− //_idris_main(vm, NULL);

5−#ifdef IDRIS_TRACE

6− idris_gcInfo(vm, 1);

16+

17+#ifdef IDRIS_DEBUG

18+ if (opts.show_summary) {

19+ idris_gcInfo(vm, 1);

20+ }

721#endif

8− terminate(vm);

22+

23+ Stats stats = terminate(vm);

24+

25+ if (opts.show_summary) {

26+ print_stats(&stats);

27+ }

28+

29+ return EXIT_SUCCESS;

930}

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 @@

1010#include "idris_gc.h"

1111#include "idris_bitstring.h"

1212

13+

1314VM* init_vm(int stack_size, size_t heap_size,

1415 int max_threads, // not implemented yet

1516 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));

1917

2018 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+

2126 vm->valstack = valstack;

2227 vm->valstack_top = valstack;

2328 vm->valstack_base = valstack;

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

2631 vm->floatstack = floatstack;

2732 vm->floatstack_ptr = floatstack;

2833 vm->stack_max = valstack + stack_size;

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

30− vm->oldheap = NULL;

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;

34+

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

36+

3737 vm->ret = NULL;

3838 vm->reg1 = NULL;

3939

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

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

6161 }

6262

63+ STATS_LEAVE_INIT(vm->stats)

6364 return vm;

6465}

6566

66−void terminate(VM* vm) {

67+Stats terminate(VM* vm) {

68+ Stats stats = vm->stats;

69+ STATS_ENTER_EXIT(stats)

70+

6771 free(vm->inbox);

6872 free(vm->valstack);

6973 free(vm->intstack);

7074 free(vm->floatstack);

71− free(vm->heap);

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

7276 free(vm->argv);

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

77+

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

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

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

7781 free(vm);

82+

83+ STATS_LEAVE_EXIT(stats)

84+ return stats;

7885}

7986

8087void 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)) {

8289 idris_gc(vm);

8390 }

8491

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

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

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

108115 }

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

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

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

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

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

116+

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)

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

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

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

124+

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

126+

114127 memset(ptr, 0, size);

128+

115129 if (lock) { // not message passing

116130 pthread_mutex_unlock(&vm->alloc_lock);

117131 }

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

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

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

210224 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"); }

212226 printf("\n");

213227 }

214228 printf("RET: ");

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

401415 callvm->processes--;

402416

403417 free(td);

404− terminate(vm);

418+

419+ Stats stats = terminate(vm);

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

405421 return NULL;

406422}

407423

408424void* 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,

410426 callvm->max_threads,

411427 0, NULL);

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

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

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

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

495511

496− int gcs = dest->collections;

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

497513 pthread_mutex_lock(&dest->alloc_lock);

498514 VAL dmsg = copyTo(dest, msg);

499515 pthread_mutex_unlock(&dest->alloc_lock);

500516

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

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

502518 // a collection will have invalidated the copy

503519 pthread_mutex_lock(&dest->alloc_lock);

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

rts/idris_rts.h+9−10

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

99#include <pthread.h>

1010#include <stdint.h>

1111

12+#include "idris_heap.h"

13+#include "idris_stats.h"

14+

1215// Closures

1316

1417typedef enum {

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

4750 VAL* valstack_base;

4851 int* intstack_ptr;

4952 double* floatstack_ptr;

50− char* heap;

51− char* oldheap;

52− char* heap_next;

53− char* heap_end;

5453 VAL* stack_max;

55−

54+

55+ Heap heap;

56+

5657 pthread_mutex_t inbox_lock;

5758 pthread_mutex_t inbox_block;

5859 pthread_mutex_t alloc_lock;

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

6667

6768 int processes; // Number of child processes

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

70+

71+ Stats stats;

6972

7073 int argc;

7174 VAL* argv; // command line arguments

7275

73− size_t heap_size;

74− size_t heap_growth;

75− int allocations;

76− int collections;

7776 VAL ret;

7877 VAL reg1;

7978} VM;

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

8382 int max_threads,

8483 int argc, char* argv[]);

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

86−void terminate(VM* vm);

85+Stats terminate(VM* vm);

8786

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

8988// 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

167167

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

169169 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 []

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

172−simpleCase tc cover phase fc cs

178+ sc' tc cover phase fc cs

173179 = let proj = phase == RunTime

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

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

src/Core/Elaborate.hs+27−18

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

471471

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

473473simple_app fun arg =

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

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

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

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

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

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

478478 claim a RType

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

516516try' t1 t2 proofSearch

517517 = do s <- get

518518 ps <- get_probs

519− case prunStateT ps t1 s of

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

521− return v

519+ case prunStateT 999999 False ps t1 s of

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

521+ return v

522522 Error e1 -> if recoverableErr e1 then

523523 do case runStateT t2 s of

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

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

539539

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

541541tryAll :: [(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)

543543 where

544544 cantResolve :: Elab' aux a

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

546546

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

548+ Int -> -- most problems

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

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

550551 Elab' aux a

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

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

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

554− tryAll' cs f (x:xs)

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

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

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

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

555556 = do s <- get

556557 ps <- get_probs

557− case prunStateT ps x s of

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

559− return v):cs) f xs

558+ case prunStateT pmax True ps x s of

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

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

560564 Error err -> do put s

561565 if (score err) < 100

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

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

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

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

564568

565569

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

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

568572 else (f, i)

569573

570−prunStateT ps x s

574+prunStateT pmax zok ps x s

571575 = case runStateT x s of

572576 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))

574580 then case reverse (problems p) of

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

576− else OK (v, s')

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

577583 Error e -> Error e

578584

585+qshow :: Fails -> String

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

587+

579588dumpprobs [] = ""

580589dumpprobs ((_,_,_,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)

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

156156unify' ctxt env topx topy =

157157 do ps <- get

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

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

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

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

158+ let dont = dontunify ps

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

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

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

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

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

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

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

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

162167 case fails of

163168-- [] -> return u

164169 err ->

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

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

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

398403 instantiate val (pToV x sc)

399− | otherwise = do ps <- get

400− lift $ tfail $ IncompleteTerm val

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

404+ | otherwise = lift $ tfail $ IncompleteTerm val

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

406+ = do ps <- get

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

403408

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

src/Core/Unify.hs+64−11

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

2929

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

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

32−unify ctxt env topx topy injtc holes =

32+unify ctxt env topx topy dont holes =

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

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

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

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

5454

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

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

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

58− injective (App f a) = injective f

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

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

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

5960 injective _ = False

6061

6162 notP (P _ _ _) = False

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

9495 = unifyFail topx topy

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

9697 = 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

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

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

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

100− = unifyFail tx ty

105+ = unifyTmpFail tx ty

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

102− = unifyFail tx ty

107+ = unifyTmpFail tx ty

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

104109 | holeIn env x || x `elem` holes

105110 = do UI s f <- get

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

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

129134

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

131− | injective fx && metavarApp appy

132− || injective fy && metavarApp appx

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

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

133138 || injective fx && injective fy

134139 || fx == fy

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

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

158163 let (heady, argsy) = unApply appy

159164 if (length argsx == length argsy &&

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

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

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

167+ then

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

162169 do uf <- un' True bnames headx heady

163170 unArgs uf argsx argsy

164171 else unifyTmpFail appx appy

165172 where hnormalise [] _ _ t = t

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

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

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

168175 | x /= y = unifyFail appx appy

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

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

183190 unArgs vs xs ys

184191

185192 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+

187219 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)

189222 _ -> False

223+ pat t = case t of

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

225+ _ -> False

190226 inenv t = case t of

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

192228 _ -> False

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

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

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

199235 | 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

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

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

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

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

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

286326 | x == y = True

287327 | 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

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

289333 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

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

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

292338 recoverable (App f a) (App f' a')

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

298344holeIn :: Env -> Name -> Bool

299345holeIn env n = case lookup n env of

300346 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

301354 _ -> False

302355

src/IRTS/CodegenJava.hs+755−591

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

1111import Control.Applicative

1212import Control.Arrow

1313import Control.Monad

14+import qualified Control.Monad.Trans as T

15+import Control.Monad.Trans.State

1416import Data.Char

1517import Data.Maybe (fromJust)

18+import Data.List (isPrefixOf, intercalate)

19+import qualified Data.Text as T

20+import qualified Data.Text.IO as TIO

1621import Language.Java.Parser

1722import Language.Java.Pretty

1823import Language.Java.Syntax hiding (Name)

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

2328import System.IO

2429import System.Process

2530

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

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

32+

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

34+

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

36+ [(Name, SDecl)] ->

2737 FilePath -> -- output file name

2838 OutputType ->

2939 IO ()

30−codegenJava defs out exec =

31− either (error)

32− (writeFile out . flatIndent . prettyPrint)

33− (mkCompilationUnit defs out)

34−

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

36− FilePath ->

37− Either String CompilationUnit

38−mkCompilationUnit defs out =

40+codegenJava globalInit defs out exec = do

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

48+ (flatIndent . prettyPrint)

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

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+

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

107+mkCompilationUnit globalInit defs out =

39108 CompilationUnit Nothing [ ImportDecl False idrisRts True

40109 , ImportDecl True idrisForeign True

41110 , ImportDecl False bigInteger False

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

44113 , ImportDecl False scanner False

45114 , ImportDecl False arrays False

46115 ] <$>

47− mkTypeDecl defs out

116+ mkTypeDecl globalInit defs out

48117 where

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

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

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

75144prefixCallNamespacesDecl :: Ident -> SDecl -> SDecl

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

77146

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

79− FilePath ->

80− Either String [TypeDecl]

81−mkTypeDecl defs out =

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

148+mkTypeDecl globalInit defs out =

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

83150 , Annotation $ SingleElementAnnotation

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

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

91158 body])

92159 <$> mkClassName out

93160 <*> ( mkClassName out

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

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

95162 )

96163

97−mkClassName :: FilePath -> Either String Ident

164+mkClassName :: FilePath -> CodeGeneration Ident

98165mkClassName path =

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

100− (parser ident . takeBaseName $ takeFileName path)

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

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

101186

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

103− Either String ClassBody

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

105− <$> mapM mkDecl defs

187+

106188

107189addMainMethod :: [Decl] -> [Decl]

108190addMainMethod decls

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

160242 mergeInner [] decl' = [decl']

161243

162244

163−mkIdentifier :: Name -> Either String Ident

245+mkIdentifier :: Name -> CodeGeneration Ident

164246mkIdentifier (NS name _) = mkIdentifier name

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

166248 <$> mkIdentifier (UN name)

167249mkIdentifier (UN name) =

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

169− ( parser ident

170− . cleanReserved

171− . cleanNonLetter

172− . cleanStart

173− $ cleanWs False name)

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

251+ ( parser ident

252+ . cleanReserved

253+ . cleanNonLetter

254+ . cleanStart

255+ $ cleanWs False name)

174256 where

175257 cleanStart (x:xs)

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

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

207289

208290

209291 cleanReserved "param" = "_param"

292+ cleanReserved "globalContext" = "_globalContext"

210293 cleanReserved "context" = "_context"

211294 cleanReserved "newcontext" = "_newcontext"

212295

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

300383 cleanReserved "fputStr" = "_fputStr"

301384 cleanReserved "fileEOF" = "_fileEOF"

302385 cleanReserved "isNull" = "_isNull"

386+ cleanReserved "idris_K" = "_idris_K"

387+ cleanReserved "idris_flipK" = "_idris_flipK"

388+ cleanReserved "idris_assignStack" = "_idris_assignStack"

303389

304390 cleanReserved x = x

305391

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

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

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

308394 <$> mkIdentifier name

309395 <*> mapM (mkIdentifier . UN) nss

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

330416idrisObjectType :: ClassType

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

332418

333−contextArray :: Exp

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

419+contextArray :: LVar -> Exp

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

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

335422

336423charType :: ClassType

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

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

369456comparableType :: ClassType

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

371458

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

373− Either String Decl

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

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

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

376462 <$> mkIdentifier (UN ns)

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

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

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

379− (\ name params cont ->

465+ (\ name params paramNames methodBody ->

380466 MemberDecl $ MethodDecl [Public, Static]

381467 []

382468 (Just . RefType $ ClassRefType objectType)

383469 name

384470 params

385471 []

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

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

472+ (MethodBody . Just $ Block

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+ )

388483 )

389484 <$> mkIdentifier name

390485 <*> mapM mkFormalParam params

391− <*> mkClosure params stackSize body

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

487+ <*> mkExp body

392488

393489

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

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

395491mkClosure params stackSize body =

396492 (\ paramArray body ->

397493 InstanceCreation []

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

402498 <$> mkStackInit params stackSize

403499 <*> mkClosureCall body

404500

405−mkFormalParam :: Name -> Either String FormalParam

501+mkFormalParam :: Name -> CodeGeneration FormalParam

406502mkFormalParam name =

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

408504 <$> mkIdentifier name

409505

410−mkClosureCall :: SExp -> Either String Decl

506+mkClosureCall :: SExp -> CodeGeneration Decl

411507mkClosureCall body =

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

413509 <$> mkMethodBody body

414510

415−mkMethodBody :: SExp -> Either String MethodBody

511+mkMethodBody :: SExp -> CodeGeneration MethodBody

416512mkMethodBody exp =

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

418514 <$> mkExp exp

419515

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

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

421517mkStackInit params stackSize =

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

423519 (map (InitExp . ExpName) localVars)

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

425521 <$> mapM mkName params

426522

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

428−mkAnonymousLetBinding var oldExp newExp =

429− (\ bindingMethod newExp ->

430− MethodInv $ PrimaryMethodCall

431− ( MethodInv $ PrimaryMethodCall ( InstanceCreation []

432− objectType

433− []

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

435− )

436− []

437− (Ident "apply")

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"] ]

476− (Just $ ClassBody [oldCall])

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

524+mkK result drop =

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

526+

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

528+mkFlipK drop result =

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

530+

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

532+mkLet (Loc pos) oldExp newExp =

533+ (\ oldExp newExp ->

534+ mkFlipK ( Assign ( ArrayLhs $ ArrayIndex (ExpName $ J.Name [Ident "context"])

535+ (Lit $ Int (toInteger pos)))

536+ EqualA

537+ newExp

538+ )

539+ oldExp

477540 )

478− <$> mkClosureCall oldExp

479−

480−

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

541+ <$> mkExp oldExp

542+ <*> mkExp newExp

543+mkLet (Glob _) _ _ = T.lift $ Left "Cannot let bind to global variable"

498544

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−

520545reverseNameSpace :: J.Name -> J.Name

521546reverseNameSpace (J.Name ids) =

522547 J.Name ((tail ids) ++ [head ids])

523548

524−mkCase :: Bool -> LVar -> [SAlt] -> Either String Exp

549+mkCase :: Bool -> LVar -> [SAlt] -> CodeGeneration Exp

525550mkCase checked var ((SConCase parentStackPos consIndex _ params branchExpression):cases) =

526551 mkConsCase checked

527552 var

@@ -531,11 +556,11 @@ mkCase checked var ((SConCase parentStackPos consIndex _ params branchExpression

531556 branchExpression

532557 (SCase var cases)

533558mkCase checked var (c@(SConstCase constant branchExpression):cases) =

534− (\ constant branchExpression alternative ->

559+ (\ constant branchExpression alternative var->

535560 Cond ( MethodInv $ PrimaryMethodCall (constant)

536561 []

537562 (Ident "equals")

538− [mkVarAccess Nothing var]

563+ [var]

539564 )

540565 branchExpression

541566 alternative

@@ -543,10 +568,11 @@ mkCase checked var (c@(SConstCase constant branchExpression):cases) =

543568 <$> mkExp (SConst constant)

544569 <*> mkExp branchExpression

545570 <*> mkCase checked var cases

571+ <*> mkVarAccess Nothing var

546572mkCase checked var (SDefaultCase exp:cases) = mkExp exp

547573mkCase checked _ [] = mkExp (SError "Non-exhaustive pattern")

548574

549−mkConsCase :: Bool -> LVar -> Int -> Int -> [Name] -> SExp -> SExp -> Either String Exp

575+mkConsCase :: Bool -> LVar -> Int -> Int -> [Name] -> SExp -> SExp -> CodeGeneration Exp

550576mkConsCase checked

551577 toDeconstruct

552578 parentStackStart

@@ -554,13 +580,13 @@ mkConsCase checked

554580 params

555581 branchExpression

556582 alternative =

557− (\ caseBinding alternative->

558− Cond (BinOp (InstanceOf (mkVarAccess Nothing toDeconstruct)

583+ (\ caseBinding alternative var varCasted->

584+ Cond (BinOp (InstanceOf (var)

559585 (ClassRefType idrisObjectType)

560586 )

561587 CAnd

562588 ( BinOp

563− ( MethodInv $ PrimaryMethodCall (mkVarAccess (Just idrisObjectType) toDeconstruct)

589+ ( MethodInv $ PrimaryMethodCall (varCasted)

564590 []

565591 (Ident "getConstructorId")

566592 []

@@ -574,11 +600,24 @@ mkConsCase checked

574600 )

575601 <$> mkCaseBinding checked toDeconstruct parentStackStart params branchExpression

576602 <*> mkExp alternative

577−

578−

579−mkCaseBinding :: Bool -> LVar -> Int -> [Name] -> SExp -> Either String Exp

580−mkCaseBinding checked var parentStackStart params branchExpression =

581− (\ bindingMethod ->

603+ <*> mkVarAccess (Nothing) toDeconstruct

604+ <*> mkVarAccess (Just idrisObjectType) toDeconstruct

605+

606+

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

619+mkCaseBinding False var parentStackStart params branchExpression =

620+ (\ bindingMethod deconstruction ->

582621 MethodInv $ PrimaryMethodCall

583622 ( MethodInv $ PrimaryMethodCall (InstanceCreation []

584623 (ClassType [(Ident "Object", [])])

@@ -587,20 +626,21 @@ mkCaseBinding checked var parentStackStart params branchExpression =

587626 )

588627 []

589628 (Ident "apply")

590− ( contextArray

591− : (mkCaseBindingDeconstruction var params)

592− )

629+ ( contextArray (Loc undefined) : deconstruction )

593630 )

594631 []

595632 (Ident "call")

596633 []

597634 )

598− <$> mkCaseBindingMethod checked parentStackStart params branchExpression

599−

635+ <$> mkCaseBindingMethod parentStackStart params branchExpression

636+ <*> mkCaseBindingDeconstruction var params

600637

638+mkCaseBindingDeconstruction :: LVar -> [Name] -> CodeGeneration [Exp]

639+mkCaseBindingDeconstruction var members =

640+ mapM (mkProjection var) ([0..(length members - 1)])

601641

602−mkCaseBindingMethod :: Bool -> Int -> [Name] -> SExp -> Either String MemberDecl

603−mkCaseBindingMethod checked parentStackStart params branchExpression =

642+mkCaseBindingMethod :: Int -> [Name] -> SExp -> CodeGeneration MemberDecl

643+mkCaseBindingMethod parentStackStart params branchExpression =

604644 (\ formalParams caseBindingStack branchExpression ->

605645 MethodDecl [Final, Public]

606646 []

@@ -612,22 +652,74 @@ mkCaseBindingMethod checked parentStackStart params branchExpression =

612652 caseBindingStack ++

613653 [BlockStmt . Return $ Just branchExpression]))

614654 <$> mapM mkFormalParam params

615− <*> mkBindingStack checked parentStackStart params

655+ <*> mkBindingStack False parentStackStart params

616656 <*> mkBindingClosure branchExpression

617657

618−mkCaseBindingDeconstruction :: LVar -> [Name] -> [Exp]

619−mkCaseBindingDeconstruction var members =

620− map (mkProjection var) ([0..(length members - 1)])

658+mkContextParam :: FormalParam

659+mkContextParam =

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

621690

622−mkProjection :: LVar -> Int -> Exp

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+

712+mkProjection :: LVar -> Int -> CodeGeneration Exp

623713mkProjection var memberNr =

624− ArrayAccess $ ArrayIndex ( MethodInv $ PrimaryMethodCall

625− (mkVarAccess (Just idrisObjectType) var)

626− []

627− (Ident "getData")

628− []

629− )

630− (Lit $ Int (toInteger memberNr))

714+ (\ var -> ArrayAccess $ ArrayIndex ( MethodInv $ PrimaryMethodCall

715+ (var)

716+ []

717+ (Ident "getData")

718+ []

719+ )

720+ (Lit $ Int (toInteger memberNr))

721+ )

722+ <$> mkVarAccess (Just idrisObjectType) var

631723

632724type ClassName = String

633725

@@ -642,22 +734,22 @@ mkClass :: ClassType -> Exp

642734mkClass classType =

643735 ClassLit . Just . RefType .ClassRefType $ classType

644736

645−mkBinOpExp :: ClassType -> Op -> [LVar] -> Exp

646−mkBinOpExp castTo op (var:vars) =

647− foldl (\ exp -> BinOp exp op . mkVarAccess (Just castTo))

648− (mkVarAccess (Just castTo) var)

737+mkBinOpExp :: ClassType -> Op -> [LVar] -> CodeGeneration Exp

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

748+ <$> mkVarAccess (Just castTo) var)

749+ start

649750 vars

650751

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

661753mkBinOpExpConv fromMethodName toType fromType@(ClassType [(cls@(Ident _), [])]) op args =

662754 mkBinOpExpTrans (\ exp -> MethodInv $ TypeMethodCall (J.Name [cls])

663755 []

@@ -673,59 +765,70 @@ mkBinOpExpConv fromMethodName toType fromType@(ClassType [(cls@(Ident _), [])])

673765 op

674766 args

675767

676−mkLogicalBinOpExp :: ClassType -> Op -> [LVar] -> Exp

677−mkLogicalBinOpExp castTo op (var:vars) =

678− foldl (\ exp -> mkBoolToNumber castTo . BinOp exp op . mkVarAccess (Just castTo))

679− (mkVarAccess (Just castTo) var)

768+mkLogicalBinOpExp :: ClassType -> Op -> [LVar] -> CodeGeneration Exp

769+mkLogicalBinOpExp castTo op (var:vars) = do

770+ start <- mkVarAccess (Just castTo) var

771+ foldM (\ exp var -> mkBoolToNumber castTo . BinOp exp op <$> mkVarAccess (Just castTo) var)

772+ start

680773 vars

681774

682−mkMethodOpChain1 :: (Exp -> Exp) -> ClassType -> String -> [LVar] -> Exp

775+mkMethodOpChain1 :: (Exp -> Exp) -> ClassType -> String -> [LVar] -> CodeGeneration Exp

683776mkMethodOpChain1 = mkMethodOpChain id

684777

685−mkMethodOpChain :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> String -> [LVar] -> Exp

686−mkMethodOpChain initialTransformation resultTransformation castTo method (arg:args) =

687− foldl (\ exp arg' ->

688− resultTransformation . MethodInv $ PrimaryMethodCall exp

689− []

690− (Ident method)

691− [mkVarAccess (Just $ castTo) arg']

778+mkMethodOpChain :: (Exp -> Exp) -> (Exp -> Exp) -> ClassType -> String -> [LVar] -> CodeGeneration Exp

779+mkMethodOpChain initialTransformation resultTransformation castTo method (arg:args) = do

780+ start <- initialTransformation <$> mkVarAccess (Just $ castTo) arg

781+ foldM (\ exp arg' ->

782+ resultTransformation

783+ . MethodInv

784+ . PrimaryMethodCall exp [] (Ident method)

785+ . (:[])

786+ <$> mkVarAccess (Just $ castTo) arg'

692787 )

693− (initialTransformation (mkVarAccess (Just $ castTo) arg))

788+ start

694789 args

695790

696791mkBoolToNumber :: ClassType -> Exp -> Exp

697792mkBoolToNumber (ClassType [(Ident name, [])]) boolExp =

698793 Cond boolExp (mkPrimitive name (Int 1)) (mkPrimitive name (Int 0))

699794

700−mkZeroExt :: String -> Int -> ClassType -> ClassType -> LVar -> Exp

701−mkZeroExt toMethod bits fromType toType@(ClassType [(toTypeName, [])]) var =

702− MethodInv $ TypeMethodCall (J.Name [toTypeName])

703− []

704− (Ident "valueOf")

705− [ Cond ( BinOp (mkVarAccess (Just $ fromType) var)

706− LThan

707− (Lit $ Int 0)

708− )

709− ( BinOp (Lit $ Int (2^bits))

710− Add

711− (mkSignedExt' toMethod fromType var)

712− )

713− (mkSignedExt' toMethod fromType var)

714− ]

795+mkZeroExt :: String -> Int -> ClassType -> ClassType -> LVar -> CodeGeneration Exp

796+mkZeroExt toMethod bits fromType toType@(ClassType [(toTypeName, [])]) var = do

797+ (\ var sext ->

798+ MethodInv $ TypeMethodCall (J.Name [toTypeName])

799+ []

800+ (Ident "valueOf")

801+ [ Cond ( BinOp (var)

802+ LThan

803+ (Lit $ Int 0)

804+ )

805+ ( BinOp (Lit $ Int (2^bits))

806+ Add

807+ (sext)

808+ )

809+ sext

810+ ]

811+ )

812+ <$> mkVarAccess (Just $ fromType) var

813+ <*> mkSignedExt' toMethod fromType var

715814

716−mkSignedExt :: String -> ClassType -> ClassType -> LVar -> Exp

815+mkSignedExt :: String -> ClassType -> ClassType -> LVar -> CodeGeneration Exp

717816mkSignedExt toMethod fromType (ClassType [(toTypeName, [])]) var =

718− MethodInv $ TypeMethodCall (J.Name [toTypeName])

719− []

720− (Ident "valueOf")

721− [ mkSignedExt' toMethod fromType var ]

817+ (\ sext -> MethodInv $ TypeMethodCall (J.Name [toTypeName])

818+ []

819+ (Ident "valueOf")

820+ [ sext ]

821+ )

822+ <$> mkSignedExt' toMethod fromType var

722823

723−mkSignedExt' :: String -> ClassType -> LVar -> Exp

824+mkSignedExt' :: String -> ClassType -> LVar -> CodeGeneration Exp

724825mkSignedExt' toMethod fromType var =

725− MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ fromType) var)

726− []

727− (Ident toMethod)

728− []

826+ (\ var -> MethodInv $ PrimaryMethodCall (var)

827+ []

828+ (Ident toMethod)

829+ []

830+ )

831+ <$> mkVarAccess (Just $ fromType) var

729832

730833data SPartialOrder

731834 = SLt

@@ -747,26 +850,39 @@ mkPartialOrder SGe x =

747850 (BinOp (Lit $ Int 0) Equal x)

748851mkPartialOrder SGt x = (BinOp (Lit $ Int 1) Equal x)

749852

750−mkVarAccess :: Maybe ClassType -> LVar -> Exp

751−mkVarAccess Nothing (Loc i) =

752− ArrayAccess $ ArrayIndex contextArray (Lit $ Int (toInteger i))

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+

861+mkVarAccess :: Maybe ClassType -> LVar -> CodeGeneration Exp

862+mkVarAccess Nothing var =

863+ (\ pos -> ArrayAccess $ ArrayIndex (contextArray var) (Lit $ Int pos))

864+ <$> varPos var

753865mkVarAccess (Just castTo) var =

754− Cast (RefType . ClassRefType $ castTo) (mkVarAccess Nothing var)

866+ Cast (RefType . ClassRefType $ castTo) <$> (mkVarAccess Nothing var)

755867

756−mkPrimitiveCast :: ClassType -> ClassType -> LVar -> Exp

868+mkPrimitiveCast :: ClassType -> ClassType -> LVar -> CodeGeneration Exp

757869mkPrimitiveCast fromType (ClassType [(toType, [])]) var =

758− 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")

870+ (\ var ->

871+ MethodInv $ TypeMethodCall (J.Name [toType])

768872 []

873+ (Ident "valueOf")

874+ [var]

875+ )

876+ <$> mkVarAccess (Just fromType) var

769877

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

770886data Std = In | Out | Err

771887

772888instance Show Std where

@@ -784,49 +900,57 @@ mkSystemOutPrint value =

784900 (Ident "print")

785901 [value]

786902

787−mkMathFun :: String -> LVar -> Exp

903+mkMathFun :: String -> LVar -> CodeGeneration Exp

788904mkMathFun funName var =

789− MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

790− []

791− (Ident "valueOf")

792− [ MethodInv $ TypeMethodCall (J.Name [Ident "Math"])

793− []

794− (Ident funName)

795− [mkVarAccess (Just doubleType) var]

796− ]

905+ (\ var -> MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

906+ []

907+ (Ident "valueOf")

908+ [ MethodInv $ TypeMethodCall (J.Name [Ident "Math"])

909+ []

910+ (Ident funName)

911+ [var]

912+ ]

913+ )

914+ <$> mkVarAccess (Just doubleType) var

797915

798−mkStringAtIndex :: LVar -> Exp -> Exp

916+mkStringAtIndex :: LVar -> Exp -> CodeGeneration Exp

799917mkStringAtIndex var indexExp =

800− MethodInv $ TypeMethodCall (J.Name [Ident "Integer"])

801− []

802− (Ident "valueOf")

803− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) var)

804− []

805− (Ident "charAt")

806− [indexExp]

807− ]

918+ (\ var -> MethodInv $ TypeMethodCall (J.Name [Ident "Integer"])

919+ []

920+ (Ident "valueOf")

921+ [ MethodInv $ PrimaryMethodCall (var)

922+ []

923+ (Ident "charAt")

924+ [indexExp]

925+ ]

926+ )

927+ <$> mkVarAccess (Just stringType) var

808928

809929mkForeignType :: FType -> Maybe ClassType

810−mkForeignType FInt = return $ integerType

811−mkForeignType FChar = return $ integerType

812−mkForeignType FString = return $ stringType

813−mkForeignType FPtr = return $ objectType

814−mkForeignType FDouble = return $ doubleType

815−mkForeignType FAny = return $ objectType

930+mkForeignType FInt = return integerType

931+mkForeignType FChar = return integerType

932+mkForeignType FString = return stringType

933+mkForeignType FPtr = return objectType

934+mkForeignType FDouble = return doubleType

935+mkForeignType FAny = return objectType

816936mkForeignType FUnit = Nothing

817937

818−mkForeignVarAccess :: FType -> LVar -> Exp

938+mkForeignVarAccess :: FType -> LVar -> CodeGeneration Exp

819939mkForeignVarAccess FInt var =

820− MethodInv $ PrimaryMethodCall (mkVarAccess (Just integerType) var)

821− []

822− (Ident "intValue")

823− []

824−mkForeignVarAccess FChar var = Cast (PrimType CharT) (mkForeignVarAccess FInt var)

940+ (\ var -> MethodInv $ PrimaryMethodCall (var)

941+ []

942+ (Ident "intValue")

943+ []

944+ )

945+ <$> mkVarAccess (Just integerType) var

946+mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess FInt var

825947mkForeignVarAccess FDouble var =

826− MethodInv $ PrimaryMethodCall (mkVarAccess (Just doubleType) var)

827− []

828− (Ident "doubleValue")

829− []

948+ (\ var -> MethodInv $ PrimaryMethodCall (var)

949+ []

950+ (Ident "doubleValue")

951+ []

952+ )

953+ <$> mkVarAccess (Just doubleType) var

830954mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

831955

832956mkFromForeignType :: FType -> Exp -> Exp

@@ -843,7 +967,7 @@ mkFromForeignType FDouble from =

843967 [from]

844968mkFromForeignType _ from = from

845969

846−mkForeignInvoke :: FType -> String -> [(FType, LVar)] -> Either String Exp

970+mkForeignInvoke :: FType -> String -> [(FType, LVar)] -> CodeGeneration Exp

847971mkForeignInvoke fType method args =

848972 (\ foreignInvokeMeth ->

849973 MethodInv $ PrimaryMethodCall (InstanceCreation []

@@ -858,7 +982,7 @@ mkForeignInvoke fType method args =

858982 <$> mkForeignInvokeMethod fType method args

859983

860984

861−mkForeignInvokeMethod :: FType -> String -> [(FType, LVar)] -> Either String MemberDecl

985+mkForeignInvokeMethod :: FType -> String -> [(FType, LVar)] -> CodeGeneration MemberDecl

862986mkForeignInvokeMethod fType method args =

863987 (\ tryBlock ->

864988 MethodDecl [Public, Final]

@@ -867,111 +991,124 @@ mkForeignInvokeMethod fType method args =

867991 (Ident "foreignInvoke")

868992 []

869993 []

870− (MethodBody . Just $ Block [ BlockStmt $

871− Try tryBlock

872− [ Catch (FormalParam []

873− (RefType $ ClassRefType exceptionType)

874− False

875− (VarId $ Ident "ex")

876− )

877− (Block [ BlockStmt . Throw $

878− InstanceCreation []

879− runtimeExceptionType

880− [ExpName $ J.Name [Ident "ex"]]

881− Nothing

882− ]

883− )

884− ]

885− Nothing

886− ]

994+ (MethodBody . Just $ Block

995+ [ BlockStmt

996+ $ Try tryBlock

997+ [ Catch (FormalParam []

998+ (RefType $ ClassRefType exceptionType)

999+ False

1000+ (VarId $ Ident "ex")

1001+ )

1002+ (Block [ BlockStmt

1003+ . Throw

1004+ $ InstanceCreation []

1005+ runtimeExceptionType

1006+ [ExpName $ J.Name [Ident "ex"]]

1007+ Nothing

1008+ ]

1009+ )

1010+ ]

1011+ Nothing

1012+ ]

8871013 )

888− )

1014+ )

8891015 <$> mkForeignInvokeTryBlock fType method args

8901016

8911017

892−mkForeignInvokeTryBlock :: FType -> String -> [(FType, LVar)] -> Either String Block

1018+mkForeignInvokeTryBlock :: FType -> String -> [(FType, LVar)] -> CodeGeneration Block

8931019mkForeignInvokeTryBlock FUnit method args =

894− (\ method -> Block [ BlockStmt . ExpStmt . MethodInv $

895− MethodCall method

896− (map (uncurry mkForeignVarAccess) args)

897− , BlockStmt $ Return (Just $ Lit Null)

898− ]

1020+ (\ method args -> Block [ BlockStmt . ExpStmt . MethodInv $ MethodCall method args

1021+ , BlockStmt $ Return (Just $ Lit Null)

1022+ ]

8991023 )

900− <$> ( left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

901− (parser name method)

1024+ <$> ( T.lift $ left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

1025+ (parser name method)

9021026 )

1027+ <*> mapM (uncurry mkForeignVarAccess) args

9031028mkForeignInvokeTryBlock fType method args =

904− (\ method -> Block [ BlockStmt . Return

1029+ (\ method args -> Block [ BlockStmt . Return

9051030 . Just

9061031 . mkFromForeignType fType

907− . MethodInv $

908− MethodCall method

909− (map (uncurry mkForeignVarAccess) args)

910− ]

1032+ . MethodInv

1033+ $ MethodCall method args

1034+ ]

9111035 )

912− <$> ( left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

913− (parser name method)

1036+ <$> ( T.lift $ left (\ err -> "Error parsing name \"" ++ method ++ "\" :" ++ (show err))

1037+ (parser name method)

9141038 )

1039+ <*> mapM (uncurry mkForeignVarAccess) args

9151040

916−mkMethodClosure :: Name -> [LVar] -> Either String Exp

1041+mkMethodClosure :: Name -> [LVar] -> CodeGeneration Exp

9171042mkMethodClosure name args =

9181043 (\ name args ->

9191044 InstanceCreation []

9201045 idrisClosureType

9211046 [ (ExpName $ J.Name [Ident "context"]) ]

922− ( Just $ ClassBody

923− [ MemberDecl $

924− MethodDecl [Public, Final]

925− []

926− (Just . RefType $ ClassRefType objectType)

927− (Ident "call")

928− []

929− []

930− ( MethodBody . Just $

931− Block [ BlockStmt . Return . Just . MethodInv $

932− MethodCall (reverseNameSpace name)

933− args

934− ]

935− )

936− ]

937− )

1047+ ( Just

1048+ $ ClassBody

1049+ [ MemberDecl

1050+ $ MethodDecl [Public, Final]

1051+ []

1052+ (Just . RefType $ ClassRefType objectType)

1053+ (Ident "call")

1054+ []

1055+ []

1056+ ( MethodBody

1057+ . Just

1058+ $ Block [ BlockStmt

1059+ . Return

1060+ . Just

1061+ . MethodInv

1062+ $ MethodCall (reverseNameSpace name)

1063+ args

1064+ ]

1065+ )

1066+ ]

1067+ )

9381068 )

9391069 <$> mkName name

9401070 <*> mapM (mkExp . SV) args

9411071

942−mkThread :: LVar -> Either String Exp

1072+mkThread :: LVar -> CodeGeneration Exp

9431073mkThread arg =

944− (\ eval -> MethodInv $

945− PrimaryMethodCall (InstanceCreation []

946− (ClassType [(Ident "Thread", [])])

947− [ eval ]

948− ( Just $ ClassBody

949− [ MemberDecl $ MethodDecl

950− [Public, Final]

951− []

952− (Just . RefType $ ClassRefType objectType)

953− (Ident "_start")

954− []

955− []

956− ( MethodBody . Just $ Block

957− [ BlockStmt . ExpStmt . MethodInv $ MethodCall

958− (J.Name [Ident "start"])

959− []

960− , BlockStmt . Return . Just $ This

1074+ (\ eval ->

1075+ MethodInv

1076+ $ PrimaryMethodCall (InstanceCreation []

1077+ (ClassType [(Ident "Thread", [])])

1078+ [ eval ]

1079+ ( Just

1080+ $ ClassBody [ MemberDecl

1081+ $ MethodDecl [Public, Final]

1082+ []

1083+ (Just . RefType $ ClassRefType objectType)

1084+ (Ident "_start")

1085+ []

1086+ []

1087+ ( MethodBody

1088+ . Just

1089+ $ Block [ BlockStmt

1090+ . ExpStmt

1091+ . MethodInv

1092+ $ MethodCall (J.Name [Ident "start"])

1093+ []

1094+ , BlockStmt

1095+ . Return

1096+ . Just

1097+ $ This

9611098 ]

962− )

963− ]

964− )

965− )

966− []

967− (Ident "_start")

968− []

1099+ )

1100+ ]

1101+ )

1102+ )

1103+ []

1104+ (Ident "_start")

1105+ []

9691106 )

9701107 <$> mkThreadBinding arg

9711108

972−mkThreadBinding :: LVar -> Either String Exp

1109+mkThreadBinding :: LVar -> CodeGeneration Exp

9731110mkThreadBinding var =

974− (\ bindingMethod ->

1111+ (\ bindingMethod var ->

9751112 MethodInv $ PrimaryMethodCall ( InstanceCreation []

9761113 objectType

9771114 []

@@ -979,12 +1116,13 @@ mkThreadBinding var =

9791116 )

9801117 []

9811118 (Ident "apply")

982− [ mkVarAccess Nothing var ]

983− )

1119+ [ var ]

1120+ )

9841121 <$> mkThreadBindingMethod

1122+ <*> mkVarAccess Nothing var

9851123

9861124

987−mkThreadBindingMethod :: Either String MemberDecl

1125+mkThreadBindingMethod :: CodeGeneration MemberDecl

9881126mkThreadBindingMethod =

9891127 (\ compute ->

9901128 MethodDecl [Final, Public]

@@ -1011,9 +1149,8 @@ mkThreadBindingStack =

10111149 ]

10121150

10131151

1014−mkExp :: SExp -> Either String Exp

1015−mkExp (SV var) =

1016− return $ mkVarAccess Nothing var

1152+mkExp :: SExp -> CodeGeneration Exp

1153+mkExp (SV var) = mkVarAccess Nothing var

10171154mkExp (SApp False name args) =

10181155 (\ methClosure ->

10191156 MethodInv $ PrimaryMethodCall ( InstanceCreation []

@@ -1036,12 +1173,14 @@ mkExp (SApp True name args) =

10361173 )

10371174 <$> mkMethodClosure name args

10381175mkExp (SLet var new old) =

1039− mkAnonymousLetBinding var old new

1040−mkExp (SUpdate (Loc i) exp) =

1041− (\ rhs -> Assign (ArrayLhs $ ArrayIndex (contextArray) (Lit $ Int (toInteger i)))

1042− EqualA

1043− rhs)

1176+ mkLet var old new

1177+mkExp (SUpdate var exp) =

1178+ (\ rhs varPos -> Assign (ArrayLhs $ ArrayIndex (contextArray var) (Lit $ Int varPos))

1179+ EqualA

1180+ rhs

1181+ )

10441182 <$> mkExp exp

1183+ <*> varPos var

10451184mkExp (SCon conId name args) =

10461185 (\ args -> InstanceCreation []

10471186 idrisObjectType

@@ -1050,7 +1189,7 @@ mkExp (SCon conId name args) =

10501189 <$> mapM (mkExp .SV) args

10511190mkExp (SCase var alts) = mkCase False var alts

10521191mkExp (SChkCase var alts) = mkCase True var alts

1053−mkExp (SProj var i) = return $ mkProjection var i

1192+mkExp (SProj var i) = mkProjection var i

10541193mkExp (SConst (I x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

10551194mkExp (SConst (BI x)) =

10561195 return $ InstanceCreation []

@@ -1077,226 +1216,235 @@ mkExp (SConst (PtrType)) = return $ mkClass objectType

10771216mkExp (SConst (VoidType)) = return $ mkClass voidType

10781217mkExp (SConst (Forgot)) = return $ mkClass objectType

10791218mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1080−mkExp (SOp LPlus args) = return $ mkBinOpExp integerType Add args

1081−mkExp (SOp LMinus args) = return $ mkBinOpExp integerType Sub args

1082−mkExp (SOp LTimes args) = return $ mkBinOpExp integerType Mult args

1083−mkExp (SOp LDiv args) = return $ mkBinOpExp integerType Div args

1084−mkExp (SOp LMod args) = return $ mkBinOpExp integerType Rem args

1085−mkExp (SOp LAnd args) = return $ mkBinOpExp integerType And args

1086−mkExp (SOp LOr args) = return $ mkBinOpExp integerType Or args

1087−mkExp (SOp LXOr args) = return $ mkBinOpExp integerType Xor args

1219+mkExp (SOp LPlus args) = mkBinOpExp integerType Add args

1220+mkExp (SOp LMinus args) = mkBinOpExp integerType Sub args

1221+mkExp (SOp LTimes args) = mkBinOpExp integerType Mult args

1222+mkExp (SOp LDiv args) = mkBinOpExp integerType Div args

1223+mkExp (SOp LMod args) = mkBinOpExp integerType Rem args

1224+mkExp (SOp LAnd args) = mkBinOpExp integerType And args

1225+mkExp (SOp LOr args) = mkBinOpExp integerType Or args

1226+mkExp (SOp LXOr args) = mkBinOpExp integerType Xor args

10881227mkExp (SOp LCompl [var]) =

1089− return $ PreBitCompl (mkVarAccess (Just $ integerType) var)

1090−mkExp (SOp LSHL args) = return $ mkBinOpExp integerType LShift args

1091−mkExp (SOp LSHR args) = return $ mkBinOpExp integerType RShift args

1228+ PreBitCompl <$> mkVarAccess (Just $ integerType) var

1229+mkExp (SOp LSHL args) = mkBinOpExp integerType LShift args

1230+mkExp (SOp LSHR args) = mkBinOpExp integerType RShift args

10921231mkExp (SOp LEq args) =

1093− return $ mkMethodOpChain1 (mkBoolToNumber integerType) objectType "equals" args

1094−mkExp (SOp LLt args) = return $ mkLogicalBinOpExp integerType LThan args

1095−mkExp (SOp LLe args) = return $ mkLogicalBinOpExp integerType LThanE args

1096−mkExp (SOp LGt args) = return $ mkLogicalBinOpExp integerType GThan args

1097−mkExp (SOp LGe args) = return $ mkLogicalBinOpExp integerType GThanE args

1098−mkExp (SOp LFPlus args) = return $ mkBinOpExp doubleType Add args

1099−mkExp (SOp LFMinus args) = return $ mkBinOpExp doubleType Sub args

1100−mkExp (SOp LFTimes args) = return $ mkBinOpExp doubleType Mult args

1101−mkExp (SOp LFDiv args) = return $ mkBinOpExp doubleType Div args

1232+ mkMethodOpChain1 (mkBoolToNumber integerType) objectType "equals" args

1233+mkExp (SOp LLt args) = mkLogicalBinOpExp integerType LThan args

1234+mkExp (SOp LLe args) = mkLogicalBinOpExp integerType LThanE args

1235+mkExp (SOp LGt args) = mkLogicalBinOpExp integerType GThan args

1236+mkExp (SOp LGe args) = mkLogicalBinOpExp integerType GThanE args

1237+mkExp (SOp LFPlus args) = mkBinOpExp doubleType Add args

1238+mkExp (SOp LFMinus args) = mkBinOpExp doubleType Sub args

1239+mkExp (SOp LFTimes args) = mkBinOpExp doubleType Mult args

1240+mkExp (SOp LFDiv args) = mkBinOpExp doubleType Div args

11021241mkExp (SOp LFEq args) =

1103− return $ mkMethodOpChain1 (mkBoolToNumber doubleType) doubleType "equals" args

1104−mkExp (SOp LFLt args) = return $ mkLogicalBinOpExp integerType LThan args

1105−mkExp (SOp LFLe args) = return $ mkLogicalBinOpExp integerType LThanE args

1106−mkExp (SOp LFGt args) = return $ mkLogicalBinOpExp integerType GThan args

1107−mkExp (SOp LFGe args) = return $ mkLogicalBinOpExp integerType GThanE args

1108−mkExp (SOp LBPlus args) = return $ mkMethodOpChain1 id bigIntegerType "add" args

1109−mkExp (SOp LBMinus args) = return $ mkMethodOpChain1 id bigIntegerType "subtract" args

1110−mkExp (SOp LBTimes args) = return $ mkMethodOpChain1 id bigIntegerType "multiply" args

1111−mkExp (SOp LBDiv args) = return $ mkMethodOpChain1 id bigIntegerType "divide" args

1112−mkExp (SOp LBMod args) = return $ mkMethodOpChain1 id bigIntegerType "mod" args

1242+ mkMethodOpChain1 (mkBoolToNumber doubleType) doubleType "equals" args

1243+mkExp (SOp LFLt args) = mkLogicalBinOpExp integerType LThan args

1244+mkExp (SOp LFLe args) = mkLogicalBinOpExp integerType LThanE args

1245+mkExp (SOp LFGt args) = mkLogicalBinOpExp integerType GThan args

1246+mkExp (SOp LFGe args) = mkLogicalBinOpExp integerType GThanE args

1247+mkExp (SOp LBPlus args) = mkMethodOpChain1 id bigIntegerType "add" args

1248+mkExp (SOp LBMinus args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1249+mkExp (SOp LBTimes args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1250+mkExp (SOp LBDiv args) = mkMethodOpChain1 id bigIntegerType "divide" args

1251+mkExp (SOp LBMod args) = mkMethodOpChain1 id bigIntegerType "mod" args

11131252mkExp (SOp LBEq args) =

1114− return $ mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1253+ mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

11151254mkExp (SOp LBLt args) =

1116− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1117− . mkPartialOrder SLt

1118− )

1119− bigIntegerType

1120− "compare"

1121− args

1255+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1256+ . mkPartialOrder SLt

1257+ )

1258+ bigIntegerType

1259+ "compare"

1260+ args

11221261mkExp (SOp LBLe args) =

1123− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1124− . mkPartialOrder SLe

1125− )

1126− bigIntegerType

1127− "compare"

1128− args

1262+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1263+ . mkPartialOrder SLe

1264+ )

1265+ bigIntegerType

1266+ "compare"

1267+ args

11291268mkExp (SOp LBGt args) =

1130− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1131− . mkPartialOrder SGt

1132− )

1133− bigIntegerType

1134− "compare"

1135− args

1269+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1270+ . mkPartialOrder SGt

1271+ )

1272+ bigIntegerType

1273+ "compare"

1274+ args

11361275mkExp (SOp LBGe args) =

1137− return $ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1138− . mkPartialOrder SGe

1139− )

1140− bigIntegerType

1141− "compare"

1142− args

1276+ mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1277+ . mkPartialOrder SGe

1278+ )

1279+ bigIntegerType

1280+ "compare"

1281+ args

11431282mkExp (SOp LStrConcat args) =

1144− return $ mkMethodOpChain (\ exp ->

1145− InstanceCreation []

1146− (ClassType [(Ident "StringBuilder", [])])

1147− [exp]

1148− Nothing

1149− )

1150− (\ exp -> MethodInv $ PrimaryMethodCall exp [] (Ident "toString") [])

1151− stringType

1152− "append"

1153− args

1283+ mkMethodOpChain (\ exp -> InstanceCreation []

1284+ (ClassType [(Ident "StringBuilder", [])])

1285+ [exp]

1286+ Nothing

1287+ )

1288+ (\ exp -> MethodInv $ PrimaryMethodCall exp [] (Ident "toString") [])

1289+ stringType

1290+ "append"

1291+ args

11541292mkExp (SOp LStrLt args@[_, _]) =

1155− return $ mkMethodOpChain1 ( mkBoolToNumber integerType

1156− . mkPartialOrder SLt

1157− )

1158− stringType

1159− "compare"

1160− args

1293+ mkMethodOpChain1 ( mkBoolToNumber integerType

1294+ . mkPartialOrder SLt

1295+ )

1296+ stringType

1297+ "compare"

1298+ args

11611299mkExp (SOp LStrEq args@[_, _]) =

1162− return $ mkMethodOpChain1 ( mkBoolToNumber integerType)

1163− stringType

1164− "equals"

1165− args

1300+ mkMethodOpChain1 ( mkBoolToNumber integerType)

1301+ stringType

1302+ "equals"

1303+ args

11661304mkExp (SOp LStrLen [arg]) =

1167− return . MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) arg) [] (Ident "length") []

1305+ (\ var -> MethodInv $ PrimaryMethodCall var [] (Ident "length") [])

1306+ <$> mkVarAccess (Just stringType) arg

11681307mkExp (SOp LIntFloat [arg]) =

1169− return $ mkPrimitiveCast integerType doubleType arg

1308+ mkPrimitiveCast integerType doubleType arg

11701309mkExp (SOp LFloatInt [arg]) =

1171− return $ mkPrimitiveCast doubleType integerType arg

1310+ mkPrimitiveCast doubleType integerType arg

11721311mkExp (SOp LIntStr [arg]) =

1173− return $ mkToString integerType arg

1312+ mkToString integerType arg

11741313mkExp (SOp LStrInt [arg]) =

1175− return $ mkPrimitiveCast stringType integerType arg

1314+ mkPrimitiveCast stringType integerType arg

11761315mkExp (SOp LFloatStr [arg]) =

1177− return $ mkToString doubleType arg

1316+ mkToString doubleType arg

11781317mkExp (SOp LStrFloat [arg]) =

1179− return $ mkPrimitiveCast doubleType stringType arg

1318+ mkPrimitiveCast doubleType stringType arg

11801319mkExp (SOp LIntBig [arg]) =

1181− return $ mkPrimitiveCast integerType bigIntegerType arg

1320+ mkPrimitiveCast integerType bigIntegerType arg

11821321mkExp (SOp LBigInt [arg]) =

1183− return $ mkPrimitiveCast bigIntegerType integerType arg

1322+ mkPrimitiveCast bigIntegerType integerType arg

11841323mkExp (SOp LStrBig [arg]) =

1185− return $ InstanceCreation [] bigIntegerType [mkVarAccess (Just stringType) arg] Nothing

1324+ (\ var -> InstanceCreation [] bigIntegerType [var] Nothing)

1325+ <$> mkVarAccess (Just stringType) arg

11861326mkExp (SOp LBigStr [arg]) =

1187− return $ mkToString bigIntegerType arg

1327+ mkToString bigIntegerType arg

11881328mkExp (SOp LChInt [arg]) =

1189− return $ mkVarAccess (Just integerType) arg

1329+ mkVarAccess (Just integerType) arg

11901330mkExp (SOp LIntCh [arg]) =

1191− return $ mkVarAccess (Just integerType) arg

1331+ mkVarAccess (Just integerType) arg

11921332mkExp (SOp LPrintNum [arg]) =

1193− return $ mkSystemOutPrint (mkVarAccess Nothing arg)

1333+ mkSystemOutPrint <$> (mkVarAccess Nothing arg)

11941334mkExp (SOp LPrintStr [arg]) =

1195− return $ mkSystemOutPrint (mkVarAccess (Just stringType) arg)

1335+ mkSystemOutPrint <$> (mkVarAccess (Just stringType) arg)

11961336mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1197−mkExp (SOp LB8Lt args) = return $ mkLogicalBinOpExp byteType LThan args

1198−mkExp (SOp LB8Lte args) = return $ mkLogicalBinOpExp byteType LThanE args

1337+mkExp (SOp LB8Lt args) = mkLogicalBinOpExp byteType LThan args

1338+mkExp (SOp LB8Lte args) = mkLogicalBinOpExp byteType LThanE args

11991339mkExp (SOp LB8Eq args) =

1200− return $ mkMethodOpChain1 (mkBoolToNumber byteType) byteType "equals" args

1201−mkExp (SOp LB8Gt args) = return $ mkLogicalBinOpExp byteType GThan args

1202−mkExp (SOp LB8Gte args) = return $ mkLogicalBinOpExp byteType GThanE args

1203−mkExp (SOp LB8Plus args) = return $ mkBinOpExp byteType Add args

1204−mkExp (SOp LB8Minus args) = return $ mkBinOpExp byteType Sub args

1205−mkExp (SOp LB8Times args) = return $ mkBinOpExp byteType Mult args

1206−mkExp (SOp LB8UDiv args) = return $ mkBinOpExpConv "shortValue" ShortT byteType Div args

1207−mkExp (SOp LB8SDiv args) = return $ mkBinOpExp byteType Div args

1208−mkExp (SOp LB8URem args) = return $ mkBinOpExpConv "shortValue" ShortT byteType Rem args

1209−mkExp (SOp LB8SRem args) = return $ mkBinOpExp byteType Rem args

1210−mkExp (SOp LB8Shl args) = return $ mkBinOpExp byteType LShift args

1211−mkExp (SOp LB8LShr args) = return $ mkBinOpExp byteType RRShift args

1212−mkExp (SOp LB8AShr args) = return $ mkBinOpExp byteType RShift args

1213−mkExp (SOp LB8And args) = return $ mkBinOpExp byteType And args

1214−mkExp (SOp LB8Or args) = return $ mkBinOpExp byteType Or args

1215−mkExp (SOp LB8Xor args) = return $ mkBinOpExp byteType Xor args

1340+ mkMethodOpChain1 (mkBoolToNumber byteType) byteType "equals" args

1341+mkExp (SOp LB8Gt args) = mkLogicalBinOpExp byteType GThan args

1342+mkExp (SOp LB8Gte args) = mkLogicalBinOpExp byteType GThanE args

1343+mkExp (SOp LB8Plus args) = mkBinOpExp byteType Add args

1344+mkExp (SOp LB8Minus args) = mkBinOpExp byteType Sub args

1345+mkExp (SOp LB8Times args) = mkBinOpExp byteType Mult args

1346+mkExp (SOp LB8UDiv args) = mkBinOpExpConv "shortValue" ShortT byteType Div args

1347+mkExp (SOp LB8SDiv args) = mkBinOpExp byteType Div args

1348+mkExp (SOp LB8URem args) = mkBinOpExpConv "shortValue" ShortT byteType Rem args

1349+mkExp (SOp LB8SRem args) = mkBinOpExp byteType Rem args

1350+mkExp (SOp LB8Shl args) = mkBinOpExp byteType LShift args

1351+mkExp (SOp LB8LShr args) = mkBinOpExp byteType RRShift args

1352+mkExp (SOp LB8AShr args) = mkBinOpExp byteType RShift args

1353+mkExp (SOp LB8And args) = mkBinOpExp byteType And args

1354+mkExp (SOp LB8Or args) = mkBinOpExp byteType Or args

1355+mkExp (SOp LB8Xor args) = mkBinOpExp byteType Xor args

12161356mkExp (SOp LB8Compl [var]) =

1217− return $ PreBitCompl (mkVarAccess (Just $ byteType) var)

1218−mkExp (SOp LB8Z16 [var]) = return $ mkZeroExt "shortValue" 8 byteType shortType var

1219−mkExp (SOp LB8Z32 [var]) = return $ mkZeroExt "intValue" 8 byteType integerType var

1220−mkExp (SOp LB8Z64 [var]) = return $ mkZeroExt "longValue" 8 byteType longType var

1221−mkExp (SOp LB8S16 [var]) = return $ mkSignedExt "shortValue" byteType shortType var

1222−mkExp (SOp LB8S32 [var]) = return $ mkSignedExt "intValue" byteType integerType var

1223−mkExp (SOp LB8S64 [var]) = return $ mkSignedExt "longValue" byteType longType var

1224−mkExp (SOp LB16Lt args) = return $ mkLogicalBinOpExp shortType LThan args

1225−mkExp (SOp LB16Lte args) = return $ mkLogicalBinOpExp shortType LThanE args

1357+ PreBitCompl <$> mkVarAccess (Just $ byteType) var

1358+mkExp (SOp LB8Z16 [var]) = mkZeroExt "shortValue" 8 byteType shortType var

1359+mkExp (SOp LB8Z32 [var]) = mkZeroExt "intValue" 8 byteType integerType var

1360+mkExp (SOp LB8Z64 [var]) = mkZeroExt "longValue" 8 byteType longType var

1361+mkExp (SOp LB8S16 [var]) = mkSignedExt "shortValue" byteType shortType var

1362+mkExp (SOp LB8S32 [var]) = mkSignedExt "intValue" byteType integerType var

1363+mkExp (SOp LB8S64 [var]) = mkSignedExt "longValue" byteType longType var

1364+mkExp (SOp LB16Lt args) = mkLogicalBinOpExp shortType LThan args

1365+mkExp (SOp LB16Lte args) = mkLogicalBinOpExp shortType LThanE args

12261366mkExp (SOp LB16Eq args) =

1227− return $ mkMethodOpChain1 (mkBoolToNumber shortType) shortType "equals" args

1228−mkExp (SOp LB16Gt args) = return $ mkLogicalBinOpExp shortType GThan args

1229−mkExp (SOp LB16Gte args) = return $ mkLogicalBinOpExp shortType GThanE args

1230−mkExp (SOp LB16Plus args) = return $ mkBinOpExp shortType Add args

1231−mkExp (SOp LB16Minus args) = return $ mkBinOpExp shortType Sub args

1232−mkExp (SOp LB16Times args) = return $ mkBinOpExp shortType Mult args

1233−mkExp (SOp LB16UDiv args) = return $ mkBinOpExpConv "intValue" IntT shortType Div args

1234−mkExp (SOp LB16SDiv args) = return $ mkBinOpExp shortType Div args

1235−mkExp (SOp LB16URem args) = return $ mkBinOpExpConv "intValue" IntT shortType Rem args

1236−mkExp (SOp LB16SRem args) = return $ mkBinOpExp shortType Rem args

1237−mkExp (SOp LB16Shl args) = return $ mkBinOpExp shortType LShift args

1238−mkExp (SOp LB16LShr args) = return $ mkBinOpExp shortType RRShift args

1239−mkExp (SOp LB16AShr args) = return $ mkBinOpExp shortType RShift args

1240−mkExp (SOp LB16And args) = return $ mkBinOpExp shortType And args

1241−mkExp (SOp LB16Or args) = return $ mkBinOpExp shortType Or args

1242−mkExp (SOp LB16Xor args) = return $ mkBinOpExp shortType Xor args

1367+ mkMethodOpChain1 (mkBoolToNumber shortType) shortType "equals" args

1368+mkExp (SOp LB16Gt args) = mkLogicalBinOpExp shortType GThan args

1369+mkExp (SOp LB16Gte args) = mkLogicalBinOpExp shortType GThanE args

1370+mkExp (SOp LB16Plus args) = mkBinOpExp shortType Add args

1371+mkExp (SOp LB16Minus args) = mkBinOpExp shortType Sub args

1372+mkExp (SOp LB16Times args) = mkBinOpExp shortType Mult args

1373+mkExp (SOp LB16UDiv args) = mkBinOpExpConv "intValue" IntT shortType Div args

1374+mkExp (SOp LB16SDiv args) = mkBinOpExp shortType Div args

1375+mkExp (SOp LB16URem args) = mkBinOpExpConv "intValue" IntT shortType Rem args

1376+mkExp (SOp LB16SRem args) = mkBinOpExp shortType Rem args

1377+mkExp (SOp LB16Shl args) = mkBinOpExp shortType LShift args

1378+mkExp (SOp LB16LShr args) = mkBinOpExp shortType RRShift args

1379+mkExp (SOp LB16AShr args) = mkBinOpExp shortType RShift args

1380+mkExp (SOp LB16And args) = mkBinOpExp shortType And args

1381+mkExp (SOp LB16Or args) = mkBinOpExp shortType Or args

1382+mkExp (SOp LB16Xor args) = mkBinOpExp shortType Xor args

12431383mkExp (SOp LB16Compl [var]) =

1244− return $ PreBitCompl (mkVarAccess (Just $ shortType) var)

1245−mkExp (SOp LB16Z32 [var]) = return $ mkZeroExt "intValue" 16 shortType integerType var

1246−mkExp (SOp LB16Z64 [var]) = return $ mkZeroExt "longValue" 16 shortType longType var

1247−mkExp (SOp LB16S32 [var]) = return $ mkSignedExt "intValue" shortType integerType var

1248−mkExp (SOp LB16S64 [var]) = return $ mkSignedExt "longValue" shortType longType var

1384+ PreBitCompl <$> mkVarAccess (Just $ shortType) var

1385+mkExp (SOp LB16Z32 [var]) = mkZeroExt "intValue" 16 shortType integerType var

1386+mkExp (SOp LB16Z64 [var]) = mkZeroExt "longValue" 16 shortType longType var

1387+mkExp (SOp LB16S32 [var]) = mkSignedExt "intValue" shortType integerType var

1388+mkExp (SOp LB16S64 [var]) = mkSignedExt "longValue" shortType longType var

12491389mkExp (SOp LB16T8 [var]) =

1250− return . MethodInv $

1251− TypeMethodCall (J.Name [Ident "Byte"])

1252− []

1253− (Ident "valueOf")

1254− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ shortType) var) [] (Ident "byteValue") [] ]

1255−mkExp (SOp LB32Lt args) = return $ mkLogicalBinOpExp integerType LThan args

1256−mkExp (SOp LB32Lte args) = return $ mkLogicalBinOpExp integerType LThanE args

1390+ (\ var -> MethodInv $

1391+ TypeMethodCall (J.Name [Ident "Byte"])

1392+ []

1393+ (Ident "valueOf")

1394+ [ MethodInv

1395+ $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1396+ )

1397+ <$> mkVarAccess (Just $ shortType) var

1398+mkExp (SOp LB32Lt args) = mkLogicalBinOpExp integerType LThan args

1399+mkExp (SOp LB32Lte args) = mkLogicalBinOpExp integerType LThanE args

12571400mkExp (SOp LB32Eq args) =

1258− return $ mkMethodOpChain1 (mkBoolToNumber integerType) integerType "equals" args

1259−mkExp (SOp LB32Gt args) = return $ mkLogicalBinOpExp integerType GThan args

1260−mkExp (SOp LB32Gte args) = return $ mkLogicalBinOpExp integerType GThanE args

1261−mkExp (SOp LB32Plus args) = return $ mkBinOpExp integerType Add args

1262−mkExp (SOp LB32Minus args) = return $ mkBinOpExp integerType Sub args

1263−mkExp (SOp LB32Times args) = return $ mkBinOpExp integerType Mult args

1264−mkExp (SOp LB32UDiv args) = return $ mkBinOpExpConv "longValue" LongT integerType Div args

1265−mkExp (SOp LB32SDiv args) = return $ mkBinOpExp integerType Div args

1266−mkExp (SOp LB32URem args) = return $ mkBinOpExpConv "longValue" LongT integerType Rem args

1267−mkExp (SOp LB32SRem args) = return $ mkBinOpExp integerType Rem args

1268−mkExp (SOp LB32Shl args) = return $ mkBinOpExp integerType LShift args

1269−mkExp (SOp LB32LShr args) = return $ mkBinOpExp integerType RRShift args

1270−mkExp (SOp LB32AShr args) = return $ mkBinOpExp integerType RShift args

1271−mkExp (SOp LB32And args) = return $ mkBinOpExp integerType And args

1272−mkExp (SOp LB32Or args) = return $ mkBinOpExp integerType Or args

1273−mkExp (SOp LB32Xor args) = return $ mkBinOpExp integerType Xor args

1401+ mkMethodOpChain1 (mkBoolToNumber integerType) integerType "equals" args

1402+mkExp (SOp LB32Gt args) = mkLogicalBinOpExp integerType GThan args

1403+mkExp (SOp LB32Gte args) = mkLogicalBinOpExp integerType GThanE args

1404+mkExp (SOp LB32Plus args) = mkBinOpExp integerType Add args

1405+mkExp (SOp LB32Minus args) = mkBinOpExp integerType Sub args

1406+mkExp (SOp LB32Times args) = mkBinOpExp integerType Mult args

1407+mkExp (SOp LB32UDiv args) = mkBinOpExpConv "longValue" LongT integerType Div args

1408+mkExp (SOp LB32SDiv args) = mkBinOpExp integerType Div args

1409+mkExp (SOp LB32URem args) = mkBinOpExpConv "longValue" LongT integerType Rem args

1410+mkExp (SOp LB32SRem args) = mkBinOpExp integerType Rem args

1411+mkExp (SOp LB32Shl args) = mkBinOpExp integerType LShift args

1412+mkExp (SOp LB32LShr args) = mkBinOpExp integerType RRShift args

1413+mkExp (SOp LB32AShr args) = mkBinOpExp integerType RShift args

1414+mkExp (SOp LB32And args) = mkBinOpExp integerType And args

1415+mkExp (SOp LB32Or args) = mkBinOpExp integerType Or args

1416+mkExp (SOp LB32Xor args) = mkBinOpExp integerType Xor args

12741417mkExp (SOp LB32Compl [var]) =

1275− return $ PreBitCompl (mkVarAccess (Just $ integerType) var)

1276−mkExp (SOp LB32Z64 [var]) = return $ mkZeroExt "longValue" 32 integerType longType var

1277−mkExp (SOp LB32S64 [var]) = return $ mkSignedExt "longValue" integerType longType var

1418+ PreBitCompl <$> mkVarAccess (Just $ integerType) var

1419+mkExp (SOp LB32Z64 [var]) = mkZeroExt "longValue" 32 integerType longType var

1420+mkExp (SOp LB32S64 [var]) = mkSignedExt "longValue" integerType longType var

12781421mkExp (SOp LB32T8 [var]) =

1279− return . MethodInv $

1280− TypeMethodCall (J.Name [Ident "Byte"])

1281− []

1282− (Ident "valueOf")

1283− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ integerType) var) [] (Ident "byteValue") [] ]

1422+ (\ var -> MethodInv

1423+ $ TypeMethodCall (J.Name [Ident "Byte"])

1424+ []

1425+ (Ident "valueOf")

1426+ [ MethodInv $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1427+ )

1428+ <$> mkVarAccess (Just $ integerType) var

12841429mkExp (SOp LB32T16 [var]) =

1285− return . MethodInv $

1286− TypeMethodCall (J.Name [Ident "Short"])

1287− []

1288− (Ident "valueOf")

1289− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ integerType) var) [] (Ident "shortValue") [] ]

1290−mkExp (SOp LB64Lt args) = return $ mkLogicalBinOpExp longType LThan args

1291−mkExp (SOp LB64Lte args) = return $ mkLogicalBinOpExp longType LThanE args

1430+ (\ var -> MethodInv

1431+ $ TypeMethodCall (J.Name [Ident "Short"])

1432+ []

1433+ (Ident "valueOf")

1434+ [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1435+ )

1436+ <$> mkVarAccess (Just $ integerType) var

1437+mkExp (SOp LB64Lt args) = mkLogicalBinOpExp longType LThan args

1438+mkExp (SOp LB64Lte args) = mkLogicalBinOpExp longType LThanE args

12921439mkExp (SOp LB64Eq args) =

1293− return $ mkMethodOpChain1 (mkBoolToNumber longType) longType "equals" args

1294−mkExp (SOp LB64Gt args) = return $ mkLogicalBinOpExp longType GThan args

1295−mkExp (SOp LB64Gte args) = return $ mkLogicalBinOpExp longType GThanE args

1296−mkExp (SOp LB64Plus args) = return $ mkBinOpExp longType Add args

1297−mkExp (SOp LB64Minus args) = return $ mkBinOpExp longType Sub args

1298−mkExp (SOp LB64Times args) = return $ mkBinOpExp longType Mult args

1299−mkExp (SOp LB64UDiv (arg:args)) =

1440+ mkMethodOpChain1 (mkBoolToNumber longType) longType "equals" args

1441+mkExp (SOp LB64Gt args) = mkLogicalBinOpExp longType GThan args

1442+mkExp (SOp LB64Gte args) = mkLogicalBinOpExp longType GThanE args

1443+mkExp (SOp LB64Plus args) = mkBinOpExp longType Add args

1444+mkExp (SOp LB64Minus args) = mkBinOpExp longType Sub args

1445+mkExp (SOp LB64Times args) = mkBinOpExp longType Mult args

1446+mkExp (SOp LB64UDiv (arg:args)) = do

1447+ (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

13001448 return $ foldl (\ exp arg ->

13011449 MethodInv $ PrimaryMethodCall

13021450 ( MethodInv $ PrimaryMethodCall

@@ -1310,17 +1458,18 @@ mkExp (SOp LB64UDiv (arg:args)) =

13101458 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

13111459 []

13121460 (Ident "valueOf")

1313− [ (mkVarAccess (Just longType) arg) ]

1461+ [ arg ]

13141462 ]

13151463 )

13161464 []

13171465 (Ident "longValue")

13181466 []

13191467 )

1320− (mkVarAccess (Just longType) arg)

1468+ arg

13211469 args

1322−mkExp (SOp LB64SDiv args) = return $ mkBinOpExp longType Div args

1323−mkExp (SOp LB64URem (arg:args)) =

1470+mkExp (SOp LB64SDiv args) = mkBinOpExp longType Div args

1471+mkExp (SOp LB64URem (arg:args)) = do

1472+ (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

13241473 return $ foldl (\ exp arg ->

13251474 MethodInv $ PrimaryMethodCall

13261475 ( MethodInv $ PrimaryMethodCall

@@ -1334,69 +1483,79 @@ mkExp (SOp LB64URem (arg:args)) =

13341483 [ MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

13351484 []

13361485 (Ident "valueOf")

1337− [ (mkVarAccess (Just longType) arg) ]

1486+ [ arg ]

13381487 ]

13391488 )

13401489 []

13411490 (Ident "longValue")

13421491 []

13431492 )

1344− (mkVarAccess (Just longType) arg)

1493+ arg

13451494 args

1346−mkExp (SOp LB64SRem args) = return $ mkBinOpExp longType Rem args

1347−mkExp (SOp LB64Shl args) = return $ mkBinOpExp longType LShift args

1348−mkExp (SOp LB64LShr args) = return $ mkBinOpExp longType RRShift args

1349−mkExp (SOp LB64AShr args) = return $ mkBinOpExp longType RShift args

1350−mkExp (SOp LB64And args) = return $ mkBinOpExp longType And args

1351−mkExp (SOp LB64Or args) = return $ mkBinOpExp longType Or args

1352−mkExp (SOp LB64Xor args) = return $ mkBinOpExp longType Xor args

1495+mkExp (SOp LB64SRem args) = mkBinOpExp longType Rem args

1496+mkExp (SOp LB64Shl args) = mkBinOpExp longType LShift args

1497+mkExp (SOp LB64LShr args) = mkBinOpExp longType RRShift args

1498+mkExp (SOp LB64AShr args) = mkBinOpExp longType RShift args

1499+mkExp (SOp LB64And args) = mkBinOpExp longType And args

1500+mkExp (SOp LB64Or args) = mkBinOpExp longType Or args

1501+mkExp (SOp LB64Xor args) = mkBinOpExp longType Xor args

13531502mkExp (SOp LB64Compl [var]) =

1354− return $ PreBitCompl (mkVarAccess (Just $ longType) var)

1503+ PreBitCompl <$> mkVarAccess (Just $ longType) var

13551504mkExp (SOp LB64T8 [var]) =

1356− return . MethodInv $

1357− TypeMethodCall (J.Name [Ident "Byte"])

1358− []

1359− (Ident "valueOf")

1360− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "byteValue") [] ]

1505+ (\ var -> MethodInv

1506+ $ TypeMethodCall (J.Name [Ident "Byte"])

1507+ []

1508+ (Ident "valueOf")

1509+ [ MethodInv

1510+ $ PrimaryMethodCall var [] (Ident "byteValue") []

1511+ ]

1512+ )

1513+ <$> mkVarAccess (Just $ longType) var

13611514mkExp (SOp LB64T16 [var]) =

1362− return . MethodInv $

1363− TypeMethodCall (J.Name [Ident "Short"])

1364− []

1365− (Ident "valueOf")

1366− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "shortValue") [] ]

1515+ (\ var -> MethodInv

1516+ $ TypeMethodCall (J.Name [Ident "Short"])

1517+ []

1518+ (Ident "valueOf")

1519+ [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1520+ )

1521+ <$> mkVarAccess (Just $ longType) var

13671522mkExp (SOp LB64T32 [var]) =

1368− return . MethodInv $

1369− TypeMethodCall (J.Name [Ident "Integer"])

1370− []

1371− (Ident "valueOf")

1372− [ MethodInv $ PrimaryMethodCall (mkVarAccess (Just $ longType) var) [] (Ident "intValue") [] ]

1523+ (\ var -> MethodInv

1524+ $ TypeMethodCall (J.Name [Ident "Integer"])

1525+ []

1526+ (Ident "valueOf")

1527+ [ MethodInv $ PrimaryMethodCall var [] (Ident "intValue") [] ]

1528+ )

1529+ <$> mkVarAccess (Just $ longType) var

13731530mkExp (SOp LIntB8 [arg]) = mkExp (SOp LB32T8 [arg])

13741531mkExp (SOp LIntB16 [arg]) = mkExp (SOp LB32T16 [arg])

13751532mkExp (SOp LIntB32 [arg]) = mkExp (SV arg)

13761533mkExp (SOp LIntB64 [arg]) = mkExp (SOp LB32S64 [arg])

13771534mkExp (SOp LB32Int [arg]) = mkExp (SV arg)

1378−mkExp (SOp LFExp [arg]) = return $ mkMathFun "exp" arg

1379−mkExp (SOp LFLog [arg]) = return $ mkMathFun "log" arg

1380−mkExp (SOp LFSin [arg]) = return $ mkMathFun "sin" arg

1381−mkExp (SOp LFCos [arg]) = return $ mkMathFun "cos" arg

1382−mkExp (SOp LFTan [arg]) = return $ mkMathFun "tan" arg

1383−mkExp (SOp LFASin [arg]) = return $ mkMathFun "asin" arg

1384−mkExp (SOp LFACos [arg]) = return $ mkMathFun "acos" arg

1385−mkExp (SOp LFATan [arg]) = return $ mkMathFun "atan" arg

1386−mkExp (SOp LFSqrt [arg]) = return $ mkMathFun "sqrt" arg

1387−mkExp (SOp LFFloor [arg]) = return $ mkMathFun "floor" arg

1388−mkExp (SOp LFCeil [arg]) = return $ mkMathFun "ceil" arg

1389−mkExp (SOp LStrHead [arg]) = return $ mkStringAtIndex arg (Lit $ Int 0)

1535+mkExp (SOp LFExp [arg]) = mkMathFun "exp" arg

1536+mkExp (SOp LFLog [arg]) = mkMathFun "log" arg

1537+mkExp (SOp LFSin [arg]) = mkMathFun "sin" arg

1538+mkExp (SOp LFCos [arg]) = mkMathFun "cos" arg

1539+mkExp (SOp LFTan [arg]) = mkMathFun "tan" arg

1540+mkExp (SOp LFASin [arg]) = mkMathFun "asin" arg

1541+mkExp (SOp LFACos [arg]) = mkMathFun "acos" arg

1542+mkExp (SOp LFATan [arg]) = mkMathFun "atan" arg

1543+mkExp (SOp LFSqrt [arg]) = mkMathFun "sqrt" arg

1544+mkExp (SOp LFFloor [arg]) = mkMathFun "floor" arg

1545+mkExp (SOp LFCeil [arg]) = mkMathFun "ceil" arg

1546+mkExp (SOp LStrHead [arg]) = mkStringAtIndex arg (Lit $ Int 0)

13901547mkExp (SOp LStrTail [arg]) =

1391− return . MethodInv $ PrimaryMethodCall (mkVarAccess (Just stringType) arg)

1548+ (\ var -> MethodInv $ PrimaryMethodCall (var)

13921549 []

13931550 (Ident "substring")

13941551 [Lit $ Int 1]

1552+ )

1553+ <$> mkVarAccess (Just stringType) arg

13951554mkExp (SOp LStrCons [c, cs]) =

1396− return . MethodInv $

1555+ (\ cVar csVar -> MethodInv $

13971556 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

13981557 (ClassType [(Ident "StringBuilder", [])])

1399− [mkVarAccess (Just stringType) cs]

1558+ [csVar]

14001559 Nothing

14011560 )

14021561 []

@@ -1404,7 +1563,7 @@ mkExp (SOp LStrCons [c, cs]) =

14041563 [ Lit $ Int 0,

14051564 Cast (PrimType CharT)

14061565 (MethodInv $ PrimaryMethodCall

1407− (mkVarAccess (Just integerType) c)

1566+ (cVar)

14081567 []

14091568 (Ident "intValue")

14101569 []

@@ -1414,12 +1573,15 @@ mkExp (SOp LStrCons [c, cs]) =

14141573 []

14151574 (Ident "toString")

14161575 []

1417−mkExp (SOp LStrIndex [str, i]) = return $ mkStringAtIndex str (mkVarAccess (Just integerType) i)

1576+ )

1577+ <$> mkVarAccess (Just integerType) c

1578+ <*> mkVarAccess (Just stringType) cs

1579+mkExp (SOp LStrIndex [str, i]) = mkVarAccess (Just integerType) i >>= mkStringAtIndex str

14181580mkExp (SOp LStrRev [str]) =

1419− return . MethodInv $

1581+ (\ var -> MethodInv $

14201582 PrimaryMethodCall ( MethodInv $ PrimaryMethodCall (InstanceCreation []

14211583 (ClassType [(Ident "StringBuffer", [])])

1422− [mkVarAccess (Just stringType) str]

1584+ [var]

14231585 Nothing

14241586 )

14251587 []

@@ -1429,13 +1591,15 @@ mkExp (SOp LStrRev [str]) =

14291591 []

14301592 (Ident "toString")

14311593 []

1594+ )

1595+ <$> mkVarAccess (Just stringType) str

14321596mkExp (SOp LStdIn []) = return $ mkSystemStd In

14331597mkExp (SOp LStdOut []) = return $ mkSystemStd Out

14341598mkExp (SOp LStdErr []) = return $ mkSystemStd Err

14351599mkExp (SOp LFork [arg]) = mkThread arg

14361600mkExp (SOp LPar [arg]) = mkExp (SV arg)

14371601mkExp (SOp LVMPtr []) =

1438− return . MethodInv $ TypeMethodCall (J.Name [Ident "Thread"]) [] (Ident "currentThread") []

1602+ return $ MethodInv $ TypeMethodCall (J.Name [Ident "Thread"]) [] (Ident "currentThread") []

14391603mkExp (SOp LNoOp args) = mkExp . SV $ last args

14401604mkExp (SNothing) = return $ Lit Null

14411605mkExp (SError err) =

src/IRTS/Compiler.hs+1−1

@@ -71,7 +71,7 @@ compile target f tm

7171 (concatMap mkObj objs)

7272 (concatMap mkLib libs) NONE

7373 ViaJava ->

74− codegenJava c f outty

74+ codegenJava [] c f outty

7575 ViaJavaScript ->

7676 codegenJavaScript JavaScript c f outty

7777 ViaNode ->

src/IRTS/LParser.hs+1−1

@@ -61,7 +61,7 @@ fovm tgt outty f

6161 case checked of

6262 OK c -> case tgt of

6363 ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

64− ViaJava -> codegenJava c "a.out" outty

64+ ViaJava -> codegenJava [] c "a.out" outty

6565 Error e -> fail $ show e

6666

6767parseFOVM :: FilePath -> IO [(Name, LDecl)]

src/Idris/AbsSyntax.hs+1−1

@@ -940,7 +940,7 @@ stripLinear i tm = evalState (sl tm) [] where

940940 if (f `elem` ns)

941941 then return Placeholder

942942 else do put (f : ns)

943− return (PRef fc f)

943+ return (PPatvar fc f)

944944 sl (PApp fc fn args) = do fn' <- sl fn

945945 args' <- mapM slA args

946946 return $ PApp fc fn' args'

src/Idris/ElabTerm.hs+14−6

@@ -57,6 +57,7 @@ build ist info pattern fn tm

5757 resolveTC 7 fn ist) ivs

5858 probs <- get_probs

5959 tm <- get_term

60+ ctxt <- get_context

6061 case probs of

6162 [] -> return ()

6263 ((_,_,_,e):es) -> lift (Error e)

@@ -122,6 +123,15 @@ elab ist info pattern tcgen fn tm

122123 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

123124 $ -}

124125 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") $

125135 elab' ina t'

126136

127137 local f = do e <- get_env

@@ -198,13 +208,8 @@ elab ist info pattern tcgen fn tm

198208 trySeq' deferr (x : xs)

199209 = try' (elab' ina x) (trySeq' deferr xs) True

200210 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

205211 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

206212 = do ctxt <- get_context

207− env <- get_env

208213 let defined = case lookupTy Nothing n ctxt of

209214 [] -> False

210215 _ -> True

@@ -421,6 +426,8 @@ elab ist info pattern tcgen fn tm

421426 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

422427 -- elaborate case

423428 updateAux (newdef : )

429+ -- if we haven't got the type yet, hopefully we'll get it later!

430+ movelast tyn

424431 solve

425432 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

426433 mkCaseName (UN x) = UN (x ++ "_case")

@@ -537,7 +544,8 @@ pruneByType (P _ n _) c as

537544

538545 typeHead var f f'

539546 = case lookupTy Nothing f' c of

540− [ty] -> case unApply (getRetTy ty) of

547+ [ty] -> let ty' = normalise c [] ty in

548+ case unApply (getRetTy ty') of

541549 (P _ ftyn _, _) -> ftyn == f

542550 (V _, _) -> var -- keep, variable

543551 _ -> False

src/Idris/Primitives.hs+3

@@ -332,6 +332,8 @@ primitives =

332332 (2, LStrEq) total,

333333 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

334334 (2, LStrLt) total,

335+ Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

336+ (1, LStrLen) total,

335337 -- Conversions

336338 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

337339 (1, LStrInt) total,

@@ -622,6 +624,7 @@ p_floatSqrt = p_fPrim sqrt

622624p_floatFloor = p_fPrim (fromInteger . floor)

623625p_floatCeil = p_fPrim (fromInteger . ceiling)

624626

627+p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

625628p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

626629p_strHead _ = Nothing

627630p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

src/Util/System.hs+38−4

@@ -1,13 +1,20 @@

11{-# LANGUAGE CPP #-}

2−module Util.System(tempfile,environment,getCC,

3− getLibFlags,getIdrisLibDir,getIncFlags,rmFile) where

2+module Util.System(tempfile,withTempdir,environment,getCC,

3+ getLibFlags,getIdrisLibDir,getIncFlags,rmFile,

4+ getMvn,getExecutablePom) where

56-- System helper functions.

6−

7−import System.Directory (getTemporaryDirectory, removeFile)

7+import Control.Monad (when)

8+import Distribution.Text (display)

9+import System.Directory (getTemporaryDirectory

10+ , removeFile

11+ , removeDirectoryRecursive

12+ , createDirectoryIfMissing

13+ )

814import System.FilePath ((</>), addTrailingPathSeparator, normalise)

915import System.Environment

1016import System.IO

17+import System.IO.Error

1118#if MIN_VERSION_base(4,0,0)

1219import Control.Exception as CE

1320#endif

@@ -17,20 +24,44 @@ import Paths_idris

1724#if MIN_VERSION_base(4,0,0)

1825catchIO :: IO a -> (IOError -> IO a) -> IO a

1926catchIO = CE.catch

27+

28+throwIO :: IOError -> IO a

29+throwIO = CE.throw

2030#else

2131catchIO = catch

32+throwIO = throw

2233#endif

2334

35+

36+

2437getCC :: IO String

2538getCC = do env <- environment "IDRIS_CC"

2639 case env of

2740 Nothing -> return "gcc"

2841 Just cc -> return cc

2942

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+

3049tempfile :: IO (FilePath, Handle)

3150tempfile = do dir <- getTemporaryDirectory

3251 openTempFile (normalise dir) "idris"

3352

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+

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

3566environment x = catchIO (do e <- getEnv x

3667 return (Just e))

@@ -51,3 +82,6 @@ getIdrisLibDir = do dir <- getDataDir

5182

5283getIncFlags = do dir <- getDataDir

5384 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:

22 perl ./runtest.pl all

44test_java:

5− perl ./runtest.pl all --java

5+ perl ./runtest.pl all --target Java

77update:

88 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 @@

33my $exitstatus = 0;

55sub runtest {

6− my ($test, $update, $usejava) = @_;

6+ my ($test, $update) = @_;

88 chdir($test);

1010 print "Running $test...";

11− if ($usejava == 1) {

12− $got = `sh ./run_java @idrOpts`;

13− } else {

14− $got = `sh ./run @idrOpts`;

15− }

11+ $got = `sh ./run @idrOpts`;

1612 $exp = `cat expected`;

1713

1814 open(OUT,">output");

@@ -78,19 +74,15 @@ $usejava = 0;

7874

7975while ($opt=shift(@opts)) {

8076 if ($opt eq "-u") { $update = 1; }

81− if ($opt eq "-d") { $diff = 1; }

82− if ($opt eq "-s") { $show = 1; }

83− if ($opt eq "--java") { $usejava = 1; }

77+ elsif ($opt eq "-d") { $diff = 1; }

78+ elsif ($opt eq "-s") { $show = 1; }

79+ else { push(@idrOpts, $opt); }

8480}

8581

8682foreach $test (@tests) {

8783

88− if ($usejava == 1 && !(-e "$test/run_java")) {

89− next;

90− }

91−

9284 if ($diff == 0 && $show == 0) {

93− runtest($test,$update, $usejava);

85+ runtest($test,$update);

9486 }

9587 else {

9688 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

1616main : IO ()

1717main = print (foo [1,2,3])

1818

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.