{-# LANGUAGE PatternGuards, ViewPatterns, FlexibleContexts, ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module HSE.Unify(
    Subst, fromSubst,
    validSubst, substitute,
    unifyExp,
    ) where

import Control.Applicative
import Data.List.Extra
import Data.Maybe
import Data.Data
import Data.Semigroup
import Config.Type
import Hint.Type
import Control.Monad
import Data.Tuple.Extra
import Util
import Prelude


---------------------------------------------------------------------
-- SUBSTITUTION DATA TYPE

-- | A list of substitutions. A key may be duplicated, you need to call 'check'
--   to ensure the substitution is valid.
newtype Subst a = Subst [(String, a)]
    deriving (b -> Subst a -> Subst a
NonEmpty (Subst a) -> Subst a
Subst a -> Subst a -> Subst a
(Subst a -> Subst a -> Subst a)
-> (NonEmpty (Subst a) -> Subst a)
-> (forall b. Integral b => b -> Subst a -> Subst a)
-> Semigroup (Subst a)
forall b. Integral b => b -> Subst a -> Subst a
forall a. NonEmpty (Subst a) -> Subst a
forall a. Subst a -> Subst a -> Subst a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> Subst a -> Subst a
stimes :: b -> Subst a -> Subst a
$cstimes :: forall a b. Integral b => b -> Subst a -> Subst a
sconcat :: NonEmpty (Subst a) -> Subst a
$csconcat :: forall a. NonEmpty (Subst a) -> Subst a
<> :: Subst a -> Subst a -> Subst a
$c<> :: forall a. Subst a -> Subst a -> Subst a
Semigroup, Semigroup (Subst a)
Subst a
Semigroup (Subst a) =>
Subst a
-> (Subst a -> Subst a -> Subst a)
-> ([Subst a] -> Subst a)
-> Monoid (Subst a)
[Subst a] -> Subst a
Subst a -> Subst a -> Subst a
forall a. Semigroup (Subst a)
forall a. Subst a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [Subst a] -> Subst a
forall a. Subst a -> Subst a -> Subst a
mconcat :: [Subst a] -> Subst a
$cmconcat :: forall a. [Subst a] -> Subst a
mappend :: Subst a -> Subst a -> Subst a
$cmappend :: forall a. Subst a -> Subst a -> Subst a
mempty :: Subst a
$cmempty :: forall a. Subst a
$cp1Monoid :: forall a. Semigroup (Subst a)
Monoid)

-- | Unpack the substitution
fromSubst :: Subst a -> [(String, a)]
fromSubst :: Subst a -> [(String, a)]
fromSubst (Subst xs :: [(String, a)]
xs) = [(String, a)]
xs

instance Functor Subst where
    fmap :: (a -> b) -> Subst a -> Subst b
fmap f :: a -> b
f (Subst xs :: [(String, a)]
xs) = [(String, b)] -> Subst b
forall a. [(String, a)] -> Subst a
Subst ([(String, b)] -> Subst b) -> [(String, b)] -> Subst b
forall a b. (a -> b) -> a -> b
$ ((String, a) -> (String, b)) -> [(String, a)] -> [(String, b)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> (String, a) -> (String, b)
forall b b' a. (b -> b') -> (a, b) -> (a, b')
second a -> b
f) [(String, a)]
xs

instance Pretty a => Show (Subst a) where
    show :: Subst a -> String
show (Subst xs :: [(String, a)]
xs) = [String] -> String
unlines [String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Pretty a => a -> String
prettyPrint a
b | (a :: String
a,b :: a
b) <- [(String, a)]
xs]


-- check the unification is valid and simplify it
validSubst :: (a -> a -> Bool) -> Subst a -> Maybe (Subst a)
validSubst :: (a -> a -> Bool) -> Subst a -> Maybe (Subst a)
validSubst eq :: a -> a -> Bool
eq = ([(String, a)] -> Subst a)
-> Maybe [(String, a)] -> Maybe (Subst a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(String, a)] -> Subst a
forall a. [(String, a)] -> Subst a
Subst (Maybe [(String, a)] -> Maybe (Subst a))
-> (Subst a -> Maybe [(String, a)]) -> Subst a -> Maybe (Subst a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, [a]) -> Maybe (String, a))
-> [(String, [a])] -> Maybe [(String, a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String, [a]) -> Maybe (String, a)
forall a. (a, [a]) -> Maybe (a, a)
f ([(String, [a])] -> Maybe [(String, a)])
-> (Subst a -> [(String, [a])]) -> Subst a -> Maybe [(String, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, a)] -> [(String, [a])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort ([(String, a)] -> [(String, [a])])
-> (Subst a -> [(String, a)]) -> Subst a -> [(String, [a])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst a -> [(String, a)]
forall a. Subst a -> [(String, a)]
fromSubst
    where f :: (a, [a]) -> Maybe (a, a)
f (x :: a
x,y :: a
y:ys :: [a]
ys) | (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> a -> Bool
eq a
y) [a]
ys = (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (a
x,a
y)
          f _ = Maybe (a, a)
forall a. Maybe a
Nothing


-- | Perform a substitution
substitute :: Subst Exp_ -> Exp_ -> Exp_
substitute :: Subst Exp_ -> Exp_ -> Exp_
substitute (Subst bind :: [(String, Exp_)]
bind) = (Exp_ -> Maybe Exp_) -> Exp_ -> Exp_
transformBracketOld Exp_ -> Maybe Exp_
exp (Exp_ -> Exp_) -> (Exp_ -> Exp_) -> Exp_ -> Exp_
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pat_ -> Pat_) -> Exp_ -> Exp_
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi Pat_ -> Pat_
pat
    where
        exp :: Exp_ -> Maybe Exp_
exp (Var _ (QName S -> String
forall a. Named a => a -> String
fromNamed -> String
x)) = String -> [(String, Exp_)] -> Maybe Exp_
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x [(String, Exp_)]
bind
        exp (InfixApp s :: S
s lhs :: Exp_
lhs (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
x) rhs :: Exp_
rhs) =
            (\op :: QOp S
op -> S -> Exp_ -> QOp S -> Exp_ -> Exp_
forall l. l -> Exp l -> QOp l -> Exp l -> Exp l
InfixApp S
s Exp_
lhs QOp S
op Exp_
rhs) (QOp S -> Exp_) -> Maybe (QOp S) -> Maybe Exp_
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe (QOp S)
forall b. Named b => String -> Maybe b
lookupOp String
x
        exp (LeftSection s :: S
s exp :: Exp_
exp (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
x)) =
            S -> Exp_ -> QOp S -> Exp_
forall l. l -> Exp l -> QOp l -> Exp l
LeftSection S
s Exp_
exp (QOp S -> Exp_) -> Maybe (QOp S) -> Maybe Exp_
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe (QOp S)
forall b. Named b => String -> Maybe b
lookupOp String
x
        exp (RightSection s :: S
s (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
x) exp :: Exp_
exp) =
            (\op :: QOp S
op -> S -> QOp S -> Exp_ -> Exp_
forall l. l -> QOp l -> Exp l -> Exp l
RightSection S
s QOp S
op Exp_
exp) (QOp S -> Exp_) -> Maybe (QOp S) -> Maybe Exp_
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe (QOp S)
forall b. Named b => String -> Maybe b
lookupOp String
x
        exp _ = Maybe Exp_
forall a. Maybe a
Nothing

        -- Substition for operator must be an operator name
        lookupOp :: String -> Maybe b
lookupOp x :: String
x = String -> b
forall a. Named a => String -> a
toNamed (String -> b) -> (Exp_ -> String) -> Exp_ -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp_ -> String
forall a. Named a => a -> String
fromNamed (Exp_ -> b) -> Maybe Exp_ -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [(String, Exp_)] -> Maybe Exp_
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x [(String, Exp_)]
bind

        pat :: Pat_ -> Pat_
pat (PVar _ (Name S -> String
forall a. Named a => a -> String
fromNamed -> String
x)) | Just y :: Exp_
y <- String -> [(String, Exp_)] -> Maybe Exp_
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x [(String, Exp_)]
bind = String -> Pat_
forall a. Named a => String -> a
toNamed (String -> Pat_) -> String -> Pat_
forall a b. (a -> b) -> a -> b
$ Exp_ -> String
forall a. Named a => a -> String
fromNamed Exp_
y
        pat x :: Pat_
x = Pat_
x :: Pat_


---------------------------------------------------------------------
-- UNIFICATION

type NameMatch = QName S -> QName S -> Bool

nmOp :: NameMatch -> QOp S -> QOp S -> Bool
nmOp :: NameMatch -> QOp S -> QOp S -> Bool
nmOp nm :: NameMatch
nm (QVarOp _ x :: QName S
x) (QVarOp _ y :: QName S
y) = NameMatch
nm QName S
x QName S
y
nmOp nm :: NameMatch
nm (QConOp _ x :: QName S
x) (QConOp _ y :: QName S
y) = NameMatch
nm QName S
x QName S
y
nmOp nm :: NameMatch
nm  _ _ = Bool
False


-- | Unification, obeys the property that if @unify a b = s@, then @substitute s a = b@.
unify :: Data a => NameMatch -> Bool -> a -> a -> Maybe (Subst Exp_)
unify :: NameMatch -> Bool -> a -> a -> Maybe (Subst Exp_)
unify nm :: NameMatch
nm root :: Bool
root x :: a
x y :: a
y
    | Just (x :: Exp_
x,y :: Exp_
y) <- (a, a) -> Maybe (Exp_, Exp_)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (a
x,a
y) = NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
root Exp_
x Exp_
y
    | Just (x :: Pat_
x,y :: Pat_
y) <- (a, a) -> Maybe (Pat_, Pat_)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (a
x,a
y) = NameMatch -> Pat_ -> Pat_ -> Maybe (Subst Exp_)
unifyPat NameMatch
nm Pat_
x Pat_
y
    | Just (S
x :: S) <- a -> Maybe S
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x = Subst Exp_ -> Maybe (Subst Exp_)
forall a. a -> Maybe a
Just Subst Exp_
forall a. Monoid a => a
mempty
    | Bool
otherwise = NameMatch -> a -> a -> Maybe (Subst Exp_)
forall a. Data a => NameMatch -> a -> a -> Maybe (Subst Exp_)
unifyDef NameMatch
nm a
x a
y


unifyDef :: Data a => NameMatch -> a -> a -> Maybe (Subst Exp_)
unifyDef :: NameMatch -> a -> a -> Maybe (Subst Exp_)
unifyDef nm :: NameMatch
nm x :: a
x y :: a
y = ([Subst Exp_] -> Subst Exp_)
-> Maybe [Subst Exp_] -> Maybe (Subst Exp_)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Subst Exp_] -> Subst Exp_
forall a. Monoid a => [a] -> a
mconcat (Maybe [Subst Exp_] -> Maybe (Subst Exp_))
-> ([Maybe (Subst Exp_)] -> Maybe [Subst Exp_])
-> [Maybe (Subst Exp_)]
-> Maybe (Subst Exp_)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Subst Exp_)] -> Maybe [Subst Exp_]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Maybe (Subst Exp_)] -> Maybe (Subst Exp_))
-> Maybe [Maybe (Subst Exp_)] -> Maybe (Subst Exp_)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall b. Data b => b -> b -> Maybe (Subst Exp_))
-> a -> a -> Maybe [Maybe (Subst Exp_)]
forall a c.
Data a =>
(forall b. Data b => b -> b -> c) -> a -> a -> Maybe [c]
gzip (NameMatch -> Bool -> b -> b -> Maybe (Subst Exp_)
forall a.
Data a =>
NameMatch -> Bool -> a -> a -> Maybe (Subst Exp_)
unify NameMatch
nm Bool
False) a
x a
y


-- App/InfixApp are analysed specially for performance reasons
-- root = True, this is the outside of the expr
-- do not expand out a dot at the root, since otherwise you get two matches because of readRule (Bug #570)
unifyExp :: NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp :: NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp nm :: NameMatch
nm root :: Bool
root x :: Exp_
x y :: Exp_
y | Bool -> Bool
not Bool
root, Exp_ -> Bool
forall l. Exp l -> Bool
isParen Exp_
x Bool -> Bool -> Bool
|| Exp_ -> Bool
forall l. Exp l -> Bool
isParen Exp_
y =
    (Exp_ -> Exp_) -> Subst Exp_ -> Subst Exp_
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Exp_ -> Exp_ -> Exp_
forall l. Eq l => Exp l -> Exp l -> Exp l
rebracket Exp_
y) (Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
root (Exp_ -> Exp_
fromParen Exp_
x) (Exp_ -> Exp_
fromParen Exp_
y)
    where
        rebracket :: Exp l -> Exp l -> Exp l
rebracket (Paren l :: l
l e' :: Exp l
e') e :: Exp l
e | Exp l
e' Exp l -> Exp l -> Bool
forall a. Eq a => a -> a -> Bool
== Exp l
e = l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l
Paren l
l Exp l
e
        rebracket e :: Exp l
e e' :: Exp l
e' = Exp l
e'

unifyExp nm :: NameMatch
nm root :: Bool
root (Var _ (QName S -> String
forall a. Named a => a -> String
fromNamed -> String
v)) y :: Exp_
y | String -> Bool
isUnifyVar String
v = Subst Exp_ -> Maybe (Subst Exp_)
forall a. a -> Maybe a
Just (Subst Exp_ -> Maybe (Subst Exp_))
-> Subst Exp_ -> Maybe (Subst Exp_)
forall a b. (a -> b) -> a -> b
$ [(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(String
v,Exp_
y)]
unifyExp nm :: NameMatch
nm root :: Bool
root (Var _ x :: QName S
x) (Var _ y :: QName S
y) | NameMatch
nm QName S
x QName S
y = Subst Exp_ -> Maybe (Subst Exp_)
forall a. a -> Maybe a
Just Subst Exp_
forall a. Monoid a => a
mempty

-- Match wildcard operators
unifyExp nm :: NameMatch
nm root :: Bool
root (InfixApp _ lhs1 :: Exp_
lhs1 (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
v) rhs1 :: Exp_
rhs1) (InfixApp _ lhs2 :: Exp_
lhs2 (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
op2) rhs2 :: Exp_
rhs2)
    | String -> Bool
isUnifyVar String
v =
        ([(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(String
v, String -> Exp_
forall a. Named a => String -> a
toNamed String
op2)] Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
<>) (Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Subst Exp_ -> Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
(<>) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
lhs1 Exp_
lhs2) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
rhs1 Exp_
rhs2)
unifyExp nm :: NameMatch
nm root :: Bool
root (LeftSection _ exp1 :: Exp_
exp1 (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
v)) (LeftSection _ exp2 :: Exp_
exp2 (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
op2))
    | String -> Bool
isUnifyVar String
v =
        ([(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(String
v, String -> Exp_
forall a. Named a => String -> a
toNamed String
op2)] Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
<>) (Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
exp1 Exp_
exp2
unifyExp nm :: NameMatch
nm root :: Bool
root (RightSection _ (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
v) exp1 :: Exp_
exp1) (RightSection _ (QOp S -> String
forall a. Named a => a -> String
fromNamed -> String
op2) exp2 :: Exp_
exp2)
    | String -> Bool
isUnifyVar String
v =
        ([(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(String
v, String -> Exp_
forall a. Named a => String -> a
toNamed String
op2)] Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
<>) (Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
exp1 Exp_
exp2

-- Options: match directly, and expand through .
unifyExp nm :: NameMatch
nm root :: Bool
root x :: Exp_
x@(App _ x1 :: Exp_
x1 x2 :: Exp_
x2) (App _ y1 :: Exp_
y1 y2 :: Exp_
y2) =
    (Subst Exp_ -> Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
(<>) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
x1 Exp_
y1) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
x2 Exp_
y2) Maybe (Subst Exp_) -> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    (do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
root
            -- don't expand . if at the root, otherwise you can get duplicate matches
            -- because the matching engine auto-generates hints in dot-form
        InfixApp _ y11 :: Exp_
y11 dot :: QOp S
dot y12 :: Exp_
y12 <- Exp_ -> Maybe Exp_
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp_ -> Maybe Exp_) -> Exp_ -> Maybe Exp_
forall a b. (a -> b) -> a -> b
$ Exp_ -> Exp_
fromParen Exp_
y1
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ QOp S -> Bool
isDot QOp S
dot
        NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
root Exp_
x (S -> Exp_ -> Exp_ -> Exp_
forall l. l -> Exp l -> Exp l -> Exp l
App S
an Exp_
y11 (S -> Exp_ -> Exp_ -> Exp_
forall l. l -> Exp l -> Exp l -> Exp l
App S
an Exp_
y12 Exp_
y2)))

-- Options: match directly, then expand through $, then desugar infix
unifyExp nm :: NameMatch
nm root :: Bool
root x :: Exp_
x (InfixApp _ lhs2 :: Exp_
lhs2 op2 :: QOp S
op2 rhs2 :: Exp_
rhs2)
    | InfixApp _ lhs1 :: Exp_
lhs1 op1 :: QOp S
op1 rhs1 :: Exp_
rhs1 <- Exp_
x = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (NameMatch -> QOp S -> QOp S -> Bool
nmOp NameMatch
nm QOp S
op1 QOp S
op2) Maybe () -> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Subst Exp_ -> Subst Exp_ -> Subst Exp_)
-> Maybe (Subst Exp_) -> Maybe (Subst Exp_) -> Maybe (Subst Exp_)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Subst Exp_ -> Subst Exp_ -> Subst Exp_
forall a. Semigroup a => a -> a -> a
(<>) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
lhs1 Exp_
lhs2) (NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
False Exp_
rhs1 Exp_
rhs2)
    | QOp S -> Bool
isDol QOp S
op2 = NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
root Exp_
x (Exp_ -> Maybe (Subst Exp_)) -> Exp_ -> Maybe (Subst Exp_)
forall a b. (a -> b) -> a -> b
$ S -> Exp_ -> Exp_ -> Exp_
forall l. l -> Exp l -> Exp l -> Exp l
App S
an Exp_
lhs2 Exp_
rhs2
    | Bool
otherwise = NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
unifyExp NameMatch
nm Bool
root Exp_
x (Exp_ -> Maybe (Subst Exp_)) -> Exp_ -> Maybe (Subst Exp_)
forall a b. (a -> b) -> a -> b
$ S -> Exp_ -> Exp_ -> Exp_
forall l. l -> Exp l -> Exp l -> Exp l
App S
an (S -> Exp_ -> Exp_ -> Exp_
forall l. l -> Exp l -> Exp l -> Exp l
App S
an (QOp S -> Exp_
opExp QOp S
op2) Exp_
lhs2) Exp_
rhs2

unifyExp nm :: NameMatch
nm root :: Bool
root x :: Exp_
x y :: Exp_
y | Exp_ -> Bool
forall l. Exp l -> Bool
isOther Exp_
x, Exp_ -> Bool
forall l. Exp l -> Bool
isOther Exp_
y = NameMatch -> Exp_ -> Exp_ -> Maybe (Subst Exp_)
forall a. Data a => NameMatch -> a -> a -> Maybe (Subst Exp_)
unifyDef NameMatch
nm Exp_
x Exp_
y
    where
        -- types that are not already handled in unify
        {-# INLINE isOther #-}
        isOther :: Exp l -> Bool
isOther Var{} = Bool
False
        isOther App{} = Bool
False
        isOther InfixApp{} = Bool
False
        isOther _ = Bool
True

unifyExp nm :: NameMatch
nm root :: Bool
root _ _ = Maybe (Subst Exp_)
forall a. Maybe a
Nothing


unifyPat :: NameMatch -> Pat_ -> Pat_ -> Maybe (Subst Exp_)
unifyPat :: NameMatch -> Pat_ -> Pat_ -> Maybe (Subst Exp_)
unifyPat nm :: NameMatch
nm (PVar _ x :: Name S
x) (PVar _ y :: Name S
y) = Subst Exp_ -> Maybe (Subst Exp_)
forall a. a -> Maybe a
Just (Subst Exp_ -> Maybe (Subst Exp_))
-> Subst Exp_ -> Maybe (Subst Exp_)
forall a b. (a -> b) -> a -> b
$ [(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(Name S -> String
forall a. Named a => a -> String
fromNamed Name S
x, String -> Exp_
forall a. Named a => String -> a
toNamed (String -> Exp_) -> String -> Exp_
forall a b. (a -> b) -> a -> b
$ Name S -> String
forall a. Named a => a -> String
fromNamed Name S
y)]
unifyPat nm :: NameMatch
nm (PVar _ x :: Name S
x) PWildCard{} = Subst Exp_ -> Maybe (Subst Exp_)
forall a. a -> Maybe a
Just (Subst Exp_ -> Maybe (Subst Exp_))
-> Subst Exp_ -> Maybe (Subst Exp_)
forall a b. (a -> b) -> a -> b
$ [(String, Exp_)] -> Subst Exp_
forall a. [(String, a)] -> Subst a
Subst [(Name S -> String
forall a. Named a => a -> String
fromNamed Name S
x, String -> Exp_
forall a. Named a => String -> a
toNamed (String -> Exp_) -> String -> Exp_
forall a b. (a -> b) -> a -> b
$ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name S -> String
forall a. Named a => a -> String
fromNamed Name S
x)]
unifyPat nm :: NameMatch
nm x :: Pat_
x y :: Pat_
y = NameMatch -> Pat_ -> Pat_ -> Maybe (Subst Exp_)
forall a. Data a => NameMatch -> a -> a -> Maybe (Subst Exp_)
unifyDef NameMatch
nm Pat_
x Pat_
y