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

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit86b4541f762f96544dac67fb059f83595515609b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 16 Jul 2013, 15:12 (13 years ago) parent293c8a2 7105d79

28 files changed+472−154

compare with master

unifiedsplit

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

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

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

4242

4343instance Functor DB where

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

45− return (fmap f res))

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

45+ return (map f res))

4646

4747

4848instance Applicative DB where

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

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

5151 case f' of

5252 Left err => return (Left err)

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

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

5454

5555

5656instance Monad DB where

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

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

2424parse (P p) inp = p inp

2525

2626instance 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

2828 Left err => Left err

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

3030

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

9090char x = sat (== x)

9191

9292string : String -> Parser String

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

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

9494

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

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

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

110110 pure False

111111

112112ident : Parser String

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

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

114114

115115nat : Parser Int

116116nat = do xs <- many digit

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

148148symbol xs = token (string xs)

149149

150150strToken : Parser String

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

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

152152

153153

154154--------------------------------------------------------------------------------

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

160160term : Parser Int

161161

162162expr = do t <- term

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

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

164164

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

166166

167167term = do f <- factor

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

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

169169

170170eval : String -> Maybe Int

171171eval 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) {

22 console.log(s);

33};

js/Runtime-common.js+16−20

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

1−var __IDRRT__ = {};

2−

31/** @constructor */

4−__IDRRT__.Type = function(type) {

2+var __IDRRT__Type = function(type) {

53 this.type = type;

64};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1513

1614

1715/** @constructor */

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

19−__IDRRT__.ffiWrap = function(fid) {

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

17+var __IDRRT__ffiWrap = function(fid) {

2018 return function(arg) {

21− return __IDRRT__.tailcall(function(){

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

19+ return __IDRRT__tailcall(function(){

20+ return __IDR__APPLY0(fid, arg);

2321 });

2422 };

2523};

2624

2725/** @constructor */

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

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

2927 this.i = i;

3028 this.vars = vars;

3129};

3230

33−__IDRRT__.tailcall = function(f) {

31+var __IDRRT__tailcall = function(f) {

3432 var __f = f;

3533 var ret;

3634 while (__f) {

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

3836 __f = null;

3937 ret = f();

4038

41− if (ret instanceof __IDRRT__.Tailcall) {

39+ if (ret instanceof __IDRRT__Tailcall) {

4240 __f = ret.f;

4341 } else {

4442 return ret;

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

5048 BigInteger Javascript code taken from:

5149 https://github.com/peterolson

5250*/

53−__IDRRT__.bigInt = (function () {

51+var __IDRRT__bigInt = (function () {

5452 var base = 10000000, logBase = 7;

5553 var sign = {

5654 positive: false,

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

391389 fnReturn.minusOne = MINUS_ONE;

392390 return fnReturn;

393391})();

394−

395−var __IDR__ = {};

js/Runtime-node.js+1−1

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

1−__IDRRT__.print = (function() {

1+var __IDRRT__print = (function() {

22 var util = require('util');

33 return function(s) {

44 util.print(s);

lib/Builtins.idr+76

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

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

260260 fromInteger = prim__toFloatBigInt

261261

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+

262338partial

263339div : Integer -> Integer -> Integer

264340div = prim__sdivBigInt

lib/Control/IOExcept.idr+1−1

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

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

1010instance Functor (IOExcept e) where

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

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

1212

1313instance Applicative (IOExcept e) where

1414 pure x = ioM (pure (pure x))

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

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

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

1010instance Functor Identity where

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

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

1212

1313instance Applicative Identity where

1414 pure x = Id x

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

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

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

1616

1717instance 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

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

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

2121

lib/Data/Morphisms.idr+1−1

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

2323applyEndo (Endo f) a = f a

2424

2525instance Functor (Morphism r) where

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

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

2727

2828instance Applicative (Morphism r) where

2929 pure a = Mor $ const a

lib/Data/SortedMap.idr+5−5

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

226226toList (M _ t) = treeToList t

227227

228228instance Functor (Tree n k) where

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

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

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

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

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

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

232232

233233instance Functor (SortedMap k) where

234− fmap _ Empty = Empty

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

234+ map _ Empty = Empty

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

2121run__IO : IO () -> IO ()

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

2323

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

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

2525data FTy = FIntT IntTy

2626 | FFunction FTy FTy

2727 | FFloat

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

4545FLong : FTy

4646FLong = FIntT IT64

4747

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+

4872interpFTy : FTy -> Type

4973interpFTy (FIntT ITNative) = Int

5074interpFTy (FIntT ITChar) = Char

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

5680interpFTy FFloat = Float

5781interpFTy FString = String

5882interpFTy FPtr = Ptr

83+interpFTy (FIntT IT8x16) = Bits8x16

84+interpFTy (FIntT IT16x8) = Bits16x8

85+interpFTy (FIntT IT32x4) = Bits32x4

86+interpFTy (FIntT IT64x2) = Bits64x2

5987interpFTy FUnit = ()

6088

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

lib/Language/Reflection.idr+9−9

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

8888

8989

9090instance Functor Binder where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

100100

101101total

102102traverse : (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)

2828getAction (MkCGI act) = act

2929

3030instance Functor CGI where

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

32− return (f a, i))

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

32+ return (f a, i))

3333

3434instance Applicative CGI where

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

lib/Prelude.idr+130−9

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

4646 show True = "True"

4747 show False = "False"

4848

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+

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

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

51163

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

69181---- Functor instances

70182

71183instance Functor IO where

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

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

73185

74186instance Functor Maybe where

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

76− fmap f Nothing = Nothing

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

188+ map f Nothing = Nothing

77189

78190instance Functor (Either e) where

79− fmap f (Left l) = Left l

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

81−

82−instance Functor List where

83− fmap = map

191+ map f (Left l) = Left l

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

84193

85194---- Applicative instances

86195

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

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

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

230339

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+

231352---- some basic io

232353

233354partial

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

252373

253374partial

254375getChar : IO Char

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

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

256377

257378---- some basic file handling

258379

lib/Prelude/Applicative.idr+3−3

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

1313

1414infixl 2 <$

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

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

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

1717

1818infixl 2 $>

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

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

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

2121

2222infixl 3 <|>

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

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

3232

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

3434sequence [] = pure []

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

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

3636

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

3838sequence_ [] = pure ()

lib/Prelude/Functor.idr+1−1

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

11module Prelude.Functor

33class 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

33import Builtins

55import Prelude.Algebra

6+import Prelude.Functor

67import Prelude.Maybe

78import Prelude.Nat

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

163164-- instance VerifiedSemigroup (List a) where

164165-- semigroupOpIsAssociative = appendAssociative

165166

167+instance Functor List where

168+ map f [] = []

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

170+

166171--------------------------------------------------------------------------------

167172-- Zips and unzips

168173--------------------------------------------------------------------------------

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

201206-- Maps

202207--------------------------------------------------------------------------------

203208

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

205−map f [] = []

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

207−

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

209210mapMaybe f [] = []

210211mapMaybe f (x::xs) =

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

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

1616 lift : IO a -> Process msg a

1717

1818instance Functor (Process msg) where

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

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

2020

2121instance Applicative (Process msg) where

2222 pure = lift . return

src/IRTS/CodegenJavaScript.hs+65−69

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

2020

2121idrNamespace :: String

2222idrNamespace = "__IDR__"

23+idrRTNamespace = "__IDRRT__"

2324

2425data JSTarget = Node | JavaScript deriving Eq

2526

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

4142 writeFile filename ( header

4243 ++ idrRuntime

4344 ++ tgtRuntime

44− ++ modules

4545 ++ functions

4646 ++ mainLoop)

4747

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

5656

5757 mainLoop :: String

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

59− , createTailcall "__IDR__.runMain0()"

59+ , createTailcall "__IDR__runMain0()"

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

6161 ]

6262

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−

7263translateIdentifier :: String -> String

7364translateIdentifier =

7465 replaceReserved . concatMap replaceBadChars

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

127118 , "yield"

128119 ]

129120

130−translateNamespace :: Name -> [String]

131−translateNamespace (UN _) = [idrNamespace]

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

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

121+translateNamespace :: Name -> String

122+translateNamespace (UN _) = idrNamespace

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

124+translateNamespace (MN _ _) = idrNamespace

134125

135126translateName :: Name -> String

136127translateName (UN name) = translateIdentifier name

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

139130

140131translateConstant :: Const -> String

141132translateConstant (I i) = show i

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

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

143134translateConstant (Fl f) = show f

144135translateConstant (Ch c) = show c

145136translateConstant (Str s) = show s

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

147−translateConstant StrType = "__IDRRT__.String"

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

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

150−translateConstant PtrType = "__IDRRT__.Ptr"

151−translateConstant Forgot = "__IDRRT__.Forgot"

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

138+translateConstant StrType = idrRTNamespace ++ "String"

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

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

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

142+translateConstant PtrType = idrRTNamespace ++ "Ptr"

143+translateConstant Forgot = idrRTNamespace ++ "Forgot"

152144translateConstant c =

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

154146

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

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

158150 translateParameter (UN name) = translateIdentifier name

159151

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

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

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

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

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

163155 ++ " = function("

164156 ++ intercalate "," p

165157 ++ "){\n"

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

205197 createTailcall $ translateFunctionCall name vars

206198

207199translateExpression (SApp True name vars) =

208− "new __IDRRT__.Tailcall("

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

209201 ++ "function(){\n"

210202 ++ "return " ++ translateFunctionCall name vars

211203 ++ ";\n})"

212204

213205translateExpression (SOp op vars)

214− | (LPlus _) <- op

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

216− | (LMinus _) <- op

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

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

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

207+

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

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

246210

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

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

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

284248 | (LGe ATFloat) <- op

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

286250

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+

287284 | LStrConcat <- op

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

289286 | LStrEq <- op

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

298295 | (LIntStr ITNative) <- op

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

300297 | (LSExt ITNative ITBig) <- op

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

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

302299 | (LTrunc ITBig ITNative) <- op

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

304301 | (LIntStr ITBig) <- op

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

306303 | (LStrInt ITBig) <- op

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

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

308305 | LFloatStr <- op

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

310307 | LStrFloat <- op

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

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

368365

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

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

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

371368

372369translateExpression (SForeign _ _ fun args)

373370 | "[]=" `isSuffixOf` fun

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

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

424421

425422 generateWrapper (ffunc, name)

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

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

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

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

428425

429426 generateWrapper (_, name) =

430427 translateVariableName name

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

444441 ++ ")"

445442

446443translateExpression (SCon i name vars) =

447− concat [ "new __IDRRT__.Con("

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

448445 , show i

449446 , ",["

450447 , intercalate "," $ map translateVariableName vars

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

480477 matchHelper tyName = translateTypeMatch var tyName e

481478

482479translateCase 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

484481 createIfBlock cond (translateExpression e)

485482

486483translateCase var (SConstCase cst e) =

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

488485 createIfBlock cond (translateExpression e)

489486

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

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

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

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

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

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

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

503500translateTypeMatch var ty exp =

504501 let e = translateExpression exp in

505502 createIfBlock (var

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

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

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

508505

509506

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

513510 ++ ";\n}"

514511

515512createTailcall call =

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

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

517514

518515translateFunctionCall name vars =

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

520− ++ "."

516+ translateNamespace name

521517 ++ translateName name

522518 ++ "("

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

src/IRTS/CodegenLLVM.hs+5

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

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

922922 box fty nv'

923923

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+

924929cgOp LStrEq [x,y] = do

925930 x' <- unbox FString x

926931 y' <- unbox FString y

src/IRTS/Compiler.hs+8

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

309309mkIty "FByte" = mkIntIty "IT8"

310310mkIty "FShort" = mkIntIty "IT16"

311311mkIty "FLong" = mkIntIty "IT64"

312+mkIty "FBits8" = mkIntIty "IT8"

313+mkIty "FBits16" = mkIntIty "IT16"

314+mkIty "FBits32" = mkIntIty "IT32"

315+mkIty "FBits64" = mkIntIty "IT64"

312316mkIty "FString" = FString

313317mkIty "FPtr" = FPtr

314318mkIty "FUnit" = FUnit

315319mkIty "FFunction" = FFunction

316320mkIty "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))

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

318326

319327mkIntIty "ITNative" = FArith (ATInt ITNative)

src/IRTS/Lang.hs+1

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

3838 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

3939 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

4040 | LPrintNum | LPrintStr | LReadStr

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

4142

4344 | LFSqrt | LFFloor | LFCeil

src/Idris/Primitives.hs+98−11

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

1212import Data.Word

1313import Data.Int

1414import Data.Char

15+import Data.Vector.Unboxed (Vector)

1516import qualified Data.Vector.Unboxed as V

1617

1718data Prim = Prim { p_name :: Name,

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

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

170171 (0, LStdIn) partial

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

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

173+ ++ concatMap vecOps vecTypes

174+ ++ vecBitcasts vecTypes

175+

176+vecTypes :: [IntTy]

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

173178

174179intOps :: IntTy -> [Prim]

175180intOps ity = intCmps ity ++ intArith ity ++ intConv ity

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

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

237242 ] ++ intArith ity ++ vecCmps ity

238243

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+

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

240320mkVecCon ity count args

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

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

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

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

266346 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"

267353

268354intTyName :: IntTy -> String

269355intTyName ITNative = "Int"

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

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

449535

450536intToInt :: 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

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

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

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

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

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

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

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

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

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

458544intToInt _ _ _ = Nothing

459545

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

461547zext from ITBig val = intToInt from ITBig val

462548zext ITBig _ _ = Nothing

463−zext from to val

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

549+zext f@(ITFixed from) t@(ITFixed 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

465553zext _ _ _ = Nothing

466554

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

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

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

476564trunc ITBig to val = intToInt ITBig to val

477565trunc _ 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

479569trunc _ _ _ = Nothing

480570

481571intToStr :: [Const] -> Maybe Const

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

553643

554644p_cantreduce :: a -> Maybe b

555645p_cantreduce _ = Nothing

556−

557−

558−

test/Makefile−1

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

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

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

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

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

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

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

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

test/reg001/reg001.idr+1−1

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

22apply f x = f x

44class 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

77data Imp : Type where

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

test/test007/test007.idr+1−1

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

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

1515

1616instance 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))

1818

1919instance Applicative Eval where

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

tutorial/examples/idiom.idr+1−1

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

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

1515

1616instance 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))

1818

1919instance Applicative Eval where

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