1-- | 2-- Module : Cryptol.TypeCheck.Subst 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE BangPatterns #-} 10{-# LANGUAGE DeriveFunctor #-} 11{-# LANGUAGE DeriveFoldable #-} 12{-# LANGUAGE DeriveTraversable #-} 13{-# LANGUAGE PatternGuards #-} 14{-# LANGUAGE RecordWildCards #-} 15{-# LANGUAGE FlexibleInstances #-} 16{-# LANGUAGE FlexibleContexts #-} 17{-# LANGUAGE Safe #-} 18module Cryptol.TypeCheck.Subst 19 ( Subst 20 , emptySubst 21 , SubstError(..) 22 , singleSubst 23 , singleTParamSubst 24 , uncheckedSingleSubst 25 , (@@) 26 , defaultingSubst 27 , listSubst 28 , listParamSubst 29 , isEmptySubst 30 , FVS(..) 31 , apSubstMaybe 32 , TVars(..) 33 , apSubstTypeMapKeys 34 , substBinds 35 , applySubstToVar 36 , substToList 37 , fmap', (!$), (.$) 38 ) where 39 40import Data.Maybe 41import Data.Either (partitionEithers) 42import qualified Data.Map.Strict as Map 43import qualified Data.IntMap as IntMap 44import Data.Set (Set) 45import qualified Data.Set as Set 46 47import Cryptol.TypeCheck.AST 48import Cryptol.TypeCheck.PP 49import Cryptol.TypeCheck.TypeMap 50import qualified Cryptol.TypeCheck.SimpType as Simp 51import qualified Cryptol.TypeCheck.SimpleSolver as Simp 52import Cryptol.Utils.Panic(panic) 53import Cryptol.Utils.Misc (anyJust, anyJust2) 54 55-- | A 'Subst' value represents a substitution that maps each 'TVar' 56-- to a 'Type'. 57-- 58-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a 59-- type @t@, then @t@ must not mention (directly or indirectly) any 60-- type parameter that is not in @tps@. In particular, if @t@ contains 61-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of 62-- @tps@. This ensures that applying the substitution will not permit 63-- any type parameter to escape from its scope. 64-- 65-- Invariant 2: The substitution must be idempotent, in that applying 66-- a substitution to any 'Type' in the map should leave that 'Type' 67-- unchanged. In other words, 'Type' values in the range of a 'Subst' 68-- should not mention any 'TVar' in the domain of the 'Subst'. In 69-- particular, this implies that a substitution must not contain any 70-- recursive variable mappings. 71-- 72-- Invariant 3: The substitution must be kind correct: Each 'TVar' in 73-- the substitution must map to a 'Type' of the same kind. 74 75data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type)) 76 , suBoundMap :: !(IntMap.IntMap (TVar, Type)) 77 , suDefaulting :: !Bool 78 } 79 deriving Show 80 81emptySubst :: Subst 82emptySubst = 83 S { suFreeMap = IntMap.empty 84 , suBoundMap = IntMap.empty 85 , suDefaulting = False 86 } 87 88-- | Reasons to reject a single-variable substitution. 89data SubstError 90 = SubstRecursive 91 -- ^ 'TVar' maps to a type containing the same variable. 92 | SubstEscaped [TParam] 93 -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables. 94 | SubstKindMismatch Kind Kind 95 -- ^ 'TVar' maps to a type with a different kind. 96 97singleSubst :: TVar -> Type -> Either SubstError Subst 98singleSubst x t 99 | kindOf x /= kindOf t = Left (SubstKindMismatch (kindOf x) (kindOf t)) 100 | x `Set.member` fvs t = Left SubstRecursive 101 | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped)) 102 | otherwise = Right (uncheckedSingleSubst x t) 103 where 104 escaped = 105 case x of 106 TVBound _ -> Set.empty 107 TVFree _ _ scope _ -> freeParams t `Set.difference` scope 108 109uncheckedSingleSubst :: TVar -> Type -> Subst 110uncheckedSingleSubst v@(TVFree i _ _tps _) t = 111 S { suFreeMap = IntMap.singleton i (v, t) 112 , suBoundMap = IntMap.empty 113 , suDefaulting = False 114 } 115uncheckedSingleSubst v@(TVBound tp) t = 116 S { suFreeMap = IntMap.empty 117 , suBoundMap = IntMap.singleton (tpUnique tp) (v, t) 118 , suDefaulting = False 119 } 120 121singleTParamSubst :: TParam -> Type -> Subst 122singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t 123 124(@@) :: Subst -> Subst -> Subst 125s2 @@ s1 126 | isEmptySubst s2 = 127 if suDefaulting s1 || not (suDefaulting s2) then 128 s1 129 else 130 s1{ suDefaulting = True } 131 132s2 @@ s1 = 133 S { suFreeMap = IntMap.map (fmap (apSubst s2)) (suFreeMap s1) `IntMap.union` suFreeMap s2 134 , suBoundMap = IntMap.map (fmap (apSubst s2)) (suBoundMap s1) `IntMap.union` suBoundMap s2 135 , suDefaulting = suDefaulting s1 || suDefaulting s2 136 } 137 138-- | A defaulting substitution maps all otherwise-unmapped free 139-- variables to a kind-appropriate default type (@Bit@ for value types 140-- and @0@ for numeric types). 141defaultingSubst :: Subst -> Subst 142defaultingSubst s = s { suDefaulting = True } 143 144-- | Makes a substitution out of a list. 145-- WARNING: We do not validate the list in any way, so the caller should 146-- ensure that we end up with a valid (e.g., idempotent) substitution. 147listSubst :: [(TVar, Type)] -> Subst 148listSubst xs 149 | null xs = emptySubst 150 | otherwise = S { suFreeMap = IntMap.fromList frees 151 , suBoundMap = IntMap.fromList bounds 152 , suDefaulting = False } 153 where 154 (frees, bounds) = partitionEithers (map classify xs) 155 classify x = 156 case fst x of 157 TVFree i _ _ _ -> Left (i, x) 158 TVBound tp -> Right (tpUnique tp, x) 159 160-- | Makes a substitution out of a list. 161-- WARNING: We do not validate the list in any way, so the caller should 162-- ensure that we end up with a valid (e.g., idempotent) substitution. 163listParamSubst :: [(TParam, Type)] -> Subst 164listParamSubst xs 165 | null xs = emptySubst 166 | otherwise = S { suFreeMap = IntMap.empty 167 , suBoundMap = IntMap.fromList bounds 168 , suDefaulting = False } 169 where 170 bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ] 171 172isEmptySubst :: Subst -> Bool 173isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su) 174 175-- Returns the empty set if this is a defaulting substitution 176substBinds :: Subst -> Set TVar 177substBinds su 178 | suDefaulting su = Set.empty 179 | otherwise = Set.fromList (map fst (assocsSubst su)) 180 181substToList :: Subst -> [(TVar, Type)] 182substToList s 183 | suDefaulting s = panic "substToList" ["Defaulting substitution."] 184 | otherwise = assocsSubst s 185 186assocsSubst :: Subst -> [(TVar, Type)] 187assocsSubst s = frees ++ bounds 188 where 189 frees = IntMap.elems (suFreeMap s) 190 bounds = IntMap.elems (suBoundMap s) 191 192instance PP (WithNames Subst) where 193 ppPrec _ (WithNames s mp) 194 | null els = text "(empty substitution)" 195 | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els)) 196 where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t 197 els = assocsSubst s 198 199instance PP Subst where 200 ppPrec n = ppWithNamesPrec IntMap.empty n 201 202 203 204infixl 0 !$ 205infixl 0 .$ 206 207-- | Left-associative variant of the strict application operator '$!'. 208(!$) :: (a -> b) -> a -> b 209(!$) = ($!) 210 211-- | Left-associative variant of the application operator '$'. 212(.$) :: (a -> b) -> a -> b 213(.$) = ($) 214 215-- Only used internally to define fmap'. 216data Done a = Done a 217 deriving (Functor, Foldable, Traversable) 218 219instance Applicative Done where 220 pure x = Done x 221 Done f <*> Done x = Done (f x) 222 223-- | Strict variant of 'fmap'. 224fmap' :: Traversable t => (a -> b) -> t a -> t b 225fmap' f xs = case traverse f' xs of Done y -> y 226 where f' x = Done $! f x 227 228-- | Apply a substitution. Returns `Nothing` if nothing changed. 229apSubstMaybe :: Subst -> Type -> Maybe Type 230apSubstMaybe su ty = 231 case ty of 232 TCon t ts -> 233 do ss <- anyJust (apSubstMaybe su) ts 234 case t of 235 TF _ -> Just $! Simp.tCon t ss 236 PC _ -> Just $! Simp.simplify mempty (TCon t ss) 237 _ -> Just (TCon t ss) 238 239 TUser f ts t -> 240 do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe su)) (apSubstMaybe su) (ts, t) 241 Just (TUser f ts1 t1) 242 243 TRec fs -> TRec `fmap` (anyJust (apSubstMaybe su) fs) 244 TNewtype nt ts -> TNewtype nt `fmap` anyJust (apSubstMaybe su) ts 245 TVar x -> applySubstToVar su x 246 247lookupSubst :: TVar -> Subst -> Maybe Type 248lookupSubst x su = 249 fmap snd $ 250 case x of 251 TVFree i _ _ _ -> IntMap.lookup i (suFreeMap su) 252 TVBound tp -> IntMap.lookup (tpUnique tp) (suBoundMap su) 253 254applySubstToVar :: Subst -> TVar -> Maybe Type 255applySubstToVar su x = 256 case lookupSubst x su of 257 -- For a defaulting substitution, we must recurse in order to 258 -- replace unmapped free vars with default types. 259 Just t 260 | suDefaulting su -> Just $! apSubst su t 261 | otherwise -> Just t 262 Nothing 263 | suDefaulting su -> Just $! defaultFreeVar x 264 | otherwise -> Nothing 265 266class TVars t where 267 apSubst :: Subst -> t -> t 268 -- ^ Replaces free variables. To prevent space leaks when used with 269 -- large 'Subst' values, every instance of 'apSubst' should satisfy 270 -- a strictness property: Forcing evaluation of @'apSubst' s x@ 271 -- should also force the evaluation of all recursive calls to 272 -- @'apSubst' s@. This ensures that unevaluated thunks will not 273 -- cause 'Subst' values to be retained on the heap. 274 275instance TVars t => TVars (Maybe t) where 276 apSubst s = fmap' (apSubst s) 277 278instance TVars t => TVars [t] where 279 apSubst s = fmap' (apSubst s) 280 281instance (TVars s, TVars t) => TVars (s,t) where 282 apSubst s (x, y) = (,) !$ apSubst s x !$ apSubst s y 283 284instance TVars Type where 285 apSubst su ty = fromMaybe ty (apSubstMaybe su ty) 286 287-- | Pick types for unconstrained unification variables. 288defaultFreeVar :: TVar -> Type 289defaultFreeVar x@(TVBound {}) = TVar x 290defaultFreeVar (TVFree _ k _ d) = 291 case k of 292 KType -> tBit 293 KNum -> tNum (0 :: Int) 294 _ -> panic "Cryptol.TypeCheck.Subst.defaultFreeVar" 295 [ "Free variable of unexpected kind." 296 , "Source: " ++ show d 297 , "Kind: " ++ show (pp k) ] 298 299instance (Traversable m, TVars a) => TVars (List m a) where 300 apSubst su = fmap' (apSubst su) 301 302instance TVars a => TVars (TypeMap a) where 303 apSubst su = fmap' (apSubst su) 304 305 306-- | Apply the substitution to the keys of a type map. 307apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a 308apSubstTypeMapKeys su = go (\_ x -> x) id 309 where 310 311 go :: (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a 312 go merge atNode TM { .. } = foldl addKey tm' tys 313 where 314 addKey tm (ty,a) = insertWithTM merge ty a tm 315 316 tm' = TM { tvar = Map.fromList vars 317 , tcon = fmap (lgo merge atNode) tcon 318 , trec = fmap (lgo merge atNode) trec 319 , tnewtype = fmap (lgo merge atNode) tnewtype 320 } 321 322 -- partition out variables that have been replaced with more specific types 323 (vars,tys) = partitionEithers 324 [ case applySubstToVar su v of 325 Just ty -> Right (ty,a') 326 Nothing -> Left (v, a') 327 328 | (v,a) <- Map.toList tvar 329 , let a' = atNode a 330 ] 331 332 lgo :: (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a 333 lgo merge atNode k = k { nil = fmap atNode (nil k) 334 , cons = go (unionTM merge) 335 (lgo merge atNode) 336 (cons k) 337 } 338 339 340{- | This instance does not need to worry about bound variable 341capture, because we rely on the 'Subst' datatype invariant to ensure 342that variable scopes will be properly preserved. -} 343 344instance TVars Schema where 345 apSubst su (Forall xs ps t) = 346 Forall xs !$ (concatMap pSplitAnd (apSubst su ps)) !$ (apSubst su t) 347 348instance TVars Expr where 349 apSubst su = go 350 where 351 go expr = 352 case expr of 353 ELocated r e -> ELocated r !$ (go e) 354 EApp e1 e2 -> EApp !$ (go e1) !$ (go e2) 355 EAbs x t e1 -> EAbs x !$ (apSubst su t) !$ (go e1) 356 ETAbs a e -> ETAbs a !$ (go e) 357 ETApp e t -> ETApp !$ (go e) !$ (apSubst su t) 358 EProofAbs p e -> EProofAbs !$ hmm !$ (go e) 359 where hmm = case pSplitAnd (apSubst su p) of 360 [p1] -> p1 361 res -> panic "apSubst@EProofAbs" 362 [ "Predicate split or disappeared after" 363 , "we applied a substitution." 364 , "Predicate:" 365 , show (pp p) 366 , "Became:" 367 , show (map pp res) 368 , "subst:" 369 , show (pp su) 370 ] 371 372 EProofApp e -> EProofApp !$ (go e) 373 374 EVar {} -> expr 375 376 ETuple es -> ETuple !$ (fmap' go es) 377 ERec fs -> ERec !$ (fmap' go fs) 378 ESet ty e x v -> ESet !$ (apSubst su ty) !$ (go e) .$ x !$ (go v) 379 EList es t -> EList !$ (fmap' go es) !$ (apSubst su t) 380 ESel e s -> ESel !$ (go e) .$ s 381 EComp len t e mss -> EComp !$ (apSubst su len) !$ (apSubst su t) !$ (go e) !$ (apSubst su mss) 382 EIf e1 e2 e3 -> EIf !$ (go e1) !$ (go e2) !$ (go e3) 383 384 EWhere e ds -> EWhere !$ (go e) !$ (apSubst su ds) 385 386instance TVars Match where 387 apSubst su (From x len t e) = From x !$ (apSubst su len) !$ (apSubst su t) !$ (apSubst su e) 388 apSubst su (Let b) = Let !$ (apSubst su b) 389 390instance TVars DeclGroup where 391 apSubst su (NonRecursive d) = NonRecursive !$ (apSubst su d) 392 apSubst su (Recursive ds) = Recursive !$ (apSubst su ds) 393 394instance TVars Decl where 395 apSubst su d = 396 let !sig' = id $! apSubst su (dSignature d) 397 !def' = apSubst su (dDefinition d) 398 in d { dSignature = sig', dDefinition = def' } 399 400instance TVars DeclDef where 401 apSubst su (DExpr e) = DExpr !$ (apSubst su e) 402 apSubst _ DPrim = DPrim 403 404instance TVars Module where 405 apSubst su m = 406 let !decls' = apSubst su (mDecls m) 407 in m { mDecls = decls' } 408