@@ -13,6 +13,8 @@
1313--
1414-----------------------------------------------------------------------------
1515
16+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
17+
1618module Language.PureScript.TypeChecker.Entailment (
1719 entails
1820) where
@@ -26,6 +28,7 @@ import qualified Data.Map as M
2628import Control.Applicative
2729import Control.Arrow (Arrow(..))
2830import Control.Monad.Except
31+import Control.Monad.State
2932
3033import Language.PureScript.AST
3134import Language.PureScript.Errors
@@ -38,6 +41,8 @@ import Language.PureScript.TypeClassDictionaries
3841import Language.PureScript.Types
3942import qualified Language.PureScript.Constants as C
4043
44+newtype Work = Work Integer deriving (Show, Eq, Ord, Num)
45+
4146-- |
4247-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
4348-- return a type class dictionary reference.
@@ -54,47 +59,59 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
5459 filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
5560 filterModule _ = False
5661
57− solve context' (className, tys) trySuperclasses =
58− checkOverlaps $ go trySuperclasses className tys
62+ solve :: [TypeClassDictionaryInScope] -> Constraint -> Bool -> Check Expr
63+ solve context' (className, tys) trySuperclasses = do
64+ let dicts = flip evalStateT (Work 0) $ go trySuperclasses className tys
65+ checkOverlaps dicts
5966 where
60− go trySuperclasses' className' tys' =
61− -- Look for regular type instances
62− [ mkDictionary (canonicalizeDictionary tcd) args
63− | tcd <- context'
64− -- Make sure the type class name matches the one we are trying to satisfy
65− , className' == tcdClassName tcd
66− -- Make sure the type unifies with the type in the type instance definition
67− , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
68− -- Solve any necessary subgoals
69− , args <- solveSubgoals subst (tcdDependencies tcd) ] ++
67+ go :: Bool -> Qualified ProperName -> [Type] -> StateT Work [] DictionaryValue
68+ go trySuperclasses' className' tys' = do
69+ workDone <- get
70+ guard $ workDone < 1000
71+ modify (1 +)
72+ directInstances <|> superclassInstances
73+ where
74+ directInstances :: StateT Work [] DictionaryValue
75+ directInstances = do
76+ tcd <- lift context'
77+ -- Make sure the type class name matches the one we are trying to satisfy
78+ guard $ className' == tcdClassName tcd
79+ -- Make sure the type unifies with the type in the type instance definition
80+ subst <- lift . maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
81+ -- Solve any necessary subgoals
82+ args <- solveSubgoals subst (tcdDependencies tcd)
83+ return $ mkDictionary (canonicalizeDictionary tcd) args
7084
71− -- Look for implementations via superclasses
72− [ SubclassDictionaryValue suDict superclass index
73− | trySuperclasses'
74− , (subclassName, (args, _, implies)) <- M.toList (typeClasses env)
75− -- Try each superclass
76− , (index, (superclass, suTyArgs)) <- zip [0..] implies
77− -- Make sure the type class name matches the superclass name
78− , className' == superclass
79− -- Make sure the types unify with the types in the superclass implication
80− , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' suTyArgs
81− -- Finally, satisfy the subclass constraint
82− , args' <- maybeToList $ mapM ((`lookup` subst) . fst) args
83− , suDict <- go True subclassName args' ]
85+ superclassInstances :: StateT Work [] DictionaryValue
86+ superclassInstances = do
87+ guard trySuperclasses'
88+ (subclassName, (args, _, implies)) <- lift $ M.toList (typeClasses env)
89+ -- Try each superclass
90+ (index, (superclass, suTyArgs)) <- lift $ zip [0..] implies
91+ -- Make sure the type class name matches the superclass name
92+ guard $ className' == superclass
93+ -- Make sure the types unify with the types in the superclass implication
94+ subst <- lift . maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' suTyArgs
95+ -- Finally, satisfy the subclass constraint
96+ args' <- lift . maybeToList $ mapM ((`lookup` subst) . fst) args
97+ suDict <- go True subclassName args'
98+ return $ SubclassDictionaryValue suDict superclass index
8499
85100 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
86101 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
87102 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
88− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> [Maybe [DictionaryValue]]
103+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT Work [] (Maybe [DictionaryValue])
89104 solveSubgoals _ Nothing = return Nothing
90105 solveSubgoals subst (Just subgoals) = do
91106 dict <- mapM (uncurry (go True) . second (map (replaceAllTypeVars subst))) subgoals
92107 return $ Just dict
108+
93109 -- Make a dictionary from subgoal dictionaries by applying the correct function
94110 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
95111 mkDictionary fnName Nothing = LocalDictionaryValue fnName
96112 mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
97113 mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
114+
98115 -- Turn a DictionaryValue into a Expr
99116 dictionaryValueToValue :: DictionaryValue -> Expr
100117 dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName