{-# OPTIONS -fglasgow-exts #-}
module PTypeInference where
import Control.Monad.State
import qualified Data.Map as Map
import qualified Data.Transform.Type as TLT
import Data.Transform.RulesPF (simplifypf)
import Dynamics
import Language.Pointfree.Syntax as PF
import Language.Pointfree.Pretty
import PType
import AnnotatedPF as APF
import Matchings
import Debug.Trace
data Constraint = UnifiesT PType PType | UnifiesF PFctr PFctr | UnifiesIso PType PType -- UnifiesIso breaks only when the first unifies with some Mu F, situation where the second has to unify with F (Mu F)
deriving Show
instance Substitution PTypeSubst Constraint Constraint where
subst s (UnifiesT t1 t2) = UnifiesT (subst s t1) (subst s t2)
subst s (UnifiesF t1 t2) = UnifiesF (subst s t1) (subst s t2)
subst s (UnifiesIso t1 t2) = UnifiesIso (subst s t1) (subst s t2)
-- | Unification of two lists of constraints.
-- first to be processed are types and functors constraints, last are the isomorphisms,
-- which can generate new types and functors constraints. process only stops when both have been processed.
unify :: MonadPlus m => ([Constraint],[Constraint]) -> StateT PTypeSubst m PTypeSubst
unify ([],[]) = get
unify (((UnifiesT (PList a) (PList b)):t),isocs) = unify $ ([UnifiesT a b] ++ t,isocs)
unify (((UnifiesT (PSet a) (PSet b)):t),isocs) = unify $ ([UnifiesT a b] ++ t,isocs)
unify (((UnifiesT (PMap a b) (PMap c d)):t),isocs) = unify $ ([UnifiesT a c, UnifiesT b d] ++ t,isocs)
unify (((UnifiesT (PEither a b) (PEither c d)):t),isocs) = unify $ ([UnifiesT a c, UnifiesT b d] ++ t,isocs)
unify (((UnifiesT (PProd a b) (PProd c d)):t),isocs) = unify $ ([UnifiesT a c, UnifiesT b d] ++ t,isocs)
unify (((UnifiesT (PFunc a b) (PFunc c d)):t),isocs) = unify $ ([UnifiesT a c, UnifiesT b d] ++ t,isocs)
unify (((UnifiesT (PTag n1 a) (PTag n2 b)):t),isocs) | n1 == n2 = unify $ ([UnifiesT a b] ++ t,isocs)
unify (((UnifiesT (PMu f) (PMu g)):t),isocs) = unify $ ([UnifiesF f g] ++ t,isocs)
unify (((UnifiesT (PPF a) (PPF b)):t),isocs) = unify $ ([UnifiesT a b] ++ t,isocs)
unify (((UnifiesF PId PId):t),isocs) = unify $ (t,isocs)
unify (((UnifiesF (PK a) (PK b)):t),isocs) = unify $ ([UnifiesT a b] ++ t,isocs)
unify (((UnifiesF (f1 ::+:: g1) (f2 ::+:: g2)):t),isocs) = unify $ ([UnifiesF f1 f2, UnifiesF f1 f2] ++ t,isocs)
unify (((UnifiesF (f1 ::*:: g1) (f2 ::*:: g2)):t),isocs) = unify $ ([UnifiesF f1 f2, UnifiesF f1 f2] ++ t,isocs)
unify (((UnifiesT (PVar v1) (PVar v2)):t),isocs) | v1 == v2 = unify $ (t,isocs)
unify (((UnifiesT (PVar v1) d2):t),isocs) = replace v1 d2 (t,isocs) >>= unify
unify (((UnifiesT d1 (PVar v2)):t),isocs) = replace v2 d1 (t,isocs) >>= unify
unify (((UnifiesT t1 t2):t),isocs) | t1 == t2 = unify $ (t,isocs)
unify ([],((UnifiesIso (PMu f) t2):t)) = unify $ ([UnifiesT t2 (mapft f (PMu f))], t)
unify ([],((UnifiesIso (PVar v1) (PVar v2)):t)) | v1 == v2 = unify $ ([],t)
unify ([],((UnifiesIso (PVar v1) d2):t)) = replace v1 d2 ([],t) >>= unify
unify ([],((UnifiesIso d1 (PVar v2)):t)) = replace v2 d1 ([],t) >>= unify
unify ([],h:t) = error $ "Cannot unify "++show h
unify (h:t,isocs) = error $ "Cannot unify "++show h
replace :: MonadPlus m => String -> PType -> ([Constraint],[Constraint]) -> StateT PTypeSubst m ([Constraint],[Constraint])
replace v dt (cs,isocs) =
do let s = Map.singleton v dt
modify (subst s)
modify (Map.insert v dt)
return $ (map (subst s) cs, map (subst s) isocs)
-- | Gathers the constraints for type inference of a term according to a type, generating also
-- an annotated PF term
constraints :: MonadPlus m => PF.Term -> PType -> StateT ([String], Map.Map String PType) m (([Constraint],[Constraint]), APF.Term PType)
constraints ID (PFunc a b) = return (([UnifiesT a b],[]), TID a)
constraints (t1 :.: t2) (PFunc a b) =
do nv <- fresh
((r2,r2iso),dt2) <- constraints t2 (PFunc a nv)
((r1,r1iso),dt1) <- constraints t1 (PFunc nv b)
return $ ((r1 ++ r2, r1iso ++ r2iso), TComp dt1 dt2 nv)
constraints FST (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
return (([UnifiesT a (nv1 `PProd` nv2), UnifiesT nv1 b],[]), TFST (nv1 `PProd` nv2))
constraints SND (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
return (([UnifiesT a (nv1 `PProd` nv2), UnifiesT nv2 b],[]), TSND (nv1 `PProd` nv2))
constraints (t1 PF.:/\: t2) (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
((r1,r1iso),tt1) <- constraints t1 (PFunc a nv1)
((r2,r2iso),tt2) <- constraints t2 (PFunc a nv2)
return ((([UnifiesT b (nv1 `PProd` nv2)] ++ (r1 ++ r2)), r1iso ++ r2iso), tt1 APF.:/\: tt2)
constraints INL (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
return (([UnifiesT b (nv1 `PEither` nv2), UnifiesT nv1 a],[]), TINL (nv1 `PEither` nv2))
constraints INR (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
return (([UnifiesT b (nv1 `PEither` nv2), UnifiesT nv2 a],[]), TINR (nv1 `PEither` nv2))
constraints (t1 PF.:\/: t2) (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
((r1,r1iso),tt1) <- constraints t1 (nv1 `PFunc` b)
((r2,r2iso),tt2) <- constraints t2 (nv2 `PFunc` b)
return ((([UnifiesT a (nv1 `PEither` nv2)] ++ (r1 ++ r2)), r1iso ++ r2iso), tt1 APF.:\/: tt2)
constraints AP (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
nv3 <- fresh
nv4 <- fresh
return (([UnifiesT a (nv1 `PProd` nv2), UnifiesT nv1 (nv3 `PFunc` nv4)
,UnifiesT nv3 nv2, UnifiesT nv4 b],[]), TAP (PFunc nv3 nv4))
constraints (Curry t1) (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
((r1,r1iso),tt1) <- constraints t1 ((a `PProd` nv1) `PFunc` nv2)
return ((([UnifiesT b (nv1 `PFunc` nv2)] ++ r1), r1iso), TCurry tt1)
constraints BANG (PFunc a b) = return (([UnifiesT b POne],[]), TBANG a)
constraints (Point str) (PFunc a b) = return (([UnifiesT a POne],[]), TPoint str b)
constraints IN (PFunc a b) = return (([],[UnifiesIso b a]), TIN b)
-- do PVar nv1 <- fresh
-- return ([UnifiesT a (PVar ('f':nv1)),UnifiesT b (PVar ('m':nv1))], TIN b)
constraints OUT (PFunc a b) = return (([],[UnifiesIso a b]), TOUT a)
-- do PVar nv1 <- fresh
-- return ([UnifiesT a (PVar ('m':nv1)),UnifiesT b (PVar ('f':nv1))], TOUT a)
--constraints (Hylo (Mu f) t1 t2) (a `PFunc` b) =
-- do (r1,tt1) <- constraints t1 ((mapft f b) `PFunc` b)
-- (r2,tt2) <- constraints t2 (a `PFunc` (mapft f a))
-- return ((r1 ++ r2), THylo (Mu f) tt1 tt2)
constraints (Macro "(-|-)" [t1,t2]) (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
nv3 <- fresh
nv4 <- fresh
((r1,r1iso),tt1) <- constraints t1 (nv1 `PFunc` nv3)
((r2,r2iso),tt2) <- constraints t2 (nv2 `PFunc` nv4)
return (([UnifiesT a (nv1 `PEither` nv2), UnifiesT b (nv3 `PEither` nv4)]
++ (r1 ++ r2), r1iso ++ r2iso), tt1 :-|-: tt2)
constraints (Macro "(><)" [t1,t2]) (PFunc a b) =
do nv1 <- fresh
nv2 <- fresh
nv3 <- fresh
nv4 <- fresh
((r1,r1iso),tt1) <- constraints t1 (nv1 `PFunc` nv3)
((r2,r2iso),tt2) <- constraints t2 (nv2 `PFunc` nv4)
return (([UnifiesT a (nv1 `PProd` nv2), UnifiesT b (nv3 `PProd` nv4)]
++ (r1 ++ r2), r1iso ++ r2iso), tt1 :><: tt2)
constraints (Macro str []) (PFunc a b) =
do funcs <- gets snd
maybe (return (([],[]), TMacro str (PFunc a b) []))
(\(PFunc a' b') -> return (([UnifiesT a a',UnifiesT b b'],[]), TMacro str (PFunc a b) []))
(Map.lookup str funcs)
--constraints (Macro str lpf) (PFunc a b) =
constraints _ _ = mzero
-- | Infers a typed PF from an expected polymorphic type and an untyped term. It also receives
-- an environment of defined functions and their types.
inferPoly :: (Map.Map String PType, [(PFctr, String)]) -> PType -> PF.Term -> Maybe DynPF
inferPoly (funcs,pfcnames) gtype term =
do trace ("Inferring "++show term++"\nwith type "++show gtype++"\n") $ do
(cts,tterm) <- evalStateT (constraints term gtype) (freshvars, funcs)
s <- evalStateT (unify cts) Map.empty
DynType t@(a `TLT.Func` b) <- ptype2type gtype
let tterm' = subst s tterm
pf <- tpf2pf pfcnames t tterm'
return $ DynPF t pf
-- | Infers a typed PF from an expected type and an untyped term. It also receives
-- an environment of defined functions and their types.
infer :: (Map.Map String PType, [(PFctr,String)]) -> TLT.Type (a -> b) -> PF.Term -> Maybe (TLT.PF (a -> b))
infer (funcs,pfcnames) t@(a `TLT.Func` b) term =
do let gtype = type2ptype t
(cts,tterm) <- evalStateT (constraints term gtype) (freshvars, funcs)
s <- evalStateT (unify cts) Map.empty
let tterm' = subst s tterm
-- trace (show tterm') $ do
-- trace (show pfcnames) $ do
-- trace (show t) $ do
tpf2pf pfcnames t tterm'
-- auxiliars
fresh :: MonadPlus m => StateT ([String],t) m PType
fresh =
do name <- gets (head . fst)
modify (\(v,t) -> (tail v,t))
return (PVar name)
freshvars = ["x"++n | n <- map show [1..]]
-- examples
ex1 = mapft (PK POne ::+:: (PK PInt ::*:: PId)) PInt
ex9 = infer
(Map.empty,[])
(((TLT.Int `TLT.Prod` TLT.Char) `TLT.Prod` TLT.One) `TLT.Func` (TLT.Char))
(SND :.: FST)
ex2 = infer
(Map.empty,[(PK POne ::+:: PId,"Nat")])
(TLT.Func (TLT.One `TLT.Either` (TLT.Mu (TLT.K TLT.One TLT.:+: TLT.Id))) (TLT.Mu (TLT.K TLT.One TLT.:+: TLT.Id)))
(PF.FST PF.:.: (PF.ID PF.:/\: PF.BANG) PF.:.: PF.IN PF.:.: PF.SND :.: (PF.BANG PF.:/\: PF.ID))
ex3 = infer
((Map.insert "swap" (PFunc ((PVar "a") `PProd` (PVar "b")) ((PVar "b") `PProd` (PVar "a"))) Map.empty),[])
(((TLT.Int `TLT.Prod` TLT.Char) `TLT.Prod` TLT.One) `TLT.Func` (TLT.One `TLT.Prod` TLT.Char))
((BANG PF.:/\: (SND :.: SND)) :.: (Macro "swap" []))
--ex4 :: Maybe (TLT.PF a)
ex4 = ex3 >>= return . simplifypf TLT.typeof
ex5 = infer
((Map.insert "eithr" (((PVar "a" `PFunc` PVar "c") `PProd` (PVar "b" `PFunc` PVar "c")) `PFunc` ((PEither (PVar "a") (PVar "b")) `PFunc` PVar "c")) Map.empty),[(PK POne ::+:: PId,"Nat")])
t5 pf5
t5 = ((TLT.Either TLT.One (TLT.Mu ((TLT.K TLT.One)TLT.:+:TLT.Id))) `TLT.Func` (TLT.Mu ((TLT.K TLT.One) TLT.:+: TLT.Id)))
pf5 = PF.AP PF.:.: pf6
pf6 = pf7 PF.:/\: PF.ID
pf7 = PF.Curry pf8 PF.:.: PF.BANG
pf8 = PF.AP PF.:.: pf9
pf9 = pf10 PF.:/\: PF.SND
pf10 = (PF.Macro "eithr" []) PF.:.: pf11
pf11 = PF.Curry pf12 PF.:/\: PF.Curry pf13
pf12 = PF.IN PF.:.: PF.INL PF.:.: PF.BANG
pf13 = PF.IN PF.:.: PF.INR PF.:.: PF.SND
t6 = TLT.Id TLT.:+: (TLT.K TLT.Int TLT.:+: (TLT.K TLT.Int TLT.:*: (((TLT.Id TLT.:+: TLT.K TLT.One) TLT.:*: TLT.Id) TLT.:+: TLT.K TLT.Char)))
|
