Merge pull request #1040 from clash-lang/appPropDeshadow

Ensure we properly deshadow in AppProp

Author: martijnbastiaan

clash-lib/src/Clash/Core/Evaluator.hs

@@ -438,7 +438,7 @@ scrutinise (Lit l) alts m = case alts of
   go def (_:alts1) = go def alts1
 
 scrutinise (DC dc xs) alts m
-  | altE:_ <- [substAlt altDc tvs pxs xs altE
+  | altE:_ <- [substInAlt altDc tvs pxs xs altE
               | (DataPat altDc tvs pxs,altE) <- alts, altDc == dc ] ++
               [altE | (DefaultPat,altE) <- alts ]
   = setTerm altE m
@@ -468,8 +468,8 @@ scrutinise v@(PrimVal p _ vs) alts m
 
 scrutinise v alts _ = error ("scrutinise: " ++ showPpr (Case (valToTerm v) (ConstTy Arrow) alts))
 
-substAlt :: DataCon -> [TyVar] -> [Id] -> [Either Term Type] -> Term -> Term
-substAlt dc tvs xs args e = substTm "Evaluator.substAlt" subst e
+substInAlt :: DataCon -> [TyVar] -> [Id] -> [Either Term Type] -> Term -> Term
+substInAlt dc tvs xs args e = substTm "Evaluator.substInAlt" subst e
  where
   tys        = rights args
   tms        = lefts args

clash-lib/src/Clash/Core/Subst.hs

@@ -39,8 +39,10 @@ module Clash.Core.Subst
   , extendGblSubstList
     -- ** Applying substitutions
   , substTm
+  , substAlt
     -- * Variable renaming
   , deShadowTerm
+  , deShadowAlt
   , freshenTm
     -- * Alpha equivalence
   , aeqType
@@ -491,6 +493,21 @@ substTm doc subst = go where
   goTick t@DeDup        = t
   goTick t@NoDeDup      = t
 
+-- | Substitute within a case-alternative
+substAlt
+  :: HasCallStack
+  => Doc ()
+  -> Subst
+  -- ^ The substitution
+  -> (Pat, Term)
+  -- ^ The alternative in which to apply the substitution
+  -> (Pat, Term)
+substAlt doc subst (pat,alt) = case pat of
+  DataPat dc tvs ids -> case List.mapAccumL substTyVarBndr' subst tvs of
+    (subst1,tvs1) -> case List.mapAccumL substIdBndr subst1 ids of
+      (subst2,ids1) -> (DataPat dc tvs1 ids1,substTm doc subst2 alt)
+  _ -> (pat, substTm doc subst alt)
+
 -- | Find the substitution for an 'Id' in the 'Subst'
 lookupIdSubst
   :: HasCallStack
@@ -596,6 +613,15 @@ deShadowTerm
   -> Term
 deShadowTerm is e = substTm "deShadowTerm" (mkSubst is) e
 
+-- | Ensure that non of the binders in an alternative shadow each-other, nor
+-- conflict with the in-scope set
+deShadowAlt ::
+  HasCallStack =>
+  InScopeSet ->
+  (Pat, Term) ->
+  (Pat, Term)
+deShadowAlt is = substAlt "deShadowAlt" (mkSubst is)
+
 -- | A much stronger variant of `deShadowTerm` that ensures that all bound
 -- variables are unique.
 --

clash-lib/src/Clash/Normalize.hs

@@ -47,7 +47,7 @@ import           Clash.Core.FreeVars
 import           Clash.Core.Name (nameOcc) -- TODO
 import           Clash.Core.Pretty                (showPpr, ppr)
 import           Clash.Core.Subst
-  (deShadowTerm, extendGblSubstList, mkSubst, substTm)
+  (extendGblSubstList, mkSubst, substTm)
 import           Clash.Core.Term                  (Term (..), collectArgsTicks)
 import           Clash.Core.Type                  (Type, splitCoreFunForallTy)
 import           Clash.Core.TyCon
@@ -321,9 +321,7 @@ flattenCallTree (CBranch (nm,(nm',sp,inl,tm)) used) = do
   newExpr <- case toInline of
     [] -> return tm
     _  -> do
-      -- To have a cheap `appProp` transformation we need to
-      -- deshadow, see also Note [AppProp no-shadow invariant]
-      let tm1 = deShadowTerm emptyInScopeSet (substTm "flattenCallTree.flattenExpr" subst tm)
+      let tm1 = substTm "flattenCallTree.flattenExpr" subst tm
 #ifdef HISTORY
       -- NB: When HISTORY is on, emit binary data holding the recorded rewrite steps
       let !_ = unsafePerformIO
@@ -347,9 +345,7 @@ flattenCallTree (CBranch (nm,(nm',sp,inl,tm)) used) = do
         let (toInline',allUsed') = unzip (map goCheap allUsed)
             subst' = extendGblSubstList (mkSubst emptyInScopeSet)
                                         (Maybe.catMaybes toInline')
-        -- To have a cheap `appProp` transformation we need to
-        -- deshadow, see also Note [AppProp no-shadow invariant]
-        let tm1 = deShadowTerm emptyInScopeSet (substTm "flattenCallTree.flattenCheap" subst' newExpr)
+        let tm1 = substTm "flattenCallTree.flattenCheap" subst' newExpr
         newExpr' <- rewriteExpr ("flattenCheap",flatten) (showPpr nm, tm1) (nm', sp)
         return (CBranch (nm,(nm',sp,inl,newExpr')) (concat allUsed'))
      else return (CBranch (nm,(nm',sp,inl,newExpr)) allUsed)