> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.JoinVariety
> Copyright : (c) 2025 Dakotah Lambert
> License   : MIT

> This module provides a mechanism for deciding membership
> in conjunctive varieties.  It extends the systems defined by
> LTK.Decide.Variety, but the more complex structure used
> incurs a performance cost.
>
> @since 1.3
> -}

> module LTK.Decide.JoinVariety ( isJoinVariety
>                               , isMJoinVariety
>                               , isJoinVarietyJS
>                               ) where

> import Data.Char (isLetter, isSpace)
> import qualified Data.Map as Map
> import qualified Data.Set as Set

> import LTK.FSA ( FSA
>                , JSemigroup
>                , neutralize
>                , renameSymbolsByMonotonic
>                , syntacticJSemigroup
>                )

> -- |Determine if the syntactic join-monoid of the given language
> -- is a member of the variety given by equations and inequalities.
> -- The precondition, that the automaton be normalized, is not checked.
> isMJoinVariety :: (Ord n, Ord e) => String -> FSA n e -> Maybe Bool
> isMJoinVariety :: forall n e. (Ord n, Ord e) => String -> FSA n e -> Maybe Bool
isMJoinVariety String
s = String -> FSA n (Maybe e) -> Maybe Bool
forall n e. (Ord n, Ord e) => String -> FSA n e -> Maybe Bool
isJoinVariety String
s
>                    (FSA n (Maybe e) -> Maybe Bool)
-> (FSA n e -> FSA n (Maybe e)) -> FSA n e -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Maybe e) -> FSA n (Maybe e) -> FSA n (Maybe e)
forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
neutralize (Maybe e -> Set (Maybe e)
forall a. a -> Set a
Set.singleton Maybe e
forall a. Maybe a
Nothing)
>                    (FSA n (Maybe e) -> FSA n (Maybe e))
-> (FSA n e -> FSA n (Maybe e)) -> FSA n e -> FSA n (Maybe e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> Maybe e) -> FSA n e -> FSA n (Maybe e)
forall e e1 n.
(Ord e, Ord e1, Ord n) =>
(e -> e1) -> FSA n e -> FSA n e1
renameSymbolsByMonotonic e -> Maybe e
forall a. a -> Maybe a
Just

> -- |Determine if the syntactic join-semigroup of the given language
> -- is a member of the variety given by equations and inequalities.
> -- The precondition, that the automaton be normalized, is not checked.
> isJoinVariety :: (Ord n, Ord e) => String -> FSA n e -> Maybe Bool
> isJoinVariety :: forall n e. (Ord n, Ord e) => String -> FSA n e -> Maybe Bool
isJoinVariety String
s = String -> JSemigroup e -> Maybe Bool
forall e. Ord e => String -> JSemigroup e -> Maybe Bool
isJoinVarietyJS String
s (JSemigroup e -> Maybe Bool)
-> (FSA n e -> JSemigroup e) -> FSA n e -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> JSemigroup e
forall n e. (Ord n, Ord e) => FSA n e -> JSemigroup e
syntacticJSemigroup

> -- |Determine if the given join-semigroup is a member of the variety
> -- given by equations and inequalities.
> isJoinVarietyJS :: Ord e => String -> JSemigroup e -> Maybe Bool
> isJoinVarietyJS :: forall e. Ord e => String -> JSemigroup e -> Maybe Bool
isJoinVarietyJS String
s JSemigroup e
j
>     | Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
1 String
s' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"[" = Maybe Bool
forall a. Maybe a
Nothing
>     | Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
1 (String -> String
forall a. [a] -> [a]
reverse String
s') String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"]" = Maybe Bool
forall a. Maybe a
Nothing
>     | Bool
otherwise = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Maybe [Bool] -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Token] -> Maybe Bool) -> [[Token]] -> Maybe [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (JSemigroup e -> [Token] -> Maybe Bool
forall e. Ord e => JSemigroup e -> [Token] -> Maybe Bool
universallySatisfies JSemigroup e
j) ([[Token]] -> Maybe [Bool]) -> Maybe [[Token]] -> Maybe [Bool]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe [[Token]]
progs)
>     where s' :: String
s' = String -> String
expand String
s
>           s'' :: String
s'' = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 String
s'
>           progs :: Maybe [[Token]]
progs = [Maybe [Token]] -> Maybe [[Token]]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ([Maybe [Token]] -> Maybe [[Token]])
-> ([String] -> [Maybe [Token]]) -> [String] -> Maybe [[Token]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe [Token]) -> [String] -> [Maybe [Token]]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> String -> Maybe [Token])
-> String -> String -> Maybe [Token]
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> String -> Maybe [Token]
shunt []) ([String] -> Maybe [[Token]]) -> [String] -> Maybe [[Token]]
forall a b. (a -> b) -> a -> b
$ Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn Char
';' String
s''

> jsappend :: [Int] -> [Int] -> [Int]
> jsappend :: [Int] -> [Int] -> [Int]
jsappend [Int]
x [Int]
y = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Int]
y[Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!!) [Int]
x

> jsomega :: [Int] -> [Int]
> jsomega :: [Int] -> [Int]
jsomega [Int]
x = [[Int]] -> [Int]
forall {a}. [a] -> a
head' ([[Int]] -> [Int]) -> ([[Int]] -> [[Int]]) -> [[Int]] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[Int]], [[Int]]) -> [[Int]]
forall a b. (a, b) -> b
snd (([[Int]], [[Int]]) -> [[Int]])
-> ([[Int]] -> ([[Int]], [[Int]])) -> [[Int]] -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> Bool) -> [[Int]] -> ([[Int]], [[Int]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break [Int] -> Bool
idem ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> [Int]) -> [Int] -> [[Int]]
forall a. (a -> a) -> a -> [a]
iterate ([Int] -> [Int] -> [Int]
jsappend [Int]
x) [Int]
x
>     where head' :: [a] -> a
head' [a]
y = case [a]
y of
>                       (a
yy:[a]
_) -> a
yy
>                       [a]
_ -> String -> a
forall a. HasCallStack => String -> a
error String
"unbounded omega search"
>           idem :: [Int] -> Bool
idem [Int]
y = [Int] -> [Int] -> [Int]
jsappend [Int]
y [Int]
y [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int]
y

> jsjoin :: JSemigroup e -> [Int] -> [Int] -> [Int]
> jsjoin :: forall e. JSemigroup e -> [Int] -> [Int] -> [Int]
jsjoin ((Map Int (Set Int)
q2qs,Map (Set Int) Int
qs2q),(Map (Set [e]) [Int], Map [Int] (Set [e]))
_) = (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Int
g
>     where g :: Int -> Int -> Int
g Int
x Int
y = Map (Set Int) Int
qs2q Map (Set Int) Int -> Set Int -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! ((Map Int (Set Int)
q2qs Map Int (Set Int) -> Int -> Set Int
forall k a. Ord k => Map k a -> k -> a
Map.! Int
x) Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Map Int (Set Int)
q2qs Map Int (Set Int) -> Int -> Set Int
forall k a. Ord k => Map k a -> k -> a
Map.! Int
y))

> universallySatisfies :: Ord e => JSemigroup e -> [Token] -> Maybe Bool
> universallySatisfies :: forall e. Ord e => JSemigroup e -> [Token] -> Maybe Bool
universallySatisfies j :: JSemigroup e
j@((Map Int (Set Int), Map (Set Int) Int)
_,(Map (Set [e]) [Int]
_,Map [Int] (Set [e])
a2s)) [Token]
ts
>     = case (Token -> Bool) -> [Token] -> [Token]
forall a. (a -> Bool) -> [a] -> [a]
filter Token -> Bool
isVar [Token]
ts of
>         (Token
x:[Token]
_) -> ([Bool] -> Bool) -> Maybe [Bool] -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Maybe [Bool] -> Maybe Bool)
-> ([[Int]] -> Maybe [Bool]) -> [[Int]] -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe Bool] -> Maybe [Bool]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA
>                  ([Maybe Bool] -> Maybe [Bool])
-> ([[Int]] -> [Maybe Bool]) -> [[Int]] -> Maybe [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> Maybe Bool) -> [[Int]] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (JSemigroup e -> [Token] -> Maybe Bool
forall e. Ord e => JSemigroup e -> [Token] -> Maybe Bool
universallySatisfies JSemigroup e
j ([Token] -> Maybe Bool)
-> ([Int] -> [Token]) -> [Int] -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> [Int] -> [Token]
bind Token
x)
>                  ([[Int]] -> Maybe Bool) -> [[Int]] -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Map [Int] (Set [e]) -> [[Int]]
forall k a. Map k a -> [k]
Map.keys Map [Int] (Set [e])
a2s
>         [Token]
_ -> JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts' []
>     where bind :: Token -> [Int] -> [Token]
bind Token
x [Int]
a = (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\Token
t -> if Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
x then [Int] -> Token
TAction [Int]
a else Token
t) [Token]
ts
>           ts' :: [Token]
ts' = let unit :: [Int]
unit = case Map [Int] (Set [e]) -> [[Int]]
forall k a. Map k a -> [k]
Map.keys Map [Int] (Set [e])
a2s of
>                              ([Int]
m:[[Int]]
_) -> (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Int
forall a b. a -> b -> a
const [Int
0..] [Int]
m
>                              [[Int]]
_ -> []
>                 in (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\Token
t -> if Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
TUnit
>                               then (if [Int]
unit [Int] -> Map [Int] (Set [e]) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map [Int] (Set [e])
a2s
>                                     then [Int] -> Token
TAction [Int]
unit
>                                     else Token
TUnit)
>                               else Token
t) [Token]
ts
>           isVar :: Token -> Bool
isVar (TVariable Char
_) = Bool
True
>           isVar Token
_ = Bool
False

> satisfies :: JSemigroup e -> [Token] -> [Token] -> Maybe Bool
> satisfies :: forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
_ [] [Token]
_ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
> satisfies JSemigroup e
j (t :: Token
t@(TAction [Int]
_):[Token]
ts) [Token]
stack = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts (Token
tToken -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:[Token]
stack)
> satisfies JSemigroup e
j (Token
TConcat : [Token]
ts) (TAction [Int]
y : TAction [Int]
x : [Token]
stack)
>     = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction ([Int] -> [Int] -> [Int]
jsappend [Int]
x [Int]
y) Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
> satisfies JSemigroup e
j (Token
TJoin : [Token]
ts) (TAction [Int]
y : TAction [Int]
x : [Token]
stack)
>     = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction (JSemigroup e -> [Int] -> [Int] -> [Int]
forall e. JSemigroup e -> [Int] -> [Int] -> [Int]
jsjoin JSemigroup e
j [Int]
x [Int]
y) Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
> satisfies JSemigroup e
j (Token
TOmega : [Token]
ts) (TAction [Int]
x : [Token]
stack)
>     = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction ([Int] -> [Int]
jsomega [Int]
x) Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
> satisfies JSemigroup e
j (Token
TLEQ : [Token]
ts) (TAction [Int]
y : TAction [Int]
x : [Token]
stack)
>     | JSemigroup e -> [Int] -> [Int] -> [Int]
forall e. JSemigroup e -> [Int] -> [Int] -> [Int]
jsjoin JSemigroup e
j [Int]
x [Int]
y [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int]
y = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction [Int]
x Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
>     | Bool
otherwise = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
> satisfies JSemigroup e
j (Token
TEQ : [Token]
ts) (TAction [Int]
y : TAction [Int]
x : [Token]
stack)
>     | [Int]
x [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int]
y = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction [Int]
x Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
>     | Bool
otherwise = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
> satisfies JSemigroup e
j (Token
TGEQ : [Token]
ts) (TAction [Int]
y : TAction [Int]
x : [Token]
stack)
>     | JSemigroup e -> [Int] -> [Int] -> [Int]
forall e. JSemigroup e -> [Int] -> [Int] -> [Int]
jsjoin JSemigroup e
j [Int]
x [Int]
y [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int]
x = JSemigroup e -> [Token] -> [Token] -> Maybe Bool
forall e. JSemigroup e -> [Token] -> [Token] -> Maybe Bool
satisfies JSemigroup e
j [Token]
ts ([Int] -> Token
TAction [Int]
x Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
stack)
>     | Bool
otherwise = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
> satisfies JSemigroup e
_ [Token]
_ [Token]
_ = Maybe Bool
forall a. Maybe a
Nothing

> data Token = TVariable Char
>            | TAction [Int]
>            | TUnit
>            | TConcat
>            | TJoin
>            | TOmega
>            | TLEQ
>            | TEQ
>            | TGEQ
>              deriving (Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
/= :: Token -> Token -> Bool
Eq, Eq Token
Eq Token =>
(Token -> Token -> Ordering)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Token)
-> (Token -> Token -> Token)
-> Ord Token
Token -> Token -> Bool
Token -> Token -> Ordering
Token -> Token -> Token
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Token -> Token -> Ordering
compare :: Token -> Token -> Ordering
$c< :: Token -> Token -> Bool
< :: Token -> Token -> Bool
$c<= :: Token -> Token -> Bool
<= :: Token -> Token -> Bool
$c> :: Token -> Token -> Bool
> :: Token -> Token -> Bool
$c>= :: Token -> Token -> Bool
>= :: Token -> Token -> Bool
$cmax :: Token -> Token -> Token
max :: Token -> Token -> Token
$cmin :: Token -> Token -> Token
min :: Token -> Token -> Token
Ord, ReadPrec [Token]
ReadPrec Token
Int -> ReadS Token
ReadS [Token]
(Int -> ReadS Token)
-> ReadS [Token]
-> ReadPrec Token
-> ReadPrec [Token]
-> Read Token
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Token
readsPrec :: Int -> ReadS Token
$creadList :: ReadS [Token]
readList :: ReadS [Token]
$creadPrec :: ReadPrec Token
readPrec :: ReadPrec Token
$creadListPrec :: ReadPrec [Token]
readListPrec :: ReadPrec [Token]
Read, Int -> Token -> String -> String
[Token] -> String -> String
Token -> String
(Int -> Token -> String -> String)
-> (Token -> String) -> ([Token] -> String -> String) -> Show Token
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Token -> String -> String
showsPrec :: Int -> Token -> String -> String
$cshow :: Token -> String
show :: Token -> String
$cshowList :: [Token] -> String -> String
showList :: [Token] -> String -> String
Show)

> prec :: Char -> Int
> prec :: Char -> Int
prec Char
'*' = Int
10
> prec Char
'.' = Int
8
> prec Char
'+' = Int
5
> prec  Char
_  = Int
0

> -- |Make explicit any implicit concatenation.
> expand :: String -> String
> expand :: String -> String
expand (Char
x:Char
y:String
s)
>     | Bool
shouldDot = Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: Char
'.' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
expand (Char
yChar -> String -> String
forall a. a -> [a] -> [a]
:String
s)
>     | Char -> Bool
isSpace Char
x = String -> String
expand (Char
yChar -> String -> String
forall a. a -> [a] -> [a]
:String
s)
>     | Bool
otherwise = Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
expand (Char
yChar -> String -> String
forall a. a -> [a] -> [a]
:String
s)
>     where shouldDot :: Bool
shouldDot = (Char -> Bool
isLetter Char
x Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'*' Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')')
>                       Bool -> Bool -> Bool
&& (Char -> Bool
isLetter Char
y Bool -> Bool -> Bool
|| Char
y Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(')
> expand String
s = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace) String
s

> shunt :: String -> [Char] -> Maybe [Token]
> shunt :: String -> String -> Maybe [Token]
shunt String
"" [] = [Token] -> Maybe [Token]
forall a. a -> Maybe a
Just []
> shunt String
"" (Char
s:String
ss) = (:) (Token -> [Token] -> [Token])
-> Maybe Token -> Maybe ([Token] -> [Token])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Char -> Maybe Token
tokenify Char
s Maybe ([Token] -> [Token]) -> Maybe [Token] -> Maybe [Token]
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> String -> Maybe [Token]
shunt String
"" String
ss
> shunt (Char
x:String
xs) String
stack
>     | Char -> Bool
isLetter Char
x = (Char -> Token
TVariable Char
x Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:) ([Token] -> [Token]) -> Maybe [Token] -> Maybe [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> Maybe [Token]
shunt String
xs String
stack
>     | Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'1' = (Token
TUnit Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:) ([Token] -> [Token]) -> Maybe [Token] -> Maybe [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> Maybe [Token]
shunt String
xs String
stack
>     | Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(' = String -> String -> Maybe [Token]
shunt String
xs (Char
'('Char -> String -> String
forall a. a -> [a] -> [a]
:String
stack)
>     | Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' = let (String
ops,String
s) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(') String
stack
>                  in case String
s of
>                       (Char
'(':String
ss) -> [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
(++) ([Token] -> [Token] -> [Token])
-> Maybe [Token] -> Maybe ([Token] -> [Token])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe [Token]
flush String
ops Maybe ([Token] -> [Token]) -> Maybe [Token] -> Maybe [Token]
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> String -> Maybe [Token]
shunt String
xs String
ss
>                       String
_ -> Maybe [Token]
forall a. Maybe a
Nothing
>     | Char -> Int
prec Char
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = if Char
'(' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
stack then Maybe [Token]
forall a. Maybe a
Nothing else Maybe [Token]
go
>     | Bool
otherwise = Maybe [Token]
go
>     where flush :: String -> Maybe [Token]
flush = [Maybe Token] -> Maybe [Token]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA ([Maybe Token] -> Maybe [Token])
-> (String -> [Maybe Token]) -> String -> Maybe [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Maybe Token) -> String -> [Maybe Token]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Maybe Token
tokenify
>           go :: Maybe [Token]
go = let (String
tighter,String
s) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Char
p -> Char -> Int
prec Char
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Char -> Int
prec Char
x) String
stack
>                in [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
(++) ([Token] -> [Token] -> [Token])
-> Maybe [Token] -> Maybe ([Token] -> [Token])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe [Token]
flush String
tighter Maybe ([Token] -> [Token]) -> Maybe [Token] -> Maybe [Token]
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> String -> Maybe [Token]
shunt String
xs (Char
xChar -> String -> String
forall a. a -> [a] -> [a]
:String
s)

> tokenify :: Char -> Maybe Token
> tokenify :: Char -> Maybe Token
tokenify Char
'*' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TOmega
> tokenify Char
'+' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TJoin
> tokenify Char
'<' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TLEQ
> tokenify Char
'≤' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TLEQ
> tokenify Char
'=' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TEQ
> tokenify Char
'≥' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TGEQ
> tokenify Char
'>' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TGEQ
> tokenify Char
'.' = Token -> Maybe Token
forall a. a -> Maybe a
Just Token
TConcat
> tokenify  Char
_  = Maybe Token
forall a. Maybe a
Nothing


Helpers
=======

> splitOn :: Eq a => a -> [a] -> [[a]]
> splitOn :: forall a. Eq a => a -> [a] -> [[a]]
splitOn a
x [a]
xs = let ([a]
a,[a]
b) = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs
>                in if [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
b then [[a]
a] else [a]
a [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: a -> [a] -> [[a]]
forall a. Eq a => a -> [a] -> [[a]]
splitOn a
x (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 [a]
b)