module UHC.Light.Compiler.AnaDomain.Utils ( RelevTyQuantHow (..) , relevtyQuant , relevQualRemoveAmbig , assSolve , relevTyArgsFromCTag , relevTyArgs ) where import UHC.Light.Compiler.Base.HsName.Builtin import UHC.Light.Compiler.Base.Common import UHC.Light.Compiler.Opts import UHC.Light.Compiler.VarMp import UHC.Light.Compiler.Substitutable import UHC.Light.Compiler.AnaDomain import UHC.Light.Compiler.AnaDomain.Trf.Subst import UHC.Light.Compiler.AnaDomain.Ftv import UHC.Light.Compiler.Gam.DataGam import qualified Data.Map as Map import qualified Data.Set as Set import Data.Array import Data.Maybe import Data.List import UHC.Util.Utils import Control.Monad.State import Control.Applicative import UHC.Light.Compiler.Base.Debug import UHC.Util.Pretty import UHC.Light.Compiler.AnaDomain.Pretty {-# LINE 37 "src/ehc/AnaDomain/Utils.chs" #-} -- | configuring quantification, for debugging data RelevTyQuantHow = RelevTyQuantHow_Solve -- solve | RelevTyQuantHow_RemoveAmbig -- constraints over vars not in type are removed | RelevTyQuantHow_VarDefaultToTop -- vars left over, and in type, are defaulted to top | RelevTyQuantHow_Quant -- quant | RelevTyQuantHow_Rec -- for recursive use deriving Eq {-# LINE 48 "src/ehc/AnaDomain/Utils.chs" #-} relevtyQuant :: [RelevTyQuantHow] -> RVarMp -> RelevQualS -> RelevTy -> ( RelevTy , RVarMp -- extra subst , RelevQualS -- removed quals ) relevtyQuant how m qs t = case funTy of t'@(RelevTy_Fun _ _ _ as r) | RelevTyQuantHow_Rec `elem` how -> ( RelevTy_Fun RQuant_Rec (varFree t') [] as r , emptyRVarMp , Set.empty ) t'@(RelevTy_Fun _ _ _ as r) -> ( RelevTy_Fun RQuant_Forall quantOver qs4 as' r' , solveVarMp , qs3rem ) where ftvT = varFreeSet t' (qs2,solveVarMp) | RelevTyQuantHow_Solve `elem` how = assSolve ftvT qsm | otherwise = (qsm, emptyRVarMp) where qsm = Set.map (varUpd m) qs as' = solveVarMp `varUpd` as r' = solveVarMp `varUpd` r ftvT' = varFreeSet as' `Set.union` varFreeSet r' (qs3,qs3rem) | RelevTyQuantHow_RemoveAmbig `elem` how = relevQualRemoveAmbig ftvT' qsm | otherwise = (qsm, Set.empty) where qsm = Set.map (varUpd solveVarMp) qs2 qs4 = Set.toList qs3 ftvTQ = ftvT' `Set.union` varFreeSet qs4 quantOver | RelevTyQuantHow_Quant `elem` how = Set.toList ftvTQ | otherwise = [] t' -> ( t' , emptyRVarMp , Set.empty ) where funTy = case m `varUpd` t of t'@(RelevTy_Fun _ _ _ _ _) -> t' t' -> RelevTy_Fun RQuant_None [] [] [] t' {-# LINE 98 "src/ehc/AnaDomain/Utils.chs" #-} -- | Remove unresolvable constraints, and those referring to free vars relevQualRemoveAmbig :: UIDS -> RelevQualS -> (RelevQualS,RelevQualS) relevQualRemoveAmbig bound qualS = Set.partition ok qualS where -- ok (RelevQual_Alt _ _ _ _ _ _) = False ok q = varFreeSet q `Set.isSubsetOf` bound {-# LINE 111 "src/ehc/AnaDomain/Utils.chs" #-} instance VarUpdatable RelevTy RVarMp where varUpd = relevtyAppVarLookup instance VarExtractable RelevTy UID where varFreeSet = relevTyFtv {-# LINE 119 "src/ehc/AnaDomain/Utils.chs" #-} instance VarUpdatable RelevQual RVarMp where varUpd = relevqualAppVarLookup instance VarExtractable RelevQual UID where varFreeSet = relevQualFtv {-# LINE 127 "src/ehc/AnaDomain/Utils.chs" #-} instance VarUpdatable RelevCoe RVarMp where varUpd = relevcoeAppVarLookup instance VarExtractable RelevCoe UID where varFreeSet = relevCoeFtv {-# LINE 163 "src/ehc/AnaDomain/Utils.chs" #-} type WL = Map.Map UID (Set.Set Int) data ASS = ASS { assWl :: !WL , assWlRedo :: !WL , assQm :: !(Map.Map Int RelevQual) , assVm :: !RVarMp , assProgress :: !Bool , assSolved :: !(Set.Set Int) , assReduced :: !(Set.Set Int) , assWlSize :: !Int , assWlPos :: !Int } assSolve :: UIDS -> RelevQualS -> (RelevQualS,RVarMp) assSolve bound qualS = -- maybe (qualS, emptyRVarMp) (\ass -> ( Set.map (qual $ assQm ass) $ (Set.unions $ Map.elems (assWl ass)) `Set.difference` assSolved ass , assVm ass ) ) --- $ tr "assSolve" (pp (show bound)) $ solve (ASS wlInit Map.empty initQualM emptyRVarMp False Set.empty Set.empty (Map.size wlInit) 0) where -- solver solve ass@(ASS {assWl=wl, assQm=qualM, assWlPos=wlPos, assWlSize=wlSize}) | check_pos {- _vUnbound -} && isJust mbN = -- tr ("solve: isJust mbN") (v >#< show is >-< "slv :" >#< show (assSolved ass) >-< "slvN:" >#< show (assSolved $ fromJust mbN) >-< "wl :" >#< show wl >-< "wlRedo:" >#< show (assWlRedo $ fromJust mbN) >-< show (assQm ass) >-< show (assQm $ fromJust mbN)) $ solve ((fromJust mbN) {assProgress = True, assWlPos = wlPos + 1}) | check_pos = -- tr ("solve: wlSz > 0(" ++ show wlSz ++ ")") (v >#< show is0 >#< show is >-< show wl) $ solve (ass {assWlPos = wlPos + 1}) | assProgress ass = -- tr ("solve: assProgress ass && Map.size wlRedo > 0") (Map.size wl >#< show wl >-< Map.size wlRedo >#< show wlRedo) $ let wl' = Map.filter (\s -> not (Set.null s)) wl in solve (ass {assProgress = False, assWlPos=0, assWl = wl', assWlSize = Map.size wl'}) | otherwise = -- tr ("solve: done") ("assVm:" >#< assVm ass) $ ass where (v,is0) = Map.elemAt (assWlPos ass) wl is = is0 `Set.difference` assSolved ass (isReduced,isToSolve) = splitRedSlv1 qualM is -- the real solving work attempts mbN = solveN v is ass -- checks, to be shared in guards check_pos = wlPos < wlSize -- split into those which cannot be further solved, and the rest splitRedSlv1 m = Set.partition (\i -> varFreeSet (qual m i) `Set.isSubsetOf` bound) -- solve combination of all quals related to single AnaEval var solveN v is ass@(ASS {assWl=wl, assQm=qualM}) = do (q,s,slv,_) <- solveQN1 (l) v (r) let (qualM2,isNw) = qmAddL q qualM slvS = Set.fromList slv touchedBySubs = (Set.fold (\v is -> is `Set.union` Map.findWithDefault Set.empty v wl) Set.empty $ Set.delete v $ rvarmpKeysSet s) `Set.difference` assSolved ass (qualM3,wl') = updQualWl slvS s wl qualM2 $ Set.toList $ Set.unions [isNw, is, touchedBySubs] `Set.difference` slvS -- filter (\i -> Set.notMember i slvS) $ isNw ++ isL updAss wl' qualM3 s slvS ass where isL = Set.toList is (l, r, o) = split ([],[],[]) [ (qual qualM i, i) | i <- isL ] split (l,r,o) (( RelevQual_SubEval a1 (AnaEval_Var v2), i) : qs) | v2 == v = split ((i,a1):l, r, o) qs split (l,r,o) (( RelevQual_SubEval (AnaEval_Var v1) a2, i) : qs) | v1 == v = split ( l, (i,a2):r, o) qs split (l,r,o) (( _ , i) : qs) = split ( l, r, i:o) qs split res _ = res -- access qual via index qual m q = panicJust "amsSolve.qual" $ Map.lookup q m -- update qualM updQualWl slvS s wl qm is = (qm', wl') where qm' = foldr (\i m -> Map.update (\q -> Just $ s `varUpd` q) i m) qm is wl' = wlAddL qm' is wl -- update ass when something is solved updAss wl qm s slv ass = Just (ass {assWl=wl, assQm=qm, assVm= s |+> assVm ass, assSolved = Set.union slv $ assSolved ass}) -- worklist: initial + remainder; TBD: variable-less quals need to be checked for being tautology wlAdd m q wl = foldr (add q) wl (varFree (qual m q)) where add q v wl = Map.alter (Just . maybe (Set.singleton q) (Set.insert q)) v wl wlAddL m qs wl = foldr (wlAdd m) wl qs -- get worklist to solve wlInit = wlAddL initQualM (Map.keys initQualM) Map.empty -- solve a combi of quals with sharing of middle AnaEval var solveQN1 (als) var (ars) = -- (\x -> tr "solveQN1.res" (ppCommas als >-< var >|< ppParens varIsBound >-< ppCommas ars >-< "=>" >#< maybe (pp "-") (\(q,s,slv,reason) -> (reason ++ ":") >#< "qual:" >#< q >#< "subs:" >#< s >-< "slv:" >#< show slv) x) x) $ case (als,ars) of {- -} -- transitive, no alternatives (ll1, rr1) | canDo && isJust mbJn -> return ( (if null ll1 || null rr1 then [] else [RelevQual_SubEval jn mt]) ++ varConstraint , amsLocalVarMp ams2 , (slv $ als ++ ars) , "transitivity 1" ) | canDo -- weaker transitivity where meet is distributed over the left sides -> return ( [ RelevQual_SubEval a mt | a <- alsq ] ++ varConstraint , amsLocalVarMp ams1 , (slv $ als ++ ars) , "transitivity 2" ) where canDo = varIsFree && not (null ll1) && not (null rr1) && isJust mbMt mbMt@(~(Just (mt,ams1))) = if null rr1 then Just (top,ams0) else r1 ams0 meetl arsq mbJn@(~(Just (jn,ams2))) = if null ll1 then Just (bot,ams1) else r1 ams1 joinl alsq varConstraint = if null rr1 then [] else [RelevQual_SubEval (AnaEval_Var var) mt] -- symmetry {- -} ((_:_), (_:_)) | not (null lr) -> case lr of ((l,v,r):_) -> return ( [], bind, [l,r] , "symmetry" ) where bind | varIsFree = bindAnaEval var (AnaEval_Var v ) | not $ v `Set.member` bound = bindAnaEval v (AnaEval_Var var) | otherwise = emptyRVarMp where mbV l = [ (fromJust mbv,i) | (i,a) <- l, let mbv = isVar a, isJust mbv ] l = mbV als r = mbV ars lr = [ (il, v, fromJust mbr) | (v,il) <- l, let mbr = lookup v r, isJust mbr ] -- reflexivity {- -} ((_:_), _) | not (null l) -> case l of (i:_) -> return ( [], emptyRVarMp, [i] , "reflexivity" ) where l = [ i | (i,a) <- als, maybe False (==var) (isVar a) ] -- a free var which is not left constrained anymore, simplifies to the right side ([], (_:_:_)) | isJust mbMt -> return ( [RelevQual_SubEval (AnaEval_Var var) mt], amsLocalVarMp ams1, slv ars , "right meet" ) where mbMt@(~(Just (mt,ams1))) = r1 ams0 meetl arsq {- ([], (_:_)) | varIsFree -> do (mt,ams1) <- r1 ams0 meetl arsq return ( [], bindAnaEval var mt |+> amsLocalVarMp ams1, slv ars , "right meet" ) -} {- -- a free var not right constrained anymore, is just forgotten, which is pessimistic because we cannot infer 'more info', i.e. down in the lattice ((_:_), []) | varIsFree -> return ( [], emptyRVarMp, slv als, "left forget" ) -} {- -> do (jn,ams1) <- r1 ams0 joinl alsq return ( [], bindAnaEval var jn |+> amsLocalVarMp ams1, slv als , "left join" ) -} -- overlaps with transitivity, fired only when we can conclude var <= bot anyway {- -} ([], (_:_)) | not (null b) -> return ( [], bindAnaEval var a2, [i] , "right bot" ) where (b,_) = partition (\(_,a) -> isBot a) ars ~(i,a2) = head b ((_:_), []) | not (null b) -> return ( [], bindAnaEval var a2, [i] , "left top" ) where (b,_) = partition (\(_,a) -> isTop a) als ~(i,a2) = head b -- top at right is non-information, throw it away (_, (_:_)) | not (null t) -> return ( [], emptyRVarMp, slv t , "right top" ) where (t,_) = partition (\(_,a) -> isTop a) ars -- bot at left is non-information, throw it away ((_:_), _) | not (null b) -> return ( [], emptyRVarMp, slv b , "left bot" ) where (b,_) = partition (\(_,a) -> isBot a) als _ -> Nothing where alsq = map snd als arsq = map snd ars slv a = map fst a ams0 = emptyAnaMatchState {amsBoundS = bound} r0 s act one l = r1 s act (one:l) r1 s act (hd:tl) = foldM (\(x,s') y -> amsRunMb s' $ act x y) (hd,s) tl varIsBound = var `Set.member` bound varIsFree = not varIsBound -- initial qual map qmAddL qs m = (m `Map.union` m', Map.keysSet m') where m' = Map.fromList $ zip [Map.size m ..] qs initQualM = -- (\v -> tr "initQualM" (pp $ show v) v) $ fst $ qmAddL (Set.toList qualS) Map.empty -- bind, with simple occur check bindAnaEval v1 a2@(AnaEval_Var v2) | v1 == v2 = emptyRVarMp bindAnaEval v1 a2 = rvarmpEvalUnit v1 a2 {-# LINE 389 "src/ehc/AnaDomain/Utils.chs" #-} -- | relev ty for tuple/constructor. isJust mbResTy <=> not isInPat relevTyArgsFromCTag :: Bool -> CTag -> Maybe RelevTy -> Int -> DataGam -> UID -> Maybe ([RelevTy],RelevQualS) relevTyArgsFromCTag isInPat ct mbResTy arity dataGam u = case ct of CTagRec -> Just (map fresh $ mkNewLevUIDL arity u, Set.empty) _ -> case dataGamTagLookup ct dataGam of Just (_,dti) -> Just (as, Set.fromList qa) where (as, qa) = relevTyArgs frC constrain u (map ((==Strictness_Strict) . dcfaiStrictness) $ dtiConFldAnnL dti) res (res, frC, constrain) = case mbResTy of Just t -> (t , fr, \(RelevTy_Ana x) (RelevTy_Ana y) -> [RelevQual_SubEval x y]) where fr _ = fresh _ -> (top, fr, \_ _ -> [] ) where fr e | e = freshStrict | otherwise = freshLazy _ -> Nothing {-# LINE 413 "src/ehc/AnaDomain/Utils.chs" #-} relevTyArgs :: (Bool -> UID -> RelevTy) -> (RelevTy -> RelevTy -> [RelevQual]) -> UID -> [Bool] -> RelevTy -> ([RelevTy],[RelevQual]) relevTyArgs fresh constrain u relevForRes res = (as, concat qa) where (as,qa) = unzip $ zipWith mk relevForRes $ mkNewLevUIDL (length relevForRes) u where mk e u | e = (t,constrain t res) | otherwise = (t,[] ) where t = fresh e u