some bitwise ops corresponding to OPE ops
This commit is contained in:
parent
9e702dd03d
commit
b61ace9c7d
1 changed files with 36 additions and 1 deletions
|
@ -84,3 +84,38 @@ export
|
|||
halfDouble n with (half (n + n)) | (n + n) proof nn
|
||||
_ | HalfOdd k | S (k + k) = void $ notEvenOdd n k nn
|
||||
_ | HalfEven k | k + k = rewrite doubleInj n k nn in Refl
|
||||
|
||||
export
|
||||
floorHalf : Nat -> Nat
|
||||
floorHalf k = case half k of
|
||||
HalfOdd n => n
|
||||
HalfEven n => n
|
||||
|
||||
|
||||
||| like in intercal ☺
|
||||
|||
|
||||
||| take all the bits of `subj` that are set in `mask`, and squish them down
|
||||
||| towards the lsb
|
||||
export
|
||||
select : (mask, subj : Nat) -> Nat
|
||||
select mask subj = go 1 (halfRec mask) subj 0 where
|
||||
go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
|
||||
go bit HalfRecZ subj res = res
|
||||
go bit (HalfRecEven _ rec) subj res = go bit rec (floorHalf subj) res
|
||||
go bit (HalfRecOdd _ rec) subj res = case half subj of
|
||||
HalfOdd subj => go (bit + bit) rec subj (res + bit)
|
||||
HalfEven subj => go (bit + bit) rec subj res
|
||||
|
||||
||| take the i least significant bits of subj (where i = popCount mask),
|
||||
||| and place them where mask's set bits are
|
||||
|||
|
||||
||| left inverse of select if mask .|. subj = mask
|
||||
export
|
||||
spread : (mask, subj : Nat) -> Nat
|
||||
spread mask subj = go 1 (halfRec mask) subj 0 where
|
||||
go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
|
||||
go bit HalfRecZ subj res = res
|
||||
go bit (HalfRecEven _ rec) subj res = go (bit + bit) rec subj res
|
||||
go bit (HalfRecOdd _ rec) subj res = case half subj of
|
||||
HalfOdd subj => go (bit + bit) rec subj (res + bit)
|
||||
HalfEven subj => go (bit + bit) rec subj res
|
||||
|
|
Loading…
Reference in a new issue