module FrontEnd.Tc.Class( Pred, ClassHierarchy(), splitPreds, generalize, splitReduce, topDefaults, freeMetaVarsPreds, simplify, assertEntailment, assertEquivalant, Preds )where import Control.Monad.Trans import Data.Monoid import List import Monad import qualified Data.Map as Map import qualified Data.Set as Set import Doc.DocLike import Doc.PPrint import FrontEnd.Class import FrontEnd.Tc.Monad import FrontEnd.Tc.Type import FrontEnd.Tc.Kind import Name.Names import Name.Name import Options import Support.CanType import FrontEnd.Warning import qualified FlagDump as FD import qualified FlagOpts as FO generalize :: [Pred] -> Rho -> Tc Sigma generalize ps r = do ch <- getClassHierarchy r <- flattenType r fmvenv <- freeMetaVarsEnv let mvs = freeMetaVars r `Set.difference` fmvenv --(nps,rp) <- splitPreds ch (Set.toList fmvenv) ps (mvs',nps,rp) <- splitReduce (Set.toList fmvenv) (Set.toList mvs) (simplify ch ps) addPreds nps quantify mvs' rp r freeMetaVarsPreds :: Preds -> [MetaVar] freeMetaVarsPreds ps = concatMap freeMetaVarsPred ps freeMetaVarsPred :: Pred -> [MetaVar] freeMetaVarsPred (IsIn _ t) = Set.toList $ freeMetaVars t freeMetaVarsPred (IsEq t1 t2) = Set.toList (freeMetaVars t1) ++ Set.toList (freeMetaVars t2) -- | split predicates into ones that only mention metavars in the list vs other ones splitPreds :: Monad m => ClassHierarchy -> [MetaVar] -> Preds -> m (Preds, Preds) splitPreds h fs ps = do ps' <- toHnfs h ps return $ partition (all (`elem` fs) . freeMetaVarsPred) $ simplify h $ ps' toHnfs :: Monad m => ClassHierarchy -> [Pred] -> m [Pred] toHnfs h ps = mapM (toHnf h) ps >>= return . concat toHnf :: Monad m => ClassHierarchy -> Pred -> m [Pred] toHnf h p | inHnf p = return [p] | otherwise = case reducePred h p of Nothing -> fail $ "context reduction, no instance for: " ++ (pprint p) Just ps -> toHnfs h ps inHnf :: Pred -> Bool inHnf (IsEq t1 t2) = True inHnf (IsIn c t) = hnf t where hnf (TVar v) = True hnf TMetaVar {} = True hnf (TCon tc) = False hnf (TAp t _) = hnf t hnf (TArrow _t1 _t2) = False hnf TForAll {} = False hnf TExists {} = False hnf TAssoc {} = True reducePred :: Monad m => ClassHierarchy -> Pred -> m [Pred] reducePred h p@(IsEq t1 t2) = fail "reducePred" -- return [p] reducePred h p@(IsIn c t) | Just x <- foldr mplus Nothing poss = return x | otherwise = fail "reducePred" where poss = map (byInst p) (instsOf h c) simplify :: ClassHierarchy -> [Pred] -> [Pred] simplify h ps = loop [] ps where loop rs [] = rs loop rs (p:ps) | entails h (rs ++ ps) p = loop rs ps | otherwise = loop (p:rs) ps -- | returns true when set of predicates implies some other predicate is satisfied. entails :: ClassHierarchy -> [Pred] -> Pred -> Bool --entails h ps e@(IsEq {}) = error $ pprint (ps,e) entails h ps p = (p `elem` concatMap (bySuper h) ps) || case reducePred h p of Nothing -> False Just qs -> all (entails h ps) qs bySuper :: ClassHierarchy -> Pred -> [Pred] bySuper h p@IsEq {} = [p] bySuper h p@(IsIn c t) = p : concatMap (bySuper h) supers where supers = [ IsIn c' t | c' <- supersOf h c ] byInst :: Monad m => Pred -> Inst -> m [Pred] byInst p Inst { instHead = ps :=> h } = do u <- matchPred h p return (map (inst mempty (Map.fromList [ (tyvarAtom mv,t) | (mv,t) <- u ])) ps) matchPred :: Monad m => Pred -> Pred -> m [(Tyvar,Type)] matchPred x@(IsIn c t) y@(IsIn c' t') | c == c' = match t t' matchPred x y = fail $ "Classes do not match: " ++ show (x,y) supersOf :: ClassHierarchy -> Class -> [Class] supersOf ch c = asksClassRecord ch c classSupers instsOf :: ClassHierarchy -> Class -> [Inst] instsOf ch c = asksClassRecord ch c classInsts match :: Monad m => Type -> Type -> m [(Tyvar,Type)] match x y = do match' x y match' (TAp l r) (TAp l' r') = do sl <- match l l' sr <- match r r' return $ mappend sl sr match' (TArrow l r) (TArrow l' r') = do sl <- match l l' sr <- match r r' return $ mappend sl sr match' (TVar u) (TVar t) | u == t = return mempty match' (TVar mv) t | getType mv == getType t = return [(mv,t)] --match' (TMetaVar mv) t | kind mv == kind t = return [(mv,t)] match' (TCon tc1) (TCon tc2) | tc1==tc2 = return mempty match' t1 t2 = fail $ "match: " ++ show (t1,t2) -- FIXME: Use sets. splitReduce :: [MetaVar] -> [MetaVar] -> [Pred] -> Tc ([MetaVar],[Pred], [Pred]) splitReduce fs gs ps = do h <- getClassHierarchy --liftIO $ putStrLn $ pprint (fs,gs,ps) (ds, rs) <- splitPreds h fs ps --liftIO $ putStrLn $ pprint (ds,rs) (rs',sub) <- genDefaults h (fs++gs) rs --liftIO $ putStrLn $ pprint (rs') flip mapM_ sub $ \ (x,y) -> do let msg = "defaulting: " <+> pprint x <+> "=>" <+> prettyPrintType y wdump FD.BoxySteps $ liftIO $ putStrLn msg addWarn "type-defaults" msg sequence_ [ varBind x y | (x,y) <- nub sub] return (nub gs List.\\ map fst sub, ds,rs') withDefaults :: Monad m => ClassHierarchy -> [MetaVar] -> [Pred] -> m [(MetaVar, [Pred], Type)] withDefaults h vs ps | any null tss = fail $ "withDefaults.ambiguity: " ++ (pprint ps) ++ pprint vs -- ++ show ps -- | otherwise = fail $ "Zambiguity: " ++ (render $ pprint ps) ++ show (ps,ps',ams) | otherwise = return $ [ (v,qs,head ts) | (v,qs,ts) <- ams ] where ams = ambig h vs ps tss = [ ts | (v,qs,ts) <- ams ] -- Return retained predicates and a defaulting substitution genDefaults :: Monad m => ClassHierarchy -> [MetaVar] -> [Pred] -> m ([Pred],[(MetaVar,Type)]) genDefaults h vs ps = do ams <- withDefaults h vs ps let ps' = [ p | (v,qs,ts) <- ams, p<-qs ] vs = [ (v,t) | (v,qs,t) <- ams ] return (ps \\ ps', vs) -- ambiguities from THIH + call to candidates ambig :: ClassHierarchy -> [MetaVar] -> [Pred] -> [(MetaVar,[Pred],[Type])] ambig h vs ps = [ (v, qs, defs h v qs) | v <- nub (freeMetaVarsPreds ps) \\ vs, let qs = [ p | p<-ps, v `elem` freeMetaVarsPred p ] ] assertEntailment :: Preds -> Preds -> Tc () assertEntailment qs ps = do -- liftIO $ putStrLn $ "Asserting entailment: " ++ pprint (qs,ps) ch <- getClassHierarchy let ns = [ p | p <- ps, not $ entails ch qs p ] if null ns then return () else fail $ "Signature too Weak: " ++ pprint qs ++ " does not imply " ++ pprint ns assertEquivalant :: Preds -> Preds -> Tc () assertEquivalant qs ps = do assertEntailment qs ps assertEntailment ps qs {- reduce :: OptionMonad m => ClassHierarchy -> [Tyvar] -> [Tyvar] -> [Pred] -> m ([Pred], [Pred]) reduce h fs gs ps = do (ds, rs) <- split h fs ps rs' <- useDefaults h (fs++gs) rs return (ds,rs') -} -- 'candidates' from THIH defs :: ClassHierarchy -> MetaVar -> [Pred] -> [Type] defs h v qs = [ t | all ((TMetaVar v)==) ts, all (`elem` stdClasses) cs, -- XXX needs fixing any (`elem` numClasses) cs, -- XXX needs fixing t <- defaults, -- XXX needs fixing and [ entails h [] (IsIn c t) | c <- cs ]] where cs = [ c | (IsIn c t) <- qs ] ts = [ t | (IsIn c t) <- qs ] defaults :: [Type] defaults | not $ fopts FO.Defaulting = [] | otherwise = map (\name -> TCon (Tycon name kindStar)) [tc_Integer, tc_Double] topDefaults :: [Pred] -> Tc () topDefaults ps = do h <- getClassHierarchy let ams = ambig h [] ps tss = [ ts | (v,qs,ts) <- ams ] _vs = [ v | (v,qs,ts) <- ams ] when (any null tss) $ fail $ "Top Level ambiguity " ++ (pprint ps) return () -- | otherwise -> return $ Map.fromList (zip vs (map head tss)) -- where ams = ambig h [] ps -- tss = [ ts | (v,qs,ts) <- ams ] -- vs = [ v | (v,qs,ts) <- ams ] numClasses,stdClasses :: [Name] stdClasses = [ class_Eq, class_Ord, class_Enum, class_Bounded, class_Show, class_Read, class_Ix, class_Functor, class_Monad, class_Num , class_Real, class_Integral, class_Fractional, class_Floating, class_RealFrac, class_RealFloat ] numClasses = [ class_Num , class_Real, class_Integral, class_Fractional, class_Floating, class_RealFrac, class_RealFloat ]