module Infernu.Infer
( runTypeInference
, test
, Pretty(..)
, pretty
, getAnnotations
, minifyVars
, TypeError
)
where
import Control.Monad (foldM, forM)
import qualified Data.Graph.Inductive as Graph
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Maybe (mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (foldr, mapM, sequence)
import Data.List (intercalate)
import Infernu.Prelude
import qualified Infernu.Builtins.Operators as Operators
import Infernu.InferState
import Infernu.Lib (safeLookup)
import Infernu.Log
import Infernu.Pretty
import Infernu.Types
import Infernu.Unify (unify, unifyAll, unifyPending, unifyPredsL, unifyRowPropertyBiased, unifyl)
getQuantificands :: TypeScheme -> [TVarName]
getQuantificands (TScheme tvars _) = tvars
getAnnotations :: Exp a -> [a]
getAnnotations = foldr (:) []
closeRowList :: TRowList Type -> TRowList Type
closeRowList (TRowProp n t rest) = TRowProp n t (closeRowList rest)
closeRowList (TRowEnd _) = TRowEnd Nothing
closeRow :: Type -> Type
closeRow (Fix (TRow r)) = Fix . TRow $ closeRowList r
closeRow t = t
accumInfer :: TypeEnv -> [Exp Source] -> Infer [(QualType, Exp (Source, QualType))]
accumInfer env =
do traceLog ("accumInfer: env: " ++ pretty env)
foldM accumInfer' []
where accumInfer' types expr =
do (t, e) <- inferType env expr
return ((t,e):types)
inferType :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType env expr = do
traceLog (">> " ++ pretty expr ++ " -- env: " ++ pretty env)
(t, e) <- inferType' env expr
unifyPending
s <- getMainSubst
st <- getState
traceLog (">> " ++ pretty expr ++ " -- inferred :: " ++ pretty (applySubst s t))
traceLog (" infer state: " ++ prettyTab 3 st)
return (applySubst s t, fmap (applySubst s) e)
inferType' :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType' _ (ELit a lit) = do
let t = Fix $ TBody $ case lit of
LitNumber _ -> TNumber
LitBoolean _ -> TBoolean
LitString _ -> TString
LitRegex{} -> TRegex
LitUndefined -> TUndefined
LitNull -> TNull
return (qualEmpty t, ELit (a, qualEmpty t) lit)
inferType' env (EVar a n) =
do t <- instantiateVar a n env
return (t, EVar (a, t) n)
inferType' env (EAbs a argNames e2) =
do argTypes <- forM argNames (const $ Fix . TBody . TVar <$> fresh)
env' <- foldM (\e (n, t) -> addVarScheme e n $ schemeEmpty t) env $ zip argNames argTypes
(t1, e2') <- inferType env' e2
pred' <- unifyPredsL a $ qualPred t1
let t = TQual pred' $ Fix $ TFunc argTypes (qualType t1)
return (t, EAbs (a, t) argNames e2')
inferType' env (EApp a e1 eArgs) =
do tvar <- Fix . TBody . TVar <$> fresh
(t1, e1') <- inferType env e1
traceLog $ "EApp: Inferred type for func expr: " ++ pretty t1
argsTE <- accumInfer env eArgs
traceLog $ "EApp: Inferred types for func args: " ++ intercalate ", " (map pretty argsTE)
let rargsTE = reverse argsTE
tArgs = map fst rargsTE
eArgs' = map snd rargsTE
preds = concatMap qualPred $ t1:tArgs
unify a (qualType t1) (Fix $ TFunc (map qualType tArgs) tvar)
traceLog $ "Inferred preds: " ++ intercalate ", " (map pretty preds)
tvar' <- do pred' <- unifyPredsL a preds
tvarSubsted <- applyMainSubst tvar
return $ TQual pred' tvarSubsted
traceLog ("Inferred func application: " ++ pretty tvar')
return (tvar', EApp (a, tvar') e1' eArgs')
inferType' env (ENew a e1 eArgs) =
do (t1, e1') <- inferType env e1
argsTE <- accumInfer env eArgs
thisT <- Fix . TBody . TVar <$> fresh
resT <- Fix . TBody . TVar <$> fresh
let rargsTE = reverse argsTE
tArgs = thisT : map (qualType . fst) rargsTE
eArgs' = map snd rargsTE
preds = concatMap qualPred $ t1 : map fst argsTE
unify a (qualType t1) (Fix $ TFunc tArgs resT)
rowConstraintVar <- RowTVar <$> fresh
unify a (Fix . TRow . TRowEnd $ Just rowConstraintVar) thisT
resolvedThisT <- applyMainSubst thisT
unify a thisT (closeRow resolvedThisT)
preds' <- unifyPredsL a preds
let thisT' = TQual preds' thisT
return (thisT', ENew (a, thisT') e1' eArgs')
inferType' env (ELet a n e1 e2) =
do recType <- Fix . TBody . TVar <$> fresh
recEnv <- addVarScheme env n $ schemeEmpty recType
(t1, e1') <- inferType recEnv e1
unify a (qualType t1) recType
t' <- generalize e1 env t1
env' <- addVarScheme env n t'
(t2, e2') <- inferType env' e2
preds' <- unifyPredsL a $ concatMap qualPred [t1, t2]
let resT = TQual preds' $ qualType t2
return (resT, ELet (a, resT) n e1' e2')
inferType' env expr@(EAssign a n expr1 expr2) =
do traceLog $ "EAssign: " ++ pretty expr
lvalueScheme <- getVarScheme a n env `failWithM` throwError a ("Unbound variable: " ++ show n ++ " in assignment " ++ pretty expr1)
traceLog $ "EAssign lvalueScheme: " ++ pretty lvalueScheme
lvalueT <- instantiate lvalueScheme
(rvalueT, expr1') <- inferType env expr1
unify a (qualType lvalueT) (qualType rvalueT)
(tRest, expr2') <- inferType env expr2
traceLog $ "EAssign lvalueT: " ++ pretty lvalueT
traceLog $ "EAssign Invoking unifyAllInstances on scheme: " ++ pretty lvalueScheme
instancePreds <- unifyAllInstances a $ getQuantificands lvalueScheme
preds <- unifyPredsL a $ concat $ (instancePreds:) $ map qualPred [lvalueT, rvalueT, tRest]
varId <- getVarId n env `failWith` throwError a ("Unbound variable: '" ++ show n ++ "'")
updatedScheme <- generalize expr1 env (schemeType lvalueScheme)
_ <- setVarScheme env n updatedScheme varId
let tRest' = TQual preds $ qualType tRest
return (tRest', EAssign (a, tRest') n expr1' expr2')
inferType' env (EPropAssign a objExpr n expr1 expr2) =
do (objT, objExpr') <- inferType env objExpr
(rvalueT, expr1') <- inferType env expr1
rowTailVar <- RowTVar <$> fresh
let rvalueScheme = schemeFromQual rvalueT
rank0Unify = unify a (qualType objT) $ Fix . TRow $ TRowProp n rvalueScheme $ TRowEnd (Just rowTailVar)
case unFix (qualType objT) of
TRow trowList ->
case Map.lookup n . fst $ flattenRow trowList of
Just lvalueScheme ->
do generalizedRvalue <- generalize expr1 env rvalueT
unifyRowPropertyBiased a rank0Unify (lvalueScheme, generalizedRvalue)
Nothing -> rank0Unify
_ -> rank0Unify
(expr2T, expr2') <- inferType env expr2
preds <- unifyPredsL a $ concatMap qualPred [objT, rvalueT, expr2T]
let tRes = TQual preds $ qualType expr2T
return (tRes, EPropAssign (a, tRes) objExpr' n expr1' expr2')
inferType' env (EIndexAssign a eArr eIdx expr1 expr2) =
do (tArr, eArr') <- inferType env eArr
elemTVarName <- fresh
arrTVarName <- fresh
idxTVarName <- fresh
let elemType = Fix . TBody . TVar $ elemTVarName
unify a (qualType tArr) $ Fix $ TBody $ TVar arrTVarName
(tId, eIdx') <- inferType env eIdx
unify a (qualType tId) $ Fix $ TBody $ TVar idxTVarName
(tExpr1, expr1') <- inferType env expr1
unify a (qualType tExpr1) elemType
(tExpr2, expr2') <- inferType env expr2
let curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
preds <- unifyPredsL a $ concat $ ([curPred]:) $ map qualPred [tArr, tId, tExpr1, tExpr2]
let tRes = TQual preds $ qualType tExpr2
return (tRes , EIndexAssign (a, tRes) eArr' eIdx' expr1' expr2')
inferType' env (EArray a exprs) =
do tv <- Fix . TBody . TVar <$> fresh
te <- accumInfer env exprs
let types = map (qualType . fst) te
unifyl unify a $ zip (tv:types) types
let t = qualEmpty $ Fix $ TCons TArray [tv]
return (t, EArray (a,t) $ map snd te)
inferType' env (ETuple a exprs) =
do te <- accumInfer env exprs
let t = TQual (concatMap (qualPred . fst) te) $ Fix . TCons TTuple . reverse $ map (qualType . fst) te
return (t, ETuple (a,t) $ map snd te)
inferType' env (EStringMap a exprs') =
do let exprs = map snd exprs'
elemType <- Fix . TBody . TVar <$> fresh
te <- accumInfer env exprs
let types = map (qualType . fst) te
unifyAll a $ elemType:types
allPreds <- unifyPredsL a . concatMap qualPred $ map fst te
let t = TQual { qualPred = allPreds, qualType = Fix $ TCons TStringMap [elemType] }
return (t, EStringMap (a,t) $ zip (map fst exprs') (map snd te))
inferType' env (ERow a isOpen propExprs) =
do te <- accumInfer env $ map snd propExprs
endVar <- RowTVar <$> fresh
let propNamesTypes = zip propExprs (reverse $ map fst te)
rowEnd' = TRowEnd $ if isOpen then Just endVar else Nothing
accumRowProp' row ((propName, propExpr), propType) =
do ts <- generalize propExpr env propType
return $ TRowProp propName ts row
rowType <- qualEmpty . Fix . TRow <$> foldM accumRowProp' rowEnd' propNamesTypes
return (rowType, ERow (a,rowType) isOpen $ zip (map fst propExprs) (map snd te))
inferType' env (ECase a eTest eBranches) =
do (eType, eTest') <- inferType env eTest
infPatterns <- accumInfer env $ map (ELit a . fst) eBranches
let patternTypes = map (qualType . fst) infPatterns
unifyAll a $ (qualType eType):patternTypes
infBranches <- accumInfer env $ map snd eBranches
let branchTypes = map (qualType . fst) infBranches
unifyAll a branchTypes
allPreds <- unifyPredsL a . concatMap qualPred $ eType : (map fst infPatterns) ++ (map fst infBranches)
let tRes = TQual { qualPred = allPreds, qualType = qualType . fst $ head infBranches }
return (tRes, ECase (a, tRes) eTest' $ zip (map fst eBranches) (map snd infBranches))
inferType' env (EProp a eObj propName) =
do (tObj, eObj') <- inferType env eObj
rowVar <- RowTVar <$> fresh
propTypeScheme <- schemeEmpty . Fix . TBody . TVar <$> fresh
unify a (Fix . TRow $ TRowProp propName propTypeScheme $ TRowEnd (Just rowVar)) (qualType tObj)
propType <- instantiate propTypeScheme
return (propType, EProp (a,propType) eObj' propName)
inferType' env (EIndex a eArr eIdx) =
do (tArr, eArr') <- inferType env eArr
elemTVarName <- fresh
arrTVarName <- fresh
idxTVarName <- fresh
unify a (qualType tArr) (Fix $ TBody $ TVar arrTVarName)
(tId, eIdx') <- inferType env eIdx
unify a (qualType tId) (Fix $ TBody $ TVar idxTVarName)
let elemType' = qualEmpty $ Fix $ TBody $ TVar elemTVarName
curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
preds <- unifyPredsL a $ (curPred:) $ concatMap qualPred [tArr, tId]
let tRes = TQual preds $ qualType elemType'
return (tRes, EIndex (a, tRes) eArr' eIdx')
indexAccessPred :: TVarName -> TVarName -> TVarName -> TPred Type
indexAccessPred arrTVarName elemTVarName idxTVarName =
let
mkv = Fix . TBody . TVar
in
TPredIsIn (ClassName "Indexable") (Fix $ TCons TTuple
[ mkv arrTVarName
, mkv idxTVarName
, mkv elemTVarName
])
unifyAllInstances :: Source -> [TVarName] -> Infer [TPred Type]
unifyAllInstances a tvs = do
m <- getVarInstances
traceLog $ "unifyAllInstances: " ++ pretty a ++ " Unifying all instances of tvars: " ++ intercalate ", " (map pretty tvs)
let equivalenceSets = map Set.fromList $ filter (not . null) $ map (mapMaybe $ Graph.lab m) $ map (flip Graph.bfs m) tvs
unifyAll' equivs =
do let equivsL = Set.toList equivs
qequivsL = map qualType equivsL
traceLog $ "unifyAllInstances - equivalence:" ++ pretty qequivsL
unifyAll a qequivsL
return $ concatMap qualPred equivsL
pred' <- concat <$> mapM unifyAll' equivalenceSets
unifyPredsL a pred'
createEnv :: Map EVarName TypeScheme -> Infer (Map EVarName VarId)
createEnv builtins = foldM addVarScheme' Map.empty $ Map.toList builtins
where allTVars :: TypeScheme -> Set TVarName
allTVars (TScheme qvars t) = freeTypeVars t `Set.union` Set.fromList qvars
addVarScheme' :: Map EVarName VarId -> (EVarName, TypeScheme) -> Infer (Map EVarName VarId)
addVarScheme' m (name, tscheme) =
do allocNames <- forM (Set.toList $ allTVars tscheme)
$ \tvName -> (tvName,) <$> fresh
addVarScheme m name $ mapVarNames (safeLookup allocNames) tscheme
typeInference :: Map EVarName TypeScheme -> Exp Source -> Infer (Exp (Source, QualType))
typeInference builtins e =
do env <- createEnv builtins
(_t, e') <- inferType env e
return e'
test :: Exp Source -> String
test e = case runTypeInference e of
Left err -> pretty err
Right expr -> pretty $ snd . head . getAnnotations . minifyVars $ expr
runTypeInference :: Exp Source -> Either TypeError (Exp (Source, QualType))
runTypeInference e = runInfer $ typeInference Operators.builtins e