628b851 · Idris-dev · git.iko.soy

lib/prelude.idr+1

compare with master

unifiedsplit

@@ -3,6 +3,7 @@ module prelude

3import builtins

4import io

5

6+import prelude.cast

6import prelude.nat

7import prelude.nat

7import prelude.list

8import prelude.list

8import prelude.maybe

9import prelude.maybe

lib/prelude/cast.idrnew file+49

@@ -0,0 +1,49 @@

1+module prelude.cast

2+

3+class Cast a b where

4+ cast : a -> b

5+

6+-- String casts

7+

8+instance Cast String Int where

9+ cast = prim__strToInt

10+

11+instance Cast String Float where

12+ cast = prim__strToFloat

13+

14+instance Cast String Integer where

15+ cast = prim__strToBigInt

16+

17+-- Int casts

18+

19+instance Cast Int String where

20+ cast = prim__intToStr

21+

22+instance Cast Int Float where

23+ cast = prim__intToFloat

24+

25+instance Cast Int Integer where

26+ cast = prim__intToBigInt

27+

28+instance Cast Int Char where

29+ cast = prim__intToChar

30+

31+-- Float casts

32+

33+instance Cast Float String where

34+ cast = prim__floatToStr

35+

36+instance Cast Float Int where

37+ cast = prim__floatToInt

38+

39+-- Integer casts

40+

41+instance Cast Integer String where

42+ cast = prim__bigIntToStr

43+

44+-- Char casts

45+

46+instance Cast Char Int where

47+ cast = prim__charToInt

48+

49+

lib/prelude/nat.idr+5

@@ -1,11 +1,16 @@

1module prelude.nat

2

3import builtins

4+import prelude.cast

4

5

5%access public

6%access public

6

7

7data Nat = O | S Nat

8data Nat = O | S Nat

8

9

10+instance Cast Nat Int where

11+ cast O = 0

12+ cast (S k) = 1 + cast k

13+

9plus : Nat -> Nat -> Nat

14plus : Nat -> Nat -> Nat

10plus O y = y

15plus O y = y

11plus (S k) y = S (plus k y)

16plus (S k) y = S (plus k y)

lib/prelude/strings.idr+7

@@ -3,6 +3,7 @@ module prelude.strings

3import builtins

4import prelude.list

5import prelude.char

6+import prelude.cast

6

7

7-- Some more complex string operations

8-- Some more complex string operations

8

9

@@ -32,6 +33,12 @@ pack : List Char -> String

32pack [] = ""

33pack [] = ""

33pack (x :: xs) = strCons x (pack xs)

34pack (x :: xs) = strCons x (pack xs)

34

35

36+instance Cast String (List Char) where

37+ cast = unpack

38+

39+instance Cast (List Char) String where

40+ cast = pack

41+

35span : (Char -> Bool) -> String -> (String, String)

42span : (Char -> Bool) -> String -> (String, String)

36span p xs with (strM xs)

43span p xs with (strM xs)

37 span p "" | StrNil = ("", "")

44 span p "" | StrNil = ("", "")

tutorial/examples/binary.idr+1−2

@@ -34,8 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else O

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− let n = prim__strToInt x

38− let b = natToBin (fromInteger n)

37+ let b = natToBin (fromInteger (cast x))

39 print b

38 print b

40

39

41---------- Proofs ----------

40---------- Proofs ----------

tutorial/examples/interp.idr+1−1

@@ -60,5 +60,5 @@ testFac = interp [] fact 4

60main : IO ()

61main = do putStr "Enter a number: "

62 x <- getLine

63− print (interp [] fact (prim__strToInt x))

63+ print (interp [] fact (cast x))

64

tutorial/interp.tex+24−2

@@ -322,13 +322,14 @@ on user input:

322main : IO ()

323main = do putStr "Enter a number: "

324 x <- getLine

325− print (interp [] fact (prim__strToInt x))

325+ print (interp [] fact (cast x))

326

327\end{SaveVerbatim}

328\useverb{factmain}

329

330\noindent

331−Here, \texttt{prim\_\_strToInt} is a primitive function which converts a string to

331+Here, \texttt{cast} is an overloaded function which converts a value from one

332+type to another if possible. Here, it conversts a string to

332an integer, giving 0 if the input is invalid. An example run of this program

333an integer, giving 0 if the input is invalid. An example run of this program

333at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

334at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

334

335

@@ -350,3 +351,24 @@ Enter a number: 6

350\end{SaveVerbatim}

351\end{SaveVerbatim}

351\codefig{factrun}{Running the well-typed interpreter}

352\codefig{factrun}{Running the well-typed interpreter}

352

353

354+\subsubsection*{Aside: \texttt{cast}}

355+

356+The prelude defines a type class \texttt{Cast} which allows conversion between

357+types:

358+

359+\begin{SaveVerbatim}{castclass}

360+

361+class Cast a b where

362+ cast : a -> b

363+

364+\end{SaveVerbatim}

365+\useverb{castclass}

366+

367+\noindent

368+It is a \emph{multi-parameter} type class, defining the source type and object

369+type of the cast. It must be possible for the type checker \remph{both}

370+parameters at the point where the cast is applied.

371+There are casts defined between all of the primitive types, as far as

372+they make sense.

373+

374+

tutorial/provisional.tex+1−2

@@ -284,8 +284,7 @@ outputs it in binary.

284main : IO ()

285main = do putStr "Enter a number: "

286 x <- getLine

287− let n = prim__strToInt x

288− let b = natToBin (fromInteger n)

287+ let b = natToBin (fromInteger (cast x))

289 print b

288 print b

290

289

291\end{SaveVerbatim}

290\end{SaveVerbatim}