927fd18 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Machine integer comparison primitives and a proofy interface to the equality case

commit927fd1856d490cd93b1c67e8a8b2b28b556490d9 authorBenjamin Saunders <besaunde@sfu.ca> dateSun 23 Dec 2012, 15:24 (14 years ago) parent0b96076

3 files changed+70

compare with master

unifiedsplit

lib/Prelude/Bits.idr+14 src/IRTS/Lang.hs+4 src/Idris/Primitives.hs+52

lib/Prelude/Bits.idr+14

@@ -191,3 +191,17 @@ bitsToStr' {n=n} x with (nextBits n)

191191public

192192bitsToStr : Bits n -> String

193193bitsToStr (MkBits x) = bitsToStr' x

194+

195+bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int

196+bitsEq' {n=n} x y with (nextBits n)

197+ | Bits8 = prim__eqB8 x y

198+ | Bits16 = prim__eqB16 x y

199+ | Bits32 = prim__eqB32 x y

200+ | Bits64 = prim__eqB64 x y

201+

202+public

203+bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y) (x = y -> _|_)

204+bitsEq (MkBits x) (MkBits y) =

205+ case (bitsEq' x y) of

206+ 0 => Right (believe_me ())

207+ _ => Left (believe_me ())

src/IRTS/Lang.hs+4

@@ -40,15 +40,19 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

4040 | LIntBig | LBigInt | LStrBig | LBigStr

4141 | LPrintNum | LPrintStr | LReadStr

4242

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

4850 | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation

5154 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

5458 | LB64T8 | LB64T16 | LB64T32

src/Idris/Primitives.hs+52

@@ -77,6 +77,16 @@ primitives =

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

7878 (2, LGe) total,

7979

80+ Prim (UN "prim__ltB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<))

81+ (2, LB8Lt) total,

82+ Prim (UN "prim__lteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<=))

83+ (2, LB8Lte) total,

84+ Prim (UN "prim__eqB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (==))

85+ (2, LB8Eq) total,

86+ Prim (UN "prim__gteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>))

87+ (2, LB8Gte) total,

88+ Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))

89+ (2, LB8Gt) total,

8090 Prim (UN "prim__b8ToStr") (ty [B8Type] StrType) 1 (b8ToStr)

8191 (1, LB8Str) total,

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

@@ -116,6 +126,16 @@ primitives =

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

117127 (1, LB8Z64) total,

118128

129+ Prim (UN "prim__ltB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<))

130+ (2, LB16Lt) total,

131+ Prim (UN "prim__lteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<=))

132+ (2, LB16Lte) total,

133+ Prim (UN "prim__eqB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (==))

134+ (2, LB16Eq) total,

135+ Prim (UN "prim__gteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>))

136+ (2, LB16Gte) total,

137+ Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))

138+ (2, LB16Gt) total,

119139 Prim (UN "prim__b16ToStr") (ty [B16Type] StrType) 1 (b16ToStr)

120140 (1, LB16Str) total,

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

@@ -153,6 +173,16 @@ primitives =

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

154174 (1, LB16T8) total,

155175

176+ Prim (UN "prim__ltB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<))

177+ (2, LB32Lt) total,

178+ Prim (UN "prim__lteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<=))

179+ (2, LB32Lte) total,

180+ Prim (UN "prim__eqB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (==))

181+ (2, LB32Eq) total,

182+ Prim (UN "prim__gteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>))

183+ (2, LB32Gte) total,

184+ Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))

185+ (2, LB32Gt) total,

156186 Prim (UN "prim__b32ToStr") (ty [B32Type] StrType) 1 (b32ToStr)

157187 (1, LB32Str) total,

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

@@ -188,6 +218,16 @@ primitives =

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

189219 (1, LB32T16) total,

190220

221+ Prim (UN "prim__ltB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<))

222+ (2, LB64Lt) total,

223+ Prim (UN "prim__lteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<=))

224+ (2, LB64Lte) total,

225+ Prim (UN "prim__eqB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (==))

226+ (2, LB64Eq) total,

227+ Prim (UN "prim__gteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>))

228+ (2, LB64Gte) total,

229+ Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))

230+ (2, LB64Gt) total,

191231 Prim (UN "prim__b64ToStr") (ty [B64Type] StrType) 1 (b64ToStr)

192232 (1, LB64Str) total,

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

@@ -419,6 +459,18 @@ b32Bin _ _ = Nothing

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

420460b64Bin _ _ = Nothing

421461

462+b8Cmp op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

463+b8Cmp _ _ = Nothing

464+

465+b16Cmp op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

466+b16Cmp _ _ = Nothing

467+

468+b32Cmp op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

469+b32Cmp _ _ = Nothing

470+

471+b64Cmp op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

472+b64Cmp _ _ = Nothing

473+

422474toB8 x = VConstant (B8 (fromIntegral x))

423475toB16 x = VConstant (B16 (fromIntegral x))

424476toB32 x = VConstant (B32 (fromIntegral x))