Fix a bug where the symbolic backends did not have newtype constructors

in scope.  Also, demote the `NewtypeEnv` to a type synonym, as the
newtype was just annoying.

cryptol-remote-api/src/CryptolServer/EvalExpr.hs

@@ -44,7 +44,7 @@ evalExpression' e =
             let su = listParamSubst tys
             let theType = apSubst su (sType schema)
             tenv  <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
-            ntEnv <- E.NewtypeEnv . loadedNewtypes <$> getModuleEnv
+            ntEnv <- loadedNewtypes <$> getModuleEnv
             let tval = E.evalValType ntEnv tenv theType
             res <- runModuleCmd (evalExpr checked)
             val <- observe $ readBack tval res

src/Cryptol/Eval.hs

@@ -27,6 +27,7 @@ module Cryptol.Eval (
   , emptyEnv
   , evalExpr
   , evalDecls
+  , evalNewtypeDecls
   , evalSel
   , evalSetSel
   , EvalError(..)

src/Cryptol/Eval/Reference.lhs

@@ -40,7 +40,7 @@
 > import qualified Cryptol.Backend.FloatHelpers as FP
 > import Cryptol.Backend.Monad (EvalError(..))
 > import Cryptol.Eval.Type
->   (TValue(..), isTBit, evalValType, evalNumType, NewtypeEnv(..), TypeEnv, bindTypeVar)
+>   (TValue(..), isTBit, evalValType, evalNumType, NewtypeEnv, TypeEnv, bindTypeVar)
 > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
 > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
 > import Cryptol.Utils.Panic (panic)
@@ -1710,7 +1710,7 @@ running the reference evaluator on an expression.
 > evaluate expr minp = return (Right (val, modEnv), [])
 >   where
 >     modEnv = M.minpModuleEnv minp
->     ntEnv  = NewtypeEnv (M.loadedNewtypes modEnv)
+>     ntEnv  = M.loadedNewtypes modEnv
 >     extDgs = concatMap mDecls (M.loadedModules modEnv)
 >     env    = foldl (evalDeclGroup ntEnv) mempty extDgs
 >     val    = evalExpr ntEnv env expr

src/Cryptol/Eval/Type.hs

@@ -107,8 +107,7 @@ instance Semigroup TypeEnv where
   l <> r = TypeEnv
     { envTypeMap  = IntMap.union (envTypeMap l) (envTypeMap r) }
 
-newtype NewtypeEnv =
-  NewtypeEnv { newtypeEnv :: Map.Map Name Newtype }
+type NewtypeEnv = Map.Map Name Newtype
 
 lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue)
 lookupTypeVar tv env = IntMap.lookup (tvUnique tv) (envTypeMap env)
@@ -143,7 +142,7 @@ evalType ntEnv env ty =
         (TCNum n, [])   -> Left $ Nat n
         (TCInf, [])     -> Left $ Inf
         (TCNewtype u@(UserTC nm _),vs) ->
-            case Map.lookup nm (newtypeEnv ntEnv) of
+            case Map.lookup nm ntEnv of
               Just nt ->
                 let vs' = map (evalType ntEnv env) vs
                  in Right $ TVNewtype u vs' $ evalNewtypeBody ntEnv env nt vs'

src/Cryptol/ModuleSystem/Base.hs

@@ -26,7 +26,6 @@ import Cryptol.ModuleSystem.Env (lookupModule
                                 , ModContext(..)
                                 , ModulePath(..), modulePathLabel)
 import qualified Cryptol.Eval                 as E
-import qualified Cryptol.Eval.Type            as E
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.Eval.Concrete (Concrete(..))
 import qualified Cryptol.ModuleSystem.NamingEnv as R
@@ -208,7 +207,7 @@ doLoadModule quiet isrc path fp pm0 =
      callStacks <- getCallStacks
      let ?callStacks = callStacks
      nts <- getNewtypes
-     let ?ntEnv = E.NewtypeEnv nts
+     let ?ntEnv = nts
      unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)
      loadedModule path fp tcm
 
@@ -574,7 +573,7 @@ evalExpr e = do
   callStacks <- getCallStacks
   let ?callStacks = callStacks
   nts <- getNewtypes
-  let ?ntEnv = E.NewtypeEnv nts
+  let ?ntEnv = nts
 
   io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)
 
@@ -589,7 +588,7 @@ evalDecls dgs = do
   callStacks <- getCallStacks
   let ?callStacks = callStacks
   nts <- getNewtypes
-  let ?ntEnv = E.NewtypeEnv nts
+  let ?ntEnv = nts
 
   deEnv' <- io $ E.runEval mempty (E.evalDecls Concrete dgs env')
   let denv' = denv { deDecls = deDecls denv ++ dgs

src/Cryptol/REPL/Command.hs

@@ -364,7 +364,7 @@ dumpTestsCmd outFile str pos fnm =
      testNum <- getKnownUser "tests" :: REPL Int
      g <- io newTFGen
      tenv <- E.envTypes . M.deEnv <$> getDynEnv
-     ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv
+     ntEnv <- M.loadedNewtypes <$> getModuleEnv
      let tyv = E.evalValType ntEnv tenv ty
      gens <-
        case TestR.dumpableType tyv of
@@ -428,7 +428,7 @@ qcExpr ::
 qcExpr qcMode exprDoc texpr schema =
   do (val,ty) <- replEvalCheckedExpr texpr schema
      testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"
-     ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv
+     ntEnv <- M.loadedNewtypes <$> getModuleEnv
      tenv <- E.envTypes . M.deEnv <$> getDynEnv
      let tyv = E.evalValType ntEnv tenv ty
      percentRef <- io $ newIORef Nothing
@@ -1740,7 +1740,7 @@ replEvalCheckedExpr def sig =
      whenDebug (rPutStrLn (dump def1))
 
      tenv <- E.envTypes . M.deEnv <$> getDynEnv
-     ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv
+     ntEnv <- M.loadedNewtypes <$> getModuleEnv
      let tyv = E.evalValType ntEnv tenv ty
 
      -- add "it" to the namespace via a new declaration

src/Cryptol/Symbolic/SBV.hs

@@ -56,7 +56,6 @@ import qualified Cryptol.Backend.FloatHelpers as FH
 
 import qualified Cryptol.Eval as Eval
 import qualified Cryptol.Eval.Concrete as Concrete
-import qualified Cryptol.Eval.Type as Eval
 import qualified Cryptol.Eval.Value as Eval
 import           Cryptol.Eval.SBV
 import           Cryptol.Parser.Position (emptyRange)
@@ -314,7 +313,7 @@ prepareQuery evo ProverCommand{..} =
      getEOpts <- M.getEvalOptsAction
 
      nts <- M.getNewtypes
-     let ?ntEnv = Eval.NewtypeEnv nts
+     let ?ntEnv = nts
 
      -- The `addAsm` function is used to combine assumptions that
      -- arise from the types of symbolic variables (e.g. Z n values
@@ -348,7 +347,8 @@ prepareQuery evo ProverCommand{..} =
                  -- evaluation environment, then we compute the value, finally
                  -- we apply it to the symbolic inputs.
                  (safety,b) <- doSBVEval $
-                     do env <- Eval.evalDecls sym extDgs mempty
+                     do env <- Eval.evalDecls sym extDgs =<<
+                                 Eval.evalNewtypeDecls sym nts mempty
                         v <- Eval.evalExpr sym env pcExpr
                         appliedVal <- foldM (Eval.fromVFun sym) v args
                         case pcQueryType of

src/Cryptol/Symbolic/What4.hs

@@ -60,7 +60,6 @@ import qualified Cryptol.Backend.What4.SFloat as W4
 
 import qualified Cryptol.Eval as Eval
 import qualified Cryptol.Eval.Concrete as Concrete
-import qualified Cryptol.Eval.Type as Eval
 import qualified Cryptol.Eval.Value as Eval
 import           Cryptol.Eval.What4
 import           Cryptol.Parser.Position (emptyRange)
@@ -237,8 +236,7 @@ prepareQuery ::
                        ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym)
                )
 prepareQuery sym ProverCommand { .. } = do
-  nts <- M.getNewtypes
-  let ntEnv = Eval.NewtypeEnv nts
+  ntEnv <- M.getNewtypes
   case predArgTypes ntEnv pcQueryType pcSchema of
     Left msg -> pure (Left msg)
     Right ts ->
@@ -290,7 +288,9 @@ prepareQuery sym ProverCommand { .. } = do
        let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
 
        doW4Eval (w4 sym)
-         do env <- Eval.evalDecls sym extDgs mempty
+         do env <- Eval.evalDecls sym extDgs =<<
+                     Eval.evalNewtypeDecls sym ntEnv mempty
+
             v   <- Eval.evalExpr  sym env    pcExpr
             appliedVal <-
               foldM (Eval.fromVFun sym) v (map (pure . varShapeToValue sym) args)