0861527 · Idris-dev · git.iko.soy

CHANGELOG+8

compare with master

unifiedsplit

@@ -1,3 +1,11 @@

1+New in 0.9.8:

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

3+

4+User visible changes:

5+

6+* Renamed EFF to EFFECT in Effect package

7+* Experimental Java backend

8+

1New in 0.9.7:

9New in 0.9.7:

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

10-------------

3

11

Setup.hs+13−13

@@ -18,7 +18,6 @@ import System.Process

18import qualified Data.Text as T

19import qualified Data.Text.IO as TIO

20

21−

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

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

23

22

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

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

@@ -70,6 +69,7 @@ installStdLib pkg local verbosity copy

70

69

71installJavaLib pkg local verbosity copy version = do

70installJavaLib pkg local verbosity copy version = do

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

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"

@@ -111,8 +111,8 @@ checkStdLib local verbosity

111

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

113

114−noJavaFlag flags =

114+javaFlag flags =

115− case lookup (FlagName "nojava") (S.configConfigurationsFlags flags) of

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

116 Just True -> True

117 Just False -> False

118 Nothing -> False

@@ -138,17 +138,17 @@ main = do

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

139 installStdLib pkg lbi verb

140 NoCopyDest

141− unless (noJavaFlag $ configFlags lbi)

141+ when (javaFlag $ configFlags lbi)

142− (installJavaLib pkg

142+ (installJavaLib pkg

143− lbi

143+ lbi

144− verb

144+ verb

145− NoCopyDest

145+ NoCopyDest

146− (pkgVersion . package $ localPkgDescr lbi)

146+ (pkgVersion . package $ localPkgDescr lbi)

147− )

147+ )

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

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

150− unless (noJavaFlag $ configFlags lbi)

150+ when (javaFlag $ configFlags lbi)

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

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

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

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

154 cleanStdLib verb

@@ -156,5 +156,5 @@ main = do

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

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

158 checkStdLib lbi verb

159− unless (noJavaFlag $ configFlags lbi) (checkJavaLib verb)

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

160 }

config.mk+3−3

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

1GMP_INCLUDE_DIR :=

2CC :=gcc

3CABAL :=cabal

4−CABALFLAGS :=

4+CABALFLAGS :=

5−## Disable Java RTS:

5+## Enable Java RTS:

6−#CABALFLAGS :=-f NoJava

6+#CABALFLAGS :=-f Java

effects/Effect/Exception.idr+1−1

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

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

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

19

20−EXCEPTION : Type -> EFF

20+EXCEPTION : Type -> EFFECT

21EXCEPTION t = MkEff () (Exception t)

22

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

effects/Effect/File.idr+1−1

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

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

41 k (FH h) e

42

43−FILE_IO : Type -> EFF

43+FILE_IO : Type -> EFFECT

44FILE_IO t = MkEff t FileIO

45

46open : Handler FileIO e =>

effects/Effect/Random.idr+1−1

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

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

12 k seed' seed'

13

14−RND : EFF

14+RND : EFFECT

15RND = MkEff Int Random

16

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

effects/Effect/Select.idr+1−1

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

15instance Handler Selection List where

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

17

18−SELECT : EFF

18+SELECT : EFFECT

19SELECT = MkEff () Selection

20

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

effects/Effect/State.idr+1−1

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

13 handle st Get k = k st st

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

15

16−STATE : Type -> EFF

16+STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19get : Eff m [STATE x] x

effects/Effect/StdIO.idr+1−1

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

38

39--- The Effect and associated functions

40

41−STDIO : EFF

41+STDIO : EFFECT

42STDIO = MkEff () StdIO

43

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

effects/Effects.idr+10−10

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

10Effect : Type

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

12

13−data EFF : Type where

13+data EFFECT : Type where

14− MkEff : Type -> Effect -> EFF

14+ MkEff : Type -> Effect -> EFFECT

15

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

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

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

28 subListId {xs = Nil} = SubNil

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

30

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

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

32 Nil : Env m Nil

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

34

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

36− List EFF -> Type where

36+ List EFFECT -> Type where

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

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

39

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

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

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

75

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

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

77− List EFF

77+ List EFFECT

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

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

80

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

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

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

85

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

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

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

88

89private

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

97-- the language of Effects

98

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

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

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

101 value : a -> EffM m xs xs a

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

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

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

114 EffM m xs xs' a

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

116

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

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

118

119implicit

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

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

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

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

194

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

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

196Eff m xs t = EffM m xs xs t

197

198-- some higher order things

idris.cabal+2−2

@@ -71,8 +71,8 @@ source-repository head

71 type: git

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

73

74−Flag NoJava

74+Flag Java

75− Description: Do not build the Java RTS

75+ Description: Build the Java RTS

76 Default: False

77

78

rts/Makefile+3−2

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

1include ../config.mk

2

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

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

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

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

5CFLAGS = -O2 -Wall

6+

6ifneq ($(GMP_INCLUDE_DIR),)

7ifneq ($(GMP_INCLUDE_DIR),)

7 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8endif

9endif

rts/idris_gc.c+21−21

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

55void cheney(VM *vm) {

56 int i;

57 int ar;

58− char* scan = vm->heap;

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

59

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

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

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

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

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

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

76 }

77 scan += inc;

78 }

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

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

80}

81

82void idris_gc(VM* vm) {

83+ HEAP_CHECK(vm)

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

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

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

84

86

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

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

86− char* oldheap = vm -> heap;

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

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

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

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

88

91

89− vm->heap = newheap;

92+ vm->heap.heap = newheap;

90− vm->heap_next = newheap;

93+ vm->heap.next = newheap;

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

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

92−

93− vm->collections++;

94

95

95 VAL* root;

96 VAL* root;

96

97

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

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

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

112 // for next time.

113 // for next time.

113

114

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

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

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

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

116 }

117 }

117− vm->oldheap = oldheap;

118+ vm->heap.old = oldheap;

118

119

119− // gcInfo(vm, 0);

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

121+ HEAP_CHECK(vm)

120}

122}

121

123

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

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

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

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

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

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

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

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

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

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

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

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

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

130}

rts/idris_heap.cnew file+125

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

1+#include "idris_heap.h"

2+#include "idris_rts.h"

3+

4+#include <stdlib.h>

5+#include <stddef.h>

6+#include <stdio.h>

7+

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

3+

4+#include <stddef.h>

5+

6+typedef struct {

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

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

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

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

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

12+

13+ char* old;

14+} Heap;

15+

16+

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

18+void free_heap(Heap * heap);

19+

20+

21+#ifdef IDRIS_DEBUG

22+void heap_check_all(Heap * heap);

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

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

25+#else

26+#define HEAP_CHECK(vm)

27+#endif // IDRIS_DEBUG

28+

29+#endif // _IDRIS_HEAP_H

rts/idris_main.c+26−5

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

1+#include "idris_opts.h"

2+#include "idris_stats.h"

3+#include "idris_rts.h"

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

5+RTSOpts opts = {

6+ .init_heap_size = 4096000,

7+ .max_stack_size = 4096000,

8+ .show_summary = 0

9+};

10+

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

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

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

13+

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

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

3 _idris__123_runMain0_125_(vm, NULL);

15 _idris__123_runMain0_125_(vm, NULL);

4− //_idris_main(vm, NULL);

16+

5−#ifdef IDRIS_TRACE

17+#ifdef IDRIS_DEBUG

18+ if (opts.show_summary) {

6− idris_gcInfo(vm, 1);

19+ idris_gcInfo(vm, 1);

20+ }

7#endif

21#endif

22+

8− terminate(vm);

23+ Stats stats = terminate(vm);

24+

25+ if (opts.show_summary) {

26+ print_stats(&stats);

27+ }

28+

29+ return EXIT_SUCCESS;

9}

30}

rts/idris_opts.cnew file+110

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

1+#include "idris_opts.h"

2+

3+#include <stdlib.h>

4+#include <stddef.h>

5+#include <stdio.h>

6+#include <string.h>

7+

8+

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

3+

4+#include <stddef.h>

5+#include <stdio.h>

6+

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+35−26

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

10#include "idris_gc.h"

11#include "idris_bitstring.h"

12

13+

13VM* init_vm(int stack_size, size_t heap_size,

14VM* init_vm(int stack_size, size_t heap_size,

14 int max_threads, // not implemented yet

15 int max_threads, // not implemented yet

15 int argc, char* argv[]) {

16 int argc, char* argv[]) {

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

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

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

19

17

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

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

19+ STATS_INIT_STATS(vm->stats)

20+ STATS_ENTER_INIT(vm->stats)

21+

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

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

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

25+

21 vm->valstack = valstack;

26 vm->valstack = valstack;

22 vm->valstack_top = valstack;

27 vm->valstack_top = valstack;

23 vm->valstack_base = valstack;

28 vm->valstack_base = valstack;

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

26 vm->floatstack = floatstack;

31 vm->floatstack = floatstack;

27 vm->floatstack_ptr = floatstack;

32 vm->floatstack_ptr = floatstack;

28 vm->stack_max = valstack + stack_size;

33 vm->stack_max = valstack + stack_size;

34+

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

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

30− vm->oldheap = NULL;

36+

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

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

33− vm->heap_size = heap_size;

34− vm->collections = 0;

35− vm->allocations = 0;

36− vm->heap_growth = heap_size;

37 vm->ret = NULL;

38 vm->reg1 = NULL;

39

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

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

61 }

62

63+ STATS_LEAVE_INIT(vm->stats)

63 return vm;

64 return vm;

64}

65}

65

66

66−void terminate(VM* vm) {

67+Stats terminate(VM* vm) {

68+ Stats stats = vm->stats;

69+ STATS_ENTER_EXIT(stats)

70+

67 free(vm->inbox);

71 free(vm->inbox);

68 free(vm->valstack);

72 free(vm->valstack);

69 free(vm->intstack);

73 free(vm->intstack);

70 free(vm->floatstack);

74 free(vm->floatstack);

71− free(vm->heap);

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

72 free(vm->argv);

76 free(vm->argv);

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

77+

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

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

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

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

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

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

77 free(vm);

81 free(vm);

82+

83+ STATS_LEAVE_EXIT(stats)

84+ return stats;

78}

85}

79

86

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

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

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

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

82 idris_gc(vm);

89 idris_gc(vm);

83 }

90 }

84

91

@@ -109,13 +116,13 @@ void* allocate(VM* vm, size_t size, int outerlock) {

109

116

110 size_t chunk_size = size + sizeof(size_t);

117 size_t chunk_size = size + sizeof(size_t);

111

118

112− if (vm -> heap_next + chunk_size < vm -> heap_end) {

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

113− vm->allocations += chunk_size;

120+ STATS_ALLOC(vm->stats, chunk_size)

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

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

115− *((size_t*)(vm->heap_next)) = chunk_size;

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

116− vm -> heap_next += chunk_size;

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

117

124

118− assert(vm->heap_next <= vm->heap_end);

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

119

126

120 memset(ptr, 0, size);

127 memset(ptr, 0, size);

121

128

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

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

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

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

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

217 dumpVal(*root);

224 dumpVal(*root);

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

219 printf("\n");

226 printf("\n");

220 }

227 }

221 printf("RET: ");

228 printf("RET: ");

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

408 callvm->processes--;

415 callvm->processes--;

409

416

410 free(td);

417 free(td);

418+

411− terminate(vm);

419+ Stats stats = terminate(vm);

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

412 return NULL;

421 return NULL;

413}

422}

414

423

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

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

416− 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,

417 callvm->max_threads,

426 callvm->max_threads,

418 0, NULL);

427 0, NULL);

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

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

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

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

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

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

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

502

511

503− int gcs = dest->collections;

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

504 pthread_mutex_lock(&dest->alloc_lock);

513 pthread_mutex_lock(&dest->alloc_lock);

505 VAL dmsg = copyTo(dest, msg);

514 VAL dmsg = copyTo(dest, msg);

506 pthread_mutex_unlock(&dest->alloc_lock);

515 pthread_mutex_unlock(&dest->alloc_lock);

507

516

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

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

509 // a collection will have invalidated the copy

518 // a collection will have invalidated the copy

510 pthread_mutex_lock(&dest->alloc_lock);

519 pthread_mutex_lock(&dest->alloc_lock);

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

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

rts/idris_rts.h+9−10

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

9#include <pthread.h>

10#include <stdint.h>

11

12+#include "idris_heap.h"

13+#include "idris_stats.h"

14+

12// Closures

15// Closures

13

16

14typedef enum {

17typedef enum {

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

47 VAL* valstack_base;

50 VAL* valstack_base;

48 int* intstack_ptr;

51 int* intstack_ptr;

49 double* floatstack_ptr;

52 double* floatstack_ptr;

50− char* heap;

51− char* oldheap;

52− char* heap_next;

53− char* heap_end;

54 VAL* stack_max;

53 VAL* stack_max;

55−

54+

55+ Heap heap;

56+

56 pthread_mutex_t inbox_lock;

57 pthread_mutex_t inbox_lock;

57 pthread_mutex_t inbox_block;

58 pthread_mutex_t inbox_block;

58 pthread_mutex_t alloc_lock;

59 pthread_mutex_t alloc_lock;

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

66

67

67 int processes; // Number of child processes

68 int processes; // Number of child processes

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

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

70+

71+ Stats stats;

69

72

70 int argc;

73 int argc;

71 VAL* argv; // command line arguments

74 VAL* argv; // command line arguments

72

75

73− size_t heap_size;

74− size_t heap_growth;

75− int allocations;

76− int collections;

77 VAL ret;

76 VAL ret;

78 VAL reg1;

77 VAL reg1;

79} VM;

78} VM;

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

83 int max_threads,

82 int max_threads,

84 int argc, char* argv[]);

83 int argc, char* argv[]);

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

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

86−void terminate(VM* vm);

85+Stats terminate(VM* vm);

87

86

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

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

89// and return nothing.

88// and return nothing.

rts/idris_stats.cnew file+53

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

1+#include "idris_stats.h"

2+

3+#include <stdio.h>

4+#include <locale.h>

5+

6+#ifdef IDRIS_ENABLE_STATS

7+

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

3+

4+#include <time.h>

5+

6+// Should not be defined in release.

7+#define IDRIS_ENABLE_STATS

8+

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

10+typedef struct {

11+#ifdef IDRIS_ENABLE_STATS

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

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

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

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

16+

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

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

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

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

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

22+#endif // IDRIS_ENABLE_STATS

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

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

25+

26+void print_stats(const Stats * stats);

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

28+

29+

30+#ifdef IDRIS_ENABLE_STATS

31+

32+#ifndef MAX

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

34+#endif

35+

36+#define STATS_INIT_STATS(stats) \

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

38+ stats.start_time = clock();

39+

40+#define STATS_ALLOC(stats, size) \

41+ stats.allocations += size; \

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

43+

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

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

46+

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

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

49+

50+#define STATS_ENTER_GC(stats, heap_size) \

51+ clock_t _start_time = clock(); \

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

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

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

55+ stats.gc_time += _pause; \

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

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

58+ stats.copied += heap_occuped; \

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

60+

61+#else

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

63+#define STATS_ENTER_INIT(stats)

64+#define STATS_LEAVE_INIT(stats)

65+#define STATS_ENTER_EXIT(stats)

66+#define STATS_LEAVE_EXIT(stats)

67+#define STATS_ALLOC(stats, size)

68+#define STATS_ENTER_GC(stats, heap_size)

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

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

71+#endif // IDRIS_ENABLE_STATS

72+

73+#endif // _IDRIS_STATS_H

src/Core/CaseTree.hs+8−2

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

167

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

169 TC CaseDef

170−simpleCase tc cover phase fc []

170+simpleCase tc cover phase fc cs

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

172+ case r of

173+ Impossible -> False

174+ _ -> True) cs)

175+ where

176+ sc' tc cover phase fc []

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

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

172−simpleCase tc cover phase fc cs

178+ sc' tc cover phase fc cs

173 = let proj = phase == RunTime

179 = let proj = phase == RunTime

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

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

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

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

src/Core/Elaborate.hs+2−2

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

471

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

473simple_app fun arg =

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

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

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

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

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

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

478 claim a RType

src/Core/ProofState.hs+6−3

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

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

156unify' ctxt env topx topy =

157 do ps <- get

158+ let dont = dontunify ps

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

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

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

159−-- trace ("Unified " ++ show (topx, topy) ++ " in " ++ show env ++

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

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

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

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

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

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

162-- -- ++ show (pterm ps)

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

163-- ++ "\n----------") $

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

src/Core/Unify.hs+13−9

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

29

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

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

32−unify ctxt env topx topy injtc holes =

32+unify ctxt env topx topy dont holes =

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

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

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

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

54

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

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

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

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

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

58− injective (App f a) = injective f

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

59 injective _ = False

60 injective _ = False

60

61

61 notP (P _ _ _) = False

62 notP (P _ _ _) = False

@@ -97,9 +98,9 @@ unify ctxt env topx topy injtc holes =

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

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

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

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

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

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

100− = unifyFail tx ty

101+ = unifyTmpFail tx ty

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

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

102− = unifyFail tx ty

103+ = unifyTmpFail tx ty

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

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

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

105 | holeIn env x || x `elem` holes

105 = do UI s f <- get

106 = do UI s f <- get

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

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

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

129

130

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

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

131− | injective fx && metavarApp appy

132+ | injective fx && metavarApp appy

132− || injective fy && metavarApp appx

133+ || injective fy && metavarApp appx

133 || injective fx && injective fy

134 || injective fx && injective fy

134 || fx == fy

135 || fx == fy

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

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

@@ -165,7 +166,7 @@ unify ctxt env topx topy injtc holes =

165 unArgs uf argsx argsy

166 unArgs uf argsx argsy

166 else unifyTmpFail appx appy

167 else unifyTmpFail appx appy

167 where hnormalise [] _ _ t = t

168 where hnormalise [] _ _ t = t

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

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

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

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

170 | x /= y = unifyFail appx appy

171 | x /= y = unifyFail appx appy

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

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

@@ -186,6 +187,8 @@ unify ctxt env topx topy injtc holes =

186

187

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

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

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

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

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

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

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

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

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

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

191

194

@@ -199,7 +202,8 @@ unify ctxt env topx topy injtc holes =

199 sameStruct _ _ = False

202 sameStruct _ _ = False

200

203

201 metavar t = case t of

204 metavar t = case t of

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

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

206+ not (x `elem` dont)

203 _ -> False

207 _ -> False

204 pat t = case t of

208 pat t = case t of

205 P _ x _ -> x `elem` holes || patIn env x

209 P _ x _ -> x `elem` holes || patIn env x

src/Idris/AbsSyntax.hs+1−1

@@ -352,7 +352,7 @@ setImportDirs fps = do i <- getIState

352

353allImportDirs :: IState -> Idris [FilePath]

354allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

355− return ("." : optdirs)

355+ return ("." : reverse optdirs)

356

357impShow :: Idris Bool

358impShow = do i <- getIState

src/Idris/ElabTerm.hs+4−6

@@ -57,6 +57,7 @@ build ist info pattern fn tm

57 resolveTC 7 fn ist) ivs

58 probs <- get_probs

59 tm <- get_term

60+ ctxt <- get_context

60 case probs of

61 case probs of

61 [] -> return ()

62 [] -> return ()

62 ((_,_,_,e):es) -> lift (Error e)

63 ((_,_,_,e):es) -> lift (Error e)

@@ -125,8 +126,10 @@ elab ist info pattern tcgen fn tm

125 g <- goal

126 g <- goal

126 tm <- get_term

127 tm <- get_term

127 ps <- get_probs

128 ps <- get_probs

129+ hs <- get_holes

128-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

130-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

129−-- ++ "\n" ++ show tm

131+-- -- ++ "\n" ++ show tm

132+-- ++ "\nholes " ++ show hs

130-- ++ "\nproblems " ++ show ps

133-- ++ "\nproblems " ++ show ps

131-- ++ "\n-----------\n") $

134-- ++ "\n-----------\n") $

132 elab' ina t'

135 elab' ina t'

@@ -205,13 +208,8 @@ elab ist info pattern tcgen fn tm

205 trySeq' deferr (x : xs)

208 trySeq' deferr (x : xs)

206 = try' (elab' ina x) (trySeq' deferr xs) True

209 = try' (elab' ina x) (trySeq' deferr xs) True

207 elab' ina (PPatvar fc n) | pattern = patvar n

210 elab' ina (PPatvar fc n) | pattern = patvar n

208−-- = do env <- get_env

209−-- case lookup n env of

210−-- Just (PVar _) -> elab' ina Placeholder

211−-- _ -> patvar n

212 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

211 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

213 = do ctxt <- get_context

212 = do ctxt <- get_context

214− env <- get_env

215 let defined = case lookupTy Nothing n ctxt of

213 let defined = case lookupTy Nothing n ctxt of

216 [] -> False

214 [] -> False

217 _ -> True

215 _ -> True

test/reg012/expected−3

@@ -1,3 +0,0 @@

1−5

2−1

3−0

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

5+

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/run+2−3

@@ -1,4 +1,3 @@

1#!/bin/bash

2−idris $@ reg012.idr -o reg012

2+idris $@ reg012.lidr --check

3−./reg012

4−rm -f reg012 *.ibc

3+rm -f *.ibc

test/reg013/expectednew file+3

@@ -0,0 +1,3 @@

1+5

2+1

3+0

test/reg012/reg012.idr → test/reg013/reg013.idrrenamed

The content is the same.

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

tutorial/idris-tutorial.pdf

Binary file not shown.