> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : Data.Representation.FiniteSemigroup.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,
> or an inequational characterization of an ordered pseudovariety.
> One parses the collection of equations,
> quantifies universally over the bound variables,
> and determines whether all specified relationships hold.
> -}

> module Data.Representation.FiniteSemigroup.Variety
>     ( -- * Documentation
>       -- $doc
>       isVariety
>     ) where

> import Data.Char (isSpace)
> import Data.List (transpose)
> import Data.Maybe (isJust,maybeToList)

> import Data.Representation.FiniteSemigroup.Base
> import Data.Representation.FiniteSemigroup.Order

> {- $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 ::= rel-list ';' conj-list | rel-list
> >  rel-list ::= value op rel-list | value op value
> >        op ::= '=' | '<' | '≤' | '>' | '≥'
> >     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@.
> The inequality @x<y@ asserts that,
> for all possible variable instantiations,
> the value @x@ is less than that of @y@ in the specified order.
> For longer chains of relations, adjacent pairs are tested.
> That is, @[a\<b>c]@ is equivalent to @[a\<b;b>c]@.
> 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 VRelChain a = VRelChain (VEx a) [(Ordering, VEx a)]
>                    deriving (VRelChain a -> VRelChain a -> Bool
forall a. Eq a => VRelChain a -> VRelChain a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VRelChain a -> VRelChain a -> Bool
$c/= :: forall a. Eq a => VRelChain a -> VRelChain a -> Bool
== :: VRelChain a -> VRelChain a -> Bool
$c== :: forall a. Eq a => VRelChain a -> VRelChain a -> Bool
Eq, VRelChain a -> VRelChain a -> Bool
VRelChain a -> VRelChain 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 (VRelChain a)
forall a. Ord a => VRelChain a -> VRelChain a -> Bool
forall a. Ord a => VRelChain a -> VRelChain a -> Ordering
forall a. Ord a => VRelChain a -> VRelChain a -> VRelChain a
min :: VRelChain a -> VRelChain a -> VRelChain a
$cmin :: forall a. Ord a => VRelChain a -> VRelChain a -> VRelChain a
max :: VRelChain a -> VRelChain a -> VRelChain a
$cmax :: forall a. Ord a => VRelChain a -> VRelChain a -> VRelChain a
>= :: VRelChain a -> VRelChain a -> Bool
$c>= :: forall a. Ord a => VRelChain a -> VRelChain a -> Bool
> :: VRelChain a -> VRelChain a -> Bool
$c> :: forall a. Ord a => VRelChain a -> VRelChain a -> Bool
<= :: VRelChain a -> VRelChain a -> Bool
$c<= :: forall a. Ord a => VRelChain a -> VRelChain a -> Bool
< :: VRelChain a -> VRelChain a -> Bool
$c< :: forall a. Ord a => VRelChain a -> VRelChain a -> Bool
compare :: VRelChain a -> VRelChain a -> Ordering
$ccompare :: forall a. Ord a => VRelChain a -> VRelChain a -> Ordering
Ord, ReadPrec [VRelChain a]
ReadPrec (VRelChain a)
ReadS [VRelChain a]
forall a. Read a => ReadPrec [VRelChain a]
forall a. Read a => ReadPrec (VRelChain a)
forall a. Read a => Int -> ReadS (VRelChain a)
forall a. Read a => ReadS [VRelChain a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [VRelChain a]
$creadListPrec :: forall a. Read a => ReadPrec [VRelChain a]
readPrec :: ReadPrec (VRelChain a)
$creadPrec :: forall a. Read a => ReadPrec (VRelChain a)
readList :: ReadS [VRelChain a]
$creadList :: forall a. Read a => ReadS [VRelChain a]
readsPrec :: Int -> ReadS (VRelChain a)
$creadsPrec :: forall a. Read a => Int -> ReadS (VRelChain a)
Read, Int -> VRelChain a -> ShowS
forall a. Show a => Int -> VRelChain a -> ShowS
forall a. Show a => [VRelChain a] -> ShowS
forall a. Show a => VRelChain a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VRelChain a] -> ShowS
$cshowList :: forall a. Show a => [VRelChain a] -> ShowS
show :: VRelChain a -> String
$cshow :: forall a. Show a => VRelChain a -> String
showsPrec :: Int -> VRelChain a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> VRelChain a -> ShowS
Show)
> data VEx a = VVar Int
>            | 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]
>                      -> [(a,a)]
>                      -> [VRelChain a] -> Bool
> satisfiedUniversally :: forall a.
Eq a =>
(a -> a -> a)
-> (a -> a)
-> Maybe a
-> Maybe a
-> [a]
-> [(a, a)]
-> [VRelChain a]
-> Bool
satisfiedUniversally a -> a -> a
cat a -> a
star Maybe a
zero Maybe a
one [a]
xs [(a, a)]
order [VRelChain a]
vs'
>     = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False [VRelChain a] -> Bool
f Maybe [VRelChain a]
vs
>     where f :: [VRelChain a] -> Bool
f = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => [(a, a)] -> VRelChain a -> Bool
evaluate [(a, a)]
order)
>               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] -> Int -> VRelChain a -> [VRelChain a]
instantiations a -> a -> a
cat a -> a
star [a]
xs Int
0)
>           vs :: Maybe [VRelChain a]
vs = forall a b. (a -> Maybe b) -> [a] -> Maybe [b]
splatMap (forall a. Maybe a -> Maybe a -> VRelChain a -> Maybe (VRelChain a)
fillzo Maybe a
zero Maybe a
one) [VRelChain 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.
> -- To check for a \(*\)-variety, pass in a monoid.
> -- For a \(+\)-variety, use a semigroup.
> isVariety :: FiniteSemigroupRep s =>
>              String -> OrderedSemigroup s -> Maybe Bool
> isVariety :: forall s.
FiniteSemigroupRep s =>
String -> OrderedSemigroup s -> Maybe Bool
isVariety String
desc OrderedSemigroup s
s
>     = 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 [VRelChain b]
v
>       forall a b. (a -> b) -> a -> b
$ forall a.
Eq a =>
(a -> a -> a)
-> (a -> a)
-> Maybe a
-> Maybe a
-> [a]
-> [(a, a)]
-> [VRelChain a]
-> Bool
satisfiedUniversally (forall a. FiniteSemigroupRep a => a -> Int -> Int -> Int
fsappend OrderedSemigroup s
s) (forall s. FiniteSemigroupRep s => s -> Int -> Int
omega OrderedSemigroup s
s)
>         Maybe Int
zero Maybe Int
one [Int]
qs (forall s. OrderedSemigroup s -> [(Int, Int)]
orel OrderedSemigroup s
s)
>     where zero :: Maybe Int
zero = forall s. FiniteSemigroupRep s => s -> Maybe Int
zeroElement OrderedSemigroup s
s
>           one :: Maybe Int
one  = forall s. FiniteSemigroupRep s => s -> Maybe Int
neutralElement OrderedSemigroup s
s
>           qs :: [Int]
qs   = [Int
0 .. forall a. FiniteSemigroupRep a => a -> Int
fssize OrderedSemigroup s
s forall a. Num a => a -> a -> a
- Int
1]
>           v :: Maybe [VRelChain b]
v    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. Eq a => a -> a -> ETree a -> [VRelChain 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

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 -> VRelChain a -> Maybe (VRelChain a)
> fillzo :: forall a. Maybe a -> Maybe a -> VRelChain a -> Maybe (VRelChain a)
fillzo Maybe a
zero Maybe a
one (VRelChain VEx a
v [(Ordering, VEx a)]
vs) = forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain 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
<*> Maybe [(Ordering, 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
>           vs' :: Maybe [(Ordering, VEx a)]
vs' = forall a. [Maybe a] -> Maybe [a]
splat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Ordering
a,VEx a
b) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) Ordering
a) forall a b. (a -> b) -> a -> b
$ VEx a -> Maybe (VEx a)
fill VEx a
b) [(Ordering, VEx a)]
vs

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
>             -> Int -> VRelChain a -> VRelChain a
> instantiate :: forall a.
(a -> a -> a) -> (a -> a) -> a -> Int -> VRelChain a -> VRelChain a
instantiate a -> a -> a
cat a -> a
star a
x Int
n (VRelChain VEx a
v [(Ordering, VEx a)]
vs)
>     = forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain (VEx a -> VEx a
f VEx a
v) (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VEx a -> VEx a
f) [(Ordering, 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 Int
m) = if Int
m forall a. Eq a => a -> a -> Bool
== Int
n then forall a. a -> VEx a
VElement a
x else forall a. Int -> VEx a
VVar Int
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]
>                -> Int -> VRelChain a -> [VRelChain a]
> instantiations :: forall a.
(a -> a -> a)
-> (a -> a) -> [a] -> Int -> VRelChain a -> [VRelChain a]
instantiations a -> a -> a
cat a -> a
star [a]
xs Int
n (VRelChain VEx a
v' [(Ordering, 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]
:forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Ordering, VEx a)]
mvs) then [VRelChain a
v] else forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [VRelChain 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 :: [(Ordering, VEx a)]
mvs = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VEx a -> VEx a
m) [(Ordering, VEx a)]
vs'
>           v :: VRelChain a
v = forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain VEx a
mv [(Ordering, VEx a)]
mvs
>           f :: a -> [VRelChain a]
f a
x = forall a.
(a -> a -> a)
-> (a -> a) -> [a] -> Int -> VRelChain a -> [VRelChain a]
instantiations a -> a -> a
cat a -> a
star [a]
xs (Int
nforall a. Num a => a -> a -> a
+Int
1)
>                 forall a b. (a -> b) -> a -> b
$ forall a.
(a -> a -> a) -> (a -> a) -> a -> Int -> VRelChain a -> VRelChain a
instantiate a -> a -> a
cat a -> a
star a
x Int
n VRelChain a
v

A chain of relations holds if and only if the adjacent elements
compare appropriately.  Equality is checked via true equality,
while inequalities are checked using the supplied ordering relation.

> evaluate :: Eq a => [(a,a)] -> VRelChain a -> Bool
> evaluate :: forall a. Eq a => [(a, a)] -> VRelChain a -> Bool
evaluate [(a, a)]
order (VRelChain VEx a
x [(Ordering, VEx a)]
xs)
>     = case [(Ordering, VEx a)]
xs of
>         [] -> Bool
True
>         ((Ordering, VEx a)
y:[(Ordering, VEx a)]
ys) -> let rest :: Bool
rest = forall a. Eq a => [(a, a)] -> VRelChain a -> Bool
evaluate [(a, a)]
order (forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain (forall a b. (a, b) -> b
snd (Ordering, VEx a)
y) [(Ordering, VEx a)]
ys)
>                       z :: VEx a
z = forall a b. (a, b) -> b
snd (Ordering, VEx a)
y
>                   in case forall a b. (a, b) -> a
fst (Ordering, VEx a)
y of
>                        Ordering
EQ -> VEx a
x forall a. Eq a => a -> a -> Bool
== VEx a
z Bool -> Bool -> Bool
&& Bool
rest
>                        Ordering
LT -> VEx a
x VEx a -> VEx a -> Bool
`leq` VEx a
z Bool -> Bool -> Bool
&& Bool
rest
>                        Ordering
GT -> VEx a
z VEx a -> VEx a -> Bool
`leq` VEx a
x Bool -> Bool -> Bool
&& Bool
rest
>     where leq :: VEx a -> VEx a -> Bool
leq (VElement a
a) (VElement a
b) = (a
a,a
b) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
order
>           leq VEx a
_ VEx a
_ = Bool
False



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

> data ETag = EXPR | CLOSE_EXP
>           | CONJ_LIST | CONJUNCT
>           | REL_LIST | ELEM_REL
>           | ITER | ELEM | CLOSE_EL
>           | SOE | EOE | OPEN | CLOSE | AND | OMEGA
>           | EQU | LTE | GTE
>             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
LTE]
>               Char
'≤' -> [forall a. ETag -> ETree a
Leaf ETag
LTE]
>               Char
'>' -> [forall a. ETag -> ETree a
Leaf ETag
GTE]
>               Char
'≥' -> [forall a. ETag -> ETree a
Leaf ETag
GTE]
>               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
REL_LIST,   ETag
EOE)        ->  [ETag
CLOSE_EXP]
>                   (ETag
CONJUNCT,   ETag
CONJ_LIST)  ->  [ETag
CONJ_LIST]
>                   (ETag
CONJUNCT,   ETag
REL_LIST)   ->  [ETag
CONJ_LIST]
>                   (ETag
REL_LIST,   ETag
AND)        ->  [ETag
CONJUNCT]
>                   (ETag
ELEM_REL,   ETag
REL_LIST)   ->  [ETag
REL_LIST]
>                   (ETag
ELEM_REL,   ETag
ELEM)       ->  [ETag
REL_LIST]
>                   (ETag
ELEM,       ETag
EQU)        ->  [ETag
ELEM_REL]
>                   (ETag
ELEM,       ETag
LTE)        ->  [ETag
ELEM_REL]
>                   (ETag
ELEM,       ETag
GTE)        ->  [ETag
ELEM_REL]
>                   (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 -> [VRelChain b]
> transform :: forall a b. Eq a => a -> a -> ETree a -> [VRelChain 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 -> [VRelChain b]
forestFromConjList a
zero a
one ETree a
x
>                  ETag
REL_LIST -> forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> a -> ETree a -> Maybe (VRelChain b)
treeFromEqList a
zero a
one ETree a
x
>                  ETag
_ -> []
>         ETree a
_ -> []
 
> forestFromConjList :: Eq a => a -> a -> ETree a -> [VRelChain b]
> forestFromConjList :: forall a b. Eq a => a -> a -> ETree a -> [VRelChain 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 -> [VRelChain 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 (VRelChain b)
treeFromEqList a
zero a
one ETree a
x
>                  ETag
REL_LIST -> let xs :: Maybe (VRelChain b)
xs = forall a b. Eq a => a -> a -> ETree a -> Maybe (VRelChain b)
treeFromEqList a
zero a
one ETree a
x
>                                  ys :: Maybe (VRelChain b)
ys = forall a b. Eq a => a -> a -> ETree a -> Maybe (VRelChain 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 (VRelChain b)
xs) forall {b}. Maybe (VRelChain 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 (VRelChain b)
> treeFromEqList :: forall a b. Eq a => a -> a -> ETree a -> Maybe (VRelChain b)
treeFromEqList a
zero a
one ETree a
t
>     = case forall a. ETree a -> ETag
tag ETree a
t of
>         ETag
REL_LIST -> forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VRelChain b)
treesFromCons a
zero a
one [a]
vs ETree a
t
>         ETag
_ -> 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
>               -> Maybe (VRelChain b)
> treesFromCons :: forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VRelChain 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 a b c. (a -> b -> c) -> b -> a -> c
flip forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain []) 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
t)
>         ETag
REL_LIST -> case ETree a
t of
>                       (Node ETag
REL_LIST (Node ETag
ELEM_REL ETree a
x (Leaf ETag
EQU)) ETree a
y)
>                           -> forall {a}. Ordering -> ETree a -> ETree a -> Maybe (VRelChain a)
f Ordering
EQ ETree a
x ETree a
y
>                       (Node ETag
REL_LIST (Node ETag
ELEM_REL ETree a
x (Leaf ETag
LTE)) ETree a
y)
>                           -> forall {a}. Ordering -> ETree a -> ETree a -> Maybe (VRelChain a)
f Ordering
LT ETree a
x ETree a
y
>                       (Node ETag
REL_LIST (Node ETag
ELEM_REL ETree a
x (Leaf ETag
GTE)) ETree a
y)
>                           -> forall {a}. Ordering -> ETree a -> ETree a -> Maybe (VRelChain a)
f Ordering
GT ETree a
x ETree a
y
>                       ETree a
_ -> forall a. Maybe a
Nothing
>         ETag
_ -> forall a. Maybe a
Nothing
>     where f :: Ordering -> ETree a -> ETree a -> Maybe (VRelChain a)
f Ordering
o ETree a
x ETree a
y = let a :: Maybe (VEx b)
a = forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VEx b)
treeFromEx a
zero a
one [a]
vs ETree a
x
>                         b :: Maybe [(Ordering, VEx a)]
b = forall {a}. Ordering -> VRelChain a -> [(Ordering, VEx a)]
g Ordering
o forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> a -> [a] -> ETree a -> Maybe (VRelChain b)
treesFromCons a
zero a
one [a]
vs ETree a
y
>                     in forall a. VEx a -> [(Ordering, VEx a)] -> VRelChain a
VRelChain forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {b}. Maybe (VEx b)
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a}. Maybe [(Ordering, VEx a)]
b
>           g :: Ordering -> VRelChain a -> [(Ordering, VEx a)]
g Ordering
o ~(VRelChain VEx a
a [(Ordering, VEx a)]
bs) = (Ordering
o,VEx a
a)forall a. a -> [a] -> [a]
:[(Ordering, VEx a)]
bs

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 relations 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. Int -> 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 Int
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


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