b896224 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on them

commitb896224c69a66662a93f5ea1d43b2746f1e349a0 authorBenjamin Saunders <besaunde@sfu.ca> dateWed 19 Dec 2012, 16:59 (14 years ago) parentbfd5b51

10 files changed+223−55

compare with master

unifiedsplit

src/Core/CaseTree.hs+4−2 src/Core/CoreParser.hs+1−1 src/Core/Evaluate.hs+4−2 src/Core/TT.hs+14−8 src/Core/Typecheck.hs+4−2 src/IRTS/Compiler.hs+4−2 src/IRTS/Lang.hs+10−4 src/Idris/IBC.hs+8−4 src/Idris/Parser.hs+4−2 src/Idris/Primitives.hs+170−28

src/Core/CaseTree.hs+4−2

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

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

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

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

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

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

230+ toPat' (Constant B8Type) [] | tc = return $ PCon (UN "Bits8") 7 []

231+ toPat' (Constant B16Type) [] | tc = return $ PCon (UN "Bits16") 8 []

232+ toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 [] -- TODO: Verify numbers

233+ toPat' (Constant B64Type) [] | tc = return $ PCon (UN "Bits64") 10 []

232234

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

234236 if n `elem` ns

src/Core/CoreParser.hs+1−1

@@ -36,7 +36,7 @@ idrisDef = haskellDef {

3636 "using", "namespace", "class", "instance",

3737 "public", "private", "abstract",

3838 "Int", "Integer", "Float", "Char", "String", "Ptr",

39− "Word8", "Word16"]

39+ "Bits8", "Bits16", "Bits32", "Bits64"]

4040 }

4141

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

src/Core/Evaluate.hs+4−2

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

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

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

528528 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 B8Type (ConCase n 6 [] v : xs) = Just v

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

531+ findConst B32Type (ConCase n 8 [] v : xs) = Just v

532+ findConst B64Type (ConCase n 9 [] v : xs) = Just v -- TODO: Verify numbers

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

532534

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

src/Core/TT.hs+14−8

@@ -260,8 +260,8 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

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

262262

263− | W8 Word8 | W16 Word16

264− | W8Type | W16Type

263+ | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

264+ | B8Type | B16Type | B32Type | B64Type

265265

266266 | PtrType | VoidType | Forgot

267267 deriving (Eq, Ord)

@@ -286,8 +286,10 @@ instance Pretty Const where

286286 pretty PtrType = text "Ptr"

287287 pretty VoidType = text "Void"

288288 pretty Forgot = text "Forgot"

289− pretty W8Type = text "Word8"

290− pretty W16Type = text "Word16"

289+ pretty B8Type = text "Bits8"

290+ pretty B16Type = text "Bits16"

291+ pretty B32Type = text "Bits32"

292+ pretty B64Type = text "Bits64"

291293

292294data Raw = Var Name

293295 | RBind Name (Binder Raw) Raw

@@ -689,16 +691,20 @@ instance Show Const where

689691 show (Fl f) = show f

690692 show (Ch c) = show c

691693 show (Str s) = show s

692− show (W8 x) = show x

693− show (W16 x) = show x

694+ show (B8 x) = show x

695+ show (B16 x) = show x

696+ show (B32 x) = show x

697+ show (B64 x) = show x

694698 show IType = "Int"

695699 show BIType = "Integer"

696700 show FlType = "Float"

697701 show ChType = "Char"

698702 show StrType = "String"

699703 show PtrType = "Ptr"

700− show W8Type = "Word8"

701− show W16Type = "Word16"

704+ show B8Type = "Bits8"

705+ show B16Type = "Bits16"

706+ show B32Type = "Bits32"

707+ show B64Type = "Bits64"

702708 show VoidType = "Void"

703709

704710showEnv env t = showEnv' env t False

src/Core/Typecheck.hs+4−2

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

100100 constType (Fl _) = Constant FlType

101101 constType (Ch _) = Constant ChType

102102 constType (Str _) = Constant StrType

103− constType (W8 _) = Constant W8Type

104− constType (W16 _) = Constant W16Type

103+ constType (B8 _) = Constant B8Type

104+ constType (B16 _) = Constant B16Type

105+ constType (B32 _) = Constant B32Type

106+ constType (B64 _) = Constant B64Type

105107 constType Forgot = Erased

106108 constType _ = TType (UVal 0)

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

src/IRTS/Compiler.hs+4−2

@@ -339,8 +339,10 @@ instance ToIR SC where

339339 matchableTy ChType = True

340340 matchableTy StrType = True

341341

342− matchableTy W8Type = True

343− matchableTy W16Type = True

342+ matchableTy B8Type = True

343+ matchableTy B16Type = True

344+ matchableTy B32Type = True

345+ matchableTy B64Type = True

344346

345347 matchableTy _ = False

346348

src/IRTS/Lang.hs+10−4

@@ -40,10 +40,16 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

4040 | LIntBig | LBigInt | LStrBig | LBigStr

4141 | LPrintNum | LPrintStr | LReadStr

4242

43− | LW8 | LW16

44−

45− | LW8Plus | LW8Minus | LW8Times

46− | LW16Plus | LW16Minus | LW16Times

43+ | LB8 | LB16

44+

46+ | LB8Z16 | LB8Z32 | LB8Z64 | LB8S16 | LB8S32 | LB8S64 -- Zero/Sign extension

48+ | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation

50+ | LB32Z64 | LB32S32 | LB32T8 | LB32T16

52+ | LB64T8 | LB64T16 | LB64T32

4753

4955 | LFSqrt | LFFloor | LFCeil

src/Idris/IBC.hs+8−4

@@ -361,8 +361,10 @@ instance Binary Const where

361361 PtrType -> putWord8 10

362362 Forgot -> putWord8 11

363363

364− W8Type -> putWord8 12

365− W16Type -> putWord8 13

364+ B8Type -> putWord8 12

365+ B16Type -> putWord8 13

366+ B32Type -> putWord8 14

367+ B64Type -> putWord8 15

366368 get

367369 = do i <- getWord8

368370 case i of

@@ -384,8 +386,10 @@ instance Binary Const where

384386 10 -> return PtrType

385387 11 -> return Forgot

386388

387− 12 -> return W8Type

388− 13 -> return W16Type

389+ 12 -> return B8Type

390+ 13 -> return B16Type

391+ 14 -> return B32Type

392+ 15 -> return B64Type

389393

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

391395

src/Idris/Parser.hs+4−2

@@ -1081,8 +1081,10 @@ pConstant = do reserved "Integer";return BIType

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

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

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

1084− <|> do reserved "Word8"; return W8Type

1085− <|> do reserved "Word16"; return W16Type

1084+ <|> do reserved "Bits8"; return B8Type

1085+ <|> do reserved "Bits16"; return B16Type

1086+ <|> do reserved "Bits32"; return B32Type

1087+ <|> do reserved "Bits64"; return B64Type

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

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

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

src/Idris/Primitives.hs+170−28

@@ -11,6 +11,8 @@ import IRTS.Lang

1111import Core.TT

1212import Core.Evaluate

1313import Data.Bits

14+import Data.Word

15+import Data.Int

1416

1517data Prim = Prim { p_name :: Name,

1618 p_type :: Type,

@@ -75,24 +77,90 @@ primitives =

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

7678 (2, LGe) total,

7779

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,

80+ Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))

81+ (2, LB8Plus) total,

82+ Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))

83+ (2, LB8Minus) total,

84+ Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))

85+ (2, LB8Times) total,

86+ Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)

87+ (2, LB8UDiv) total,

88+ Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)

89+ (2, LB8SDiv) total,

90+ Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16

91+ (1, LB8Z16) total,

92+ Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32

93+ (1, LB8Z32) total,

94+ Prim (UN "prim__zextB8_64") (ty [B8Type] B64Type) 1 zext8_64

95+ (1, LB8Z64) total,

96+ Prim (UN "prim__sextB8_16") (ty [B8Type] B16Type) 1 sext8_16

97+ (1, LB8Z16) total,

98+ Prim (UN "prim__sextB8_32") (ty [B8Type] B32Type) 1 sext8_32

99+ (1, LB8Z32) total,

100+ Prim (UN "prim__sextB8_64") (ty [B8Type] B64Type) 1 sext8_64

101+ (1, LB8Z64) total,

102+

103+ Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))

104+ (2, LB16Plus) total,

105+ Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))

106+ (2, LB16Minus) total,

107+ Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))

108+ (2, LB16Times) total,

109+ Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)

110+ (2, LB16UDiv) total,

111+ Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)

112+ (2, LB16SDiv) total,

113+ Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32

114+ (1, LB16Z32) total,

115+ Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64

116+ (1, LB16Z64) total,

117+ Prim (UN "prim__sextB16_32") (ty [B16Type] B32Type) 1 sext16_32

118+ (1, LB16Z32) total,

119+ Prim (UN "prim__sextB16_64") (ty [B16Type] B64Type) 1 sext16_64

120+ (1, LB16Z64) total,

121+ Prim (UN "prim__truncB16_8") (ty [B16Type] B8Type) 1 trunc16_8

122+ (1, LB16T8) total,

123+

124+ Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))

125+ (2, LB32Plus) total,

126+ Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))

127+ (2, LB32Minus) total,

128+ Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))

129+ (2, LB32Times) total,

130+ Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)

131+ (2, LB32UDiv) total,

132+ Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)

133+ (2, LB32SDiv) total,

134+ Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64

135+ (1, LB32Z64) total,

136+ Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64

137+ (1, LB32Z64) total,

138+ Prim (UN "prim__truncB32_8") (ty [B32Type] B8Type) 1 trunc32_8

139+ (1, LB32T8) total,

140+ Prim (UN "prim__truncB32_16") (ty [B32Type] B16Type) 1 trunc32_16

141+ (1, LB32T16) total,

142+

143+ Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))

144+ (2, LB64Plus) total,

145+ Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))

146+ (2, LB64Minus) total,

147+ Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))

148+ (2, LB64Times) total,

149+ Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)

150+ (2, LB64UDiv) total,

151+ Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)

152+ (2, LB64SDiv) total,

153+ Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8

154+ (1, LB64T8) total,

155+ Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16

156+ (1, LB64T16) total,

157+ Prim (UN "prim__truncB64_32") (ty [B64Type] B32Type) 1 trunc64_32

158+ (1, LB64T32) total,

159+

160+ Prim (UN "prim__intToBits8") (ty [IType] B8Type) 1 intToBits8

161+ (1, LB8) total,

162+ Prim (UN "prim__intToBits16") (ty [IType] B16Type) 1 intToBits16

163+ (1, LB16) total,

96164

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

98166 (2, LBPlus) total,

@@ -245,19 +313,93 @@ bsBin _ _ = Nothing

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

246314sBin _ _ = Nothing

247315

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

249−w8Bin _ _ = Nothing

316+s8div :: Word8 -> Word8 -> Word8

317+s8div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)

250318

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

252−w16Bin _ _ = Nothing

319+s16div :: Word16 -> Word16 -> Word16

320+s16div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)

253321

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

255−-- w32Bin _ _ = Nothing

322+s32div :: Word32 -> Word32 -> Word32

323+s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)

256324

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

325+s64div :: Word64 -> Word64 -> Word64

326+s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)

327+

328+b8Bin op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))

329+b8Bin _ _ = Nothing

330+

331+b16Bin op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))

332+b16Bin _ _ = Nothing

333+

334+b32Bin op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))

335+b32Bin _ _ = Nothing

336+

337+b64Bin op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))

338+b64Bin _ _ = Nothing

339+

340+toB8 x = VConstant (B8 (fromIntegral x))

341+toB16 x = VConstant (B16 (fromIntegral x))

342+toB32 x = VConstant (B32 (fromIntegral x))

343+toB64 x = VConstant (B64 (fromIntegral x))

344+

345+zext8_16 [VConstant (B8 x)] = Just $ toB16 x

346+zext8_16 _ = Nothing

347+

348+zext8_32 [VConstant (B8 x)] = Just $ toB32 x

349+zext8_32 _ = Nothing

350+

351+zext8_64 [VConstant (B8 x)] = Just $ toB64 x

352+zext8_64 _ = Nothing

353+

354+sext8_16 [VConstant (B8 x)] = Just $ toB16 (fromIntegral x :: Int8)

355+sext8_16 _ = Nothing

356+

357+sext8_32 [VConstant (B8 x)] = Just $ toB32 (fromIntegral x :: Int8)

358+sext8_32 _ = Nothing

359+

360+sext8_64 [VConstant (B8 x)] = Just $ toB64 (fromIntegral x :: Int8)

361+sext8_64 _ = Nothing

362+

363+zext16_32 [VConstant (B16 x)] = Just $ toB32 x

364+zext16_32 _ = Nothing

365+

366+zext16_64 [VConstant (B16 x)] = Just $ toB64 x

367+zext16_64 _ = Nothing

368+

369+sext16_32 [VConstant (B16 x)] = Just $ toB32 (fromIntegral x :: Int16)

370+sext16_32 _ = Nothing

371+

372+sext16_64 [VConstant (B16 x)] = Just $ toB64 (fromIntegral x :: Int16)

373+sext16_64 _ = Nothing

374+

375+trunc16_8 [VConstant (B16 x)] = Just $ toB8 x

376+trunc16_8 _ = Nothing

377+

378+zext32_64 [VConstant (B32 x)] = Just $ toB64 x

379+zext32_64 _ = Nothing

380+

381+sext32_64 [VConstant (B32 x)] = Just $ toB64 (fromIntegral x :: Int32)

382+sext32_64 _ = Nothing

383+

384+trunc32_8 [VConstant (B32 x)] = Just $ toB8 x

385+trunc32_8 _ = Nothing

386+

387+trunc32_16 [VConstant (B32 x)] = Just $ toB16 x

388+trunc32_16 _ = Nothing

389+

390+trunc64_8 [VConstant (B64 x)] = Just $ toB8 x

391+trunc64_8 _ = Nothing

392+

393+trunc64_16 [VConstant (B64 x)] = Just $ toB16 x

394+trunc64_16 _ = Nothing

395+

396+trunc64_32 [VConstant (B64 x)] = Just $ toB32 x

397+trunc64_32 _ = Nothing

398+

399+intToBits8 [VConstant (I x)] = Just $ toB8 x

400+intToBits8 _ = Nothing

401+intToBits16 [VConstant (I x)] = Just $ toB16 x

402+intToBits16 _ = Nothing

261403

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

263405c_intToStr _ = Nothing