nnf property

gen0_virtuous_cycle/gen0-virtuous-cycle.cabal

@@ -11,7 +11,7 @@ Library StaX
     exposed-modules:     PSLex, AnnoLex, AnnoParse, ExpTerm, BaseTypes, TC
     default-language:    Haskell2010
 
-executable Main.hs
+executable Main
     main-is:          Main.hs
     other-modules:    TC0, TC, PSLex, AnnoLex, AnnoParse, ExpTerm, BaseTypes
     build-depends:    base >=4.13.0.0,
@@ -25,7 +25,7 @@ executable Main.hs
 Test-Suite Test
    type:                  exitcode-stdio-1.0
    main-is:               Test.hs
-   other-modules:         AnnoLex, PSLex, TC0, TC
+   other-modules:         AnnoLex, AnnoParse, ExpTerm, PSLex, BaseTypes, TC0, TC
    build-depends:         base >= 4.13.0.0,
                           QuickCheck ^>=2.15,
                           hspec >=2.10,

gen0_virtuous_cycle/test/Test.hs

@@ -14,10 +14,20 @@ import PSLex
 import AnnoLex
 import TC0
 import TC
+import ExpTerm
 
 ps_program :: Gen [String]
 ps_program = listOf $ elements ["1 ","add "]
 
+--instance Arbitrary (Expr Int) where
+
+int_expr :: Gen (Expr Int)
+int_expr = oneof [ Node <$> arbitrary
+                 , Seq  <$> listOf int_expr
+                 , Neg  <$> int_expr
+                 , return (Zero "qc")
+                 ]
+
 extract_Stack_Height :: String -> Maybe Int
 extract_Stack_Height "GS>GS>" = Just 0
 extract_Stack_Height ('G':('S':('>':('E':_)))) = Nothing
@@ -57,8 +67,16 @@ prop_stackShorterProgram = forAll ps_program $ \tokens -> monadicIO $ do
                                                                     return $ case height of
                                                                              Nothing -> True
                                                                              Just  n -> n == (length tokens)
+
+--prop_expr_nnf_same_frac :: Property
+--prop_expr_nnf_same_frac = forAll int_expression
+
 main :: IO ()
 main = hspec $ do
+  describe "expr2nnf" $ do
+    it "converts epxr to nnf retaining the semantic meaning" $ do
+      result <- quickCheckResult prop_expr2nnf_retains_frac_semantic
+      unless (isSuccess result) exitFailure
   describe "scanPS" $ do
     it "scanns the example file" $ do
       s      <- readFile "output.ps"
@@ -70,13 +88,36 @@ main = hspec $ do
       let ts = parseBlocks $ scanPS s
       (find_prefix ts) > 10 `shouldBe` True
 
-int_interpretation :: (Expr Int) -> Int
-int_interpretation = undefined
---    it "returns the first element of an *arbitrary* list" $
---      property $ \x xs -> head (x:xs) == (x :: Int)
---
---    it "throws an exception if used with an empty list" $ do
---      evaluate (head []) `shouldThrow` anyException
+
+
+expr2nnf_retains_frac_semantic :: Expr Int -> Bool
+expr2nnf_retains_frac_semantic expr = expr_frac expr == (nnf_frac.expr2nnf) expr
+
+prop_expr2nnf_retains_frac_semantic :: Property
+prop_expr2nnf_retains_frac_semantic = forAll int_expr $ \expr -> expr2nnf_retains_frac_semantic expr
+
+expr_frac :: (Expr Int) -> Rational
+expr_frac (Node n) = toRational n
+expr_frac (Tag _) = 1
+expr_frac (Seq xs) = foldl (\s x -> s * (expr_frac x)) 1 xs
+expr_frac (Thing) = 97 --some prime
+expr_frac (Var i) = error "not yet thought of"
+expr_frac (Neg x) = if (expr_frac x) == 0 then 0 else 1 / (expr_frac x)
+expr_frac (Zero m) = 0
+expr_frac _      = error "will think of later"
+
+nnf_frac :: (NNF Int) -> Rational
+nnf_frac (Push n) = toRational n
+nnf_frac (Pop n) = 1 / (toRational n)
+nnf_frac (NNF_Tag _) = 1
+nnf_frac (NNF_Seq xs) = foldl (\s x -> s * (nnf_frac x)) 1 xs
+nnf_frac (NNF_Thing) = 97 --some prime
+nnf_frac (NNF_Plop) = 1/97 --some prime
+nnf_frac (NNF_Var i) = error "not yet thought of"
+nnf_frac (NNF_Zero m) = 0
+nnf_frac _      = error "will think of later"
+
+
 {-
 main = do
      s      <- readFile "output.ps"

gen0_virtuous_cycle/test/Test.hs.save

+module Main where
+import Control.Monad
+import Control.Exception (evaluate)
+import Test.QuickCheck
+import Test.QuickCheck.Test
+import Test.QuickCheck.Monadic (assert, monadicIO, run)
+
+import Test.Hspec
+
+import System.Process
+import System.Exit (exitFailure)
+
+import PSLex
+import AnnoLex
+import TC0
+import TC
+import ExpTerm
+
+ps_program :: Gen [String]
+ps_program = listOf $ elements ["1 ","add "]
+
+extract_Stack_Height :: String -> Maybe Int
+extract_Stack_Height "GS>GS>" = Just 0
+extract_Stack_Height ('G':('S':('>':('E':_)))) = Nothing
+--example "1 1\n add \n" => "GS>GS<2>GS<1>"
+extract_Stack_Height output = Just $ f output where
+               f :: String -> Int
+               f = read.reverse.(takeWhile (/= '<')).tail.reverse
+
+
+gs :: [String] -> IO String
+gs program = readProcess "gs" ["-q", "-dNODISPLAY"] $ (concat program) ++ "\n"
+
+prop_show_inv_scan :: [Token] -> Bool
+prop_show_inv_scan tokens = tokens == (scanPS (concat (show <$> tokens)))
+
+check_prefix_height :: [Token] -> Int -> IO Bool
+check_prefix_height tokens  n = do
+  --testing stuff
+  let useless = scanAnnos "I -> I"
+  --test done
+  let prefix = (take n tokens)
+  output <- gs $ show <$> prefix
+  let run_height = extract_Stack_Height output --Maybe Int
+  let exp_program = token2Type <$> prefix
+  let exp_height = fmap fst $ join $ (runState stackHeight) <$> snd <$>(nsteps 10000 (buildins,[],exp_program))
+  return $ exp_height == run_height
+
+
+--find_max_valid_prefix :: [Token] -> Int
+--find_max_valid_prefix :: tokens  = last $ takeWhile (\x -> x <= length tokens) [1..]
+
+
+prop_stackShorterProgram :: Property
+prop_stackShorterProgram = forAll ps_program $ \tokens -> monadicIO $ do
+                                                                    output <- run (gs tokens)
+                                                                    let height = extract_Stack_Height output
+                                                                    return $ case height of
+                                                                             Nothing -> True
+                                                                             Just  n -> n == (length tokens)
+main :: IO ()
+main = hspec $ do
+  describe "scanPS" $ do
+    it "scanns the example file" $ do
+      s      <- readFile "output.ps"
+      let ts = parseBlocks $ scanPS s
+      (length ts) > 0 `shouldBe` True
+  describe "find_prefix" $ do
+    it "works for 10" $ do
+      s      <- readFile "output.ps"
+      let ts = parseBlocks $ scanPS s
+      (find_prefix ts) > 10 `shouldBe` True
+
+int_interpretation :: (Expr Int) -> Int
+int_interpretation = 
+--    it "returns the first element of an *arbitrary* list" $
+--      property $ \x xs -> head (x:xs) == (x :: Int)
+--
+--    it "throws an exception if used with an empty list" $ do
+--      evaluate (head []) `shouldThrow` anyException
+{-
+main = do
+     s      <- readFile "output.ps"
+     let ts = parseBlocks $ scanPS s
+--     result <- quickCheckResult prop_stackShorterProgram
+--     unless (isSuccess result) exitFailure
+--     result2 <- quickCheckResult $ prop_show_inv_scan ts
+--     unless (isSuccess result2) exitFailure
+     result_height_eqv <- quickCheckResult $ monadicIO $ run $ check_prefix_height ts 30
+     unless (isSuccess result_height_eqv) exitFailure
+-}