<commit_before>{-# LANGUAGE CPP #-}

{- |
Module      : Verifier.SAW.Prim
Copyright   : Galois, Inc. 2012-2014
License     : BSD3
Maintainer  : <EMAIL>
Stability   : experimental
Portability : non-portable (language extensions)
-}

module Verifier.SAW.Prim where

import Control.Applicative
import Control.Exception (assert)
import Data.Bits
import Data.Vector ( Vector )
import qualified Data.Vector as V

------------------------------------------------------------
-- Natural numbers

-- | A natural number.
newtype Nat = Nat { unNat :: Integer }
  deriving (Eq,Ord)

instance Show Nat where
  show (Nat x) = show x

instance Num Nat where
  Nat x + Nat y = Nat (x + y)
  Nat x * Nat y = Nat (x * y)
  Nat x - Nat y | r >= 0 = Nat r
                | otherwise = error "internal: Nat subtraction result must be non-negative."
    where r = x - y

  negate (Nat 0) = Nat 0
  negate _ = error "Nat negation is upsupported."

  abs = id

  signum (Nat 0) = 0
  signum (Nat _) = 1

  fromInteger r | r >= 0 = Nat r
                | otherwise = error "internal: Natural numbers must be non-negative."

instance Enum Nat where
  succ (Nat x) = Nat (succ x)
  pred (Nat 0) = error "Nat 0 has no predecessor."
  pred (Nat x) = Nat (pred x)

  toEnum   = fromIntegral
  fromEnum = fromIntegral

  enumFrom       (Nat x)                 = Nat <$> enumFrom x
  enumFromThen   (Nat x) (Nat y)         = Nat <$> enumFromThen x y
  enumFromTo     (Nat x)         (Nat z) = Nat <$> enumFromTo x z
  enumFromThenTo (Nat x) (Nat y) (Nat z) = Nat <$> enumFromThenTo x y z


instance Real Nat where
  toRational (Nat x) = toRational x

instance Integral Nat where
  Nat x `quotRem` Nat y | y == 0 = error "Nat division by zero."
                        | otherwise = (Nat q, Nat r)
    where (q,r) = x `quotRem` y
  divMod = quotRem
  toInteger (Nat x) = x  

instance Bits Nat where
  Nat x .&. Nat y   = Nat (x .&. y)
  Nat x .|. Nat y   = Nat (x .|. y)
  Nat x `xor` Nat y = Nat (x `xor` y)

  complement = error "complement(Nat) unsupported."
  Nat x `shift` i = Nat (x `shift` i)

  rotate = shift

  bit = Nat . bit
  Nat x `setBit` i = Nat (x `setBit` i)

  Nat x `clearBit` i = Nat (x `clearBit` i)

  complementBit (Nat x) i = Nat (x `complementBit` i)

  testBit (Nat x) i = testBit x i

  bitSize = error "bitSize(Nat) unsupported."
  bitSizeMaybe _ = Nothing

  isSigned _ = False

#if MIN_VERSION_base(4,6,0)
  popCount (Nat x) = popCount x
#endif

-- | width(n) = 1 + floor(log_2(n))
widthNat :: Nat -> Nat
widthNat 0 = 0
widthNat n = 1 + widthNat (n `div` 2)

------------------------------------------------------------
-- Finite indices

data Fin = FinVal { finVal :: !Nat, finRem :: Nat }
    deriving (Eq, Show)

finFromBound :: Nat -> Nat -> Fin
finFromBound i n
  | i < n = FinVal i (pred (n - i))
  | otherwise = error "finFromBound given out-of-range index."
                                                                                  
finSize :: Fin -> Nat<commit_msg>Compile on older 'base'<commit_after>{-# LANGUAGE CPP #-}

{- |
Module      : Verifier.SAW.Prim
Copyright   : Galois, Inc. 2012-2014
License     : BSD3
Maintainer  : <EMAIL>
Stability   : experimental
Portability : non-portable (language extensions)
-}

module Verifier.SAW.Prim where

import Control.Applicative
import Control.Exception (assert)
import Data.Bits
import Data.Vector ( Vector )
import qualified Data.Vector as V

------------------------------------------------------------
-- Natural numbers

-- | A natural number.
newtype Nat = Nat { unNat :: Integer }
  deriving (Eq,Ord)

instance Show Nat where
  show (Nat x) = show x

instance Num Nat where
  Nat x + Nat y = Nat (x + y)
  Nat x * Nat y = Nat (x * y)
  Nat x - Nat y | r >= 0 = Nat r
                | otherwise = error "internal: Nat subtraction result must be non-negative."
    where r = x - y

  negate (Nat 0) = Nat 0
  negate _ = error "Nat negation is upsupported."

  abs = id

  signum (Nat 0) = 0
  signum (Nat _) = 1

  fromInteger r | r >= 0 = Nat r
                | otherwise = error "internal: Natural numbers must be non-negative."

instance Enum Nat where
  succ (Nat x) = Nat (succ x)
  pred (Nat 0) = error "Nat 0 has no predecessor."
  pred (Nat x) = Nat (pred x)

  toEnum   = fromIntegral
  fromEnum = fromIntegral

  enumFrom       (Nat x)                 = Nat <$> enumFrom x
  enumFromThen   (Nat x) (Nat y)         = Nat <$> enumFromThen x y
  enumFromTo     (Nat x)         (Nat z) = Nat <$> enumFromTo x z
  enumFromThenTo (Nat x) (Nat y) (Nat z) = Nat <$> enumFromThenTo x y z


instance Real Nat where
  toRational (Nat x) = toRational x

instance Integral Nat where
  Nat x `quotRem` Nat y | y == 0 = error "Nat division by zero."
                        | otherwise = (Nat q, Nat r)
    where (q,r) = x `quotRem` y
  divMod = quotRem
  toInteger (Nat x) = x  

instance Bits Nat where
  Nat x .&. Nat y   = Nat (x .&. y)
  Nat x .|. Nat y   = Nat (x .|. y)
  Nat x `xor` Nat y = Nat (x `xor` y)

  complement = error "complement(Nat) unsupported."
  Nat x `shift` i = Nat (x `shift` i)

  rotate = shift

  bit = Nat . bit
  Nat x `setBit` i = Nat (x `setBit` i)

  Nat x `clearBit` i = Nat (x `clearBit` i)

  complementBit (Nat x) i = Nat (x `complementBit` i)

  testBit (Nat x) i = testBit x i

  bitSize = error "bitSize(Nat) unsupported."

#if MIN_VERSION_base(4,7,0)
  bitSizeMaybe _ = Nothing
#endif

  isSigned _ = False

#if MIN_VERSION_base(4,6,0)
  popCount (Nat x) = popCount x
#endif

-- | width(n) = 1 + floor(log_2(n))
widthNat :: Nat -> Nat
widthNat 0 = 0
widthNat n = 1 + widthNat (n `div` 2)

------------------------------------------------------------
-- Finite indices

data Fin = FinVal { finVal :: !Nat, finRem :: Nat }
    deriving (Eq, Show)

finFromBound :: Nat -> Nat -> Fin
finFromBound i n
  | i < n = FinVal i (pred (n - i))
  | otherwise = error "finFromBound given out-of-range index."
                                                                                  
finSize :: Fin -> Nat
{'fraction_non_alphanumeric': 0.15003326679973386, 'fraction_numerical': 0.009813705921490353, 'mean_word_length': 1.997507477567298, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2099173', 'n_tokens_mistral': 2142, 'n_tokens_neox': 1978, 'n_words': 763}