397542c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A load of primitives and library stuff

commit397542cd3e607d8cd772efd96805bdb95bd1b9b5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 21 Dec 2011, 01:31 (15 years ago) parentd8edff9

4 files changed+96−4

compare with master

unifiedsplit

lib/prelude.idr+30 lib/prelude/char.idr+9 lib/prelude/list.idr+3 src/Idris/Primitives.hs+54−4

lib/prelude.idr+30

@@ -129,6 +129,36 @@ exp x = prim__floatExp x;

129129log : Float -> Float;

130130log x = prim__floatLog x;

131131

132+pi : Float;

133+pi = 3.141592653589793;

134+

135+sin : Float -> Float;

136+sin x = prim__floatSin x;

137+

138+cos : Float -> Float;

139+cos x = prim__floatCos x;

140+

141+tan : Float -> Float;

142+tan x = prim__floatTan x;

143+

144+asin : Float -> Float;

145+asin x = prim__floatASin x;

146+

147+acos : Float -> Float;

148+acos x = prim__floatACos x;

149+

150+atan : Float -> Float;

151+atan x = prim__floatATan x;

152+

153+sqrt : Float -> Float;

154+sqrt x = prim__floatSqrt x;

155+

156+floor : Float -> Float;

157+floor x = prim__floatFloor x;

158+

159+ceiling : Float -> Float;

160+ceiling x = prim__floatCeil x;

161+

132162---- some basic io

133163

134164putStr : String -> IO ();

lib/prelude/char.idr+9

@@ -22,4 +22,13 @@ isSpace x = x == ' ' || x == '\t' || x == '\r' ||

2222 x == '\n' || x == '\f' || x == '\v' ||

2323 x == '\xa0';

2424

25+toUpper : Char -> Char;

26+toUpper x = if (isLower x)

27+ then (prim__intToChar (prim__charToInt x - 32))

28+ else x;

29+

30+toLower : Char -> Char;

31+toLower x = if (isUpper x)

32+ then (prim__intToChar (prim__charToInt x + 32))

33+ else x;

2534

lib/prelude/list.idr+3

@@ -38,6 +38,9 @@ filter pred (x :: xs) with (pred x, filter pred xs) {

3838 | (False, fxs) = fxs;

3939}

4040

41+elem : Eq a => a -> List a -> Bool;

42+elem x [] = False;

43+elem x (y :: ys) = if (x == y) then True else (elem x ys);

4144

4245sort : Ord a => List a -> List a;

4346sort [] = [];

src/Idris/Primitives.hs+54−4

@@ -41,6 +41,8 @@ eOpFn ty rty op = ([E.name "x", E.name "y"],

4141

4242strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]

4343intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]

44+charToInt x = x

45+intToChar x = x

4446intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]

4547strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]

4648bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]

@@ -51,6 +53,15 @@ floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]

5153

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

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

56+floatSin x = foreign_ tyFloat "sin" [(x, tyFloat)]

57+floatCos x = foreign_ tyFloat "cos" [(x, tyFloat)]

58+floatTan x = foreign_ tyFloat "tan" [(x, tyFloat)]

59+floatASin x = foreign_ tyFloat "asin" [(x, tyFloat)]

60+floatACos x = foreign_ tyFloat "acos" [(x, tyFloat)]

61+floatATan x = foreign_ tyFloat "atan" [(x, tyFloat)]

62+floatFloor x = foreign_ tyFloat "floor" [(x, tyFloat)]

63+floatCeil x = foreign_ tyFloat "ceil" [(x, tyFloat)]

64+floatSqrt x = foreign_ tyFloat "sqrt" [(x, tyFloat)]

5465

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

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

@@ -137,6 +148,10 @@ primitives =

137148 ([E.name "x"], strToInt (fun "x")),

138149 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

139150 ([E.name "x"], intToStr (fun "x")),

151+ Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

152+ ([E.name "x"], charToInt (fun "x")),

153+ Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

154+ ([E.name "x"], intToChar (fun "x")),

140155 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

141156 ([E.name "x"], intToBigInt (fun "x")),

142157 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

@@ -151,10 +166,30 @@ primitives =

151166 ([E.name "x"], intToFloat (fun "x")),

152167 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

153168 ([E.name "x"], floatToInt (fun "x")),

169+

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

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

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

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

174+ Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

175+ ([E.name "x"], floatSin (fun "x")),

176+ Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)

177+ ([E.name "x"], floatCos (fun "x")),

178+ Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)

179+ ([E.name "x"], floatTan (fun "x")),

180+ Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)

181+ ([E.name "x"], floatASin (fun "x")),

182+ Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)

183+ ([E.name "x"], floatACos (fun "x")),

184+ Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)

185+ ([E.name "x"], floatATan (fun "x")),

186+ Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)

187+ ([E.name "x"], floatSqrt (fun "x")),

188+ Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)

189+ ([E.name "x"], floatFloor (fun "x")),

190+ Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)

191+ ([E.name "x"], floatCeil (fun "x")),

192+

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

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

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

@@ -209,6 +244,11 @@ c_intToStr _ = Nothing

209244c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))

210245c_strToInt _ = Nothing

211246

247+c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

248+c_intToChar _ = Nothing

249+c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

250+c_charToInt _ = Nothing

251+

212252c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))

213253c_intToBigInt _ = Nothing

214254

@@ -228,10 +268,20 @@ c_floatToInt _ = Nothing

228268c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))

229269c_intToFloat _ = Nothing

230270

231−p_floatExp [VConstant (Fl x)] = Just $ VConstant (Fl (exp x))

232−p_floatExp _ = Nothing

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

234−p_floatLog _ = Nothing

271+p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

272+p_fPrim f _ = Nothing

273+

274+p_floatExp = p_fPrim exp

275+p_floatLog = p_fPrim log

276+p_floatSin = p_fPrim sin

277+p_floatCos = p_fPrim cos

278+p_floatTan = p_fPrim tan

279+p_floatASin = p_fPrim asin

280+p_floatACos = p_fPrim acos

281+p_floatATan = p_fPrim atan

282+p_floatSqrt = p_fPrim sqrt

283+p_floatFloor = p_fPrim (fromInteger . floor)

284+p_floatCeil = p_fPrim (fromInteger . ceiling)

235285

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

237287p_strHead _ = Nothing