-- 
-- (c) Susumu Katayama
--
\begin{code}
{-# OPTIONS -cpp #-}
module MagicHaskeller.DebMT where
import MagicHaskeller.Types as Types
import MagicHaskeller.TyConLib
import Control.Monad

-- import CoreLang
import Control.Monad.Search.Combinatorial
import MagicHaskeller.PriorSubsts
import Data.Array

import MagicHaskeller.T10((!?))

import Data.List(genericIndex)

import System.IO.Unsafe(unsafeInterleaveIO)

-- type MemoTrie    = MapType (Matrix Possibility)
type Possibility e = (Bag e, Subst, TyVar)
data MapType a
    = MT  {
           MapType a -> [a]
tvMT   :: [a],
           MapType a -> [a]
tcMT   :: [a],
           MapType a -> [a]
genMT  :: [a], -- "forall" stuff
           MapType a -> MapType (MapType a)
taMT   :: MapType (MapType a),
           MapType a -> MapType (MapType a)
funMT  :: MapType (MapType a)
          }

lookupMT :: MapType a -> Type -> a
-- lookupMT :: MonadPlus m => MapType (m a) -> Type -> (m a)
lookupMT :: MapType a -> Type -> a
lookupMT MapType a
mt (TV TyVar
tv)    = MapType a -> [a]
forall a. MapType a -> [a]
tvMT  MapType a
mt [a] -> TyVar -> a
forall i a. Integral i => [a] -> i -> a
`genericIndex` TyVar
tv
lookupMT MapType a
mt (TC TyVar
tc)    | TyVar
tc TyVar -> TyVar -> Bool
forall a. Ord a => a -> a -> Bool
< TyVar
0  = MapType a -> [a]
forall a. MapType a -> [a]
genMT MapType a
mt [a] -> TyVar -> a
forall i a. Integral i => [a] -> i -> a
`genericIndex` (-TyVar
1TyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
-TyVar
tc)
                       | Bool
otherwise = MapType a -> [a]
forall a. MapType a -> [a]
tcMT MapType a
mt [a] -> TyVar -> a
forall i a. Integral i => [a] -> i -> a
`genericIndex` TyVar
tc
lookupMT MapType a
mt (TA Type
t0 Type
t1) = MapType a -> Type -> a
forall a. MapType a -> Type -> a
lookupMT (MapType (MapType a) -> Type -> MapType a
forall a. MapType a -> Type -> a
lookupMT (MapType a -> MapType (MapType a)
forall a. MapType a -> MapType (MapType a)
taMT MapType a
mt) Type
t0) Type
t1
lookupMT MapType a
mt (Type
t0:->Type
t1)  = MapType a -> Type -> a
forall a. MapType a -> Type -> a
lookupMT (MapType (MapType a) -> Type -> MapType a
forall a. MapType a -> Type -> a
lookupMT (MapType a -> MapType (MapType a)
forall a. MapType a -> MapType (MapType a)
funMT MapType a
mt) Type
t0) Type
t1


retrieve :: Decoder -> Subst -> Subst
-- retrieve deco sub = let news = [ (decodeVar deco i, decode deco ty) | (i, ty) <- sub ] in trace ("sub = " ++ show sub ++ " and news = " ++ show news ++ " and deco = " ++ show deco) news
retrieve :: Decoder -> Subst -> Subst
retrieve Decoder
deco Subst
sub = [ (Decoder -> TyVar -> TyVar
decodeVar Decoder
deco TyVar
i, Decoder -> Type -> Type
decode Decoder
deco Type
ty) | (TyVar
i, Type
ty) <- Subst
sub ]

decode :: Decoder -> Type -> Type
decode :: Decoder -> Type -> Type
decode Decoder
deco Type
t = (TyVar -> TyVar) -> Type -> Type
mapTV (Decoder -> TyVar -> TyVar
decodeVar Decoder
deco) Type
t
decodeVar :: Decoder -> TyVar -> TyVar
decodeVar (Dec [TyVar]
tvs TyVar
margin) TyVar
tv = case [TyVar]
tvs [TyVar] -> TyVar -> Maybe TyVar
forall t a. (Eq t, Num t) => [a] -> t -> Maybe a
!? TyVar
tv of Maybe TyVar
Nothing  -> TyVar
tvTyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
+TyVar
margin
                                                  Just TyVar
ntv -> TyVar
ntv

encode   :: Type -> TyVar -> (Type, Decoder)
encode :: Type -> TyVar -> (Type, Decoder)
encode = Type -> TyVar -> (Type, Decoder)
Types.normalizeVarIDs


mkMT :: TyConLib -> (Type->a) -> MapType a
mkMT :: TyConLib -> (Type -> a) -> MapType a
mkMT TyConLib
tcl Type -> a
f = TyConLib -> Kind -> (Type -> a) -> MapType a
forall a. TyConLib -> Kind -> (Type -> a) -> MapType a
mkMT' TyConLib
tcl Kind
0 Type -> a
f
mkMT' :: TyConLib -> Kind -> (Type->a) -> MapType a
mkMT' :: TyConLib -> Kind -> (Type -> a) -> MapType a
mkMT' TyConLib
tcl Kind
k Type -> a
f = [a]
-> [a]
-> [a]
-> MapType (MapType a)
-> MapType (MapType a)
-> MapType a
forall a.
[a]
-> [a]
-> [a]
-> MapType (MapType a)
-> MapType (MapType a)
-> MapType a
MT [a]
tvTree [a]
tcTree [a]
genTree MapType (MapType a)
taTree MapType (MapType a)
funTree where
      tcs :: [(TypeName, TyVar)]
tcs = TyConLib -> Array Kind [(TypeName, TyVar)]
forall a b. (a, b) -> b
snd TyConLib
tcl Array Kind [(TypeName, TyVar)] -> Kind -> [(TypeName, TyVar)]
forall i e. Ix i => Array i e -> i -> e
! Kind
k
      tvTree :: [a]
tvTree  = [ Type -> a
f (TyVar -> Type
TV TyVar
i) | TyVar
i <- [TyVar
0..] ]
      tcTree :: [a]
tcTree  = [ Type -> a
f (TyVar -> Type
TC TyVar
i) | TyVar
i <- [TyVar
0..] ]
      genTree :: [a]
genTree  = [ Type -> a
f (TyVar -> Type
TC TyVar
i) | TyVar
i <- [-TyVar
1,-TyVar
2..] ]
      taTree :: MapType (MapType a)
taTree  = TyConLib -> Kind -> (Type -> MapType a) -> MapType (MapType a)
forall a. TyConLib -> Kind -> (Type -> a) -> MapType a
mkMT' TyConLib
tcl (Kind
kKind -> Kind -> Kind
forall a. Num a => a -> a -> a
+Kind
1) (\Type
t0 -> TyConLib -> (Type -> a) -> MapType a
forall a. TyConLib -> (Type -> a) -> MapType a
mkMT TyConLib
tcl (\Type
t1 -> Type -> a
f (Type -> Type -> Type
TA Type
t0 Type
t1)))
      funTree :: MapType (MapType a)
funTree = if Kind
kKind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
==Kind
0 then TyConLib -> (Type -> MapType a) -> MapType (MapType a)
forall a. TyConLib -> (Type -> a) -> MapType a
mkMT TyConLib
tcl (\Type
t0 -> TyConLib -> (Type -> a) -> MapType a
forall a. TyConLib -> (Type -> a) -> MapType a
mkMT TyConLib
tcl (\Type
t1 -> Type -> a
f (Type
t0 Type -> Type -> Type
:-> Type
t1))) else TypeName -> MapType (MapType a)
forall a. HasCallStack => TypeName -> a
error TypeName
"mkMT': the kind of functions must always be *"
mkMTIO :: TyConLib -> (Type -> IO a) -> IO (MapType a)
mkMTIO :: TyConLib -> (Type -> IO a) -> IO (MapType a)
mkMTIO TyConLib
tcl Type -> IO a
f = TyConLib -> Kind -> (Type -> IO a) -> IO (MapType a)
forall a. TyConLib -> Kind -> (Type -> IO a) -> IO (MapType a)
mkMTIO' TyConLib
tcl Kind
0 Type -> IO a
f
mkMTIO' :: TyConLib -> Kind -> (Type -> IO a) -> IO (MapType a) -- IOのところはMonad m => mでよさそう．実際にはMonadIOでやるかも．
mkMTIO' :: TyConLib -> Kind -> (Type -> IO a) -> IO (MapType a)
mkMTIO' TyConLib
tcl Kind
k Type -> IO a
f = IO (MapType a) -> IO (MapType a)
forall a. IO a -> IO a
unsafeInterleaveIO (IO (MapType a) -> IO (MapType a))
-> IO (MapType a) -> IO (MapType a)
forall a b. (a -> b) -> a -> b
$ ([a]
 -> [a]
 -> [a]
 -> MapType (MapType a)
 -> MapType (MapType a)
 -> MapType a)
-> IO [a]
-> IO [a]
-> IO [a]
-> IO (MapType (MapType a))
-> IO (MapType (MapType a))
-> IO (MapType a)
forall (m :: * -> *) a1 a2 a3 a4 a5 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> a5 -> r)
-> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
liftM5 [a]
-> [a]
-> [a]
-> MapType (MapType a)
-> MapType (MapType a)
-> MapType a
forall a.
[a]
-> [a]
-> [a]
-> MapType (MapType a)
-> MapType (MapType a)
-> MapType a
MT IO [a]
tvTree IO [a]
tcTree IO [a]
genTree IO (MapType (MapType a))
taTree IO (MapType (MapType a))
funTree where
      tcs :: [(TypeName, TyVar)]
tcs = TyConLib -> Array Kind [(TypeName, TyVar)]
forall a b. (a, b) -> b
snd TyConLib
tcl Array Kind [(TypeName, TyVar)] -> Kind -> [(TypeName, TyVar)]
forall i e. Ix i => Array i e -> i -> e
! Kind
k
      lazyf :: Type -> IO a
lazyf = IO a -> IO a
forall a. IO a -> IO a
unsafeInterleaveIO (IO a -> IO a) -> (Type -> IO a) -> Type -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> IO a
f
      tvTree :: IO [a]
tvTree  = [IO a] -> IO [a]
forall a. [IO a] -> IO [a]
interleaveActions ([IO a] -> IO [a]) -> [IO a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ (TyVar -> IO a) -> [TyVar] -> [IO a]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> IO a
f (Type -> IO a) -> (TyVar -> Type) -> TyVar -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
TV) [TyVar
0..]
      tcTree :: IO [a]
tcTree  = [IO a] -> IO [a]
forall a. [IO a] -> IO [a]
interleaveActions ([IO a] -> IO [a]) -> [IO a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ (TyVar -> IO a) -> [TyVar] -> [IO a]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> IO a
f (Type -> IO a) -> (TyVar -> Type) -> TyVar -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
TC) [TyVar
0..]
      genTree :: IO [a]
genTree = [IO a] -> IO [a]
forall a. [IO a] -> IO [a]
interleaveActions ([IO a] -> IO [a]) -> [IO a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ (TyVar -> IO a) -> [TyVar] -> [IO a]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> IO a
f (Type -> IO a) -> (TyVar -> Type) -> TyVar -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
TC) [-TyVar
1,-TyVar
2..]
      taTree :: IO (MapType (MapType a))
taTree  = TyConLib
-> Kind -> (Type -> IO (MapType a)) -> IO (MapType (MapType a))
forall a. TyConLib -> Kind -> (Type -> IO a) -> IO (MapType a)
mkMTIO' TyConLib
tcl (Kind
kKind -> Kind -> Kind
forall a. Num a => a -> a -> a
+Kind
1) (\Type
t0 -> TyConLib -> (Type -> IO a) -> IO (MapType a)
forall a. TyConLib -> (Type -> IO a) -> IO (MapType a)
mkMTIO TyConLib
tcl  (\Type
t1 -> Type -> IO a
lazyf (Type -> Type -> Type
TA Type
t0 Type
t1)))
      funTree :: IO (MapType (MapType a))
funTree = TyConLib -> (Type -> IO (MapType a)) -> IO (MapType (MapType a))
forall a. TyConLib -> (Type -> IO a) -> IO (MapType a)
mkMTIO TyConLib
tcl ((Type -> IO (MapType a)) -> IO (MapType (MapType a)))
-> (Type -> IO (MapType a)) -> IO (MapType (MapType a))
forall a b. (a -> b) -> a -> b
$ if Kind
kKind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
==Kind
0 then (\Type
t0 -> TyConLib -> (Type -> IO a) -> IO (MapType a)
forall a. TyConLib -> (Type -> IO a) -> IO (MapType a)
mkMTIO TyConLib
tcl (\Type
t1 -> Type -> IO a
lazyf (Type
t0 Type -> Type -> Type
:-> Type
t1))) else TypeName -> Type -> IO (MapType a)
forall a. HasCallStack => TypeName -> a
error TypeName
"mkMTIO': the kind of functions must always be *"
--      funTree = if k==0 then mkMTIO tcl (\t0 -> mkMTIO tcl (\t1 -> lazyf (t0 :-> t1))) else error "mkMTIO': the kind of functions must always be *" -- これは間違い．一番外側にunsafeInterleaveIOがないと，kindが0でないinvalidな関数の型も作ろうとしてしまう．

-- I do not add unsafe because I do not understand in what sense unsafeInterleaveIO is unsafe!
interleaveActions :: [IO a] -> IO [a]
interleaveActions :: [IO a] -> IO [a]
interleaveActions = (IO a -> IO [a] -> IO [a]) -> IO [a] -> [IO a] -> IO [a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\IO a
x IO [a]
xs -> IO [a] -> IO [a]
forall a. IO a -> IO a
unsafeInterleaveIO ((a -> [a] -> [a]) -> IO a -> IO [a] -> IO [a]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
Control.Monad.liftM2 (:) IO a
x IO [a]
xs)) ([a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []) ([IO a] -> IO [a]) -> ([IO a] -> [IO a]) -> [IO a] -> IO [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IO a -> IO a) -> [IO a] -> [IO a]
forall a b. (a -> b) -> [a] -> [b]
map IO a -> IO a
forall a. IO a -> IO a
unsafeInterleaveIO
\end{code}