opentheory-primitive 1.3 → 1.4
raw patch · 4 files changed
+88/−54 lines, 4 files
Files
- opentheory-primitive.cabal +6/−11
- src/OpenTheory/Primitive/Natural.hs +39/−6
- src/Test.hs +43/−0
- testsrc/Main.hs +0/−37
opentheory-primitive.cabal view
@@ -1,5 +1,5 @@ name: opentheory-primitive-version: 1.3+version: 1.4 category: Formal Methods synopsis: Haskell primitives used by OpenTheory packages license: MIT@@ -13,16 +13,13 @@ Prelude to provide the core execution platform assumed by Haskell packages exported from formally verified OpenTheory packages. -Library+library build-depends: base >= 4.0 && < 5.0, random >= 1.0.1.1 && < 2.0, QuickCheck >= 2.4.0.1 && < 3.0- hs-source-dirs: src- ghc-options: -Wall- exposed-modules: OpenTheory.Primitive.Byte OpenTheory.Primitive.Natural@@ -30,14 +27,12 @@ OpenTheory.Primitive.Word16 OpenTheory.Primitive.Test -Executable opentheory-primitive-test+test-suite opentheory-primitive-test+ type: exitcode-stdio-1.0 build-depends: base >= 4.0 && < 5.0, random >= 1.0.1.1 && < 2, QuickCheck >= 2.4.0.1 && < 3.0-- hs-source-dirs: src, testsrc-+ hs-source-dirs: src ghc-options: -Wall-- main-is: Main.hs+ main-is: Test.hs
src/OpenTheory/Primitive/Natural.hs view
@@ -8,21 +8,27 @@ portability: portable -} module OpenTheory.Primitive.Natural- ( Natural )+ ( Natural,+ shiftLeft,+ shiftRight ) where +import Data.Bits import qualified Test.QuickCheck newtype Natural = Natural { unNatural :: Integer }- deriving Eq+ deriving (Eq, Ord) -instance Show Natural where- show n = show (unNatural n)+shiftLeft :: Natural -> Natural -> Natural+shiftLeft (Natural x) k = Natural (shiftL x (fromIntegral k)) -instance Ord Natural where- compare x y = compare (unNatural x) (unNatural y)+shiftRight :: Natural -> Natural -> Natural+shiftRight (Natural x) k = Natural (shiftR x (fromIntegral k)) +instance Show Natural where+ show x = show (unNatural x)+ instance Num Natural where x + y = Natural (unNatural x + unNatural y) @@ -69,6 +75,33 @@ in (Natural q, Natural r) toInteger = unNatural++instance Data.Bits.Bits Natural where+ x .&. y = Natural (unNatural x .&. unNatural y)++ x .|. y = Natural (unNatural x .|. unNatural y)++ xor x y = Natural (xor (unNatural x) (unNatural y))++ complement _ = error "OpenTheory.Primitive.Natural.complement"++ shift x k = Natural (shift (unNatural x) k)++ shiftL x k = Natural (shiftL (unNatural x) k)++ shiftR x k = Natural (shiftR (unNatural x) k)++ rotate _ _ = error "OpenTheory.Primitive.Natural.rotate"++ bitSize _ = error "OpenTheory.Primitive.Natural.bitSize"++ isSigned _ = False++ testBit x k = testBit (unNatural x) k++ bit k = Natural (bit k)++ popCount x = popCount (unNatural x) instance Test.QuickCheck.Arbitrary Natural where arbitrary = fmap fromRandomInteger Test.QuickCheck.arbitrary
+ src/Test.hs view
@@ -0,0 +1,43 @@+{- |+Module: $Header$+Description: Testing the OpenTheory standard theory library+License: MIT++Maintainer: Joe Leslie-Hurd <joe@gilith.com>+Stability: provisional+Portability: portable+-}+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++proposition2 :: Natural -> Natural -> Bool+proposition2 n k = shiftLeft n k == (2 ^ k) * n++proposition3 :: Natural -> Natural -> Bool+proposition3 n k = shiftRight n k == n `div` (2 ^ k)++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+ check "Proposition 2:\n !n k. shiftLeft n k = 2 ^ k * n\n " proposition2+ check "Proposition 3:\n !n k. shiftRight n k = n div 2 ^ k\n " proposition3+ return ()
− testsrc/Main.hs
@@ -1,37 +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 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 ()