1+ {-# LANGUAGE CPP #-}
12{-# LANGUAGE ViewPatterns #-}
23
34module Wingman.Judgements.Theta
4- ( getMethodHypothesisAtHole
5+ ( Evidence
6+ , getEvidenceAtHole
7+ , mkEvidence
8+ , evidenceToSubst
9+ , evidenceToHypothesis
510 ) where
611
7- import Data.Maybe (fromMaybe )
12+ import Data.Maybe (fromMaybe , mapMaybe )
813import Data.Set (Set )
914import qualified Data.Set as S
1015import Development.IDE.GHC.Compat
11- import Generics.SYB
12- import GhcPlugins (EvVar , mkVarOcc )
16+ import Generics.SYB hiding (tyConName )
17+ import GhcPlugins (mkVarOcc , splitTyConApp_maybe , getTyVar_maybe )
18+ #if __GLASGOW_HASKELL__ > 806
19+ import GhcPlugins (eqTyCon )
20+ #else
21+ import GhcPlugins (nameRdrName , tyConName )
22+ import PrelNames (eqTyCon_RDR )
23+ #endif
24+ import TcEvidence
25+ import TcType (tcTyConAppTyCon_maybe )
26+ import TysPrim (eqPrimTyCon )
1327import Wingman.Machinery
1428import Wingman.Types
1529
1630
1731------------------------------------------------------------------------------
18- -- | Create a 'Hypothesis' containing 'ClassMethodPrv' provenance. For every
19- -- dictionary that is in scope at the given 'SrcSpan', find every method and
20- -- superclass method available.
21- getMethodHypothesisAtHole :: SrcSpan -> LHsBinds GhcTc -> Hypothesis CType
22- getMethodHypothesisAtHole dst
23- = Hypothesis
24- . excludeForbiddenMethods
25- . fromMaybe []
26- . foldMap methodHypothesis
27- . (everything (<>) $ mkQ mempty $ evbinds dst)
32+ -- | Something we've learned about the type environment.
33+ data Evidence
34+ -- | The two types are equal, via a @a ~ b@ relationship
35+ = EqualityOfTypes Type Type
36+ -- | We have an instance in scope
37+ | HasInstance PredType
38+ deriving (Show )
39+
40+
41+ ------------------------------------------------------------------------------
42+ -- | Given a 'PredType', pull an 'Evidence' out of it.
43+ mkEvidence :: PredType -> Maybe Evidence
44+ mkEvidence (getEqualityTheta -> Just (a, b))
45+ = Just $ EqualityOfTypes a b
46+ mkEvidence inst@ (tcTyConAppTyCon_maybe -> Just (isClassTyCon -> True
47+ = Just $ HasInstance inst
48+ mkEvidence _ = Nothing
49+
50+
51+ ------------------------------------------------------------------------------
52+ -- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
53+ getEvidenceAtHole :: SrcSpan -> LHsBinds GhcTc -> [Evidence ]
54+ getEvidenceAtHole dst
55+ = mapMaybe mkEvidence
56+ . (everything (<>) $
57+ mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
58+
59+
60+ ------------------------------------------------------------------------------
61+ -- | Update our knowledge of which types are equal.
62+ evidenceToSubst :: Evidence -> TacticState -> TacticState
63+ evidenceToSubst (EqualityOfTypes a b) ts =
64+ let tyvars = S. fromList $ mapMaybe getTyVar_maybe [a, b]
65+ -- If we can unify our skolems, at least one is no longer a skolem.
66+ -- Removing them from this set ensures we can get a subtitution between
67+ -- the two. But it's okay to leave them in 'ts_skolems' in general, since
68+ -- they won't exist after running this substitution.
69+ skolems = ts_skolems ts S. \\
70+ in
71+ case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
72+ Just subst -> updateSubst subst ts
73+ Nothing -> ts
74+ evidenceToSubst HasInstance {} ts = ts
75+
76+
77+ ------------------------------------------------------------------------------
78+ -- | Get all of the methods that are in scope from this piece of 'Evidence'.
79+ evidenceToHypothesis :: Evidence -> Hypothesis CType
80+ evidenceToHypothesis EqualityOfTypes {} = mempty
81+ evidenceToHypothesis (HasInstance t) =
82+ Hypothesis . excludeForbiddenMethods . fromMaybe [] $ methodHypothesis t
83+
84+
85+ ------------------------------------------------------------------------------
86+ -- | Given @a ~ b@ or @a ~# b@, returns @Just (a, b)@, otherwise @Nothing@.
87+ getEqualityTheta :: PredType -> Maybe Type , Type )
88+ getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k, a, b]))
89+ #if __GLASGOW_HASKELL__ > 806
90+ | tc == eqTyCon
91+ #else
92+ | nameRdrName (tyConName tc) == eqTyCon_RDR
93+ #endif
94+ = Just (a, b)
95+ getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k1, _k2, a, b]))
96+ | tc == eqPrimTyCon = Just (a, b)
97+ getEqualityTheta _ = Nothing
2898
2999
30100------------------------------------------------------------------------------
@@ -38,13 +108,48 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name
38108 forbiddenMethods = S. map mkVarOcc $ S. fromList
39109 [ -- monadfail
40110 " fail"
111+ -- show
112+ , " showsPrec"
113+ , " showList"
41114 ]
42115
43116
44117------------------------------------------------------------------------------
45- -- | Extract the types of the evidence bindings in scope.
46- evbinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType ]
47- evbinds dst (L src (AbsBinds _ _ h _ _ _ _))
118+ -- | Extract evidence from 'AbsBinds' in scope.
119+ absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType ]
120+ absBinds dst (L src (AbsBinds _ _ h _ _ _ _))
48121 | dst `isSubspanOf` src = fmap idType h
49- evbinds _ _ = []
122+ absBinds _ _ = []
123+
124+
125+ ------------------------------------------------------------------------------
126+ -- | Extract evidence from 'HsWrapper's in scope
127+ wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType ]
128+ wrapperBinds dst (L src (HsWrap _ h _))
129+ | dst `isSubspanOf` src = wrapper h
130+ wrapperBinds _ _ = []
131+
132+
133+ ------------------------------------------------------------------------------
134+ -- | Extract evidence from the 'ConPatOut's bound in this 'Match'.
135+ matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc ) -> [PredType ]
136+ matchBinds dst (L src (Match _ _ pats _))
137+ | dst `isSubspanOf` src = everything (<>) (mkQ mempty patBinds) pats
138+ matchBinds _ _ = []
139+
140+
141+ ------------------------------------------------------------------------------
142+ -- | Extract evidence from a 'ConPatOut'.
143+ patBinds :: Pat GhcTc -> [PredType ]
144+ patBinds (ConPatOut { pat_dicts = dicts })
145+ = fmap idType dicts
146+ patBinds _ = []
147+
148+
149+ ------------------------------------------------------------------------------
150+ -- | Extract the types of the evidence bindings in scope.
151+ wrapper :: HsWrapper -> [PredType ]
152+ wrapper (WpCompose h h2) = wrapper h <> wrapper h2
153+ wrapper (WpEvLam v) = [idType v]
154+ wrapper _ = []
50155
0 commit comments