bbbe563 · Idris-dev · git.iko.soy

lib/Data/Word.idrnew file+19

compare with master

unifiedsplit

@@ -0,0 +1,19 @@

1+module Data.Word

2+

3+%access public

4+

5+instance Num Word8 where

6+ (+) = prim__addW8

7+ (-) = prim__subW8

8+ (*) = prim__mulW8

9+

10+ abs x = x

11+ fromInteger = prim__intToWord8

12+

13+instance Num Word16 where

14+ (+) = prim__addW16

15+ (-) = prim__subW16

16+ (*) = prim__mulW16

17+

18+ abs x = x

19+ fromInteger = prim__intToWord16

lib/base.ipkg+1−1

@@ -15,7 +15,7 @@ modules = Builtins, Prelude, IO, System,

15

16 Language.Reflection,

17

18− Data.Morphisms, Data.Bits,

18+ Data.Morphisms, Data.Bits, Data.Word,

19

20 Control.Monad.Identity, Control.Monad.State, Control.Category,

21 Control.Arrow

src/Core/CaseTree.hs+2

@@ -230,6 +230,8 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

230 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

231 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

232 toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

233+ toPat' (Constant W8Type) [] | tc = return $ PCon (UN "Word8") 7 []

234+ toPat' (Constant W16Type) [] | tc = return $ PCon (UN "Word16") 8 []

233

235

234 toPat' (P Bound n _) [] = do ns <- get

236 toPat' (P Bound n _) [] = do ns <- get

235 if n `elem` ns

237 if n `elem` ns

src/Core/CoreParser.hs+2−1

@@ -35,7 +35,8 @@ idrisDef = haskellDef {

35 "where", "with", "syntax", "proof", "postulate",

36 "using", "namespace", "class", "instance",

37 "public", "private", "abstract",

38− "Int", "Integer", "Float", "Char", "String", "Ptr"]

38+ "Int", "Integer", "Float", "Char", "String", "Ptr",

39+ "Word8", "Word16"]

39 }

40 }

40

41

41iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

42iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

src/Core/Evaluate.hs+2

@@ -526,6 +526,8 @@ eval_hnf ctxt statics genv tm = ev [] tm where

526 findConst ChType (ConCase n 3 [] v : xs) = Just v

527 findConst StrType (ConCase n 4 [] v : xs) = Just v

528 findConst PtrType (ConCase n 5 [] v : xs) = Just v

529+ findConst W8Type (ConCase n 6 [] v : xs) = Just v

530+ findConst W16Type (ConCase n 7 [] v : xs) = Just v

529 findConst c (_ : xs) = findConst c xs

531 findConst c (_ : xs) = findConst c xs

530

532

531 getValArgs (HApp t env args) = (t, env, args)

533 getValArgs (HApp t env args) = (t, env, args)

src/Core/TT.hs+11−1

@@ -257,7 +257,11 @@ addAlist [] ctxt = ctxt

257addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

258

259data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

261+

262+ | W8 Word8 | W16 Word16

263+ | W8Type | W16Type

264+

261 | PtrType | VoidType | Forgot

265 | PtrType | VoidType | Forgot

262 deriving (Eq, Ord)

266 deriving (Eq, Ord)

263{-!

267{-!

@@ -281,6 +285,8 @@ instance Pretty Const where

281 pretty PtrType = text "Ptr"

285 pretty PtrType = text "Ptr"

282 pretty VoidType = text "Void"

286 pretty VoidType = text "Void"

283 pretty Forgot = text "Forgot"

287 pretty Forgot = text "Forgot"

288+ pretty W8Type = text "Word8"

289+ pretty W16Type = text "Word16"

284

290

285data Raw = Var Name

291data Raw = Var Name

286 | RBind Name (Binder Raw) Raw

292 | RBind Name (Binder Raw) Raw

@@ -666,12 +672,16 @@ instance Show Const where

666 show (Fl f) = show f

672 show (Fl f) = show f

667 show (Ch c) = show c

673 show (Ch c) = show c

668 show (Str s) = show s

674 show (Str s) = show s

675+ show (W8 x) = show x

676+ show (W16 x) = show x

669 show IType = "Int"

677 show IType = "Int"

670 show BIType = "Integer"

678 show BIType = "Integer"

671 show FlType = "Float"

679 show FlType = "Float"

672 show ChType = "Char"

680 show ChType = "Char"

673 show StrType = "String"

681 show StrType = "String"

674 show PtrType = "Ptr"

682 show PtrType = "Ptr"

683+ show W8Type = "Word8"

684+ show W16Type = "Word16"

675 show VoidType = "Void"

685 show VoidType = "Void"

676

686

677showEnv env t = showEnv' env t False

687showEnv env t = showEnv' env t False

src/Core/Typecheck.hs+2

@@ -100,6 +100,8 @@ check' holes ctxt env top = chk env top where

100 constType (Fl _) = Constant FlType

101 constType (Ch _) = Constant ChType

102 constType (Str _) = Constant StrType

103+ constType (W8 _) = Constant W8Type

104+ constType (W16 _) = Constant W16Type

103 constType Forgot = Erased

105 constType Forgot = Erased

104 constType _ = Set (UVal 0)

106 constType _ = Set (UVal 0)

105 chk env (RForce t) = do (_, ty) <- chk env t

107 chk env (RForce t) = do (_, ty) <- chk env t

src/IRTS/Compiler.hs+4

@@ -317,5 +317,9 @@ instance ToIR SC where

317 matchableTy BIType = True

318 matchableTy ChType = True

319 matchableTy StrType = True

320+

321+ matchableTy W8Type = True

322+ matchableTy W16Type = True

323+

320 matchableTy _ = False

324 matchableTy _ = False

321

325

src/IRTS/Lang.hs+5

@@ -40,6 +40,11 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

40 | LIntBig | LBigInt | LStrBig | LBigStr

41 | LPrintNum | LPrintStr | LReadStr

42

43+ | LW8 | LW16

44+

45+ | LW8Plus | LW8Minus | LW8Times

46+ | LW16Plus | LW16Minus | LW16Times

47+

44 | LFSqrt | LFFloor | LFCeil

49 | LFSqrt | LFFloor | LFCeil

45

50

src/Idris/IBC.hs+7

@@ -360,6 +360,9 @@ instance Binary Const where

360 StrType -> putWord8 9

361 PtrType -> putWord8 10

362 Forgot -> putWord8 11

363+

364+ W8Type -> putWord8 12

365+ W16Type -> putWord8 13

363 get

366 get

364 = do i <- getWord8

367 = do i <- getWord8

365 case i of

368 case i of

@@ -380,6 +383,10 @@ instance Binary Const where

380 9 -> return StrType

383 9 -> return StrType

381 10 -> return PtrType

384 10 -> return PtrType

382 11 -> return Forgot

385 11 -> return Forgot

386+

387+ 12 -> return W8Type

388+ 13 -> return W16Type

389+

383 _ -> error "Corrupted binary data for Const"

390 _ -> error "Corrupted binary data for Const"

384

391

385

392

src/Idris/Parser.hs+2

@@ -1078,6 +1078,8 @@ pConstant = do reserved "Integer";return BIType

1078 <|> do reserved "Float"; return FlType

1079 <|> do reserved "String"; return StrType

1080 <|> do reserved "Ptr"; return PtrType

1081+ <|> do reserved "Word8"; return W8Type

1082+ <|> do reserved "Word16"; return W16Type

1081 <|> try (do f <- float; return $ Fl f)

1083 <|> try (do f <- float; return $ Fl f)

1082-- <|> try (do i <- natural; lchar 'L'; return $ BI i)

1084-- <|> try (do i <- natural; lchar 'L'; return $ BI i)

1083 <|> try (do i <- natural; return $ I (fromInteger i))

1085 <|> try (do i <- natural; return $ I (fromInteger i))

src/Idris/Primitives.hs+34−1

@@ -74,8 +74,27 @@ primitives =

74 (2, LGt) total,

75 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

76 (2, LGe) total,

77+

78+ Prim (UN "prim__addW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (+))

79+ (2, LW8Plus) total,

80+ Prim (UN "prim__subW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (-))

81+ (2, LW8Minus) total,

82+ Prim (UN "prim__mulW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (*))

83+ (2, LW8Times) total,

84+

85+ Prim (UN "prim__addW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (+))

86+ (2, LW16Plus) total,

87+ Prim (UN "prim__subW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (-))

88+ (2, LW16Minus) total,

89+ Prim (UN "prim__mulW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (*))

90+ (2, LW16Times) total,

91+

92+ Prim (UN "prim__intToWord8") (ty [IType] W8Type) 1 intToWord8

93+ (1, LW8) total,

94+ Prim (UN "prim__intToWord16") (ty [IType] W16Type) 1 intToWord16

95+ (1, LW16) total,

96+

77 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

97 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

78−

79 (2, LBPlus) total,

98 (2, LBPlus) total,

80 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

99 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

81 (2, LBMinus) total,

100 (2, LBMinus) total,

@@ -226,6 +245,20 @@ bsBin _ _ = Nothing

226sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

245sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

227sBin _ _ = Nothing

246sBin _ _ = Nothing

228

247

248+w8Bin op [VConstant (W8 x), VConstant (W8 y)] = Just $ VConstant (W8 (op x y))

249+w8Bin _ _ = Nothing

250+

251+w16Bin op [VConstant (W16 x), VConstant (W16 y)] = Just $ VConstant (W16 (op x y))

252+w16Bin _ _ = Nothing

253+

254+w32Bin op [VConstant (W32 x), VConstant (W32 y)] = Just $ VConstant (W32 (op x y))

255+w32Bin _ _ = Nothing

256+

257+intToWord8 [VConstant (I x)] = Just $ VConstant (W8 $ fromIntegral x)

258+intToWord8 _ = Nothing

259+intToWord16 [VConstant (I x)] = Just $ VConstant (W16 $ fromIntegral x)

260+intToWord16 _ = Nothing

261+

229c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))

262c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))

230c_intToStr _ = Nothing

263c_intToStr _ = Nothing

231c_strToInt [VConstant (Str x)] = case reads x of

264c_strToInt [VConstant (Str x)] = case reads x of