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