git.iko.soy/Idris-dev
on master help sign in
tinker tinker
commit1c9392ec49db18dbf264d6533e771f1e7af3610f authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 15 Oct 2011, 13:50 (15 years ago) parentbda1f6f
4 files changed+11−1
compare with master
unifiedsplit
impl-paper/Makefile+1−1 impl-paper/impldtp.tex+2 interp.idr+7 src/Idris/Compiler.hs+1
impl-paper/Makefile+1−1
@@ -3,7 +3,7 @@ PAPER = impldtp
33all: ${PAPER}.pdf
44
55TEXFILES = ${PAPER}.tex intro.tex conclusions.tex overview.tex hll.tex\
6− typechecking.tex proofstate.tex elaboration.tex
6+ typechecking.tex proofstate.tex elaboration.tex compiling.tex
77
88DIAGS =
99
impl-paper/impldtp.tex+2
@@ -91,6 +91,8 @@ KY16 9SX
9191
9292\input{elaboration.tex}
9393
94+\input{compiling.tex}
95+
9496\input{conclusions.tex}
9597
9698\bibliographystyle{acmtrans}
interp.idr+7
@@ -53,3 +53,10 @@ using (G : Vect Ty n) {
5353test : Nat;
5454test = interp Empty eAdd (S (S O)) (S (S O));
5555
56+natToStr : Nat -> String;
57+natToStr O = "O";
58+natToStr (S k) = "s" ++ natToStr k;
59+
60+main : IO ();
61+main = putStrLn (natToStr test);
62+
src/Idris/Compiler.hs+1
@@ -70,6 +70,7 @@ doForeign (_ : fgn : args)
7070 = let tys = getFTypes fgnArgTys
7171 rty = mkEty ret in
7272 do args' <- mapM epic args
73+ -- wrap it in a prim__IO
7374 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
7475 | otherwise = fail "Badly formed foreign function call"
7576