git.iko.soy/Idris-dev
on master help sign in
tinker tinker
1c9392eEdwin Brady
impl-paper/Makefile+1−1
compare with master
unifiedsplit
@@ -3,7 +3,7 @@ PAPER = impldtp
3all: ${PAPER}.pdf
3all: ${PAPER}.pdf
4
4
5TEXFILES = ${PAPER}.tex intro.tex conclusions.tex overview.tex hll.tex\
5TEXFILES = ${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
7
7
8DIAGS =
8DIAGS =
9
9
impl-paper/impldtp.tex+2
@@ -91,6 +91,8 @@ KY16 9SX
91
91
92\input{elaboration.tex}
92\input{elaboration.tex}
93
93
94+\input{compiling.tex}
95+
94\input{conclusions.tex}
96\input{conclusions.tex}
95
97
96\bibliographystyle{acmtrans}
98\bibliographystyle{acmtrans}
interp.idr+7
@@ -53,3 +53,10 @@ using (G : Vect Ty n) {
53test : Nat;
53test : Nat;
54test = interp Empty eAdd (S (S O)) (S (S O));
54test = interp Empty eAdd (S (S O)) (S (S O));
55
55
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)
70 = let tys = getFTypes fgnArgTys
70 = let tys = getFTypes fgnArgTys
71 rty = mkEty ret in
71 rty = mkEty ret in
72 do args' <- mapM epic args
72 do args' <- mapM epic args
73+ -- wrap it in a prim__IO
73 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
74 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
74 | otherwise = fail "Badly formed foreign function call"
75 | otherwise = fail "Badly formed foreign function call"
75
76