> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.Finite ( isFinite, isFiniteM
> , isCofinite, isCofiniteM
> , isTFinite, isTFiniteM
> , isTCofinite, isTCofiniteM
> ) where
> import LTK.FSA
> import LTK.Algebra
> import LTK.Tiers (project)
> import LTK.Decide.PT (isPTM)
>
> isFinite :: (Ord n, Ord e) => FSA n e -> Bool
> isFinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFinite = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM (SynMon n e -> Bool) -> (FSA n e -> SynMon n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> SynMon n e
forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
>
> isCofinite :: (Ord n, Ord e) => FSA n e -> Bool
> isCofinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isCofinite = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM (SynMon n e -> Bool) -> (FSA n e -> SynMon n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> SynMon n e
forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
>
>
>
>
> isFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM SynMon n e
s = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (Set (State ([Maybe n], [Symbol e])) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e])) -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e. FSA n e -> Set (State n)
finals SynMon n e
s) Set (State ([Maybe n], [Symbol e]))
i)
> where i :: Set (State ([Maybe n], [Symbol e]))
i = SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (State (n, [Symbol e]))
idempotents SynMon n e
s
>
>
>
>
> isCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isCofiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM SynMon n e
s = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isPTM SynMon n e
s Bool -> Bool -> Bool
&& (Set (State ([Maybe n], [Symbol e])) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State ([Maybe n], [Symbol e]))
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) Bool -> Bool -> Bool
&& Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e])) -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e. FSA n e -> Set (State n)
finals SynMon n e
s) Set (State ([Maybe n], [Symbol e]))
i
> where i :: Set (State ([Maybe n], [Symbol e]))
i = SynMon n e -> Set (State ([Maybe n], [Symbol e]))
forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (State (n, [Symbol e]))
idempotents SynMon n e
s
>
>
>
> isTFinite :: (Ord n, Ord e) => FSA n e -> Bool
> isTFinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isTFinite = FSA n e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFinite (FSA n e -> Bool) -> (FSA n e -> FSA n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
>
> isTFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isTFiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isTFiniteM = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFiniteM (SynMon n e -> Bool)
-> (SynMon n e -> SynMon n e) -> SynMon n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> SynMon n e
forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
> isTCofinite :: (Ord n, Ord e) => FSA n e -> Bool
> isTCofinite :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isTCofinite = FSA n e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isCofinite (FSA n e -> Bool) -> (FSA n e -> FSA n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project
>
>
>
>
> isTCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
> isTCofiniteM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isTCofiniteM = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM (SynMon n e -> Bool)
-> (SynMon n e -> SynMon n e) -> SynMon n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> SynMon n e
forall n e. (Ord n, Ord e) => FSA n e -> FSA n e
project