Merge pull request #1018 from GaloisInc/text-lambda

Update submodules and adapt to GaloisInc/saw-core#119.

src/SAWScript/Builtins.hs

@@ -41,6 +41,7 @@ import qualified Data.Set as Set
 import Data.Maybe
 import Data.Time.Clock
 import Data.Typeable
+import Data.Text (Text)
 import qualified Data.Text as Text
 import System.Directory
 import qualified System.Environment
@@ -578,7 +579,7 @@ goal_apply (Theorem (Prop rule) _stats) =
                          return ((), ProofState (newgoals ++ goals') concl stats timeout)
          applyFirst (asPiLists rule)
   where
-    asPiLists :: Term -> [([(String, Term)], Term)]
+    asPiLists :: Term -> [([(Text, Term)], Term)]
     asPiLists t =
       case asPi t of
         Nothing -> [([], t)]
@@ -608,7 +609,7 @@ goal_intro s =
       case asPi (unProp (goalProp goal)) of
         Nothing -> fail "goal_intro failed: not a pi type"
         Just (nm, tp, body) ->
-          do let name = if null s then nm else s
+          do let name = if null s then Text.unpack nm else s
              sc <- SV.getSharedContext
              x <- io $ scFreshGlobal sc name tp
              tt <- io $ mkTypedTerm sc x
@@ -983,7 +984,7 @@ w4AbcVerilog _unints sc _hashcons g =
               else do bits <- reverse <$> parseAigerCex cexText
                       let goalArgs' = reverse goalArgs
                           argTys = map snd goalArgs'
-                          argNms = map fst goalArgs'
+                          argNms = map (Text.unpack . fst) goalArgs'
                       finiteArgTys <- traverse (asFiniteType sc) argTys
                       case liftCexBB finiteArgTys bits of
                         Left parseErr -> fail parseErr

src/SAWScript/ImportAIG.hs

@@ -6,6 +6,7 @@ Maintainer  : huffman
 Stability   : provisional
 -}
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
@@ -25,6 +26,7 @@ import Control.Exception
 import Control.Monad
 import Control.Monad.State.Strict
 import Control.Monad.Trans.Except
+import Data.Text (Text)
 import qualified Data.Vector as V
 import Prettyprinter
 
@@ -60,7 +62,7 @@ bitblastSharedTerm sc v (asBitvectorType -> Just w) = do
   modify (V.++ inputs)
 bitblastSharedTerm _ _ tp = throwTP $ show $
   vcat
-  [ pretty "Could not parse AIG input type:"
+  [ "Could not parse AIG input type:"
   , indent 2 (ppTerm defaultPPOpts tp)
   ]
 
@@ -149,7 +151,7 @@ translateNetwork :: AIG.IsAIG l g
                  -> SharedContext    -- ^ Context to build in term.
                  -> g x              -- ^ Network to bitblast
                  -> [l x]            -- ^ Outputs for network.
-                 -> [(String, Term)] -- ^ Expected types
+                 -> [(Text, Term)]   -- ^ Expected types
                  -> Term             -- ^ Expected output type.
                  -> ExceptT String IO Term
 translateNetwork opts sc ntk outputLits args resultType = do

src/SAWScript/Prover/MRSolver.hs

@@ -13,6 +13,7 @@ import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Except
 import Data.Semigroup
+import qualified Data.Text as Text
 
 import Prettyprinter
 
@@ -612,7 +613,7 @@ askMRSolver sc smt_conf timeout t1 t2 =
        flip evalStateT init_st $ runExceptT $
        do mrSolveEq (Type tp1) (Type tp2)
           let (pi_args, ret_tp) = asPiList tp1
-          vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal x x_tp) pi_args
+          vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal (Text.unpack x) x_tp) pi_args
           case asCompMApp ret_tp of
             Just _ -> return ()
             Nothing -> throwError (NotCompFunType tp1)

src/SAWScript/Prover/RME.hs

@@ -1,6 +1,7 @@
 module SAWScript.Prover.RME where
 
 import qualified Data.Map as Map
+import qualified Data.Text as Text
 
 import qualified Data.RME as RME
 
@@ -25,7 +26,7 @@ proveRME sc goal =
      t <- bindAllExts sc t0 >>= rewriteEqs sc
      tp <- scWhnf sc =<< scTypeOf sc t
      let (args, _) = asPiList tp
-         argNames = map fst args
+         argNames = map (Text.unpack . fst) args
      RME.withBitBlastedPred sc Map.empty t $ \lit0 shapes ->
        let lit = RME.compl lit0
            stats = solverStats "RME" (scSharedSize t0)

src/SAWScript/Prover/SBV.hs

@@ -11,6 +11,7 @@ import           Data.Maybe
 import           Data.Map ( Map )
 import qualified Data.Map as Map
 import           Data.Set ( Set )
+import qualified Data.Text as Text
 import qualified Data.Vector as V
 import           Control.Monad
 
@@ -65,7 +66,7 @@ proveUnintSBV conf unintSet timeout sc term =
 
        SBV.Satisfiable {} ->
          do let dict = SBV.getModelDictionary r
-                r'   = getLabels labels dict argNames
+                r'   = getLabels labels dict (map Text.unpack argNames)
             return (r', stats)
 
        SBV.SatExtField {} -> fail "Prover returned model in extension field"