opentheory-primitive 1.2 → 1.3

raw patch · 6 files changed

+60/−44 lines, 6 files

Files

• opentheory-primitive.cabal +3/−3
• src/OpenTheory/Primitive/Byte.hs +10/−6
• src/OpenTheory/Primitive/Natural.hs +8/−0
• src/OpenTheory/Primitive/Random.hs +2/−4
• testsrc/Main.hs +37/−0
• testsrc/Test.hs +0/−31

@@ -1,10 +1,10 @@ name: opentheory-primitive-version: 1.2+version: 1.3 category: Formal Methods synopsis: Haskell primitives used by OpenTheory packages license: MIT license-file: LICENSE-cabal-version: >= 1.8.0.6+cabal-version: >= 1.8.0.2 build-type: Simple author: Joe Leslie-Hurd <joe@gilith.com> maintainer: Joe Leslie-Hurd <joe@gilith.com>@@ -40,4 +40,4 @@    ghc-options: -Wall -  main-is: Test.hs+  main-is: Main.hs

@@ -15,23 +15,24 @@     not,     or,     shiftLeft,-    shiftRight )+    shiftRight,+    toNatural ) where  import Prelude (Bool, (<), (&&), fromIntegral) import qualified Data.Bits import qualified Data.Word-import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Natural as Natural  type Byte = Data.Word.Word8  and :: Byte -> Byte -> Byte and w1 w2 = (Data.Bits..&.) w1 w2 -bit :: Byte -> Primitive.Natural.Natural -> Bool+bit :: Byte -> Natural.Natural -> Bool bit w i = i < 8 && Data.Bits.testBit w (fromIntegral i) -fromNatural :: Primitive.Natural.Natural -> Byte+fromNatural :: Natural.Natural -> Byte fromNatural = fromIntegral  not :: Byte -> Byte@@ -40,10 +41,13 @@ or :: Byte -> Byte -> Byte or w1 w2 = (Data.Bits..|.) w1 w2 -shiftLeft :: Byte -> Primitive.Natural.Natural -> Byte+shiftLeft :: Byte -> Natural.Natural -> Byte shiftLeft w n =     if n < 8 then (Data.Bits.shiftL) w (fromIntegral n) else 0 -shiftRight :: Byte -> Primitive.Natural.Natural -> Byte+shiftRight :: Byte -> Natural.Natural -> Byte shiftRight w n =     if n < 8 then (Data.Bits.shiftR) w (fromIntegral n) else 0++toNatural :: Byte -> Natural.Natural+toNatural = fromIntegral

@@ -11,6 +11,8 @@   ( Natural ) where +import qualified Test.QuickCheck+ newtype Natural =     Natural { unNatural :: Integer }   deriving Eq@@ -67,3 +69,9 @@           in (Natural q, Natural r)    toInteger = unNatural++instance Test.QuickCheck.Arbitrary Natural where+  arbitrary = fmap fromRandomInteger Test.QuickCheck.arbitrary+      where+    fromRandomInteger x =+      Natural (if x < 0 then -(x + 1) else x)

@@ -28,10 +28,8 @@ instance Show Random where   show r = "Random<" ++ show (seed r) ++ ">" -bit :: Random -> (Bool,Random)-bit r =-  let (b,g) = System.Random.random (gen r) in-  (b, r {gen = g})+bit :: Random -> Bool+bit r = fst (System.Random.random (gen r))  split :: Random -> (Random,Random) split r =

@@ -0,0 +1,37 @@+{- |+Module: $Header$+Description: OpenTheory QuickCheck interface+License: MIT++Maintainer: Joe Leslie-Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++OpenTheory QuickCheck interface+-}+module Main+  ( main )+where++import OpenTheory.Primitive.Natural+import OpenTheory.Primitive.Test++assertion0 :: Bool+assertion0 = True++assertion1 :: Bool+assertion1 = (2 :: Natural) + 2 == 4++proposition0 :: Bool -> Bool+proposition0 p = p || not p++proposition1 :: Natural -> Natural -> Bool+proposition1 m n = m + n == n + m++main :: IO ()+main =+    do assert "Assertion 0:\n  T\n  " assertion0+       assert "Assertion 1:\n  2 + 2 = 4\n  " assertion1+       check "Proposition 0:\n  !p. p \\/ ~p\n  " proposition0+       check "Proposition 1:\n  !m n. m + n = n + m\n  " proposition1+       return ()

@@ -1,31 +0,0 @@-{- |-Module: $Header$-Description: OpenTheory QuickCheck interface-License: MIT--Maintainer: Joe Leslie-Hurd <joe@gilith.com>-Stability: provisional-Portability: portable--OpenTheory QuickCheck interface--}-module Main-  ( main )-where--import qualified OpenTheory.Primitive.Random as Primitive.Random-import qualified OpenTheory.Primitive.Test as Primitive.Test--assertion0 :: Bool-assertion0 = True--proposition0 :: Primitive.Random.Random -> Bool-proposition0 r =-  let (p,_) = Primitive.Random.bit r in-  p || not p--main :: IO ()-main =-    do Primitive.Test.assert "Assertion 0:\n  T\n  " assertion0-       Primitive.Test.check "Proposition 0:\n  !p. p \\/ ~p\n  " proposition0-       return ()