git.iko.soy/Idris-dev
on master help sign in
rename rts include file
b70780fEdwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -40,7 +40,7 @@ Description: Idris is a general purpose language with full dependent types.
40Cabal-Version: >= 1.6
40Cabal-Version: >= 1.6
41Build-type: Custom
41Build-type: Custom
42
42
43−Data-files: rts/libidris_rts.a rts/closure.h
43+Data-files: rts/libidris_rts.a rts/idris_rts.h
44Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
44Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
45 lib/control/monad/*.idr lib/language/*.idr
45 lib/control/monad/*.idr lib/language/*.idr
46 tutorial/examples/*.idr
46 tutorial/examples/*.idr
iif/ctest.c+1−1
@@ -1,4 +1,4 @@
1−#include <closure.h>
1+#include <idris_rts.h>
2
2
3void plus(VM* vm, VAL* oldbase) {
3void plus(VM* vm, VAL* oldbase) {
4 INITFRAME;
4 INITFRAME;
rts/Makefile+3−3
@@ -1,5 +1,5 @@
1−OBJS = closure.o
1+OBJS = idris_rts.o
2−HDRS = closure.h
2+HDRS = idris_rts.h
3CFLAGS = -g
3CFLAGS = -g
4
4
5LIBTARGET = libidris_rts.a
5LIBTARGET = libidris_rts.a
@@ -17,6 +17,6 @@ install : .PHONY
17clean : .PHONY
17clean : .PHONY
18 rm -f $(OBJS) $(LIBTARGET)
18 rm -f $(OBJS) $(LIBTARGET)
19
19
20−closure.o: closure.h
20+idris_rts.o: idris_rts.h
21
21
22.PHONY:
22.PHONY:
rts/closure.c → rts/idris_rts.crenamed+1−1
@@ -4,7 +4,7 @@
4#include <unistd.h>
4#include <unistd.h>
5#include <stdarg.h>
5#include <stdarg.h>
6
6
7−#include "closure.h"
7+#include "idris_rts.h"
8
8
9VM* init_vm(int stack_size, size_t heap_size) {
9VM* init_vm(int stack_size, size_t heap_size) {
10 VAL* valstack = malloc(stack_size*sizeof(VAL));
10 VAL* valstack = malloc(stack_size*sizeof(VAL));
rts/closure.h → rts/idris_rts.hrenamed+2−2
@@ -1,5 +1,5 @@
1−#ifndef _CLOSURE_H
1+#ifndef _IDRISRTS_H
2−#define _CLOSURE_H
2+#define _IDRISRTS_H
3
3
4#include <stdlib.h>
4#include <stdlib.h>
5#include <stdio.h>
5#include <stdio.h>
src/Core/Elaborate.hs+1−1
@@ -322,7 +322,7 @@ apply fn imps =
322 map fst (filter (not.snd) (zip args (map fst imps)))
322 map fst (filter (not.snd) (zip args (map fst imps)))
323 ES (p, a) s prev <- get
323 ES (p, a) s prev <- get
324 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $
324 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $
325− unified p
325+ unified p
326 let unify = dropGiven dontunify hs
326 let unify = dropGiven dontunify hs
327 put (ES (p { unified = (n, unify) }, a) s prev)
327 put (ES (p { unified = (n, unify) }, a) s prev)
328 end_unify
328 end_unify
src/Idris/ElabTerm.hs+3−1
@@ -234,7 +234,9 @@ elab ist info pattern tcgen fn tm
234 let isinf = f == inferCon || tcname f
234 let isinf = f == inferCon || tcname f
235 ctxt <- get_context
235 ctxt <- get_context
236 let guarded = isConName Nothing f ctxt
236 let guarded = isConName Nothing f ctxt
237+-- when True
238+ try
237− try (do ns <- apply (Var f) (map isph args)
239+ (do ns <- apply (Var f) (map isph args)
238 let (ns', eargs)
240 let (ns', eargs)
239 = unzip $
241 = unzip $
240 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
242 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))