f6451ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

word 8/16 primitive types

commitf6451efcf8e179e2b79bc2d62890f4398f9e8e4e authorraichoo <raichoo@googlemail.com> dateSat 1 Dec 2012, 18:56 (14 years ago) parent0c8d6e7

12 files changed+91−4

compare with master

unifiedsplit

lib/Data/Word.idr+19 lib/base.ipkg+1−1 src/Core/CaseTree.hs+2 src/Core/CoreParser.hs+2−1 src/Core/Evaluate.hs+2 src/Core/TT.hs+11−1 src/Core/Typecheck.hs+2 src/IRTS/Compiler.hs+4 src/IRTS/Lang.hs+5 src/Idris/IBC.hs+7 src/Idris/Parser.hs+2 src/Idris/Primitives.hs+34−1

lib/Data/Word.idrnew file+19

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

1+module Data.Word

3+%access public

5+instance Num Word8 where

6+ (+) = prim__addW8

7+ (-) = prim__subW8

8+ (*) = prim__mulW8

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

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

1414

1515 Language.Reflection,

1616

17− Data.Morphisms, Data.Bits,

17+ Data.Morphisms, Data.Bits, Data.Word,

1818

1919 Control.Monad.Identity, Control.Monad.State, Control.Category,

2020 Control.Arrow

src/Core/CaseTree.hs+2

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

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

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

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

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

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

227229

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

229231 if n `elem` ns

src/Core/CoreParser.hs+2−1

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

3535 "where", "with", "syntax", "proof", "postulate",

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

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

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

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

39+ "Word8", "Word16"]

3940 }

4041

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

src/Core/Evaluate.hs+2

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

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

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

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

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

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

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

518520

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

src/Core/TT.hs+11−1

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

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

258258

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

261+

262+ | W8 Word8 | W16 Word16

263+ | W8Type | W16Type

264+

261265 | PtrType | VoidType | Forgot

262266 deriving (Eq, Ord)

263267{-!

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

281285 pretty PtrType = text "Ptr"

282286 pretty VoidType = text "Void"

283287 pretty Forgot = text "Forgot"

288+ pretty W8Type = text "Word8"

289+ pretty W16Type = text "Word16"

284290

285291data Raw = Var Name

286292 | RBind Name (Binder Raw) Raw

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

666672 show (Fl f) = show f

667673 show (Ch c) = show c

668674 show (Str s) = show s

675+ show (W8 x) = show x

676+ show (W16 x) = show x

669677 show IType = "Int"

670678 show BIType = "Integer"

671679 show FlType = "Float"

672680 show ChType = "Char"

673681 show StrType = "String"

674682 show PtrType = "Ptr"

683+ show W8Type = "Word8"

684+ show W16Type = "Word16"

675685 show VoidType = "Void"

676686

677687showEnv env t = showEnv' env t False

src/Core/Typecheck.hs+2

@@ -100,6 +100,8 @@ 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

103105 constType Forgot = Erased

104106 constType _ = Set (UVal 0)

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

src/IRTS/Compiler.hs+4

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

315315 matchableTy BIType = True

316316 matchableTy ChType = True

317317 matchableTy StrType = True

318+

319+ matchableTy W8Type = True

320+ matchableTy W16Type = True

321+

318322 matchableTy _ = False

319323

src/IRTS/Lang.hs+5

@@ -40,6 +40,11 @@ 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

47+

4449 | LFSqrt | LFFloor | LFCeil

4550

src/Idris/IBC.hs+7

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

360360 StrType -> putWord8 9

361361 PtrType -> putWord8 10

362362 Forgot -> putWord8 11

363+

364+ W8Type -> putWord8 12

365+ W16Type -> putWord8 13

363366 get

364367 = do i <- getWord8

365368 case i of

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

380383 9 -> return StrType

381384 10 -> return PtrType

382385 11 -> return Forgot

386+

387+ 12 -> return W8Type

388+ 13 -> return W16Type

389+

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

384391

385392

src/Idris/Parser.hs+2

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

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

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

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

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

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

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

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

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

src/Idris/Primitives.hs+34−1

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

7474 (2, LGt) total,

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

7676 (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+

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

78−

7998 (2, LBPlus) total,

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

81100 (2, LBMinus) total,

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

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

227246sBin _ _ = Nothing

228247

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+

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

230263c_intToStr _ = Nothing

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