saw-core: Rename function 'scInstantiateExt' to 'scInstantiate'.

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -588,7 +588,7 @@ buildSubstMap sc substs0 = go IntMap.empty substs0
     go sm ((vn, term) : substs) = do
         -- Rewrite the RHSs of previous substitutions using the current one.
         let sm1 = IntMap.singleton (SAW.vnIndex vn) term
-        sm' <- mapM (SAW.scInstantiateExt sc sm1) sm
+        sm' <- mapM (SAW.scInstantiate sc sm1) sm
         -- Add the current subst and continue.
         go (IntMap.insert (SAW.vnIndex vn) term sm') substs
 
@@ -677,7 +677,7 @@ substMethodSpec sc sm ms = do
         term' <- goTerm $ SAW.ttTerm tt
         return $ tt { SAW.ttTerm = term' }
 
-    goTerm term = SAW.scInstantiateExt sc sm term
+    goTerm term = SAW.scInstantiate sc sm term
 
 
 

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -545,7 +545,7 @@ setupToReg sym termSub myRegMap allocMap shp0 sv0 = go shp0 sv0
     go (UnitShape _) (MS.SetupTuple _ []) = return ()
     go (PrimShape _ btpr) (MS.SetupTerm tt) = do
         let sc = mirSharedContext (sym ^. W4.userState)
-        term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
+        term <- liftIO $ SAW.scInstantiate sc termSub $ SAW.ttTerm tt
         Some expr <- termToExpr sym myRegMap term
         Refl <- case testEquality (W4.exprType expr) btpr of
             Just x -> return x
@@ -607,7 +607,7 @@ condTerm _sc (MS.SetupCond_Equal _loc _sv1 _sv2) = do
     error $ "learnCond: SetupCond_Equal NYI" -- TODO
 condTerm sc (MS.SetupCond_Pred md tt) = do
     sub <- use MS.termSub
-    t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt
+    t' <- liftIO $ SAW.scInstantiate sc sub $ SAW.ttTerm tt
     return (md, t')
 condTerm _ (MS.SetupCond_Ghost _ _ _) = do
     error $ "learnCond: SetupCond_Ghost is not supported"

saw-central/src/SAWCentral/Bisimulation.hs

@@ -226,8 +226,7 @@ buildCompositionSideCondition bc innerBt = do
   lhsTuple <- io $ scTuple sc [lhsOuterState, input]  -- (f_lhs_s, in)
   rhsTuple <- io $ scTuple sc [rhsOuterState, input]  -- (f_rhs_s, in)
   innerRel' <- io $
-    scInstantiateExt sc
-                     (IntMap.fromList [ (vnIndex lhsInnerVar, lhsTuple)
+    scInstantiate sc (IntMap.fromList [ (vnIndex lhsInnerVar, lhsTuple)
                                       , (vnIndex rhsInnerVar, rhsTuple)])
                      innerRel
 

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

@@ -689,7 +689,7 @@ executeGhost ::
   OverrideMatcher ext RW ()
 executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) =
   do s <- OM (use termSub)
-     tm' <- liftIO (scInstantiateExt sc s tm)
+     tm' <- liftIO (scInstantiate sc s tm)
      writeGlobal var (sch,tm')
 executeGhost _sc _md _var (TypedTerm tp _) =
   fail $ unlines
@@ -708,7 +708,7 @@ instantiateExtMatchTerm ::
   OverrideMatcher ext md ()
 instantiateExtMatchTerm sc md prepost actual expected = do
   sub <- OM (use termSub)
-  matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected)
+  matchTerm sc md prepost actual =<< liftIO (scInstantiate sc sub expected)
 
 matchTerm ::
   SharedContext   {- ^ context for constructing SAW terms    -} ->

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

@@ -730,7 +730,7 @@ learnPred ::
   OverrideMatcher CJ.JVM w ()
 learnPred sc cc md prepost t =
   do s <- OM (use termSub)
-     u <- liftIO $ scInstantiateExt sc s t
+     u <- liftIO $ scInstantiate sc s t
      p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) u
      let loc = MS.conditionLoc md
      addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))
@@ -742,7 +742,7 @@ instantiateExtResolveSAWPred ::
   OverrideMatcher CJ.JVM md (W4.Pred Sym)
 instantiateExtResolveSAWPred sc cc cond = do
   sub <- OM (use termSub)
-  liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
+  liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
 
 ------------------------------------------------------------------------
 
@@ -918,7 +918,7 @@ executePred ::
   OverrideMatcher CJ.JVM w ()
 executePred sc cc md tt =
   do s <- OM (use termSub)
-     t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
+     t <- liftIO $ scInstantiate sc s (ttTerm tt)
      p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) t
      addAssume p md
 
@@ -949,7 +949,7 @@ instantiateSetupValue sc s v =
     MS.SetupGlobalInitializer empty _ -> absurd empty
     MS.SetupMux empty _ _ _           -> absurd empty
   where
-    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
+    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
 
 ------------------------------------------------------------------------
 

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

@@ -459,7 +459,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
                 IntMap.fromList $
                 zip (map (vnIndex . fst) output_parameters) (map ttTerm applied_extracted_func_selectors)
           let substitute_output_parameters =
-                ttTermLens $ scInstantiateExt shared_context output_parameter_substitution
+                ttTermLens $ scInstantiate shared_context output_parameter_substitution
           let setup_value_substitute_output_parameter setup_value
                 | SetupTerm term <- setup_value = SetupTerm <$> substitute_output_parameters term
                 | otherwise = return $ setup_value

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

@@ -1483,7 +1483,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
                           zero_byte_tm <- scBvNat sc byte_width_tm =<< scNat sc 0
                           zero_arr_const_tm <- scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm
 
-                          instantiated_expected_sz_tm <- scInstantiateExt sc sub $ ttTerm expected_sz_tm
+                          instantiated_expected_sz_tm <- scInstantiate sc sub $ ttTerm expected_sz_tm
                           scArrayCopy sc ptr_width_tm byte_type_tm
                             zero_arr_const_tm -- dest array
                             zero_off_tm -- dest offset
@@ -1502,7 +1502,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
 
               _ ->
                 do sub <- OM (use termSub)
-                   instantiated_expected_sz_tm <- liftIO $ scInstantiateExt sc sub $ ttTerm expected_sz_tm
+                   instantiated_expected_sz_tm <- liftIO $ scInstantiate sc sub $ ttTerm expected_sz_tm
                    normalized_expected_sz_tm <- liftIO $
                      scTypeCheckWHNF sc =<< scUnfoldConstantSet sc False mempty instantiated_expected_sz_tm
                    case asUnsignedConcreteBv normalized_expected_sz_tm of
@@ -1743,7 +1743,7 @@ instantiateExtResolveSAWPred ::
   OverrideMatcher (LLVM arch) md (W4.Pred Sym)
 instantiateExtResolveSAWPred sc cc cond = do
   sub <- OM (use termSub)
-  liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
+  liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
 
 instantiateExtResolveSAWSymBV ::
   (?w4EvalTactic :: W4EvalTactic, 1 <= w) =>
@@ -1754,7 +1754,7 @@ instantiateExtResolveSAWSymBV ::
   OverrideMatcher (LLVM arch) md (W4.SymBV Sym w)
 instantiateExtResolveSAWSymBV sc cc w tm = do
   sub <- OM (use termSub)
-  liftIO $ resolveSAWSymBV cc w =<< scInstantiateExt sc sub tm
+  liftIO $ resolveSAWSymBV cc w =<< scInstantiate sc sub tm
 
 ------------------------------------------------------------------------
 
@@ -1979,7 +1979,7 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v
      val' <- liftIO $ case val of
        ConcreteSizeValue val'' -> ConcreteSizeValue <$> instantiateSetupValue sc s val''
        SymbolicSizeValue arr sz ->
-         SymbolicSizeValue <$> ttTermLens (scInstantiateExt sc s) arr <*> ttTermLens (scInstantiateExt sc s) sz
+         SymbolicSizeValue <$> ttTermLens (scInstantiate sc s) arr <*> ttTermLens (scInstantiate sc s) sz
      cond' <- mapM (instantiateExtResolveSAWPred sc cc . ttTerm) cond
      let Crucible.LLVMPointer blk _ = ptr'
      let invalidate_msg = Map.lookup blk overwritten_allocs
@@ -2330,7 +2330,7 @@ instantiateSetupValue sc s v =
     SetupTuple empty _       -> absurd empty
     SetupSlice empty         -> absurd empty
   where
-    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
+    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
 
 ------------------------------------------------------------------------
 

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

@@ -660,7 +660,7 @@ executePred ::
   OverrideMatcher MIR w ()
 executePred sc cc md tt =
   do s <- OM (use termSub)
-     t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
+     t <- liftIO $ scInstantiate sc s (ttTerm tt)
      p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) t
      addAssume p md
 
@@ -900,7 +900,7 @@ instantiateExtResolveSAWPred ::
   OverrideMatcher MIR md (W4.Pred Sym)
 instantiateExtResolveSAWPred sc cc cond = do
   sub <- OM (use termSub)
-  liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
+  liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
 
 -- | Map the given substitution over all 'SetupTerm' constructors in
 -- the given 'MirPointsTo' value.
@@ -949,7 +949,7 @@ instantiateSetupValue sc s v =
                                            <*> instantiateSetupValue sc s t
                                            <*> instantiateSetupValue sc s f
   where
-    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
+    doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
 
     instantiateSetupEnum :: MirSetupEnum -> IO MirSetupEnum
     instantiateSetupEnum (MirSetupEnumVariant adt variant variantIdx vs) =
@@ -1085,7 +1085,7 @@ learnPred ::
   OverrideMatcher MIR w ()
 learnPred sc cc md prepost t =
   do s <- OM (use termSub)
-     u <- liftIO $ scInstantiateExt sc s t
+     u <- liftIO $ scInstantiate sc s t
      p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) u
      let loc = MS.conditionLoc md
      addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))

saw-central/src/SAWCentral/Proof.hs

@@ -1741,7 +1741,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
                      , showTerm ty
                      ]
                    x' <- scVariable sc x xty
-                   body' <- scInstantiateExt sc (IntMap.singleton (vnIndex nm) x') body
+                   body' <- scInstantiate sc (IntMap.singleton (vnIndex nm) x') body
                    check nenv e' (mkSqt (Prop body'))
 
 passthroughEvidence :: [Evidence] -> IO Evidence
@@ -2017,7 +2017,7 @@ propApply sc rule goal = applyFirst (asPiLists (unProp rule))
                       case IntMap.lookup (vnIndex vn) inst of
                         Nothing ->
                           -- this argument not solved by unification, so make it a goal
-                          do c0 <- scInstantiateExt sc inst tp
+                          do c0 <- scInstantiate sc inst tp
                              mp <- termToMaybeProp sc c0
                              let nm = vnName vn
                              case mp of
@@ -2052,7 +2052,7 @@ tacticIntro sc usernm = Tactic \goal ->
              vn' <- liftIO $ scFreshVarName sc name
              x  <- liftIO $ scVariable sc vn' tp
              tt <- liftIO $ mkTypedTerm sc x
-             body' <- liftIO $ scInstantiateExt sc (IntMap.singleton (vnIndex vn) x) body
+             body' <- liftIO $ scInstantiate sc (IntMap.singleton (vnIndex vn) x) body
              let goal' = goal { goalSequent = mkSqt (Prop body') }
              return (tt, mempty, [goal'], introEvidence vn' tp)
 

saw-core/src/SAWCore/Rewriter.hs

@@ -240,7 +240,7 @@ scMatch sc ctxt pat term =
     check inst (t, n) = do
       --lift $ putStrLn $ "checking: " ++ show (t, n)
       -- apply substitution to the term
-      t' <- lift $ scInstantiateExt sc inst t
+      t' <- lift $ scInstantiate sc inst t
       --lift $ putStrLn $ "t': " ++ show t'
       -- constant-fold nat operations
       -- ensure that it evaluates to the same number
@@ -480,7 +480,7 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
                   -- Define function to substitute the constructor @c@
                   -- in for the old local variable @x@.
                   let subst = IntMap.singleton (vnIndex x) c
-                  let adjust t = scInstantiateExt sc subst t
+                  let adjust t = scInstantiate sc subst t
                   -- Build the list of types of the new context.
                   ctxt2' <- traverse (traverse adjust) ctxt2
                   let ctxt' = ctxt1 ++ argCtx ++ ctxt2'
@@ -523,7 +523,7 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
              case R.asLambda f' of
                Nothing -> scApply sc f' arg
                Just (vn, _, body) ->
-                 scInstantiateExt sc (IntMap.singleton (vnIndex vn) arg) body
+                 scInstantiate sc (IntMap.singleton (vnIndex vn) arg) body
 
 -- | Like 'R.asPiList', but freshen all variables in the context.
 asFreshPiList :: SharedContext -> Term -> IO ([(VarName, Term)], Term)
@@ -535,7 +535,7 @@ asFreshPiList sc t =
          let basename = if vnName x == "_" then "_x" else vnName x
          x' <- scFreshVarName sc basename
          var <- scVariable sc x' t1
-         t2' <- scInstantiateExt sc (IntMap.singleton (vnIndex x) var) t2
+         t2' <- scInstantiate sc (IntMap.singleton (vnIndex x) var) t2
          (ctx, body) <- asFreshPiList sc t2'
          pure ((x', t1) : ctx, body)
 
@@ -692,7 +692,7 @@ termWeightLt t t' =
 -- level, if possible.
 reduceSharedTerm :: SharedContext -> Term -> IO (Maybe Term)
 reduceSharedTerm sc (asBetaRedex -> Just (vn, _, body, arg)) =
-  Just <$> scInstantiateExt sc (IntMap.singleton (vnIndex vn) arg) body
+  Just <$> scInstantiate sc (IntMap.singleton (vnIndex vn) arg) body
 reduceSharedTerm _ (asPairRedex -> Just t) = pure (Just t)
 reduceSharedTerm _ (asRecordRedex -> Just t) = pure (Just t)
 reduceSharedTerm sc (asNatIotaRedex -> Just (f1, f2, n)) =
@@ -767,19 +767,19 @@ rewriteSharedTerm sc ss t0 =
                apply rules t
           | permutative ->
             do
-              t' <- scInstantiateExt sc inst rhs
+              t' <- scInstantiate sc inst rhs
               case termWeightLt t' t of
                 True -> recordAnn annotation >> rewriteAll t' -- keep the result only if it is "smaller"
                 False -> apply rules t
           | shallow ->
             -- do not to further rewriting to the result of a "shallow" rule
             do recordAnn annotation
-               scInstantiateExt sc inst rhs
+               scInstantiate sc inst rhs
           | otherwise ->
             do -- putStrLn "REWRITING:"
                -- print lhs
                recordAnn annotation
-               rewriteAll =<< scInstantiateExt sc inst rhs
+               rewriteAll =<< scInstantiate sc inst rhs
     apply (Right conv : rules) t =
         do -- putStrLn "REWRITING:"
            -- print (Net.toPat conv)
@@ -868,7 +868,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
         Nothing -> apply rules t
         Just inst ->
           do recordAnn (annotation rule)
-             rewriteAll =<< scInstantiateExt sc inst (rhs rule)
+             rewriteAll =<< scInstantiate sc inst (rhs rule)
     apply (Right conv : rules) t =
       case runConversion conv t of
         Nothing -> apply rules t

saw-core/src/SAWCore/SCTypeCheck.hs

@@ -507,7 +507,7 @@ applyPiTyped err fun_tp arg =
   ensurePiType err fun_tp >>= \(nm, arg_tp, ret_tp) ->
   do checkSubtype arg arg_tp
      let sub = IntMap.singleton (vnIndex nm) (SC.rawTerm arg)
-     liftTCM scInstantiateExt sub ret_tp
+     liftTCM scInstantiate sub ret_tp
 
 -- | Ensure that a 'Term' matches a recognizer function, normalizing if
 -- necessary; otherwise throw the supplied 'TCError'
@@ -562,7 +562,7 @@ isSubtype (unwrapTermF -> Pi x1 a1 b1) (unwrapTermF -> Pi x2 a2 b2)
     do conv1 <- areConvertible a1 a2
        var1 <- liftTCM scVariable x1 a1
        let sub = IntMap.singleton (vnIndex x2) var1
-       b2' <- liftTCM scInstantiateExt sub b2
+       b2' <- liftTCM scInstantiate sub b2
        conv2 <- withVar x1 a1 (isSubtype b1 b2')
        pure (conv1 && conv2)
 isSubtype (asSort -> Just s1) (asSort -> Just s2) | s1 <= s2 = return True