-- This module infers the type of given CoreExpr.
-- This is an updated version of the old Infer.lhs
{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}
module MagicHaskeller.TICE where
import MagicHaskeller.CoreLang
import MagicHaskeller.Types
import MagicHaskeller.TyConLib
import MagicHaskeller.Execute(unsafeExecute, unDeBruijn, s, sprime, bprime, cprime, fix)
import MagicHaskeller.PriorSubsts
import qualified MagicHaskeller.PolyDynamic as PD
import MagicHaskeller.MyDynamic(unsafeFromDyn)
import MagicHaskeller.ReadTHType(thTypeToType)
import Data.Array.IArray
import Control.Monad(MonadPlus)
import Language.Haskell.TH(pprint)

import Debug.Trace

type TI = PriorSubsts Maybe

ceToDynamic :: TyConLib -> VarLib -> CoreExpr -> PD.Dynamic
ceToDynamic :: TyConLib -> VarLib -> CoreExpr -> Dynamic
ceToDynamic TyConLib
tcl VarLib
vl CoreExpr
ce = case TyConLib -> VarLib -> CoreExpr -> Maybe Type
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
TyConLib -> VarLib -> CoreExpr -> m Type
tiCE TyConLib
tcl VarLib
vl CoreExpr
ce of
                          Maybe Type
Nothing -> [Char] -> Dynamic
forall a. HasCallStack => [Char] -> a
error ([Char]
"ceToDynamic: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Exp -> [Char]
forall a. Ppr a => a -> [Char]
pprint (Bool -> VarLib -> CoreExpr -> Exp
exprToTHExp' Bool
False VarLib
vl CoreExpr
ce) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" type mismatch.")
                          Just Type
ty -> TyConLib -> Type -> Any -> Exp -> Dynamic
forall a. TyConLib -> Type -> a -> Exp -> Dynamic
PD.unsafeToDyn TyConLib
tcl Type
ty (Dynamic -> forall a. a
unsafeFromDyn (Dynamic -> forall a. a) -> Dynamic -> forall a. a
forall a b. (a -> b) -> a -> b
$ VarLib -> CoreExpr -> Dynamic
unsafeExecute VarLib
vl CoreExpr
ce) (Exp -> Dynamic) -> Exp -> Dynamic
forall a b. (a -> b) -> a -> b
$ VarLib -> CoreExpr -> Exp
exprToTHExp VarLib
vl CoreExpr
ce

tiCE :: (Functor m, MonadPlus m) => TyConLib -> VarLib -> CoreExpr -> m Type
tiCE :: TyConLib -> VarLib -> CoreExpr -> m Type
tiCE TyConLib
tcl VarLib
vl CoreExpr
ce = do Type
t <- PriorSubsts m Type -> m Type
forall (m :: * -> *) a. Monad m => PriorSubsts m a -> m a
runPS (TyConLib -> VarLib -> CoreExpr -> PriorSubsts m Type
forall (a :: * -> * -> *) (m :: * -> *) p.
(IArray a Dynamic, MonadPlus m) =>
p -> a Var Dynamic -> CoreExpr -> PriorSubsts m Type
tiEx TyConLib
tcl VarLib
vl (CoreExpr -> CoreExpr
unDeBruijn CoreExpr
ce) PriorSubsts m Type
-> (Type -> PriorSubsts m Type) -> PriorSubsts m Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> PriorSubsts m Type
forall (m :: * -> *). Monad m => Type -> PriorSubsts m Type
applyPS)
                    Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
normalize Type
t
tiEx :: p -> a Var Dynamic -> CoreExpr -> PriorSubsts m Type
tiEx p
tcl a Var Dynamic
vl CoreExpr
ex = CoreExpr -> PriorSubsts m Type
forall (m :: * -> *). MonadPlus m => CoreExpr -> PriorSubsts m Type
tie CoreExpr
ex
    where
      tie :: CoreExpr -> PriorSubsts m Type
tie (CoreExpr
e :$ CoreExpr
f) = do
        Type
te <- CoreExpr -> PriorSubsts m Type
tie CoreExpr
e
        Type
tf <- CoreExpr -> PriorSubsts m Type
tie CoreExpr
f
        TyVar
tv <- PriorSubsts m TyVar
forall (m :: * -> *). Monad m => PriorSubsts m TyVar
newTVar
        let t :: Type
t = TyVar -> Type
TV TyVar
tv
        (if PriorSubsts Maybe () -> Maybe ()
forall (m :: * -> *) a. Monad m => PriorSubsts m a -> m a
runPS (Type -> Type -> PriorSubsts Maybe ()
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
Type -> Type -> PriorSubsts m ()
unify (Type
tf Type -> Type -> Type
:-> Type
t) Type
te) Maybe () -> Maybe () -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ()
forall a. Maybe a
Nothing then [Char]
-> (Type -> Type -> PriorSubsts m ())
-> Type
-> Type
-> PriorSubsts m ()
forall a. [Char] -> a -> a
trace ([Char]
"unifying " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show (Type
tf Type -> Type -> Type
:-> Type
t) [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
te) else (Type -> Type -> PriorSubsts m ())
-> Type -> Type -> PriorSubsts m ()
forall a. a -> a
id)
                     Type -> Type -> PriorSubsts m ()
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
Type -> Type -> PriorSubsts m ()
unify (Type
tf Type -> Type -> Type
:-> Type
t) Type
te
        Type
t' <- Type -> PriorSubsts m Type
forall (m :: * -> *). Monad m => Type -> PriorSubsts m Type
applyPS Type
t -- 勝手にこの行入れちゃったけど，いらないの？
        Type -> PriorSubsts m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
      tie CoreExpr
prim     = Type -> PriorSubsts m Type
forall (m :: * -> *).
(Functor m, Monad m) =>
Type -> PriorSubsts m Type
freshInst (Dynamic -> Type
PD.dynType (Dynamic -> Type) -> Dynamic -> Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Dynamic
exe CoreExpr
prim)
      -- myTypeOf is a version of exe defined in Execute.hs. 
      {-# INLINE exe #-}
      exe :: CoreExpr -> PD.Dynamic
      exe :: CoreExpr -> Dynamic
exe (Primitive Var
n) = a Var Dynamic
vla Var Dynamic -> Var -> Dynamic
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!Var
n
      exe (PrimCon   Var
n) = a Var Dynamic
vla Var Dynamic -> Var -> Dynamic
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!Var
n
      exe (Context (Dict Dynamic
pd)) = Dynamic
pd
      exe CoreExpr
S = $(PD.dynamic [|defaultTCL|] [| s     :: (b->c->a) -> (b->c) -> b -> a |])
      exe CoreExpr
K = $(PD.dynamic [|defaultTCL|] [| const :: a->b->a |])
      exe CoreExpr
I = $(PD.dynamic [|defaultTCL|] [| id    :: a->a    |])
      exe CoreExpr
B = $(PD.dynamic [|defaultTCL|] [| (.)   :: (c->a) ->    (b->c) -> b -> a |])
      exe CoreExpr
C = $(PD.dynamic [|defaultTCL|] [| flip  :: (b->c->a) ->     c  -> b -> a |])
      exe CoreExpr
S' = $(PD.dynamic [|defaultTCL|] [| sprime :: (a->b->c)->(d->a)->(d->b)->d->c |])
      exe CoreExpr
B' = $(PD.dynamic [|defaultTCL|] [| bprime :: (a->b->c)->    a ->(d->b)->d->c |])
      exe CoreExpr
C' = $(PD.dynamic [|defaultTCL|] [| cprime :: (a->b->c)->(d->a)->b->d->c |])
      exe CoreExpr
Y  = $(PD.dynamic [|defaultTCL|] [| fix    :: (a->a)->a |])
      exe CoreExpr
foo = [Char] -> Dynamic
forall a. HasCallStack => [Char] -> a
error ([Char]
"TICE.tiEx: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. Show a => a -> [Char]
show CoreExpr
foo [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : unknown combinator")