diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index 369ba1f5..3a1db7e1 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -116,6 +116,11 @@ instance TrieMap RewMap' (QName,[Type],Int) where , (ts,pM) <- toListTM tM , (n,y) <- toListTM pM ] + mapMaybeWithKeyTM f (RM m) = + RM (mapWithKeyTM (\qn tm -> + mapWithKeyTM (\tys is -> + mapMaybeWithKeyTM (\i a -> f (qn,tys,i) a) is) tm) m) + -- | Note that this assumes that this pass will be run only once for each -- module, otherwise we will get name collisions. rewModule :: Module -> Module diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index d0e83d49..0bee427b 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -271,7 +271,15 @@ instance FVS DelayedCt where -- values that remain, as applying the substitution to the keys will only ever -- reduce the number of values that remain. instance TVars Goals where - apSubst su (Goals goals) = Goals (apSubst su (apSubstTypeMapKeys su goals)) + apSubst su (Goals goals) = + Goals (mapWithKeyTM setGoal (apSubstTypeMapKeys su goals)) + where + -- as the key for the goal map is the same as the goal, and the substitution + -- has been applied to the key already, just replace the existing goal with + -- the key. + setGoal key g = g { goalSource = apSubst su (goalSource g) + , goal = key + } instance TVars Goal where apSubst su g = Goal { goalSource = apSubst su (goalSource g) diff --git a/src/Cryptol/TypeCheck/TypeMap.hs b/src/Cryptol/TypeCheck/TypeMap.hs index a58036c0..b2ea1414 100644 --- a/src/Cryptol/TypeCheck/TypeMap.hs +++ b/src/Cryptol/TypeCheck/TypeMap.hs @@ -14,6 +14,7 @@ module Cryptol.TypeCheck.TypeMap ( TypeMap(..), TypesMap, TrieMap(..) , insertTM, insertWithTM , membersTM + , mapTM, mapWithKeyTM, mapMaybeTM , List(..) ) where @@ -36,6 +37,8 @@ class TrieMap m k | m -> k where unionTM :: (a -> a -> a) -> m a -> m a -> m a toListTM :: m a -> [(k,a)] + mapMaybeWithKeyTM :: (k -> a -> Maybe b) -> m a -> m b + membersTM :: TrieMap m k => m a -> [a] membersTM = map snd . toListTM @@ -47,6 +50,18 @@ insertWithTM f t new = alterTM t $ \mb -> Just $ case mb of Nothing -> new Just old -> f old new +{-# INLINE mapTM #-} +mapTM :: TrieMap m k => (a -> b) -> m a -> m b +mapTM f = mapMaybeWithKeyTM (\ _ a -> Just (f a)) + +{-# INLINE mapWithKeyTM #-} +mapWithKeyTM :: TrieMap m k => (k -> a -> b) -> m a -> m b +mapWithKeyTM f = mapMaybeWithKeyTM (\ k a -> Just (f k a)) + +{-# INLINE mapMaybeTM #-} +mapMaybeTM :: TrieMap m k => (a -> Maybe b) -> m a -> m b +mapMaybeTM f = mapMaybeWithKeyTM (\_ -> f) + data List m a = L { nil :: Maybe a , cons :: m (List m a) } deriving (Functor) @@ -78,6 +93,12 @@ instance TrieMap m a => TrieMap (List m) [a] where , cons = unionTM (unionTM f) (cons m1) (cons m2) } + mapMaybeWithKeyTM f = go [] + where + go acc l = L { nil = f (reverse acc) =<< nil l + , cons = mapMaybeWithKeyTM (\k a -> Just (go (k:acc) a)) (cons l) + } + instance Ord a => TrieMap (Map a) a where emptyTM = Map.empty @@ -87,6 +108,8 @@ instance Ord a => TrieMap (Map a) a where toListTM = Map.toList unionTM = Map.unionWith + mapMaybeWithKeyTM = Map.mapMaybeWithKey + type TypesMap = List TypeMap @@ -130,6 +153,14 @@ instance TrieMap TypeMap Type where , trec = unionTM (unionTM f) (trec m1) (trec m2) } + mapMaybeWithKeyTM f m = + TM { tvar = mapMaybeWithKeyTM (\v -> f (TVar v)) (tvar m) + , tcon = mapWithKeyTM (\c l -> mapMaybeWithKeyTM + (\ts a -> f (TCon c ts) a) l) (tcon m) + , trec = mapWithKeyTM (\fs l -> mapMaybeWithKeyTM + (\ts a -> f (TRec (zip fs ts)) a) l) (trec m) + } + updSub :: TrieMap m k => k -> (Maybe a -> Maybe a) -> Maybe (m a) -> Maybe (m a) updSub k f = Just . alterTM k f . fromMaybe emptyTM diff --git a/tests/issues/issue225.icry.stdout b/tests/issues/issue225.icry.stdout index 2d4e2d9c..49f9c178 100644 --- a/tests/issues/issue225.icry.stdout +++ b/tests/issues/issue225.icry.stdout @@ -1,5 +1,3 @@ Loading module Cryptol Loading module Cryptol Loading module EnigmaBroke -Loading module Cryptol -Loading module EnigmaBroke