Reimplement extract_uninterp via the new term model.

Actually pass through the replacement value tuples.

This currently fails because `mkTypedTerm` doesn't know what
to do with `Cryptol.Num` values, etc.

CF #718

Make `extract_uninterp2` return tuples containing only the
Cryptol-value arguments to an uninterpreted function.

saw-core/src/Verifier/SAW/Simulator/TermModel.hs

@@ -20,11 +20,13 @@ module Verifier.SAW.Simulator.TermModel
        , VExtra(..)
        , readBackValue, readBackTValue
        , normalizeSharedTerm
+       , extractUninterp
        ) where
 
 import Control.Monad
 import Control.Monad.Fix
 import Data.IORef
+import Data.Maybe (fromMaybe)
 import qualified Data.Vector as V
 import Data.Map (Map)
 import qualified Data.Map as Map

src/SAWScript/Builtins.hs

@@ -540,6 +540,57 @@ goal_eval unints =
      prop' <- io (evalProp sc unintSet (goalProp goal))
      return (prop', EvalEvidence unintSet)
 
+extract_uninterp2 :: [String] -> TypedTerm -> TopLevel (TypedTerm, [(String,[(TypedTerm,TypedTerm)])])
+extract_uninterp2 unints tt =
+  do sc <- getSharedContext
+     idxs <- mapM (resolveName sc) unints
+     let unintSet = Set.fromList idxs
+     mmap <- io (scGetModuleMap sc)
+     (tm, repls) <- io (TM.extractUninterp sc mmap mempty mempty unintSet (ttTerm tt))
+     tt' <- io (mkTypedTerm sc tm)
+
+     let f = traverse $ \(ec,vs) ->
+               do ectm <- scExtCns sc ec
+                  vs'  <- filterCryTerms sc vs
+                  pure (ectm, vs')
+     repls' <- io (traverse f repls)
+
+     -- printOutLnTop Info "====== Replacement values ======"
+     -- forM_ (zip unints idxs) $ \(nm,idx) ->
+     --   do printOutLnTop Info ("== Values for " ++ nm ++ " ==")
+     --      let ls = fromMaybe [] (Map.lookup idx repls')
+     --      forM_ ls $ \(e,vs) ->
+     --        do es  <- show_term e
+     --           vss <- show_term vs
+     --           printOutLnTop Info (unwords ["output:", es, "inputs:", vss])
+     -- printOutLnTop Info "====== End Replacement values ======"
+
+     replList <- io $
+        forM (zip unints idxs) $ \(nm,idx) ->
+           do let ls = fromMaybe [] (Map.lookup idx repls')
+              xs <- forM ls $ \(e,vs) ->
+                      do e'  <- mkTypedTerm sc e
+                         vs' <- tupleTypedTerm sc vs
+                         pure (e',vs')
+              pure (nm,xs)
+
+     pure (tt', replList)
+
+filterCryTerms :: SharedContext -> [Term] -> IO [TypedTerm]
+filterCryTerms sc = loop
+  where
+  loop [] = pure []
+  loop (x:xs) =
+    do tp <- Cryptol.scCryptolType sc =<< scTypeOf sc x
+       case tp of
+         Just (Right cty) ->
+           do let x' = TypedTerm (TypedTermSchema (C.tMono cty)) x
+              xs' <- loop xs
+              pure (x':xs')
+
+         _ -> loop xs
+
+
 beta_reduce_goal :: ProofScript ()
 beta_reduce_goal =
   execTactic $ tacticChange $ \goal ->

src/SAWScript/Interpreter.hs

@@ -907,6 +907,12 @@ primitives = Map.fromList
     Experimental
     [ "Apply Cryptol defaulting rules to the given term." ]
 
+  , prim "extract_uninterp2" "[String] -> Term -> TopLevel (Term, [(String,[(Term, Term)])])"
+    (pureVal extract_uninterp2)
+    Experimental
+    [ "Docs TODO!!"
+    ]
+
   , prim "sbv_uninterpreted"   "String -> Term -> TopLevel Uninterp"
     (pureVal sbvUninterpreted)
     Deprecated