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

git.iko.soy/Idris-dev

on master help sign in

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

927fd18Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+14

compare with master

unifiedsplit

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

191public

192bitsToStr : Bits n -> String

193bitsToStr (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

40 | LIntBig | LBigInt | LStrBig | LBigStr

41 | LPrintNum | LPrintStr | LReadStr

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

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

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

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

51 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

54 | LB32Z64 | LB32S64 | LB32T8 | LB32T16

54 | LB64T8 | LB64T16 | LB64T32

58 | LB64T8 | LB64T16 | LB64T32

src/Idris/Primitives.hs+52

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

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

78 (2, LGe) total,

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,

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

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

81 (1, LB8Str) total,

91 (1, LB8Str) total,

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

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

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

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

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

117 (1, LB8Z64) total,

127 (1, LB8Z64) total,

118

128

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,

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

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

120 (1, LB16Str) total,

140 (1, LB16Str) total,

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

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

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

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

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

154 (1, LB16T8) total,

174 (1, LB16T8) total,

155

175

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,

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

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

157 (1, LB32Str) total,

187 (1, LB32Str) total,

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

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

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

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

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

189 (1, LB32T16) total,

219 (1, LB32T16) total,

190

220

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,

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

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

192 (1, LB64Str) total,

232 (1, LB64Str) total,

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

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

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

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

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

420b64Bin _ _ = Nothing

460b64Bin _ _ = Nothing

421

461

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+

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

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

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

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

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

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