packages feed

opentheory 1.76 → 1.195

raw patch · 18 files changed

+79/−371 lines, 18 filesdep −randomdep ~opentheory-primitive

Dependencies removed: random

Dependency ranges changed: opentheory-primitive

Files

opentheory.cabal view
@@ -1,52 +1,39 @@ name: opentheory-version: 1.76+version: 1.195 category: Formal Methods-synopsis: The Haskell base+synopsis: The standard theory library 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> description:-  The Haskell base - automatically generated from the opentheory package-  haskell-1.76+  The standard theory library - this package was automatically generated+  from the OpenTheory package base-1.195  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+    opentheory-primitive >= 1.3 && < 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+    OpenTheory.List+    OpenTheory.Natural  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+    opentheory-primitive >= 1.3 && < 2.0    hs-source-dirs: src, testsrc    ghc-options: -Wall -  main-is: Test.hs+  main-is: Main.hs
− src/OpenTheory/Data/Byte.hs 
@@ -1,23 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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)
− src/OpenTheory/Data/Byte/Bits.hs 
@@ -1,19 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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
− src/OpenTheory/Data/List.hs 
@@ -1,35 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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--length' :: [a] -> Primitive.Natural.Natural-length' [] = 0-length' (_ : t) = 1 + length' t
− src/OpenTheory/Data/List/Geometric.hs 
@@ -1,23 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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'
− src/OpenTheory/Data/Option.hs 
@@ -1,18 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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
− src/OpenTheory/Data/Stream.hs 
@@ -1,22 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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)--take' :: [a] -> Primitive.Natural.Natural -> [a]-take' s n = if n == 0 then [] else head s : take' (tail s) (n - 1)--unfold :: (b -> (a, b)) -> b -> [a]-unfold f b = let (a, b') = f b in a : unfold f b'
− src/OpenTheory/Data/Word16.hs 
@@ -1,24 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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)
− src/OpenTheory/Data/Word16/Bits.hs 
@@ -1,19 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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
+ src/OpenTheory/List.hs view
@@ -0,0 +1,18 @@+{- |+module: $Header$+description: The standard theory library+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}++module OpenTheory.List+where++import qualified OpenTheory.Primitive.Natural as Natural++naturalLength :: [a] -> Natural.Natural+naturalLength [] = 0+naturalLength (_ : t) = naturalLength t + 1
+ src/OpenTheory/Natural.hs view
@@ -0,0 +1,20 @@+{- |+module: $Header$+description: The standard theory library+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}++module OpenTheory.Natural+where++import qualified OpenTheory.Primitive.Natural as Natural++naturalEven :: Natural.Natural -> Bool+naturalEven n = n `mod` 2 == 0++naturalOdd :: Natural.Natural -> Bool+naturalOdd n = not (naturalEven n)
− src/OpenTheory/Number/Natural.hs 
@@ -1,34 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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--divides :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool-divides m n = if m == 0 then n == 0 else n `mod` m == 0--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'
− src/OpenTheory/Number/Natural/Bits.hs 
@@ -1,20 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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
− src/OpenTheory/Number/Natural/Geometric.hs 
@@ -1,27 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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'
− src/OpenTheory/Number/Natural/Uniform.hs 
@@ -1,33 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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'
− src/OpenTheory/Probability/Random.hs 
@@ -1,20 +0,0 @@-{- |-module: $Header$-description: The Haskell base-license: MIT--maintainer: Joe Leslie-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
+ testsrc/Main.hs view
@@ -0,0 +1,31 @@+{- |+module: Main+description: The standard theory library - testing+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module Main+  ( main )+where++import qualified Data.Maybe as Maybe+import OpenTheory.Primitive.Test++proposition0 :: Maybe Bool -> Bool+proposition0 x = not (Maybe.isJust x == Maybe.isNothing x)++proposition1 :: Bool -> Bool -> Bool+proposition1 a b = not (Left a == Right b)++proposition2 :: [(Bool, Bool)] -> Bool+proposition2 l = (let (x, y) = unzip l in zip x y) == l++main :: IO ()+main =+    do check "Proposition 0:\n  !x. ~(isSome x <=> isNone x)\n  " proposition0+       check "Proposition 1:\n  !a b. ~(left a = right b)\n  " proposition1+       check "Proposition 2:\n  !l. (let (x, y) <- unzip l in zip x y) = l\n  " proposition2+       return ()
− testsrc/Test.hs 
@@ -1,31 +0,0 @@-{- |-module: Main-description: The Haskell base - testing-license: MIT--maintainer: Joe Leslie-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--assertion0 :: Bool-assertion0 = 2 + 2 == 4--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.assert "Assertion 0:\n  2 + 2 = 4\n  " assertion0-       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 ()