git.iko.soy/Idris-dev
on master help sign in
Added Cast to the prelude, and defined casts between primitives
commit628b851aca20aa02edbf1e0b435db2584b55c2f1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 18:06 (15 years ago) parent8b1e498
8 files changed+89−7
compare with master
unifiedsplit
lib/prelude.idr+1 lib/prelude/cast.idr+49 lib/prelude/nat.idr+5 lib/prelude/strings.idr+7 tutorial/examples/binary.idr+1−2 tutorial/examples/interp.idr+1−1 tutorial/interp.tex+24−2 tutorial/provisional.tex+1−2
lib/prelude.idr+1
@@ -3,6 +3,7 @@ module prelude
33import builtins
44import io
55
6+import prelude.cast
67import prelude.nat
78import prelude.list
89import 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 @@
11module prelude.nat
22
33import builtins
4+import prelude.cast
45
56%access public
67
78data Nat = O | S Nat
89
10+instance Cast Nat Int where
11+ cast O = 0
12+ cast (S k) = 1 + cast k
13+
914plus : Nat -> Nat -> Nat
1015plus O y = y
1116plus (S k) y = S (plus k y)
lib/prelude/strings.idr+7
@@ -3,6 +3,7 @@ module prelude.strings
33import builtins
44import prelude.list
55import prelude.char
6+import prelude.cast
67
78-- Some more complex string operations
89
@@ -32,6 +33,12 @@ pack : List Char -> String
3233pack [] = ""
3334pack (x :: xs) = strCons x (pack xs)
3435
36+instance Cast String (List Char) where
37+ cast = unpack
38+
39+instance Cast (List Char) String where
40+ cast = pack
41+
3542span : (Char -> Bool) -> String -> (String, String)
3643span p xs with (strM xs)
3744 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
3434main : IO ()
3535main = do putStr "Enter a number: "
3636 x <- getLine
37− let n = prim__strToInt x
38− let b = natToBin (fromInteger n)
37+ let b = natToBin (fromInteger (cast x))
3938 print b
4039
4140---------- Proofs ----------
tutorial/examples/interp.idr+1−1
@@ -60,5 +60,5 @@ testFac = interp [] fact 4
6060main : IO ()
6161main = do putStr "Enter a number: "
6262 x <- getLine
63− print (interp [] fact (prim__strToInt x))
63+ print (interp [] fact (cast x))
6464
tutorial/interp.tex+24−2
@@ -322,13 +322,14 @@ on user input:
322322main : IO ()
323323main = do putStr "Enter a number: "
324324 x <- getLine
325− print (interp [] fact (prim__strToInt x))
325+ print (interp [] fact (cast x))
326326
327327\end{SaveVerbatim}
328328\useverb{factmain}
329329
330330\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
332333an integer, giving 0 if the input is invalid. An example run of this program
333334at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
334335
@@ -350,3 +351,24 @@ Enter a number: 6
350351\end{SaveVerbatim}
351352\codefig{factrun}{Running the well-typed interpreter}
352353
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.
284284main : IO ()
285285main = do putStr "Enter a number: "
286286 x <- getLine
287− let n = prim__strToInt x
288− let b = natToBin (fromInteger n)
287+ let b = natToBin (fromInteger (cast x))
289288 print b
290289
291290\end{SaveVerbatim}