Skip to content
Snippets Groups Projects
Commit 99c32cd5 authored by Hendrik Rassmann's avatar Hendrik Rassmann
Browse files

naive of Star still some work

parent 2cecae2f
No related branches found
No related tags found
No related merge requests found
module Derv where module Derv where
import Data.List (nub, sort) import Data.List (nub, sort)
import Data.Set (Set, singleton, empty, map, union, cartesianProduct, filter) import Data.Set (Set, singleton, empty, map, member, union, cartesianProduct, filter)
import Debug.Trace import Debug.Trace
data RegEx = Empty data RegEx = Empty
...@@ -23,10 +23,9 @@ lang (Seq l r) = Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r) ...@@ -23,10 +23,9 @@ lang (Seq l r) = Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r)
lang (Alt l r) = (lang l) `union` (lang r) lang (Alt l r) = (lang l) `union` (lang r)
lang_deriv :: RegEx -> Set String -> Set String lang_deriv :: RegEx -> Set String -> Set String
lang_deriv Push = Data.Set.map (\ word -> if word == [] then "-" else lang_deriv Push = Data.Set.map (init) . (
(if (last word == '+') then init word else (word ++ "-"))) Data.Set.filter (\word -> (word /= "") && (last word == '+')))
lang_deriv Pop = Data.Set.map (\word -> if word == "" then "+" else init word) . ( lang_deriv Pop = Data.Set.map (\word -> if (word == "") then "+" else (if (last word == '+') then (word ++ "+") else (init word)) )
Data.Set.filter (\word -> word == "" || last word == '+'))
--assuming ausmultiplizierte normalform --assuming ausmultiplizierte normalform
...@@ -35,7 +34,10 @@ lang2 Empty = singleton "" ...@@ -35,7 +34,10 @@ lang2 Empty = singleton ""
lang2 Zero = empty lang2 Zero = empty
lang2 Push = singleton "+" lang2 Push = singleton "+"
lang2 Pop = singleton "-" lang2 Pop = singleton "-"
lang2 (Seq l Pop) = lang_deriv Push (lang2 l) --Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r) lang2 (Seq l Pop) = Data.Set.map (\word -> (
if (word == "") then "-" else
(if (last word == '+') then (init word) else (word ++ "-") ))) (lang2 l)
-- would be nice, doesn't wokr lang_deriv Push (lang2 l) --Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r)
lang2 (Seq l Push) = Data.Set.map (++ "+") (lang2 l) --Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r) lang2 (Seq l Push) = Data.Set.map (++ "+") (lang2 l) --Data.Set.map (merge_word) $ cartesianProduct (lang l) (lang r)
lang2 (Seq _ _) = error "assume normal form, ausmulipliziert" lang2 (Seq _ _) = error "assume normal form, ausmulipliziert"
lang2 (Alt l r) = (lang2 l) `union` (lang2 r) lang2 (Alt l r) = (lang2 l) `union` (lang2 r)
...@@ -57,7 +59,7 @@ final (Seq l Push) = False --f rs then final l else rs where rs = final r -- Wro ...@@ -57,7 +59,7 @@ final (Seq l Push) = False --f rs then final l else rs where rs = final r -- Wro
--final (Seq (Alt l1 l2) r) = final (l1 <.> r) || final (l2 <.> r) -- --final (Seq (Alt l1 l2) r) = final (l1 <.> r) || final (l2 <.> r) --
final (Seq l Pop) = final (derPush l) -- assuming normal form final (Seq l Pop) = final (derPush l) -- assuming normal form
final x@(Seq l r) | final r = final l final x@(Seq l r) | final r = final l
| otherwise = error "to numb" --final $ norm $ deriv (invert r) l--trace (show x) $ undefined -- only if normalized undefined --if rs then final l else rs where rs = final r -- Wrong definition CONTINUE: find real definition | otherwise = "" `Data.Set.member` (lang x) -- please find a smarter way!! error "too numb" --final $ norm $ deriv (invert r) l--trace (show x) $ undefined -- only if normalized undefined --if rs then final l else rs where rs = final r -- Wrong definition CONTINUE: find real definition
final (Alt l r) = final l || final r final (Alt l r) = final l || final r
final (Star _) = True final (Star _) = True
...@@ -69,6 +71,7 @@ derPush Pop = Zero ...@@ -69,6 +71,7 @@ derPush Pop = Zero
derPush (Alt l r) = (derPush l) <+> (derPush r) -- Alt (derPush l) (derPush r) derPush (Alt l r) = (derPush l) <+> (derPush r) -- Alt (derPush l) (derPush r)
derPush (Seq l r) | final r = (l <.> (derPush r)) <+> (derPush l) -- Alt (Seq l (derPush r)) (derPush l) derPush (Seq l r) | final r = (l <.> (derPush r)) <+> (derPush l) -- Alt (Seq l (derPush r)) (derPush l)
| otherwise = l <.> (derPush r) -- Seq l (derPush r) | otherwise = l <.> (derPush r) -- Seq l (derPush r)
derPush (Star x) = (Star x) <.> (derPush x) --
derPop :: RegEx -> RegEx derPop :: RegEx -> RegEx
derPop Empty = Push derPop Empty = Push
...@@ -78,6 +81,9 @@ derPop Pop = Empty ...@@ -78,6 +81,9 @@ derPop Pop = Empty
derPop (Alt l r) = (derPop l) <+> (derPop r) -- Alt (derPop l) (derPop r) derPop (Alt l r) = (derPop l) <+> (derPop r) -- Alt (derPop l) (derPop r)
derPop (Seq l r) | final r = (l <.> (derPop r)) <+> (derPop l) -- Alt (Seq l (derPop r)) (derPop l) derPop (Seq l r) | final r = (l <.> (derPop r)) <+> (derPop l) -- Alt (Seq l (derPop r)) (derPop l)
| otherwise = l <.> (derPop r)-- Seq l (derPop r) | otherwise = l <.> (derPop r)-- Seq l (derPop r)
derPop (Star x) = (Star x) <.> (derPop x) -- is this correct?
deriv :: RegEx -> (RegEx -> RegEx) deriv :: RegEx -> (RegEx -> RegEx)
deriv Push = derPush deriv Push = derPush
...@@ -97,14 +103,31 @@ ends_in (Alt l r ) = nub $ sort $ ends_in l ++ ends_in r ...@@ -97,14 +103,31 @@ ends_in (Alt l r ) = nub $ sort $ ends_in l ++ ends_in r
ends_in (Seq l r) = if (null rs) then ends_in l else rs where rs = ends_in r ends_in (Seq l r) = if (null rs) then ends_in l else rs where rs = ends_in r
ends_in (Star x) = ends_in x ends_in (Star x) = ends_in x
to_check l r = ends_in (Alt (Alt l Pop) r)
-- only works without *, otherwise wouldn't terminate
bisim l r = f (norm l) (norm r) where bisim l r = f (norm l) (norm r) where
f :: RegEx -> RegEx -> Bool f :: RegEx -> RegEx -> Bool
f (Star _) _ = error "doesn't work for star operator"
f _ (Star _) = error "doesn't work for star operator"
f l r | l == r = True f l r | l == r = True
| final l /= final r = False | final l /= final r = False
| otherwise = -- trace (show l <> " =?= " <> (show r)) $ | otherwise = -- trace (show l <> " =?= " <> (show r)) $
all (uncurry f) [ (deriv a l, deriv a r) | a <- ends_in (Alt l r)] all (uncurry f) [ (deriv a l, deriv a r) | a <- ends_in (Alt l r)]
is_bisim :: [(RegEx, RegEx)] -> Bool
is_bisim pairs = all (\(l,r) -> all (flip elem pairs) [(deriv a l, deriv a r) | a <- ( [Pop] ++ ends_in (Alt l r)) ]) pairs
naive :: RegEx -> RegEx -> Maybe [(RegEx, RegEx)]
naive l r = f [] [(l,r)] where
f :: [(RegEx, RegEx)] -> [(RegEx, RegEx)] -> Maybe [(RegEx, RegEx)]
f rel [] = Just rel
f rel ((x,y):todo) | x == y = f rel todo -- symmetry
| (final x) /= (final y) = trace (show rel) $ Nothing -- assuming final computation is easy, which I don't really know right now
| (x,y) `elem` (rel ++ todo) = f rel todo
| length rel > 5 = trace (show rel) $ Nothing
| otherwise = f ((x,y):rel) ([(norm (deriv a x), norm (deriv a y)) | a <- to_check x y ] ++ todo)
norm :: RegEx -> RegEx norm :: RegEx -> RegEx
norm Empty = Empty norm Empty = Empty
...@@ -144,5 +167,5 @@ instance SemiRing RegEx where ...@@ -144,5 +167,5 @@ instance SemiRing RegEx where
| otherwise = Alt s (r <+> t) | otherwise = Alt s (r <+> t)
r <+> s | r == s = r r <+> s | r == s = r
| r <= s = Alt r s | r <= s = Alt r s
| otherwise = Alt s r -- depends on arbitrary <=, scary | otherwise = Alt s r -- depends on arbitrary, derived (<=), scary
...@@ -3,6 +3,8 @@ ...@@ -3,6 +3,8 @@
--module Test where --module Test where
import Derv import Derv
import Data.Set (member) import Data.Set (member)
import Control.Applicative (liftA2)
import Control.Monad ( when)
import Hedgehog import Hedgehog
import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range import qualified Hedgehog.Range as Range
...@@ -75,7 +77,6 @@ prop_ann = ...@@ -75,7 +77,6 @@ prop_ann =
norm (a <.> zero) === zero norm (a <.> zero) === zero
norm (zero <.> a) === zero norm (zero <.> a) === zero
--fails for Seq Push (Seq (Alt Push Empty) Pop)
prop_final :: Property prop_final :: Property
prop_final = prop_final =
property $ do property $ do
...@@ -96,7 +97,18 @@ prop_lang_lang2 = ...@@ -96,7 +97,18 @@ prop_lang_lang2 =
a <- forAll $ expr a <- forAll $ expr
lang (norm a) === (lang2 (norm a)) lang (norm a) === (lang2 (norm a))
prop_lang_deriv_r_deriv_lang_r :: Property
prop_lang_deriv_r_deriv_lang_r =
property $ do
r <- forAll $ expr
(lang.derPush.norm) r === (((lang_deriv Push).lang.norm) r)
prop_bisim_is_bisim :: Property
prop_bisim_is_bisim =
property $ do
pairs <- forAll $ Gen.list (Range.linear 0 5) (liftA2 (,) expr expr)
when (is_bisim pairs) $ do
all (\(l,r) -> bisim l r) pairs === True
tests :: IO Bool tests :: IO Bool
tests = tests =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment