saw-core: Use named variables for Lambda and Pi binders.

intTests/test2049/test.log.1.good

@@ -11,9 +11,7 @@
  Subgoal failed: zero test.saw:52:4: error: in ghost_value
 Literal equality postcondition
 Expected term: 
-let { x@1 = Prelude.Vec 8 Prelude.Bool
-    }
- in zero::table
+zero::table
 Actual term:
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }

intTests/test2049/test.log.2.good

@@ -11,9 +11,7 @@
  Subgoal failed: zero test.saw:52:4: error: in ghost_value
 Literal equality postcondition
 Expected term: 
-let { x@1 = Prelude.Vec 8 Prelude.Bool
-    }
- in zero::table
+zero::table
 Actual term:
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }

intTests/test_solver_cache/test_basics.saw

@@ -10,32 +10,32 @@ test_solver_cache_stats 0 0 0 0 0;
 prove_print z3 {{ \(x:[64]) -> x == x }};
 test_solver_cache_stats 1 0 0 1 0;
 
-// Testing that cached results do not depend on variable names - thus, the
-// cache should now have one more usage, but not a new entry or insertion
+// Testing that cached results depend on variable names - thus, the cache
+// should now have one more entry and one more insertion, but not a new usage
 prove_print z3 {{ \(new_name:[64]) -> new_name == new_name }};
-test_solver_cache_stats 1 1 0 1 0;
+test_solver_cache_stats 2 0 0 2 0;
 
 // Testing that cached results depend on the backend used - thus, the cache
 // should now have one more entry and one more insertion, but not a new usage
 prove_print (w4_unint_z3 []) {{ \(x:[64]) -> x == x }};
-test_solver_cache_stats 2 1 0 2 0;
+test_solver_cache_stats 3 0 0 3 0;
 
 // Testing that cached results depend on the options passed to the given
 // backend - thus, the cache should now have one more entry and one more
 // insertion, but not a new usage
 prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64]) -> x == x }};
-test_solver_cache_stats 3 1 0 3 0;
+test_solver_cache_stats 4 0 0 4 0;
 
 // Same as the above but for sat results
 
 fails (prove_print z3 {{ \(x:[64])(y:[64]) -> x == y }});
-test_solver_cache_stats 4 1 0 4 0;
+test_solver_cache_stats 5 0 0 5 0;
 
 fails (prove_print z3 {{ \(new_name_1:[64])(new_name_2:[64]) -> new_name_1 == new_name_2 }});
-test_solver_cache_stats 4 2 0 4 0;
+test_solver_cache_stats 6 0 0 6 0;
 
 fails (prove_print w4 {{ \(x:[64])(y:[64]) -> x == y }});
-test_solver_cache_stats 5 2 0 5 0;
+test_solver_cache_stats 7 0 0 7 0;
 
 fails (prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64])(y:[64]) -> x == y }});
-test_solver_cache_stats 6 2 0 6 0;
+test_solver_cache_stats 8 0 0 8 0;

intTests/test_solver_cache/test_clean.saw

@@ -3,7 +3,7 @@
 set_solver_cache_path "test_solver_cache.cache";
 
 // The cache still has entries from prior runs
-test_solver_cache_stats 6 0 0 0 0;
+test_solver_cache_stats 8 0 0 0 0;
 
 // After cleaning, all SBV entries should be removed (see test.sh)
 clean_mismatched_versions_solver_cache;
@@ -13,4 +13,4 @@ test_solver_cache_stats 4 0 0 0 0;
 // as many insertions as there were SBV entries, and as many usages as there
 // were in test_path_second less the number of SBV entries
 include "test_ops.saw";
-test_solver_cache_stats 6 6 0 2 0;
+test_solver_cache_stats 8 4 0 4 0;

intTests/test_solver_cache/test_path_and_reuse.saw

@@ -3,10 +3,10 @@
 set_solver_cache_path "test_solver_cache.cache";
 
 // The cache still has entries from the last run
-test_solver_cache_stats 6 0 0 0 0;
+test_solver_cache_stats 8 0 0 0 0;
 
 // After running test_path_ops, we should have the same number of entries, but
 // no insertions and and as many usages as there were insertions plus usages
 // the first time
 include "test_ops.saw";
-test_solver_cache_stats 6 8 0 0 0;
+test_solver_cache_stats 8 8 0 0 0;

otherTests/saw-core/Tests/Functor.hs

@@ -50,15 +50,14 @@ shared :: TermIndex -> TermF Term -> Term
 shared ix t = STApp {
     stAppIndex = ix,
     stAppHash = hash t,
-    stAppLooseVars = emptyBitSet,
     stAppFreeVars = mempty,
     stAppTermF = t
  }
 
--- | Some LocalNames (LocalName is just Text)
-lnFoo, lnBar :: LocalName
-lnFoo = "foo"
-lnBar = "bar"
+-- | Some variable names
+vnFoo, vnBar :: VarName
+vnFoo = VarName 2 "foo"
+vnBar = VarName 3 "bar"
 
 -- | An external constant
 nmFoo :: Name
@@ -75,7 +74,7 @@ nmFoo = Name {
 type Failure = (String, String, String)
 type Result = Either Failure ()
 
--- | Check a result. 
+-- | Check a result.
 check :: Failure -> Bool -> Result
 check _ True = Right ()
 check f False = Left f
@@ -175,19 +174,19 @@ instance TestIt Term where
         let depth' = depth + 1
             unit = Unshared $ FTermF $ UnitValue
             zero = Unshared $ FTermF $ NatLit 0
-            localvar = Unshared $ LocalVar 0
+            localvar = Unshared $ Variable vnBar t
         testOne depth' $ PairValue t t
         testOne depth' $ PairValue t zero
         testOne depth' $ PairValue unit t
         testOne depth' $ App t t
         testOne depth' $ App t zero
         testOne depth' $ App unit t
-        testOne depth' $ Lambda lnFoo t t
-        testOne depth' $ Lambda lnBar t localvar
-        testOne depth' $ Pi lnFoo t t
-        testOne depth' $ Pi lnBar t localvar
-        testTwo depth' GT (Lambda lnFoo t t) (Lambda lnBar t t)
-        testTwo depth' GT (Pi lnFoo t t) (Pi lnBar t t)
+        testOne depth' $ Lambda vnFoo t t
+        testOne depth' $ Lambda vnBar t localvar
+        testOne depth' $ Pi vnFoo t t
+        testOne depth' $ Pi vnBar t localvar
+        testTwo depth' LT (Lambda vnFoo t t) (Lambda vnBar t t)
+        testTwo depth' LT (Pi vnFoo t t) (Pi vnBar t t)
         testTwo depth' EQ (Constant nmFoo :: TermF Term) (Constant nmFoo :: TermF Term)
 
   testTwo depth comp t1 t2 = do
@@ -197,12 +196,12 @@ instance TestIt Term where
       when (depth < 2 && comp /= EQ) $ do
         let depth' = depth + 1
         -- check that the variable name affects the comparison
-        testTwo depth' comp (Lambda lnFoo t1 t1) (Lambda lnFoo t2 t2)
-        testTwo depth' GT (Lambda lnFoo t1 t1) (Lambda lnBar t2 t2)
-        testTwo depth' LT (Lambda lnBar t1 t1) (Lambda lnFoo t2 t2)
-        testTwo depth' comp (Pi lnFoo t1 t1) (Pi lnFoo t2 t2)
-        testTwo depth' GT (Pi lnFoo t1 t1) (Pi lnBar t2 t2)
-        testTwo depth' LT (Pi lnBar t1 t1) (Pi lnFoo t2 t2)
+        testTwo depth' comp (Lambda vnFoo t1 t1) (Lambda vnFoo t2 t2)
+        testTwo depth' LT (Lambda vnFoo t1 t1) (Lambda vnBar t2 t2)
+        testTwo depth' GT (Lambda vnBar t1 t1) (Lambda vnFoo t2 t2)
+        testTwo depth' comp (Pi vnFoo t1 t1) (Pi vnFoo t2 t2)
+        testTwo depth' LT (Pi vnFoo t1 t1) (Pi vnBar t2 t2)
+        testTwo depth' GT (Pi vnBar t1 t1) (Pi vnFoo t2 t2)
         pure ()
 
 -- | Run some tests

otherTests/saw-core/Tests/Parser.hs

@@ -24,11 +24,11 @@ checkDef :: Def -> Assertion
 checkDef d = do
   let sym = nameInfo (defName d)
   let tp = defType d
-  assertBool (namedMsg sym "Type is not ground.") (termIsClosed tp)
+  assertBool (namedMsg sym "Type is not ground.") (closedTerm tp)
   case defBody d of
     Nothing -> return ()
     Just body ->
-      assertBool (namedMsg sym "Body is not ground.") (termIsClosed body)
+      assertBool (namedMsg sym "Body is not ground.") (closedTerm body)
 
 checkPrelude :: Assertion
 checkPrelude =

saw-central/src/SAWCentral/Bisimulation.hs

@@ -259,7 +259,6 @@ openConstantApp :: TypedTerm
                 -- 'Constant' (will be unfolded).
                 -> TopLevel (ExtCns Term, TermF Term)
 openConstantApp constant t = do
-  sc <- getSharedContext
   -- Unfold constant
   name <- constantName (unwrapTermF (ttTerm t))
   tUnfolded <- unfold_term [name] t
@@ -269,15 +268,15 @@ openConstantApp constant t = do
 
   -- Replace outer function's argument with an 'ExtCns'
   -- NOTE: The bisimulation relation type ensures this is a single argument
-  -- lambda, so it's OK to apply scOpenTerm once and not recurse
-  (ec, tExtconsified) <- io $ scOpenTerm sc nm tp 0 body
-  extractedF <- extractApp constant tExtconsified
+  -- lambda, so it's OK to not recurse
+  let ec = EC nm tp
+  extractedF <- extractApp constant body
   pure (ec, extractedF)
 
   where
     -- Break down lambda into its component parts.  Fails if 'tt' is not a
     -- lambda.
-    lambdaOrFail :: TypedTerm -> TopLevel (LocalName, Term, Term)
+    lambdaOrFail :: TypedTerm -> TopLevel (VarName, Term, Term)
     lambdaOrFail tt =
       case asLambda (ttTerm tt) of
         Just lambda -> return lambda

saw-central/src/SAWCentral/Builtins.hs

@@ -71,7 +71,7 @@ import SAWCore.FiniteValue
   , FirstOrderValue(..)
   , scFirstOrderValue
   )
-import SAWCore.Name (ecShortName)
+import SAWCore.Name (VarName(..), ecShortName)
 import SAWCore.SATQuery
 import SAWCore.SCTypeCheck
 import SAWCore.Recognizer
@@ -272,10 +272,10 @@ replacePrim pat replace t = do
   let tpat  = ttTerm pat
   let trepl = ttTerm replace
 
-  unless (termIsClosed tpat) $ fail $ unlines
+  unless (closedTerm tpat) $ fail $ unlines
     [ "pattern term is not closed", show tpat ]
 
-  unless (termIsClosed trepl) $ fail $ unlines
+  unless (closedTerm trepl) $ fail $ unlines
     [ "replacement term is not closed", show trepl ]
 
   io $ do
@@ -732,15 +732,15 @@ build_congruence sc tm =
      case asPiList ty of
        ([],_) -> fail "congruence_for: Term is not a function"
        (pis, body) ->
-         if termIsClosed body then
+         if closedTerm body then
            loop pis []
          else
            fail "congruence_for: cannot build congruence for dependent functions"
  where
   loop ((nm,tp):pis) vars =
-    if termIsClosed tp then
-      do l <- scFreshEC sc (nm <> "_1") tp
-         r <- scFreshEC sc (nm <> "_2") tp
+    if closedTerm tp then
+      do l <- scFreshEC sc (vnName nm <> "_1") tp
+         r <- scFreshEC sc (vnName nm <> "_2") tp
          loop pis ((l,r):vars)
      else
        fail "congruence_for: cannot build congruence for dependent functions"
@@ -1396,8 +1396,8 @@ proveByBVInduction script t =
   -- and the width of the bitvector we are doing induction on.
   checkInductionScheme sc opts pis ty =
     do ty' <- scWhnf sc ty
-       scAsPi sc ty' >>= \case
-         Just (ec, body) -> checkInductionScheme sc opts (ec : pis) body
+       case asPi ty' of
+         Just (nm, tp, body) -> checkInductionScheme sc opts (EC nm tp : pis) body
          Nothing ->
            case asTupleType ty' of
              Just [bv, bool] ->
@@ -1953,7 +1953,7 @@ parseCoreMod mnm_str input =
      let mnm =
            mkModuleName $ Text.splitOn "." mnm_str
      _ <- io $ scFindModule sc mnm -- Check that mnm exists
-     err_or_t <- io $ inferCompleteTermCtx sc (Just mnm) [] uterm
+     err_or_t <- io $ inferCompleteTermCtx sc (Just mnm) mempty uterm
      case err_or_t of
        Left err -> fail (show err)
        Right x -> pure x

saw-central/src/SAWCentral/Crucible/Common/Override.hs

@@ -108,7 +108,7 @@ import           Data.Parameterized.TraversableFC (toListFC)
 
 import qualified SAWSupport.Pretty as PPS (defaultOpts, limitMaxDepth)
 
-import           SAWCore.Name (ecShortName)
+import           SAWCore.Name (VarName(..), ecShortName)
 import           SAWCore.Prelude as SAWVerifier (scEq)
 import           SAWCore.SharedTerm as SAWVerifier
 import           SAWCore.Term.Functor (unwrapTermF)
@@ -723,9 +723,9 @@ matchTerm sc md prepost real expect =
   do let loc = MS.conditionLoc md
      free <- OM (use osFree)
      case unwrapTermF expect of
-       Variable ec
-         | Set.member (ecVarIndex ec) free ->
-         do assignTerm sc md prepost (ecVarIndex ec) real
+       Variable vn _tp
+         | Set.member (vnIndex vn) free ->
+         do assignTerm sc md prepost (vnIndex vn) real
 
        _ ->
          do t <- liftIO $ scEq sc real expect