mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
Added support/ directory so that library can use C support files
This commit is contained in:
parent
9e399b2599
commit
e7906ba591
9
Setup.hs
9
Setup.hs
@ -26,6 +26,11 @@ installStdLib pkg local verbosity copy
|
||||
, "TARGET=" ++ idir
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
make verbosity
|
||||
[ "-C", "support", "install"
|
||||
, "TARGET=" ++ idir
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
|
||||
checkStdLib local verbosity
|
||||
= do let icmd = ".." </> buildDir local </> "idris" </> "idris"
|
||||
@ -34,6 +39,10 @@ checkStdLib local verbosity
|
||||
[ "-C", "lib", "check"
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
make verbosity
|
||||
[ "-C", "support", "check"
|
||||
, "IDRIS=" ++ icmd
|
||||
]
|
||||
|
||||
-- Install libraries during both copy and install
|
||||
-- See http://hackage.haskell.org/trac/hackage/ticket/718
|
||||
|
@ -41,7 +41,8 @@ Cabal-Version: >= 1.6
|
||||
Build-type: Custom
|
||||
|
||||
Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
|
||||
lib/control/monad/*.idr tutorial/examples/*.idr
|
||||
lib/control/monad/*.idr lib/language/*.idr
|
||||
tutorial/examples/*.idr
|
||||
|
||||
source-repository head
|
||||
type: git
|
||||
|
@ -7,19 +7,22 @@ recheck: clean check
|
||||
install: check
|
||||
mkdir -p $(TARGET)/prelude
|
||||
mkdir -p $(TARGET)/network
|
||||
mkdir -p $(TARGET)/language
|
||||
mkdir -p $(TARGET)/control/monad
|
||||
install *.ibc $(TARGET)
|
||||
install prelude/*.ibc $(TARGET)/prelude
|
||||
install network/*.ibc $(TARGET)/network
|
||||
install language/*.ibc $(TARGET)/language
|
||||
install control/monad/*.ibc $(TARGET)/control/monad
|
||||
|
||||
clean: .PHONY
|
||||
rm -f *.ibc
|
||||
rm -f prelude/*.ibc
|
||||
rm -f network/*.ibc
|
||||
rm -f language/*.ibc
|
||||
rm -f control/monad/*.ibc
|
||||
|
||||
linecount: .PHONY
|
||||
wc -l *.idr network/*.idr prelude/*.idr control/monad/*.idr
|
||||
wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr
|
||||
|
||||
.PHONY:
|
||||
|
@ -25,5 +25,7 @@ import prelude.complex
|
||||
|
||||
import network.cgi
|
||||
|
||||
import language.reflection
|
||||
|
||||
import control.monad.identity
|
||||
import control.monad.state
|
||||
|
11
lib/language/reflection.idr
Normal file
11
lib/language/reflection.idr
Normal file
@ -0,0 +1,11 @@
|
||||
module language.reflection
|
||||
|
||||
TTName : Set
|
||||
TTName = String
|
||||
|
||||
data TT = Var TTName
|
||||
| Lam TTName TT TT
|
||||
| Pi TTName TT TT
|
||||
| Let TTName TT TT TT
|
||||
| App TTName TT TT
|
||||
|
@ -16,6 +16,8 @@ import System.IO
|
||||
import System.Directory
|
||||
import System.Environment
|
||||
|
||||
import Paths_idris
|
||||
|
||||
import Epic.Epic hiding (Term, Type, Name, fn, compile)
|
||||
import qualified Epic.Epic as E
|
||||
|
||||
@ -32,13 +34,15 @@ compile f tm
|
||||
hdrs <- getHdrs
|
||||
let incs = map Include hdrs
|
||||
so <- getSO
|
||||
ddir <- liftIO $ getDataDir
|
||||
let ilib = ddir ++ "/libidris.a"
|
||||
case so of
|
||||
Nothing ->
|
||||
do m <- epicMain tm
|
||||
let mainval = EpicFn (name "main") m
|
||||
liftIO $ compileObjWith []
|
||||
(mkProgram (incs ++ mainval : ds)) (f ++ ".o")
|
||||
liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
|
||||
liftIO $ link ((f ++ ".o") : ilib : objs ++ (map ("-l"++) libs)) f
|
||||
where checkMVs = do i <- get
|
||||
case idris_metavars i \\ primDefs of
|
||||
[] -> return ()
|
||||
|
12
support/Makefile
Normal file
12
support/Makefile
Normal file
@ -0,0 +1,12 @@
|
||||
OBJS = testidr.o
|
||||
CFLAGS = `epic -includedirs`
|
||||
|
||||
LIBTARGET = libidris.a
|
||||
|
||||
check: $(OBJS)
|
||||
ar -r $(LIBTARGET) $(OBJS)
|
||||
|
||||
install: check
|
||||
install $(LIBTARGET) $(TARGET)
|
||||
|
||||
.PHONY:
|
6
support/testidr.c
Normal file
6
support/testidr.c
Normal file
@ -0,0 +1,6 @@
|
||||
#include "testidr.h"
|
||||
#include <stdio.h>
|
||||
|
||||
void testIdr() {
|
||||
printf("Hello Idris support library!\n");
|
||||
}
|
7
support/testidr.h
Normal file
7
support/testidr.h
Normal file
@ -0,0 +1,7 @@
|
||||
#ifndef __TESTIDR_H
|
||||
#define __TESTIDR_H
|
||||
|
||||
void testIdr();
|
||||
|
||||
#endif
|
||||
|
Loading…
Reference in New Issue
Block a user