.agda

-- Type 

module Data.U64.Type where

open import Data.Nat.Type
open import Data.Bool.Type

-- Represents a 64-bit machine word.
postulate U64 : Set
{-# BUILTIN WORD64 U64 #-}

-- Primitive operations for U64.
primitive
  primWord64ToNat   : U64 → Nat
  primWord64FromNat : Nat → U64

-- div 
module Data.U64.div where

open import Data.U64.Type
open import Data.Bool.Type
open import Data.Nat.Type
open import Data.U64.if
open import Data.U64.lte
open import Data.U64.min

divU64 : U64 → U64 → U64
divU64 x y = primWord64FromNat (go (primWord64ToNat x) (primWord64ToNat y))
  where
    go : Nat → Nat → Nat
    go Zero _ = Zero
    go _ Zero = Zero  -- Handle division by zero
    go m n = if (lteU64 (primWord64FromNat m) (primWord64FromNat n) )
             Zero
             (Succ (go (primWord64ToNat (min (primWord64FromNat m) (primWord64FromNat n))) n))
    

-- mod 

module Data.U64.mod where

open import Data.U64.Type
open import Data.U64.div
open import Data.U64.mul
open import Data.U64.sub

modU64 : U64 → U64 → U64
modU64 a b = subU64 a (mulU64 b (divU64 a b))

-- if 

module Data.U64.if where 


open import Data.U64.Type 
open import Data.Bool.Type 
open import Data.Nat.Type

ifU64 : ∀ {a} {A : Set a} → U64 → A → A → A
ifU64 n t f = go (primWord64ToNat n) t f
  where 
   go :  ∀ {a} {A : Set a} → Nat → A → A → A 
   go Zero t f = f
   go (Succ _) t f = t
   

-- to bits 

module Data.U64.to-bits where

open import Data.U64.Type
open import Data.Bits.Type
open import Data.U64.mod
open import Data.U64.div
open import Data.U64.if
open import Data.Nat.Type
open import Data.Bool.Type

-- Helper function for to_bits that handles the recursive case.
-- - n: The remaining part of the U64 number to convert.
-- = The binary representation of the number as Bits.
{-# TERMINATING #-}
to-bits-helper : U64 → Bits
to-bits-helper n =
  let two = primWord64FromNat 2
      quotient = divU64 n two
      remainder = modU64 n two
  in ifU64 remainder
      (I (to-bits-helper quotient))
      (O (to-bits-helper quotient))

-- Converts a U64 number to its binary representation.
-- - n: The U64 number to convert.
-- = The binary representation of the number as Bits.
to-bits : U64 → Bits
to-bits n = 
  ifU64 n
    (to-bits-helper n)
    (O E)

--min 
module Data.U64.min where 

open import Data.U64.Type
open import Data.U64.lte
open import Data.U64.if

minU64 : U64 → U64 → U64
minU64 x y = if (lteU64 x y) x y

--lte

module Data.U64.lte where

open import Data.U64.Type
open import Data.Bool.Type
open import Data.Nat.Type

lteU64 : U64 → U64 → U64
lteU64 x y = go (primWord64ToNat x) (primWord64ToNat y)
  where
    go : Nat → Nat → U64
    go Zero Zero = primWord64FromNat 1
    go Zero (Succ _) = primWord64FromNat 1
    go (Succ _) Zero = primWord64FromNat 0
    go (Succ m) (Succ n) = go m n

--mul 
module Data.U64.mul where

open import Data.U64.Type
open import Data.Nat.mul

-- Multiplies two U64 values.
-- - a: The first U64 to multiply.
-- - b: The second U64 to multiply.
-- = The result of a * b, potentially wrapping around due to 64-bit limitation.
mulU64 : U64 → U64 → U64
mulU64 a b = primWord64FromNat (primWord64ToNat a * primWord64ToNat b)