86b4541 · Idris-dev · git.iko.soy

contribs/lib/SQLite3/Sqlite3.idr+3−3

compare with master

unifiedsplit

@@ -41,8 +41,8 @@ forM xs f = (sequence (map f xs))

41data DB a = MkDB (IO (Either String a))

42

43instance Functor DB where

44− fmap f (MkDB action) = MkDB (do res <- action

44+ map f (MkDB action) = MkDB (do res <- action

45− return (fmap f res))

45+ return (map f res))

46

47

48instance Applicative DB where

@@ -50,7 +50,7 @@ instance Applicative DB where

50 (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51 case f' of

52 Left err => return (Left err)

53− Right op => x >>= (return . fmap op))

53+ Right op => x >>= (return . map op))

54

55

56instance Monad DB where

contribs/lib/SimpleParser/SimpleParser.idr+6−6

@@ -24,7 +24,7 @@ parse : Parser a -> String -> Either String (a, String)

24parse (P p) inp = p inp

25

26instance Functor Parser where

27− fmap f p = P (\inp => case parse p inp of

27+ map f p = P (\inp => case parse p inp of

28 Left err => Left err

29 Right (v, rest) => Right ((f v), rest))

30

@@ -90,7 +90,7 @@ char : Char -> Parser Char

90char x = sat (== x)

91

92string : String -> Parser String

93−string s = fmap pack (traverse char (unpack s))

93+string s = map pack (traverse char (unpack s))

94

95many1 : Parser a -> Parser (List a)

96many : Parser a -> Parser (List a)

@@ -110,7 +110,7 @@ bool = parseTrue <|> parseFalse

110 pure False

111

112ident : Parser String

113−ident = fmap pack [| letter :: many1 alphanum |]

113+ident = map pack [| letter :: many1 alphanum |]

114

115nat : Parser Int

116nat = do xs <- many digit

@@ -148,7 +148,7 @@ symbol : String -> Parser String

148symbol xs = token (string xs)

149

150strToken : Parser String

151−strToken = fmap pack (token (many1 alphanum))

151+strToken = map pack (token (many1 alphanum))

152

153

154--------------------------------------------------------------------------------

@@ -160,12 +160,12 @@ factor : Parser Int

160term : Parser Int

161

162expr = do t <- term

163− fmap (t+) (symbol "+" $> expr) <|> pure t

163+ map (t+) (symbol "+" $> expr) <|> pure t

164

165factor = (symbol "(" $> expr <$ symbol ")") <|> natural

166

167term = do f <- factor

168− fmap (f*) (symbol "*" $> term) <|> pure f

168+ map (f*) (symbol "*" $> term) <|> pure f

169

170eval : String -> Maybe Int

171eval xs = case (parse expr xs) of

js/Runtime-browser.js+1−1

@@ -1,3 +1,3 @@

1−__IDRRT__.print = function(s) {

1+var __IDRRT__print = function(s) {

2 console.log(s);

3};

js/Runtime-common.js+16−20

@@ -1,36 +1,34 @@

1−var __IDRRT__ = {};

2−

3/** @constructor */

1/** @constructor */

4−__IDRRT__.Type = function(type) {

2+var __IDRRT__Type = function(type) {

5 this.type = type;

3 this.type = type;

6};

4};

7

5

8−__IDRRT__.Int = new __IDRRT__.Type('Int');

6+var __IDRRT__Int = new __IDRRT__Type('Int');

9−__IDRRT__.Char = new __IDRRT__.Type('Char');

7+var __IDRRT__Char = new __IDRRT__Type('Char');

10−__IDRRT__.String = new __IDRRT__.Type('String');

8+var __IDRRT__String = new __IDRRT__Type('String');

11−__IDRRT__.Integer = new __IDRRT__.Type('Integer');

9+var __IDRRT__Integer = new __IDRRT__Type('Integer');

12−__IDRRT__.Float = new __IDRRT__.Type('Float');

10+var __IDRRT__Float = new __IDRRT__Type('Float');

13−__IDRRT__.Ptr = new __IDRRT__.Type('Pointer');

11+var __IDRRT__Ptr = new __IDRRT__Type('Pointer');

14−__IDRRT__.Forgot = new __IDRRT__.Type('Forgot');

12+var __IDRRT__Forgot = new __IDRRT__Type('Forgot');

15

13

16

14

17/** @constructor */

15/** @constructor */

18−__IDRRT__.Tailcall = function(f) { this.f = f };

16+var __IDRRT__Tailcall = function(f) { this.f = f };

19−__IDRRT__.ffiWrap = function(fid) {

17+var __IDRRT__ffiWrap = function(fid) {

20 return function(arg) {

18 return function(arg) {

21− return __IDRRT__.tailcall(function(){

19+ return __IDRRT__tailcall(function(){

22− return __IDR__.APPLY0(fid, arg);

20+ return __IDR__APPLY0(fid, arg);

23 });

21 });

24 };

22 };

25};

23};

26

24

27/** @constructor */

25/** @constructor */

28−__IDRRT__.Con = function(i,vars) {

26+var __IDRRT__Con = function(i,vars) {

29 this.i = i;

27 this.i = i;

30 this.vars = vars;

28 this.vars = vars;

31};

29};

32

30

33−__IDRRT__.tailcall = function(f) {

31+var __IDRRT__tailcall = function(f) {

34 var __f = f;

32 var __f = f;

35 var ret;

33 var ret;

36 while (__f) {

34 while (__f) {

@@ -38,7 +36,7 @@ __IDRRT__.tailcall = function(f) {

38 __f = null;

36 __f = null;

39 ret = f();

37 ret = f();

40

38

41− if (ret instanceof __IDRRT__.Tailcall) {

39+ if (ret instanceof __IDRRT__Tailcall) {

42 __f = ret.f;

40 __f = ret.f;

43 } else {

41 } else {

44 return ret;

42 return ret;

@@ -50,7 +48,7 @@ __IDRRT__.tailcall = function(f) {

50 BigInteger Javascript code taken from:

48 BigInteger Javascript code taken from:

51 https://github.com/peterolson

49 https://github.com/peterolson

52*/

50*/

53−__IDRRT__.bigInt = (function () {

51+var __IDRRT__bigInt = (function () {

54 var base = 10000000, logBase = 7;

52 var base = 10000000, logBase = 7;

55 var sign = {

53 var sign = {

56 positive: false,

54 positive: false,

@@ -391,5 +389,3 @@ __IDRRT__.bigInt = (function () {

391 fnReturn.minusOne = MINUS_ONE;

389 fnReturn.minusOne = MINUS_ONE;

392 return fnReturn;

390 return fnReturn;

393})();

391})();

394−

395−var __IDR__ = {};

js/Runtime-node.js+1−1

@@ -1,4 +1,4 @@

1−__IDRRT__.print = (function() {

1+var __IDRRT__print = (function() {

2 var util = require('util');

3 return function(s) {

4 util.print(s);

lib/Builtins.idr+76

@@ -259,6 +259,82 @@ instance Num Float where

259 abs x = if x < (prim__toFloatBigInt 0) then -x else x

260 fromInteger = prim__toFloatBigInt

261

262+instance Num Bits8 where

263+ (+) = prim__addB8

264+ (-) = prim__subB8

265+ (*) = prim__mulB8

266+ abs = id

267+ fromInteger = prim__truncBigInt_B8

268+

269+instance Num Bits16 where

270+ (+) = prim__addB16

271+ (-) = prim__subB16

272+ (*) = prim__mulB16

273+ abs = id

274+ fromInteger = prim__truncBigInt_B16

275+

276+instance Num Bits32 where

277+ (+) = prim__addB32

278+ (-) = prim__subB32

279+ (*) = prim__mulB32

280+ abs = id

281+ fromInteger = prim__truncBigInt_B32

282+

283+instance Num Bits64 where

284+ (+) = prim__addB64

285+ (-) = prim__subB64

286+ (*) = prim__mulB64

287+ abs = id

288+ fromInteger = prim__truncBigInt_B64

289+

290+instance Eq Bits8 where

291+ x == y = intToBool (prim__eqB8 x y)

292+

293+instance Eq Bits16 where

294+ x == y = intToBool (prim__eqB16 x y)

295+

296+instance Eq Bits32 where

297+ x == y = intToBool (prim__eqB32 x y)

298+

299+instance Eq Bits64 where

300+ x == y = intToBool (prim__eqB64 x y)

301+

302+instance Ord Bits8 where

303+ (<) = boolOp prim__ltB8

304+ (>) = boolOp prim__gtB8

305+ (<=) = boolOp prim__lteB8

306+ (>=) = boolOp prim__gteB8

307+ compare l r = if l < r then LT

308+ else if l > r then GT

309+ else EQ

310+

311+instance Ord Bits16 where

312+ (<) = boolOp prim__ltB16

313+ (>) = boolOp prim__gtB16

314+ (<=) = boolOp prim__lteB16

315+ (>=) = boolOp prim__gteB16

316+ compare l r = if l < r then LT

317+ else if l > r then GT

318+ else EQ

319+

320+instance Ord Bits32 where

321+ (<) = boolOp prim__ltB32

322+ (>) = boolOp prim__gtB32

323+ (<=) = boolOp prim__lteB32

324+ (>=) = boolOp prim__gteB32

325+ compare l r = if l < r then LT

326+ else if l > r then GT

327+ else EQ

328+

329+instance Ord Bits64 where

330+ (<) = boolOp prim__ltB64

331+ (>) = boolOp prim__gtB64

332+ (<=) = boolOp prim__lteB64

333+ (>=) = boolOp prim__gteB64

334+ compare l r = if l < r then LT

335+ else if l > r then GT

336+ else EQ

337+

262partial

338partial

263div : Integer -> Integer -> Integer

339div : Integer -> Integer -> Integer

264div = prim__sdivBigInt

340div = prim__sdivBigInt

lib/Control/IOExcept.idr+1−1

@@ -8,7 +8,7 @@ data IOExcept : Type -> Type -> Type where

8 ioM : IO (Either err a) -> IOExcept err a

9

10instance Functor (IOExcept e) where

11− fmap f (ioM fn) = ioM (fmap (fmap f) fn)

11+ map f (ioM fn) = ioM (map (map f) fn)

12

13instance Applicative (IOExcept e) where

14 pure x = ioM (pure (pure x))

lib/Control/Monad/Identity.idr+1−1

@@ -8,7 +8,7 @@ public record Identity : Type -> Type where

8 Id : (runIdentity : a) -> Identity a

9

10instance Functor Identity where

11− fmap fn (Id a) = Id (fn a)

11+ map fn (Id a) = Id (fn a)

12

13instance Applicative Identity where

14 pure x = Id x

lib/Control/Monad/State.idr+1−1

@@ -15,7 +15,7 @@ record StateT : Type -> (Type -> Type) -> Type -> Type where

15 (runStateT : s -> m (a, s)) -> StateT s m a

16

17instance Functor f => Functor (StateT s f) where

18− fmap f (ST g) = ST (\st => fmap (mapFst f) (g st)) where

18+ map f (ST g) = ST (\st => map (mapFst f) (g st)) where

19 mapFst : (a -> x) -> (a, b) -> (x, b)

20 mapFst fn (a, b) = (fn a, b)

21

lib/Data/Morphisms.idr+1−1

@@ -23,7 +23,7 @@ applyEndo : Endomorphism a -> a -> a

23applyEndo (Endo f) a = f a

24

25instance Functor (Morphism r) where

26− fmap f (Mor a) = Mor (f . a)

26+ map f (Mor a) = Mor (f . a)

27

28instance Applicative (Morphism r) where

29 pure a = Mor $ const a

lib/Data/SortedMap.idr+5−5

@@ -226,10 +226,10 @@ toList Empty = []

226toList (M _ t) = treeToList t

227

228instance Functor (Tree n k) where

229− fmap f (Leaf k v) = Leaf k (f v)

229+ map f (Leaf k v) = Leaf k (f v)

230− fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)

230+ map f (Branch2 t1 k t2) = Branch2 (map f t1) k (map f t2)

231− fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)

231+ map f (Branch3 t1 k1 t2 k2 t3) = Branch3 (map f t1) k1 (map f t2) k2 (map f t3)

232

233instance Functor (SortedMap k) where

234− fmap _ Empty = Empty

234+ map _ Empty = Empty

235− fmap f (M n t) = M _ (fmap f t)

235+ map f (M n t) = M _ (map f t)

lib/IO.idr+29−1

@@ -21,7 +21,7 @@ io_return x = prim__IO x

21run__IO : IO () -> IO ()

22run__IO v = io_bind v (\v' => io_return v')

23

24−data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64

24+data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2

25data FTy = FIntT IntTy

26 | FFunction FTy FTy

27 | FFloat

@@ -45,6 +45,30 @@ FShort = FIntT IT16

45FLong : FTy

46FLong = FIntT IT64

47

48+FBits8 : FTy

49+FBits8 = FIntT IT8

50+

51+FBits16 : FTy

52+FBits16 = FIntT IT16

53+

54+FBits32 : FTy

55+FBits32 = FIntT IT32

56+

57+FBits64 : FTy

58+FBits64 = FIntT IT64

59+

60+FBits8x16 : FTy

61+FBits8x16 = FIntT IT8x16

62+

63+FBits16x8 : FTy

64+FBits16x8 = FIntT IT16x8

65+

66+FBits32x4 : FTy

67+FBits32x4 = FIntT IT32x4

68+

69+FBits64x2 : FTy

70+FBits64x2 = FIntT IT64x2

71+

48interpFTy : FTy -> Type

72interpFTy : FTy -> Type

49interpFTy (FIntT ITNative) = Int

73interpFTy (FIntT ITNative) = Int

50interpFTy (FIntT ITChar) = Char

74interpFTy (FIntT ITChar) = Char

@@ -56,6 +80,10 @@ interpFTy (FAny t) = t

56interpFTy FFloat = Float

80interpFTy FFloat = Float

57interpFTy FString = String

81interpFTy FString = String

58interpFTy FPtr = Ptr

82interpFTy FPtr = Ptr

83+interpFTy (FIntT IT8x16) = Bits8x16

84+interpFTy (FIntT IT16x8) = Bits16x8

85+interpFTy (FIntT IT32x4) = Bits32x4

86+interpFTy (FIntT IT64x2) = Bits64x2

59interpFTy FUnit = ()

87interpFTy FUnit = ()

60

88

61interpFTy (FFunction a b) = interpFTy a -> interpFTy b

89interpFTy (FFunction a b) = interpFTy a -> interpFTy b

lib/Language/Reflection.idr+9−9

@@ -88,15 +88,15 @@ data Binder a = Lam a

88

89

90instance Functor Binder where

91− fmap f (Lam x) = Lam (f x)

91+ map f (Lam x) = Lam (f x)

92− fmap f (Pi x) = Pi (f x)

92+ map f (Pi x) = Pi (f x)

93− fmap f (Let x y) = Let (f x) (f y)

93+ map f (Let x y) = Let (f x) (f y)

94− fmap f (NLet x y) = NLet (f x) (f y)

94+ map f (NLet x y) = NLet (f x) (f y)

95− fmap f (Hole x) = Hole (f x)

95+ map f (Hole x) = Hole (f x)

96− fmap f (GHole x) = GHole (f x)

96+ map f (GHole x) = GHole (f x)

97− fmap f (Guess x y) = Guess (f x) (f y)

97+ map f (Guess x y) = Guess (f x) (f y)

98− fmap f (PVar x) = PVar (f x)

98+ map f (PVar x) = PVar (f x)

99− fmap f (PVTy x) = PVTy (f x)

99+ map f (PVTy x) = PVTy (f x)

100

101total

102traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)

lib/Network/Cgi.idr+2−2

@@ -28,8 +28,8 @@ getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)

28getAction (MkCGI act) = act

29

30instance Functor CGI where

31− fmap f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

31+ map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

32− return (f a, i))

32+ return (f a, i))

33

34instance Applicative CGI where

35 pure v = MkCGI (\s => return (v, s))

lib/Prelude.idr+130−9

@@ -46,6 +46,118 @@ instance Show Bool where

46 show True = "True"

47 show False = "False"

48

49+instance Show Bits8 where

50+ show = prim__toStrB8

51+

52+instance Show Bits16 where

53+ show = prim__toStrB16

54+

55+instance Show Bits32 where

56+ show = prim__toStrB32

57+

58+instance Show Bits64 where

59+ show = prim__toStrB64

60+

61+%assert_total

62+viewB8x16 : Bits8x16 -> (Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8)

63+viewB8x16 x = ( prim__indexB8x16 x (prim__truncBigInt_B32 0)

64+ , prim__indexB8x16 x (prim__truncBigInt_B32 1)

65+ , prim__indexB8x16 x (prim__truncBigInt_B32 2)

66+ , prim__indexB8x16 x (prim__truncBigInt_B32 3)

67+ , prim__indexB8x16 x (prim__truncBigInt_B32 4)

68+ , prim__indexB8x16 x (prim__truncBigInt_B32 5)

69+ , prim__indexB8x16 x (prim__truncBigInt_B32 6)

70+ , prim__indexB8x16 x (prim__truncBigInt_B32 7)

71+ , prim__indexB8x16 x (prim__truncBigInt_B32 8)

72+ , prim__indexB8x16 x (prim__truncBigInt_B32 9)

73+ , prim__indexB8x16 x (prim__truncBigInt_B32 10)

74+ , prim__indexB8x16 x (prim__truncBigInt_B32 11)

75+ , prim__indexB8x16 x (prim__truncBigInt_B32 12)

76+ , prim__indexB8x16 x (prim__truncBigInt_B32 13)

77+ , prim__indexB8x16 x (prim__truncBigInt_B32 14)

78+ , prim__indexB8x16 x (prim__truncBigInt_B32 15)

79+ )

80+

81+instance Show Bits8x16 where

82+ show x =

83+ case viewB8x16 x of

84+ (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) =>

85+ "<" ++ prim__toStrB8 a

86+ ++ ", " ++ prim__toStrB8 b

87+ ++ ", " ++ prim__toStrB8 c

88+ ++ ", " ++ prim__toStrB8 d

89+ ++ ", " ++ prim__toStrB8 e

90+ ++ ", " ++ prim__toStrB8 f

91+ ++ ", " ++ prim__toStrB8 g

92+ ++ ", " ++ prim__toStrB8 h

93+ ++ ", " ++ prim__toStrB8 i

94+ ++ ", " ++ prim__toStrB8 j

95+ ++ ", " ++ prim__toStrB8 k

96+ ++ ", " ++ prim__toStrB8 l

97+ ++ ", " ++ prim__toStrB8 m

98+ ++ ", " ++ prim__toStrB8 n

99+ ++ ", " ++ prim__toStrB8 o

100+ ++ ", " ++ prim__toStrB8 p

101+ ++ ">"

102+

103+%assert_total

104+viewB16x8 : Bits16x8 -> (Bits16, Bits16, Bits16, Bits16, Bits16, Bits16, Bits16, Bits16)

105+viewB16x8 x = ( prim__indexB16x8 x (prim__truncBigInt_B32 0)

106+ , prim__indexB16x8 x (prim__truncBigInt_B32 1)

107+ , prim__indexB16x8 x (prim__truncBigInt_B32 2)

108+ , prim__indexB16x8 x (prim__truncBigInt_B32 3)

109+ , prim__indexB16x8 x (prim__truncBigInt_B32 4)

110+ , prim__indexB16x8 x (prim__truncBigInt_B32 5)

111+ , prim__indexB16x8 x (prim__truncBigInt_B32 6)

112+ , prim__indexB16x8 x (prim__truncBigInt_B32 7)

113+ )

114+

115+instance Show Bits16x8 where

116+ show x =

117+ case viewB16x8 x of

118+ (a, b, c, d, e, f, g, h) =>

119+ "<" ++ prim__toStrB16 a

120+ ++ ", " ++ prim__toStrB16 b

121+ ++ ", " ++ prim__toStrB16 c

122+ ++ ", " ++ prim__toStrB16 d

123+ ++ ", " ++ prim__toStrB16 e

124+ ++ ", " ++ prim__toStrB16 f

125+ ++ ", " ++ prim__toStrB16 g

126+ ++ ", " ++ prim__toStrB16 h

127+ ++ ">"

128+

129+%assert_total

130+viewB32x4 : Bits32x4 -> (Bits32, Bits32, Bits32, Bits32)

131+viewB32x4 x = ( prim__indexB32x4 x (prim__truncBigInt_B32 0)

132+ , prim__indexB32x4 x (prim__truncBigInt_B32 1)

133+ , prim__indexB32x4 x (prim__truncBigInt_B32 2)

134+ , prim__indexB32x4 x (prim__truncBigInt_B32 3)

135+ )

136+

137+instance Show Bits32x4 where

138+ show x =

139+ case viewB32x4 x of

140+ (a, b, c, d) =>

141+ "<" ++ prim__toStrB32 a

142+ ++ ", " ++ prim__toStrB32 b

143+ ++ ", " ++ prim__toStrB32 c

144+ ++ ", " ++ prim__toStrB32 d

145+ ++ ">"

146+

147+%assert_total

148+viewB64x2 : Bits64x2 -> (Bits64, Bits64)

149+viewB64x2 x = ( prim__indexB64x2 x (prim__truncBigInt_B32 0)

150+ , prim__indexB64x2 x (prim__truncBigInt_B32 1)

151+ )

152+

153+instance Show Bits64x2 where

154+ show x =

155+ case viewB64x2 x of

156+ (a, b) =>

157+ "<" ++ prim__toStrB64 a

158+ ++ ", " ++ prim__toStrB64 b

159+ ++ ">"

160+

49instance (Show a, Show b) => Show (a, b) where

161instance (Show a, Show b) => Show (a, b) where

50 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

162 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

51

163

@@ -69,18 +181,15 @@ instance Show a => Show (Maybe a) where

69---- Functor instances

181---- Functor instances

70

182

71instance Functor IO where

183instance Functor IO where

72− fmap f io = io_bind io (io_return . f)

184+ map f io = io_bind io (io_return . f)

73

185

74instance Functor Maybe where

186instance Functor Maybe where

75− fmap f (Just x) = Just (f x)

187+ map f (Just x) = Just (f x)

76− fmap f Nothing = Nothing

188+ map f Nothing = Nothing

77

189

78instance Functor (Either e) where

190instance Functor (Either e) where

79− fmap f (Left l) = Left l

191+ map f (Left l) = Left l

80− fmap f (Right r) = Right (f r)

192+ map f (Right r) = Right (f r)

81−

82−instance Functor List where

83− fmap = map

84

193

85---- Applicative instances

194---- Applicative instances

86

195

@@ -228,6 +337,18 @@ curry f a b = f (a, b)

228uncurry : (a -> b -> c) -> (a, b) -> c

337uncurry : (a -> b -> c) -> (a, b) -> c

229uncurry f (a, b) = f a b

338uncurry f (a, b) = f a b

230

339

340+uniformB8x16 : Bits8 -> Bits8x16

341+uniformB8x16 x = prim__mkB8x16 x x x x x x x x x x x x x x x x

342+

343+uniformB16x8 : Bits16 -> Bits16x8

344+uniformB16x8 x = prim__mkB16x8 x x x x x x x x

345+

346+uniformB32x4 : Bits32 -> Bits32x4

347+uniformB32x4 x = prim__mkB32x4 x x x x

348+

349+uniformB64x2 : Bits64 -> Bits64x2

350+uniformB64x2 x = prim__mkB64x2 x x

351+

231---- some basic io

352---- some basic io

232

353

233partial

354partial

@@ -252,7 +373,7 @@ putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)

252

373

253partial

374partial

254getChar : IO Char

375getChar : IO Char

255−getChar = fmap cast $ mkForeign (FFun "getchar" [] FInt)

376+getChar = map cast $ mkForeign (FFun "getchar" [] FInt)

256

377

257---- some basic file handling

378---- some basic file handling

258

379

lib/Prelude/Applicative.idr+3−3

@@ -13,11 +13,11 @@ class Functor f => Applicative (f : Type -> Type) where

13

14infixl 2 <$

15(<$) : Applicative f => f a -> f b -> f a

16−a <$ b = fmap const a <$> b

16+a <$ b = map const a <$> b

17

18infixl 2 $>

19($>) : Applicative f => f a -> f b -> f b

20−a $> b = fmap (const id) a <$> b

20+a $> b = map (const id) a <$> b

21

22infixl 3 <|>

23class Applicative f => Alternative (f : Type -> Type) where

@@ -32,7 +32,7 @@ when a f = if a then f else pure ()

32

33sequence : Applicative f => List (f a) -> f (List a)

34sequence [] = pure []

35−sequence (x :: xs) = fmap (::) x <$> sequence xs

35+sequence (x :: xs) = map (::) x <$> sequence xs

36

37sequence_ : Applicative f => List (f a) -> f ()

38sequence_ [] = pure ()

lib/Prelude/Functor.idr+1−1

@@ -1,4 +1,4 @@

1module Prelude.Functor

2

3class Functor (f : Type -> Type) where

4− fmap : (a -> b) -> f a -> f b

4+ map : (a -> b) -> f a -> f b

lib/Prelude/List.idr+5−4

@@ -3,6 +3,7 @@ module Prelude.List

3import Builtins

4

5import Prelude.Algebra

6+import Prelude.Functor

6import Prelude.Maybe

7import Prelude.Maybe

7import Prelude.Nat

8import Prelude.Nat

8

9

@@ -163,6 +164,10 @@ instance Monoid (List a) where

163-- instance VerifiedSemigroup (List a) where

164-- instance VerifiedSemigroup (List a) where

164-- semigroupOpIsAssociative = appendAssociative

165-- semigroupOpIsAssociative = appendAssociative

165

166

167+instance Functor List where

168+ map f [] = []

169+ map f (x::xs) = f x :: map f xs

170+

166--------------------------------------------------------------------------------

171--------------------------------------------------------------------------------

167-- Zips and unzips

172-- Zips and unzips

168--------------------------------------------------------------------------------

173--------------------------------------------------------------------------------

@@ -201,10 +206,6 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)

201-- Maps

206-- Maps

202--------------------------------------------------------------------------------

207--------------------------------------------------------------------------------

203

208

204−map : (a -> b) -> List a -> List b

205−map f [] = []

206−map f (x::xs) = f x :: map f xs

207−

208mapMaybe : (a -> Maybe b) -> List a -> List b

209mapMaybe : (a -> Maybe b) -> List a -> List b

209mapMaybe f [] = []

210mapMaybe f [] = []

210mapMaybe f (x::xs) =

211mapMaybe f (x::xs) =

lib/System/Concurrency/Process.idr+1−1

@@ -16,7 +16,7 @@ data Process : (msgType : Type) -> Type -> Type where

16 lift : IO a -> Process msg a

17

18instance Functor (Process msg) where

19− fmap f (lift a) = lift (fmap f a)

19+ map f (lift a) = lift (map f a)

20

21instance Applicative (Process msg) where

22 pure = lift . return

src/IRTS/CodegenJavaScript.hs+65−69

@@ -20,6 +20,7 @@ import System.Directory

20

21idrNamespace :: String

22idrNamespace = "__IDR__"

23+idrRTNamespace = "__IDRRT__"

23

24

24data JSTarget = Node | JavaScript deriving Eq

25data JSTarget = Node | JavaScript deriving Eq

25

26

@@ -41,7 +42,6 @@ codegenJavaScript target definitions filename outputType = do

41 writeFile filename ( header

42 writeFile filename ( header

42 ++ idrRuntime

43 ++ idrRuntime

43 ++ tgtRuntime

44 ++ tgtRuntime

44− ++ modules

45 ++ functions

46 ++ mainLoop)

47

@@ -56,19 +56,10 @@ codegenJavaScript target definitions filename outputType = do

56

57 mainLoop :: String

58 mainLoop = intercalate "\n" [ "\nfunction main() {"

59− , createTailcall "__IDR__.runMain0()"

59+ , createTailcall "__IDR__runMain0()"

60 , "}\n\nmain();\n"

61 ]

62

63− modules =

64− concatMap allocMod mods

65− where

66− allocMod m = intercalate "." m ++ " = {};\n"

67− sortMods a b = compare (length a) (length b)

68−

69− mods =

70− drop 1 $ sortBy sortMods $ nub $ concatMap (inits . fst) def

71−

72translateIdentifier :: String -> String

63translateIdentifier :: String -> String

73translateIdentifier =

64translateIdentifier =

74 replaceReserved . concatMap replaceBadChars

65 replaceReserved . concatMap replaceBadChars

@@ -127,10 +118,10 @@ translateIdentifier =

127 , "yield"

118 , "yield"

128 ]

119 ]

129

120

130−translateNamespace :: Name -> [String]

121+translateNamespace :: Name -> String

131−translateNamespace (UN _) = [idrNamespace]

122+translateNamespace (UN _) = idrNamespace

132−translateNamespace (NS _ ns) = idrNamespace : map translateIdentifier ns

123+translateNamespace (NS _ ns) = idrNamespace ++ concatMap translateIdentifier ns

133−translateNamespace (MN _ _) = [idrNamespace]

124+translateNamespace (MN _ _) = idrNamespace

134

125

135translateName :: Name -> String

126translateName :: Name -> String

136translateName (UN name) = translateIdentifier name

127translateName (UN name) = translateIdentifier name

@@ -139,16 +130,17 @@ translateName (MN i name) = translateIdentifier name ++ show i

139

130

140translateConstant :: Const -> String

131translateConstant :: Const -> String

141translateConstant (I i) = show i

132translateConstant (I i) = show i

142−translateConstant (BI i) = "__IDRRT__.bigInt('" ++ show i ++ "')"

133+translateConstant (BI i) = idrRTNamespace ++ "bigInt('" ++ show i ++ "')"

143translateConstant (Fl f) = show f

134translateConstant (Fl f) = show f

144translateConstant (Ch c) = show c

135translateConstant (Ch c) = show c

145translateConstant (Str s) = show s

136translateConstant (Str s) = show s

146−translateConstant (AType (ATInt ITNative)) = "__IDRRT__.Int"

137+translateConstant (AType (ATInt ITNative)) = idrRTNamespace ++ "Int"

147−translateConstant StrType = "__IDRRT__.String"

138+translateConstant StrType = idrRTNamespace ++ "String"

148−translateConstant (AType (ATInt ITBig)) = "__IDRRT__.Integer"

139+translateConstant (AType (ATInt ITBig)) = idrRTNamespace ++ "Integer"

149−translateConstant (AType ATFloat) = "__IDRRT__.Float"

140+translateConstant (AType ATFloat) = idrRTNamespace ++ "Float"

150−translateConstant PtrType = "__IDRRT__.Ptr"

141+translateConstant (AType (ATInt ITChar)) = idrRTNamespace ++ "Char"

142+translateConstant PtrType = idrRTNamespace ++ "Ptr"

151−translateConstant Forgot = "__IDRRT__.Forgot"

143+translateConstant Forgot = idrRTNamespace ++ "Forgot"

152translateConstant c =

144translateConstant c =

153 "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()"

145 "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()"

154

146

@@ -157,9 +149,9 @@ translateParameterlist =

157 where translateParameter (MN i name) = translateIdentifier name ++ show i

149 where translateParameter (MN i name) = translateIdentifier name ++ show i

158 translateParameter (UN name) = translateIdentifier name

150 translateParameter (UN name) = translateIdentifier name

159

151

160−translateDeclaration :: ([String], SDecl) -> String

152+translateDeclaration :: (String, SDecl) -> String

161translateDeclaration (path, SFun name params stackSize body) =

153translateDeclaration (path, SFun name params stackSize body) =

162− intercalate "." (path ++ [translateName name])

154+ "var " ++ path ++ translateName name

163 ++ " = function("

155 ++ " = function("

164 ++ intercalate "," p

156 ++ intercalate "," p

165 ++ "){\n"

157 ++ "){\n"

@@ -205,44 +197,16 @@ translateExpression (SApp False name vars) =

205 createTailcall $ translateFunctionCall name vars

197 createTailcall $ translateFunctionCall name vars

206

198

207translateExpression (SApp True name vars) =

199translateExpression (SApp True name vars) =

208− "new __IDRRT__.Tailcall("

200+ "new " ++ idrRTNamespace ++ "Tailcall("

209 ++ "function(){\n"

201 ++ "function(){\n"

210 ++ "return " ++ translateFunctionCall name vars

202 ++ "return " ++ translateFunctionCall name vars

211 ++ ";\n})"

203 ++ ";\n})"

212

204

213translateExpression (SOp op vars)

205translateExpression (SOp op vars)

214− | (LPlus _) <- op

206+ | LNoOp <- op = translateVariableName (last vars)

215− , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

207+

216− | (LMinus _) <- op

208+ | (LZExt _ ITBig) <- op =

217− , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

209+ idrRTNamespace ++ "bigInt(" ++ translateVariableName (last vars) ++ ")"

218− | (LTimes _) <- op

219− , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

220− | (LSDiv _) <- op

221− , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

222− | (LSRem _) <- op

223− , (lhs:rhs:_) <- vars = translateBinaryOp "%" lhs rhs

224− | (LEq _) <- op

225− , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

226− | (LLt _) <- op

227− , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

228− | (LLe _) <- op

229− , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

230− | (LGt _) <- op

231− , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

232− | (LGe _) <- op

233− , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

234− | (LAnd _) <- op

235− , (lhs:rhs:_) <- vars = translateBinaryOp "&" lhs rhs

236− | (LOr _) <- op

237− , (lhs:rhs:_) <- vars = translateBinaryOp "|" lhs rhs

238− | (LXOr _) <- op

239− , (lhs:rhs:_) <- vars = translateBinaryOp "^" lhs rhs

240− | (LSHL _) <- op

241− , (lhs:rhs:_) <- vars = translateBinaryOp "<<" rhs lhs

242− | (LASHR _) <- op

243− , (lhs:rhs:_) <- vars = translateBinaryOp ">>" rhs lhs

244− | (LCompl _) <- op

245− , (arg:_) <- vars = '~' : translateVariableName arg

246

210

247 | (LPlus (ATInt ITBig)) <- op

211 | (LPlus (ATInt ITBig)) <- op

248 , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

212 , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

@@ -284,6 +248,39 @@ translateExpression (SOp op vars)

284 | (LGe ATFloat) <- op

248 | (LGe ATFloat) <- op

285 , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

249 , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

286

250

251+ | (LPlus _) <- op

252+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

253+ | (LMinus _) <- op

254+ , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

255+ | (LTimes _) <- op

256+ , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

257+ | (LSDiv _) <- op

258+ , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

259+ | (LSRem _) <- op

260+ , (lhs:rhs:_) <- vars = translateBinaryOp "%" lhs rhs

261+ | (LEq _) <- op

262+ , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

263+ | (LLt _) <- op

264+ , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

265+ | (LLe _) <- op

266+ , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

267+ | (LGt _) <- op

268+ , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

269+ | (LGe _) <- op

270+ , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

271+ | (LAnd _) <- op

272+ , (lhs:rhs:_) <- vars = translateBinaryOp "&" lhs rhs

273+ | (LOr _) <- op

274+ , (lhs:rhs:_) <- vars = translateBinaryOp "|" lhs rhs

275+ | (LXOr _) <- op

276+ , (lhs:rhs:_) <- vars = translateBinaryOp "^" lhs rhs

277+ | (LSHL _) <- op

278+ , (lhs:rhs:_) <- vars = translateBinaryOp "<<" rhs lhs

279+ | (LASHR _) <- op

280+ , (lhs:rhs:_) <- vars = translateBinaryOp ">>" rhs lhs

281+ | (LCompl _) <- op

282+ , (arg:_) <- vars = '~' : translateVariableName arg

283+

287 | LStrConcat <- op

284 | LStrConcat <- op

288 , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

285 , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

289 | LStrEq <- op

286 | LStrEq <- op

@@ -298,13 +295,13 @@ translateExpression (SOp op vars)

298 | (LIntStr ITNative) <- op

295 | (LIntStr ITNative) <- op

299 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

296 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

300 | (LSExt ITNative ITBig) <- op

297 | (LSExt ITNative ITBig) <- op

301− , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

298+ , (arg:_) <- vars = idrRTNamespace ++ "bigInt(" ++ translateVariableName arg ++ ")"

302 | (LTrunc ITBig ITNative) <- op

299 | (LTrunc ITBig ITNative) <- op

303 , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"

300 , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"

304 | (LIntStr ITBig) <- op

301 | (LIntStr ITBig) <- op

305 , (arg:_) <- vars = translateVariableName arg ++ ".toString()"

302 , (arg:_) <- vars = translateVariableName arg ++ ".toString()"

306 | (LStrInt ITBig) <- op

303 | (LStrInt ITBig) <- op

307− , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

304+ , (arg:_) <- vars = idrRTNamespace ++ "bigInt(" ++ translateVariableName arg ++ ")"

308 | LFloatStr <- op

305 | LFloatStr <- op

309 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

306 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

310 | LStrFloat <- op

307 | LStrFloat <- op

@@ -367,7 +364,7 @@ translateExpression (SError msg) =

367 "(function(){throw \'" ++ msg ++ "\';})()"

364 "(function(){throw \'" ++ msg ++ "\';})()"

368

365

369translateExpression (SForeign _ _ "putStr" [(FString, var)]) =

366translateExpression (SForeign _ _ "putStr" [(FString, var)]) =

370− "__IDRRT__.print(" ++ translateVariableName var ++ ")"

367+ idrRTNamespace ++ "print(" ++ translateVariableName var ++ ")"

371

368

372translateExpression (SForeign _ _ fun args)

369translateExpression (SForeign _ _ fun args)

373 | "[]=" `isSuffixOf` fun

370 | "[]=" `isSuffixOf` fun

@@ -423,8 +420,8 @@ translateExpression (SForeign _ _ fun args)

423 '(' : intercalate "," (map generateWrapper as) ++ ")"

420 '(' : intercalate "," (map generateWrapper as) ++ ")"

424

421

425 generateWrapper (ffunc, name)

422 generateWrapper (ffunc, name)

426− | FFunction <- ffunc = "__IDRRT__.ffiWrap(" ++ translateVariableName name ++ ")"

423+ | FFunction <- ffunc = idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"

427− | FFunctionIO <- ffunc = "__IDRRT__.ffiWrap(" ++ translateVariableName name ++ ")"

424+ | FFunctionIO <- ffunc = idrRTNamespace ++ "ffiWrap(" ++ translateVariableName name ++ ")"

428

425

429 generateWrapper (_, name) =

426 generateWrapper (_, name) =

430 translateVariableName name

427 translateVariableName name

@@ -444,7 +441,7 @@ translateExpression (SCase var cases) =

444 ++ ")"

441 ++ ")"

445

442

446translateExpression (SCon i name vars) =

443translateExpression (SCon i name vars) =

447− concat [ "new __IDRRT__.Con("

444+ concat [ "new " ++ idrRTNamespace ++ "Con("

448 , show i

445 , show i

449 , ",["

446 , ",["

450 , intercalate "," $ map translateVariableName vars

447 , intercalate "," $ map translateVariableName vars

@@ -480,7 +477,7 @@ translateCase var (SConstCase ty e)

480 matchHelper tyName = translateTypeMatch var tyName e

477 matchHelper tyName = translateTypeMatch var tyName e

481

478

482translateCase var (SConstCase cst@(BI _) e) =

479translateCase var (SConstCase cst@(BI _) e) =

483− let cond = "__IDRRT__.bigInt(" ++ var ++ ").equals(" ++ translateConstant cst ++ ")" in

480+ let cond = idrRTNamespace ++ "bigInt(" ++ var ++ ").equals(" ++ translateConstant cst ++ ")" in

484 createIfBlock cond (translateExpression e)

481 createIfBlock cond (translateExpression e)

485

482

486translateCase var (SConstCase cst e) =

483translateCase var (SConstCase cst e) =

@@ -488,7 +485,7 @@ translateCase var (SConstCase cst e) =

488 createIfBlock cond (translateExpression e)

485 createIfBlock cond (translateExpression e)

489

486

490translateCase var (SConCase a i name vars e) =

487translateCase var (SConCase a i name vars e) =

491− let isCon = var ++ " instanceof __IDRRT__.Con"

488+ let isCon = var ++ " instanceof " ++ idrRTNamespace ++ "Con"

492 isI = show i ++ " == " ++ var ++ ".i"

489 isI = show i ++ " == " ++ var ++ ".i"

493 params = intercalate "," $ map (("__var_" ++) . show) [a..(a+length vars)]

490 params = intercalate "," $ map (("__var_" ++) . show) [a..(a+length vars)]

494 args = ".apply(this," ++ var ++ ".vars)"

491 args = ".apply(this," ++ var ++ ".vars)"

@@ -503,7 +500,7 @@ translateTypeMatch :: String -> String -> SExp -> String

503translateTypeMatch var ty exp =

500translateTypeMatch var ty exp =

504 let e = translateExpression exp in

501 let e = translateExpression exp in

505 createIfBlock (var

502 createIfBlock (var

506− ++ " instanceof __IDRRT__.Type && "

503+ ++ " instanceof " ++ idrRTNamespace ++ "Type && "

507 ++ var ++ ".type == '"++ ty ++"'") e

504 ++ var ++ ".type == '"++ ty ++"'") e

508

505

509

506

@@ -513,11 +510,10 @@ createIfBlock cond e =

513 ++ ";\n}"

510 ++ ";\n}"

514

511

515createTailcall call =

512createTailcall call =

516− "__IDRRT__.tailcall(function(){return " ++ call ++ "})"

513+ idrRTNamespace ++ "tailcall(function(){return " ++ call ++ "})"

517

514

518translateFunctionCall name vars =

515translateFunctionCall name vars =

519− concat (intersperse "." $ translateNamespace name)

516+ translateNamespace name

520− ++ "."

521 ++ translateName name

517 ++ translateName name

522 ++ "("

518 ++ "("

523 ++ intercalate "," (map translateVariableName vars)

519 ++ intercalate "," (map translateVariableName vars)

src/IRTS/CodegenLLVM.hs+5

@@ -921,6 +921,11 @@ cgOp (LUpdateVec ety c) [v,i,e] = do

921 nv' <- inst $ InsertElement nv ne ni []

922 box fty nv'

923

924+cgOp (LBitCast from to) [x] = do

925+ nx <- unbox (FArith from) x

926+ nx' <- inst $ BitCast nx (ftyToTy (FArith to)) []

927+ box (FArith to) nx'

928+

924cgOp LStrEq [x,y] = do

929cgOp LStrEq [x,y] = do

925 x' <- unbox FString x

930 x' <- unbox FString x

926 y' <- unbox FString y

931 y' <- unbox FString y

src/IRTS/Compiler.hs+8

@@ -309,11 +309,19 @@ mkIty "FChar" = mkIntIty "ITChar"

309mkIty "FByte" = mkIntIty "IT8"

310mkIty "FShort" = mkIntIty "IT16"

311mkIty "FLong" = mkIntIty "IT64"

312+mkIty "FBits8" = mkIntIty "IT8"

313+mkIty "FBits16" = mkIntIty "IT16"

314+mkIty "FBits32" = mkIntIty "IT32"

315+mkIty "FBits64" = mkIntIty "IT64"

312mkIty "FString" = FString

316mkIty "FString" = FString

313mkIty "FPtr" = FPtr

317mkIty "FPtr" = FPtr

314mkIty "FUnit" = FUnit

318mkIty "FUnit" = FUnit

315mkIty "FFunction" = FFunction

319mkIty "FFunction" = FFunction

316mkIty "FFunctionIO" = FFunctionIO

320mkIty "FFunctionIO" = FFunctionIO

321+mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

322+mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

323+mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

324+mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

317mkIty x = error $ "Unknown type " ++ x

325mkIty x = error $ "Unknown type " ++ x

318

326

319mkIntIty "ITNative" = FArith (ATInt ITNative)

327mkIntIty "ITNative" = FArith (ATInt ITNative)

src/IRTS/Lang.hs+1

@@ -38,6 +38,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

38 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

39 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

40 | LPrintNum | LPrintStr | LReadStr

41+ | LBitCast ArithTy ArithTy -- Only for values of equal width

41

42

43 | LFSqrt | LFFloor | LFCeil

44 | LFSqrt | LFFloor | LFCeil

src/Idris/Primitives.hs+98−11

@@ -12,6 +12,7 @@ import Data.Bits

12import Data.Word

13import Data.Int

14import Data.Char

15+import Data.Vector.Unboxed (Vector)

15import qualified Data.Vector.Unboxed as V

16import qualified Data.Vector.Unboxed as V

16

17

17data Prim = Prim { p_name :: Name,

18data Prim = Prim { p_name :: Name,

@@ -169,7 +170,11 @@ primitives =

169 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

170 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

170 (0, LStdIn) partial

171 (0, LStdIn) partial

171 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

172 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

173+ ++ concatMap vecOps vecTypes

174+ ++ vecBitcasts vecTypes

175+

176+vecTypes :: [IntTy]

172− ++ concatMap vecOps [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]

177+vecTypes = [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]

173

178

174intOps :: IntTy -> [Prim]

179intOps :: IntTy -> [Prim]

175intOps ity = intCmps ity ++ intArith ity ++ intConv ity

180intOps ity = intCmps ity ++ intArith ity ++ intConv ity

@@ -236,6 +241,81 @@ vecOps ity@(ITVec elem count) =

236 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces

241 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces

237 ] ++ intArith ity ++ vecCmps ity

242 ] ++ intArith ity ++ vecCmps ity

238

243

244+bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim

245+bitcastPrim from to impl prim =

246+ Prim (UN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)

247+ (1, prim) total

248+

249+vecBitcasts :: [IntTy] -> [Prim]

250+vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)

251+ | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]

252+

253+mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b

254+mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))

255+

256+mapDouble :: (V.Unbox a, V.Unbox b) => (Bool -> a -> b) -> Vector a -> Vector b

257+mapDouble f xs = V.generate (V.length xs * 2) (\i -> f (i `rem` 2 == 0) (xs V.! (i `div` 2)))

258+

259+concatWord8 :: (Word8, Word8) -> Word16

260+concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)

261+

262+concatWord16 :: (Word16, Word16) -> Word32

263+concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)

264+

265+concatWord32 :: (Word32, Word32) -> Word64

266+concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)

267+

268+truncWord16 :: Bool -> Word16 -> Word8

269+truncWord16 True x = fromIntegral (x `shiftR` 8)

270+truncWord16 False x = fromIntegral x

271+

272+truncWord32 :: Bool -> Word32 -> Word16

273+truncWord32 True x = fromIntegral (x `shiftR` 16)

274+truncWord32 False x = fromIntegral x

275+

276+truncWord64 :: Bool -> Word64 -> Word32

277+truncWord64 True x = fromIntegral (x `shiftR` 32)

278+truncWord64 False x = fromIntegral x

279+

280+bitcastVec :: ArithTy -> [Const] -> Maybe Const

281+bitcastVec (ATInt (ITVec IT8 n)) [x@(B8V v)]

282+ | V.length v == n = Just x

283+bitcastVec (ATInt (ITVec IT16 n)) [B8V v]

284+ | V.length v == n*2 = Just . B16V . mapHalf concatWord8 $ v

285+bitcastVec (ATInt (ITVec IT32 n)) [B8V v]

286+ | V.length v == n*4 = Just . B32V . mapHalf concatWord16 . mapHalf concatWord8 $ v

287+bitcastVec (ATInt (ITVec IT64 n)) [B8V v]

288+ | V.length v == n*8 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 . mapHalf concatWord8 $ v

289+

290+bitcastVec (ATInt (ITVec IT8 n)) [B16V v]

291+ | V.length v * 2 == n = Just . B8V . mapDouble truncWord16 $ v

292+bitcastVec (ATInt (ITVec IT16 n)) [x@(B16V v)]

293+ | V.length v == n = Just x

294+bitcastVec (ATInt (ITVec IT32 n)) [B16V v]

295+ | V.length v == n*2 = Just . B32V . mapHalf concatWord16 $ v

296+bitcastVec (ATInt (ITVec IT64 n)) [B16V v]

297+ | V.length v == n*4 = Just . B64V . mapHalf concatWord32 . mapHalf concatWord16 $ v

298+

299+bitcastVec (ATInt (ITVec IT8 n)) [B32V v]

300+ | V.length v * 4 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 $ v

301+bitcastVec (ATInt (ITVec IT16 n)) [B32V v]

302+ | V.length v * 2 == n = Just . B16V . mapDouble truncWord32 $ v

303+bitcastVec (ATInt (ITVec IT32 n)) [x@(B32V v)]

304+ | V.length v == n = Just x

305+bitcastVec (ATInt (ITVec IT64 n)) [B32V v]

306+ | V.length v == n*2 = Just . B64V . mapHalf concatWord32 $ v

307+

308+bitcastVec (ATInt (ITVec IT8 n)) [B64V v]

309+ | V.length v * 8 == n = Just . B8V . mapDouble truncWord16 . mapDouble truncWord32 . mapDouble truncWord64 $ v

310+bitcastVec (ATInt (ITVec IT16 n)) [B64V v]

311+ | V.length v * 4 == n = Just . B16V . mapDouble truncWord32 . mapDouble truncWord64 $ v

312+bitcastVec (ATInt (ITVec IT32 n)) [B64V v]

313+ | V.length v == n*2 = Just . B32V . mapDouble truncWord64 $ v

314+bitcastVec (ATInt (ITVec IT64 n)) [x@(B64V v)]

315+ | V.length v == n = Just x

316+

317+bitcastVec _ _ = Nothing

318+

239mkVecCon :: NativeTy -> Int -> [Const] -> Maybe Const

319mkVecCon :: NativeTy -> Int -> [Const] -> Maybe Const

240mkVecCon ity count args

320mkVecCon ity count args

241 | length ints == count = Just (mkVec ity count ints)

321 | length ints == count = Just (mkVec ity count ints)

@@ -264,6 +344,12 @@ mkVecUpdate ity count [vec, B32 i, newElem] = updateVec vec newElem

264 updateVec (B16V v) (B16 e) = Just . B16V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

344 updateVec (B16V v) (B16 e) = Just . B16V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

265 updateVec (B32V v) (B32 e) = Just . B32V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

345 updateVec (B32V v) (B32 e) = Just . B32V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

266 updateVec (B64V v) (B64 e) = Just . B64V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

346 updateVec (B64V v) (B64 e) = Just . B64V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

347+ updateVec _ _ = Nothing

348+mkVecUpdate _ _ _ = Nothing

349+

350+aTyName :: ArithTy -> String

351+aTyName (ATInt t) = intTyName t

352+aTyName ATFloat = "Float"

267

353

268intTyName :: IntTy -> String

354intTyName :: IntTy -> String

269intTyName ITNative = "Int"

355intTyName ITNative = "Int"

@@ -448,20 +534,22 @@ toInt ITNative x = I (fromIntegral x)

448toInt ITChar x = Ch (chr $ fromIntegral x)

534toInt ITChar x = Ch (chr $ fromIntegral x)

449

535

450intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const

536intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const

451−intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x

537+intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x

452intToInt (ITFixed IT16) out [B16 x] = Just $ toInt out x

538intToInt (ITFixed IT16) out [B16 x] = Just $ toInt out x

453intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x

539intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x

454intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x

540intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x

455−intToInt ITBig out [BI x] = Just $ toInt out x

541+intToInt ITBig out [BI x] = Just $ toInt out x

456−intToInt ITNative out [I x] = Just $ toInt out x

542+intToInt ITNative out [I x] = Just $ toInt out x

457−intToInt ITChar out [Ch x] = Just $ toInt out (ord x)

543+intToInt ITChar out [Ch x] = Just $ toInt out (ord x)

458intToInt _ _ _ = Nothing

544intToInt _ _ _ = Nothing

459

545

460zext :: IntTy -> IntTy -> [Const] -> Maybe Const

546zext :: IntTy -> IntTy -> [Const] -> Maybe Const

461zext from ITBig val = intToInt from ITBig val

547zext from ITBig val = intToInt from ITBig val

462zext ITBig _ _ = Nothing

548zext ITBig _ _ = Nothing

463−zext from to val

549+zext f@(ITFixed from) t@(ITFixed to) val

464− | intTyWidth from < intTyWidth to = intToInt from to val

550+ | nativeTyWidth from < nativeTyWidth to = intToInt f t val

551+zext ITNative to [I x] = Just $ toInt to (fromIntegral x :: Word)

552+zext from ITNative val = intToInt from ITNative val

465zext _ _ _ = Nothing

553zext _ _ _ = Nothing

466

554

467sext :: IntTy -> IntTy -> [Const] -> Maybe Const

555sext :: IntTy -> IntTy -> [Const] -> Maybe Const

@@ -475,7 +563,9 @@ sext from to val = intToInt from to val

475trunc :: IntTy -> IntTy -> [Const] -> Maybe Const

563trunc :: IntTy -> IntTy -> [Const] -> Maybe Const

476trunc ITBig to val = intToInt ITBig to val

564trunc ITBig to val = intToInt ITBig to val

477trunc _ ITBig _ = Nothing

565trunc _ ITBig _ = Nothing

478−trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

566+trunc f@(ITFixed from) t@(ITFixed to) val | nativeTyWidth from > nativeTyWidth to = intToInt f t val

567+trunc ITNative to [I x] = Just $ toInt to x

568+trunc from ITNative val = intToInt from ITNative val

479trunc _ _ _ = Nothing

569trunc _ _ _ = Nothing

480

570

481intToStr :: [Const] -> Maybe Const

571intToStr :: [Const] -> Maybe Const

@@ -553,6 +643,3 @@ p_strRev _ = Nothing

553

643

554p_cantreduce :: a -> Maybe b

644p_cantreduce :: a -> Maybe b

555p_cantreduce _ = Nothing

645p_cantreduce _ = Nothing

556−

557−

558−

test/Makefile−1

@@ -9,7 +9,6 @@ test_js:

9 @perl ./runtest.pl reg002 --codegen node

10 @perl ./runtest.pl reg003 --codegen node

11 @perl ./runtest.pl reg004 --codegen node

12− @perl ./runtest.pl reg004 --codegen node

13 @perl ./runtest.pl reg005 --codegen node

12 @perl ./runtest.pl reg005 --codegen node

14 @perl ./runtest.pl reg006 --codegen node

13 @perl ./runtest.pl reg006 --codegen node

15 @perl ./runtest.pl reg007 --codegen node

14 @perl ./runtest.pl reg007 --codegen node

test/reg001/reg001.idr+1−1

@@ -2,7 +2,7 @@ apply : (a -> b) -> a -> b

2apply f x = f x

3

4class Functor f => VerifiedFunctor (f : Type -> Type) where

5− identity : (fa : f a) -> fmap id fa = fa

5+ identity : (fa : f a) -> map id fa = fa

6

7data Imp : Type where

8 MkImp : {any : Type} -> any -> Imp

test/test007/test007.idr+1−1

@@ -14,7 +14,7 @@ fetch x = MkEval (\e => fetchVal e) where

14 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

15

16instance Functor Eval where

17− fmap f (MkEval g) = MkEval (\e => fmap f (g e))

17+ map f (MkEval g) = MkEval (\e => map f (g e))

18

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

tutorial/examples/idiom.idr+1−1