From b61ace9c7d7620085dd553136a05c54f0408468a Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 5 Jun 2023 16:41:40 +0200 Subject: [PATCH] some bitwise ops corresponding to OPE ops --- lib/Quox/NatExtra.idr | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/lib/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr index b9635ee..efa6e72 100644 --- a/lib/Quox/NatExtra.idr +++ b/lib/Quox/NatExtra.idr @@ -82,5 +82,40 @@ doubleInj (S m) (S n) prf = export 0 halfDouble : (n : Nat) -> half (n + n) = HalfEven n halfDouble n with (half (n + n)) | (n + n) proof nn - _ | HalfOdd k | S (k + k) = void $ notEvenOdd n k 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