@@ -187,32 +187,24 @@ makeIntBound isBigInt bits =
187
187
name = if isBigInt then " bigint_bound_" else " int_bound_"
188
188
in addConstToPreamble (name ++ show bits) (f " 2" ++ " ** " ++ f (show bits))
189
189
190
- truncateIntWithBitMask : {auto c : Ref ESs ESSt} -> Int -> String -> Core String
191
- truncateIntWithBitMask bits e =
192
- let bs = show bits
193
- f = adjInt bits
194
- in do ib <- makeIntBound (useBigInt' bits) bits
195
- mn <- addConstToPreamble (" int_mask_neg_" ++ bs) (" -" ++ ib)
196
- mp <- addConstToPreamble (" int_mask_pos_" ++ bs) (ib ++ " - " ++ f " 1" )
197
- pure $ concat {t = List }
198
- [ " ((" , ib, " & " , e, " ) == " ++ ib ++ " ? "
199
- , " (" , e, " | " , mn, " ) : "
200
- , " (" , e, " & " , mp, " )"
201
- , " )"
202
- ]
203
-
204
- -- We can't determine `isBigInt` from the given number of bits, since
205
- -- when casting from BigInt to Number we need to truncate the BigInt
206
- -- first, otherwise we might lose precision
207
- boundedInt : {auto c : Ref ESs ESSt} ->
208
- (isBigInt : Bool ) -> Int -> String -> Core String
209
- boundedInt isBigInt bits e =
210
- let name = if isBigInt then " truncToBigInt" else " truncToInt"
211
- in do n <- makeIntBound isBigInt bits
212
- fn <- addConstToPreamble
190
+ boundedInt : {auto c : Ref ESs ESSt}
191
+ -> (isBigInt : Bool )
192
+ -> Int
193
+ -> String
194
+ -> Core String
195
+ boundedInt useBigInt bits e =
196
+ let bs = show bits
197
+ f = if useBigInt then toBigInt else id
198
+ name = if useBigInt then " truncToBigInt" else " truncToInt"
199
+ in do max <- makeIntBound useBigInt bits
200
+ half <- makeIntBound useBigInt (bits - 1 )
201
+ fn <- addConstToPreamble
213
202
(name ++ show bits)
214
- (" x=>(x<(-" ++ n ++ " )||(x>=" ++ n ++ " ))?x%" ++ n ++ " :x" )
215
- pure $ fn ++ " (" ++ e ++ " )"
203
+ ( concat {t = List }
204
+ [ " x=>{ const v = x<" ,f " 0" ," ?x%" ,max ," +" ,max ," :x%" ,max ," ;"
205
+ , " return v>=" ,half," ?" ," v-" ,max ," :v}"
206
+ ])
207
+ pure $ fn ++ " (" ++ e ++ " )"
216
208
217
209
boundedUInt : {auto c : Ref ESs ESSt} ->
218
210
(isBigInt : Bool ) -> Int -> String -> Core String
@@ -229,10 +221,6 @@ boundedIntOp : {auto c : Ref ESs ESSt} ->
229
221
boundedIntOp bits o lhs rhs =
230
222
boundedInt (useBigInt' bits) bits (binOp o lhs rhs)
231
223
232
- boundedIntBitOp : {auto c : Ref ESs ESSt} ->
233
- Int -> String -> String -> String -> Core String
234
- boundedIntBitOp bits o lhs rhs = truncateIntWithBitMask bits (binOp o lhs rhs)
235
-
236
224
boundedUIntOp : {auto c : Ref ESs ESSt} ->
237
225
Int -> String -> String -> String -> Core String
238
226
boundedUIntOp bits o lhs rhs =
@@ -267,12 +255,12 @@ mult : {auto c : Ref ESs ESSt}
267
255
-> (y : String)
268
256
-> Core String
269
257
mult (Just $ Signed $ P 32 ) x y =
270
- fromBigInt <$> boundedInt True 31 (binOp " *" (toBigInt x) (toBigInt y))
258
+ fromBigInt <$> boundedInt True 32 (binOp " *" (toBigInt x) (toBigInt y))
271
259
272
260
mult (Just $ Unsigned 32 ) x y =
273
261
fromBigInt <$> boundedUInt True 32 (binOp " *" (toBigInt x) (toBigInt y))
274
262
275
- mult (Just $ Signed $ P n) x y = boundedIntOp (n - 1 ) " *" x y
263
+ mult (Just $ Signed $ P n) x y = boundedIntOp n " *" x y
276
264
mult (Just $ Unsigned n) x y = boundedUIntOp n " *" x y
277
265
mult _ x y = pure $ binOp " *" x y
278
266
@@ -281,7 +269,11 @@ div : {auto c : Ref ESs ESSt}
281
269
-> (x : String)
282
270
-> (y : String)
283
271
-> Core String
284
- div (Just k) x y =
272
+ div (Just $ Signed $ Unlimited ) x y = pure $ binOp " /" x y
273
+ div (Just $ k@(Signed $ P n)) x y =
274
+ if useBigInt k then boundedIntOp n " /" x y
275
+ else boundedInt False n (jsIntOfDouble k (x ++ " / " ++ y))
276
+ div (Just $ k@(Unsigned n)) x y =
285
277
if useBigInt k then pure $ binOp " /" x y
286
278
else pure $ jsIntOfDouble k (x ++ " / " ++ y)
287
279
div Nothing x y = pure $ binOp " /" x y
@@ -295,7 +287,7 @@ arithOp : {auto c : Ref ESs ESSt}
295
287
-> (x : String)
296
288
-> (y : String)
297
289
-> Core String
298
- arithOp (Just $ Signed $ P n) op x y = boundedIntOp (n - 1 ) op x y
290
+ arithOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y
299
291
arithOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y
300
292
arithOp _ op x y = pure $ binOp op x y
301
293
@@ -310,7 +302,7 @@ bitOp : {auto c : Ref ESs ESSt}
310
302
-> (x : String)
311
303
-> (y : String)
312
304
-> Core String
313
- bitOp (Just $ Signed $ P n) op x y = boundedIntBitOp (n - 1 ) op x y
305
+ bitOp (Just $ Signed $ P n) op x y = boundedIntOp n op x y
314
306
bitOp (Just $ Unsigned 32 ) op x y =
315
307
fromBigInt <$> boundedUInt True 32 (binOp op (toBigInt x) (toBigInt y))
316
308
bitOp (Just $ Unsigned n) op x y = boundedUIntOp n op x y
@@ -328,7 +320,7 @@ constPrimitives = MkConstantPrimitives {
328
320
}
329
321
where truncInt : (isBigInt : Bool ) -> IntKind -> String -> Core String
330
322
truncInt b (Signed Unlimited ) = pure
331
- truncInt b (Signed $ P n) = boundedInt b (n - 1 )
323
+ truncInt b (Signed $ P n) = boundedInt b n
332
324
truncInt b (Unsigned n) = boundedUInt b n
333
325
334
326
shrink : IntKind -> IntKind -> String -> String
0 commit comments