[clean up substitution code, add docs, fix bug in getting free vars in type substitution
John Meacham <john@repetae.net>**20051011001834] hunk ./E/Subst.hs 1
-module E.Subst(subst,subst',eAp, substMap,substMap',noShadow,doSubst,typeSubst,typeSubst',substMap'',litSMapM ) where
+module E.Subst(subst,subst',eAp, substMap,substMap',doSubst,typeSubst,typeSubst',substMap'',litSMapM ) where
hunk ./E/Subst.hs 32
---subst (TVr { tvrIdent = i }) w e = doSubst False False (Map.insert i (Just w) $ Map.fromList [ (x,Nothing) | x <- freeVars (getType w) ++ freeVars e ]) e
-subst (TVr { tvrIdent = i }) w e = doSubst False False (Map.insert i (Just w) $ Map.fromList [ (x,Nothing) | x <- freeVars w ++ freeVars e ]) e
+subst (TVr { tvrIdent = i }) w e = doSubst False False (Map.insert i (Just w) $ (freeVars w `Map.union` freeVars e))  e
hunk ./E/Subst.hs 42
---subst' (TVr { tvrIdent = (i) }) w e = doSubst True False (Map.insert i (Just w) $ Map.fromList [ (x,Nothing) | x <- freeVars (getType w) ++ freeVars e ]) e
-subst' (TVr { tvrIdent = (i) }) w e = doSubst True False (Map.insert i (Just w) $ Map.fromList [ (x,Nothing) | x <- freeVars w ++ freeVars e ]) e
+subst' (TVr { tvrIdent = (i) }) w e = doSubst True False (Map.insert i (Just w) $ (freeVars w `Map.union` freeVars e)) e
hunk ./E/Subst.hs 45
-substMap :: IM.IntMap E -> E -> E
-substMap im e = substMapScope im (IS.unions $ freeVars e: (map freeVars (IM.elems im))) e
hunk ./E/Subst.hs 54
---litSMapM f l = fmapM f l
hunk ./E/Subst.hs 62
-noShadow :: E -> E
-noShadow e = doSubst False False (Map.fromList [ (x,Nothing) | x <- freeVars e ]) e
-
hunk ./E/Subst.hs 65
+substMap :: IM.IntMap E -> E -> E
+substMap im e = substMapScope im (IS.unions $ freeVars e: (map freeVars (IM.elems im))) e
+
hunk ./E/Subst.hs 179
-substType t e e' = typeSubst (freeVars e) (Map.singleton t e) e'
--- Monadic code is so much nicer
-typeSubst :: Map.Map Id (Maybe E) -> Map.Map Id E -> E -> E
+substType t e e' = typeSubst (freeVars e `Map.union` freeVars e') (Map.singleton t e) e'
+
+-- | substitution routine that can substitute different values at the term and type level.
+-- this is useful to enforce the invarient that let-bound variables must not occur at the type level, yet
+-- non-atomic values (even typelike ones) cannot appear in argument positions at the term level.
+
+typeSubst ::
+    Map.Map Id (Maybe E)  -- ^ substitution to carry out at term level as well as a list of in-scope variables
+    -> Map.Map Id E       -- ^ substitution to carry out at type level
+    -> (E -> E)           -- ^ the substitution function