@@ -32,7 +32,7 @@ bitsUsed n = 8 * (2 `power` n)
32%assert_total
32%assert_total
33natToBits' : machineTy n -> Nat -> machineTy n
33natToBits' : machineTy n -> Nat -> machineTy n
34natToBits' a Z = a
34natToBits' a Z = a
35−natToBits' {n=n} a x with n
35+natToBits' {n=n} a x with (n)
36 -- it seems I have to manually recover the value of n here, instead of being able to reference it
36 -- it seems I have to manually recover the value of n here, instead of being able to reference it
37 natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
37 natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
38 natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
38 natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
@@ -40,7 +40,7 @@ natToBits' {n=n} a x with n
40 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
40 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
42natToBits : Nat -> machineTy n
42natToBits : Nat -> machineTy n
43−natToBits {n=n} x with n
43+natToBits {n=n} x with (n)
44 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
44 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
45 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
45 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
46 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
46 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
@@ -106,7 +106,7 @@ shiftLeft : Bits n -> Bits n -> Bits n
106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
108shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
108shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
109−shiftRightLogical' {n=n} x c with n
109+shiftRightLogical' {n=n} x c with (n)
110 | Z = prim__lshrB8 x c
110 | Z = prim__lshrB8 x c
111 | S Z = prim__lshrB16 x c
111 | S Z = prim__lshrB16 x c
112 | S (S Z) = prim__lshrB32 x c
112 | S (S Z) = prim__lshrB32 x c
@@ -129,7 +129,7 @@ shiftRightArithmetic : Bits n -> Bits n -> Bits n
129shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
129shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
131and' : machineTy n -> machineTy n -> machineTy n
131and' : machineTy n -> machineTy n -> machineTy n
132−and' {n=n} x y with n
132+and' {n=n} x y with (n)
133 | Z = prim__andB8 x y
133 | Z = prim__andB8 x y
134 | S Z = prim__andB16 x y
134 | S Z = prim__andB16 x y
135 | S (S Z) = prim__andB32 x y
135 | S (S Z) = prim__andB32 x y
@@ -140,7 +140,7 @@ and : Bits n -> Bits n -> Bits n
140and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
140and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
142or' : machineTy n -> machineTy n -> machineTy n
142or' : machineTy n -> machineTy n -> machineTy n
143−or' {n=n} x y with n
143+or' {n=n} x y with (n)
144 | Z = prim__orB8 x y
144 | Z = prim__orB8 x y
145 | S Z = prim__orB16 x y
145 | S Z = prim__orB16 x y
146 | S (S Z) = prim__orB32 x y
146 | S (S Z) = prim__orB32 x y
@@ -151,7 +151,7 @@ or : Bits n -> Bits n -> Bits n
151or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
151or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
153xor' : machineTy n -> machineTy n -> machineTy n
153xor' : machineTy n -> machineTy n -> machineTy n
154−xor' {n=n} x y with n
154+xor' {n=n} x y with (n)
155 | Z = prim__xorB8 x y
155 | Z = prim__xorB8 x y
156 | S Z = prim__xorB16 x y
156 | S Z = prim__xorB16 x y
157 | S (S Z) = prim__xorB32 x y
157 | S (S Z) = prim__xorB32 x y