e7906ba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added support/ directory so that library can use C support files

commite7906ba591352bdc7ffcfe731e66b74f83a89c9a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 10 Apr 2012, 14:49 (15 years ago) parent9e399b2

9 files changed+58−3

compare with master

unifiedsplit

Setup.hs+9 idris.cabal+2−1 lib/Makefile+4−1 lib/checkall.idr+2 lib/language/reflection.idr+11 src/Idris/Compiler.hs+5−1 support/Makefile+12 support/testidr.c+6 support/testidr.h+7

Setup.hs+9

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

2626 , "TARGET=" ++ idir

2727 , "IDRIS=" ++ icmd

2828 ]

29+ make verbosity

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

31+ , "TARGET=" ++ idir

32+ , "IDRIS=" ++ icmd

33+ ]

2934

3035checkStdLib local verbosity

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

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

3439 [ "-C", "lib", "check"

3540 , "IDRIS=" ++ icmd

3641 ]

42+ make verbosity

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

44+ , "IDRIS=" ++ icmd

45+ ]

3746

3847-- Install libraries during both copy and install

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

idris.cabal+2−1

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

4141Build-type: Custom

4242

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

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

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

45+ tutorial/examples/*.idr

4546

4647source-repository head

4748 type: git

lib/Makefile+4−1

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

77install: check

88 mkdir -p $(TARGET)/prelude

99 mkdir -p $(TARGET)/network

10+ mkdir -p $(TARGET)/language

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

1112 install *.ibc $(TARGET)

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

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

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

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

1517

1618clean: .PHONY

1719 rm -f *.ibc

1820 rm -f prelude/*.ibc

1921 rm -f network/*.ibc

22+ rm -f language/*.ibc

2023 rm -f control/monad/*.ibc

2124

2225linecount: .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

2427

2528.PHONY:

lib/checkall.idr+2

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

2525

2626import network.cgi

2727

28+import language.reflection

29+

2830import control.monad.identity

2931import control.monad.state

lib/language/reflection.idrnew file+11

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

1+module language.reflection

3+TTName : Set

4+TTName = String

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

1616import System.Directory

1717import System.Environment

1818

19+import Paths_idris

20+

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

2022import qualified Epic.Epic as E

2123

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

3234 hdrs <- getHdrs

3335 let incs = map Include hdrs

3436 so <- getSO

37+ ddir <- liftIO $ getDataDir

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

3539 case so of

3640 Nothing ->

3741 do m <- epicMain tm

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

3943 liftIO $ compileObjWith []

4044 (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

4246 where checkMVs = do i <- get

4347 case idris_metavars i \\ primDefs of

4448 [] -> return ()

support/Makefilenew file+12

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

1+OBJS = testidr.o

2+CFLAGS = `epic -includedirs`

4+LIBTARGET = libidris.a

6+check: $(OBJS)

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

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>

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

4+void testIdr();

6+#endif