2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
4 \section[Subst]{Substitutions}
7 #include "HsVersions.h"
10 Subst, SubstResult(..), -- Subst is an abstract data type
12 mkEmptySubst, extendSubst,
14 --not exported: applySubstToTauTy,
16 applySubstToThetaTy, applySubstToTyVar,
18 getSubstTyVarUniques, getSubstTyVarUnique,
20 pushSubstUndos, combineSubstUndos, undoSubstUndos,
23 -- and to make the interface self-sufficient...
27 import AbsUniType -- lots of stuff, plus...
28 import UniType -- UniType(..) -- *********** YOW!!! ********
29 import Bag ( emptyBag, unionBags, snocBag,
30 bagToList, filterBag, unitBag, Bag )
31 import Maybes ( Maybe(..), maybeToBool )
37 %************************************************************************
39 \subsection[Subst-magic-importst]{Funny imports to support magic implementation}
41 %************************************************************************
45 If we are compiling with Glasgow Haskell we can use mutable
46 arrays to implement the substitution ...
49 #ifndef __GLASGOW_HASKELL__
53 #else {- __GLASGOW_HASKELL__ -}
57 type STWorld = _State _RealWorld
59 newWorld (S# real_world) = S# real_world
61 #endif {- __GLASGOW_HASKELL__ -}
64 %************************************************************************
66 \subsection[Subst-common]{@Subst@: common implementation-independent bits}
68 %************************************************************************
75 | AlreadyBound TauType -- The variable is already bound
76 -- to this type. The type is *not*
77 -- necessarily a fixed pt of the
81 Common signatures of major functions.
84 mkEmptySubst :: Int -> Subst
89 @extendSubst@: Add a single binding to the substitution. We have to:
92 apply the existing bindings to the new one;
94 check whether we are adding a trivial substitution of a type
95 variable to itself (if so, do nothing);
97 perform an occurs check on the right-hand side of the new binding;
99 We do not apply the new binding to all the existing ones. This is
100 delayed until the substitution is applied.
102 extendSubst :: TyVar -- Tyvar to bind
103 -> TauType -- Type to bind it to; NB can be a synonym
104 -> SubstM SubstResult
109 Apply a substitution to a given type.
111 {\em The type returned is guaranteed to be
112 a fixed point of the substitution.}
114 Hence, we have to traverse the type determining the type mapped to
115 tyvars. The type mapped must be recusively traversed as the substition
116 is not stored idempotently.
118 @applySubstToTauTy@ does not expect to meet a dict or forall type.
119 @applySubstToTy@ may encounter these, but complains if the forall
120 binds a variable which is in the domain of the substitution.
123 applySubstToTy :: Subst -> UniType -> (Subst, UniType)
124 applySubstToTauTy :: Subst -> TauType -> (Subst, TauType)
125 applySubstToThetaTy :: Subst -> ThetaType -> (Subst, ThetaType)
126 applySubstToTyVar :: Subst -> TyVar -> (Subst, TauType)
129 These functions are only used by the type checker. We know that
130 all the for-all'd type variables are fixed points of the substitution,
131 so it's quite safe just to apply the substitution inside foralls.
137 getSubstTyVarUnique :: Subst -> (Subst, Unique)
138 getSubstTyVarUniques :: Int -> Subst -> (Subst, [Unique])
143 @pushSubstUndos@ starts a new subst undo scope, saving the old scopes.
144 It also saves the current unique supply so that it can be restored if
147 @combineSubstUndos@ is called after a successful typecheck. It
148 combines the current undos with the previos ones in case we fail in an
149 outer scope. If no previous undos exist the undos are thrown away as
150 we must have succeeded at the top level. The unique supply of the
151 successful scope is returned to the unique supply of the current
154 @undoSubstUndos@ is called when a typecheck failed. The any
155 substitution modifications are undone and the undo information
156 discarded. The saved unique supply of the enclosing scope is restored.
158 pushSubstUndos, combineSubstUndos, undoSubstUndos :: Subst -> Subst
161 %************************************************************************
163 \subsection[Subst-Arrays]{@Subst@ with mutable @Arrays@ !!!}
165 %************************************************************************
169 #ifdef __GLASGOW_HASKELL__
172 %************************************************************************
174 \subsubsection{@Subst@: specification and representation}
176 %************************************************************************
179 * When new bindings are added to the substitution, an occurs check is performed.
180 * The applySubst function guarantees to return a fixed point of the substitution.
182 {\em Representation:}
183 A substitution binds type variables to tau-types, that is @UniType@s without
184 any @UniForall@ or @UniDict@ constructors.
186 It is represented as an array, indexed on Int, with a world
187 token, and a stack of type variables whos subst may be undone. The
188 array is extended (by copying) if it overflows. The supply of
189 Ints and the size of the array are linked so the substitution
190 is also responsible for allocating the supply of uniques.
192 The undo information is a stack of bags of the nested modifications to
193 the substitution. If the typecheck fails the modifications to the
194 substition are undone. If it succeeds the current undos are combined
195 with the undos in the enclosing scope so that they would be undone if
196 the enclsing scope typecheck fails.
198 The unique supply is also stacked so that it can be restored if a
201 NOTE: The uniqueness of the world token, and hence the substitution,
202 is critical as the 'worldSEQ' operation is unsafe if the token can be
206 type SubstArray = _MutableArray _RealWorld Int (Maybe TauType)
208 type SubstArrayIndex = Int -- Allocated within this module, single-threadedly
211 = MkSubst SubstArray -- Mapping for allocated tyvars
213 [(SubstArrayIndex, Bag (SubstArrayIndex, Maybe TauType))]
214 -- Stack to be undone if we fail, plus next free
215 -- slot when reverting. All the undos are for
216 -- slots earlier than the corresp "next free" index.
218 -- The "bag" is a lie: it's really a sequence, with
219 -- the most recently performed write appearing first.
221 STWorld -- State token
223 SubstArrayIndex -- Next free slot
226 Here's a local monad for threading the substitution around:
229 type SubstM a = Subst -> (Subst,a)
231 returnSubstM x = \s -> (s,x)
232 thenSubstM m k = \s -> case m s of { (s1, r) -> k r s1 }
234 mapSubstM f [] = returnSubstM []
235 mapSubstM f (x:xs) = f x `thenSubstM` \ r ->
236 mapSubstM f xs `thenSubstM` \ rs ->
239 -- Breaks the ST abstraction. But we have to do so somewhere...
240 doST :: STWorld -> ST _RealWorld a -> (a, STWorld)
244 %********************************************************
246 \subsubsection{@Subst@: the array}
248 %********************************************************
251 writeSubst :: SubstArrayIndex -> Maybe TauType -> SubstM ()
252 -- writeSubst writes in such a way that we can undo it later
254 writeSubst index new_val
255 (MkSubst arr undo_stack@((checkpoint, undos):rest_undo_stack)
257 | index < checkpoint -- Record in undos
259 (old, new_world) = doST world (
260 readArray arr index `thenStrictlyST` \ old_val ->
261 writeArray arr index new_val `seqStrictlyST`
262 returnStrictlyST old_val
264 new_undos = unitBag (index,old) `unionBags` undos
265 -- The order is significant! The right most thing
268 (MkSubst arr ((checkpoint, new_undos) : rest_undo_stack) new_world next_free, ())
270 writeSubst index new_val (MkSubst arr undo_stack world next_free)
271 -- No need to record in undos: undo_stack is empty,
272 -- or index is after checkpoint
274 (_, new_world) = doST world (writeArray arr index new_val)
276 (MkSubst arr undo_stack new_world next_free, ())
278 readSubst :: SubstArrayIndex -> SubstM (Maybe TauType)
279 readSubst index (MkSubst arr undos world supplies)
281 (result, new_world) = doST world (readArray arr index)
283 (MkSubst arr undos new_world supplies, result)
285 tyVarToIndex :: TyVar -> SubstArrayIndex
286 tyVarToIndex tyvar = unpkUnifiableTyVarUnique (getTheUnique tyvar)
289 %********************************************************
291 \subsubsection{@Subst@: building them}
293 %********************************************************
295 The function @mkEmptySubst@ used to be a CAF containing a mutable
296 array. The imperative world had a name for this kind of thing:
297 ``global variable'' and has observed that using these ``global variables''
298 leads to something they call ``side effects''.
300 These ``side effects'' never caused a problem for @hsc@ because empty
301 substitutions are only used in one place (the typechecker) and only
302 used once in every program run. In \tr{ghci} however, we might use the
303 typechecker several times---in which case we'd like to have a
304 different (fresh) substitution each time. The easy way (HACK) to
305 achieve this is to deCAFinate so that a fresh substitution will be
306 created each time the typechecker runs.
312 mkEmptySubst aRRAY_SIZE
314 world = newWorld (S# realWorld#)
315 (arr, new_world) = doST world (newArray (aRRAY_START,aRRAY_SIZE) Nothing)
317 MkSubst arr [] new_world aRRAY_START
319 extendSubstArr :: Subst
321 extendSubstArr (MkSubst old_arr undos world next_free)
323 -- these "sizes" are really end-limits (WDP 94/11)
324 cur_size = case (boundsOfArray old_arr) of { (_, x) -> x }
325 new_size = (cur_size * 2) + 1
327 (new_arr, new_world) = doST world (
328 newArray (aRRAY_START,new_size) Nothing `thenStrictlyST` \ new_arr ->
331 | pos > cur_size = returnStrictlyST ()
333 = readArray old_arr pos `thenStrictlyST` \ ele ->
334 writeArray new_arr pos ele `seqStrictlyST`
337 copyArr aRRAY_START `seqStrictlyST`
338 returnStrictlyST new_arr
341 MkSubst new_arr undos new_world next_free
345 extendSubst tyvar tau_ty
346 = readSubst index `thenSubstM` \ maybe_ty ->
349 Just exist_ty -> -- Bound already
350 returnSubstM (AlreadyBound exist_ty)
352 Nothing -> -- Not already bound
353 apply_rep_to_ty tau_ty `thenSubstM` \ new_tau_ty ->
354 case expandVisibleTySyn new_tau_ty of
355 UniTyVar tv | tv `eqTyVar` tyvar ->
356 -- Trivial new binding of a type variable to itself;
357 -- return old substition
360 other | tyvar `is_elem` (extractTyVarsFromTy new_tau_ty) ->
361 -- Occurs check finds error
362 returnSubstM (OccursCheck tyvar new_tau_ty)
366 writeSubst index (Just new_tau_ty) `thenSubstM` \ _ ->
369 index = tyVarToIndex tyvar
370 is_elem = isIn "extendSubst"
373 %********************************************************
375 \subsubsection{@Subst@: lookup}
377 %********************************************************
379 All of them use the underlying function, @apply_rep_to_ty@, which
380 ensures that an idempotent result is returned.
383 applySubstToTy subst ty = apply_rep_to_ty ty subst
384 applySubstToTauTy subst tau_ty = apply_rep_to_ty tau_ty subst
385 applySubstToTyVar subst tyvar = apply_rep_to_ty (mkTyVarTy tyvar) subst
386 applySubstToThetaTy subst theta_ty
388 do_one (clas, ty) = apply_rep_to_ty ty `thenSubstM` \ new_ty ->
389 returnSubstM (clas, new_ty)
391 mapSubstM do_one theta_ty subst
394 And now down to serious business...
396 apply_rep_to_ty :: UniType -> SubstM UniType
398 apply_rep_to_ty (UniTyVar tyvar)
399 = readSubst index `thenSubstM` \ maybe_ty ->
402 Nothing -> -- Not found, so return a trivial type
403 returnSubstM (mkTyVarTy tyvar)
405 Just ty -> -- Found, so recursively apply the subst the result to
406 -- maintain idempotence!
407 apply_rep_to_ty ty `thenSubstM` \ new_ty ->
409 -- The mapping for this tyvar is then updated with the
410 -- result to reduce the number of subsequent lookups
411 writeSubst index (Just new_ty) `thenSubstM` \ _ ->
415 index = tyVarToIndex tyvar
417 apply_rep_to_ty (UniFun t1 t2)
418 = apply_rep_to_ty t1 `thenSubstM` \ new_t1 ->
419 apply_rep_to_ty t2 `thenSubstM` \ new_t2 ->
420 returnSubstM (UniFun new_t1 new_t2)
422 apply_rep_to_ty (UniData con args)
423 = mapSubstM apply_rep_to_ty args `thenSubstM` \ new_args ->
424 returnSubstM (UniData con new_args)
426 apply_rep_to_ty (UniSyn con args ty)
427 = mapSubstM apply_rep_to_ty args `thenSubstM` \ new_args ->
428 apply_rep_to_ty ty `thenSubstM` \ new_ty ->
429 returnSubstM (UniSyn con new_args new_ty)
431 apply_rep_to_ty (UniDict clas ty)
432 = apply_rep_to_ty ty `thenSubstM` \ new_ty ->
433 returnSubstM (UniDict clas new_ty)
435 apply_rep_to_ty (UniForall v ty)
436 = apply_rep_to_ty ty `thenSubstM` \ new_ty ->
437 returnSubstM (UniForall v new_ty)
439 apply_rep_to_ty ty@(UniTyVarTemplate v) = returnSubstM ty
442 %************************************************************************
444 \subsubsection{Allocating @TyVarUniques@}
446 %************************************************************************
448 The array is extended if the allocated type variables would cause an
452 getSubstTyVarUnique subst@(MkSubst arr undo world next_free)
453 | next_free <= size -- The common case; there's a spare slot
454 = (MkSubst arr undo world new_next_free, uniq)
456 | otherwise -- Need more room: Extend first, then re-try
457 = getSubstTyVarUnique (extendSubstArr subst)
460 size = case (boundsOfArray arr) of { (_, x) -> x }
461 uniq = mkUnifiableTyVarUnique next_free
462 new_next_free = next_free + 1
465 getSubstTyVarUniques n subst@(MkSubst arr undo world next_free)
466 | new_next_free - 1 <= size -- The common case; there's a spare slot
467 = (MkSubst arr undo world new_next_free, uniqs)
469 | otherwise -- Need more room: extend, then re-try
470 = getSubstTyVarUniques n (extendSubstArr subst)
473 size = case (boundsOfArray arr) of { (_, x) -> x }
474 uniqs = [mkUnifiableTyVarUnique (next_free + i) | i <- [0..n-1]]
475 new_next_free = next_free + n
478 %************************************************************************
480 \subsubsection{Undoing substitution on typechecking failure}
482 %************************************************************************
485 pushSubstUndos (MkSubst arr undos world next_free)
486 = MkSubst arr ((next_free,emptyBag):undos) world next_free
488 combineSubstUndos (MkSubst arr [_] world next_free)
489 = MkSubst arr [] world next_free -- top level undo ignored
491 combineSubstUndos (MkSubst arr ((_,u1):(checkpoint,u2):undo_stack)
493 = MkSubst arr ((checkpoint, new_u1 `unionBags` u2):undo_stack) world next_free
495 -- Keep only undos which apply to indices before checkpoint
496 new_u1 = filterBag (\ (index,val) -> index < checkpoint) u1
498 undoSubstUndos (MkSubst arr ((checkpoint,undo_now):undo_stack) world next_free)
499 = MkSubst arr undo_stack new_world checkpoint
501 (_, new_world) = doST world (perform_undo (bagToList undo_now) `seqStrictlyST`
502 clear_block checkpoint
505 perform_undo [] = returnStrictlyST ()
506 perform_undo ((index,val):undos) = writeArray arr index val `seqStrictlyST`
509 -- (clear_block n) clears the array from n up to next_free
510 -- This is necessary because undos beyond supp2 aren't recorded in undos
511 clear_block n | n >= next_free = returnStrictlyST ()
512 | otherwise = writeArray arr n Nothing `seqStrictlyST`
516 %************************************************************************
518 \subsubsection{Pruning a substitution}
520 %************************************************************************
522 ToDo: Implement with array !! Ignore? Restore unique supply?
524 @pruneSubst@ prunes a substitution to a given level.
526 This is tricky stuff. The idea is that if we
527 (a) catch the current unique supply
529 (c) back-substitute over the results of the work
530 (d) prune the substitution back to the level caught in (a)
531 then everything will be fine. Any *subsequent* unifications to
532 these just-pruned ones will be added and not subsequently deleted.
534 NB: this code relies on the idempotence property, otherwise discarding
535 substitions might be dangerous.
539 pruneSubst :: TyVarUnique -> Subst -> Subst
541 pruneSubst keep_marker (MkSubst subst_rep)
542 = -- BSCC("pruneSubst")
543 MkSubst [(tyvar,ty) | (tyvar,ty) <- subst_rep,
544 getTheUnique tyvar `ltUnique` keep_marker]
549 %************************************************************************
551 \subsection[Subst-Lists]{@Subst@ with poor list implementation}
553 %************************************************************************
555 If don't have Glasgow Haskell we have to revert to list implementation
559 #else {- ! __GLASGOW_HASKELL__ -}
562 %************************************************************************
564 \subsubsection{@Subst@: specification and representation}
566 %************************************************************************
569 * When new bindings are added to the substitution, an occurs check is performed.
570 * The applySubst function guarantees to return a fixed point of the substitution.
572 {\em Representation:}
573 A substitution binds type variables to tau-types, that is @UniType@s without
574 any @UniForall@ or @UniDict@ constructors.
576 It is represented as an association list, indexed on Uniques
577 with a stack of type variable unique markers indicating undo
578 checkpoints. The supply of TyVarUniques is also part of the
581 The undo information is a stack of tyvar markers. If the typecheck
582 fails all extensions to the association list subsequent to (and
583 including) the marker are undone. If it succeeds the current marker is
586 The unique supply is also stacked so that it can be restored if a
590 type SubstRep = [(Unique, TauType)]
593 = MkSubst SubstRep -- mapping for allocated tyvars
594 [Maybe Unique] -- stack of markers to strip off if we fail
595 [UniqueSupply] -- stack of tyvar unique supplies
597 mkEmptySubst size = MkSubst [] [] []
601 lookup_rep :: SubstRep -> TyVar -> Maybe TauType
602 lookup_rep alist tyvar
604 key = getTheUnique tyvar
608 = case (cmpUnique key u) of { EQ_ -> Just ty; _ -> lookup rest }
613 %********************************************************
615 \subsubsection{@Subst@: building them}
617 %********************************************************
620 --OLD? initSubst init = MkSubst [] [] [mkUniqueSupply init]
624 extendSubst subst@(MkSubst srep undo supp) tyvar tau_ty
625 = -- BSCC("extendSubst")
626 apply_rep_to_ty srep tau_ty `thenLft` \ new_tau_ty ->
628 case expandVisibleTySyn new_tau_ty of
630 UniTyVar tv | tv `eqTyVar` tyvar ->
631 -- Trivial new binding; return old substition
635 is_elem = isIn "extendSubst2"
637 if (tyvar `is_elem` (extractTyVarsFromTy new_tau_ty)) then
638 (OccursCheck tyvar new_tau_ty, subst)
640 case lookup_rep srep tyvar of
642 (AlreadyBound exist_ty, subst)
645 new_srep = (getTheUnique tyvar, new_tau_ty) : srep
646 new_undo = case undo of
648 -- top level undo ignored
650 (Nothing : undos) -> (Just (getTheUnique tyvar)) : undos
651 (Just _ : _ ) -> undo
652 -- only first undo recorded
654 (SubstOK, MkSubst new_srep new_undo supp)
658 %********************************************************
660 \subsubsection{@Subst@: lookup}
662 %********************************************************
664 All of them use the underlying function, @apply_rep_to_ty@, which
665 ensures that an idempotent result is returned.
668 applySubstToTy subst@(MkSubst srep undo supp) ty
669 = -- BSCC("applySubstToTy")
670 apply_rep_to_ty srep ty `thenLft` \ new_ty ->
674 applySubstToTauTy subst@(MkSubst srep undo supp) tauty
675 = -- BSCC("applySubstToTauTy")
676 apply_rep_to_ty srep tauty `thenLft`\ new_tauty ->
680 applySubstToThetaTy subst@(MkSubst srep undo supp) theta
681 = -- BSCC("applySubstToThetaTy")
683 do_one (clas, ty) = apply_rep_to_ty srep ty `thenLft` \ new_ty ->
684 returnLft (clas, new_ty)
686 mapLft do_one theta `thenLft` \ new_theta ->
690 applySubstToTyVar subst@(MkSubst srep undo supp) tyvar
691 = -- BSCC("applySubstToTyVar")
692 apply_rep_to_ty srep (mkTyVarTy tyvar) `thenLft` \ new_tauty ->
697 And now down to serious business...
699 apply_rep_to_ty :: SubstRep -> UniType -> LiftM UniType
701 apply_rep_to_ty srep (UniTyVar tyvar)
702 = case lookup_rep srep tyvar of
703 Nothing -> -- Not found, so return a trivial type
704 returnLft (mkTyVarTy tyvar)
706 Just ty -> -- Found, so recursively apply the subst the result to
707 -- maintain idempotence!
708 apply_rep_to_ty srep ty
710 apply_rep_to_ty srep (UniFun t1 t2)
711 = apply_rep_to_ty srep t1 `thenLft` \ new_t1 ->
712 apply_rep_to_ty srep t2 `thenLft` \ new_t2 ->
713 returnLft (UniFun new_t1 new_t2)
715 apply_rep_to_ty srep (UniData con args)
716 = mapLft (apply_rep_to_ty srep) args `thenLft` \ new_args ->
717 returnLft (UniData con new_args)
719 apply_rep_to_ty srep (UniSyn con args ty)
720 = mapLft (apply_rep_to_ty srep) args `thenLft` \ new_args ->
721 apply_rep_to_ty srep ty `thenLft` \ new_ty ->
722 returnLft (UniSyn con new_args new_ty)
724 apply_rep_to_ty srep (UniDict clas ty)
725 = apply_rep_to_ty srep ty `thenLft` \ new_ty ->
726 returnLft (UniDict clas new_ty)
728 apply_rep_to_ty srep (UniForall v ty)
729 = apply_rep_to_ty srep ty `thenLft` \ new_ty ->
730 returnLft (UniForall v new_ty)
732 apply_rep_to_ty srep ty@(UniTyVarTemplate v) = returnLft ty
735 %************************************************************************
737 \subsubsection{Allocating TyVarUniques}
739 %************************************************************************
741 The array is extended if the allocated type variables would cause an
745 getSubstTyVarUnique subst@(MkSubst srep undo (supp:supps))
746 = -- BSCC("allocTyVarUniques")
747 case getUnique supp of
748 (new_supp, uniq) -> (MkSubst srep undo (new_supp:supps), uniq)
751 getSubstTyVarUniques n subst@(MkSubst srep undo (supp:supps))
752 = -- BSCC("allocTyVarUniques")
753 case getUniques n supp of
754 (new_supp, uniqs) -> (MkSubst srep undo (new_supp:supps), uniqs)
758 %************************************************************************
760 \subsubsection[Subst-undo]{Undoing substitution on typechecking failure}
762 %************************************************************************
765 pushSubstUndos subst@(MkSubst srep undos (supp:supps))
766 = -- BSCC("pushSubstUndos")
767 MkSubst srep (Nothing:undos) (supp:supp:supps)
770 combineSubstUndos subst@(MkSubst srep (u:us) (supp1:supp2:supps))
771 = -- BSCC("combineSubstUndos")
772 MkSubst srep us (supp1:supps)
775 undoSubstUndos subst@(MkSubst srep (u:us) (supp1:supp2:supps))
776 = -- BSCC("undoSubstUndos")
779 strip_to ((u,ty):srep) key
780 = case (cmpUnique u key) of { EQ_ -> srep; _ -> strip_to srep key }
782 perform_undo Nothing srep = srep
783 perform_undo (Just uniq) srep = strip_to srep uniq
785 MkSubst (perform_undo u srep) us (supp2:supps)
787 -- Note: the saved unique supply is restored from the enclosing scope
792 %************************************************************************
794 \subsubsection{Pruning a substitution}
796 %************************************************************************
798 ToDo: Implement with list !! Ignore? Restore unique supply?
800 @pruneSubst@ prunes a substitution to a given level.
802 This is tricky stuff. The idea is that if we
803 (a) catch the current unique supply
805 (c) back-substitute over the results of the work
806 (d) prune the substitution back to the level caught in (a)
807 then everything will be fine. Any *subsequent* unifications to
808 these just-pruned ones will be added and not subsequently deleted.
810 NB: this code relies on the idempotence property, otherwise discarding
811 substitions might be dangerous.
815 pruneSubst :: TyVarUnique -> Subst -> Subst
817 pruneSubst keep_marker (MkSubst subst_rep)
818 = -- BSCC("pruneSubst")
819 MkSubst [(tyvar,ty) | (tyvar,ty) <- subst_rep,
820 getTheUnique tyvar `ltUnique` keep_marker]
826 #endif {- ! __GLASGOW_HASKELL__ -}