packages feed

opentheory-parser (empty) → 1.105

raw patch · 6 files changed

+260/−0 lines, 6 filesdep +QuickCheckdep +basedep +opentheorysetup-changed

Dependencies added: QuickCheck, base, opentheory, opentheory-primitive, 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-parser.cabal view
@@ -0,0 +1,43 @@+name: opentheory-parser+version: 1.105+category: Parsing+synopsis: Simple stream parsers+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:+  Simple stream parsers+  Automatically generated from the opentheory package haskell-parser-1.105++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 == 1.61++  hs-source-dirs: src++  ghc-options: -Wall++  exposed-modules:+    OpenTheory.Parser+    OpenTheory.Parser.Stream++executable opentheory-parser-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 == 1.61++  hs-source-dirs: src, testsrc++  ghc-options: -Wall++  main-is: Test.hs
+ src/OpenTheory/Parser.hs view
@@ -0,0 +1,78 @@+{- |+module: $Header$+description: Simple stream parsers+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Parser+where++import qualified OpenTheory.Parser.Stream as Stream++newtype Parser a b =+  Parser { unParser :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a) }++partialMap :: (b -> Maybe c) -> Parser a b -> Parser a c+partialMap f p =+  Parser pf+  where+  {-pf :: a -> Stream.Stream a -> Maybe (c, Stream.Stream a)-}+    pf a s =+      case unParser p a s of+        Nothing -> Nothing+        Just (b, s') ->+          case f b of+            Nothing -> Nothing+            Just c -> Just (c, s')++map :: (b -> c) -> Parser a b -> Parser a c+map f p = partialMap (\b -> Just (f b)) p++parse :: Parser a b -> Stream.Stream a -> Maybe (b, Stream.Stream a)+parse _ Stream.Error = Nothing+parse _ Stream.Eof = Nothing+parse p (Stream.Cons a s) = unParser p a s++parseAll :: Parser a a+parseAll =+  Parser pa+  where+  {-pa :: a -> Stream.Stream a -> Maybe (a, Stream.Stream a)-}+    pa a s = Just (a, s)++parseNone :: Parser a b+parseNone =+  Parser pn+  where+  {-pn :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}+    pn _ _ = Nothing++parseOption :: (a -> Maybe b) -> Parser a b+parseOption f = partialMap f parseAll++parsePair :: Parser a b -> Parser a c -> Parser a (b, c)+parsePair pb pc =+  Parser pbc+  where+  {-pbc :: a -> Stream.Stream a -> Maybe ((b, c), Stream.Stream a)-}+    pbc a s =+      case unParser pb a s of+        Nothing -> Nothing+        Just (b, s') ->+          case parse pc s' of+            Nothing -> Nothing+            Just (c, s'') -> Just ((b, c), s'')++parseSome :: (a -> Bool) -> Parser a a+parseSome p = parseOption (\a -> if p a then Just a else Nothing)++parseStream :: Parser a b -> Stream.Stream a -> Stream.Stream b+parseStream _ Stream.Error = Stream.Error+parseStream _ Stream.Eof = Stream.Eof+parseStream p (Stream.Cons a s) =+  case unParser p a s of+    Nothing -> Stream.Error+    Just (b, s') -> Stream.Cons b (parseStream p s')
+ src/OpenTheory/Parser/Stream.hs view
@@ -0,0 +1,48 @@+{- |+module: $Header$+description: Simple stream parsers+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module OpenTheory.Parser.Stream+where++import qualified OpenTheory.Data.List.Geometric as Data.List.Geometric+import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import qualified OpenTheory.Primitive.Random as Primitive.Random++data Stream a =+    Error+  | Eof+  | Cons a (Stream a)++append :: [a] -> Stream a -> Stream a+append [] s = s+append (h : t) s = Cons h (append t s)++fromList :: [a] -> Stream a+fromList l = append l Eof++fromRandom ::+  (Primitive.Random.Random -> (a, Primitive.Random.Random)) ->+    Primitive.Random.Random -> (Stream a, Primitive.Random.Random)+fromRandom d r =+  let (l, r') = Data.List.Geometric.fromRandom d r in+  let (b, r'') = Primitive.Random.bit r' in+  (append l (if b then Error else Eof), r'')++size :: Stream a -> Primitive.Natural.Natural+size Error = 0+size Eof = 0+size (Cons _ s) = size s + 1++toList :: Stream a -> Maybe [a]+toList Error = Nothing+toList Eof = Just []+toList (Cons a s) =+  case toList s of+    Nothing -> Nothing+    Just l -> Just (a : l)
+ testsrc/Test.hs view
@@ -0,0 +1,68 @@+{- |+module: Main+description: Simple stream parsers - testing+license: MIT++maintainer: Joe Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module Main+  ( main )+where++import qualified OpenTheory.Data.List as Data.List+import qualified OpenTheory.Data.List.Geometric as Data.List.Geometric+import qualified OpenTheory.Data.Option as Data.Option+import qualified OpenTheory.Number.Natural as Number.Natural+import qualified OpenTheory.Parser.Stream as Parser.Stream+import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Primitive.Test as Primitive.Test++proposition0 :: Primitive.Random.Random -> Bool+proposition0 r =+  let (l, _) =+        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in+  Parser.Stream.size (Parser.Stream.fromList l) == Data.List.size l++proposition1 :: Primitive.Random.Random -> Bool+proposition1 r =+  let (l, _) =+        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in+  Data.Option.equal (Data.List.equal (==))+    (Parser.Stream.toList (Parser.Stream.fromList l)) (Just l)++proposition2 :: Primitive.Random.Random -> Bool+proposition2 r =+  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r in+  case Parser.Stream.toList s of+    Nothing -> True+    Just l -> Data.List.size l == Parser.Stream.size s++proposition3 :: Primitive.Random.Random -> Bool+proposition3 r =+  let (l, r') =+        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in+  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r' in+  Parser.Stream.size (Parser.Stream.append l s) ==+  Data.List.size l + Parser.Stream.size s++proposition4 :: Primitive.Random.Random -> Bool+proposition4 r =+  let (l, r') =+        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in+  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r' in+  Data.Option.equal (Data.List.equal (==))+    (Parser.Stream.toList (Parser.Stream.append l s))+    (case Parser.Stream.toList s of+       Nothing -> Nothing+       Just ls -> Just (l ++ ls))++main :: IO ()+main =+    do Primitive.Test.check "Proposition 0:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    H.Stream.size (H.Stream.fromList l) = H.size l\n  " proposition0+       Primitive.Test.check "Proposition 1:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    H.equal (H.equal (=)) (H.Stream.toList (H.Stream.fromList l)) (some l)\n  " proposition1+       Primitive.Test.check "Proposition 2:\n  !r.\n    let (s, r') <- H.Stream.fromRandom H.fromRandom r in\n    case H.Stream.toList s of\n      none -> T\n    | some l -> H.size l = H.Stream.size s\n  " proposition2+       Primitive.Test.check "Proposition 3:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    let (s, r'') <- H.Stream.fromRandom H.fromRandom r' in\n    H.Stream.size (H.Stream.append l s) = H.size l + H.Stream.size s\n  " proposition3+       Primitive.Test.check "Proposition 4:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    let (s, r'') <- H.Stream.fromRandom H.fromRandom r' in\n    H.equal (H.equal (=)) (H.Stream.toList (H.Stream.append l s))\n      (case H.Stream.toList s of none -> none | some ls -> some (l @ ls))\n  " proposition4+       return ()