-- 
-- (c) Susumu Katayama
--
-- Dynamic with unsafe execution.

{-# LANGUAGE CPP, TemplateHaskell, MagicHash, RankNTypes #-}
module MagicHaskeller.PolyDynamic (
        Dynamic(..),
        fromDyn,        -- :: Type -> Dynamic -> a -> a
        fromDynamic,    -- :: Type -> Dynamic -> Maybe a
        dynApply,
        dynApp,
        dynAppErr,
        unsafeToDyn -- :: Type -> a -> Dynamic
        , aLittleSafeFromDyn -- :: Type -> Dynamic -> a
        , fromPD, dynamic,dynamicH
        -- I (susumu) believe the above is enough, provided unsafeFromDyn does not invoke typeOf for type checking. (Otherwise there would be ambiguity error.)
  ) where


import Data.Typeable
import Data.Maybe

import GHC.Exts(unsafeCoerce#)

import MagicHaskeller.Types
import MagicHaskeller.TyConLib
import Control.Monad

import Language.Haskell.TH hiding (Type)

import Debug.Trace

import MagicHaskeller.ReadTypeRep(trToType)
import MagicHaskeller.ReadTHType(typeToTHType)


import MagicHaskeller.ReadTHType(thTypeToType)
import MagicHaskeller.MHTH
import Data.Typeable(typeOf)


infixl `dynApp`

data Dynamic = Dynamic {Dynamic -> Type
dynType::Type, Dynamic -> forall a. a
unsafeFromDyn::forall a. a, Dynamic -> Exp
dynExp::Exp}
-- CoreExprはPrimitiveがDynamicを使っているので，Expの代わりに使うとhibootしないといけなくなる．

unsafeToDyn :: TyConLib -> Type -> a -> Exp -> Dynamic
unsafeToDyn :: TyConLib -> Type -> a -> Exp -> Dynamic
unsafeToDyn TyConLib
tcl Type
tr a
a Exp
e = Type -> (forall a. a) -> Exp -> Dynamic
Dynamic (Type -> Type
unChin Type
tr) (a -> a
unsafeCoerce# a
a) Exp
e
-- unsafeToDyn tcl tr a e = Dynamic tr (unsafeCoerce# a) (SigE e (typeToTHType tcl tr)) -- こっちはこっちで便利っぽいのだが．

aLittleSafeFromDyn :: Type -> Dynamic -> a
aLittleSafeFromDyn :: Type -> Dynamic -> a
aLittleSafeFromDyn Type
tr (Dynamic Type
t forall a. a
o Exp
_)
    = case Type -> Type -> Maybe Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
tr Type
t of
        Just Subst
_  -> a
forall a. a
o
        Maybe Subst
Nothing -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"aLittleSafeFromDyn: type mismatch between "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Type -> [Char]
forall a. Show a => a -> [Char]
show Type
tr[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
" and "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Type -> [Char]
forall a. Show a => a -> [Char]
show Type
t)
fromDyn :: Typeable a => TyConLib -> Dynamic -> a -> a
fromDyn :: TyConLib -> Dynamic -> a -> a
fromDyn TyConLib
tcl (Dynamic Type
t forall a. a
o Exp
_) a
dflt
    = case Type -> Type -> Maybe Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (TyConLib -> TypeRep -> Type
trToType TyConLib
tcl (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
dflt)) Type
t of
        Just Subst
_  -> a
forall a. a
o
        Maybe Subst
Nothing -> a
dflt
fromDynamic :: MonadPlus m => Type -> Dynamic -> m a
fromDynamic :: Type -> Dynamic -> m a
fromDynamic Type
tr (Dynamic Type
t forall a. a
o Exp
_) = Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
tr Type
t m Subst -> m a -> m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall a. a
o

instance Show Dynamic where
   showsPrec :: Int -> Dynamic -> [Char] -> [Char]
showsPrec Int
_ (Dynamic Type
t forall a. a
_ Exp
e) = ([Char]
"<dynamic "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exp -> [Char]
forall a. Ppr a => a -> [Char]
pprint Exp
e[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"::"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
0 Type
t ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'>'Char -> [Char] -> [Char]
forall k1. k1 -> [k1] -> [k1]
:)

-- (f::(a->b)) `dynApply` (x::a) = (f a)::b
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dynamic Type
t1 forall a. a
f Exp
e1) (Dynamic Type
t2 forall a. a
x Exp
e2) =
  case Type -> Type -> Maybe Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
mguFunAp Type
t1 Type
t2 of
    Just Type
t3 -> -- trace ("dynApply t1 = "++ show t1++", and t2 = "++show t2++", and t3 = "++show t3) $
               Dynamic -> Maybe Dynamic
forall k1. k1 -> Maybe k1
Just (Type -> (forall a. a) -> Exp -> Dynamic
Dynamic Type
t3 ((Any -> Any -> a
unsafeCoerce# Any
forall a. a
f) Any
forall a. a
x) (Exp -> Exp -> Exp
AppE Exp
e1 Exp
e2))
    Maybe Type
Nothing -> Maybe Dynamic
forall k1. Maybe k1
Nothing

dynApp :: Dynamic -> Dynamic -> Dynamic
dynApp :: Dynamic -> Dynamic -> Dynamic
dynApp = [Char] -> Dynamic -> Dynamic -> Dynamic
dynAppErr [Char]
""
dynAppErr :: String ->Dynamic -> Dynamic -> Dynamic
dynAppErr :: [Char] -> Dynamic -> Dynamic -> Dynamic
dynAppErr [Char]
s Dynamic
f Dynamic
x = case Dynamic -> Dynamic -> Maybe Dynamic
dynApply Dynamic
f Dynamic
x of 
                    Just Dynamic
r -> Dynamic
r
                    Maybe Dynamic
Nothing -> [Char] -> Dynamic
forall a. HasCallStack => [Char] -> a
error ([Char]
"Type error in dynamic application.\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                               [Char]
"Can't apply function " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Dynamic -> [Char]
forall a. Show a => a -> [Char]
show Dynamic
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                               [Char]
" to argument " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Dynamic -> [Char]
forall a. Show a => a -> [Char]
show Dynamic
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)

fromPD :: a -> a
fromPD = a -> a
forall a. a -> a
id


-- 以下はMyDynamicからとってきたもので，PolyDynamicにあるのと全く同じ．
{-
$(dynamic [|tcl|] [| (,) :: forall a b. a->b->(a,b) |])
のようにできるようにする．CLEANのdynamicみたいな感じ．
-}
dynamic :: ExpQ -> ExpQ -> ExpQ
dynamic :: ExpQ -> ExpQ -> ExpQ
dynamic ExpQ
eqtcl ExpQ
eq = ExpQ
eq ExpQ -> (Exp -> ExpQ) -> ExpQ
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ExpQ -> Exp -> ExpQ
p' ExpQ
eqtcl


-- Quasi-quotes with higher-rank types are not permitted. When that is the case, take the type info apart from the expression.
-- E.g. $(dynamicH [|tcl|] 'foo [t| forall a b. a->b->(a,b) |]) is equivalent to $(dynamic [|tcl|] [| foo :: forall a b. a->b->(a,b) |])
dynamicH :: ExpQ -> Name -> TypeQ -> ExpQ
dynamicH :: ExpQ -> Name -> TypeQ -> ExpQ
dynamicH ExpQ
eqtcl Name
nm TypeQ
tq = do Type
t <- TypeQ
tq
                          ExpQ -> Exp -> Type -> ExpQ
px ExpQ
eqtcl (Name -> Exp
VarE Name
nm) Type
t
-- p' is like MagicHaskeller.p'
p' :: ExpQ -> Exp -> ExpQ
p' ExpQ
eqtcl (SigE Exp
e Type
ty) = ExpQ -> Exp -> Type -> ExpQ
px ExpQ
eqtcl Exp
e Type
ty
p' ExpQ
eqtcl Exp
e           = [| unsafeToDyn $eqtcl (trToType $eqtcl (typeOf $(return e)))    $(return e)  $(expToExpExp e) |]
-- px eqtcl e ty        = [| unsafeToDyn $eqtcl (thTypeToType $eqtcl $(typeToExpType ty)) $(return se) $(expToExpExp se) |] -- こっちはこっちで便利っぽいのだが．
px :: ExpQ -> Exp -> Type -> ExpQ
px ExpQ
eqtcl Exp
e Type
ty        = [| unsafeToDyn $eqtcl (thTypeToType $eqtcl $(typeToExpType ty)) $(return se) $(expToExpExp e) |]
    where se :: Exp
se = Exp -> Type -> Exp
SigE Exp
e Type
ty