idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] Bitwise XOR for Bits64 and Integer (#1026)

Browse Source
This commit is contained in:
Stefan Hoeck 2021-02-16 16:14:56 +01:00 committed by GitHub
parent 0ac34538ec
commit 7401961425
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
13 changed files with 91 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Primitives.idr
View File

@ -529,7 +529,7 @@ allPrimitives =
map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType, Bits8Type, Bits16Type, Bits32Type] ++
map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++

38
tests/chez/chez032/BitOps.idr
View File

@ -260,23 +260,23 @@ xorBits32 = [ prim__xor_Bits32 11 b32max
, prim__xor_Bits32 11 11
]
-- xorBits64 : List Bits64
-- xorBits64 = [ prim__xor_Bits64 11 b64max
-- , prim__xor_Bits64 11 0
-- , prim__xor_Bits64 11 1
-- , prim__xor_Bits64 11 2
-- , prim__xor_Bits64 11 4
-- , prim__xor_Bits64 11 11
-- ]
--
-- xorInteger : List Integer
-- xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
-- , prim__xor_Integer 11 0
-- , prim__xor_Integer 11 1
-- , prim__xor_Integer 11 2
-- , prim__xor_Integer 11 4
-- , prim__xor_Integer 11 11
-- ]
xorBits64 : List Bits64
xorBits64 = [ prim__xor_Bits64 11 b64max
, prim__xor_Bits64 11 0
, prim__xor_Bits64 11 1
, prim__xor_Bits64 11 2
, prim__xor_Bits64 11 4
, prim__xor_Bits64 11 11
]
xorInteger : List Integer
xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
, prim__xor_Integer 11 0
, prim__xor_Integer 11 1
, prim__xor_Integer 11 2
, prim__xor_Integer 11 4
, prim__xor_Integer 11 11
]
xorInt : List Int
xorInt = [ prim__xor_Int 11 intmax
@ -349,7 +349,7 @@ main = do printLn shiftRBits8
printLn xorBits8
printLn xorBits16
printLn xorBits32
-- printLn xorBits64
-- printLn xorInteger
printLn xorBits64
printLn xorInteger
printLn xorInt
printLn xorNegativeInt

2
tests/chez/chez032/expected
View File

@ -33,6 +33,8 @@
[244, 11, 10, 9, 15, 0]
[65524, 11, 10, 9, 15, 0]
[4294967284, 11, 10, 9, 15, 0]
[18446744073709551604, 11, 10, 9, 15, 0]
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
[2147483636, 11, 10, 9, 15, 0]
[-2147483638, -11, -12, -9, -15, -2, 2147483637, 10, 11, 9, 0]
1/1: Building BitOps (BitOps.idr)

38
tests/gambit/bitops001/BitOps.idr
View File

@ -260,23 +260,23 @@ xorBits32 = [ prim__xor_Bits32 11 b32max
, prim__xor_Bits32 11 11
]
-- xorBits64 : List Bits64
-- xorBits64 = [ prim__xor_Bits64 11 b64max
-- , prim__xor_Bits64 11 0
-- , prim__xor_Bits64 11 1
-- , prim__xor_Bits64 11 2
-- , prim__xor_Bits64 11 4
-- , prim__xor_Bits64 11 11
-- ]
--
-- xorInteger : List Integer
-- xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
-- , prim__xor_Integer 11 0
-- , prim__xor_Integer 11 1
-- , prim__xor_Integer 11 2
-- , prim__xor_Integer 11 4
-- , prim__xor_Integer 11 11
-- ]
xorBits64 : List Bits64
xorBits64 = [ prim__xor_Bits64 11 b64max
, prim__xor_Bits64 11 0
, prim__xor_Bits64 11 1
, prim__xor_Bits64 11 2
, prim__xor_Bits64 11 4
, prim__xor_Bits64 11 11
]
xorInteger : List Integer
xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
, prim__xor_Integer 11 0
, prim__xor_Integer 11 1
, prim__xor_Integer 11 2
, prim__xor_Integer 11 4
, prim__xor_Integer 11 11
]
xorInt : List Int
xorInt = [ prim__xor_Int 11 intmax
@ -349,7 +349,7 @@ main = do printLn shiftRBits8
printLn xorBits8
printLn xorBits16
printLn xorBits32
-- printLn xorBits64
-- printLn xorInteger
printLn xorBits64
printLn xorInteger
printLn xorInt
printLn xorNegativeInt

2
tests/gambit/bitops001/expected
View File

@ -33,5 +33,7 @@
[244, 11, 10, 9, 15, 0]
[65524, 11, 10, 9, 15, 0]
[4294967284, 11, 10, 9, 15, 0]
[18446744073709551604, 11, 10, 9, 15, 0]
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
[2147483636, 11, 10, 9, 15, 0]
[-2147483638, -11, -12, -9, -15, -2, 2147483637, 10, 11, 9, 0]

38
tests/idris2/basic055/BitOps.idr
View File

@ -260,23 +260,23 @@ xorBits32 = [ prim__xor_Bits32 11 b32max
, prim__xor_Bits32 11 11
]
-- xorBits64 : List Bits64
-- xorBits64 = [ prim__xor_Bits64 11 b64max
-- , prim__xor_Bits64 11 0
-- , prim__xor_Bits64 11 1
-- , prim__xor_Bits64 11 2
-- , prim__xor_Bits64 11 4
-- , prim__xor_Bits64 11 11
-- ]
--
-- xorInteger : List Integer
-- xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
-- , prim__xor_Integer 11 0
-- , prim__xor_Integer 11 1
-- , prim__xor_Integer 11 2
-- , prim__xor_Integer 11 4
-- , prim__xor_Integer 11 11
-- ]
xorBits64 : List Bits64
xorBits64 = [ prim__xor_Bits64 11 b64max
, prim__xor_Bits64 11 0
, prim__xor_Bits64 11 1
, prim__xor_Bits64 11 2
, prim__xor_Bits64 11 4
, prim__xor_Bits64 11 11
]
xorInteger : List Integer
xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
, prim__xor_Integer 11 0
, prim__xor_Integer 11 1
, prim__xor_Integer 11 2
, prim__xor_Integer 11 4
, prim__xor_Integer 11 11
]
xorInt : List Int
xorInt = [ prim__xor_Int 11 intmax
@ -349,7 +349,7 @@ main = do printLn shiftRBits8
printLn xorBits8
printLn xorBits16
printLn xorBits32
-- printLn xorBits64
-- printLn xorInteger
printLn xorBits64
printLn xorInteger
printLn xorInt
printLn xorNegativeInt

2
tests/idris2/basic055/expected
View File

@ -33,6 +33,8 @@
[244, 11, 10, 9, 15, 0]
[65524, 11, 10, 9, 15, 0]
[4294967284, 11, 10, 9, 15, 0]
[18446744073709551604, 11, 10, 9, 15, 0]
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
[2147483636, 11, 10, 9, 15, 0]
[-2147483638, -11, -12, -9, -15, -2, 2147483637, 10, 11, 9, 0]
1/1: Building BitOps (BitOps.idr)

38
tests/node/node024/BitOps.idr
View File

@ -260,23 +260,23 @@ xorBits32 = [ prim__xor_Bits32 11 b32max
, prim__xor_Bits32 11 11
]
-- xorBits64 : List Bits64
-- xorBits64 = [ prim__xor_Bits64 11 b64max
-- , prim__xor_Bits64 11 0
-- , prim__xor_Bits64 11 1
-- , prim__xor_Bits64 11 2
-- , prim__xor_Bits64 11 4
-- , prim__xor_Bits64 11 11
-- ]
--
-- xorInteger : List Integer
-- xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
-- , prim__xor_Integer 11 0
-- , prim__xor_Integer 11 1
-- , prim__xor_Integer 11 2
-- , prim__xor_Integer 11 4
-- , prim__xor_Integer 11 11
-- ]
xorBits64 : List Bits64
xorBits64 = [ prim__xor_Bits64 11 b64max
, prim__xor_Bits64 11 0
, prim__xor_Bits64 11 1
, prim__xor_Bits64 11 2
, prim__xor_Bits64 11 4
, prim__xor_Bits64 11 11
]
xorInteger : List Integer
xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
, prim__xor_Integer 11 0
, prim__xor_Integer 11 1
, prim__xor_Integer 11 2
, prim__xor_Integer 11 4
, prim__xor_Integer 11 11
]
xorInt : List Int
xorInt = [ prim__xor_Int 11 intmax
@ -349,7 +349,7 @@ main = do printLn shiftRBits8
printLn xorBits8
printLn xorBits16
printLn xorBits32
-- printLn xorBits64
-- printLn xorInteger
printLn xorBits64
printLn xorInteger
printLn xorInt
printLn xorNegativeInt

2
tests/node/node024/expected
View File

@ -33,6 +33,8 @@
[244, 11, 10, 9, 15, 0]
[65524, 11, 10, 9, 15, 0]
[4294967284, 11, 10, 9, 15, 0]
[18446744073709551604, 11, 10, 9, 15, 0]
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
[2147483636, 11, 10, 9, 15, 0]
[-2147483638, -11, -12, -9, -15, -2, 2147483637, 10, 11, 9, 0]
1/1: Building BitOps (BitOps.idr)

2
tests/ttimp/basic006/expected
View File

@ -2,5 +2,5 @@ Processing as TTImp
Written TTC
Yaffle> ((Main.Just [a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [k = Main.Z]) [a = Integer]) 1) (Main.Vect.Nil [a = Integer])))
Yaffle> ((Main.MkInfer [a = (Main.List.List Integer)]) (((Main.List.Cons [a = Integer]) 1) (Main.List.Nil [a = Integer])))
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved207 ?Main.{a:62}_[]), ($resolved187 ?Main.{a:62}_[])]
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved209 ?Main.{a:62}_[]), ($resolved189 ?Main.{a:62}_[])]
Yaffle> Bye for now!

2
tests/ttimp/coverage001/expected
View File

@ -2,7 +2,7 @@ Processing as TTImp
Written TTC
Yaffle> Bye for now!
Processing as TTImp
Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved203 {b:27}[1] {a:26}[0] $resolved185 ($resolved194 {a:26}[0]) ($resolved194 {b:27}[1])) is not a valid impossible pattern because it typechecks
Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved205 {b:27}[1] {a:26}[0] $resolved187 ($resolved196 {a:26}[0]) ($resolved196 {b:27}[1])) is not a valid impossible pattern because it typechecks
Yaffle> Bye for now!
Processing as TTImp
Vect3.yaff:25:1--26:1:Not a valid impossible pattern:

2
tests/ttimp/coverage002/expected
View File

@ -2,6 +2,6 @@ Processing as TTImp
Written TTC
Yaffle> Main.lookup: All cases covered
Yaffle> Main.lookup':
($resolved234 [__] [__] ($resolved200 [__]) {_:62})
($resolved236 [__] [__] ($resolved202 [__]) {_:62})
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
Yaffle> Bye for now!

6
tests/ttimp/dot001/expected
View File

@ -3,13 +3,13 @@ Written TTC
Yaffle> Bye for now!
Processing as TTImp
Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
Dot2.yaff:15:28--15:30:Pattern variable {P:n:189} unifies with ?{P:m:189}_[]
Dot2.yaff:15:28--15:30:Pattern variable {P:n:191} unifies with ?{P:m:191}_[]
Yaffle> Bye for now!
Processing as TTImp
Dot3.yaff:18:1--19:1:When elaborating left hand side of Main.addBaz3:
Dot3.yaff:18:10--18:15:Can't match on ($resolved181 ?{P:x:194}_[] ?{P:x:194}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved181 ?Main.{_:13}_[] ?Main.{_:14}_[])
Dot3.yaff:18:10--18:15:Can't match on ($resolved183 ?{P:x:196}_[] ?{P:x:196}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved183 ?Main.{_:13}_[] ?Main.{_:14}_[])
Yaffle> Bye for now!
Processing as TTImp
Dot4.yaff:17:1--18:1:When elaborating left hand side of Main.addBaz4:
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:196}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:198}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
Yaffle> Bye for now!