Merge pull request #1396 from GaloisInc/newtype-fix

Newtype fix

cabal.GHC-8.10.3.config

@@ -267,7 +267,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

cabal.GHC-8.10.4.config

@@ -277,7 +277,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

cabal.GHC-8.8.4.config

@@ -269,7 +269,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.30,
              simple-sendfile +allow-bsd,
-             any.simple-smt ==0.9.5,
+             any.simple-smt ==0.9.7,
              any.smallcheck ==1.2.1,
              any.split ==0.2.3.4,
              any.splitmix ==0.1.0.3,

cryptol-saw-core/css/Main.hs

@@ -95,7 +95,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do
     modEnv <- CM.initialModuleEnv
     let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
     (e,warn) <-
-      SMT.withSolver (meSolverConfig modEnv) $ \s ->
+      SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
       CM.loadModuleByPath inputModule (minp s)
     mapM_ (print . pp) warn
     case e of
@@ -136,7 +136,7 @@ extractCryptol sc modEnv input = do
       Right x -> return x
   let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
   (exprResult, exprWarnings) <-
-    SMT.withSolver (meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
     CM.checkExpr pexpr (minp s)
   mapM_ (print . pp) exprWarnings
   ((_, expr, schema), _modEnv') <-

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -890,21 +890,20 @@ importExpr sc env expr =
           do e' <- importExpr sc env e
              let t = fastTypeOf (envC env) e
              case C.tIsTuple t of
-               Just ts ->
-                 do scTupleSelector sc e' (i+1) (length ts)
-               Nothing ->
-                 do f <- mapTupleSelector sc env i t
-                    scApply sc f e'
+               Just ts -> scTupleSelector sc e' (i+1) (length ts)
+               Nothing -> panic "importExpr" ["invalid tuple selector", show i, pretty t]
         C.RecordSel x _ ->
           do e' <- importExpr sc env e
              let t = fastTypeOf (envC env) e
-             case C.tIsRec t of
-               Just fm ->
+             case C.tNoUser t of
+               C.TRec fm ->
                  do i <- the (elemIndex x (map fst (C.canonicalFields fm)))
                     scTupleSelector sc e' (i+1) (length (C.canonicalFields fm))
-               Nothing ->
-                 do f <- mapRecordSelector sc env x t
-                    scApply sc f e'
+               C.TNewtype nt _args ->
+                 do let fs = C.ntFields nt
+                    i <- the (elemIndex x (map fst (C.canonicalFields fs)))
+                    scTupleSelector sc e' (i+1) (length (C.canonicalFields fs))
+               _ -> panic "importExpr" ["invalid record selector", pretty x, pretty t]
         C.ListSel i _maybeLen ->
           do let t = fastTypeOf (envC env) e
              (n, a) <-
@@ -936,7 +935,7 @@ importExpr sc env expr =
              e2' <- importExpr sc env e2
              let t1 = fastTypeOf (envC env) e1
              case C.tIsRec t1 of
-               Nothing -> panic "importExpr" ["ESet/TupleSel: not a tuple type"]
+               Nothing -> panic "importExpr" ["ESet/RecordSel: not a record type"]
                Just tm ->
                  do i <- the (elemIndex x (map fst (C.canonicalFields tm)))
                     ts' <- traverse (importType sc env . snd) (C.canonicalFields tm)
@@ -1110,62 +1109,6 @@ importExpr' sc env schema expr =
          expr' <- importExpr sc env expr
          coerceTerm sc env t1 t2 expr'
 
-mapTupleSelector :: SharedContext -> Env -> Int -> C.Type -> IO Term
-mapTupleSelector sc env i = fmap fst . go
-  where
-    go :: C.Type -> IO (Term, C.Type)
-    go t =
-      case C.tNoUser t of
-        (C.tIsSeq -> Just (n, a)) -> do
-          (f, b) <- go a
-          a' <- importType sc env a
-          b' <- importType sc env b
-          n' <- importType sc env n
-          g <- scGlobalApply sc "Cryptol.seqMap" [a', b', n', f]
-          return (g, C.tSeq n b)
-        (C.tIsFun -> Just (n, a)) -> do
-          (f, b) <- go a
-          a' <- importType sc env a
-          b' <- importType sc env b
-          n' <- importType sc env n
-          g <- scGlobalApply sc "Cryptol.compose" [n', a', b', f]
-          return (g, C.tFun n b)
-        (C.tIsTuple -> Just ts) -> do
-          x <- scLocalVar sc 0
-          y <- scTupleSelector sc x (i+1) (length ts)
-          t' <- importType sc env t
-          f <- scLambda sc "x" t' y
-          return (f, ts !! i)
-        _ -> panic "importExpr" ["invalid tuple selector", show i, show t]
-
-mapRecordSelector :: SharedContext -> Env -> C.Ident -> C.Type -> IO Term
-mapRecordSelector sc env i = fmap fst . go
-  where
-    go :: C.Type -> IO (Term, C.Type)
-    go t =
-      case C.tNoUser t of
-        (C.tIsSeq -> Just (n, a)) ->
-          do (f, b) <- go a
-             a' <- importType sc env a
-             b' <- importType sc env b
-             n' <- importType sc env n
-             g <- scGlobalApply sc "Cryptol.seqMap" [a', b', n', f]
-             return (g, C.tSeq n b)
-        (C.tIsFun -> Just (n, a)) ->
-          do (f, b) <- go a
-             a' <- importType sc env a
-             b' <- importType sc env b
-             n' <- importType sc env n
-             g <- scGlobalApply sc "Cryptol.compose" [n', a', b', f]
-             return (g, C.tFun n b)
-        (C.tIsRec -> Just tm) | Just k <- elemIndex i (map fst (C.canonicalFields tm)) ->
-          do x <- scLocalVar sc 0
-             y <- scTupleSelector sc x (k+1) (length (C.canonicalFields tm))
-             t' <- importType sc env t
-             f <- scLambda sc "x" t' y
-             return (f, snd (C.canonicalFields tm !! k))
-        _ -> panic "importExpr" ["invalid record selector", show i, show t]
-
 tupleUpdate :: SharedContext -> Term -> Int -> [Term] -> IO Term
 tupleUpdate _ f 0 [_] = return f
 tupleUpdate sc f 0 (a : ts) =

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -493,7 +493,7 @@ resolveIdentifier env nm =
   nameEnv = getNamingEnv env
 
   doResolve pnm =
-    SMT.withSolver (meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
     do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
        (res, _ws) <- MM.runModuleM (minp s) $
           MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm))
@@ -653,7 +653,7 @@ liftModuleM ::
   ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
 liftModuleM env m =
   do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
-     SMT.withSolver (meSolverConfig env) $ \s ->
+     SMT.withSolver (return ()) (meSolverConfig env) $ \s ->
        MM.runModuleM (minp s) m >>= moduleCmdResult
 
 defaultEvalOpts :: E.EvalOpts

saw-remote-api/src/SAWServer/CryptolExpression.hs

@@ -63,7 +63,7 @@ getTypedTermOfCExp fileReader sc cenv expr =
      let env = eModuleEnv cenv
      let minp = ModuleInput True (pure defaultEvalOpts) B.readFile env
      mres <-
-       withSolver (meSolverConfig env) $ \s ->
+       withSolver (return ()) (meSolverConfig env) $ \s ->
        runModuleM (minp s) $
        do npe <- interactive (noPat expr) -- eliminate patterns
 

saw-remote-api/src/SAWServer/ProofScript.hs

@@ -35,7 +35,7 @@ import qualified SAWScript.Builtins as SB
 import qualified SAWScript.Value as SV
 import qualified SAWScript.Proof as PF
 import SAWServer
-    ( ServerVal(VTerm, VSimpset),
+    ( ServerVal(VSimpset),
       ServerName,
       SAWState,
       setServerVal,
@@ -49,9 +49,8 @@ import SAWServer.OK ( OK, ok )
 import SAWServer.TopLevel ( tl )
 import Verifier.SAW.FiniteValue (FirstOrderValue(..))
 import Verifier.SAW.Name (ecName, toShortName)
-import Verifier.SAW.Rewriter (addSimp, emptySimpset)
+import Verifier.SAW.Rewriter (emptySimpset)
 import Verifier.SAW.TermNet (merge)
-import Verifier.SAW.TypedTerm (TypedTerm(..))
 
 data Prover
   = RME

saw-script.cabal

@@ -216,13 +216,13 @@ executable saw
     , cryptol-saw-core
     , aig
 
-  GHC-options: -O2 -Wall -Werror -fno-ignore-asserts -fno-spec-constr-count
+  GHC-options: -O2 -Wall -Werror -threaded -fno-ignore-asserts -fno-spec-constr-count
 
 test-suite integration_tests
   type: exitcode-stdio-1.0
   hs-source-dirs: intTests
 
-  ghc-options: -Wall
+  ghc-options: -Wall -threaded
   default-language: Haskell2010
 
   main-is: IntegrationTest.hs

src/SAWScript/AutoMatch/Cryptol.hs

@@ -36,7 +36,7 @@ getDeclsCryptol path = do
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
    (result, warnings) <-
-     SMT.withSolver (meSolverConfig modEnv) $ \s ->
+     SMT.withSolver (return ()) (meSolverConfig modEnv) $ \s ->
      M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty

src/SAWScript/Builtins.hs

@@ -1311,7 +1311,7 @@ defaultTypedTerm :: Options -> SharedContext -> C.SolverConfig -> TypedTerm -> I
 defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm)
   | null (C.sVars schema) = return tt
   | otherwise = do
-  mdefault <- C.withSolver cfg (\s -> C.defaultReplExpr s undefined schema)
+  mdefault <- C.withSolver (return ()) cfg (\s -> C.defaultReplExpr s undefined schema)
   let inst = do (soln, _) <- mdefault
                 mapM (`lookup` soln) (C.sVars schema)
   case inst of