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

> This module provides a general mechanism
> for constructing decision procedures
> given an equational characterization of a pseudovariety.
> One parses the collection of equations,
> quantifies universally over the bound variables,
> and determines whether all specified relationships hold.
>
> @since 1.1
> -}

> module LTK.Decide.Variety ( -- * Documentation
>                             -- $doc
>                             isVariety
>                           , isVarietyM) where

> import Data.Char (isSpace)
> import Data.Maybe (isJust,maybeToList)
> import Data.Set (Set)
> import qualified Data.Set as Set

> import LTK.FSA
> import LTK.Algebra (SynMon, omega)

> {- $doc
> A (pseudo)variety is specified here by a system of equations.
> These equations may contain (single-letter) variables,
> which are universally quantified.
> The grammar is as follows:

> >      expr ::= '[' conj-list ']'
> > conj-list ::= eq-list ';' conj-list | eq-list
> >   eq-list ::= value '=' eq-list | value '=' value
> >     value ::= value value | iter
> >      iter ::= '0' | '1' | LETTER | '(' value ')' | iter '*'

> Here, @LETTER@ refers to any character which Unicode deems a letter.
> Concatenation is denoted by adjacency,
> and @x*@ represents the unique element of the form
> @x@, @xx@, and so on, such that @x*x*=x*@.
> A @LETTER@ represents a universally-quantified variable,
> while @0@ and @1@ refer to the unique elements where for all @x@
> it holds that @0x=0=x0@ and @1x=x=x1@,
> if such elements exist.
> If @0@ or @1@ is used in an equation,
> but the given structure lacks such an element,
> then the structure of course does not satisfy the equality.

> The equality @x=y@ asserts that,
> for all possible variable instantiations,
> the value of @x@ is the same as that of @y@.
> For longer chains of equality, all values must be equal.
> Then @[e1;e2]@ asserts that the equalities @e1@ and @e2@
> both hold universally.
> Essentially, the semicolon is an "and" operator.

> Suppose we wish to express the *-variety
> of idempotent and commutative monoids.
> A monoid is idempotent if and only if it holds that @xx=x@
> for all values @x@, which can also be expressed as @x*=x@.
> It is commutative if and only if @ab=ba@ for all @a@ and @b@.
> This variety could then be expressed as @[ab=ba;x*=x]@.
> -}

We shall assume that we are working with forests
wherein each tree represents a set of equalities that must hold
and all variables are universally quantified.
Variables are formal and represented only by integer indices.

> data VEquality a = VEquality (VEx a) [VEx a]
>                    deriving (VEquality a -> VEquality a -> Bool
forall a. Eq a => VEquality a -> VEquality a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VEquality a -> VEquality a -> Bool
$c/= :: forall a. Eq a => VEquality a -> VEquality a -> Bool
== :: VEquality a -> VEquality a -> Bool
$c== :: forall a. Eq a => VEquality a -> VEquality a -> Bool
Eq, VEquality a -> VEquality a -> Bool
VEquality a -> VEquality a -> Ordering
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
forall {a}. Ord a => Eq (VEquality a)
forall a. Ord a => VEquality a -> VEquality a -> Bool
forall a. Ord a => VEquality a -> VEquality a -> Ordering
forall a. Ord a => VEquality a -> VEquality a -> VEquality a
min :: VEquality a -> VEquality a -> VEquality a
$cmin :: forall a. Ord a => VEquality a -> VEquality a -> VEquality a
max :: VEquality a -> VEquality a -> VEquality a
$cmax :: forall a. Ord a => VEquality a -> VEquality a -> VEquality a
>= :: VEquality a -> VEquality a -> Bool
$c>= :: forall a. Ord a => VEquality a -> VEquality a -> Bool
> :: VEquality a -> VEquality a -> Bool
$c> :: forall a. Ord a => VEquality a -> VEquality a -> Bool
<= :: VEquality a -> VEquality a -> Bool
$c<= :: forall a. Ord a => VEquality a -> VEquality a -> Bool
< :: VEquality a -> VEquality a -> Bool
$c< :: forall a. Ord a => VEquality a -> VEquality a -> Bool
compare :: VEquality a -> VEquality a -> Ordering
$ccompare :: forall a. Ord a => VEquality a -> VEquality a -> Ordering
Ord, ReadPrec [VEquality a]
ReadPrec (VEquality a)
ReadS [VEquality a]
forall a. Read a => ReadPrec [VEquality a]
forall a. Read a => ReadPrec (VEquality a)
forall a. Read a => Int -> ReadS (VEquality a)
forall a. Read a => ReadS [VEquality a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [VEquality a]
$creadListPrec :: forall a. Read a => ReadPrec [VEquality a]
readPrec :: ReadPrec (VEquality a)
$creadPrec :: forall a. Read a => ReadPrec (VEquality a)
readList :: ReadS [VEquality a]
$creadList :: forall a. Read a => ReadS [VEquality a]
readsPrec :: Int -> ReadS (VEquality a)
$creadsPrec :: forall a. Read a => Int -> ReadS (VEquality a)
Read, Int -> VEquality a -> ShowS
forall a. Show a => Int -> VEquality a -> ShowS
forall a. Show a => [VEquality a] -> ShowS
forall a. Show a => VEquality a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VEquality a] -> ShowS
$cshowList :: forall a. Show a => [VEquality a] -> ShowS
show :: VEquality a -> String
$cshow :: forall a. Show a => VEquality a -> String
showsPrec :: Int -> VEquality a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> VEquality a -> ShowS
Show)
> data VEx a = VVar Integer
>            | VOmega (VEx a)
>            | VConcat (VEx a) [VEx a]
>            | VOne
>            | VZero
>            | VElement a
>              deriving (VEx a -> VEx a -> Bool
forall a. Eq a => VEx a -> VEx a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VEx a -> VEx a -> Bool
$c/= :: forall a. Eq a => VEx a -> VEx a -> Bool
== :: VEx a -> VEx a -> Bool
$c== :: forall a. Eq a => VEx a -> VEx a -> Bool
Eq, VEx a -> VEx a -> Ordering
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
forall {a}. Ord a => Eq (VEx a)
forall a. Ord a => VEx a -> VEx a -> Bool
forall a. Ord a => VEx a -> VEx a -> Ordering
forall a. Ord a => VEx a -> VEx a -> VEx a
min :: VEx a -> VEx a -> VEx a
$cmin :: forall a. Ord a => VEx a -> VEx a -> VEx a
max :: VEx a -> VEx a -> VEx a
$cmax :: forall a. Ord a => VEx a -> VEx a -> VEx a
>= :: VEx a -> VEx a -> Bool
$c>= :: forall a. Ord a => VEx a -> VEx a -> Bool
> :: VEx a -> VEx a -> Bool
$c> :: forall a. Ord a => VEx a -> VEx a -> Bool
<= :: VEx a -> VEx a -> Bool
$c<= :: forall a. Ord a => VEx a -> VEx a -> Bool
< :: VEx a -> VEx a -> Bool
$c< :: forall a. Ord a => VEx a -> VEx a -> Bool
compare :: VEx a -> VEx a -> Ordering
$ccompare :: forall a. Ord a => VEx a -> VEx a -> Ordering
Ord, ReadPrec [VEx a]
ReadPrec (VEx a)
ReadS [VEx a]
forall a. Read a => ReadPrec [VEx a]
forall a. Read a => ReadPrec (VEx a)
forall a. Read a => Int -> ReadS (VEx a)
forall a. Read a => ReadS [VEx a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [VEx a]
$creadListPrec :: forall a. Read a => ReadPrec [VEx a]
readPrec :: ReadPrec (VEx a)
$creadPrec :: forall a. Read a => ReadPrec (VEx a)
readList :: ReadS [VEx a]
$creadList :: forall a. Read a => ReadS [VEx a]
readsPrec :: Int -> ReadS (VEx a)
$creadsPrec :: forall a. Read a => Int -> ReadS (VEx a)
Read, Int -> VEx a -> ShowS
forall a. Show a => Int -> VEx a -> ShowS
forall a. Show a => [VEx a] -> ShowS
forall a. Show a => VEx a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VEx a] -> ShowS
$cshowList :: forall a. Show a => [VEx a] -> ShowS
show :: VEx a -> String
$cshow :: forall a. Show a => VEx a -> String
showsPrec :: Int -> VEx a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> VEx a -> ShowS
Show)

The VOne and VZero expressions stand in for a neutral element and a zero,
respectively, in the senses typical when discussion semigroups.
VConcat represents the semigroup's multiplication.
And finally, VOmega represents the omega operator, \(x^{\omega}\),
the unique idempotent power of \(x\).

The end goal is a function to decide whether a collection of equalities
always holds true for all possible instantiations:

> satisfiedUniversally :: Eq a => (a -> a -> a) -> (a -> a)
>                      -> Maybe a -> Maybe a -> [a]
>                      -> [VEquality a] -> Bool
> satisfiedUniversally :: forall a.
Eq a =>
(a -> a -> a)
-> (a -> a) -> Maybe a -> Maybe a -> [a] -> [VEquality a] -> Bool
satisfiedUniversally a -> a -> a
cat a -> a
star Maybe a
zero Maybe a
one [a]
xs [VEquality a]
vs'
>     = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False [VEquality a] -> Bool
f Maybe [VEquality a]
vs
>     where f :: [VEquality a] -> Bool
f = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Eq a => VEquality a -> Bool
evaluate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a.
(a -> a -> a)
-> (a -> a) -> [a] -> Integer -> VEquality a -> [VEquality a]
instantiations a -> a -> a
cat a -> a
star [a]
xs Integer
0)
>           vs :: Maybe [VEquality a]
vs = forall a b. (a -> Maybe b) -> [a] -> Maybe [b]
splatMap (forall a. Maybe a -> Maybe a -> VEquality a -> Maybe (VEquality a)
fillzo Maybe a
zero Maybe a
one) [VEquality a]
vs'

We then can use this to decide membership in a variety.

> -- |Determine whether a given semigroup is in the pseudovariety
> -- described by the given equation set.
> -- Returns Nothing if and only if the equation set cannot be parsed.
> -- The Boolean operand determines whether
> -- to check for a *-variety (True) or a +-variety (False).
> -- In other words, it determines whether the class containing
> -- the empty string is included.
> isVarietyM :: (Ord n, Ord e) => Bool -> String -> SynMon n e
>            -> Maybe Bool
> isVarietyM :: forall n e.
(Ord n, Ord e) =>
Bool -> String -> SynMon n e -> Maybe Bool
isVarietyM Bool
star String
desc SynMon n e
m
>     = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {b}. Maybe [VEquality b]
v
>       forall a b. (a -> b) -> a -> b
$ forall a.
Eq a =>
(a -> a -> a)
-> (a -> a) -> Maybe a -> Maybe a -> [a] -> [VEquality a] -> Bool
satisfiedUniversally (forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m) (forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
m) Maybe (State ([Maybe n], [Symbol e]))
zero Maybe (State ([Maybe n], [Symbol e]))
one [State ([Maybe n], [Symbol e])]
qs
>     where zero :: Maybe (State ([Maybe n], [Symbol e]))
zero = forall n e.
(Ord n, Ord e) =>
Bool -> SynMon n e -> Maybe (State ([Maybe n], [Symbol e]))
findZero Bool
star SynMon n e
m
>           one :: Maybe (State ([Maybe n], [Symbol e]))
one  = forall n e.
(Ord n, Ord e) =>
Bool -> SynMon n e -> Maybe (State ([Maybe n], [Symbol e]))
findOne  Bool
star SynMon n e
m
>           sts :: Set (State ([Maybe n], [Symbol e]))
sts  = if Bool
star
>                  then forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
m
>                  else forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions SynMon n e
m
>           qs :: [State ([Maybe n], [Symbol e])]
qs   = forall a. Set a -> [a]
Set.toList Set (State ([Maybe n], [Symbol e]))
sts
>           v :: Maybe [VEquality b]
v    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. Eq a => a -> a -> ETree a -> [VEquality b]
transform Char
'0' Char
'1') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [[Cell Char]] -> String -> (Maybe (ETree Char), String)
ckyParse [] String
desc

> -- |The @isVariety star desc@ function is equivalent to
> -- @isVarietyM star desc . syntacticMonoid@.
> isVariety :: (Ord n, Ord e) => Bool -> String -> FSA n e -> Maybe Bool
> isVariety :: forall n e.
(Ord n, Ord e) =>
Bool -> String -> FSA n e -> Maybe Bool
isVariety Bool
star String
desc = forall n e.
(Ord n, Ord e) =>
Bool -> String -> SynMon n e -> Maybe Bool
isVarietyM Bool
star String
desc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid

In order to make this actually work, we shall attempt,
for each chain of equalities, to find a counterexample.
The first step is to actually instantiate any zeros or ones.
If they are used in the equalities but do not exist,
then clearly the system cannot hold true.

> fillzo :: Maybe a -> Maybe a -> VEquality a -> Maybe (VEquality a)
> fillzo :: forall a. Maybe a -> Maybe a -> VEquality a -> Maybe (VEquality a)
fillzo Maybe a
zero Maybe a
one (VEquality VEx a
v [VEx a]
vs)
>     = forall a. VEx a -> [VEx a] -> VEquality a
VEquality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VEx a -> Maybe (VEx a)
fill VEx a
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. (a -> Maybe b) -> [a] -> Maybe [b]
splatMap VEx a -> Maybe (VEx a)
fill [VEx a]
vs
>     where fill :: VEx a -> Maybe (VEx a)
fill (VOmega VEx a
x) = forall a. VEx a -> VEx a
VOmega forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VEx a -> Maybe (VEx a)
fill VEx a
x
>           fill (VConcat VEx a
x [VEx a]
y) = forall a. VEx a -> [VEx a] -> VEx a
VConcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VEx a -> Maybe (VEx a)
fill VEx a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. (a -> Maybe b) -> [a] -> Maybe [b]
splatMap VEx a -> Maybe (VEx a)
fill [VEx a]
y
>           fill VEx a
VOne = forall a. a -> VEx a
VElement forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
one
>           fill VEx a
VZero = forall a. a -> VEx a
VElement forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
zero
>           fill VEx a
x = forall a. a -> Maybe a
Just VEx a
x

Next, we'd like a way to evaluate any levels of the tree
whose children are fully concrete into something concrete.

> mkconcrete :: (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
> mkconcrete :: forall a. (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
mkconcrete a -> a -> a
cat a -> a
star (VOmega VEx a
x)
>     = case forall a. (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
mkconcrete a -> a -> a
cat a -> a
star VEx a
x of
>         VElement a
e -> forall a. a -> VEx a
VElement forall a b. (a -> b) -> a -> b
$ a -> a
star a
e
>         VEx a
y -> forall a. VEx a -> VEx a
VOmega VEx a
y
> mkconcrete a -> a -> a
cat a -> a
star (VConcat VEx a
x [VEx a]
xs) = VEx a -> [VEx a] -> VEx a
f (VEx a -> VEx a
m VEx a
x) (forall a b. (a -> b) -> [a] -> [b]
map VEx a -> VEx a
m [VEx a]
xs)
>     where f :: VEx a -> [VEx a] -> VEx a
f (VElement a
y) [VEx a]
ys
>               = case [VEx a]
ys of
>                   VElement a
z : [VEx a]
zs  ->  VEx a -> [VEx a] -> VEx a
f (forall a. a -> VEx a
VElement forall a b. (a -> b) -> a -> b
$ a -> a -> a
cat a
y a
z) [VEx a]
zs
>                   []               ->  forall a. a -> VEx a
VElement a
y
>                   [VEx a]
_                ->  forall a. VEx a -> [VEx a] -> VEx a
VConcat (forall a. a -> VEx a
VElement a
y) [VEx a]
ys
>           f VEx a
y [VEx a]
ys = forall a. VEx a -> [VEx a] -> VEx a
VConcat VEx a
y [VEx a]
ys
>           m :: VEx a -> VEx a
m = forall a. (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
mkconcrete a -> a -> a
cat a -> a
star
> mkconcrete a -> a -> a
_ a -> a
_ VEx a
v = VEx a
v

Given a set of elements,
we'd like to instantiate every possible assignment of variables,
until either a counterexample is found or all options are exhausted.
We'll start by instantiating a single given variable to a value

> instantiate :: (a -> a -> a) -> (a -> a) -> a
>             -> Integer -> VEquality a -> VEquality a
> instantiate :: forall a.
(a -> a -> a)
-> (a -> a) -> a -> Integer -> VEquality a -> VEquality a
instantiate a -> a -> a
cat a -> a
star a
x Integer
n (VEquality VEx a
v [VEx a]
vs) = forall a. VEx a -> [VEx a] -> VEquality a
VEquality (VEx a -> VEx a
f VEx a
v) (forall a b. (a -> b) -> [a] -> [b]
map VEx a -> VEx a
f [VEx a]
vs)
>     where mkc :: VEx a -> VEx a
mkc = forall a. (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
mkconcrete a -> a -> a
cat a -> a
star
>           f :: VEx a -> VEx a
f (VOmega VEx a
a) = VEx a -> VEx a
mkc forall a b. (a -> b) -> a -> b
$ forall a. VEx a -> VEx a
VOmega (VEx a -> VEx a
f VEx a
a)
>           f (VConcat VEx a
a [VEx a]
b) = VEx a -> VEx a
mkc forall a b. (a -> b) -> a -> b
$ forall a. VEx a -> [VEx a] -> VEx a
VConcat (VEx a -> VEx a
f VEx a
a) (forall a b. (a -> b) -> [a] -> [b]
map VEx a -> VEx a
f [VEx a]
b)
>           f (VVar Integer
m) = if Integer
m forall a. Eq a => a -> a -> Bool
== Integer
n then forall a. a -> VEx a
VElement a
x else forall a. Integer -> VEx a
VVar Integer
m
>           f VEx a
a = VEx a
a

As long as there are variables remaining,
we'd like to instantiate another variable.

> instantiations :: (a -> a -> a) -> (a -> a) -> [a]
>                -> Integer -> VEquality a -> [VEquality a]
> instantiations :: forall a.
(a -> a -> a)
-> (a -> a) -> [a] -> Integer -> VEquality a -> [VEquality a]
instantiations a -> a -> a
cat a -> a
star [a]
xs Integer
n (VEquality VEx a
v' [VEx a]
vs')
>     = if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {a}. VEx a -> Bool
concrete (VEx a
mvforall a. a -> [a] -> [a]
:[VEx a]
mvs) then [VEquality a
v] else forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [VEquality a]
f [a]
xs
>     where concrete :: VEx a -> Bool
concrete (VElement a
_) = Bool
True
>           concrete VEx a
_ = Bool
False
>           m :: VEx a -> VEx a
m = forall a. (a -> a -> a) -> (a -> a) -> VEx a -> VEx a
mkconcrete a -> a -> a
cat a -> a
star
>           mv :: VEx a
mv = VEx a -> VEx a
m VEx a
v'
>           mvs :: [VEx a]
mvs = forall a b. (a -> b) -> [a] -> [b]
map VEx a -> VEx a
m [VEx a]
vs'
>           v :: VEquality a
v = forall a. VEx a -> [VEx a] -> VEquality a
VEquality VEx a
mv [VEx a]
mvs
>           f :: a -> [VEquality a]
f a
x = forall a.
(a -> a -> a)
-> (a -> a) -> [a] -> Integer -> VEquality a -> [VEquality a]
instantiations a -> a -> a
cat a -> a
star [a]
xs (Integer
nforall a. Num a => a -> a -> a
+Integer
1)
>                 forall a b. (a -> b) -> a -> b
$ forall a.
(a -> a -> a)
-> (a -> a) -> a -> Integer -> VEquality a -> VEquality a
instantiate a -> a -> a
cat a -> a
star a
x Integer
n VEquality a
v

An equality holds if and only if all of the elements are equal.

> evaluate :: Eq a => VEquality a -> Bool
> evaluate :: forall a. Eq a => VEquality a -> Bool
evaluate (VEquality VEx a
x [VEx a]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== VEx a
x) [VEx a]
xs



Parsing Simply: CKY
===================

> data ETag = EXPR | CLOSE_EXP
>           | CONJ_LIST | CONJUNCT
>           | EQ_LIST | ELEM_EQ
>           | ITER | ELEM | CLOSE_EL
>           | SOE | EOE | OPEN | CLOSE | AND | EQU | OMEGA
>             deriving (ETag -> ETag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ETag -> ETag -> Bool
$c/= :: ETag -> ETag -> Bool
== :: ETag -> ETag -> Bool
$c== :: ETag -> ETag -> Bool
Eq, Eq ETag
ETag -> ETag -> Bool
ETag -> ETag -> Ordering
ETag -> ETag -> ETag
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
min :: ETag -> ETag -> ETag
$cmin :: ETag -> ETag -> ETag
max :: ETag -> ETag -> ETag
$cmax :: ETag -> ETag -> ETag
>= :: ETag -> ETag -> Bool
$c>= :: ETag -> ETag -> Bool
> :: ETag -> ETag -> Bool
$c> :: ETag -> ETag -> Bool
<= :: ETag -> ETag -> Bool
$c<= :: ETag -> ETag -> Bool
< :: ETag -> ETag -> Bool
$c< :: ETag -> ETag -> Bool
compare :: ETag -> ETag -> Ordering
$ccompare :: ETag -> ETag -> Ordering
Ord, ReadPrec [ETag]
ReadPrec ETag
Int -> ReadS ETag
ReadS [ETag]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ETag]
$creadListPrec :: ReadPrec [ETag]
readPrec :: ReadPrec ETag
$creadPrec :: ReadPrec ETag
readList :: ReadS [ETag]
$creadList :: ReadS [ETag]
readsPrec :: Int -> ReadS ETag
$creadsPrec :: Int -> ReadS ETag
Read, Int -> ETag -> ShowS
[ETag] -> ShowS
ETag -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ETag] -> ShowS
$cshowList :: [ETag] -> ShowS
show :: ETag -> String
$cshow :: ETag -> String
showsPrec :: Int -> ETag -> ShowS
$cshowsPrec :: Int -> ETag -> ShowS
Show)
> data ETree a = Leaf ETag
>              | VLeaf a ETag
>              | Node ETag (ETree a) (ETree a)
>                deriving (ETree a -> ETree a -> Bool
forall a. Eq a => ETree a -> ETree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ETree a -> ETree a -> Bool
$c/= :: forall a. Eq a => ETree a -> ETree a -> Bool
== :: ETree a -> ETree a -> Bool
$c== :: forall a. Eq a => ETree a -> ETree a -> Bool
Eq, ETree a -> ETree a -> Bool
ETree a -> ETree a -> Ordering
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
forall {a}. Ord a => Eq (ETree a)
forall a. Ord a => ETree a -> ETree a -> Bool
forall a. Ord a => ETree a -> ETree a -> Ordering
forall a. Ord a => ETree a -> ETree a -> ETree a
min :: ETree a -> ETree a -> ETree a
$cmin :: forall a. Ord a => ETree a -> ETree a -> ETree a
max :: ETree a -> ETree a -> ETree a
$cmax :: forall a. Ord a => ETree a -> ETree a -> ETree a
>= :: ETree a -> ETree a -> Bool
$c>= :: forall a. Ord a => ETree a -> ETree a -> Bool
> :: ETree a -> ETree a -> Bool
$c> :: forall a. Ord a => ETree a -> ETree a -> Bool
<= :: ETree a -> ETree a -> Bool
$c<= :: forall a. Ord a => ETree a -> ETree a -> Bool
< :: ETree a -> ETree a -> Bool
$c< :: forall a. Ord a => ETree a -> ETree a -> Bool
compare :: ETree a -> ETree a -> Ordering
$ccompare :: forall a. Ord a => ETree a -> ETree a -> Ordering
Ord, ReadPrec [ETree a]
ReadPrec (ETree a)
ReadS [ETree a]
forall a. Read a => ReadPrec [ETree a]
forall a. Read a => ReadPrec (ETree a)
forall a. Read a => Int -> ReadS (ETree a)
forall a. Read a => ReadS [ETree a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ETree a]
$creadListPrec :: forall a. Read a => ReadPrec [ETree a]
readPrec :: ReadPrec (ETree a)
$creadPrec :: forall a. Read a => ReadPrec (ETree a)
readList :: ReadS [ETree a]
$creadList :: forall a. Read a => ReadS [ETree a]
readsPrec :: Int -> ReadS (ETree a)
$creadsPrec :: forall a. Read a => Int -> ReadS (ETree a)
Read, Int -> ETree a -> ShowS
forall a. Show a => Int -> ETree a -> ShowS
forall a. Show a => [ETree a] -> ShowS
forall a. Show a => ETree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ETree a] -> ShowS
$cshowList :: forall a. Show a => [ETree a] -> ShowS
show :: ETree a -> String
$cshow :: forall a. Show a => ETree a -> String
showsPrec :: Int -> ETree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ETree a -> ShowS
Show)

> tag :: ETree a -> ETag
> tag :: forall a. ETree a -> ETag
tag (Leaf ETag
x) = ETag
x
> tag (VLeaf a
_ ETag
x) = ETag
x
> tag (Node ETag
x ETree a
_ ETree a
_) = ETag
x

There is a one-to-one mapping between tokens and symbols;
use that and we don't need a tokenizer.
We'll allow for whitespace in expressions
by simply stripping it before parsing.

> mkunary :: Char -> [ETree Char]
> mkunary :: Char -> Cell Char
mkunary Char
x = case Char
x of
>               Char
'[' -> [forall a. ETag -> ETree a
Leaf ETag
SOE]
>               Char
']' -> [forall a. ETag -> ETree a
Leaf ETag
EOE]
>               Char
'(' -> [forall a. ETag -> ETree a
Leaf ETag
OPEN]
>               Char
')' -> [forall a. ETag -> ETree a
Leaf ETag
CLOSE]
>               Char
';' -> [forall a. ETag -> ETree a
Leaf ETag
AND]
>               Char
'=' -> [forall a. ETag -> ETree a
Leaf ETag
EQU]
>               Char
'*' -> [forall a. ETag -> ETree a
Leaf ETag
OMEGA]
>               Char
_   -> [ forall a. a -> ETag -> ETree a
VLeaf Char
x ETag
ITER
>                      , forall a. a -> ETag -> ETree a
VLeaf Char
x ETag
ELEM
>                      ]

The combine function handles the binary branches in our CNF.

> combine :: ETree a -> ETree a -> [ETree a]
> combine :: forall a. ETree a -> ETree a -> [ETree a]
combine ETree a
x ETree a
y = forall a b. (a -> b) -> [a] -> [b]
map (\ETag
t -> forall a. ETag -> ETree a -> ETree a -> ETree a
Node ETag
t ETree a
x ETree a
y)
>               forall a b. (a -> b) -> a -> b
$ case (forall a. ETree a -> ETag
tag ETree a
x, forall a. ETree a -> ETag
tag ETree a
y) of
>                   (ETag
SOE,        ETag
CLOSE_EXP)  ->  [ETag
EXPR]
>                   (ETag
CONJ_LIST,  ETag
EOE)        ->  [ETag
CLOSE_EXP]
>                   (ETag
EQ_LIST,    ETag
EOE)        ->  [ETag
CLOSE_EXP]
>                   (ETag
CONJUNCT,   ETag
CONJ_LIST)  ->  [ETag
CONJ_LIST]
>                   (ETag
CONJUNCT,   ETag
EQ_LIST)    ->  [ETag
CONJ_LIST]
>                   (ETag
EQ_LIST,    ETag
AND)        ->  [ETag
CONJUNCT]
>                   (ETag
ELEM_EQ,    ETag
EQ_LIST)    ->  [ETag
EQ_LIST]
>                   (ETag
ELEM_EQ,    ETag
ELEM)       ->  [ETag
EQ_LIST]
>                   (ETag
ELEM,       ETag
EQU)        ->  [ETag
ELEM_EQ]
>                   (ETag
ELEM,       ETag
ELEM)       ->  [ETag
ELEM]
>                   (ETag
ITER,       ETag
OMEGA)      ->  [ETag
ITER, ETag
ELEM]
>                   (ETag
OPEN,       ETag
CLOSE_EL)   ->  [ETag
ITER, ETag
ELEM]
>                   (ETag
ELEM,       ETag
CLOSE)      ->  [ETag
CLOSE_EL]
>                   (ETag, ETag)
_                        ->  []

With that out of the way, we now have a complete grammar for expressions.
As the grammar is CNF, we can incrementally parse with CKY.
We'll grab the smallest expression out of a stream of input characters
and return the remainder.

> type Cell a = [ETree a]
> ckyExtend :: Cell a -> [[Cell a]] -> [[Cell a]]
> ckyExtend :: forall a. Cell a -> [[Cell a]] -> [[Cell a]]
ckyExtend Cell a
a [[Cell a]]
xs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (:) [Cell a]
nexts ([] forall a. a -> [a] -> [a]
: [[Cell a]]
xs)
>     where nexts :: [Cell a]
nexts = Cell a
a forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map [Cell a] -> Cell a
f [[Cell a]]
xs
>           f :: [Cell a] -> Cell a
f [Cell a]
x = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Cell a -> Cell a -> Cell a
combineCells [Cell a]
nexts [Cell a]
x

> combineCells :: Cell a -> Cell a -> Cell a
> combineCells :: forall a. Cell a -> Cell a -> Cell a
combineCells Cell a
q Cell a
p = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. ETree a -> ETree a -> [ETree a]
combine) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
cartesian Cell a
p Cell a
q

> extractExpr :: [[Cell a]] -> Maybe (ETree a)
> extractExpr :: forall a. [[Cell a]] -> Maybe (ETree a)
extractExpr [] = forall a. Maybe a
Nothing
> extractExpr [[Cell a]]
t = forall {a}. [[ETree a]] -> Maybe (ETree a)
extract (forall a. [a] -> a
last [[Cell a]]
t)
>     where extract :: [[ETree a]] -> Maybe (ETree a)
extract [] = forall a. Maybe a
Nothing
>           extract ([ETree a]
x:[[ETree a]]
_) = case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== ETag
EXPR) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ETree a -> ETag
tag) [ETree a]
x of
>                             (ETree a
e:[ETree a]
_)  ->  forall a. a -> Maybe a
Just ETree a
e
>                             [ETree a]
_      ->  forall a. Maybe a
Nothing

> ckyParse :: [[Cell Char]] -> String -> (Maybe (ETree Char), String)
> ckyParse :: [[Cell Char]] -> String -> (Maybe (ETree Char), String)
ckyParse [[Cell Char]]
t [] = (forall a. [[Cell a]] -> Maybe (ETree a)
extractExpr [[Cell Char]]
t, [])
> ckyParse [[Cell Char]]
t (Char
x:String
xs)
>     | forall a. Maybe a -> Bool
isJust Maybe (ETree Char)
output  =  (Maybe (ETree Char)
output, Char
xforall a. a -> [a] -> [a]
:String
xs)
>     | Char -> Bool
isSpace Char
x      =  [[Cell Char]] -> (Maybe (ETree Char), String)
try [[Cell Char]]
t
>     | Bool
otherwise      =  [[Cell Char]] -> (Maybe (ETree Char), String)
try forall a b. (a -> b) -> a -> b
$ forall a. Cell a -> [[Cell a]] -> [[Cell a]]
ckyExtend (Char -> Cell Char
mkunary Char
x) [[Cell Char]]
t
>     where output :: Maybe (ETree Char)
output = forall a. [[Cell a]] -> Maybe (ETree a)
extractExpr [[Cell Char]]
t
>           try :: [[Cell Char]] -> (Maybe (ETree Char), String)
try [[Cell Char]]
t' = let ~(Maybe (ETree Char)
me, String
s) = [[Cell Char]] -> String -> (Maybe (ETree Char), String)
ckyParse [[Cell Char]]
t' String
xs
>                    in case Maybe (ETree Char)
me of
>                         Maybe (ETree Char)
Nothing  ->  (Maybe (ETree Char)
me, Char
xforall a. a -> [a] -> [a]
:String
xs)
>                         Maybe (ETree Char)
_        ->  (Maybe (ETree Char)
me, String
s)

To parse a string @s@, call @ckyParse [] s@.



The preceding CNF generates a grammar that is easy to parse,
but not necessarily easy to compute with.
Here we transform these trees into our originally-specified forests
wherein the trees are better suited for computation.

For each equality we'll be doing variable renaming.
Rather than carrying around arbitrary symbols,
we use formal variables numbered consecutively from 0.
Then we would say that [ab=ba;x*=x] truly uses only two variables,
rather than the three that one might first expect.

> vars :: Eq a => [a] -> ETree a -> [a]
> vars :: forall a. Eq a => [a] -> ETree a -> [a]
vars [a]
excl (Node ETag
_ ETree a
x ETree a
y)
>     = let v :: [a]
v = forall a. Eq a => [a] -> ETree a -> [a]
vars [a]
excl ETree a
x
>       in [a]
v forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
v) (forall a. Eq a => [a] -> ETree a -> [a]
vars [a]
excl ETree a
y)
> vars [a]
excl (VLeaf a
a ETag
_) = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
excl) [a
a]
> vars [a]
_ ETree a
_  = []

Now we are ready to translate between the tree formats.
At a high level, we either have a single equality
or a conjunction of several.
Each equality becomes a tree, and the whole is a forest.

> transform :: Eq a => a -> a -> ETree a -> [VEquality b]
> transform :: forall a b. Eq a => a -> a -> ETree a -> [VEquality b]
transform a
zero a
one ETree a
e
>     = case ETree a
e of
>         (Node ETag
EXPR ETree a
_ (Node ETag
CLOSE_EXP ETree a
x ETree a
_))
>             -> case forall a. ETree a -> ETag
tag ETree a
x of
>                  ETag
CONJ_LIST -> forall a b. Eq a => a -> a -> ETree a -> [VEquality b]
forestFromConjList a
zero a
one ETree a
x
>                  ETag
EQ_LIST -> forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> a -> ETree a -> Maybe (VEquality b)
treeFromEqList a
zero a
one ETree a
x
>                  ETag
_ -> []
>         ETree a
_ -> []

> forestFromConjList :: Eq a => a -> a -> ETree a -> [VEquality b]
> forestFromConjList :: forall a b. Eq a => a -> a -> ETree a -> [VEquality b]
forestFromConjList a
zero a
one ETree a
t
>     = case ETree a
t of
>         (Node ETag
CONJ_LIST (Node ETag
CONJUNCT ETree a
x ETree a
_) ETree a
y)
>             -> case forall a. ETree a -> ETag
tag ETree a
y of
>                  ETag
CONJ_LIST -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. a -> [a] -> [a]
: forall a b. Eq a => a -> a -> ETree a -> [VEquality b]
forestFromConjList a
zero a
one ETree a
y)
>                               forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> a -> ETree a -> Maybe (VEquality b)
treeFromEqList a
zero a
one ETree a
x
>                  ETag
EQ_LIST -> let xs :: Maybe (VEquality b)
xs = forall a b. Eq a => a -> a -> ETree a -> Maybe (VEquality b)
treeFromEqList a
zero a
one ETree a
x
>                                 ys :: Maybe (VEquality b)
ys = forall a b. Eq a => a -> a -> ETree a -> Maybe (VEquality b)
treeFromEqList a
zero a
one ETree a
y
>                             in forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> b -> a
const []) forall {a}. a -> a -> [a]
f forall {b}. Maybe (VEquality b)
xs) forall {b}. Maybe (VEquality b)
ys
>                  ETag
_ -> []
>         ETree a
_ -> []
>       where f :: a -> a -> [a]
f a
x a
y = [a
x,a
y]

> treeFromEqList :: Eq a => a -> a -> ETree a -> Maybe (VEquality b)
> treeFromEqList :: forall a b. Eq a => a -> a -> ETree a -> Maybe (VEquality b)
treeFromEqList a
zero a
one ETree a
t
>     = case ETree a
t of
>         (Node ETag
EQ_LIST (Node ETag
ELEM_EQ ETree a
x ETree a
_) ETree a
y)
>             -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. VEx a -> [VEx a] -> VEquality a
VEquality (forall a b. Eq a => a -> a -> [a] -> ETree a -> [VEx b]
treesFromCons a
zero a
one [a]
vs ETree a
y)
>                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
treeFromEx a
zero a
one [a]
vs ETree a
x
>         ETree a
_ -> forall a. Maybe a
Nothing
>     where vs :: [a]
vs = forall a. Eq a => [a] -> ETree a -> [a]
vars [a
zero, a
one] ETree a
t

> treesFromCons :: Eq a => a -> a -> [a] -> ETree a -> [VEx b]
> treesFromCons :: forall a b. Eq a => a -> a -> [a] -> ETree a -> [VEx b]
treesFromCons a
zero a
one [a]
vs ETree a
t
>     = case forall a. ETree a -> ETag
tag ETree a
t of
>         ETag
ELEM -> forall {b}. ETree a -> [VEx b]
f ETree a
t
>         ETag
EQ_LIST -> case ETree a
t of
>                      (Node ETag
EQ_LIST (Node ETag
ELEM_EQ ETree a
x ETree a
_) ETree a
y)
>                          -> forall {b}. ETree a -> [VEx b]
f ETree a
x forall a. [a] -> [a] -> [a]
++ forall a b. Eq a => a -> a -> [a] -> ETree a -> [VEx b]
treesFromCons a
zero a
one [a]
vs ETree a
y
>                      ETree a
_ -> []
>         ETag
_ -> []
>     where f :: ETree a -> [VEx b]
f = forall a. Maybe a -> [a]
maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
treeFromEx a
zero a
one [a]
vs

The meat of the system lies in collapsing interior nodes
and removing unnecessary levels introduced for the sake of the CNF.
Originally explicit, parentheses are made implicit.
Chains of equality or concatenation are each lifted to a single level.

> treeFromEx :: Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
> treeFromEx :: forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
treeFromEx a
zero a
one [a]
vs (Node ETag
_ ETree a
x ETree a
y)
>     | forall a. ETree a -> ETag
tag ETree a
x forall a. Eq a => a -> a -> Bool
== forall a. ETree a -> ETag
tag ETree a
y Bool -> Bool -> Bool
&& forall a. ETree a -> ETag
tag ETree a
x forall a. Eq a => a -> a -> Bool
== ETag
ELEM
>         = forall {a}. VEx a -> VEx a -> VEx a
merge forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {b}. ETree a -> Maybe (VEx b)
next ETree a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {b}. ETree a -> Maybe (VEx b)
next ETree a
y
>     | forall a. ETree a -> ETag
tag ETree a
y forall a. Eq a => a -> a -> Bool
== ETag
OMEGA = forall a. VEx a -> VEx a
VOmega forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {b}. ETree a -> Maybe (VEx b)
next ETree a
x
>     | forall a. ETree a -> ETag
tag ETree a
x forall a. Eq a => a -> a -> Bool
== ETag
OPEN
>         = case ETree a
y of
>             Node ETag
CLOSE_EL ETree a
a ETree a
_ -> forall {b}. ETree a -> Maybe (VEx b)
next ETree a
a
>             ETree a
_ -> forall a. Maybe a
Nothing
>     where next :: ETree a -> Maybe (VEx b)
next = forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
treeFromEx a
zero a
one [a]
vs
>           mklist :: VEx a -> [VEx a]
mklist (VConcat VEx a
a [VEx a]
b) = VEx a
aforall a. a -> [a] -> [a]
:[VEx a]
b
>           mklist VEx a
a = [VEx a
a]
>           merge :: VEx a -> VEx a -> VEx a
merge (VConcat VEx a
f [VEx a]
fs) VEx a
v = forall a. VEx a -> [VEx a] -> VEx a
VConcat VEx a
f ([VEx a]
fs forall a. [a] -> [a] -> [a]
++ forall {a}. VEx a -> [VEx a]
mklist VEx a
v)
>           merge VEx a
v (VConcat VEx a
f [VEx a]
fs) = forall a. VEx a -> [VEx a] -> VEx a
VConcat VEx a
v (VEx a
fforall a. a -> [a] -> [a]
:[VEx a]
fs)
>           merge VEx a
f VEx a
g = forall a. VEx a -> [VEx a] -> VEx a
VConcat VEx a
f [VEx a
g]
> treeFromEx a
zero a
one [a]
vs (VLeaf a
a ETag
_)
>     | a
a forall a. Eq a => a -> a -> Bool
== a
zero  =  forall a. a -> Maybe a
Just forall a. VEx a
VZero
>     | a
a forall a. Eq a => a -> a -> Bool
== a
one   =  forall a. a -> Maybe a
Just forall a. VEx a
VOne
>     | Bool
otherwise  =  forall a. Integer -> VEx a
VVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t} {t}. (Eq t, Num t) => t -> [t] -> t -> Maybe t
ind a
a [a]
vs Integer
0
>     where ind :: t -> [t] -> t -> Maybe t
ind t
_ [] t
_ = forall a. Maybe a
Nothing
>           ind t
x (t
y:[t]
ys) t
n = if t
x forall a. Eq a => a -> a -> Bool
== t
y then forall a. a -> Maybe a
Just t
n else t -> [t] -> t -> Maybe t
ind t
x [t]
ys (t
n forall a. Num a => a -> a -> a
+ t
1)
> treeFromEx a
_ a
_ [a]
_ ETree a
_ = forall a. Maybe a
Nothing


Appendix: Helpers
=================

Beyond this point are some helpful functions that are used by this module
but do not necessarily flow with its narrative.
This includes various utilities,
a mechanism for finding one / zero in a semigroup,
and a cartesian product for the CKY parser.

> splat :: [Maybe a] -> Maybe [a]
> splat :: forall a. [Maybe a] -> Maybe [a]
splat = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:))) (forall a. a -> Maybe a
Just [])

> splatMap :: (a -> Maybe b) -> [a] -> Maybe [b]
> splatMap :: forall a b. (a -> Maybe b) -> [a] -> Maybe [b]
splatMap a -> Maybe b
f = forall a. [Maybe a] -> Maybe [a]
splat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map a -> Maybe b
f

> safeMin :: Set a -> Maybe a
> safeMin :: forall a. Set a -> Maybe a
safeMin Set a
s = if forall a. Set a -> Bool
Set.null Set a
s then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Set a -> a
Set.findMin Set a
s

Semigroup Parts
===============

> moncat :: (Ord n, Ord e) => SynMon n e
>        -> State ([Maybe n], [Symbol e])
>        -> State ([Maybe n], [Symbol e])
>        -> State ([Maybe n], [Symbol e])
> moncat :: forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m State ([Maybe n], [Symbol e])
p State ([Maybe n], [Symbol e])
q = forall a. Set a -> a
Set.findMin forall a b. (a -> b) -> a -> b
$ forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
m (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall n. State n -> n
nodeLabel State ([Maybe n], [Symbol e])
q) State ([Maybe n], [Symbol e])
p

> findOne :: (Ord n, Ord e) => Bool -> SynMon n e
>         -> Maybe (State ([Maybe n], [Symbol e]))
> findOne :: forall n e.
(Ord n, Ord e) =>
Bool -> SynMon n e -> Maybe (State ([Maybe n], [Symbol e]))
findOne Bool
star SynMon n e
m
>     = if Bool
star Bool -> Bool -> Bool
|| Bool
hasid then forall a. Set a -> Maybe a
safeMin Set (State ([Maybe n], [Symbol e]))
inits else forall a. Set a -> Maybe a
safeMin Set (State ([Maybe n], [Symbol e]))
neuts
>     where trs :: Set (Transition ([Maybe n], [Symbol e]) e)
trs   = forall n e. FSA n e -> Set (Transition n e)
transitions SynMon n e
m
>           sts :: Set (State ([Maybe n], [Symbol e]))
sts   = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination Set (Transition ([Maybe n], [Symbol e]) e)
trs
>           inits :: Set (State ([Maybe n], [Symbol e]))
inits = forall n e. FSA n e -> Set (State n)
initials SynMon n e
m
>           hasid :: Bool
hasid = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set (State ([Maybe n], [Symbol e]))
inits Set (State ([Maybe n], [Symbol e]))
sts
>           isNeut :: State ([Maybe n], [Symbol e]) -> Bool
isNeut State ([Maybe n], [Symbol e])
x
>               = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\State ([Maybe n], [Symbol e])
y -> forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m State ([Maybe n], [Symbol e])
x State ([Maybe n], [Symbol e])
y forall a. Eq a => a -> a -> Bool
== State ([Maybe n], [Symbol e])
y Bool -> Bool -> Bool
&& forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m State ([Maybe n], [Symbol e])
y State ([Maybe n], [Symbol e])
x forall a. Eq a => a -> a -> Bool
== State ([Maybe n], [Symbol e])
y) Set (State ([Maybe n], [Symbol e]))
sts
>           neuts :: Set (State ([Maybe n], [Symbol e]))
neuts = forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep State ([Maybe n], [Symbol e]) -> Bool
isNeut Set (State ([Maybe n], [Symbol e]))
sts

> findZero :: (Ord n, Ord e) => Bool -> SynMon n e
>          -> Maybe (State ([Maybe n], [Symbol e]))
> findZero :: forall n e.
(Ord n, Ord e) =>
Bool -> SynMon n e -> Maybe (State ([Maybe n], [Symbol e]))
findZero Bool
star SynMon n e
m = forall a. Set a -> Maybe a
safeMin Set (State ([Maybe n], [Symbol e]))
zeros
>     where sts :: Set (State ([Maybe n], [Symbol e]))
sts   = if Bool
star
>                   then forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
m
>                   else forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions SynMon n e
m
>           isZero :: State ([Maybe n], [Symbol e]) -> Bool
isZero State ([Maybe n], [Symbol e])
x
>               = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\State ([Maybe n], [Symbol e])
y -> forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m State ([Maybe n], [Symbol e])
x State ([Maybe n], [Symbol e])
y forall a. Eq a => a -> a -> Bool
== State ([Maybe n], [Symbol e])
x Bool -> Bool -> Bool
&& forall n e.
(Ord n, Ord e) =>
SynMon n e
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
moncat SynMon n e
m State ([Maybe n], [Symbol e])
y State ([Maybe n], [Symbol e])
x forall a. Eq a => a -> a -> Bool
== State ([Maybe n], [Symbol e])
x) Set (State ([Maybe n], [Symbol e]))
sts
>           zeros :: Set (State ([Maybe n], [Symbol e]))
zeros = forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep State ([Maybe n], [Symbol e]) -> Bool
isZero Set (State ([Maybe n], [Symbol e]))
sts

Streamable Cartesian Product
----------------------------

> cartesian :: [a] -> [b] -> [(a, b)]
> cartesian :: forall a b. [a] -> [b] -> [(a, b)]
cartesian = forall a b c. ((a, b) -> c) -> a -> b -> c
curry (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [[a]] -> [[a]]
diagonalize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. [a] -> [b] -> [[(a, b)]]
basicProduct)

> diagonalize :: [[a]] -> [[a]]
> diagonalize :: forall a. [[a]] -> [[a]]
diagonalize = forall a. Int -> [a] -> [a]
drop Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [[a]] -> [[a]] -> [[a]]
f []
>     where f :: [[a]] -> [[a]] -> [[a]]
f [[a]]
crows [[a]]
rest
>               = [a]
heads
>                 forall a. a -> [a] -> [a]
: case [[a]]
rest of
>                     []   -> forall a. [[a]] -> [[a]]
transpose [[a]]
crows'
>                     [a]
r:[[a]]
rs -> [[a]] -> [[a]] -> [[a]]
f ([a]
rforall a. a -> [a] -> [a]
:[[a]]
crows') [[a]]
rs
>               where ~([a]
heads, [[a]]
crows') = forall {a}. [[a]] -> ([a], [[a]])
g [[a]]
crows
>                     g :: [[a]] -> ([a], [[a]])
g [] = ([], [])
>                     g ([a]
x:[[a]]
xs) = let ~([a]
hs, [[a]]
ts) = [[a]] -> ([a], [[a]])
g [[a]]
xs
>                                in case [a]
x of
>                                     [] -> ([a]
hs, [[a]]
ts)
>                                     [a
y] -> (a
y forall a. a -> [a] -> [a]
: [a]
hs, [[a]]
ts)
>                                     (a
y:[a]
ys) -> (a
y forall a. a -> [a] -> [a]
: [a]
hs, [a]
ys forall a. a -> [a] -> [a]
: [[a]]
ts)

> basicProduct :: [a] -> [b] -> [[(a, b)]]
> basicProduct :: forall a b. [a] -> [b] -> [[(a, b)]]
basicProduct [a]
as [b]
bs = forall a b. (a -> b) -> [a] -> [b]
map (\a
a -> forall a b. (a -> b) -> [a] -> [b]
map ((,) a
a) [b]
bs) [a]
as

> transpose :: [[a]] -> [[a]]
> transpose :: forall a. [[a]] -> [[a]]
transpose [] = []
> transpose [[a]]
xs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. Int -> [a] -> [a]
take Int
1) [[a]]
xs
>                forall a. a -> [a] -> [a]
: forall a. [[a]] -> [[a]]
transpose (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Int -> [a] -> [a]
drop Int
1) [[a]]
xs)