expressions almost-work (see nondet in test file) for 1 Type, next refactoring to Alphabet

Reverse_Brzozowski/Reverse-Brzozowski.cabal

@@ -30,6 +30,7 @@ test-suite test
     build-depends:
         hedgehog
       , hedgehog-quickcheck
+      , lifted-async
       , base
       , Derv, containers
 

Reverse_Brzozowski/lib/Derv.hs

@@ -6,7 +6,7 @@ import Data.Set (Set, toList, singleton, empty, map, member, union,  cartesianPr
 import Debug.Trace
 
 data RegEx = Empty
-           | Zero
+           | Zero String
            | Push
            | Pop
            | Seq RegEx RegEx
@@ -14,9 +14,24 @@ data RegEx = Empty
            | Star RegEx deriving (Show,Eq, Ord)
 
 
+approx :: Int -> RegEx -> Set String
+approx n expr = lang_n n (singleton "") $ norm expr where
+  lang_n :: Int -> (Set String) -> RegEx -> Set String
+  lang_n _ acc Empty = acc
+  lang_n _ acc (Zero _) = empty
+  lang_n n acc Push = Data.Set.map (\w -> if length w > n then "overflow" else w) $ Data.Set.map (\w -> merge_word (w,"+")) acc
+  lang_n n acc Pop  = Data.Set.map (\w -> if length w > n then "underflow" else w) $ Data.Set.map (\w -> merge_word (w,"-")) acc
+  lang_n n acc (Seq l r) = lang_n n (lang_n n acc l) r
+  lang_n n acc (Alt l r) = (lang_n n acc r) `union` (lang_n n acc l)
+  lang_n n acc (Star e) = fp (\acc' -> lang_n n acc' (Alt e Empty)) acc
+
+fp :: (Eq a) => (a->a) -> a -> a
+fp f a | (f a) == a = a
+       | otherwise  = fp f (f a)
+
 lang :: RegEx -> Set String
 lang Empty = singleton ""
-lang Zero = empty
+lang (Zero _) = empty
 lang Push = singleton "+"
 lang Pop = singleton "-"
 -- this doesnt work, Seq Pop Pop -> emptylang (Seq l Pop) = lang (deriv Push l) -- ^-1 operation needed, to do this generaly, since Seq (_) (_ <+> Pop) doesn't work
@@ -35,7 +50,7 @@ lang_deriv Pop =  Data.Set.map (\word -> if (word == "") then "+" else (if (last
 --assuming ausmultiplizierte normalform
 lang2 :: RegEx -> Set String
 lang2 Empty = singleton ""
-lang2 Zero = empty
+lang2 (Zero _) = empty
 lang2 Push = singleton "+"
 lang2 Pop = singleton "-"
 lang2 (Seq l Pop) = Data.Set.map (\word -> (
@@ -48,6 +63,10 @@ lang2 (Alt l r) = (lang2 l) `union` (lang2 r)
 
 
 merge_word :: (String, String) -> String -- assume normal form
+merge_word ("underflow", _ ) = "underflow" -- underflow
+merge_word ("overflow", _ ) = "overflow" -- underflow
+merge_word (_, "underflow" ) = "underflow" -- underflow
+merge_word (_, "overflow" ) = "overflow" -- underflow
 merge_word ([], r) = r
 merge_word (l, ('-':rest)) | last l == '+' = merge_word (init l, rest)
                            | otherwise     = l ++ ('-':rest)
@@ -55,7 +74,7 @@ merge_word (l,r) = l <> r
 
 final :: RegEx -> Bool
 final Empty = True
-final Zero = False
+final (Zero _) = False
 final Push = False
 final Pop = False
 final (Seq l Push) = False --f rs then final l else rs where rs = final r -- Wrong definition CONTINUE: find real definition
@@ -68,10 +87,10 @@ final (Alt l r) = final l || final r
 final (Star _) = True
 
 derPush :: RegEx -> RegEx
-derPush Empty = Zero
-derPush Zero = Zero
+derPush Empty = Zero "Empty/Push"
+derPush (Zero m) = Zero m
 derPush Push = Empty
-derPush Pop = Zero
+derPush Pop = Zero "Pop/Zero"
 derPush (Alt l r) = (derPush l) <+> (derPush r)
 derPush (Seq l r) | final r = (l <.> (derPush r)) <+> (derPush l)
                   | otherwise = l <.> (derPush r) --
@@ -79,7 +98,7 @@ derPush (Star x) = (Star x) <.> (derPush x) -- hmm??
 
 derPop :: RegEx -> RegEx
 derPop Empty = Push
-derPop Zero = Zero
+derPop (Zero x) = Zero x
 derPop Push = Seq Push Push
 derPop Pop = Empty <+> (Pop <.> Push) -- oof
 derPop (Alt l r) = (derPop l) <+> (derPop r)
@@ -94,14 +113,14 @@ deriv :: RegEx -> (RegEx -> RegEx)
 deriv Push = derPush
 deriv Pop = derPop
 deriv Empty = id
-deriv Zero = const Zero
+deriv (Zero x) = const (Zero x)
 deriv (Seq l r) = (deriv l).(deriv r)
 deriv (Alt l r) = error "not thought about it enough" -- const Zero -- doesn't ALLWAYS exist -- \ word -> (deriv l word)<+>(deriv r word) -- WONG, doesn't exist
 deriv _ = error "blub"
 
 ends_in :: RegEx -> [RegEx]
 ends_in Empty = [Pop] -- Push.Pop == 1
-ends_in Zero = []
+ends_in (Zero _) = []
 ends_in Push = [Push]
 ends_in Pop = [Pop]
 ends_in (Alt l r ) = nub $ sort $ ends_in l ++ ends_in r
@@ -130,7 +149,8 @@ closure :: [(RegEx, RegEx)] -> [(RegEx, RegEx)] -> Maybe [(RegEx, RegEx)]
 closure rel []                 = Just rel
 closure rel ((x,y):todo)
   | x == y                     = closure rel todo -- symmetry
-  | (final x) /= (final y)     = trace ("finality diff: " <> (show (pp x,pp y)) <> "\nRel: " <> (show rel)) Nothing
+  | (final x) /= (final y)     = --trace ("finality diff: " <> (show (pp x,pp y)) <> "\nRel: " <> (show rel))
+                             Nothing
   | (x,y) `elem` (rel ++ todo) = closure rel todo
   | length rel > 1000          = trace "non det?" $ Nothing
   | otherwise                  = closure ((x,y):rel) ([(norm (deriv a x), norm (deriv a y)) | a <- to_check x y ] ++ todo)
@@ -139,7 +159,7 @@ naive :: RegEx -> RegEx -> Maybe [(RegEx, RegEx)]
 naive l r = closure [] [(l,r)] where
 
 naive_bisim :: RegEx -> RegEx -> Bool
-naive_bisim l r = isJust $ is_bisim <$> naive l r
+naive_bisim l r = isJust $ is_bisim <$> naive (norm l) (norm r)
 
 -- assuming norm, else nondet
 (<#) :: RegEx -> RegEx -> Bool
@@ -153,7 +173,7 @@ expr `accepts` word = final (deriv word expr)
 
 norm :: RegEx -> RegEx
 norm Empty = Empty
-norm Zero = Zero
+norm (Zero m) = Zero m
 norm Push = Push
 norm Pop = Pop
 norm (Alt l r) -- | (norm l) <# (norm r) = norm r -- nondet
@@ -167,9 +187,14 @@ norm x@(Seq l r) = let normed = norm l <.> norm r in -- > only 1 evaluation step
 
 norm (Star (Star x)) = norm $ Star x
 norm (Star x) | (norm x) == Empty = Empty
-              | (norm x) == Zero  = Empty
-              | otherwise          = Star $ norm $ x
+              | is_Zero (norm x)  = Empty
+              | idempotent x      = norm (x <+> Empty) -- this solves some issues, but is it premature optim?
+              | otherwise         = case (norm x) of
+                                         (Alt Empty nx) -> Star $ nx
+                                         alt            -> Star alt
 
+idempotent :: RegEx -> Bool
+idempotent x = (norm x) `naive_bisim` (norm (x <.> x))
 
 class SemiRing a where
   one :: a
@@ -179,18 +204,21 @@ class SemiRing a where
 
 pp :: RegEx -> String
 pp Empty = "1"
-pp Zero = "0"
+pp (Zero _) = "0"
 pp Pop = "-"
 pp Push = "x"
 pp (Seq l r) = "(" <> (pp l) <> " " <> (pp r) <> ")"
 pp (Alt l r) = "(" <> (pp l) <> " | " <> (pp r) <> ")"
 pp (Star x) = "(" <> (pp x) <> ")*"
 
+is_Zero (Zero _) = True
+is_Zero _ = False
+
 instance SemiRing RegEx where
   one = Empty
-  zero = Zero
-  Zero <.> _ = Zero
-  _ <.> Zero = Zero
+  zero = Zero "default"
+  (Zero m) <.> _ = Zero m
+  _ <.> (Zero m) = Zero m
   Empty <.> r = r
   l <.> Empty = l
 --  (Star l) <.> r = ----
@@ -200,8 +228,8 @@ instance SemiRing RegEx where
   l <.> (Alt s t) = (l <.> s) <+> (l <.> t) -- slows down performance, makes other steps easier
   (Alt r s) <.> t = (r <.> t) <+> (s <.> t) -- same. custom hinzugefügt. Alternativly could make every other function smarter
   l <.> r = Seq l r
-  Zero <+> r = r
-  l <+> Zero = l
+  (Zero _) <+> r = r
+  l <+> (Zero _) = l
   Empty <+> (Star x) = (Star x)
   (Star x) <+> Empty = (Star x)
   (Alt r s) <+> t = r <+> (s <+> t)
@@ -212,3 +240,4 @@ instance SemiRing RegEx where
           | r <= s = Alt r s
           | otherwise = Alt s r -- depends on arbitrary, derived (<=), scary
 
+--------------------- lexicographic order

Reverse_Brzozowski/test/test.hs

@@ -4,6 +4,12 @@
 import Derv
 
 import Debug.Trace
+import System.Timeout (timeout)
+
+import Control.Concurrent (threadDelay)
+import Control.Concurrent.Async.Lifted (race)
+import Control.Exception (evaluate)
+
 
 import Data.Set (member)
 import Control.Applicative (liftA2)
@@ -14,11 +20,11 @@ import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 
 single_expr :: Gen RegEx
-single_expr = Gen.element [Empty, Zero, Push, Pop]
+single_expr = Gen.element [Empty, zero, Push, Pop]
 
 expr :: Gen RegEx
 expr = Gen.recursive Gen.choice
- (Gen.constant <$> [Empty, Zero, Push, Pop])  -- nonrecursives
+ (Gen.constant <$> [Empty, zero, Push, Pop])  -- nonrecursives
  (Gen.subterm2 expr expr <$> [Seq, Alt])      -- recursives
 
 -- * means works with star expressions
@@ -156,15 +162,29 @@ prop_lang_deriv_r_deriv_lang_r =
 --todo, generate words (== sequences of symbols)
 
 --only to check that accepts terminates
-prop_accepts_implies_includes :: Property
+
+{-prop_accepts_implies_includes :: Property
 prop_accepts_implies_includes =
-  property $ do
+  withTests 10000 $ withRetries 0 $ withShrinks 0 $ property $ do
     matcher <- forAll star_expr
     w       <- forAll word
-    liftIO $ print (pp matcher <> " accepts " <> (pp w))
-    (if ((norm matcher) `accepts` (norm w)) then True else True) === True
+    liftIO $ print "A"
+    result <- liftIO $ timeout 2 $ do
+      pure $ if ((norm matcher) `accepts` (norm w)) then True else True
+    liftIO $ print "B"
+    case result of
+         Nothing -> fail "Timeout"
+         Just passed -> passed === True
+-}
 
 
+prop_fast_timeout :: Property
+prop_fast_timeout =
+  property $ do
+    matcher <- forAll star_expr
+    w       <- forAll word
+    test $ withTimeLimit 10000 $
+      assert $ (if ((norm matcher) `accepts` (norm w)) then True else True) == True
 
 tests :: IO Bool
 tests =
@@ -172,6 +192,20 @@ tests =
 
 main = tests
 
+withTimeLimit :: Int -> TestT IO a -> TestT IO a
+withTimeLimit timeout v = do
+  result <-
+    race
+      (liftIO $ threadDelay timeout)
+      v
+  case result of
+    Left () -> fail "Timeout exceeded"
+    Right x -> pure x
+
+
 -- deriv Push ((Star Push) <.> (Pop)) => Zero
 -- naive (Pop <+> (Star Push)) ((Star Push) <.> (Pop))
 -- this gives the wrong answer
+-- final $ deriv Push $ Star (Seq Pop (Alt Push Pop)) :: Nondet
+------  but don't know why
+