packages feed

opentheory-primitive (empty) → 1.0

raw patch · 9 files changed

+346/−0 lines, 9 filesdep +QuickCheckdep +basedep +randomsetup-changed

Dependencies added: QuickCheck, base, random

Files

+ LICENSE view
@@ -0,0 +1,17 @@+Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN+THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main(main)++import Distribution.Simple++main :: IO ()+main = defaultMain
+ opentheory-primitive.cabal view
@@ -0,0 +1,43 @@+Name: opentheory-primitive+Version: 1.0+Category: Formal Methods+Synopsis: Haskell primitives used by OpenTheory packages+License: MIT+License-file: LICENSE+Cabal-version: >= 1.8.0.6+Build-type: Simple+Author: Joe Hurd <joe@gilith.com>+Maintainer: Joe Hurd <joe@gilith.com>+Description:+  The types and values defined in this package extend those in the+  Prelude to provide the core execution platform assumed by Haskell+  packages exported from formally verified OpenTheory packages.++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+    OpenTheory.Primitive.Random+    OpenTheory.Primitive.Word16+    OpenTheory.Primitive.Test++Executable opentheory-primitive-test+  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++  ghc-options: -Wall++  Main-is: Test.hs
+ src/OpenTheory/Primitive/Byte.hs view
@@ -0,0 +1,51 @@+{- |+Module: $Header$+Description: Byte primitive functions+License: MIT++Maintainer: Joe Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++Byte primitive functions+-}+module OpenTheory.Primitive.Byte+  ( Byte,+    and,+    bit,+    fromNatural,+    not,+    or,+    shiftLeft,+    shiftRight )+where++import Prelude (Bool, (<), (&&), fromIntegral)+import qualified Data.Bits+import qualified Data.Word+import qualified OpenTheory.Primitive.Natural as Primitive.Natural++type Byte = Data.Word.Word8++and :: Byte -> Byte -> Byte+and w1 w2 = (Data.Bits..&.) w1 w2++bit :: Byte -> Primitive.Natural.Natural -> Bool+bit w i = i < 8 && Data.Bits.testBit w (fromIntegral i)++fromNatural :: Primitive.Natural.Natural -> Byte+fromNatural = fromIntegral++not :: Byte -> Byte+not w = (Data.Bits.complement) w++or :: Byte -> Byte -> Byte+or w1 w2 = (Data.Bits..|.) w1 w2++shiftLeft :: Byte -> Primitive.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 w n =+    if n < 8 then (Data.Bits.shiftR) w (fromIntegral n) else 0
+ src/OpenTheory/Primitive/Natural.hs view
@@ -0,0 +1,71 @@+{- |+Module: $Header$+Description: A natural number type+License: MIT++Maintainer: Joe Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++A natural number type+-}+module OpenTheory.Primitive.Natural+  ( Natural )+where++newtype Natural =+    Natural { unNatural :: Integer }+  deriving Eq++instance Show Natural where+  show n = show (unNatural n)++instance Ord Natural where+  compare x y = compare (unNatural x) (unNatural y)++instance Num Natural where+  x + y = Natural (unNatural x + unNatural y)++  x - y =+      if x < y+        then error "OpenTheory.Primitive.Natural.-"+        else Natural (unNatural x - unNatural y)++  x * y = Natural (unNatural x * unNatural y)++  abs x = x++  signum x = if unNatural x == 0 then x else Natural 1++  fromInteger x =+      if x < 0+        then error "OpenTheory.Primitive.Natural.fromInteger"+        else Natural x++instance Real Natural where+  toRational x = toRational (unNatural x)++instance Enum Natural where+  toEnum x =+      if x < 0+        then error "OpenTheory.Primitive.Natural.toEnum"+        else Natural (toEnum x)++  fromEnum x = fromEnum (unNatural x)++instance Integral Natural where+  divMod x y =+      if y == 0+        then error "OpenTheory.Primitive.Natural.divMod"+        else+          let (d,m) = divMod (unNatural x) (unNatural y)+          in (Natural d, Natural m)++  quotRem x y =+      if y == 0+        then error "OpenTheory.Primitive.Natural.quotRem"+        else+          let (q,r) = quotRem (unNatural x) (unNatural y)+          in (Natural q, Natural r)++  toInteger = unNatural
+ src/OpenTheory/Primitive/Random.hs view
@@ -0,0 +1,47 @@+{- |+Module: $Header$+Description: Random stream primitives+License: MIT++Maintainer: Joe Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++Random stream primitives+-}+module OpenTheory.Primitive.Random+  ( Random,+    bit,+    split,+    fromInt )+where++import qualified System.Random+import qualified Test.QuickCheck++data Random =+    Random+      { seed :: Int,+        gen :: System.Random.StdGen }++instance Test.QuickCheck.Arbitrary Random where+  arbitrary = fmap fromInt Test.QuickCheck.arbitrary++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})++split :: Random -> (Random,Random)+split r =+  let (g1,g2) = System.Random.split (gen r) in+  (r {gen = g1}, r {gen = g2})++fromInt :: Int -> Random+fromInt i =+    Random+      {seed = i,+       gen = System.Random.mkStdGen i}
+ src/OpenTheory/Primitive/Test.hs view
@@ -0,0 +1,24 @@+{- |+Module: $Header$+Description: OpenTheory QuickCheck interface+License: MIT++Maintainer: Joe Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++OpenTheory QuickCheck interface+-}+module OpenTheory.Primitive.Test+  ( check )+where++import Test.QuickCheck++checkArgs :: Test.QuickCheck.Args+checkArgs = Test.QuickCheck.stdArgs { maxSuccess = 100 }++check :: Testable prop => String -> prop -> IO ()+check desc prop =+  do putStr desc+     Test.QuickCheck.quickCheckWith checkArgs prop
+ src/OpenTheory/Primitive/Word16.hs view
@@ -0,0 +1,60 @@+{- |+Module: $Header$+Description: Word16 primitive functions+License: MIT++Maintainer: Joe Hurd <joe@gilith.com>+Stability: provisional+Portability: portable++Word16 primitive functions+-}+module OpenTheory.Primitive.Word16+  ( Word16,+    and,+    bit,+    fromBytes,+    fromNatural,+    not,+    or,+    shiftLeft,+    shiftRight,+    toBytes )+where++import Prelude (Bool, (<), (&&), fromIntegral)+import qualified Data.Bits+import qualified Data.Word+import qualified OpenTheory.Primitive.Byte as Primitive.Byte+import qualified OpenTheory.Primitive.Natural as Primitive.Natural++type Word16 = Data.Word.Word16++and :: Word16 -> Word16 -> Word16+and w1 w2 = (Data.Bits..&.) w1 w2++bit :: Word16 -> Primitive.Natural.Natural -> Bool+bit w i = i < 16 && Data.Bits.testBit w (fromIntegral i)++fromBytes :: Primitive.Byte.Byte -> Primitive.Byte.Byte -> Word16+fromBytes b0 b1 = or (fromIntegral b0) (shiftLeft (fromIntegral b1) 8)++fromNatural :: Primitive.Natural.Natural -> Word16+fromNatural = fromIntegral++not :: Word16 -> Word16+not w = (Data.Bits.complement) w++or :: Word16 -> Word16 -> Word16+or w1 w2 = (Data.Bits..|.) w1 w2++shiftLeft :: Word16 -> Primitive.Natural.Natural -> Word16+shiftLeft w n =+    if n < 16 then (Data.Bits.shiftL) w (fromIntegral n) else 0++shiftRight :: Word16 -> Primitive.Natural.Natural -> Word16+shiftRight w n =+    if n < 16 then (Data.Bits.shiftR) w (fromIntegral n) else 0++toBytes :: Word16 -> (Primitive.Byte.Byte,Primitive.Byte.Byte)+toBytes w = (fromIntegral w, fromIntegral (shiftRight w 8))
+ testsrc/Test.hs view
@@ -0,0 +1,27 @@+{- |+Module: $Header$+Description: OpenTheory QuickCheck interface+License: MIT++Maintainer: Joe 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++proposition0 :: Primitive.Random.Random -> Bool+proposition0 r =+  let (p,_) = Primitive.Random.bit r in+  p || not p++main :: IO ()+main =+    do Primitive.Test.check "Proposition 0:\n  !p. p \\/ ~p\n  " proposition0+       return ()