{-# LANGUAGE LambdaCase #-}

{-|
Module      : Framework.Grammar.Lexica.SynSem.Convenience
Description : Some convenience functions.
Copyright   : (c) Julian Grove and Aaron Steven White, 2025
License     : MIT
Maintainer  : julian.grove@gmail.com
-}

module Framework.Grammar.Lexica.SynSem.Convenience where

import Framework.Grammar.CCG
import Framework.Grammar.Lexica.SynSem
import Framework.Lambda

--------------------------------------------------------------------------------
-- * Some convenience functions

data PairFun f g a b = PairFun { forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST :: f a, forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> g b
sND :: g b } deriving (PairFun f g a b -> PairFun f g a b -> Bool
(PairFun f g a b -> PairFun f g a b -> Bool)
-> (PairFun f g a b -> PairFun f g a b -> Bool)
-> Eq (PairFun f g a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (f :: * -> *) (g :: * -> *) a b.
(Eq (f a), Eq (g b)) =>
PairFun f g a b -> PairFun f g a b -> Bool
$c== :: forall (f :: * -> *) (g :: * -> *) a b.
(Eq (f a), Eq (g b)) =>
PairFun f g a b -> PairFun f g a b -> Bool
== :: PairFun f g a b -> PairFun f g a b -> Bool
$c/= :: forall (f :: * -> *) (g :: * -> *) a b.
(Eq (f a), Eq (g b)) =>
PairFun f g a b -> PairFun f g a b -> Bool
/= :: PairFun f g a b -> PairFun f g a b -> Bool
Eq, Int -> PairFun f g a b -> ShowS
[PairFun f g a b] -> ShowS
PairFun f g a b -> String
(Int -> PairFun f g a b -> ShowS)
-> (PairFun f g a b -> String)
-> ([PairFun f g a b] -> ShowS)
-> Show (PairFun f g a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
Int -> PairFun f g a b -> ShowS
forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
[PairFun f g a b] -> ShowS
forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
PairFun f g a b -> String
$cshowsPrec :: forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
Int -> PairFun f g a b -> ShowS
showsPrec :: Int -> PairFun f g a b -> ShowS
$cshow :: forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
PairFun f g a b -> String
show :: PairFun f g a b -> String
$cshowList :: forall (f :: * -> *) (g :: * -> *) a b.
(Show (f a), Show (g b)) =>
[PairFun f g a b] -> ShowS
showList :: [PairFun f g a b] -> ShowS
Show)

compDepth :: String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth :: String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" (Cat
c :/: Cat
b1) Cat
b2                 | Cat
b1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
b2
  = Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun ((Int, Cat) -> Maybe (Int, Cat)
forall a. a -> Maybe a
Just (Int
0, Cat
c)) ((Int, Cat) -> Maybe (Int, Cat)
forall a. a -> Maybe a
Just (Int
0, Cat
c))
compDepth String
"r" c1 :: Cat
c1@(Cat
c2 :/: Cat
a1) b1 :: Cat
b1@(Cat
b2 :/: Cat
a2) | Cat
a1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
a2
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" Cat
c1 Cat
b2
        y2 :: Maybe (Int, Cat)
y2  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> g b
sND (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" Cat
c2 Cat
b2
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c) -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c Cat -> Cat -> Cat
:/: Cat
a1))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
        y2' :: Maybe (Int, Cat)
y2' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
y2
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
y2'
compDepth String
"r" c1 :: Cat
c1@(Cat
c2 :\: Cat
a1) b1 :: Cat
b1@(Cat
b2 :\: Cat
a2) | Cat
a1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
a2
  = let y2 :: Maybe (Int, Cat)
y2  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> g b
sND (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" Cat
c2 Cat
b2
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c) -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c Cat -> Cat -> Cat
:\: Cat
a1))
        y2' :: Maybe (Int, Cat)
y2' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
y2
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
forall a. Maybe a
Nothing Maybe (Int, Cat)
y2'
compDepth String
"r" Cat
c (Cat
b :/: Cat
a)
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" Cat
c Cat
b
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c') -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c' Cat -> Cat -> Cat
:/: Cat
a))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
forall a. Maybe a
Nothing
compDepth String
"r" Cat
c (Cat
b :\: Cat
a)
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
"r" Cat
c Cat
b
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c') -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c' Cat -> Cat -> Cat
:\: Cat
a))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
forall a. Maybe a
Nothing
compDepth String
l Cat
b2 (Cat
c :\: Cat
b1)                  | Cat
b1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
b2
  = Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun ((Int, Cat) -> Maybe (Int, Cat)
forall a. a -> Maybe a
Just (Int
0, Cat
c)) ((Int, Cat) -> Maybe (Int, Cat)
forall a. a -> Maybe a
Just (Int
0, Cat
c))
compDepth String
l b1 :: Cat
b1@(Cat
b2 :\: Cat
a2) c1 :: Cat
c1@(Cat
c2 :\: Cat
a1)  | Cat
a1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
a2
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
l Cat
b2 Cat
c1
        y2 :: Maybe (Int, Cat)
y2  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> g b
sND (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
l Cat
b2 Cat
c2
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c) -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c Cat -> Cat -> Cat
:/: Cat
a1))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
        y2' :: Maybe (Int, Cat)
y2' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
y2
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
y2'
compDepth String
l b1 :: Cat
b1@(Cat
b2 :/: Cat
a2) c1 :: Cat
c1@(Cat
c2 :/: Cat
a1)  | Cat
a1 Cat -> Cat -> Bool
forall a. Eq a => a -> a -> Bool
== Cat
a2
  = let y2 :: Maybe (Int, Cat)
y2  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> g b
sND (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
l Cat
b2 Cat
c2
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c) -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c Cat -> Cat -> Cat
:\: Cat
a1))
        y2' :: Maybe (Int, Cat)
y2' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
y2
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
forall a. Maybe a
Nothing Maybe (Int, Cat)
y2'
compDepth String
l (Cat
b :/: Cat
a) Cat
c
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
l Cat
b Cat
c
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c') -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c' Cat -> Cat -> Cat
:/: Cat
a))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
forall a. Maybe a
Nothing
compDepth String
l (Cat
b :\: Cat
a) Cat
c
  = let x1 :: Maybe (Int, Cat)
x1  = PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b. PairFun f g a b -> f a
fST (PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat))
-> PairFun Maybe Maybe (Int, Cat) (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> a -> b
$ String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
l Cat
b Cat
c
        upd :: Maybe (Int, Cat) -> Maybe (Int, Cat)
upd = ((Int, Cat) -> (Int, Cat)) -> Maybe (Int, Cat) -> Maybe (Int, Cat)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
d, Cat
c') -> (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Cat
c' Cat -> Cat -> Cat
:\: Cat
a))
        x1' :: Maybe (Int, Cat)
x1' = Maybe (Int, Cat) -> Maybe (Int, Cat)
upd Maybe (Int, Cat)
x1
    in  Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x1' Maybe (Int, Cat)
forall a. Maybe a
Nothing
compDepth String
_ Cat
_ Cat
_
  = Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
forall a. Maybe a
Nothing Maybe (Int, Cat)
forall a. Maybe a
Nothing

compDepthEnglish :: String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepthEnglish :: String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepthEnglish String
d Cat
c1 Cat
c2 = let PairFun Maybe (Int, Cat)
x Maybe (Int, Cat)
y = String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepth String
d Cat
c1 Cat
c2
                           in  case Maybe (Int, Cat)
x of
                                 Just (Int
n1, Cat
_) | Int
n1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 -> case Maybe (Int, Cat)
y of
                                                            Just (Int
n2, Cat
_) | Int
n2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
forall a. Maybe a
Nothing Maybe (Int, Cat)
forall a. Maybe a
Nothing
                                                            Maybe (Int, Cat)
_                     -> Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
forall a. Maybe a
Nothing Maybe (Int, Cat)
y
                                 Maybe (Int, Cat)
_                     -> case Maybe (Int, Cat)
y of
                                                            Just (Int
n2, Cat
_) | Int
n2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x Maybe (Int, Cat)
forall a. Maybe a
Nothing
                                                            Maybe (Int, Cat)
_                     -> Maybe (Int, Cat)
-> Maybe (Int, Cat) -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
forall (f :: * -> *) (g :: * -> *) a b.
f a -> g b -> PairFun f g a b
PairFun Maybe (Int, Cat)
x Maybe (Int, Cat)
y

genComp :: [Term]
genComp :: [Term]
genComp = String -> Term -> Term
Lam String
"f" (String -> Term -> Term
Lam String
"x" (String -> Term
Var String
"f" Term -> Term -> Term
@@ String -> Term
Var String
"x")) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Term -> Term
App (String -> Term -> Term
Lam String
"g" (String -> Term -> Term
Lam String
"f" (String -> Term -> Term
Lam String
"x" (String -> Term -> Term
Lam String
"y" (String -> Term
Var String
"g" Term -> Term -> Term
@@ String -> Term
Var String
"f" Term -> Term -> Term
@@ (String -> Term
Var String
"x" Term -> Term -> Term
@@ String -> Term
Var String
"y"))))))) [Term]
genComp

genSub :: [Term]
genSub :: [Term]
genSub = String -> Term -> Term
Lam String
"f" (String -> Term -> Term
Lam String
"x" (String -> Term
Var String
"f" Term -> Term -> Term
@@ String -> Term
Var String
"x")) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Term -> Term
App (String -> Term -> Term
Lam String
"g" (String -> Term -> Term
Lam String
"f" (String -> Term -> Term
Lam String
"x" (String -> Term -> Term
Lam String
"y" (String -> Term
Var String
"g" Term -> Term -> Term
@@ (String -> Term
Var String
"f" Term -> Term -> Term
@@ String -> Term
Var String
"y") Term -> Term -> Term
@@ (String -> Term
Var String
"x" Term -> Term -> Term
@@ String -> Term
Var String
"y"))))))) [Term]
genSub

flipp :: Term -> Term
flipp :: Term -> Term
flipp Term
t = String -> Term -> Term
Lam String
fr (String -> Term -> Term
Lam String
e (Term
t Term -> Term -> Term
@@ String -> Term
Var String
e Term -> Term -> Term
@@ String -> Term
Var String
fr))
  where String
fr:String
e:[String]
sh = [Term] -> [String]
fresh [Term
t]

combineR :: SynSem -> SynSem -> [SynSem]
combineR (SynSem Cat
b Typed
x) (SynSem Cat
a Typed
y)
  = case String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepthEnglish String
"r" Cat
b Cat
a of
      PairFun (Just (Int
dComp, Cat
cComp)) (Just (Int
dSub, Cat
cSub))
        -> [ Cat -> Typed -> SynSem
SynSem Cat
cComp (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
genComp [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dComp Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))
           , Cat -> Typed -> SynSem
SynSem Cat
cSub (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
genSub [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dSub Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y)) ]
      PairFun (Just (Int
dComp, Cat
cComp)) Maybe (Int, Cat)
Nothing
        -> [Cat -> Typed -> SynSem
SynSem Cat
cComp (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
genComp [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dComp Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))]
      PairFun Maybe (Int, Cat)
Nothing (Just (Int
dSub, Cat
cSub))
        -> [Cat -> Typed -> SynSem
SynSem Cat
cSub (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
genSub [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dSub Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))]
      PairFun Maybe Maybe (Int, Cat) (Int, Cat)
_ -> []

combineL :: SynSem -> SynSem -> [SynSem]
combineL (SynSem Cat
a Typed
x) (SynSem Cat
b Typed
y)
  = case String -> Cat -> Cat -> PairFun Maybe Maybe (Int, Cat) (Int, Cat)
compDepthEnglish String
"l" Cat
a Cat
b of
      PairFun (Just (Int
dComp, Cat
cComp)) (Just (Int
dSub, Cat
cSub))
        -> [ Cat -> Typed -> SynSem
SynSem Cat
cComp (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
flipp ([Term]
genComp [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dComp) Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))
           , Cat -> Typed -> SynSem
SynSem Cat
cSub (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
flipp ([Term]
genSub [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dSub) Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y)) ]
      PairFun (Just (Int
dComp, Cat
cComp)) Maybe (Int, Cat)
Nothing
        -> [Cat -> Typed -> SynSem
SynSem Cat
cComp (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
flipp ([Term]
genComp [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dComp) Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))]
      PairFun Maybe (Int, Cat)
Nothing (Just (Int
dSub, Cat
cSub))
        -> [Cat -> Typed -> SynSem
SynSem Cat
cSub (Sig -> Term -> Typed
ty Sig
tau0 (Term -> Term
betaEtaNormal (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
flipp ([Term]
genSub [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
dSub) Term -> Term -> Term
<$$> Typed -> Term
termOf Typed
x Term -> Term -> Term
<**> Typed -> Term
termOf Typed
y))]
      PairFun Maybe Maybe (Int, Cat) (Int, Cat)
_ -> []