SAWCore fixes for variable name shadowing

intTests/test2939/test01.log.good

@@ -9,11 +9,3 @@ at test01.saw:11:1-16:3
 (y : Bool)
 -> EqTrue (ecEq Bool PEqBit (ecAnd Bool PLogicBit y True) y)
 
-Stack trace:
-   (builtin) in goal_apply
-   test01.saw:13:4-13:25 in (callback)
-   (builtin) in prove_print
-   test01.saw:11:1-16:3 (at top level)
-apply tactic failed: no match
-
-FAILED

intTests/test2939/test06c.log.good

@@ -4,16 +4,8 @@ Theorem ((x : Bool)
 -> EqTrue (ecEq Bool PEqBit x x))
 ======
 Goal prove_print (goal number 0): prove
-at test06c.saw:16:1-23:3
+at test06c.saw:16:1-22:3
 
 (y : Bool)
 -> EqTrue (ecEq Bool PEqBit y y)
 
-Stack trace:
-   (builtin) in goal_apply
-   test06c.saw:19:4-19:27 in (callback)
-   (builtin) in prove_print
-   test06c.saw:16:1-23:3 (at top level)
-apply tactic failed: no match
-
-FAILED

intTests/test2939/test06c.saw

@@ -17,7 +17,6 @@ prove_print (do {
    simplify (addsimp and_true_r empty_ss);
    print_goal;
    goal_apply eq_refl_bool;
-   trivial;
 }) {{
    \y -> y && True == y
 }};

saw-central/src/SAWCentral/Builtins.hs

@@ -279,7 +279,7 @@ replacePrim pat replace t = do
   io $ do
     ty1 <- scTypeOf sc tpat
     ty2 <- scTypeOf sc trepl
-    c <- scConvertible sc False ty1 ty2
+    c <- scConvertible sc ty1 ty2
     unless c $ fail $ unlines
       [ "terms do not have convertible types", show tpat, show ty1, show trepl, show ty2 ]
 
@@ -289,7 +289,7 @@ replacePrim pat replace t = do
   io $ do
     ty  <- scTypeOf sc (ttTerm t)
     ty' <- scTypeOf sc t'
-    c' <- scConvertible sc False ty ty'
+    c' <- scConvertible sc ty ty'
     unless c' $ fail $ unlines
       [ "term does not have the same type after replacement", show ty, show ty' ]
 
@@ -304,7 +304,7 @@ hoistIfsPrim t = do
   io $ do
     ty  <- scTypeOf sc (ttTerm t)
     ty' <- scTypeOf sc t'
-    c' <- scConvertible sc False ty ty'
+    c' <- scConvertible sc ty ty'
     unless c' $ fail $ unlines
       [ "term does not have the same type after hoisting ifs", show ty, show ty' ]
 
@@ -313,7 +313,7 @@ hoistIfsPrim t = do
 isConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel Bool
 isConvertiblePrim x y = do
    sc <- getSharedContext
-   io $ scConvertible sc False (ttTerm x) (ttTerm y)
+   io $ scConvertible sc (ttTerm x) (ttTerm y)
 
 checkConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel ()
 checkConvertiblePrim x y = do
@@ -1597,7 +1597,7 @@ check_term tt = do
       TypedTermSchema schema -> io $ importSchemaCEnv sc cenv schema
       TypedTermKind k -> io $ Cryptol.importKind sc k
       TypedTermOther ty' -> pure ty'
-  convertible <- io $ scConvertible sc True ty expectedTy
+  convertible <- io $ scConvertible sc ty expectedTy
   ty' <- liftIO $ ppTerm sc opts ty
   unless convertible $ do
     expectedTy' <- liftIO $ ppTerm sc opts expectedTy

saw-central/src/SAWCentral/Crucible/LLVM/X86.hs

@@ -909,7 +909,7 @@ setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func
 
        -- check that the produced term is type-correct
        tp <- scTypeOf sc inv
-       ok <- scConvertible sc True tp =<< scBoolType sc
+       ok <- scConvertible sc tp =<< scBoolType sc
        unless ok $ do
          -- TODO, get ppOpts from the right place
          tp' <- ppTerm sc PPS.defaultOpts tp

saw-central/src/SAWCentral/Proof.hs

@@ -619,7 +619,7 @@ sequentConstantSet sqt = foldr (\p m -> Map.union (getConstantSet (unProp p)) m)
 convertibleProps :: SharedContext -> [Prop] -> [Prop] -> IO Bool
 convertibleProps _sc [] [] = return True
 convertibleProps sc (p1:ps1) (p2:ps2) =
-  do ok1 <- scConvertible sc True (unProp p1) (unProp p2)
+  do ok1 <- scConvertible sc (unProp p1) (unProp p2)
      ok2 <- convertibleProps sc ps1 ps2
      return (ok1 && ok2)
 convertibleProps _sc _ _ = return False
@@ -1379,15 +1379,15 @@ propsSubset sc ps1 ps2 =
 -- exists y in ps where x == y
 propsElem :: SharedContext -> Prop -> [Prop] -> IO Bool
 propsElem sc x ps =
-  or <$> sequence [ scConvertible sc True (unProp x) (unProp y) | y <- ps ]
+  or <$> sequence [ scConvertible sc (unProp x) (unProp y) | y <- ps ]
 
 -- | Test if a sequent is an instance of the sequent calculus axiom.
 --   This occurs precisely when some hypothesis is convertible
 --   to some conclusion.
 sequentIsAxiom :: SharedContext -> Sequent -> IO Bool
 sequentIsAxiom sc sqt =
   do let RawSequent hs gs = sequentToRawSequent sqt
-     or <$> sequence [ scConvertible sc True (unProp x) (unProp y) | x <- hs, y <- gs ]
+     or <$> sequence [ scConvertible sc (unProp x) (unProp y) | x <- hs, y <- gs ]
 
 -- | Test if the first given sequent subsumes the
 --   second given sequent. This is a shallow syntactic
@@ -1575,7 +1575,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
         case sequentState sqt of
           ConclFocus (Prop ptm) _ ->
             do ty <- scTypeOf sc tm
-               ok <- scConvertible sc True ptm ty
+               ok <- scConvertible sc ptm ty
                unless ok $ do
                    ptm' <- ppTerm sc PPS.defaultOpts ptm
                    tm' <- ppTerm sc PPS.defaultOpts tm
@@ -1632,7 +1632,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
             case genericDrop n hs of
               (h:_) ->
                 do (d,sy,p') <- checkApply nenv (\g' -> ConclFocusedSequent hs (FB gs1 g' gs2)) h es
-                   ok <- scConvertible sc False (unProp g) p'
+                   ok <- scConvertible sc (unProp g) p'
                    unless ok $ do
                        g' <- ppTerm sc PPS.defaultOpts (unProp g)
                        p'' <- ppTerm sc PPS.defaultOpts p'
@@ -1656,7 +1656,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
         case sequentState sqt of
           ConclFocus p mkSqt ->
             do (d,sy,p') <- checkApply nenv mkSqt (thmProp thm) es
-               ok <- scConvertible sc False (unProp p) p'
+               ok <- scConvertible sc (unProp p) p'
                unless ok $ do
                    sp <- ppTerm sc PPS.defaultOpts (unProp p)
                    sp' <- ppTerm sc PPS.defaultOpts p'
@@ -1759,7 +1759,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
                   ptm' <- ppTerm sc PPS.defaultOpts ptm
                   fail $ unlines ["Intro evidence expected function prop", ptm']
               Just (nm, ty, body) ->
-                do ok <- scConvertible sc False ty xty
+                do ok <- scConvertible sc ty xty
                    unless ok $ do
                        xty' <- ppTerm sc PPS.defaultOpts xty
                        ty' <- ppTerm sc PPS.defaultOpts ty
@@ -1924,7 +1924,7 @@ predicateToSATQuery sc unintSet tm0 =
           -- TODO: check that the type is a boolean
         Nothing ->
           do ty <- scTypeOf sc tm
-             ok <- scConvertible sc True ty =<< scBoolType sc
+             ok <- scConvertible sc ty =<< scBoolType sc
              unless ok $ do
                ty' <- ppTerm sc PPS.defaultOpts ty
                tm0' <- ppTerm sc PPS.defaultOpts tm0
@@ -2270,7 +2270,7 @@ tacticTrivial sc = Tactic \goal ->
         Right pf ->
            do let gp = unProp g
               ty <- liftIO $ scTypeOf sc pf
-              ok <- liftIO $ scConvertible sc True gp ty
+              ok <- liftIO $ scConvertible sc gp ty
               unless ok $ do
                   gp' <- liftIO $ ppTerm sc PPS.defaultOpts gp
                   fail $ unlines [
@@ -2288,7 +2288,7 @@ tacticExact sc tm = Tactic \goal ->
     ConclFocus g _ ->
       do let gp = unProp g
          ty <- liftIO $ scTypeOf sc tm
-         ok <- liftIO $ scConvertible sc True gp ty
+         ok <- liftIO $ scConvertible sc gp ty
          unless ok $ do
              gp' <- liftIO $ ppTerm sc PPS.defaultOpts gp
              tm' <- liftIO $ ppTerm sc PPS.defaultOpts tm

saw-core/src/SAWCore/Name.hs

@@ -40,6 +40,10 @@ module SAWCore.Name
     -- * VarName
   , VarName(..)
   , wildcardVarName
+  , VarCtx(..)
+  , emptyVarCtx
+  , consVarCtx
+  , lookupVarCtx
     -- * Display Name Environments
   , DisplayNameEnv(..)
   , emptyDisplayNameEnv
@@ -303,6 +307,33 @@ instance Hashable VarName where
 wildcardVarName :: VarName
 wildcardVarName = VarName 0 "_"
 
+-- | A data type representing a context of bound 'VarName's.
+-- It maps each 'VarName' to a de Bruijn index.
+data VarCtx =
+  VarCtx
+  !Int -- ^ Context size
+  !(IntMap Int) -- ^ Mapping from VarIndex to (size - de Bruijn index)
+
+-- | The empty 'VarName' context.
+emptyVarCtx :: VarCtx
+emptyVarCtx = VarCtx 0 IntMap.empty
+
+-- | Extend a 'VarCtx' with a new bound 'VarName'.
+-- The new name has de Bruijn index 0; the index of each previous name
+-- is incremented by one.
+consVarCtx :: VarName -> VarCtx -> VarCtx
+consVarCtx x (VarCtx size m) =
+  let size' = size + 1
+  in VarCtx size' (IntMap.insert (vnIndex x) size' m)
+
+-- | Look up the de Bruijn index of the given 'VarName' in a 'VarCtx'.
+-- Return 'Nothing' if the name is not present in the context.
+lookupVarCtx :: VarName -> VarCtx -> Maybe Int
+lookupVarCtx x (VarCtx size m) =
+  case IntMap.lookup (vnIndex x) m of
+    Just i -> Just (size - i)
+    Nothing -> Nothing
+
 
 -- Display Name Environments --------------------------------------------------------
 

saw-core/src/SAWCore/Rewriter.hs

@@ -222,7 +222,7 @@ scMatch ::
 scMatch sc ctxt pat term =
   runMaybeT $
   do -- lift $ putStrLn $ "********** scMatch **********"
-     MatchState inst cs <- match IntSet.empty pat term emptyMatchState
+     MatchState inst cs <- match emptyVarCtx emptyVarCtx [] pat term emptyMatchState
      mapM_ (check inst) cs
      return inst
   where
@@ -246,40 +246,51 @@ scMatch sc ctxt pat term =
     -- Check if a term is a higher-order variable pattern, i.e., a free variable
     -- (meaning one that can match anything) applied to 0 or more bound variable
     -- arguments.
-    asVarPat :: IntSet -> Term -> Maybe (VarIndex, [(VarName, Term)])
+    asVarPat :: VarCtx -> Term -> Maybe (VarIndex, [Int])
     asVarPat locals = go []
       where
-        go js x =
-          case unwrapTermF x of
-            Variable nm _tp
-              | IntSet.member (vnIndex nm) ixs -> Just (vnIndex nm, js)
+        go js t =
+          case unwrapTermF t of
+            Variable x _tp
+              | IntSet.member (vnIndex x) ixs -> Just (vnIndex x, js)
               | otherwise  -> Nothing
-            App t (unwrapTermF -> Variable nm tp)
-              | IntSet.member (vnIndex nm) locals -> go ((nm, tp) : js) t
+            App t1 (unwrapTermF -> Variable x _) ->
+              case lookupVarCtx x locals of
+                Just j -> go (j : js) t1
+                Nothing -> Nothing
             _ -> Nothing
 
     -- Test if term y matches pattern x, meaning whether there is a substitution
     -- to the free variables of x to make it equal to y.
-    -- The IntSet contains the VarIndexes named variables that are locally bound.
-    match :: IntSet -> Term -> Term -> MatchState -> MaybeT IO MatchState
-    match _ x y s
-      | closedTerm x && termIndex x == termIndex y = pure s
-    match locals x y s@(MatchState m cs) =
+    -- The IntMap contains the VarIndexes of locally bound variables.
+    -- The first two arguments are the bound variable contexts of x and y, respectively.
+    match ::
+      VarCtx -> VarCtx -> [(VarName, Term)] ->
+      Term -> Term -> MatchState -> MaybeT IO MatchState
+    match (VarCtx _ xm) (VarCtx _ ym) _ x y s
+      | termIndex x == termIndex y &&
+        -- bound variables must also refer to the same de Bruijn indices
+        IntMap.intersection xm (varTypes x) ==
+        IntMap.intersection ym (varTypes y) = pure s
+    match xenv yenv ybinds x y s@(MatchState m cs) =
       -- (lift $ putStrLn $ "matching (lhs): " ++ ppTermPure PPS.defaultOpts x) >>
       -- (lift $ putStrLn $ "matching (rhs): " ++ ppTermPure PPS.defaultOpts y) >>
-      case asVarPat locals x of
+      case asVarPat xenv x of
         -- If the lhs pattern is of the form (?u b1..bk) where ?u is a
         -- unification variable and b1..bk are all locally bound
         -- variables: First check whether the rhs contains any locally
         -- bound variables *not* in the list b1..bk. If it contains any
         -- others, then there is no match. If it only uses a subset of
         -- b1..bk, then we can instantiate ?u to (\b1..bk -> rhs).
-        Just (i, vs) ->
+        Just (i, js) ->
           do -- ensure parameter variables are distinct
-             guard (Set.size (Set.fromList vs) == length vs)
-             -- ensure y mentions only variables that are in vs
-             let vset = IntSet.fromList (map (vnIndex . fst) vs)
-             guard (IntSet.disjoint (IntSet.difference locals vset) (freeVars y))
+             guard (Set.size (Set.fromList js) == length js)
+             -- ensure y mentions no local variables not in js
+             let VarCtx ysize ym = yenv
+             let ks = map (ysize -) $ IntMap.elems $ IntMap.intersection ym (varTypes y)
+             -- ks must be a subset of js
+             guard (IntSet.isSubsetOf (IntSet.fromList ks) (IntSet.fromList js))
+             let vs = map (ybinds !!) js
              y2 <- lift $ scLambdaList sc vs y
              let (my3, m') = insertLookup i y2 m
              case my3 of
@@ -289,18 +300,26 @@ scMatch sc ctxt pat term =
           case (unwrapTermF x, unwrapTermF y) of
             -- check that neither x nor y contains bound variables less than `depth`
             (FTermF xf, FTermF yf) ->
-              case zipWithFlatTermF (match locals) xf yf of
+              case zipWithFlatTermF (match xenv yenv ybinds) xf yf of
                 Nothing -> mzero
                 Just zf -> Foldable.foldl (>=>) return zf s
             (App x1 x2, App y1 y2) ->
-              match locals x1 y1 s >>= match locals x2 y2
-            (Lambda nm t1 x1, Lambda _ t2 x2) ->
-              match locals t1 t2 s >>= match (IntSet.insert (vnIndex nm) locals) x1 x2
-            (Pi nm t1 x1, Pi _ t2 x2) ->
-              match locals t1 t2 s >>= match (IntSet.insert (vnIndex nm) locals) x1 x2
+              do s' <- match xenv yenv ybinds x1 y1 s
+                 match xenv yenv ybinds x2 y2 s'
+            (Lambda xv xt xbody, Lambda yv yt ybody) ->
+              do s' <- match xenv yenv ybinds xt yt s
+                 match (consVarCtx xv xenv) (consVarCtx yv yenv) ((yv, yt) : ybinds) xbody ybody s'
+            (Pi xv x1 x2, Pi yv y1 y2) ->
+              do s' <- match xenv yenv ybinds x1 y1 s
+                 match (consVarCtx xv xenv) (consVarCtx yv yenv) ((yv, y1) : ybinds) x2 y2 s'
+            (Variable xv _, Variable yv _) ->
+              case (lookupVarCtx xv xenv, lookupVarCtx yv yenv) of
+                (Just xj, Just yj) | xj == yj -> pure s
+                (Nothing, Nothing) | xv == yv -> pure s
+                _ -> mzero
             (_, _) ->
-              -- other possible matches are local vars and constants
-              if x == y then return s else mzero
+              -- other possible matches include constants
+              if x == y then pure s else mzero
 
 ----------------------------------------------------------------------
 -- Building rewrite rules

saw-core/src/SAWCore/SharedTerm.hs

@@ -1030,12 +1030,11 @@ scWhnf sc t = execSCM sc (scmWhnf t)
 -- by 'scWhnf'.
 scConvertible ::
   SharedContext ->
-  Bool {- ^ Should constants be unfolded during this check? -} ->
   Term ->
   Term ->
   IO Bool
-scConvertible sc unfoldConst t1 t2 =
-  execSCM sc (scmConvertible unfoldConst t1 t2)
+scConvertible sc t1 t2 =
+  execSCM sc (scmConvertible t1 t2)
 
 -- | Check whether one type is a subtype of another: Either they are
 -- convertible, or they are both Pi types with convertible argument