e7906ba · Idris-dev · git.iko.soy

Setup.hs+9

compare with master

unifiedsplit

@@ -26,6 +26,11 @@ installStdLib pkg local verbosity copy

26 , "TARGET=" ++ idir

27 , "IDRIS=" ++ icmd

28 ]

29+ make verbosity

30+ [ "-C", "support", "install"

31+ , "TARGET=" ++ idir

32+ , "IDRIS=" ++ icmd

33+ ]

29

34

30checkStdLib local verbosity

35checkStdLib local verbosity

31 = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

36 = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

@@ -34,6 +39,10 @@ checkStdLib local verbosity

34 [ "-C", "lib", "check"

39 [ "-C", "lib", "check"

35 , "IDRIS=" ++ icmd

40 , "IDRIS=" ++ icmd

36 ]

41 ]

42+ make verbosity

43+ [ "-C", "support", "check"

44+ , "IDRIS=" ++ icmd

45+ ]

37

46

38-- Install libraries during both copy and install

47-- Install libraries during both copy and install

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

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

idris.cabal+2−1

@@ -41,7 +41,8 @@ Cabal-Version: >= 1.6

41Build-type: Custom

42

43Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

44+ lib/control/monad/*.idr lib/language/*.idr

44− lib/control/monad/*.idr tutorial/examples/*.idr

45+ tutorial/examples/*.idr

45

46

46source-repository head

47source-repository head

47 type: git

48 type: git

lib/Makefile+4−1

@@ -7,19 +7,22 @@ recheck: clean check

7install: check

8 mkdir -p $(TARGET)/prelude

9 mkdir -p $(TARGET)/network

10+ mkdir -p $(TARGET)/language

10 mkdir -p $(TARGET)/control/monad

11 mkdir -p $(TARGET)/control/monad

11 install *.ibc $(TARGET)

12 install *.ibc $(TARGET)

12 install prelude/*.ibc $(TARGET)/prelude

13 install prelude/*.ibc $(TARGET)/prelude

13 install network/*.ibc $(TARGET)/network

14 install network/*.ibc $(TARGET)/network

15+ install language/*.ibc $(TARGET)/language

14 install control/monad/*.ibc $(TARGET)/control/monad

16 install control/monad/*.ibc $(TARGET)/control/monad

15

17

16clean: .PHONY

18clean: .PHONY

17 rm -f *.ibc

19 rm -f *.ibc

18 rm -f prelude/*.ibc

20 rm -f prelude/*.ibc

19 rm -f network/*.ibc

21 rm -f network/*.ibc

22+ rm -f language/*.ibc

20 rm -f control/monad/*.ibc

23 rm -f control/monad/*.ibc

21

24

22linecount: .PHONY

25linecount: .PHONY

23− wc -l *.idr network/*.idr prelude/*.idr control/monad/*.idr

26+ wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr

24

27

25.PHONY:

28.PHONY:

lib/checkall.idr+2

@@ -25,5 +25,7 @@ import prelude.complex

25

26import network.cgi

27

28+import language.reflection

29+

28import control.monad.identity

30import control.monad.identity

29import control.monad.state

31import control.monad.state

lib/language/reflection.idrnew file+11

@@ -0,0 +1,11 @@

1+module language.reflection

2+

3+TTName : Set

4+TTName = String

5+

6+data TT = Var TTName

7+ | Lam TTName TT TT

8+ | Pi TTName TT TT

9+ | Let TTName TT TT TT

10+ | App TTName TT TT

11+

src/Idris/Compiler.hs+5−1

@@ -16,6 +16,8 @@ import System.IO

16import System.Directory

17import System.Environment

18

19+import Paths_idris

20+

19import Epic.Epic hiding (Term, Type, Name, fn, compile)

21import Epic.Epic hiding (Term, Type, Name, fn, compile)

20import qualified Epic.Epic as E

22import qualified Epic.Epic as E

21

23

@@ -32,13 +34,15 @@ compile f tm

32 hdrs <- getHdrs

34 hdrs <- getHdrs

33 let incs = map Include hdrs

35 let incs = map Include hdrs

34 so <- getSO

36 so <- getSO

37+ ddir <- liftIO $ getDataDir

38+ let ilib = ddir ++ "/libidris.a"

35 case so of

39 case so of

36 Nothing ->

40 Nothing ->

37 do m <- epicMain tm

41 do m <- epicMain tm

38 let mainval = EpicFn (name "main") m

42 let mainval = EpicFn (name "main") m

39 liftIO $ compileObjWith []

43 liftIO $ compileObjWith []

40 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")

44 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")

41− liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

45+ liftIO $ link ((f ++ ".o") : ilib : objs ++ (map ("-l"++) libs)) f

42 where checkMVs = do i <- get

46 where checkMVs = do i <- get

43 case idris_metavars i \\ primDefs of

47 case idris_metavars i \\ primDefs of

44 [] -> return ()

48 [] -> return ()

support/Makefilenew file+12

@@ -0,0 +1,12 @@

1+OBJS = testidr.o

2+CFLAGS = `epic -includedirs`

3+

4+LIBTARGET = libidris.a

5+

6+check: $(OBJS)

7+ ar -r $(LIBTARGET) $(OBJS)

8+

9+install: check

10+ install $(LIBTARGET) $(TARGET)

11+

12+.PHONY:

support/testidr.cnew file+6

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

1+#include "testidr.h"

2+#include <stdio.h>

3+

4+void testIdr() {

5+ printf("Hello Idris support library!\n");

6+}

support/testidr.hnew file+7

@@ -0,0 +1,7 @@

1+#ifndef __TESTIDR_H

2+#define __TESTIDR_H

3+

4+void testIdr();

5+

6+#endif

7+