opentheory (empty) → 1.61

raw patch · 17 files changed

+413/−0 lines, 17 filesdep +QuickCheckdep +basedep +opentheory-primitivesetup-changed

Dependencies added: QuickCheck, base, opentheory-primitive, random

Files

• LICENSE +17/−0
• Setup.hs +6/−0
• opentheory.cabal +52/−0
• src/OpenTheory/Data/Byte.hs +23/−0
• src/OpenTheory/Data/Byte/Bits.hs +19/−0
• src/OpenTheory/Data/List.hs +35/−0
• src/OpenTheory/Data/List/Geometric.hs +23/−0
• src/OpenTheory/Data/Option.hs +18/−0
• src/OpenTheory/Data/Stream.hs +19/−0
• src/OpenTheory/Data/Word16.hs +24/−0
• src/OpenTheory/Data/Word16/Bits.hs +19/−0
• src/OpenTheory/Number/Natural.hs +31/−0
• src/OpenTheory/Number/Natural/Bits.hs +20/−0
• src/OpenTheory/Number/Natural/Geometric.hs +27/−0
• src/OpenTheory/Number/Natural/Uniform.hs +33/−0
• src/OpenTheory/Probability/Random.hs +20/−0
• testsrc/Test.hs +27/−0

@@ -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.

@@ -0,0 +1,6 @@+module Main(main)++import Distribution.Simple++main :: IO ()+main = defaultMain

@@ -0,0 +1,52 @@+name: opentheory+version: 1.61+category: Formal Methods+synopsis: The Haskell base+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 Haskell base+  Automatically generated from the opentheory package haskell-1.61++library+  build-depends:+    base >= 4.0 && < 5.0,+    random >= 1.0.1.1 && < 2.0,+    QuickCheck >= 2.4.0.1 && < 3.0,+    opentheory-primitive >= 1.0 && < 2.0++  hs-source-dirs: src++  ghc-options: -Wall++  exposed-modules:+    OpenTheory.Data.Byte+    OpenTheory.Data.Byte.Bits+    OpenTheory.Data.List+    OpenTheory.Data.List.Geometric+    OpenTheory.Data.Option+    OpenTheory.Data.Stream+    OpenTheory.Data.Word16+    OpenTheory.Data.Word16.Bits+    OpenTheory.Number.Natural+    OpenTheory.Number.Natural.Bits+    OpenTheory.Number.Natural.Geometric+    OpenTheory.Number.Natural.Uniform+    OpenTheory.Probability.Random++executable opentheory-test+  build-depends:+    base >= 4.0 && < 5.0,+    random >= 1.0.1.1 && < 2.0,+    QuickCheck >= 2.4.0.1 && < 3.0,+    opentheory-primitive >= 1.0 && < 2.0++  hs-source-dirs: src, testsrc++  ghc-options: -Wall++  main-is: Test.hs

@@ -0,0 +1,23 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Byte+where++import qualified OpenTheory.Data.Byte.Bits as Bits+import qualified OpenTheory.Primitive.Byte as Primitive.Byte+import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Probability.Random as Probability.Random++fromRandom ::+  Primitive.Random.Random -> (Primitive.Byte.Byte, Primitive.Random.Random)+fromRandom r =+  let (r1, r2) = Primitive.Random.split r in+  let (l, _) = Probability.Random.bits 8 r1 in+  (Bits.toByte l, r2)

@@ -0,0 +1,19 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Byte.Bits+where++import qualified OpenTheory.Primitive.Byte as Primitive.Byte++toByte :: [Bool] -> Primitive.Byte.Byte+toByte [] = 0+toByte (h : t) =+  if h then Primitive.Byte.shiftLeft (toByte t) 1 + 1+  else Primitive.Byte.shiftLeft (toByte t) 1

@@ -0,0 +1,35 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.List+where++import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random++fromRandom ::+  (Primitive.Random.Random -> (a, Primitive.Random.Random)) ->+    Primitive.Natural.Natural -> Primitive.Random.Random ->+    ([a], Primitive.Random.Random)+fromRandom d n r =+  if n == 0 then ([], r)+  else+    let (h, r') = d r in+    let (t, r'') = fromRandom d (n - 1) r' in+    (h : t, r'')++equal :: (a -> a -> Bool) -> [a] -> [a] -> Bool+equal _ [] [] = True+equal _ [] (_ : _) = False+equal _ (_ : _) [] = False+equal eq (h1 : t1) (h2 : t2) = eq h1 h2 && equal eq t1 t2++size :: [a] -> Primitive.Natural.Natural+size [] = 0+size (_ : t) = 1 + size t

@@ -0,0 +1,23 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.List.Geometric+where++import qualified OpenTheory.Data.List as Data.List+import qualified OpenTheory.Number.Natural.Geometric+  as Number.Natural.Geometric+import qualified OpenTheory.Primitive.Random as Primitive.Random++fromRandom ::+  (Primitive.Random.Random -> (a, Primitive.Random.Random)) ->+    Primitive.Random.Random -> ([a], Primitive.Random.Random)+fromRandom d r =+  let (n, r') = Number.Natural.Geometric.fromRandom r in+  Data.List.fromRandom d n r'

@@ -0,0 +1,18 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Option+where+++equal :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool+equal _ Nothing Nothing = True+equal _ Nothing (Just _) = False+equal _ (Just _) Nothing = False+equal eq (Just x1) (Just x2) = eq x1 x2

@@ -0,0 +1,19 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Stream+where++import qualified OpenTheory.Primitive.Natural as Primitive.Natural++nth :: [a] -> Primitive.Natural.Natural -> a+nth s n = if n == 0 then head s else nth (tail s) (n - 1)++unfold :: (b -> (a, b)) -> b -> [a]+unfold f b = let (a, b') = f b in a : unfold f b'

@@ -0,0 +1,24 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Word16+where++import qualified OpenTheory.Data.Word16.Bits as Bits+import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Primitive.Word16 as Primitive.Word16+import qualified OpenTheory.Probability.Random as Probability.Random++fromRandom ::+  Primitive.Random.Random ->+    (Primitive.Word16.Word16, Primitive.Random.Random)+fromRandom r =+  let (r1, r2) = Primitive.Random.split r in+  let (l, _) = Probability.Random.bits 16 r1 in+  (Bits.toWord16 l, r2)

@@ -0,0 +1,19 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Data.Word16.Bits+where++import qualified OpenTheory.Primitive.Word16 as Primitive.Word16++toWord16 :: [Bool] -> Primitive.Word16.Word16+toWord16 [] = 0+toWord16 (h : t) =+  if h then Primitive.Word16.shiftLeft (toWord16 t) 1 + 1+  else Primitive.Word16.shiftLeft (toWord16 t) 1

@@ -0,0 +1,31 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Number.Natural+where++import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random++fromRandom ::+  Primitive.Random.Random ->+    (Primitive.Natural.Natural, Primitive.Random.Random)+fromRandom =+  \r ->+    let (r1, r2) = Primitive.Random.split r in+    (dest False 0 1 0 r1 - 1, r2)+  where+  {-dest ::+        Bool -> Primitive.Natural.Natural -> Primitive.Natural.Natural ->+          Primitive.Natural.Natural -> Primitive.Random.Random ->+          Primitive.Natural.Natural-}+    dest b n f p r =+      let (b', r') = Primitive.Random.bit r in+      if b' && b then n+      else let s = f + p in dest b' (if b' then s + n else n) s f r'

@@ -0,0 +1,20 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Number.Natural.Bits+where++import qualified OpenTheory.Primitive.Natural as Primitive.Natural++toNatural :: [Bool] -> Primitive.Natural.Natural+toNatural [] = 0+toNatural (h : t) = 2 * toNatural t + if h then 1 else 0++width :: Primitive.Natural.Natural -> Primitive.Natural.Natural+width n = if n == 0 then 0 else width (n `div` 2) + 1

@@ -0,0 +1,27 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Number.Natural.Geometric+where++import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random++fromRandom ::+  Primitive.Random.Random ->+    (Primitive.Natural.Natural, Primitive.Random.Random)+fromRandom =+  \r -> let (r1, r2) = Primitive.Random.split r in (loop 0 r1, r2)+  where+  {-loop ::+        Primitive.Natural.Natural -> Primitive.Random.Random ->+          Primitive.Natural.Natural-}+    loop n r =+      let (b, r') = Primitive.Random.bit r in+      if b then n else loop (n + 1) r'

@@ -0,0 +1,33 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Number.Natural.Uniform+where++import qualified OpenTheory.Number.Natural.Bits as Number.Natural.Bits+import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Probability.Random as Probability.Random++fromRandom ::+  Primitive.Natural.Natural -> Primitive.Random.Random ->+    (Primitive.Natural.Natural, Primitive.Random.Random)+fromRandom n =+  \r ->+    let w = Number.Natural.Bits.width (n - 1) in+    let (r1, r2) = Primitive.Random.split r in+    (loop w r1 `mod` n, r2)+  where+  {-loop ::+        Primitive.Natural.Natural -> Primitive.Random.Random ->+          Primitive.Natural.Natural-}+    loop w r =+      let (l, r') = Probability.Random.bits w r in+      let m = Number.Natural.Bits.toNatural l in+      if m < n then m else loop w r'

@@ -0,0 +1,20 @@+{- |+module: $Header$+description: The Haskell base+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Probability.Random+where++import qualified OpenTheory.Data.List as Data.List+import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random++bits ::+  Primitive.Natural.Natural -> Primitive.Random.Random ->+    ([Bool], Primitive.Random.Random)+bits = Data.List.fromRandom Primitive.Random.bit

@@ -0,0 +1,27 @@+{- |+module: Main+description: The Haskell base - testing+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module Main+  ( main )+where++import qualified OpenTheory.Number.Natural as Number.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Primitive.Test as Primitive.Test++proposition0 :: Primitive.Random.Random -> Bool+proposition0 r =+  let (n1, r') = Number.Natural.fromRandom r in+  let (n2, _) = Number.Natural.fromRandom r' in+  not (n1 == n2) || n2 == n1++main :: IO ()+main =+    do Primitive.Test.check "Proposition 0:\n  !r.\n    let (n1, r') <- H.fromRandom r in\n    let (n2, r'') <- H.fromRandom r' in\n    ~(n1 = n2) \\/ n2 = n1\n  " proposition0+       return ()