e261167 · Idris-dev · git.iko.soy

lib/builtins.idr+15

compare with master

unifiedsplit

@@ -194,4 +194,19 @@ div = prim__divInt;

194(++) : String -> String -> String;

195(++) = prim__concat;

196

197+strHead : String -> Char;

198+strHead = prim__strHead;

199+

200+strTail : String -> String;

201+strTail = prim__strTail;

202+

203+strCons : Char -> String -> String;

204+strCons = prim__strCons;

205+

206+strIndex : String -> Int -> Char;

207+strIndex = prim__strIndex;

208+

209+rev : String -> String;

210+rev = prim__strRev;

211+

197}

212}

lib/prelude.idr+8

@@ -32,6 +32,14 @@ instance Show Float where {

32 show = prim__floatToStr;

33}

34

35+instance Show Char where {

36+ show x = strCons x "";

37+}

38+

39+instance Show String where {

40+ show = id;

41+}

42+

35instance Show Bool where {

43instance Show Bool where {

36 show True = "True";

44 show True = "True";

37 show False = "False";

45 show False = "False";

src/Idris/Primitives.hs+29−1

@@ -48,6 +48,12 @@ floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]

48floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]

49floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]

50

51+strIndex x i = foreign_ tyChar "strIndex" [(x, tyString), (i, tyInt)]

52+strHead x = foreign_ tyChar "strHead" [(x, tyString)]

53+strTail x = foreign_ tyString "strTail" [(x, tyString)]

54+strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]

55+strRev x = foreign_ tyString "strrev" [(x, tyString)]

56+

51primitives =

57primitives =

52 -- operators

58 -- operators

53 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

59 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

@@ -128,7 +134,17 @@ primitives =

128 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

134 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

129 ([E.name "x"], floatExp (fun "x")),

135 ([E.name "x"], floatExp (fun "x")),

130 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

136 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

131− ([E.name "x"], floatLog (fun "x"))

137+ ([E.name "x"], floatLog (fun "x")),

138+ Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

139+ ([E.name "x"], strHead (fun "x")),

140+ Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

141+ ([E.name "x"], strTail (fun "x")),

142+ Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

143+ ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")),

144+ Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

145+ ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")),

146+ Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

147+ ([E.name "x"], strRev (fun "x"))

132 ]

148 ]

133

149

134iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

150iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

@@ -182,6 +198,18 @@ p_floatExp _ = Nothing

182p_floatLog [VConstant (Fl x)] = Just $ VConstant (Fl (log x))

198p_floatLog [VConstant (Fl x)] = Just $ VConstant (Fl (log x))

183p_floatLog _ = Nothing

199p_floatLog _ = Nothing

184

200

201+p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

202+p_strHead _ = Nothing

203+p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

204+p_strTail _ = Nothing

205+p_strIndex [VConstant (Str xs), VConstant (I i)]

206+ | i < length xs = Just $ VConstant (Ch (xs!!i))

207+p_strIndex _ = Nothing

208+p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))

209+p_strCons _ = Nothing

210+p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

211+p_strRev _ = Nothing

212+

185elabPrim :: Prim -> Idris ()

213elabPrim :: Prim -> Idris ()

186elabPrim (Prim n ty i def epic)

214elabPrim (Prim n ty i def epic)

187 = do updateContext (addOperator n ty i def)

215 = do updateContext (addOperator n ty i def)

test/test003/expected+4−1

@@ -1,2 +1,5 @@

1./test003a.lidr:1:Program line next to comment

2−Foo

2+a

3+d

4+zabcdefg

5+gfedcba

test/test003/lit.lidr+10−1

@@ -1,6 +1,15 @@

1> module lit;

2

3+Test some string primitives while we're at it

4+

5+> st : String;

6+> st = "abcdefg";

7+

3Literate main program

8Literate main program

4

9

5> main : IO ();

10> main : IO ();

6−> main = putStrLn "Foo";

11+> main = do { putStrLn (show (strHead st));

12+> putStrLn (show (strIndex st 3));

13+> putStrLn (strCons 'z' st);

14+> putStrLn (rev st); };

15+

tutorial/Makefile+2−2

@@ -33,9 +33,9 @@ progress: .PHONY

33 $(DITAA) -o -E $<

34

35todropbox: .PHONY

36− cp ${SOURCES} ~/Dropbox/TeX/ImplDTP/

36+ cp ${SOURCES} ~/Dropbox/TeX/idris-tutorial

37

38fromdropbox: .PHONY

39− cp ~/Dropbox/TeX/ImplDTP/* .

39+ cp ~/Dropbox/TeX/idris-tutorial/* .

40

41.PHONY:

tutorial/idris-tutorial.tex+2−2

@@ -10,7 +10,7 @@

10

11\newcommand{\Idris}{\textsc{Idris}}

12

13−\title{Dependently Typed Programming in \Idris{}}

13+\title{Programming in \Idris{}: a tutorial}

14\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}

15

16\begin{document}

@@ -31,7 +31,7 @@

31\section{Theorem Proving}

32\section{Provisional Definitions}

33\section{Syntax Extensions}

34−\section{Example: A verified binary adder}

34+%\section{Example: A verified binary adder}

35

36\input{miscellany}

37

tutorial/typesfuns.tex+2

@@ -291,6 +291,8 @@ impossible. Since there is no element of \texttt{Fin O}, and the location is a

291look up an element in an empty vector would give a compile time type error,

292since it would force \texttt{n} to be \tDC{O}.

293

294+\subsubsection{Dependent Function Types}

295+

294\subsubsection{Implicit Arguments}

296\subsubsection{Implicit Arguments}

295

297

296\subsection{Useful Data Types}

298\subsection{Useful Data Types}