e261167 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add some string primitives (may need latest Epic)

commite2611670ea2efe453869c7f72495c4cba907d6c3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 14 Dec 2011, 22:13 (15 years ago) parent72c7dba

8 files changed+72−7

compare with master

unifiedsplit

lib/builtins.idr+15 lib/prelude.idr+8 src/Idris/Primitives.hs+29−1 test/test003/expected+4−1 test/test003/lit.lidr+10−1 tutorial/Makefile+2−2 tutorial/idris-tutorial.tex+2−2 tutorial/typesfuns.tex+2

lib/builtins.idr+15

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

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

195195(++) = prim__concat;

196196

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+

197212}

lib/prelude.idr+8

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

3232 show = prim__floatToStr;

3333}

3434

35+instance Show Char where {

36+ show x = strCons x "";

37+}

38+

39+instance Show String where {

40+ show = id;

41+}

42+

3543instance Show Bool where {

3644 show True = "True";

3745 show False = "False";

src/Idris/Primitives.hs+29−1

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

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

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

5050

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+

5157primitives =

5258 -- operators

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

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

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

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

130136 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"))

132148 ]

133149

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

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

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

183199p_floatLog _ = Nothing

184200

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+

185213elabPrim :: Prim -> Idris ()

186214elabPrim (Prim n ty i def epic)

187215 = do updateContext (addOperator n ty i def)

test/test003/expected+4−1

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

11./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 @@

11> module lit;

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

5+> st : String;

6+> st = "abcdefg";

38Literate main program

510> 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

3333 $(DITAA) -o -E $<

3434

3535todropbox: .PHONY

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

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

3737

3838fromdropbox: .PHONY

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

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

4040

4141.PHONY:

tutorial/idris-tutorial.tex+2−2

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

1010

1111\newcommand{\Idris}{\textsc{Idris}}

1212

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

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

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

1515

1616\begin{document}

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

3131\section{Theorem Proving}

3232\section{Provisional Definitions}

3333\section{Syntax Extensions}

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

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

3535

3636\input{miscellany}

3737

tutorial/typesfuns.tex+2

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

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

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

293293

294+\subsubsection{Dependent Function Types}

295+

294296\subsubsection{Implicit Arguments}

295297

296298\subsection{Useful Data Types}