{-# LANGUAGE FlexibleContexts #-}
-- 
-- (C) Susumu Katayama
--
module MagicHaskeller.Analytical.UniT where

import Control.Monad -- hiding (guard)
import Control.Monad.State -- hiding (guard)

import MagicHaskeller.Analytical.Syntax

type UniT a = StateT (St a)
data St   a = St {St a -> Subst a
subst::Subst a, St a -> Int
nextVar :: Int} deriving Int -> St a -> ShowS
[St a] -> ShowS
St a -> String
(Int -> St a -> ShowS)
-> (St a -> String) -> ([St a] -> ShowS) -> Show (St a)
forall a. Show a => Int -> St a -> ShowS
forall a. Show a => [St a] -> ShowS
forall a. Show a => St a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [St a] -> ShowS
$cshowList :: forall a. Show a => [St a] -> ShowS
show :: St a -> String
$cshow :: forall a. Show a => St a -> String
showsPrec :: Int -> St a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> St a -> ShowS
Show

emptySt :: St a
emptySt = St :: forall a. Subst a -> Int -> St a
St {subst :: Subst a
subst=[], nextVar :: Int
nextVar=Int
0}
{-
freshVar :: Monad m => UniT m Expr
freshVar = do st <- get
              let nv = nextVar st
              put st{nextVar = succ nv}
              return $ E nv
-}
freshIOP :: IOPair a -> m (IOPair a)
freshIOP (IOP Int
n [Expr a]
ins Expr a
out) = do St a
st <- m (St a)
forall s (m :: * -> *). MonadState s m => m s
get
                              let nv :: Int
nv = St a -> Int
forall a. St a -> Int
nextVar St a
st
                              St a -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put St a
st{nextVar :: Int
nextVar = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n}
                              IOPair a -> m (IOPair a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IOPair a -> m (IOPair a)) -> IOPair a -> m (IOPair a)
forall a b. (a -> b) -> a -> b
$ Int -> [Expr a] -> Expr a -> IOPair a
forall a. Int -> [Expr a] -> Expr a -> IOPair a
IOP Int
0 ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> Expr a -> Expr a
forall a. (Int -> Int) -> Expr a -> Expr a
fresh (Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+)) [Expr a]
ins) ((Int -> Int) -> Expr a -> Expr a
forall a. (Int -> Int) -> Expr a -> Expr a
fresh (Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+) Expr a
out)

applyUT :: Monad m => Expr a -> UniT a m (Expr a)
applyUT :: Expr a -> UniT a m (Expr a)
applyUT Expr a
ex = do Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                Expr a -> UniT a m (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> UniT a m (Expr a)) -> Expr a -> UniT a m (Expr a)
forall a b. (a -> b) -> a -> b
$ Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s Expr a
ex
applyIOPUT :: IOPair a -> m (IOPair a)
applyIOPUT IOPair a
iop = do Subst a
s <- (St a -> Subst a) -> m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                    IOPair a -> m (IOPair a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IOPair a -> m (IOPair a)) -> IOPair a -> m (IOPair a)
forall a b. (a -> b) -> a -> b
$ Subst a -> IOPair a -> IOPair a
forall a. [(Int, Expr a)] -> IOPair a -> IOPair a
applyIOP Subst a
s IOPair a
iop
 
unifyUT :: MonadPlus m => Expr a -> Expr a -> UniT a m ()
unifyUT :: Expr a -> Expr a -> UniT a m ()
unifyUT Expr a
e1 Expr a
e2 = case Expr a -> Expr a -> Maybe [(Int, Expr a)]
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> m [(Int, Expr a)]
unify Expr a
e1 Expr a
e2 of Just [(Int, Expr a)]
s  -> (St a -> St a) -> UniT a m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\St a
st -> St a
st{subst :: [(Int, Expr a)]
subst = [(Int, Expr a)]
s [(Int, Expr a)] -> [(Int, Expr a)] -> [(Int, Expr a)]
forall a. Subst a -> Subst a -> Subst a
`plusSubst` St a -> [(Int, Expr a)]
forall a. St a -> Subst a
subst St a
st})
                                    Maybe [(Int, Expr a)]
Nothing -> UniT a m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
{- Obviously this is slower, but I do not remember why I used this.
unifyUT e1 e2 = do s <- unify e1 e2
                   modify (\st -> st{subst = s `plusSubst` subst st})
-}
appUnifyUT :: Expr a -> Expr a -> StateT (St a) m ()
appUnifyUT Expr a
e1 Expr a
e2 = do Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                      Expr a -> Expr a -> StateT (St a) m ()
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> UniT a m ()
unifyUT (Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s Expr a
e1) (Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s Expr a
e2)