{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns    #-}

module AlgebraCheckers.Unification where

import           Control.Applicative
import           Control.Monad.State
import           Control.Monad.Trans.Writer
import           Data.Data
import           Data.Function
import           Data.Generics.Aliases
import           Data.Generics.Schemes
import qualified Data.Map as M
import           Language.Haskell.TH
import           Language.Haskell.TH.Syntax
import           Prelude hiding (exp)
import {-# SOURCE #-} AlgebraCheckers.Types


data SubExp = SubExp
  { SubExp -> Exp
seExp  :: Exp
  , SubExp -> Int
seSubId :: Int
  } deriving (SubExp -> SubExp -> Bool
(SubExp -> SubExp -> Bool)
-> (SubExp -> SubExp -> Bool) -> Eq SubExp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SubExp -> SubExp -> Bool
$c/= :: SubExp -> SubExp -> Bool
== :: SubExp -> SubExp -> Bool
$c== :: SubExp -> SubExp -> Bool
Eq, Eq SubExp
Eq SubExp
-> (SubExp -> SubExp -> Ordering)
-> (SubExp -> SubExp -> Bool)
-> (SubExp -> SubExp -> Bool)
-> (SubExp -> SubExp -> Bool)
-> (SubExp -> SubExp -> Bool)
-> (SubExp -> SubExp -> SubExp)
-> (SubExp -> SubExp -> SubExp)
-> Ord SubExp
SubExp -> SubExp -> Bool
SubExp -> SubExp -> Ordering
SubExp -> SubExp -> SubExp
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 :: SubExp -> SubExp -> SubExp
$cmin :: SubExp -> SubExp -> SubExp
max :: SubExp -> SubExp -> SubExp
$cmax :: SubExp -> SubExp -> SubExp
>= :: SubExp -> SubExp -> Bool
$c>= :: SubExp -> SubExp -> Bool
> :: SubExp -> SubExp -> Bool
$c> :: SubExp -> SubExp -> Bool
<= :: SubExp -> SubExp -> Bool
$c<= :: SubExp -> SubExp -> Bool
< :: SubExp -> SubExp -> Bool
$c< :: SubExp -> SubExp -> Bool
compare :: SubExp -> SubExp -> Ordering
$ccompare :: SubExp -> SubExp -> Ordering
$cp1Ord :: Eq SubExp
Ord, Int -> SubExp -> ShowS
[SubExp] -> ShowS
SubExp -> String
(Int -> SubExp -> ShowS)
-> (SubExp -> String) -> ([SubExp] -> ShowS) -> Show SubExp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SubExp] -> ShowS
$cshowList :: [SubExp] -> ShowS
show :: SubExp -> String
$cshow :: SubExp -> String
showsPrec :: Int -> SubExp -> ShowS
$cshowsPrec :: Int -> SubExp -> ShowS
Show)


deModuleName :: Data a => a -> a
deModuleName :: a -> a
deModuleName = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((forall a. Data a => a -> a) -> forall a. Data a => a -> a)
-> (forall a. Data a => a -> a) -> forall a. Data a => a -> a
forall a b. (a -> b) -> a -> b
$ (NameFlavour -> NameFlavour) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((NameFlavour -> NameFlavour) -> a -> a)
-> (NameFlavour -> NameFlavour) -> a -> a
forall a b. (a -> b) -> a -> b
$ \case
  NameQ ModName
_ -> NameFlavour
NameS
  NameG NameSpace
_ PkgName
_ ModName
_ -> NameFlavour
NameS
  NameFlavour
n       -> NameFlavour
n


unboundVars :: Exp -> [Name]
unboundVars :: Exp -> [Name]
unboundVars = ([Name] -> [Name] -> [Name]) -> GenericQ [Name] -> GenericQ [Name]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
(++) (GenericQ [Name] -> GenericQ [Name])
-> GenericQ [Name] -> GenericQ [Name]
forall a b. (a -> b) -> a -> b
$
  [Name] -> (Exp -> [Name]) -> a -> [Name]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [] ((Exp -> [Name]) -> a -> [Name]) -> (Exp -> [Name]) -> a -> [Name]
forall a b. (a -> b) -> a -> b
$ \case
    UnboundVarE Name
n -> [Name
n]
    Exp
_ -> []


------------------------------------------------------------------------------
-- | Operates over UnboundVarEs
bindVars :: Data a => M.Map Name Exp -> a -> a
bindVars :: Map Name Exp -> a -> a
bindVars Map Name Exp
m = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((forall a. Data a => a -> a) -> forall a. Data a => a -> a)
-> (forall a. Data a => a -> a) -> forall a. Data a => a -> a
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((Exp -> Exp) -> a -> a) -> (Exp -> Exp) -> a -> a
forall a b. (a -> b) -> a -> b
$ \case
  e :: Exp
e@(UnboundVarE Name
n) ->
    case Name -> Map Name Exp -> Maybe Exp
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name Exp
m of
      Just Exp
e' -> Exp
e'
      Maybe Exp
Nothing -> Exp
e
  Exp
t -> Exp
t


------------------------------------------------------------------------------
-- | Operates over VarEs
rebindVars :: Data a => M.Map Name Exp -> a -> a
rebindVars :: Map Name Exp -> a -> a
rebindVars Map Name Exp
m = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((forall a. Data a => a -> a) -> forall a. Data a => a -> a)
-> (forall a. Data a => a -> a) -> forall a. Data a => a -> a
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((Exp -> Exp) -> a -> a) -> (Exp -> Exp) -> a -> a
forall a b. (a -> b) -> a -> b
$ \case
  e :: Exp
e@(VarE Name
n) ->
    case Name -> Map Name Exp -> Maybe Exp
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name Exp
m of
      Just Exp
e' -> Exp
e'
      Maybe Exp
Nothing -> Exp
e
  Exp
t -> Exp
t


renameVars :: Data a => (String -> String) -> a -> a
renameVars :: ShowS -> a -> a
renameVars ShowS
f = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((forall a. Data a => a -> a) -> forall a. Data a => a -> a)
-> (forall a. Data a => a -> a) -> forall a. Data a => a -> a
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((Exp -> Exp) -> a -> a) -> (Exp -> Exp) -> a -> a
forall a b. (a -> b) -> a -> b
$ \case
  UnboundVarE Name
n -> Name -> Exp
UnboundVarE (Name -> Exp) -> (String -> Name) -> String -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
mkName (String -> Name) -> ShowS -> String -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
f (String -> Exp) -> String -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> String
nameBase Name
n
  Exp
t -> Exp
t


type Subst = M.Map Name Exp

sub :: Data a => Subst -> a -> a
sub :: Map Name Exp -> a -> a
sub = Map Name Exp -> a -> a
forall a. Data a => Map Name Exp -> a -> a
bindVars

unifySub :: Subst -> Exp -> Exp -> Maybe Subst
unifySub :: Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s Exp
a
  = (Map Name Exp -> Map Name Exp)
-> Maybe (Map Name Exp) -> Maybe (Map Name Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Exp -> Exp) -> Map Name Exp -> Map Name Exp
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Exp -> Exp) -> Map Name Exp -> Map Name Exp)
-> (Map Name Exp -> Exp -> Exp) -> Map Name Exp -> Map Name Exp
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name Exp -> Exp -> Exp
forall a. Data a => Map Name Exp -> a -> a
sub) (Map Name Exp -> Map Name Exp)
-> (Map Name Exp -> Map Name Exp) -> Map Name Exp -> Map Name Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Name Exp -> Map Name Exp -> Map Name Exp)
-> Map Name Exp -> Map Name Exp -> Map Name Exp
forall a b c. (a -> b -> c) -> b -> a -> c
flip Map Name Exp -> Map Name Exp -> Map Name Exp
forall a. Monoid a => a -> a -> a
mappend Map Name Exp
s)
  (Maybe (Map Name Exp) -> Maybe (Map Name Exp))
-> (Exp -> Maybe (Map Name Exp)) -> Exp -> Maybe (Map Name Exp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exp -> Exp -> Maybe (Map Name Exp))
-> (Exp -> Exp) -> Exp -> Exp -> Maybe (Map Name Exp)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Exp -> Exp -> Maybe (Map Name Exp)
unify (Map Name Exp -> Exp -> Exp
forall a. Data a => Map Name Exp -> a -> a
sub Map Name Exp
s) Exp
a



type Critical = (Exp, Exp)

criticalPairs :: Law a -> Law a -> [Critical]
criticalPairs :: Law a -> Law a -> [Critical]
criticalPairs Law a
other Law a
me = do
  let (Exp
otherlhs, Exp
otherrhs)
        = ShowS -> Critical -> Critical
forall a. Data a => ShowS -> a -> a
renameVars (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"1") (Law a -> Exp
forall a. Law a -> Exp
lawLhsExp Law a
other, Law a -> Exp
forall a. Law a -> Exp
lawRhsExp Law a
other)
      (Exp
melhs, Exp
merhs)
        = ShowS -> Critical -> Critical
forall a. Data a => ShowS -> a -> a
renameVars (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"2") (Law a -> Exp
forall a. Law a -> Exp
lawLhsExp Law a
me, Law a -> Exp
forall a. Law a -> Exp
lawRhsExp Law a
me)

  SubExp
pat <- Exp -> [SubExp]
subexps Exp
melhs
  Just Map Name Exp
subs <- Maybe (Map Name Exp) -> [Maybe (Map Name Exp)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Map Name Exp) -> [Maybe (Map Name Exp)])
-> Maybe (Map Name Exp) -> [Maybe (Map Name Exp)]
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Maybe (Map Name Exp)
unify (SubExp -> Exp
seExp SubExp
pat) Exp
otherlhs
  let res :: Critical
res = Map Name Exp -> Critical -> Critical
forall a. Data a => Map Name Exp -> a -> a
bindVars Map Name Exp
subs (Exp
merhs, SubExp -> (Exp -> Exp) -> Exp -> Exp
replaceSubexp SubExp
pat (Exp -> Exp -> Exp
forall a b. a -> b -> a
const Exp
otherrhs) Exp
melhs)
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Bool) -> Critical -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Critical
res
  let (Exp
a,Exp
b) = Critical
res
  Critical -> [Critical]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Exp -> Exp
forall a. Ord a => a -> a -> a
min Exp
a Exp
b, Exp -> Exp -> Exp
forall a. Ord a => a -> a -> a
max Exp
a Exp
b)



subexps :: Exp -> [SubExp]
subexps :: Exp -> [SubExp]
subexps Exp
e =
  (State Int [SubExp] -> Int -> [SubExp])
-> Int -> State Int [SubExp] -> [SubExp]
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int [SubExp] -> Int -> [SubExp]
forall s a. State s a -> s -> a
evalState Int
0 (State Int [SubExp] -> [SubExp]) -> State Int [SubExp] -> [SubExp]
forall a b. (a -> b) -> a -> b
$ WriterT [SubExp] (StateT Int Identity) Exp -> State Int [SubExp]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT [SubExp] (StateT Int Identity) Exp -> State Int [SubExp])
-> WriterT [SubExp] (StateT Int Identity) Exp -> State Int [SubExp]
forall a b. (a -> b) -> a -> b
$
    GenericM (WriterT [SubExp] (StateT Int Identity))
-> Exp -> WriterT [SubExp] (StateT Int Identity) Exp
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
everywhereM ((Exp -> WriterT [SubExp] (StateT Int Identity) Exp)
-> a -> WriterT [SubExp] (StateT Int Identity) a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM  ((Exp -> WriterT [SubExp] (StateT Int Identity) Exp)
 -> a -> WriterT [SubExp] (StateT Int Identity) a)
-> (Exp -> WriterT [SubExp] (StateT Int Identity) Exp)
-> a
-> WriterT [SubExp] (StateT Int Identity) a
forall a b. (a -> b) -> a -> b
$ \Exp
e' -> do
      Int
ix <- WriterT [SubExp] (StateT Int Identity) Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int -> Int) -> WriterT [SubExp] (StateT Int Identity) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
      case Exp
e' of
        UnboundVarE Name
_ -> () -> WriterT [SubExp] (StateT Int Identity) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Exp
se -> [SubExp] -> WriterT [SubExp] (StateT Int Identity) ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [(Exp -> Int -> SubExp
SubExp Exp
se Int
ix)]
      Exp -> WriterT [SubExp] (StateT Int Identity) Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e'
                             ) Exp
e


replaceSubexp :: SubExp -> (Exp -> Exp) -> Exp -> Exp
replaceSubexp :: SubExp -> (Exp -> Exp) -> Exp -> Exp
replaceSubexp (SubExp Exp
_ Int
ix) Exp -> Exp
f Exp
old =
  (State Int Exp -> Int -> Exp) -> Int -> State Int Exp -> Exp
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int Exp -> Int -> Exp
forall s a. State s a -> s -> a
evalState Int
0 (State Int Exp -> Exp) -> State Int Exp -> Exp
forall a b. (a -> b) -> a -> b
$
    GenericM (StateT Int Identity) -> Exp -> State Int Exp
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
everywhereM ((Exp -> State Int Exp) -> a -> StateT Int Identity a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM ((Exp -> State Int Exp) -> a -> StateT Int Identity a)
-> (Exp -> State Int Exp) -> a -> StateT Int Identity a
forall a b. (a -> b) -> a -> b
$ \Exp
e' -> do
      Int
ix' <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int -> Int) -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
      Exp -> State Int Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> State Int Exp) -> Exp -> State Int Exp
forall a b. (a -> b) -> a -> b
$ case Int
ix Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ix' of
        Bool
True  -> Exp -> Exp
f Exp
e'
        Bool
False -> Exp
e'
                ) Exp
old


equalUpToAlpha :: Exp -> Exp -> Bool
equalUpToAlpha :: Exp -> Exp -> Bool
equalUpToAlpha Exp
a Exp
b =
  Bool -> (Map Name Exp -> Bool) -> Maybe (Map Name Exp) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    Bool
False
    (\Map Name Exp
subst -> (Exp -> Bool) -> Map Name Exp -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Exp -> Bool
isUnbound Map Name Exp
subst
            Bool -> Bool -> Bool
&& (Exp -> Exp -> Bool) -> Critical -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Map Name Exp -> Critical -> Critical
forall a. Data a => Map Name Exp -> a -> a
bindVars Map Name Exp
subst (Exp
a, Exp
b)))
    (Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
a Exp
b)
  where
    isUnbound :: Exp -> Bool
isUnbound (UnboundVarE Name
_) = Bool
True
    isUnbound Exp
_ = Bool
False


unify :: Exp -> Exp -> Maybe Subst
unify :: Exp -> Exp -> Maybe (Map Name Exp)
unify (ParensE Exp
exp1) Exp
exp2 = Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
unify Exp
exp1 (ParensE Exp
exp2) = Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
unify (UnboundVarE Name
name) Exp
exp = Map Name Exp -> Maybe (Map Name Exp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Name Exp -> Maybe (Map Name Exp))
-> Map Name Exp -> Maybe (Map Name Exp)
forall a b. (a -> b) -> a -> b
$ Name -> Exp -> Map Name Exp
forall k a. k -> a -> Map k a
M.singleton Name
name Exp
exp
unify Exp
exp (UnboundVarE Name
name) = Map Name Exp -> Maybe (Map Name Exp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Name Exp -> Maybe (Map Name Exp))
-> Map Name Exp -> Maybe (Map Name Exp)
forall a b. (a -> b) -> a -> b
$ Name -> Exp -> Map Name Exp
forall k a. k -> a -> Map k a
M.singleton Name
name Exp
exp
unify (AppE Exp
f1 Exp
exp1) (AppE Exp
f2 Exp
exp2) = do
  Map Name Exp
s1 <- Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
f1 Exp
f2
  Map Name Exp
s2 <- Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s1 Exp
exp1 Exp
exp2
  Map Name Exp -> Maybe (Map Name Exp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Name Exp
s2
unify (AppTypeE Exp
exp1 Type
t1) (AppTypeE Exp
exp2 Type
t2) = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2
  Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
unify (InfixE (Just Exp
lhs1) Exp
exp1 (Just Exp
rhs1))
      (InfixE (Just Exp
lhs2) Exp
exp2 (Just Exp
rhs2)) = do
  Map Name Exp
s1 <- Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
  Map Name Exp
s2 <- Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s1 Exp
lhs1 Exp
lhs2
  Map Name Exp
s3 <- Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s2 Exp
rhs1 Exp
rhs2
  Map Name Exp -> Maybe (Map Name Exp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Name Exp
s3
unify (InfixE Maybe Exp
Nothing Exp
exp1 (Just Exp
rhs1))
      (InfixE Maybe Exp
Nothing Exp
exp2 (Just Exp
rhs2)) = do
  Map Name Exp
s1 <- Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
  Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s1 Exp
rhs1 Exp
rhs2
unify (InfixE (Just Exp
lhs1) Exp
exp1 Maybe Exp
Nothing)
      (InfixE (Just Exp
lhs2) Exp
exp2 Maybe Exp
Nothing) = do
  Map Name Exp
s1 <- Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
lhs1 Exp
lhs2
  Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s1 Exp
exp1 Exp
exp2
unify (TupE ([Maybe Exp] -> Maybe [Exp]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA -> Just [Exp]
exps1)) (TupE ([Maybe Exp] -> Maybe [Exp]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA -> Just [Exp]
exps2)) = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [Exp]
exps1 [Exp] -> [Exp] -> Bool
forall a. Eq a => a -> a -> Bool
== [Exp]
exps2
  (Map Name Exp -> Critical -> Maybe (Map Name Exp))
-> Map Name Exp -> [Critical] -> Maybe (Map Name Exp)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Exp -> Exp -> Maybe (Map Name Exp))
-> Critical -> Maybe (Map Name Exp)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Exp -> Exp -> Maybe (Map Name Exp))
 -> Critical -> Maybe (Map Name Exp))
-> (Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp))
-> Map Name Exp
-> Critical
-> Maybe (Map Name Exp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub) Map Name Exp
forall a. Monoid a => a
mempty ([Critical] -> Maybe (Map Name Exp))
-> [Critical] -> Maybe (Map Name Exp)
forall a b. (a -> b) -> a -> b
$ [Exp] -> [Exp] -> [Critical]
forall a b. [a] -> [b] -> [(a, b)]
zip [Exp]
exps1 [Exp]
exps2
unify (CondE Exp
cond1 Exp
then1 Exp
else1) (CondE Exp
cond2 Exp
then2 Exp
else2) = do
  Map Name Exp
s1 <- Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
cond1 Exp
cond2
  Map Name Exp
s2 <- Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s1 Exp
then1 Exp
then2
  Map Name Exp -> Exp -> Exp -> Maybe (Map Name Exp)
unifySub Map Name Exp
s2 Exp
else1 Exp
else2
unify (SigE Exp
exp1 Type
t1) (SigE Exp
exp2 Type
t2) = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2
  Exp -> Exp -> Maybe (Map Name Exp)
unify Exp
exp1 Exp
exp2
unify Exp
a Exp
b = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Exp
a Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
== Exp
b
  Map Name Exp -> Maybe (Map Name Exp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Name Exp
forall a. Monoid a => a
mempty