-- 
-- (C) Susumu Katayama
--
-- Finite trie indexed by Expr, used for fast pattern match
module MagicHaskeller.Analytical.FMExpr where

import qualified Data.IntMap as IntMap

import qualified MagicHaskeller.Types as Types

import MagicHaskeller.Analytical.Syntax


iopsToVisFME :: TBS -> [IOPair a] -> FMExpr [IOPair a]
iopsToVisFME :: TBS -> [IOPair a] -> FMExpr [IOPair a]
iopsToVisFME TBS
tbs = [IOPair a] -> FMExpr [IOPair a]
forall a. [IOPair a] -> FMExpr [IOPair a]
iopsToFME ([IOPair a] -> FMExpr [IOPair a])
-> ([IOPair a] -> [IOPair a]) -> [IOPair a] -> FMExpr [IOPair a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IOPair a -> IOPair a) -> [IOPair a] -> [IOPair a]
forall a b. (a -> b) -> [a] -> [b]
map (TBS -> IOPair a -> IOPair a
forall a. TBS -> IOPair a -> IOPair a
visIOP TBS
tbs)
iopsToFME :: [IOPair a] -> FMExpr [IOPair a]
iopsToFME :: [IOPair a] -> FMExpr [IOPair a]
iopsToFME = [(Expr a, IOPair a)] -> FMExpr [IOPair a]
forall b a. [(Expr b, a)] -> FMExpr [a]
assocsToFME ([(Expr a, IOPair a)] -> FMExpr [IOPair a])
-> ([IOPair a] -> [(Expr a, IOPair a)])
-> [IOPair a]
-> FMExpr [IOPair a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IOPair a -> (Expr a, IOPair a))
-> [IOPair a] -> [(Expr a, IOPair a)]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> (Expr a, IOPair a)
forall a. IOPair a -> (Expr a, IOPair a)
iop2Assoc

visIOP :: TBS -> IOPair a -> IOPair a
visIOP :: TBS -> IOPair a -> IOPair a
visIOP TBS
tbs IOPair a
iop = IOPair a
iop {inputs :: [Expr a]
inputs = TBS -> [Expr a] -> [Expr a]
forall a. TBS -> [a] -> [a]
visibles TBS
tbs ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop}

iop2Assoc :: IOPair a -> (Expr a, IOPair a)
iop2Assoc :: IOPair a -> (Expr a, IOPair a)
iop2Assoc IOPair a
iop = (IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
iop, IOPair a
iop)



-- | @FMExpr a@ is a finite trie representing @Expr () -> a@
data FMExpr a = EmptyFME -- use of emptyFME in place of EmptyFME should not be as efficient, because there are many EmptyFME's.
              | FME { FMExpr a -> IntMap a
existentialFME :: IntMap.IntMap a, FMExpr a -> [a]
universalFME :: [a], FMExpr a -> IntMap (FMExprs a)
conApFME :: IntMap.IntMap (FMExprs a) } deriving Int -> FMExpr a -> ShowS
[FMExpr a] -> ShowS
FMExpr a -> String
(Int -> FMExpr a -> ShowS)
-> (FMExpr a -> String) -> ([FMExpr a] -> ShowS) -> Show (FMExpr a)
forall a. Show a => Int -> FMExpr a -> ShowS
forall a. Show a => [FMExpr a] -> ShowS
forall a. Show a => FMExpr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FMExpr a] -> ShowS
$cshowList :: forall a. Show a => [FMExpr a] -> ShowS
show :: FMExpr a -> String
$cshow :: forall a. Show a => FMExpr a -> String
showsPrec :: Int -> FMExpr a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FMExpr a -> ShowS
Show
data FMExprs a = EmptyFMEs -- and there are many EmptyFMEs's, too.
               | FMEs { FMExprs a -> a
nilFMEs :: a, FMExprs a -> FMExpr (FMExprs a)
consFMEs :: FMExpr (FMExprs a) } deriving Int -> FMExprs a -> ShowS
[FMExprs a] -> ShowS
FMExprs a -> String
(Int -> FMExprs a -> ShowS)
-> (FMExprs a -> String)
-> ([FMExprs a] -> ShowS)
-> Show (FMExprs a)
forall a. Show a => Int -> FMExprs a -> ShowS
forall a. Show a => [FMExprs a] -> ShowS
forall a. Show a => FMExprs a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FMExprs a] -> ShowS
$cshowList :: forall a. Show a => [FMExprs a] -> ShowS
show :: FMExprs a -> String
$cshow :: forall a. Show a => FMExprs a -> String
showsPrec :: Int -> FMExprs a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FMExprs a -> ShowS
Show
instance Functor FMExpr where
  fmap :: (a -> b) -> FMExpr a -> FMExpr b
fmap a -> b
_ FMExpr a
EmptyFME = FMExpr b
forall a. FMExpr a
EmptyFME
  fmap a -> b
f (FME {existentialFME :: forall a. FMExpr a -> IntMap a
existentialFME=IntMap a
e, universalFME :: forall a. FMExpr a -> [a]
universalFME=[a]
u, conApFME :: forall a. FMExpr a -> IntMap (FMExprs a)
conApFME=IntMap (FMExprs a)
c}) = FME :: forall a. IntMap a -> [a] -> IntMap (FMExprs a) -> FMExpr a
FME{existentialFME :: IntMap b
existentialFME = (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f IntMap a
e, universalFME :: [b]
universalFME = (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f [a]
u, conApFME :: IntMap (FMExprs b)
conApFME = (FMExprs a -> FMExprs b)
-> IntMap (FMExprs a) -> IntMap (FMExprs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> FMExprs a -> FMExprs b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) IntMap (FMExprs a)
c}
instance Functor FMExprs where
  fmap :: (a -> b) -> FMExprs a -> FMExprs b
fmap a -> b
f FMExprs a
EmptyFMEs = FMExprs b
forall a. FMExprs a
EmptyFMEs
  fmap a -> b
f (FMEs {nilFMEs :: forall a. FMExprs a -> a
nilFMEs = a
n, consFMEs :: forall a. FMExprs a -> FMExpr (FMExprs a)
consFMEs = FMExpr (FMExprs a)
c}) = FMEs :: forall a. a -> FMExpr (FMExprs a) -> FMExprs a
FMEs {nilFMEs :: b
nilFMEs = a -> b
f a
n, consFMEs :: FMExpr (FMExprs b)
consFMEs = (FMExprs a -> FMExprs b)
-> FMExpr (FMExprs a) -> FMExpr (FMExprs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> FMExprs a -> FMExprs b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) FMExpr (FMExprs a)
c}
assocsToFME :: [(Expr b, a)] -> FMExpr [a]
assocsToFME :: [(Expr b, a)] -> FMExpr [a]
assocsToFME = ((Expr b, a) -> FMExpr [a] -> FMExpr [a])
-> FMExpr [a] -> [(Expr b, a)] -> FMExpr [a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Expr b
k,a
v) -> ([a] -> [a]) -> [a] -> Expr b -> FMExpr [a] -> FMExpr [a]
forall a b. (a -> a) -> a -> Expr b -> FMExpr a -> FMExpr a
updateFME (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:) [] Expr b
k) FMExpr [a]
forall a. FMExpr a
emptyFME
updateFME :: (a->a) -> a -> Expr b -> FMExpr a -> FMExpr a
updateFME :: (a -> a) -> a -> Expr b -> FMExpr a -> FMExpr a
updateFME a -> a
f a
x Expr b
t                FMExpr a
EmptyFME = (a -> a) -> a -> Expr b -> FMExpr a -> FMExpr a
forall a b. (a -> a) -> a -> Expr b -> FMExpr a -> FMExpr a
updateFME a -> a
f a
x Expr b
t FMExpr a
forall a. FMExpr a
emptyFME
updateFME a -> a
f a
x (E b
_ Int
i)            FMExpr a
fme      = FMExpr a
fme { existentialFME :: IntMap a
existentialFME = (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith (\a
_ -> a -> a
f) Int
i (a -> a
f a
x) (IntMap a -> IntMap a) -> IntMap a -> IntMap a
forall a b. (a -> b) -> a -> b
$ FMExpr a -> IntMap a
forall a. FMExpr a -> IntMap a
existentialFME FMExpr a
fme }
updateFME a -> a
f a
x (U b
_ Int
i)            FMExpr a
fme      = FMExpr a
fme { universalFME :: [a]
universalFME   = (a -> a) -> a -> Int -> [a] -> [a]
forall t. (t -> t) -> t -> Int -> [t] -> [t]
insertNth a -> a
f a
x Int
i ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ FMExpr a -> [a]
forall a. FMExpr a -> [a]
universalFME FMExpr a
fme }
updateFME a -> a
f a
x (C b
_ Int
_ (Constr
c Types.:::Type
_) [Expr b]
fs) FMExpr a
fme  = FMExpr a
fme { conApFME :: IntMap (FMExprs a)
conApFME       = (FMExprs a -> FMExprs a -> FMExprs a)
-> Int -> FMExprs a -> IntMap (FMExprs a) -> IntMap (FMExprs a)
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith (\FMExprs a
_ -> (a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
forall a b. (a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
updateFMEs a -> a
f a
x [Expr b]
fs) (Constr -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Constr
c) ((a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
forall a b. (a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
updateFMEs a -> a
f a
x [Expr b]
fs FMExprs a
forall a. FMExprs a
EmptyFMEs) (IntMap (FMExprs a) -> IntMap (FMExprs a))
-> IntMap (FMExprs a) -> IntMap (FMExprs a)
forall a b. (a -> b) -> a -> b
$ FMExpr a -> IntMap (FMExprs a)
forall a. FMExpr a -> IntMap (FMExprs a)
conApFME FMExpr a
fme }
updateFMEs :: (a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
updateFMEs a -> a
f a
x [Expr b]
es         FMExprs a
EmptyFMEs = (a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
updateFMEs a -> a
f a
x [Expr b]
es FMEs :: forall a. a -> FMExpr (FMExprs a) -> FMExprs a
FMEs{nilFMEs :: a
nilFMEs = a
x, consFMEs :: FMExpr (FMExprs a)
consFMEs = FMExpr (FMExprs a)
forall a. FMExpr a
EmptyFME} 
updateFMEs a -> a
f a
x []              FMExprs a
fmes = FMExprs a
fmes { nilFMEs :: a
nilFMEs  = a -> a
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FMExprs a -> a
forall a. FMExprs a -> a
nilFMEs FMExprs a
fmes }
updateFMEs a -> a
f a
x (Expr b
e:[Expr b]
es)          FMExprs a
fmes = FMExprs a
fmes { consFMEs :: FMExpr (FMExprs a)
consFMEs = (FMExprs a -> FMExprs a)
-> FMExprs a -> Expr b -> FMExpr (FMExprs a) -> FMExpr (FMExprs a)
forall a b. (a -> a) -> a -> Expr b -> FMExpr a -> FMExpr a
updateFME ((a -> a) -> a -> [Expr b] -> FMExprs a -> FMExprs a
updateFMEs a -> a
f a
x [Expr b]
es) FMExprs a
forall a. FMExprs a
EmptyFMEs Expr b
e (FMExpr (FMExprs a) -> FMExpr (FMExprs a))
-> FMExpr (FMExprs a) -> FMExpr (FMExprs a)
forall a b. (a -> b) -> a -> b
$ FMExprs a -> FMExpr (FMExprs a)
forall a. FMExprs a -> FMExpr (FMExprs a)
consFMEs FMExprs a
fmes }
emptyFME :: FMExpr a
emptyFME = FME :: forall a. IntMap a -> [a] -> IntMap (FMExprs a) -> FMExpr a
FME{ existentialFME :: IntMap a
existentialFME = IntMap a
forall a. IntMap a
IntMap.empty, universalFME :: [a]
universalFME = [], conApFME :: IntMap (FMExprs a)
conApFME = IntMap (FMExprs a)
forall a. IntMap a
IntMap.empty }


insertNth :: (t -> t) -> t -> Int -> [t] -> [t]
insertNth t -> t
upd t
zero Int
n []     = Int -> t -> [t]
forall a. Int -> a -> [a]
replicate Int
n t
zero [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ [t -> t
upd t
zero]
insertNth t -> t
upd t
zero Int
0 (t
x:[t]
xs) = t -> t
upd t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
xs
insertNth t -> t
upd t
zero Int
n (t
x:[t]
xs) = t
x t -> [t] -> [t]
forall a. a -> [a] -> [a]
: (t -> t) -> t -> Int -> [t] -> [t]
insertNth t -> t
upd t
zero (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [t]
xs



-- returns the set of possible substitutions. Should the name be matchFME?
unifyFME :: Expr b -> FMExpr a -> [(a, Subst b)]
unifyFME :: Expr b -> FMExpr a -> [(a, Subst b)]
unifyFME Expr b
x FMExpr a
fme = Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
unifyFME' Expr b
x FMExpr a
fme Subst b
forall a. [a]
emptySubst
--unifyFME = matchFME
unifyFME' :: Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
unifyFME' :: Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
unifyFME' Expr b
x         FMExpr a
EmptyFME Subst b
s = []
-- unifyFME' (E i)        fme s = error "cannot happen for now"
unifyFME' (E{})        FMExpr a
fme Subst b
s = [ (a
x, Subst b
s) | a
x <- FMExpr a -> [a]
forall a. FMExpr a -> [a]
valsFME FMExpr a
fme ] -- ただし，unifyFME (E _) fmeの場合（全体がexistentialの場合）はそもそもintroBKせずにundefinedな引数にしてしまうべき．どうせその引数は使われないってことだから．
  {-
unifyFME' x@(E i)        fme s o = case lookup i s of Nothing -> [ (x, [(i,e')] `plusSubst` s) | (e,x) <- assocsFME fme, let e' = fresh (o+) e ] -- assocsFME :: FMExpr a -> [(Expr,a)]だけど，FMExprに情報を残しておけば無駄な計算がなくなるか．てゆーか，Typed ConstrのTypeの部分のためにそうする必要がある．
	       		       	   	       	      Just e  -> unifyFME' e fme s o
-}
unifyFME' x :: Expr b
x@(U b
_ Int
i)      FMExpr a
fme Subst b
s = [ (a
v, Subst b
subst Subst b -> Subst b -> Subst b
forall a. Subst a -> Subst a -> Subst a
`plusSubst` Subst b
s)
                                 | (Int
k,a
v) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (FMExpr a -> [a]
forall a. FMExpr a -> [a]
universalFME FMExpr a
fme)
                                 , Subst b
subst <- case Int -> Subst b -> Maybe (Expr b)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
k Subst b
s of Maybe (Expr b)
Nothing        -> [[(Int
k,Expr b
x)]]
                                                               Just (E{iD :: forall a. Expr a -> Int
iD=Int
j}) -> [[(Int
j,Expr b
x)]]
                                                               Just (U{iD :: forall a. Expr a -> Int
iD=Int
j}) | Int
iInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
j -> [[]]
                                                               Maybe (Expr b)
_              -> []
                                 ]
unifyFME' x :: Expr b
x@(C b
_ Int
_sz (Constr
c Types.::: Type
_) [Expr b]
xs) FMExpr a
fme Subst b
s = [(a, Subst b)]
matchExistential [(a, Subst b)] -> [(a, Subst b)] -> [(a, Subst b)]
forall a. [a] -> [a] -> [a]
++ [(a, Subst b)]
matchConstr
    where matchExistential :: [(a, Subst b)]
matchExistential = [ (a
v, Subst b
subst Subst b -> Subst b -> Subst b
forall a. Subst a -> Subst a -> Subst a
`plusSubst` Subst b
s)
                             | (Int
k,a
v) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (FMExpr a -> [a]
forall a. FMExpr a -> [a]
universalFME FMExpr a
fme)
                             , Subst b
subst <- case Int -> Subst b -> Maybe (Expr b)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
k Subst b
s of Maybe (Expr b)
Nothing -> [[(Int
k,Expr b
x)]]
                                                           Just Expr b
e  -> Expr b -> Expr b -> [Subst b]
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> m [(Int, Expr a)]
unify Expr b
e Expr b
x
                             ]
          matchConstr :: [(a, Subst b)]
matchConstr      = case Int -> IntMap (FMExprs a) -> Maybe (FMExprs a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Constr -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Constr
c) (FMExpr a -> IntMap (FMExprs a)
forall a. FMExpr a -> IntMap (FMExprs a)
conApFME FMExpr a
fme) of 
                                                                    Maybe (FMExprs a)
Nothing   -> []
                                                                    Just FMExprs a
fmes -> [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
forall b a. [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
unifyFMEs [Expr b]
xs FMExprs a
fmes Subst b
s
unifyFMEs :: [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
unifyFMEs :: [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
unifyFMEs [Expr b]
_ FMExprs a
EmptyFMEs Subst b
_ = []
unifyFMEs []     FMExprs a
fmes Subst b
s = [ (FMExprs a -> a
forall a. FMExprs a -> a
nilFMEs FMExprs a
fmes, Subst b
s) ]
unifyFMEs (Expr b
x:[Expr b]
xs) FMExprs a
fmes Subst b
s = [ (a, Subst b)
t | (FMExprs a
fmes', Subst b
s') <- Expr b -> FMExpr (FMExprs a) -> Subst b -> [(FMExprs a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
unifyFME' Expr b
x (FMExprs a -> FMExpr (FMExprs a)
forall a. FMExprs a -> FMExpr (FMExprs a)
consFMEs FMExprs a
fmes) Subst b
s, (a, Subst b)
t <- [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
forall b a. [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
unifyFMEs [Expr b]
xs FMExprs a
fmes' Subst b
s' ]
{-
assocsFME :: FMExpr a -> [(Expr,a)]
assocsFME EmptyFME = []
assocsFME fme = [ (E i, v) | (i,v) <- IntMap.toList (existentialFME fme) ] ++ [ (U i, v) | (i,v) <- zip [0..] (universalFME fme) ]
	   ++ [ (C (sum $ map size xs) (c Types.::: error "Not implemented yet!") xs, v)  | (c,fmes) <- IntMap.toList (conApFME fme), (xs, v) <- assocsFMEs fmes ]
assocsFMEs :: FMExprs a -> [([Expr],a)]
assocsFMEs EmptyFMEs = []
assocsFMEs fmes = ([], nilFMEs fmes) : [ (x:xs, v) | (x,fmes') <- assocsFME (consFMEs fmes), (xs, v) <- assocsFMEs fmes ]
-}

-- valsFME = map snd . assocsFME
valsFME :: FMExpr a -> [a]
valsFME :: FMExpr a -> [a]
valsFME FMExpr a
EmptyFME = []
valsFME FMExpr a
fme = IntMap a -> [a]
forall a. IntMap a -> [a]
IntMap.elems (FMExpr a -> IntMap a
forall a. FMExpr a -> IntMap a
existentialFME FMExpr a
fme) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ FMExpr a -> [a]
forall a. FMExpr a -> [a]
universalFME FMExpr a
fme
	   [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [ a
v  | FMExprs a
fmes <- IntMap (FMExprs a) -> [FMExprs a]
forall a. IntMap a -> [a]
IntMap.elems (FMExpr a -> IntMap (FMExprs a)
forall a. FMExpr a -> IntMap (FMExprs a)
conApFME FMExpr a
fme), a
v <- FMExprs a -> [a]
forall a. FMExprs a -> [a]
valsFMEs FMExprs a
fmes ]
valsFMEs :: FMExprs a -> [a]
valsFMEs :: FMExprs a -> [a]
valsFMEs FMExprs a
EmptyFMEs = []
valsFMEs FMExprs a
fmes = FMExprs a -> a
forall a. FMExprs a -> a
nilFMEs FMExprs a
fmes a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [ a
v | FMExprs a
fmes' <- FMExpr (FMExprs a) -> [FMExprs a]
forall a. FMExpr a -> [a]
valsFME (FMExprs a -> FMExpr (FMExprs a)
forall a. FMExprs a -> FMExpr (FMExprs a)
consFMEs FMExprs a
fmes), a
v <- FMExprs a -> [a]
forall a. FMExprs a -> [a]
valsFMEs FMExprs a
fmes' ]

-- 短くした物．効率は確認してない．
matchFME :: Expr b -> FMExpr a -> [(a, Subst b)]
matchFME :: Expr b -> FMExpr a -> [(a, Subst b)]
matchFME Expr b
x FMExpr a
fme = Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchFME' Expr b
x FMExpr a
fme Subst b
forall a. [a]
emptySubst
matchFME' :: Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchFME' :: Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchFME' Expr b
x         FMExpr a
EmptyFME Subst b
s = []
matchFME' (E {}) FMExpr a
fme Subst b
s = [ (a
x, Subst b
s) | a
x <- FMExpr a -> [a]
forall a. FMExpr a -> [a]
valsFME FMExpr a
fme ] -- ただし，matchFME (E _) fmeの場合（全体がexistentialの場合）はそもそもintroBKせずにundefinedな引数にしてしまうべき．どうせその引数は使われないってことだから．
-- Universal variables only match to existentials
matchFME' x :: Expr b
x@(U{}) FMExpr a
fme Subst b
s = Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchExistential Expr b
x FMExpr a
fme Subst b
s
-- Constractor applications can match to both existentials and constructor applications with the same constructor.
matchFME' x :: Expr b
x@(C b
_ Int
_sz (Constr
c Types.::: Type
_) [Expr b]
xs) FMExpr a
fme Subst b
s = Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchExistential Expr b
x FMExpr a
fme Subst b
s [(a, Subst b)] -> [(a, Subst b)] -> [(a, Subst b)]
forall a. [a] -> [a] -> [a]
++ [(a, Subst b)]
matchConstr
    where matchConstr :: [(a, Subst b)]
matchConstr = case Int -> IntMap (FMExprs a) -> Maybe (FMExprs a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Constr -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Constr
c) (FMExpr a -> IntMap (FMExprs a)
forall a. FMExpr a -> IntMap (FMExprs a)
conApFME FMExpr a
fme) of 
                                                               Maybe (FMExprs a)
Nothing   -> []
                                                               Just FMExprs a
fmes -> [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
forall b a. [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
matchFMEs [Expr b]
xs FMExprs a
fmes Subst b
s
matchExistential :: Expr a -> FMExpr a -> [(Int, Expr a)] -> [(a, [(Int, Expr a)])]
matchExistential Expr a
x FMExpr a
fme [(Int, Expr a)]
s = [ (a
v, [(Int, Expr a)]
subst [(Int, Expr a)] -> [(Int, Expr a)] -> [(Int, Expr a)]
forall a. Subst a -> Subst a -> Subst a
`plusSubst` [(Int, Expr a)]
s)
                           | (Int
k,a
v) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (FMExpr a -> [a]
forall a. FMExpr a -> [a]
universalFME FMExpr a
fme)
                           , [(Int, Expr a)]
subst <- case Int -> [(Int, Expr a)] -> Maybe (Expr a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
k [(Int, Expr a)]
s of Maybe (Expr a)
Nothing -> [[(Int
k,Expr a
x)]]
                                                         Just Expr a
e  -> Expr a -> Expr a -> [[(Int, Expr a)]]
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> m [(Int, Expr a)]
unify Expr a
e Expr a
x
                           ]
-- matchFMEs matches corresponding constructor fields
matchFMEs :: [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
matchFMEs :: [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
matchFMEs [Expr b]
_ FMExprs a
EmptyFMEs Subst b
_ = []
matchFMEs []     FMExprs a
fmes Subst b
s = [ (FMExprs a -> a
forall a. FMExprs a -> a
nilFMEs FMExprs a
fmes, Subst b
s) ]
matchFMEs (Expr b
x:[Expr b]
xs) FMExprs a
fmes Subst b
s = [ (a, Subst b)
t | (FMExprs a
fmes', Subst b
s') <- Expr b -> FMExpr (FMExprs a) -> Subst b -> [(FMExprs a, Subst b)]
forall b a. Expr b -> FMExpr a -> Subst b -> [(a, Subst b)]
matchFME' Expr b
x (FMExprs a -> FMExpr (FMExprs a)
forall a. FMExprs a -> FMExpr (FMExprs a)
consFMEs FMExprs a
fmes) Subst b
s, (a, Subst b)
t <- [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
forall b a. [Expr b] -> FMExprs a -> Subst b -> [(a, Subst b)]
matchFMEs [Expr b]
xs FMExprs a
fmes' Subst b
s' ]