Merge branch 'master' into wip/cs

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

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)

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

tests/issues/issue225.icry.stdout

@@ -1,5 +1,3 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module EnigmaBroke
-Loading module Cryptol
-Loading module EnigmaBroke