cryptol 3.0.0 → 3.1.0

raw patch · 80 files changed

+2963/−1254 lines, 80 filesdep ~sbvdep ~what4PVP ok

version bump matches the API change (PVP)

Dependency ranges changed: sbv, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +48/−2
• LICENSE +1/−1
• cryptol.cabal +5/−4
• cryptol/CheckExercises.hs +2/−1
• lib/Cryptol.cry +19/−0
• src/Cryptol/Backend/FFI.hs +27/−19
• src/Cryptol/Backend/FFI/Error.hs +6/−4
• src/Cryptol/Backend/Monad.hs +9/−3
• src/Cryptol/Backend/SeqMap.hs +30/−19
• src/Cryptol/Eval.hs +108/−52
• src/Cryptol/Eval/Concrete.hs +32/−2
• src/Cryptol/Eval/FFI.hs +12/−11
• src/Cryptol/Eval/Generic.hs +22/−38
• src/Cryptol/Eval/Reference.lhs +82/−45
• src/Cryptol/Eval/Type.hs +44/−18
• src/Cryptol/Eval/Value.hs +100/−12
• src/Cryptol/IR/FreeVars.hs +24/−5
• src/Cryptol/IR/TraverseNames.hs +47/−34
• src/Cryptol/ModuleSystem/Base.hs +53/−39
• src/Cryptol/ModuleSystem/Binds.hs +36/−5
• src/Cryptol/ModuleSystem/Env.hs +50/−26
• src/Cryptol/ModuleSystem/Exports.hs +10/−3
• src/Cryptol/ModuleSystem/Interface.hs +19/−19
• src/Cryptol/ModuleSystem/Monad.hs +5/−2
• src/Cryptol/ModuleSystem/Name.hs +19/−6
• src/Cryptol/ModuleSystem/NamingEnv.hs +27/−41
• src/Cryptol/ModuleSystem/NamingEnv/Types.hs +43/−0
• src/Cryptol/ModuleSystem/Renamer.hs +67/−44
• src/Cryptol/ModuleSystem/Renamer/Error.hs +9/−1
• src/Cryptol/ModuleSystem/Renamer/Imports.hs +5/−4
• src/Cryptol/Parser.y +90/−37
• src/Cryptol/Parser/AST.hs +113/−6
• src/Cryptol/Parser/ExpandPropGuards.hs +39/−35
• src/Cryptol/Parser/Layout.hs +1/−0
• src/Cryptol/Parser/Lexer.x +3/−0
• src/Cryptol/Parser/Name.hs +11/−0
• src/Cryptol/Parser/Names.hs +55/−17
• src/Cryptol/Parser/NoInclude.hs +1/−0
• src/Cryptol/Parser/NoPat.hs +119/−49
• src/Cryptol/Parser/ParserUtils.hs +126/−19
• src/Cryptol/Parser/Token.hs +3/−0
• src/Cryptol/REPL/Browse.hs +11/−9
• src/Cryptol/REPL/Command.hs +6/−2
• src/Cryptol/REPL/Help.hs +62/−37
• src/Cryptol/REPL/Monad.hs +41/−0
• src/Cryptol/Symbolic.hs +76/−11
• src/Cryptol/Symbolic/SBV.hs +16/−3
• src/Cryptol/Symbolic/What4.hs +5/−2
• src/Cryptol/Testing/Random.hs +98/−11
• src/Cryptol/Transform/MonoValues.hs +19/−9
• src/Cryptol/Transform/Specialize.hs +9/−4
• src/Cryptol/TypeCheck.hs +1/−1
• src/Cryptol/TypeCheck/AST.hs +53/−17
• src/Cryptol/TypeCheck/Error.hs +69/−3
• src/Cryptol/TypeCheck/Infer.hs +235/−81
• src/Cryptol/TypeCheck/Instantiate.hs +22/−1
• src/Cryptol/TypeCheck/Interface.hs +4/−5
• src/Cryptol/TypeCheck/Kind.hs +93/−35
• src/Cryptol/TypeCheck/Module.hs +111/−44
• src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +41/−29
• src/Cryptol/TypeCheck/ModuleInstance.hs +54/−32
• src/Cryptol/TypeCheck/Monad.hs +33/−49
• src/Cryptol/TypeCheck/Parseable.hs +12/−1
• src/Cryptol/TypeCheck/Sanity.hs +94/−26
• src/Cryptol/TypeCheck/SimpType.hs +6/−6
• src/Cryptol/TypeCheck/Solver/Class.hs +16/−16
• src/Cryptol/TypeCheck/Solver/SMT.hs +1/−1
• src/Cryptol/TypeCheck/Solver/Selector.hs +12/−8
• src/Cryptol/TypeCheck/Solver/Utils.hs +3/−3
• src/Cryptol/TypeCheck/Subst.hs +36/−16
• src/Cryptol/TypeCheck/TCon.hs +0/−21
• src/Cryptol/TypeCheck/Type.hs +125/−104
• src/Cryptol/TypeCheck/TypeMap.hs +9/−9
• src/Cryptol/TypeCheck/TypeOf.hs +16/−3
• src/Cryptol/TypeCheck/TypePat.hs +0/−6
• src/Cryptol/TypeCheck/Unify.hs +4/−4
• src/Cryptol/Utils/Ident.hs +24/−7
• src/Cryptol/Utils/PP.hs +10/−9
• src/Cryptol/Utils/RecordMap.hs +4/−3
• src/Cryptol/Version.hs +10/−3

@@ -1,3 +1,49 @@+# 3.1.0 -- 2024-02-05++## Language changes++* Cryptol now supports *enum* declarations. An enum is a named typed which is+  defined by one or more constructors. Enums correspond to the notion of+  algebraic data types, which are commonly found in other programming+  languages.  See the [manual+  section](https://galoisinc.github.io/cryptol/master/TypeDeclarations.html#enums)+  for more information.++* Add two enum declarations to the Cryptol standard library:++  ```+  enum Option a = None | Some a++  enum Result t e = Ok t | Err e+  ```++  These types are useful for representing optional values (`Option`) or values+  that may fail in some way (`Result`).++* `foreign` functions can now have an optional Cryptol implementation, which by+  default is used when the foreign implementation cannot be found, or if the FFI+  is unavailable. The `:set evalForeign` REPL option controls this behavior.++## Bug fixes++* Fixed #1455, making anything in scope of the functor in scope at the REPL as+  well when an instantiation of the functor is loaded and focused, design+  choice (3) on the ticket.  In particular, the prelude will be in scope.++* Fix #1578, which caused `parmap` to crash when evaluated on certain types of+  sequences.++* Closed issues #813, #1237, #1397, #1446, #1486, #1492, #1495, #1537,+  #1538, #1542, #1544, #1548, #1551, #1552, #1554, #1556, #1561, #1562, #1566,+  #1567, #1569, #1571, #1584, #1588, #1590, #1598, #1599, #1604, #1605, #1606,+  #1607, #1609, #1610, #1611, #1612, #1613, #1615, #1616, #1617, #1618, and+  #1619.++* Merged pull requests #1429, #1512, #1534, #1535, #1536, #1540, #1541, #1543,+  #1547, #1549, #1550, #1555, #1557, #1558, #1559, #1564, #1565, #1568, #1570,+  #1572, #1573, #1577, #1579, #1580, #1583, #1585, #1586, #1592, #1600, #1601,+  and #1602.+ # 3.0.0 -- 2023-06-26  ## Language changes@@ -22,11 +68,11 @@  * Declarations may now use *numeric constraint guards*.   This is a feature   that allows a function to behave differently depending on its numeric-  type parameters.  See the [manual section](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards))+  type parameters.  See this [manual section](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards)   for more information.  * The foreign function interface (FFI) has been added, which allows Cryptol to-  call functions written in C. See the [manual section](https://galoisinc.github.io/cryptol/master/FFI.html)+  call functions written in C. See this [manual section](https://galoisinc.github.io/cryptol/master/FFI.html)   for more information.  * The unary `-` operator now has the same precedence as binary `-`, meaning

@@ -1,4 +1,4 @@-Copyright (c) 2013-2020 Galois Inc.+Copyright (c) 2013-2023 Galois Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             3.0.0+Version:             3.1.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD-3-Clause@@ -27,7 +27,7 @@   type:     git   location: https://github.com/GaloisInc/cryptol.git   -- add a tag on release branches-  tag:      3.0.0+  tag:      3.1.0   flag static@@ -74,7 +74,7 @@                        prettyprinter     >= 1.7.0,                        pretty-show,                        process           >= 1.2,-                       sbv               >= 9.1 && < 10.2,+                       sbv               >= 9.1 && < 10.3,                        simple-smt        >= 0.9.7,                        stm               >= 2.4,                        strict,@@ -85,7 +85,7 @@                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.4 && < 1.5+                       what4             >= 1.4 && < 1.6    if impl(ghc >= 9.0)     build-depends:     ghc-bignum        >= 1.0 && < 1.4@@ -141,6 +141,7 @@                        Cryptol.ModuleSystem.Name,                        Cryptol.ModuleSystem.Names,                        Cryptol.ModuleSystem.NamingEnv,+                       Cryptol.ModuleSystem.NamingEnv.Types,                        Cryptol.ModuleSystem.Binds                        Cryptol.ModuleSystem.Exports,                        Cryptol.ModuleSystem.Renamer,

@@ -5,7 +5,8 @@  module Main(main) where -import Control.Monad.State+import Control.Monad (forM_, when)+import Control.Monad.State (State, execState, gets, modify, modify') import Options.Applicative import Data.Char (isSpace, isAlpha) import Data.Foldable (traverse_)

@@ -633,6 +633,25 @@ (>=$) : {a} (SignedCmp a) => a -> a -> Bit x >=$ y = ~(x <$ y) +// The Option and Result types ------------------------------------++/**+ * The 'Option a' type represents an optional value. Every 'Option a' value is+ * either 'Some' and contains a value of type 'a', or 'None' and does not. Among+ * other uses, optional values are useful for modeling return values for partial+ * functions, i.e., functions that are not defined over their entire input+ * range. In these situations, 'None' can be used as a placeholder return value.+ */+enum Option a = None | Some a++/**+ * Values of the 'Result t e' type can either be 'Ok', representing success and+ * containing a value of type 't', or 'Err', representing error and containing+ * an error value of type 'e'. Functions can return 'Result' whenever errors are+ * expected and recoverable. For instance, 'e' might be a 'String' with an error+ * message, or it might be an 'Integer' with an error code.+ */+enum Result t e = Ok t | Err e  // Bit specific operations ---------------------------------------- 

@@ -6,6 +6,7 @@ {-# LANGUAGE LambdaCase                #-} {-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TupleSections             #-} {-# LANGUAGE TypeApplications          #-}  -- | The implementation of loading and calling external functions from shared@@ -37,15 +38,16 @@ import           Control.Exception import           Control.Monad import           Data.Bifunctor+import           Data.Maybe import           Data.Word import           Foreign                    hiding (newForeignPtr) import           Foreign.C.Types import           Foreign.Concurrent import           Foreign.LibFFI+import           System.Directory           (canonicalizePath, doesFileExist) import           System.FilePath            ((-<.>))-import           System.Directory(doesFileExist)+import           System.Info                (os) import           System.IO.Error-import           System.Info(os)  #if defined(mingw32_HOST_OS) import           System.Win32.DLL@@ -98,32 +100,35 @@   pure ForeignSrc {..}  --- | Given the path to a Cryptol module, compute the location of--- the shared library we'd like to load.-foreignLibPath :: FilePath -> IO (Maybe FilePath)-foreignLibPath path =-  search+-- | Given the path to a Cryptol module, compute the location of the shared+-- library we'd like to load. If FFI is supported, returns the location and+-- whether or not it actually exists on disk. Otherwise, returns Nothing.+foreignLibPath :: FilePath -> IO (Maybe (FilePath, Bool))+foreignLibPath path = do+  path' <- canonicalizePath path+  let libPaths = map (path' -<.>) exts+      search ps =+        case ps of+          [] -> pure ((, False) <$> listToMaybe libPaths)+          p : more -> do+            yes <- doesFileExist p+            if yes then pure (Just (p, True)) else search more+  search libPaths+  where+  exts =     case os of       "mingw32" -> ["dll"]       "darwin"  -> ["dylib","so"]       _         -> ["so"] -  where-  search es =-    case es of-      [] -> pure Nothing-      e : more ->-        do let p = path -<.> e-           yes <- doesFileExist p-           if yes then pure (Just p) else search more-- loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ())) loadForeignLib path =   do mb <- foreignLibPath path      case mb of-       Nothing      -> pure (Left (CantLoadFFISrc path "File not found"))-       Just libPath -> tryLoad (CantLoadFFISrc path) (open libPath)+       Just (libPath, True) ->+         tryLoad (CantLoadFFISrc path) (open libPath)+       _ ->+         pure (Left (CantLoadFFISrc path "File not found"))    where open libPath = do #if defined(mingw32_HOST_OS)@@ -272,5 +277,8 @@  unloadForeignSrc :: ForeignSrc -> IO () unloadForeignSrc _ = pure ()++foreignLibPath :: FilePath -> IO (Maybe (FilePath, Bool))+foreignLibPath _ = pure Nothing  #endif

@@ -30,10 +30,12 @@         hang ("Could not load foreign source for module located at"               <+> text path <.> colon)           4 (text msg)-      CantLoadFFIImpl name msg ->-        hang ("Could not load foreign implementation for binding"-              <+> text name <.> colon)-          4 (text msg)+      CantLoadFFIImpl name _msg ->+        "Could not load foreign implementation for binding" <+> text name+        -- We don't print the OS error message for more consistent test output+        -- hang ("Could not load foreign implementation for binding"+        --       <+> text name <.> colon)+        --   4 (text _msg)       FFIDuplicates xs ->         hang "Multiple foreign declarations with the same name:"            4 (backticks (pp (nameIdent (head xs))) <+>

@@ -422,6 +422,7 @@   | BadRoundingMode Integer              -- ^ Invalid rounding mode   | BadValue String                      -- ^ Value outside the domain of a partial function.   | NoMatchingPropGuardCase String    -- ^ No prop guard holds for the given type variables.+  | NoMatchingConstructor (Maybe String) -- ^ Missing `case` alternative   | FFINotSupported Name                 -- ^ Foreign function cannot be called   | FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function                                          --   as a type argument is too large@@ -447,15 +448,20 @@     NoMatchingPropGuardCase msg -> text $ "No matching constraint guard; " ++ msg     FFINotSupported x -> vcat       [ text "cannot call foreign function" <+> pp x-      , text "FFI calls are not supported in this context"-      , text "If you are trying to evaluate an expression, try rebuilding"-      , text "  Cryptol with FFI support enabled."+      , text "No foreign implementation is loaded,"+      , text "  or FFI calls are not supported in this context."       ]     FFITypeNumTooBig f p n -> vcat       [ text "numeric type argument to foreign function is too large:"         <+> integer n       , text "in type parameter" <+> pp p <+> "of function" <+> pp f       , text "type arguments must fit in a C `size_t`" ]+    NoMatchingConstructor mbCon -> vcat+      [ "Missing `case` alternative" <+> con <.> "."+      ]+      where con = case mbCon of+                    Just c -> "for constructor" <+> backticks (text c)+                    Nothing -> mempty  instance Show EvalError where   show = show . pp

@@ -72,8 +72,9 @@                  !(SeqMap sym a)   | MemoSeqMap      !Nat'-     !(IORef (Map Integer a))-     !(IORef (Integer -> SEval sym a))+     !(IORef (Map Integer a, Integer -> SEval sym a))+     !(Integer -> SEval sym a)+      -- Use this to overwrite the evaluation function when the cache is full  indexSeqMap :: (Integer -> SEval sym a) -> SeqMap sym a indexSeqMap = IndexSeqMap@@ -84,21 +85,23 @@   case Map.lookup i m of     Just x  -> x     Nothing -> lookupSeqMap xs i-lookupSeqMap (MemoSeqMap sz cache eval) i =-  do mz <- liftIO (Map.lookup i <$> readIORef cache)-     case mz of-       Just z  -> return z++lookupSeqMap (MemoSeqMap sz cache_eval evalPanic) i =+  do (cache,eval) <- liftIO (readIORef cache_eval)+     case Map.lookup i cache of+       Just z -> pure z        Nothing ->-         do f <- liftIO (readIORef eval)-            v <- f i-            msz <- liftIO $ atomicModifyIORef' cache (\m ->-                        let m' = Map.insert i v m in (m', Map.size m'))-            -- If we memoize the entire map, overwrite the evaluation closure to let-            -- the garbage collector reap it-            when (case sz of Inf -> False; Nat sz' -> toInteger msz >= sz')-                 (liftIO (writeIORef eval-                    (\j -> panic "lookupSeqMap" ["Messed up size accounting", show sz, show j])))-            return v+        do v <- eval i+           liftIO $ atomicModifyIORef' cache_eval $ \(oldCache,oldFun) ->+             let !newCache = Map.insert i v oldCache+                 -- If we memoize the entire map,+                 -- overwrite the evaluation closure to let+                 -- the garbage collector reap it+                 !newEval =+                   case sz of+                     Nat sz' | toInteger (Map.size newCache) >= sz' -> evalPanic+                     _ -> oldFun+             in ((newCache, newEval), v)  instance Backend sym => Functor (SeqMap sym) where   fmap f xs = IndexSeqMap (\i -> f <$> lookupSeqMap xs i)@@ -173,12 +176,20 @@  memoMap sym sz x = do   stk <- sGetCallStack sym-  cache <- liftIO $ newIORef $ Map.empty-  evalRef <- liftIO $ newIORef $ eval stk-  return (MemoSeqMap sz cache evalRef)+  cache <- liftIO $ newIORef (Map.empty, eval stk)+  return (MemoSeqMap sz cache evalPanic)    where     eval stk i = sWithCallStack sym stk (lookupSeqMap x i)++    -- Not 100% sure that we actually need to do the bounds check here,+    -- or if we are assuming that the argument would be in bounds, but+    -- it doesn't really hurt to do it, as if we *did* already do the check+    -- this code should never run (unless we messed up something).+    evalPanic i = case sz of+                    Nat sz' | i < 0 || i >= sz' -> invalidIndex sym i+                    _ -> panic "lookupSeqMap"+                            ["Messed up size accounting", show sz, show i]   -- | Apply the given evaluation function pointwise to the two given

@@ -11,7 +11,6 @@ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ParallelListComp #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ViewPatterns #-}@@ -28,9 +27,10 @@   , emptyEnv   , evalExpr   , evalDecls-  , evalNewtypeDecls+  , evalNominalDecls   , evalSel   , evalSetSel+  , evalEnumCon   , EvalError(..)   , EvalErrorEx(..)   , Unsupported(..)@@ -53,7 +53,7 @@ import Cryptol.Parser.Position import Cryptol.Parser.Selector(ppSelector) import Cryptol.TypeCheck.AST-import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))+import Cryptol.TypeCheck.Solver.InfNat(Nat'(..),nMul) import Cryptol.Utils.Ident import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP@@ -62,6 +62,8 @@ import           Control.Monad import           Data.List import           Data.Maybe+import           Data.Vector(Vector)+import qualified Data.Vector as Vector import qualified Data.IntMap.Strict as IntMap import qualified Data.Map.Strict as Map import           Data.Semigroup@@ -96,7 +98,8 @@   Module         {- ^ Module containing declarations to evaluate -} ->   GenEvalEnv sym {- ^ Environment to extend -} ->   SEval sym (GenEvalEnv sym)-moduleEnv sym m env = evalDecls sym (mDecls m) =<< evalNewtypeDecls sym (mNewtypes m) env+moduleEnv sym m env = evalDecls sym (mDecls m) =<<+                          evalNominalDecls sym (mNominalTypes m) env  {-# SPECIALIZE evalExpr ::   (?range :: Range, ConcPrims) =>@@ -161,6 +164,17 @@      b <- fromVBit <$> eval c      iteValue sym b (eval t) (eval f) +  ECase e as d -> {-# SCC "evalExpr->ECase" #-} do+    val <- eval e+    let (con,fs) = fromVEnum val+    caseValue sym con fs+      CaseCont+        { caseCon = evalCase <$> as+        , caseDflt =+            do rhs <- d+               pure (evalCase rhs [pure val])+        }+   EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do       let len  = evalNumType (envTypes env) n       let elty = evalValType (envTypes env) t@@ -230,6 +244,10 @@   {-# INLINE eval #-}   eval = evalExpr sym env   ppV = ppValue sym defaultPPOpts+  evalCase (CaseAlt xs e) vs =+    do let addVar env' ((x,_),v) = bindVar sym x v env'+       newEnv <- foldM addVar env (zip xs vs)+       evalExpr sym newEnv e  -- | Checks whether an evaluated `Prop` holds checkProp :: Prop -> Bool@@ -296,42 +314,67 @@  -- Newtypes -------------------------------------------------------------------- -{-# SPECIALIZE evalNewtypeDecls ::+{-# SPECIALIZE evalNominalDecls ::   ConcPrims =>   Concrete ->-  Map.Map Name Newtype ->+  Map.Map Name NominalType ->   GenEvalEnv Concrete ->   SEval Concrete (GenEvalEnv Concrete)   #-} -evalNewtypeDecls ::+evalNominalDecls ::   EvalPrims sym =>   sym ->-  Map.Map Name Newtype ->+  Map.Map Name NominalType ->   GenEvalEnv sym ->   SEval sym (GenEvalEnv sym)-evalNewtypeDecls sym nts env = foldM (flip (evalNewtypeDecl sym)) env $ Map.elems nts+evalNominalDecls sym nts env = foldM (flip (evalNominalDecl sym)) env $ Map.elems nts  -- | Introduce the constructor function for a newtype.-evalNewtypeDecl ::+evalNominalDecl ::   EvalPrims sym =>   sym ->-  Newtype ->+  NominalType ->   GenEvalEnv sym ->   SEval sym (GenEvalEnv sym)-evalNewtypeDecl _sym nt = pure . bindVarDirect (ntConName nt) (foldr tabs con (ntParams nt))+evalNominalDecl sym nt env0 =+  case ntDef nt of+    Struct c -> pure (bindVarDirect (ntConName c) (mkCon structCon) env0)+    Enum cs  -> foldM enumCon env0 cs+    Abstract -> pure env0   where-  con           = PFun PPrim+  structCon = PFun PPrim+  mkCon c   = foldr tabs c (ntParams nt) +  enumCon env c =+    do con <- evalEnumCon sym (nameIdent (ecName c)) (ecNumber c)+       let done        = PVal . con . Vector.fromList . reverse+           fu _t f xs  = PFun (\v -> f (v:xs))+       pure (bindVarDirect (ecName c)+                           (mkCon (foldr fu done (ecFields c) [])) env)+   tabs tp body =     case tpKind tp of       KType -> PTyPoly  (\ _ -> body)       KNum  -> PNumPoly (\ _ -> body)-      k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show (pp k)]+      k ->+        evalPanic "evalNominalDecl" [ "illegal newtype parameter kind"+                                    , show (pp k)+                                    ] -{-# INLINE evalNewtypeDecl #-}+{-# INLINE evalNominalDecl #-} +-- | Make the function for a known constructor+evalEnumCon ::+  Backend sym =>+  sym -> Ident -> Int ->+  SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)+evalEnumCon sym i n =+  do tag <- integerLit sym (toInteger n)+     pure (VEnum tag . IntMap.singleton n . ConInfo i) ++ -- Declarations ----------------------------------------------------------------  {-# SPECIALIZE evalDecls ::@@ -368,7 +411,16 @@   SEval sym (GenEvalEnv sym) evalDeclGroup sym env dg = do   case dg of-    Recursive ds -> do+    Recursive ds0 -> do+      let ds = filter shouldEval ds0+          -- If there are foreign declarations, we should only evaluate them if+          -- they are not already bound in the environment by the previous+          -- Cryptol.Eval.FFI.evalForeignDecls pass.+          shouldEval d =+            case (dDefinition d, lookupVar (dName d) env) of+              (DForeign _ _, Just _) -> False+              _                      -> True+       -- declare a "hole" for each declaration       -- and extend the evaluation environment       holes <- mapM (declHole sym) ds@@ -432,14 +484,19 @@   sym -> Decl -> SEval sym (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) declHole sym d =   case dDefinition d of-    DPrim      -> evalPanic "Unexpected primitive declaration in recursive group"-                            [show (ppLocName nm)]-    DForeign _ -> evalPanic "Unexpected foreign declaration in recursive group"-                            [show (ppLocName nm)]-    DExpr _    -> do-      (hole, fill) <- sDeclareHole sym msg-      return (nm, sch, hole, fill)+    DPrim -> evalPanic "Unexpected primitive declaration in recursive group"+                       [show (ppLocName nm)]+    DForeign _ me ->+      case me of+        Nothing -> evalPanic+          "Unexpected foreign declaration with no cryptol implementation in recursive group"+          [show (ppLocName nm)]+        Just _ -> doHole+    DExpr _ -> doHole   where+  doHole = do+    (hole, fill) <- sDeclareHole sym msg+    return (nm, sch, hole, fill)   nm = dName d   sch = dSignature d   msg = unwords ["while evaluating", show (pp nm)]@@ -470,17 +527,22 @@         Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env         Nothing        -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env -    DForeign _ -> do+    DForeign _ me -> do       -- Foreign declarations should have been handled by the previous       -- Cryptol.Eval.FFI.evalForeignDecls pass already, so they should already-      -- be in the environment. If not, then either Cryptol was not compiled-      -- with FFI support enabled, or we are in a non-Concrete backend. In that-      -- case, we just bind the name to an error computation which will raise an-      -- error if we try to evaluate it.+      -- be in the environment. If not, then either the foreign source was+      -- missing, Cryptol was not compiled with FFI support enabled, or we are+      -- in a non-Concrete backend. In that case, we bind the name to the+      -- fallback cryptol implementation if present, or otherwise to an error+      -- computation which will raise an error if we try to evaluate it.       case lookupVar (dName d) env of         Just _  -> pure env-        Nothing -> bindVar sym (dName d)-          (raiseError sym $ FFINotSupported $ dName d) env+        Nothing -> bindVar sym (dName d) val env+          where+          val =+            case me of+              Just e -> evalExpr sym renv e+              Nothing -> raiseError sym $ FFINotSupported $ dName d      DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env @@ -689,23 +751,23 @@   ListEnv sym ->   [Match] ->   SEval sym (ListEnv sym)-branchEnvs sym env matches = snd <$> foldM (evalMatch sym) (1, env) matches+branchEnvs sym env matches = snd <$> foldM (evalMatch sym) (Nat 1, env) matches  {-# SPECIALIZE evalMatch ::   (?range :: Range, ConcPrims) =>   Concrete ->-  (Integer, ListEnv Concrete) ->+  (Nat', ListEnv Concrete) ->   Match ->-  SEval Concrete (Integer, ListEnv Concrete)+  SEval Concrete (Nat', ListEnv Concrete)   #-}  -- | Turn a match into the list of environments it represents. evalMatch ::   (?range :: Range, EvalPrims sym) =>   sym ->-  (Integer, ListEnv sym) ->+  (Nat', ListEnv sym) ->   Match ->-  SEval sym (Integer, ListEnv sym)+  SEval sym (Nat', ListEnv sym) evalMatch sym (lsz, lenv) m = seq lsz $ case m of    -- many envs@@ -714,7 +776,7 @@       -- Select from a sequence of finite length.  This causes us to 'stutter'       -- through our previous choices `nLen` times.       Nat nLen -> do-        vss <- memoMap sym (Nat lsz) $ indexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr+        vss <- memoMap sym lsz $ indexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr         let stutter xs = \i -> xs (i `div` nLen)         let lenv' = lenv { leVars = fmap stutter (leVars lenv) }         let vs i = do let (q, r) = i `divMod` nLen@@ -723,27 +785,21 @@                         VSeq _ xs'  -> lookupSeqMap xs' r                         VStream xs' -> lookupSeqMap xs' r                         _           -> evalPanic "evalMatch" ["Not a list value"]-        return (lsz * nLen, bindVarList n vs lenv')+        return (nMul lsz len, bindVarList n vs lenv') -      -- Select from a sequence of infinite length.  Note that this means we-      -- will never need to backtrack into previous branches.  Thus, we can convert-      -- `leVars` elements of the comprehension environment into `leStatic` elements-      -- by selecting out the 0th element.+      {- Select from a sequence of infinite length.  Note that only the+         first generator in a sequence of generators may have infinite length,+         so we can just evaluate it once an for all (i.e., it does not change+         on each loop iteration, as it may happen in the finite case). -}       Inf -> do-        let allvars = IntMap.union (fmap (Right . ($ 0)) (leVars lenv)) (leStatic lenv)-        let lenv' = lenv { leVars   = IntMap.empty-                         , leStatic = allvars-                         }-        let env   = EvalEnv allvars (leTypes lenv)+        let env = EvalEnv (leStatic lenv) (leTypes lenv)         xs <- evalExpr sym env expr         let vs i = case xs of                      VWord _ w   -> VBit <$> indexWordValue sym w i                      VSeq _ xs'  -> lookupSeqMap xs' i                      VStream xs' -> lookupSeqMap xs' i                      _           -> evalPanic "evalMatch" ["Not a list value"]-        -- Selecting from an infinite list effectively resets the length of the-        -- list environment, so return 1 as the length-        return (1, bindVarList n vs lenv')+        return (Inf, bindVarList n vs lenv)      where       len  = evalNumType (leTypes lenv) l@@ -755,6 +811,6 @@     where       f env =           case dDefinition d of-            DPrim      -> evalPanic "evalMatch" ["Unexpected local primitive"]-            DForeign _ -> evalPanic "evalMatch" ["Unexpected local foreign"]-            DExpr e    -> evalExpr sym env e+            DPrim        -> evalPanic "evalMatch" ["Unexpected local primitive"]+            DForeign _ _ -> evalPanic "evalMatch" ["Unexpected local foreign"]+            DExpr e      -> evalExpr sym env e

@@ -20,6 +20,8 @@   ) where  import Control.Monad (guard, zipWithM, foldM, mzero)+import Data.Foldable (foldl')+import Data.List (find) import Data.Ratio(numerator,denominator) import Data.Word(Word32, Word64) import MonadLib( ChoiceT, findOne, lift )@@ -28,6 +30,8 @@  import qualified Data.Map.Strict as Map import Data.Map(Map)+import qualified Data.Vector as Vector+import qualified Data.IntMap.Strict as IMap  import Cryptol.TypeCheck.Solver.InfNat (Nat'(..)) @@ -75,14 +79,40 @@              Left _ -> mismatch -- different fields              Right efs -> pure (ERec efs) -      (TVNewtype nt ts tfs, VRecord vfs) ->+      (TVNominal nt ts (TVStruct tfs), VRecord vfs) ->         do -- NB, vfs first argument to keep their display order            res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs            case res of              Left _ -> mismatch -- different fields              Right efs ->-               let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts+               let c = case ntDef nt of+                         Struct co -> ntConName co+                         Enum {} -> panic "toExpr" ["Enum vs Record"]+                         Abstract -> panic "toExp" ["Asbtract vs Record"]+                   f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar c) ts                 in pure (EApp f (ERec efs))+      (TVNominal nt ts (TVEnum tfss), VEnum i' vf_map) ->+        let i = fromInteger i'+        in+        case tfss Vector.!? i of+          Nothing -> mismatch -- enum constructor not found+          Just conT ->+            do let tfs = conFields conT+               vfs <- case IMap.lookup i vf_map of+                        Just con -> pure (conFields con)+                        Nothing  -> panic "toExpr" ["Missing constructor"]+               guard (Vector.length tfs == Vector.length vfs)+               c <- case ntDef nt of+                      Struct {} -> panic "toExpr" ["Enum vs Record"]+                      Abstract {} -> panic "toExpr" ["Enum vs Abstract"]+                      Enum cons ->+                        case find (\con -> ecNumber con == i) cons of+                          Just con -> pure (ecName con)+                          Nothing -> mismatch+               let f = foldl' (\x t -> ETApp x (tNumValTy t)) (EVar c) ts+               foldl' EApp f <$>+                  (zipWithM go (Vector.toList tfs) =<<+                              lift (sequence (Vector.toList vfs)))        (TVTuple ts, VTuple tvs) ->         do guard (length ts == length tvs)

@@ -59,18 +59,19 @@ #ifdef FFI_ENABLED  -- | Add the given foreign declarations to the environment, loading their--- implementations from the given 'ForeignSrc'. This is a separate pass from the--- main evaluation functions in "Cryptol.Eval" since it only works for the--- Concrete backend.+-- implementations from the given 'ForeignSrc'. If some implementations fail to+-- load then errors are reported for them but any successfully loaded+-- implementations are still added to the environment.+--+-- This is a separate pass from the main evaluation functions in "Cryptol.Eval"+-- since it only works for the Concrete backend. evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->-  Eval (Either [FFILoadError] EvalEnv)+  Eval ([FFILoadError], EvalEnv) evalForeignDecls fsrc decls env = io do-  ePrims <- for decls \(name, ffiFunType) ->+  (errs, prims) <- partitionEithers <$> for decls \(name, ffiFunType) ->     fmap ((name,) . foreignPrimPoly name ffiFunType) <$>       loadForeignImpl fsrc (unpackIdent $ nameIdent name)-  pure case partitionEithers ePrims of-    ([], prims) -> Right $ foldr (uncurry bindVarDirect) env prims-    (errs, _)   -> Left errs+  pure (errs, foldr (uncurry bindVarDirect) env prims)  -- | Generate a 'Prim' value representing the given foreign function, containing -- all the code necessary to marshal arguments and return values and do the@@ -422,9 +423,9 @@ #else  -- | Dummy implementation for when FFI is disabled. Does not add anything to--- the environment.+-- the environment or report any errors. evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->-  Eval (Either [FFILoadError] EvalEnv)-evalForeignDecls _ _ env = pure $ Right env+  Eval ([FFILoadError], EvalEnv)+evalForeignDecls _ _ env = pure ([], env)  #endif

@@ -250,11 +250,8 @@               (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))               fs -    TVAbstract {} ->-      evalPanic "ringBinary" ["Abstract type not in `Ring`"]--    TVNewtype {} ->-      evalPanic "ringBinary" ["Newtype not in `Ring`"]+    TVNominal {} ->+      evalPanic "ringBinary" ["Nominal type not in `Ring`"]  type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym) @@ -330,9 +327,7 @@           (\f fty -> sDelay sym (loop' fty (lookupRecord f v)))           fs -    TVAbstract {} -> evalPanic "ringUnary" ["Abstract type not in `Ring`"]--    TVNewtype {} -> evalPanic "ringUnary" ["Newtype not in `Ring`"]+    TVNominal {} -> evalPanic "ringUnary" ["Nominal type not in `Ring`"]   {-# SPECIALIZE ringNullary ::@@ -398,11 +393,8 @@              do xs <- traverse (sDelay sym . loop) fs                 pure $ VRecord xs -        TVAbstract {} ->-          evalPanic "ringNullary" ["Abstract type not in `Ring`"]--        TVNewtype {} ->-          evalPanic "ringNullary" ["Newtype not in `Ring`"]+        TVNominal {} ->+          evalPanic "ringNullary" ["Nominal type not in `Ring`"]  {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->@@ -777,11 +769,9 @@                             (recordElements (fromVRecord v1))                             (recordElements (fromVRecord v2))                             k-        TVAbstract {} -> evalPanic "cmpValue"-                          [ "Abstract type not in `Cmp`" ] -        TVNewtype {} -> evalPanic "cmpValue"-                          [ "Newtype not in `Cmp`" ]+        TVNominal {} -> evalPanic "cmpValue"+                          [ "Nominal type not in `Cmp`" ]      cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =       do x1' <- x1@@ -951,9 +941,7 @@       do xs <- traverse (sDelay sym . zeroV sym) fields          pure $ VRecord xs -  TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ]--  TVNewtype {} -> evalPanic "zeroV" [ "Newtype not in `Zero`" ]+  TVNominal {} -> evalPanic "zeroV" [ "Nominal type not in `Zero`" ]   {-# SPECIALIZE joinSeq ::@@ -1292,11 +1280,8 @@           (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))           fields -    TVAbstract {} -> evalPanic "logicBinary"-                        [ "Abstract type not in `Logic`" ]--    TVNewtype {} -> evalPanic "logicBinary"-                        [ "Newtype not in `Logic`" ]+    TVNominal {} -> evalPanic "logicBinary"+                        [ "Nominal type not in `Logic`" ]  {-# SPECIALIZE logicUnary ::   Concrete ->@@ -1352,9 +1337,7 @@           (\f fty -> sDelay sym (loop' fty (lookupRecord f val)))           fields -    TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ]--    TVNewtype {} -> evalPanic "logicUnary" [ "Newtype not in `Logic`" ]+    TVNominal {} -> evalPanic "logicUnary" [ "Nominal type not in `Logic`" ]   {-# INLINE assertIndexInBounds #-}@@ -1877,22 +1860,23 @@ parmapV :: Backend sym => sym -> Prim sym parmapV sym =   PTyPoly \_a ->-  PTyPoly \_b ->-  PFinPoly \_n ->+  PTyPoly \b ->+  PFinPoly \n ->   PFun \f ->   PFun \xs ->   PPrim     do f' <- fromVFun sym <$> f        xs' <- xs-       case xs' of-          VWord n w ->-            do let m = asBitsMap sym w-               m' <- sparkParMap sym (\x -> f' (VBit <$> x)) n m-               VWord n <$> (bitmapWordVal sym n (fromVBit <$> m'))-          VSeq n m ->-            VSeq n <$> sparkParMap sym f' n m+       m <-+         case xs' of+           VWord _n w ->+             let m = asBitsMap sym w in+             sparkParMap sym (\x -> f' (VBit <$> x)) n m+           VSeq _n m ->+             sparkParMap sym f' n m -          _ -> panic "parmapV" ["expected sequence!"]+           _ -> panic "parmapV" ["expected finite sequence!"]+       mkSeq sym (Nat n) b m   sparkParMap ::

@@ -36,16 +36,17 @@ > import qualified GHC.Num.Compat as Integer > import qualified Data.List as List >-> import Cryptol.ModuleSystem.Name (asPrim)+> import Cryptol.ModuleSystem.Name (asPrim,nameIdent) > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul) > import Cryptol.TypeCheck.AST > import Cryptol.Backend.FloatHelpers (BF(..)) > import qualified Cryptol.Backend.FloatHelpers as FP > import Cryptol.Backend.Monad (EvalError(..)) > import Cryptol.Eval.Type->   (TValue(..), isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)+>   (TValue(..), TNominalTypeValue(..),+>    isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar) > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)-> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)+> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim, unpackIdent) > import Cryptol.Utils.Panic (panic) > import Cryptol.Utils.PP > import Cryptol.Utils.RecordMap@@ -53,7 +54,7 @@ > import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy) > > import qualified Cryptol.ModuleSystem as M-> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)+> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNominalTypes)  Overview ========@@ -176,6 +177,7 @@ >   | VList Nat' [E Value]       -- ^ @ [n]a   @ finite or infinite lists >   | VTuple [E Value]           -- ^ @ ( .. ) @ tuples >   | VRecord [(Ident, E Value)] -- ^ @ { .. } @ records+>   | VEnum Ident [E Value]      -- ^ @ Just x @, sum types >   | VFun (E Value -> E Value)  -- ^ functions >   | VPoly (TValue -> E Value)  -- ^ polymorphic values (kind *) >   | VNumPoly (Nat' -> E Value) -- ^ polymorphic values (kind #)@@ -222,6 +224,11 @@ > fromVRecord (VRecord fs) = fs > fromVRecord _            = evalPanic "fromVRecord" ["Expected a record"] >+> -- | Destructor for @VEnum@.+> fromVEnum :: Value -> (Ident,[E Value])+> fromVEnum (VEnum i fs) = (i,fs)+> fromVEnum _            = evalPanic "fromVEnum" ["Expected an enum value."]+> > -- | Destructor for @VFun@. > fromVFun :: Value -> (E Value -> E Value) > fromVFun (VFun f) = f@@ -310,6 +317,8 @@ >     EIf c t f -> >       condValue (fromVBit <$> evalExpr env c) (evalExpr env t) (evalExpr env f) >+>     ECase e alts dflt -> evalCase env (evalExpr env e) alts dflt+> >     EComp _n _ty e branches -> evalComp env e branches > >     EVar n ->@@ -338,7 +347,7 @@ >     EProofApp e    -> evalExpr env e >     EWhere e dgs   -> evalExpr (foldl evalDeclGroup env dgs) e >->     EPropGuards guards _ty -> +>     EPropGuards guards _ty -> >       case List.find (all (checkProp . evalProp env) . fst) guards of >         Just (_, e) -> evalExpr env e >         Nothing -> evalPanic "fromVBit" ["No guard constraint was satisfied"]@@ -346,7 +355,7 @@ > appFun :: E Value -> E Value -> E Value > appFun f v = f >>= \f' -> fromVFun f' v -> -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables +> -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables > -- according to `envTypes` and expanding all type synonyms via `tNoUser`. > evalProp :: Env -> Prop -> Prop > evalProp env@Env { envTypes } = \case@@ -355,7 +364,7 @@ >   prop@TUser {} -> evalProp env (tNoUser prop) >   TVar tv | Nothing <- lookupTypeVar tv envTypes -> panic "evalProp" ["Could not find type variable `" ++ pretty tv ++ "` in the type evaluation environment"] >   prop -> panic "evalProp" ["Cannot use the following as a type constraint: `" ++ pretty prop ++ "`"]->   where +>   where >     toType = either tNumTy tValTy  @@ -399,7 +408,7 @@ >   case (tyv, sel) of >     (TVTuple ts, TupleSel n _) -> updTupleAt ts n >     (TVRec fs, RecordSel n _)  -> updRecAt fs n->     (TVNewtype _ _ fs, RecordSel n _) -> updRecAt fs n+>     (TVNominal _ _ (TVStruct fs), RecordSel n _) -> updRecAt fs n >     (TVSeq len _, ListSel n _) -> updSeqAt len n >     (_, _) -> evalPanic "evalSet" ["type/selector mismatch", show tyv, show sel] >   where@@ -432,6 +441,20 @@ > condValue :: E Bool -> E Value -> E Value -> E Value > condValue c l r = c >>= \b -> if b then l else r +> evalCase :: Env -> E Value -> Map Ident CaseAlt -> Maybe CaseAlt -> E Value+> evalCase env e alts dflt =+>   do val <- e+>      let (tag,fields) = fromVEnum val+>      case Map.lookup tag alts of+>        Just alt -> evalCaseBranch alt fields+>        Nothing  ->+>          case dflt of+>            Just alt -> evalCaseBranch alt [pure val]+>            Nothing  -> Err (NoMatchingConstructor (Just (unpackIdent tag)))+>   where+>   evalCaseBranch (CaseAlt xs k) vs = evalExpr env' k+>     where env' = foldr bindVar env (zip (map fst xs) vs)+ List Comprehensions ------------------- @@ -531,29 +554,51 @@ > evalDecl :: Env -> Decl -> (Name, E Value) > evalDecl env d = >   case dDefinition d of->     DPrim      -> (dName d, pure (evalPrim (dName d)))->     DForeign _ -> (dName d, cryError $ FFINotSupported $ dName d)->     DExpr e    -> (dName d, evalExpr env e)+>     DPrim         -> (dName d, pure (evalPrim (dName d)))+>     DForeign _ me -> (dName d, val)+>       where+>         val =+>           case me of+>             Just e  -> evalExpr env e+>             Nothing -> cryError $ FFINotSupported $ dName d+>     DExpr e       -> (dName d, evalExpr env e) > -Newtypes---------+Nominal Types+------------- +We have three forms of nominal types: newtypes, enums, and abstract types.+ At runtime, newtypes values are represented in exactly the same way as records.  The constructor function for newtypes is thus basically just an identity function that consumes and ignores its type arguments. -> evalNewtypeDecl :: Env -> Newtype -> Env-> evalNewtypeDecl env nt = bindVar (ntConName nt, pure val) env+Enums are represented with a tag, which indicates what constructor+was used to create a value, as well as the types of the values stored in the+constructor.++> evalNominalDecl :: Env -> NominalType -> Env+> evalNominalDecl env nt =+>   case ntDef nt of+>     Struct c -> bindVar (ntConName c, mkCon newtypeCon) env+>     Enum cs  -> foldr enumCon env cs+>     Abstract -> env >   where->     val = foldr tabs con (ntParams nt)->     con = VFun (\x -> x)+>     mkCon con  = pure (foldr tabs con (ntParams nt))+>     newtypeCon = VFun id+>     enumCon c  =+>       bindVar (ecName c, mkCon (foldr addField tag (ecFields c) []))+>       where+>       tag                 = VEnum (nameIdent (ecName c)) . reverse+>       addField _t mk args = VFun (\v -> pure (mk (v:args)))+> >     tabs tp body = >       case tpKind tp of >         KType -> VPoly (\_ -> pure body) >         KNum  -> VNumPoly (\_ -> pure body)->         k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show k]+>         k -> evalPanic "evalNominalDecl"+>                                   ["illegal newtype parameter kind", show k]  Primitives ==========@@ -1016,8 +1061,7 @@ > zero (TVRec fields) = VRecord [ (f, pure (zero fty)) >                               | (f, fty) <- canonicalFields fields ] > zero (TVFun _ bty)  = VFun (\_ -> pure (zero bty))-> zero (TVAbstract{}) = evalPanic "zero" ["Abstract type not in `Zero`"]-> zero (TVNewtype{})  = evalPanic "zero" ["Newtype not in `Zero`"]+> zero (TVNominal {})  = evalPanic "zero" ["Nominal type not in `Zero`"]  Literals --------@@ -1085,8 +1129,7 @@ >         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"] >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"] >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]->         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]->         TVNewtype{}  -> evalPanic "logicUnary" ["Newtype not in `Logic`"]+>         TVNominal {}  -> evalPanic "logicUnary" ["Nominal type not in `Logic`"]  > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value > logicBinary op = go@@ -1124,8 +1167,7 @@ >         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"] >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"] >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]->         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]->         TVNewtype{}  -> evalPanic "logicBinary" ["Newtype not in `Logic`"]+>         TVNominal {} -> evalPanic "logicBinary" ["Nominal type not in `Logic`"]   Ring Arithmetic@@ -1171,9 +1213,7 @@ >           pure $ VTuple (map go tys) >         TVRec fs -> >           pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ]->         TVAbstract {} ->->           evalPanic "arithNullary" ["Abstract type not in `Ring`"]->         TVNewtype {} ->+>         TVNominal {} -> >           evalPanic "arithNullary" ["Newtype type not in `Ring`"]  > ringUnary ::@@ -1211,10 +1251,8 @@ >           do val' <- val >              pure $ VRecord [ (f, go fty (lookupRecord f val')) >                             | (f, fty) <- canonicalFields fs ]->         TVAbstract {} ->->           evalPanic "arithUnary" ["Abstract type not in `Ring`"]->         TVNewtype {} ->->           evalPanic "arithUnary" ["Newtype not in `Ring`"]+>         TVNominal {} ->+>           evalPanic "arithUnary" ["Nominal type not in `Ring`"]  > ringBinary :: >   (Integer -> Integer -> E Integer) ->@@ -1261,10 +1299,8 @@ >              pure $ VRecord >                [ (f, go fty (lookupRecord f l') (lookupRecord f r')) >                | (f, fty) <- canonicalFields fs ]->         TVAbstract {} ->->           evalPanic "arithBinary" ["Abstract type not in class `Ring`"]->         TVNewtype {} ->->           evalPanic "arithBinary" ["Newtype not in class `Ring`"]+>         TVNominal {} ->+>           evalPanic "arithBinary" ["Nominal type not in class `Ring`"]   Integral@@ -1441,10 +1477,8 @@ >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r >          lexList (zipWith3 lexCompare tys ls rs)->     TVAbstract {} ->->       evalPanic "lexCompare" ["Abstract type not in `Cmp`"]->     TVNewtype {} ->->       evalPanic "lexCompare" ["Newtype not in `Cmp`"]+>     TVNominal {} ->+>       evalPanic "lexCompare" ["Nominal type not in `Cmp`"] > > lexList :: [E Ordering] -> E Ordering > lexList [] = pure EQ@@ -1497,10 +1531,8 @@ >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r >          lexList (zipWith3 lexSignedCompare tys ls rs)->     TVAbstract {} ->->       evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]->     TVNewtype {} ->->       evalPanic "lexSignedCompare" ["Newtype type not in `Cmp`"]+>     TVNominal {} ->+>       evalPanic "lexSignedCompare" ["Nominal type not in `Cmp`"]   Sequences@@ -1799,6 +1831,11 @@ >     VTuple vs  -> ppTuple (map (ppEValue opts) vs) >     VRecord fs -> ppRecord (map ppField fs) >       where ppField (f,r) = pp f <+> char '=' <+> ppEValue opts r+>     VEnum tag vs ->+>       case vs of+>         [] -> tagT+>         _  -> parens (tagT <+> hsep (map (ppEValue opts) vs))+>       where tagT = text (unpackIdent tag) >     VFun _     -> text "<function>" >     VPoly _    -> text "<polymorphic value>" >     VNumPoly _ -> text "<polymorphic value>"@@ -1815,6 +1852,6 @@ >   where >     modEnv = M.minpModuleEnv minp >     extDgs = concatMap mDecls (M.loadedModules modEnv) ++ M.deDecls (M.meDynEnv modEnv)->     nts    = Map.elems (M.loadedNewtypes modEnv)->     env    = foldl evalDeclGroup (foldl evalNewtypeDecl mempty nts) extDgs+>     nts    = Map.elems (M.loadedNominalTypes modEnv)+>     env    = foldl evalDeclGroup (foldl evalNominalDecl mempty nts) extDgs >     val    = evalExpr env expr

@@ -6,12 +6,17 @@ -- Stability   :  provisional -- Portability :  portable -{-# LANGUAGE Safe, PatternGuards #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-} module Cryptol.Eval.Type where +import Data.Vector (Vector)+import qualified Data.Vector as Vector+import Data.List(sortOn) import Cryptol.Backend.Monad (evalPanic)+import Cryptol.ModuleSystem.Name(nameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.PP(pp) import Cryptol.TypeCheck.Solver.InfNat@@ -39,12 +44,35 @@   | TVTuple [TValue]          -- ^ @ (a, b, c )@   | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @   | TVFun TValue TValue       -- ^ @ a -> b @-  | TVNewtype Newtype+  | TVNominal NominalType               [Either Nat' TValue]-              (RecordMap Ident TValue)     -- ^ a named newtype-  | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type+              TNominalTypeValue    -- ^ a named newtype     deriving (Generic, NFData, Eq) +data TNominalTypeValue =+    TVStruct (RecordMap Ident TValue)+  | TVEnum   (Vector (ConInfo TValue))  -- ^ Indexed by constructor number+  | TVAbstract+    deriving (Generic, NFData, Eq)++data ConInfo a = ConInfo+  { conIdent :: Ident+  , conFields :: Vector a+  } deriving (Generic,NFData,Eq,Functor,Foldable,Traversable)++isNullaryCon :: ConInfo a -> Bool+isNullaryCon = Vector.null . conFields++zipConInfo :: (a -> b -> c) -> ConInfo a -> ConInfo b -> ConInfo c+zipConInfo f x y+  | conIdent x == conIdent y =+    x { conFields = Vector.zipWith f (conFields x) (conFields y) }+  | otherwise = panic "zipConInfo" [ "Mismatched constructors"+                                   ,  show (pp (conIdent x))+                                   ,  show (pp (conIdent y))+                                   ]++ -- | Convert a type value back into a regular type tValTy :: TValue -> Type tValTy tv =@@ -60,8 +88,7 @@     TVTuple ts  -> tTuple (map tValTy ts)     TVRec fs    -> tRec (fmap tValTy fs)     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)-    TVNewtype nt vs _ -> tNewtype nt (map tNumValTy vs)-    TVAbstract u vs -> tAbstract u (map tNumValTy vs)+    TVNominal nt vs _ -> tNominal nt (map tNumValTy vs)  tNumTy :: Nat' -> Type tNumTy Inf     = tInf@@ -132,7 +159,7 @@     TUser _ _ ty'  -> evalType env ty'     TRec fields    -> Right $ TVRec (fmap val fields) -    TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody env nt tvs+    TNominal nt ts -> Right $ TVNominal nt tvs $ evalNominalTypeBody env nt tvs         where tvs = map (evalType env) ts      TCon (TC c) ts ->@@ -150,15 +177,6 @@         (TCTuple _, _)  -> Right $ TVTuple (map val ts)         (TCNum n, [])   -> Left $ Nat n         (TCInf, [])     -> Left $ Inf-        (TCAbstract u,vs) ->-            case kindOf ty of-              KType -> Right $ TVAbstract u (map (evalType env) vs)-              k -> evalPanic "evalType"-                [ "Unsupported"-                , "*** Abstract type of kind: " ++ show (pp k)-                , "*** Name: " ++ show (pp u)-                ]-         _ -> evalPanic "evalType" ["not a value type", show ty]     TCon (TF f) ts      -> Left $ evalTF f (map num ts)     TCon (PC p) _       -> evalPanic "evalType" ["invalid predicate symbol", show p]@@ -173,10 +191,18 @@                                   ["Expecting a finite size, but got `inf`"]  -- | Evaluate the body of a newtype, given evaluated arguments-evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue-evalNewtypeBody env0 nt args = fmap (evalValType env') (ntFields nt)+evalNominalTypeBody ::+  TypeEnv -> NominalType -> [Either Nat' TValue] -> TNominalTypeValue+evalNominalTypeBody env0 nt args =+  case ntDef nt of+    Struct c -> TVStruct (fmap (evalValType env') (ntFields c))+    Enum cs  -> TVEnum (Vector.fromList (map doEnum (sortOn ecNumber cs)))+    Abstract -> TVAbstract   where   env' = loop env0 (ntParams nt) args++  doEnum c = ConInfo (nameIdent (ecName c))+                     (Vector.fromList (map (evalValType env') (ecFields c)))    loop env [] [] = env   loop env (p:ps) (a:as) = loop (bindTypeVar (TVBound p) a env) ps as

@@ -25,7 +25,7 @@  module Cryptol.Eval.Value   ( -- * GenericValue-    GenValue(..)+    GenValue(..), ConValue   , forceValue   , Backend(..)   , asciiMode@@ -57,22 +57,30 @@   , fromVTuple   , fromVRecord   , lookupRecord+  , fromVEnum     -- ** Pretty printing   , defaultPPOpts   , ppValue+  , ppValuePrec     -- * Merge and if/then/else   , iteValue+  , caseValue, CaseCont(..)   , mergeValue   ) where  import Data.Ratio import Numeric (showIntAtBase)+import Data.Map(Map)+import qualified Data.Map as Map+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IMap+import qualified Data.Vector as Vector  import Cryptol.Backend import Cryptol.Backend.SeqMap import qualified Cryptol.Backend.Arch as Arch import Cryptol.Backend.Monad-  ( evalPanic, wordTooWide, CallStack, combineCallStacks )+  ( evalPanic, wordTooWide, CallStack, combineCallStacks,EvalError(..)) import Cryptol.Backend.FloatHelpers (fpPP) import Cryptol.Backend.WordValue @@ -80,7 +88,7 @@  import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) -import Cryptol.Utils.Ident (Ident)+import Cryptol.Utils.Ident (Ident,unpackIdent) import Cryptol.Utils.Logger(Logger) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.PP@@ -105,6 +113,11 @@ data GenValue sym   = VRecord !(RecordMap Ident (SEval sym (GenValue sym))) -- ^ @ { .. } @   | VTuple ![SEval sym (GenValue sym)]              -- ^ @ ( .. ) @+  | VEnum !(SInteger sym) !(IntMap (ConValue sym))+    -- ^ As an example, consider the enum value @Just ()@. The 'SInteger' is the+    -- tag (e.g., 'Just' would have the tag @0@), and the 'IntMap' contains the+    -- fields (e.g., @{ 0 -> ("Just",()) }@. The 'IntMap' is only really needed+    -- to represent symbolic values.   | VBit !(SBit sym)                           -- ^ @ Bit    @   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @   | VRational !(SRational sym)                 -- ^ @ Rational @@@ -118,12 +131,14 @@   | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)  deriving Generic +type ConValue sym = ConInfo (SEval sym (GenValue sym))  -- | Force the evaluation of a value forceValue :: Backend sym => GenValue sym -> SEval sym () forceValue v = case v of   VRecord fs  -> mapM_ (forceValue =<<) fs   VTuple xs   -> mapM_ (forceValue =<<) xs+  VEnum i xs  -> seq i (mapM_ forceConValue xs)   VSeq n xs   -> mapM_ (forceValue =<<) (enumerateSeqMap n xs)   VBit b      -> seq b (return ())   VInteger i  -> seq i (return ())@@ -135,12 +150,14 @@   VPoly{}     -> return ()   VNumPoly{}  -> return () -+forceConValue :: Backend sym => ConValue sym -> SEval sym ()+forceConValue (ConInfo i vs) = i `seq` mapM_ (forceValue =<<) vs  instance Show (GenValue sym) where   show v = case v of     VRecord fs -> "record:" ++ show (displayOrder fs)     VTuple xs  -> "tuple:" ++ show (length xs)+    VEnum _ _  -> "enum"     VBit _     -> "bit"     VInteger _ -> "integer"     VRational _ -> "rational"@@ -160,23 +177,33 @@   PPOpts ->   GenValue sym ->   SEval sym Doc-ppValue x opts = loop+ppValue x opts = ppValuePrec x opts 0++ppValuePrec :: forall sym.+  Backend sym =>+  sym ->+  PPOpts ->+  Int ->+  GenValue sym ->+  SEval sym Doc+ppValuePrec x opts = loop   where-  loop :: GenValue sym -> SEval sym Doc-  loop val = case val of-    VRecord fs         -> do fs' <- traverse (>>= loop) fs+  loop :: Int -> GenValue sym -> SEval sym Doc+  loop prec val = case val of+    VRecord fs         -> do fs' <- traverse (>>= loop 0) fs                              return $ ppRecord (map ppField (fields fs'))       where       ppField (f,r) = pp f <+> char '=' <+> r-    VTuple vals        -> do vals' <- traverse (>>=loop) vals+    VTuple vals        -> do vals' <- traverse (>>=loop 0) vals                              return $ ppTuple vals'+    VEnum c vs         -> ppEnumVal prec c vs     VBit b             -> ppSBit x b     VInteger i         -> ppSInteger x i     VRational q        -> ppSRational x q     VFloat i           -> ppSFloat x opts i     VSeq sz vals       -> ppWordSeq sz vals     VWord _ wv         -> ppWordVal wv-    VStream vals       -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals+    VStream vals       -> do vals' <- traverse (>>=loop 0) $ enumerateSeqMap (useInfLength opts) vals                              return $ ppList ( vals' ++ [text "..."] )     VFun{}             -> return $ text "<function>"     VPoly{}            -> return $ text "<polymorphic value>"@@ -187,6 +214,19 @@     DisplayOrder -> displayFields     CanonicalOrder -> canonicalFields +  ppEnumVal prec i mp =+    case integerAsLit x i of+      Just c ->+        case IMap.lookup (fromInteger c) mp of+          Just con+            | isNullaryCon con -> pure (pp (conIdent con))+            | otherwise ->+              do vds <- traverse (>>= loop 1) (conFields con)+                 let d = pp (conIdent con) <+> hsep (Vector.toList vds)+                 pure (if prec > 0 then parens d else d)+          Nothing -> panic "ppEnumVal" ["Malformed enum value", show c]+      Nothing -> pure (text "[?]")+   ppWordVal :: WordValue sym -> SEval sym Doc   ppWordVal w = ppSWord x opts =<< asWordVal x w @@ -202,7 +242,7 @@                 Just str -> return $ text (show str)                 _ -> do vs' <- mapM (ppSWord x opts) vs                         return $ ppList vs'-      _ -> do ws' <- traverse loop ws+      _ -> do ws' <- traverse (loop 0) ws               return $ ppList ws'  ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc@@ -437,6 +477,12 @@   VRecord fs -> fs   _          -> evalPanic "fromVRecord" ["not a record", show val] +fromVEnum :: GenValue sym -> (SInteger sym, IntMap (ConValue sym))+fromVEnum val =+  case val of+    VEnum c xs -> (c,xs)+    _          -> evalPanic "fromVEnum" ["not an enum", show val]+ fromVFloat :: GenValue sym -> SFloat sym fromVFloat val =   case val of@@ -451,7 +497,7 @@     Nothing -> evalPanic "lookupRecord" ["malformed record", show val]  --- Merge and if/then/else+-- Merge and if/then/else and case  {-# INLINE iteValue #-} iteValue :: Backend sym =>@@ -465,6 +511,39 @@   | Just False <- bitAsLit sym b = y   | otherwise = mergeValue' sym b x y +data CaseCont sym = CaseCont+  { caseCon  :: Map Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))+  , caseDflt :: Maybe (SEval sym (GenValue sym))+  }++caseValue :: Backend sym =>+  sym ->+  SInteger sym ->+  IntMap (ConValue sym) ->+  CaseCont sym ->+  SEval sym (GenValue sym)+caseValue sym tag alts k+  | Just c <- integerAsLit sym tag =+    case IMap.lookup (fromInteger c) alts of+      Just conV -> doCase conV+      Nothing -> panic "caseValue" ["Missing constructor for tag", show c]+  | otherwise = foldr doSymCase (doDefault Nothing) (IMap.toList alts)+  where+  doSymCase (n,con) otherOpts =+    do expect <- integerLit sym (toInteger n)+       yes    <- intEq sym tag expect+       iteValue sym yes (doCase con) otherOpts++  doDefault mb =+    case caseDflt k of+      Just yes -> yes+      Nothing  -> raiseError sym (NoMatchingConstructor mb)++  doCase (ConInfo con fs) =+    case Map.lookup con (caseCon k) of+      Just yes -> yes (Vector.toList fs)+      Nothing  -> doDefault (Just $! unpackIdent con)+ {-# INLINE mergeValue' #-} mergeValue' :: Backend sym =>   sym ->@@ -474,6 +553,10 @@   SEval sym (GenValue sym) mergeValue' sym = mergeEval sym (mergeValue sym) +mergeConValue ::+  Backend sym => sym -> SBit sym -> ConValue sym -> ConValue sym -> ConValue sym+mergeConValue sym c = zipConInfo (mergeValue' sym c)+ mergeValue :: Backend sym =>   sym ->   SBit sym ->@@ -487,6 +570,11 @@          case res of            Left f -> panic "Cryptol.Eval.Value" [ "mergeValue: incompatible record values", show f ]            Right r -> pure (VRecord r)++    (VEnum c1 fs1, VEnum c2 fs2) ->+      VEnum <$> iteInteger sym c c1 c2+            <*> pure (IMap.unionWith (mergeConValue sym c) fs1 fs2)+     (VTuple vs1  , VTuple vs2  ) | length vs1 == length vs2  ->                                   pure $ VTuple $ zipWith (mergeValue' sym c) vs1 vs2     (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2

@@ -93,7 +93,7 @@ instance FreeVars DeclDef where   freeVars d = case d of                  DPrim -> mempty-                 DForeign _ -> mempty+                 DForeign _ me -> foldMap freeVars me                  DExpr e -> freeVars e  @@ -107,6 +107,8 @@       ESel e _          -> freeVars e       ESet ty e _ v     -> freeVars ty <> freeVars [e,v]       EIf e1 e2 e3      -> freeVars [e1,e2,e3]+      ECase e as d      -> freeVars e <> freeVars (Map.elems as)+                                      <> maybe mempty freeVars d       EComp t1 t2 e mss -> freeVars [t1,t2] <> rmVals (defs mss) (freeVars e)                                             <> mconcat (map foldFree mss)       EVar x            -> mempty { valDeps = Set.singleton x }@@ -117,12 +119,16 @@       EProofAbs p e     -> freeVars p <> freeVars e       EProofApp e       -> freeVars e       EWhere e ds       -> foldFree ds <> rmVals (defs ds) (freeVars e)-      EPropGuards guards _ -> mconcat [ freeVars e | (_, e) <- guards ]+      EPropGuards guards t -> mconcat [ freeVars e | (_, e) <- guards ]+                              <> freeVars t     where       foldFree :: (FreeVars a, Defs a) => [a] -> Deps       foldFree = foldr updateFree mempty       updateFree x rest = freeVars x <> rmVals (defs x) rest +instance FreeVars CaseAlt where+  freeVars (CaseAlt xs e) = foldr (rmVal . fst) (freeVars e) xs+ instance FreeVars Match where   freeVars m = case m of                  From _ t1 t2 e -> freeVars t1 <> freeVars t2 <> freeVars e@@ -142,7 +148,7 @@        TUser _ _ t -> freeVars t       TRec fs     -> freeVars (recordElements fs)-      TNewtype nt ts -> freeVars nt <> freeVars ts+      TNominal nt ts -> freeVars nt <> freeVars ts  instance FreeVars TVar where   freeVars tv = case tv of@@ -152,9 +158,22 @@ instance FreeVars TCon where   freeVars _tc = mempty -instance FreeVars Newtype where+instance FreeVars NominalType where   freeVars nt = foldr rmTParam base (ntParams nt)-    where base = freeVars (ntConstraints nt) <> freeVars (recordElements (ntFields nt))+    where base = freeVars (ntConstraints nt) <> freeVars (ntDef nt)++instance FreeVars NominalTypeDef where+  freeVars def =+    case def of+      Struct c -> freeVars c+      Enum cs -> freeVars cs+      Abstract -> mempty++instance FreeVars StructCon where+  freeVars c = freeVars (recordElements (ntFields c))++instance FreeVars EnumCon where+  freeVars c = freeVars (ecFields c)   --------------------------------------------------------------------------------

@@ -61,6 +61,9 @@       EIf e1 e2 e3      -> EIf <$> traverseNamesIP e1                                <*> traverseNamesIP e2                                <*> traverseNamesIP e3+      ECase e as d      -> ECase <$> traverseNamesIP e+                                 <*> traverse traverseNamesIP as+                                 <*> traverse traverseNamesIP d        EComp t1 t2 e mss -> EComp <$> traverseNamesIP t1                                  <*> traverseNamesIP t2@@ -82,6 +85,11 @@       EPropGuards gs t  -> EPropGuards <$> traverse doG gs <*> traverseNamesIP t         where doG (xs, e) = (,) <$> traverseNamesIP xs <*> traverseNamesIP e +instance TraverseNames CaseAlt where+  traverseNamesIP (CaseAlt xs e) =+    CaseAlt <$> traverse doPair xs <*> traverseNamesIP e+      where doPair (x,y) = (,) <$> traverseNamesIP x <*> traverseNamesIP y+ instance TraverseNames Match where   traverseNamesIP mat =     case mat of@@ -110,7 +118,7 @@   traverseNamesIP d =     case d of       DPrim   -> pure d-      DForeign t -> DForeign <$> traverseNamesIP t+      DForeign t me -> DForeign <$> traverseNamesIP t <*> traverseNamesIP me       DExpr e -> DExpr <$> traverseNamesIP e  instance TraverseNames Schema where@@ -138,7 +146,7 @@       TPSchemaParam x   -> TPSchemaParam  <$> traverseNamesIP x       TPTySynParam x    -> TPTySynParam   <$> traverseNamesIP x       TPPropSynParam x  -> TPPropSynParam <$> traverseNamesIP x-      TPNewtypeParam x  -> TPNewtypeParam <$> traverseNamesIP x+      TPNominalParam x  -> TPNominalParam <$> traverseNamesIP x       TPPrimParam x     -> TPPrimParam    <$> traverseNamesIP x  instance TraverseNames TVarInfo where@@ -167,6 +175,8 @@       TypeFromUserAnnotation      -> pure src       GeneratorOfListComp         -> pure src       TypeErrorPlaceHolder        -> pure src+      CasedExpression             -> pure src+      ConPat                      -> pure src  instance TraverseNames ArgDescr where   traverseNamesIP arg = mk <$> traverseNamesIP (argDescrFun arg)@@ -175,50 +185,53 @@ instance TraverseNames Type where   traverseNamesIP ty =     case ty of-      TCon tc ts    -> TCon <$> traverseNamesIP tc <*> traverseNamesIP ts+      TCon tc ts    -> TCon tc <$> traverseNamesIP ts       TVar x        -> TVar <$> traverseNamesIP x       TUser x ts t  -> TUser <$> traverseNamesIP x                              <*> traverseNamesIP ts                              <*> traverseNamesIP t-      TRec rm       -> TRec <$> traverseRecordMap (\_ -> traverseNamesIP) rm-      TNewtype nt ts -> TNewtype <$> traverseNamesIP nt <*> traverseNamesIP ts+      TRec rm       -> TRec <$> traverseRecordMap (const traverseNamesIP) rm+      TNominal nt ts -> TNominal <$> traverseNamesIP nt <*> traverseNamesIP ts  -instance TraverseNames TCon where-  traverseNamesIP tcon =-    case tcon of-      TC tc -> TC <$> traverseNamesIP tc-      _     -> pure tcon--instance TraverseNames TC where-  traverseNamesIP tc =-    case tc of-      TCAbstract ut -> TCAbstract <$> traverseNamesIP ut-      _             -> pure tc--instance TraverseNames UserTC where-  traverseNamesIP (UserTC x k) = UserTC <$> traverseNamesIP x <*> pure k- instance TraverseNames TVar where   traverseNamesIP tvar =     case tvar of       TVFree x k ys i -> TVFree x k <$> traverseNamesIP ys <*> traverseNamesIP i       TVBound x       -> TVBound <$> traverseNamesIP x -instance TraverseNames Newtype where-  traverseNamesIP nt = mk <$> traverseNamesIP (ntName nt)-                          <*> traverseNamesIP (ntParams nt)-                          <*> traverseNamesIP (ntConstraints nt)-                          <*> traverseNamesIP (ntConName nt)-                          <*> traverseRecordMap (\_ -> traverseNamesIP)-                                                (ntFields nt)-    where-    mk a b c d e = nt { ntName = a-                      , ntParams = b-                      , ntConstraints = c-                      , ntConName = d-                      , ntFields = e-                      }+instance TraverseNames NominalType where+  traverseNamesIP nt =+    NominalType+      <$> traverseNamesIP (ntName nt)+      <*> traverseNamesIP (ntParams nt)+      <*> pure (ntKind nt)+      <*> traverseNamesIP (ntConstraints nt)+      <*> traverseNamesIP (ntDef nt)+      <*> pure (ntFixity nt)+      <*> pure (ntDoc nt)++instance TraverseNames NominalTypeDef where+  traverseNamesIP def =+    case def of+      Struct c -> Struct <$> traverseNamesIP c+      Enum cs  -> Enum   <$> traverseNamesIP cs+      Abstract -> pure Abstract++instance TraverseNames StructCon where+  traverseNamesIP c =+    StructCon <$> traverseNamesIP (ntConName c)+              <*> traverseRecordMap (const traverseNamesIP) (ntFields c)++instance TraverseNames EnumCon where+  traverseNamesIP c =+    EnumCon <$> traverseNamesIP (ecName c)+            <*> pure (ecNumber c)+            <*> traverseNamesIP (ecFields c)+            <*> pure (ecPublic c)+            <*> pure (ecDoc c)++  instance TraverseNames ModTParam where   traverseNamesIP nt = mk <$> traverseNamesIP (mtpName nt)

@@ -54,7 +54,8 @@                                 , LoadedModuleG(..), lmInterface                                 , meCoreLint, CoreLint(..)                                 , ModContext(..), ModContextParams(..)-                                , ModulePath(..), modulePathLabel)+                                , ModulePath(..), modulePathLabel+                                , EvalForeignPolicy (..)) import           Cryptol.Backend.FFI import qualified Cryptol.Eval                 as E import qualified Cryptol.Eval.Concrete as Concrete@@ -79,7 +80,7 @@ import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName                            , preludeReferenceName, interactiveName, modNameChunks                            , modNameToNormalModName )-import Cryptol.Utils.PP (pretty)+import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) import Cryptol.Utils.Benchmark@@ -306,33 +307,46 @@       ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)     | null foreigns = pure Nothing     | otherwise =-      case path of-        InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=-          \case--            Right fsrc -> do-              unless quiet $-                case getForeignSrcPath fsrc of-                  Just fpath -> withLogger logPutStrLn $-                    "Loading dynamic library " ++ takeFileName fpath-                  Nothing -> pure ()-              modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>=-                \case-                  Right () -> pure $ Just fsrc-                  Left errs -> ffiLoadErrors (T.mName tcm) errs--            Left err -> ffiLoadErrors (T.mName tcm) [err]--        InMem m _ -> panic "doLoadModule"-          ["Can't find foreign source of in-memory module", m]+      getEvalForeignPolicy >>= \case+        AlwaysEvalForeign -> doEvalForeign (ffiLoadErrors (T.mName tcm))+        PreferEvalForeign -> doEvalForeign \errs ->+          withLogger logPrint $+            hang+              ("[warning] Could not load all foreign implementations for module"+                <+> pp (T.mName tcm) <.> colon) 4 $+              vcat (map pp errs)+              $$ "Fallback cryptol implementations will be used if available"+        NeverEvalForeign -> pure Nothing      where foreigns  = findForeignDecls tcm           foreignFs = T.findForeignDeclsInFunctors tcm           dups      = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)                                            $ sortBy (compare `on` nameIdent)                                            $ map fst foreigns ]+          doEvalForeign handleErrs =+            case path of+              InFile p -> io (loadForeignSrc p) >>=+                \case +                  Right fsrc -> do+                    unless quiet $+                      case getForeignSrcPath fsrc of+                        Just fpath -> withLogger logPutStrLn $+                          "Loading dynamic library " ++ takeFileName fpath+                        Nothing -> pure ()+                    (errs, ()) <-+                      modifyEvalEnvM (evalForeignDecls fsrc foreigns)+                    unless (null errs) $+                      handleErrs errs+                    pure $ Just fsrc +                  Left err -> do+                    handleErrs [err]+                    pure Nothing++              InMem m _ -> panic "doLoadModule"+                ["Can't find foreign source of in-memory module", m]+ -- | Rewrite an import declaration to be of the form: -- -- > import foo as foo [ [hiding] (a,b,c) ]@@ -434,27 +448,25 @@      findDepsOf mpath  findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)-findDepsOf mpath' =-  do mpath <- case mpath' of-                InFile file -> InFile <$> io (canonicalizePath file)-                InMem {}    -> pure mpath'-     (fp, incs, ms) <- parseModule mpath+findDepsOf mpath =+  do (fp, incs, ms) <- parseModule mpath      let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms)-     fpath <- if getAny anyF+     fdeps <- if getAny anyF                 then do mb <- io case mpath of-                                   InFile can -> foreignLibPath can-                                   InMem {}   -> pure Nothing+                                   InFile path -> foreignLibPath path+                                   InMem {}    -> pure Nothing                         pure case mb of-                               Nothing -> Set.empty-                               Just f  -> Set.singleton f-                else pure Set.empty+                               Nothing -> Map.empty+                               Just (fpath, exists) ->+                                 Map.singleton fpath exists+                else pure Map.empty      pure        ( mpath        , FileInfo            { fiFingerprint = fp            , fiIncludeDeps = incs            , fiImportDeps  = Set.fromList (map importedModule (appEndo imps []))-           , fiForeignDeps = fpath+           , fiForeignDeps = fdeps            }        ) @@ -605,12 +617,11 @@   renMod <- renameModule epgm  -{--  -- dump renamed+  {- dump renamed   unless (thing (mName (R.rmModule renMod)) == preludeName)        do (io $ print (T.pp renMod))           -- io $ exitSuccess---}+  --}     -- when generating the prim map for the typechecker, if we're checking the@@ -631,7 +642,11 @@   rewMod <- case tcm of               T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)               T.TCTopSignature {} -> pure tcm-  pure (R.rmInScope renMod,rewMod)+  let nameEnv = case tcm of+                  T.TCTopModule mo -> T.mInScope mo+                  -- Name env for signatures does not change after typechecking+                  T.TCTopSignature {} -> mInScope (R.rmModule renMod)+  pure (nameEnv,rewMod)  data TCLinter o = TCLinter   { lintCheck ::@@ -742,8 +757,7 @@     { T.inpRange            = r     , T.inpVars             = Map.map ifDeclSig (ifDecls env)     , T.inpTSyns            = ifTySyns env-    , T.inpNewtypes         = ifNewtypes env-    , T.inpAbstractTypes    = ifAbstractTypes env+    , T.inpNominalTypes     = ifNominalTypes env     , T.inpSignatures       = ifSignatures env     , T.inpNameSeeds        = seeds     , T.inpMonoBinds        = monoBinds

@@ -1,7 +1,6 @@ {-# Language BlockArguments #-} {-# Language RecordWildCards #-} {-# Language FlexibleInstances #-}-{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} module Cryptol.ModuleSystem.Binds   ( BindsNames@@ -13,6 +12,7 @@   , topModuleDefs   , topDeclsDefs   , newModParam+  , newFunctorInst   , InModule(..)   , ifaceToMod   , ifaceSigToMod@@ -25,7 +25,7 @@ import Data.Set(Set) import qualified Data.Set as Set import Data.Maybe(fromMaybe)-import Control.Monad(foldM)+import Control.Monad(foldM,forM) import qualified MonadLib as M  import Cryptol.Utils.Panic (panic)@@ -125,7 +125,7 @@   , modState     = ()   }   where-  env = modParamsNamingEnv ps+  env = modParamNamesNamingEnv ps   @@ -323,6 +323,7 @@       Decl d           -> namingEnv (InModule ns (tlValue d))       DPrimType d      -> namingEnv (InModule ns (tlValue d))       TDNewtype d      -> namingEnv (InModule ns (tlValue d))+      TDEnum d         -> namingEnv (InModule ns (tlValue d))       DParamDecl {}    -> mempty       Include _        -> mempty       DImport {}       -> mempty -- see 'openLoop' in the renamer@@ -363,10 +364,22 @@   namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $     do let Located { .. } = nName        ntName    <- newTop NSType  ns thing Nothing srcRange-       ntConName <- newTop NSValue ns thing Nothing srcRange+       ntConName <- newTop NSConstructor ns thing Nothing srcRange        return (singletonNS NSType thing ntName `mappend`-               singletonNS NSValue thing ntConName)+               singletonNS NSConstructor thing ntConName) +instance BindsNames (InModule (EnumDecl PName)) where+  namingEnv (InModule (Just ns) EnumDecl { .. }) = BuildNamingEnv $+    do enName   <- newTop NSType ns (thing eName) Nothing (srcRange eName)+       conNames <- forM eCons \topc ->+                      do let c     = ecName (tlValue topc)+                             pname = thing c+                         cName <- newTop NSConstructor ns pname Nothing+                                                                  (srcRange c)+                         pure (singletonNS NSConstructor pname cName)+       pure (mconcat (singletonNS NSType (thing eName) enName : conNames))+  namingEnv _ = panic "namingEnv" ["Unreachable"]+ -- | The naming environment for a single declaration. instance BindsNames (InModule (Decl PName)) where   namingEnv (InModule pfx d) = case d of@@ -400,6 +413,17 @@       SigTySyn ts _    -> namingEnv (InModule m (DType ts))       SigPropSyn ps _  -> namingEnv (InModule m (DProp ps)) +instance BindsNames (Pattern PName) where+  namingEnv pat =+    case pat of+      PVar x -> BuildNamingEnv (+        do y <- newLocal NSValue (thing x) (srcRange x)+           pure (singletonNS NSValue (thing x) y)+        )+      PCon _ xs     -> mconcat (map namingEnv xs)+      PLocated p _r -> namingEnv p+      PTyped p _t   -> namingEnv p+      _ -> panic "namingEnv" ["Unexpected pattern"]   @@ -419,6 +443,13 @@ -- to the signature. newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name newModParam m i rng n = liftSupply (mkModParam m i rng n)++-- | Given a name in a functor, make a fresh name for the corresponding thing in+-- the instantiation.+--+-- The 'ModPath' should be the instantiation not the functor.+newFunctorInst :: FreshM m => ModPath -> Name -> m Name+newFunctorInst m n = liftSupply (freshNameFor m n)   {- | Do something in the context of a module.

@@ -61,40 +61,43 @@  -- | This is the current state of the interpreter. data ModuleEnv = ModuleEnv-  { meLoadedModules :: LoadedModules+  { meLoadedModules     :: LoadedModules     -- ^ Information about all loaded modules.  See 'LoadedModule'.     -- Contains information such as the file where the module was loaded     -- from, as well as the module's interface, used for type checking. -  , meNameSeeds     :: T.NameSeeds+  , meNameSeeds         :: T.NameSeeds     -- ^ A source of new names for the type checker. -  , meEvalEnv       :: EvalEnv+  , meEvalEnv           :: EvalEnv     -- ^ The evaluation environment.  Contains the values for all loaded     -- modules, both public and private. -  , meCoreLint      :: CoreLint+  , meCoreLint          :: CoreLint     -- ^ Should we run the linter to ensure sanity. -  , meMonoBinds     :: !Bool+  , meMonoBinds         :: !Bool     -- ^ Are we assuming that local bindings are monomorphic.     -- XXX: We should probably remove this flag, and set it to 'True'.   -  , meFocusedModule :: Maybe ModName+  , meFocusedModule     :: Maybe ModName     -- ^ The "current" module.  Used to decide how to print names, for example. -  , meSearchPath    :: [FilePath]+  , meSearchPath        :: [FilePath]     -- ^ Where we look for things. -  , meDynEnv        :: DynamicEnv+  , meDynEnv            :: DynamicEnv     -- ^ This contains additional definitions that were made at the command     -- line, and so they don't reside in any module. -  , meSupply        :: !Supply+  , meSupply            :: !Supply     -- ^ Name source for the renamer +  , meEvalForeignPolicy :: EvalForeignPolicy+    -- ^ How to evaluate @foreign@ bindings.+   } deriving Generic  instance NFData ModuleEnv where@@ -105,6 +108,26 @@               | CoreLint          -- ^ Run core lint   deriving (Generic, NFData) +-- | How to evaluate @foreign@ bindings.+data EvalForeignPolicy+  -- | Use foreign implementation and report an error at module load time if it+  -- is unavailable.+  = AlwaysEvalForeign+  -- | Use foreign implementation by default, and when unavailable, fall back to cryptol implementation if present and report runtime error otherwise.+  | PreferEvalForeign+  -- | Always use cryptol implementation if present, and report runtime error+  -- otherwise.+  | NeverEvalForeign+  deriving Eq++defaultEvalForeignPolicy :: EvalForeignPolicy+defaultEvalForeignPolicy =+#ifdef FFI_ENABLED+  PreferEvalForeign+#else+  NeverEvalForeign+#endif+ resetModuleEnv :: ModuleEnv -> IO ModuleEnv resetModuleEnv env = do   for_ (getLoadedModules $ meLoadedModules env) $ \lm ->@@ -153,16 +176,17 @@                    ]    return ModuleEnv-    { meLoadedModules = mempty-    , meNameSeeds     = T.nameSeeds-    , meEvalEnv       = mempty-    , meFocusedModule = Nothing+    { meLoadedModules     = mempty+    , meNameSeeds         = T.nameSeeds+    , meEvalEnv           = mempty+    , meFocusedModule     = Nothing       -- we search these in order, taking the first match-    , meSearchPath    = searchPath-    , meDynEnv        = mempty-    , meMonoBinds     = True-    , meCoreLint      = NoCoreLint-    , meSupply        = emptySupply+    , meSearchPath        = searchPath+    , meDynEnv            = mempty+    , meMonoBinds         = True+    , meCoreLint          = NoCoreLint+    , meSupply            = emptySupply+    , meEvalForeignPolicy = defaultEvalForeignPolicy     }  -- | Try to focus a loaded module in the module environment.@@ -182,9 +206,9 @@ loadedNonParamModules :: ModuleEnv -> [T.Module] loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules -loadedNewtypes :: ModuleEnv -> Map Name T.Newtype-loadedNewtypes menv = Map.unions-   [ ifNewtypes (ifDefines i) <> ifNewtypes (ifDefines i)+loadedNominalTypes :: ModuleEnv -> Map Name T.NominalType+loadedNominalTypes menv = Map.unions+   [ ifNominalTypes (ifDefines i) <> ifNominalTypes (ifDefines i)    | i <- map lmInterface (getLoadedModules (meLoadedModules menv))    ] @@ -540,7 +564,7 @@   { fiFingerprint :: Fingerprint   , fiIncludeDeps :: Set FilePath   , fiImportDeps  :: Set ModName-  , fiForeignDeps :: Set FilePath+  , fiForeignDeps :: Map FilePath Bool   } deriving (Show,Generic,NFData)  @@ -555,9 +579,10 @@     { fiFingerprint = fp     , fiIncludeDeps = incDeps     , fiImportDeps  = impDeps-    , fiForeignDeps = fromMaybe Set.empty+    , fiForeignDeps = fromMaybe Map.empty                       do src <- fsrc-                         Set.singleton <$> getForeignSrcPath src+                         fpath <- getForeignSrcPath src+                         pure $ Map.singleton fpath True     }  @@ -599,8 +624,7 @@ deIfaceDecls :: DynamicEnv -> IfaceDecls deIfaceDecls DEnv { deDecls = dgs, deTySyns = tySyns } =     IfaceDecls { ifTySyns = tySyns-               , ifNewtypes = Map.empty-               , ifAbstractTypes = Map.empty+               , ifNominalTypes = Map.empty                , ifDecls = decls                , ifModules = Map.empty                , ifFunctors = Map.empty

@@ -11,7 +11,8 @@ import GHC.Generics (Generic)  import Cryptol.Parser.AST-import Cryptol.Parser.Names(namesD,tnamesD,namesNT,tnamesNT)+import Cryptol.Parser.Names+         (namesD,tnamesD,namesNT,tnamesNT,tnamesEnum,namesEnum) import Cryptol.ModuleSystem.Name  exportedDecls :: Ord name => [TopDecl name] -> ExportSpec name@@ -24,7 +25,9 @@               ++ map exportType (names tnamesD td)       DPrimType t -> [ exportType (thing . primTName <$> t) ]       TDNewtype nt -> map exportType (names tnamesNT nt) ++-                      map exportBind (names namesNT nt)+                      map exportCon (names namesNT nt)+      TDEnum en -> map exportType (names tnamesEnum en)+                ++ map exportCon (names namesEnum en)       Include {}  -> []       DImport {} -> []       DParamDecl {} -> []@@ -67,6 +70,10 @@ exportBind :: Ord name => TopLevel name -> ExportSpec name exportBind = exportName NSValue +-- | Add a constructor name to the export list, if it should be exported.+exportCon :: Ord name => TopLevel name -> ExportSpec name+exportCon = exportName NSConstructor+ -- | Add a type synonym name to the export list, if it should be exported. exportType :: Ord name => TopLevel name -> ExportSpec name exportType = exportName NSType@@ -81,7 +88,7 @@  -- | Check to see if a binding is exported. isExportedBind :: Ord name => name -> ExportSpec name -> Bool-isExportedBind = isExported NSValue+isExportedBind x s = isExported NSValue x s || isExported NSConstructor x s  -- | Check to see if a type synonym is exported. isExportedType :: Ord name => name -> ExportSpec name -> Bool

@@ -97,8 +97,7 @@ -- modules, but not things from nested functors, which are in `ifFunctors`. data IfaceDecls = IfaceDecls   { ifTySyns        :: Map.Map Name TySyn-  , ifNewtypes      :: Map.Map Name Newtype-  , ifAbstractTypes :: Map.Map Name AbstractType+  , ifNominalTypes  :: Map.Map Name NominalType   , ifDecls         :: Map.Map Name IfaceDecl   , ifModules       :: !(Map.Map Name (IfaceNames Name))   , ifSignatures    :: !(Map.Map Name ModParamNames)@@ -117,8 +116,7 @@ filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls filterIfaceDecls p ifs = IfaceDecls   { ifTySyns        = filterMap (ifTySyns ifs)-  , ifNewtypes      = filterMap (ifNewtypes ifs)-  , ifAbstractTypes = filterMap (ifAbstractTypes ifs)+  , ifNominalTypes  = filterMap (ifNominalTypes ifs)   , ifDecls         = filterMap (ifDecls ifs)   , ifModules       = filterMap (ifModules ifs)   , ifFunctors      = filterMap (ifFunctors ifs)@@ -130,8 +128,7 @@  ifaceDeclsNames :: IfaceDecls -> Set Name ifaceDeclsNames i = Set.unions [ Map.keysSet (ifTySyns i)-                               , Map.keysSet (ifNewtypes i)-                               , Map.keysSet (ifAbstractTypes i)+                               , Map.keysSet (ifNominalTypes i)                                , Map.keysSet (ifDecls i)                                , Map.keysSet (ifModules i)                                , Map.keysSet (ifFunctors i)@@ -142,8 +139,7 @@ instance Semigroup IfaceDecls where   l <> r = IfaceDecls     { ifTySyns   = Map.union (ifTySyns l)   (ifTySyns r)-    , ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r)-    , ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r)+    , ifNominalTypes = Map.union (ifNominalTypes l) (ifNominalTypes r)     , ifDecls    = Map.union (ifDecls l)    (ifDecls r)     , ifModules  = Map.union (ifModules l)  (ifModules r)     , ifFunctors = Map.union (ifFunctors l) (ifFunctors r)@@ -153,8 +149,7 @@ instance Monoid IfaceDecls where   mempty      = IfaceDecls                   { ifTySyns = mempty-                  , ifNewtypes = mempty-                  , ifAbstractTypes = mempty+                  , ifNominalTypes = mempty                   , ifDecls = mempty                   , ifModules = mempty                   , ifFunctors = mempty@@ -163,8 +158,7 @@   mappend = (<>)   mconcat ds  = IfaceDecls     { ifTySyns   = Map.unions (map ifTySyns   ds)-    , ifNewtypes = Map.unions (map ifNewtypes ds)-    , ifAbstractTypes = Map.unions (map ifAbstractTypes ds)+    , ifNominalTypes = Map.unions (map ifNominalTypes ds)     , ifDecls    = Map.unions (map ifDecls    ds)     , ifModules  = Map.unions (map ifModules ds)     , ifFunctors = Map.unions (map ifFunctors ds)@@ -194,8 +188,8 @@  ifaceDeclsPrimMap :: IfaceDecls -> PrimMap ifaceDeclsPrimMap IfaceDecls { .. } =-  PrimMap { primDecls = Map.fromList (newtypes ++ exprs)-          , primTypes = Map.fromList (newtypes ++ types)+  PrimMap { primDecls = Map.fromList (nominalVs ++ exprs)+          , primTypes = Map.fromList (nominalTs ++ types)           }   where   entry n = case asPrim n of@@ -205,9 +199,13 @@                           [ "Top level name not declared in a module?"                           , show n ] -  newtypes = map entry (Map.keys ifNewtypes)-  exprs    = map entry (Map.keys ifDecls)-  types    = map entry (Map.keys ifTySyns)+  nominalTs = map entry (Map.keys ifNominalTypes)+  nominalVs = [ entry n+              | nt <- Map.elems ifNominalTypes+              , (n,_) <- nominalTypeConTypes nt+              ]+  exprs     = map entry (Map.keys ifDecls)+  types     = map entry (Map.keys ifTySyns)   -- | Given an interface computing a map from original names to actual names,@@ -227,10 +225,12 @@    decls       = ifDefines ifa   from f      = Map.keysSet (f decls)-  tyNames     = Set.unions [ from ifTySyns, from ifNewtypes, from ifAbstractTypes ]+  tyNames     = Set.unions [ from ifTySyns, from ifNominalTypes ]   moNames     = Set.unions [ from ifModules, from ifSignatures, from ifFunctors ]   vaNames     = Set.unions [ newtypeCons, from ifDecls ]-  newtypeCons = Set.fromList (map ntConName (Map.elems (ifNewtypes decls)))+  newtypeCons = Set.fromList+                  (concatMap conNames (Map.elems (ifNominalTypes decls)))+    where conNames = map fst . nominalTypeConTypes   

@@ -508,6 +508,9 @@ getMonoBinds :: ModuleM Bool getMonoBinds  = ModuleT (meMonoBinds `fmap` get) +getEvalForeignPolicy :: ModuleM EvalForeignPolicy+getEvalForeignPolicy = ModuleT (meEvalForeignPolicy <$> get)+ setMonoBinds :: Bool -> ModuleM () setMonoBinds b = ModuleT $ do   env <- get@@ -571,8 +574,8 @@   do act <- getEvalOptsAction      liftIO act -getNewtypes :: ModuleM (Map T.Name T.Newtype)-getNewtypes = ModuleT (loadedNewtypes <$> get)+getNominalTypes :: ModuleM (Map T.Name T.NominalType)+getNominalTypes = ModuleT (loadedNominalTypes <$> get)  getFocusedModule :: ModuleM (Maybe P.ModName) getFocusedModule  = ModuleT (meFocusedModule `fmap` get)

@@ -29,6 +29,7 @@   , nameLoc   , nameFixity   , nameNamespace+  , nameToDefPName   , asPrim   , asOrigName   , nameModPath@@ -70,7 +71,8 @@ import           Data.Char(isAlpha,toUpper)  -+import           Cryptol.Parser.Name (PName)+import qualified Cryptol.Parser.Name as PName import           Cryptol.Parser.Position (Range,Located(..)) import           Cryptol.Utils.Fixity import           Cryptol.Utils.Ident@@ -146,9 +148,9 @@                  NotInScope  ->                     let m = Text.pack (show (pp (ogModule og)))                     in-                    case ogSource og of-                      FromModParam q  -> m <> "::" <> Text.pack (show (pp q))-                      _ -> m+                    case ogFromParam og of+                      Just q  -> m <> "::" <> Text.pack (show (pp q))+                      Nothing -> m    -- Note that this assumes that `xs` is `l` and `ys` is `r`   cmpText xs ys =@@ -227,12 +229,21 @@ nameFixity :: Name -> Maybe Fixity nameFixity = nFixity +-- | Compute a `PName` for the definition site corresponding to the given+-- `Name`.   Usually this is an unqualified name, but names that come+-- from module parameters are qualified with the corresponding parameter name.+nameToDefPName :: Name -> PName+nameToDefPName n =+  case nInfo n of+    GlobalName _ og -> PName.origNameToDefPName og+    LocalName _ txt -> PName.mkUnqual txt+ -- | Primtiives must be in a top level module, at least for now. asPrim :: Name -> Maybe PrimIdent asPrim n =   case nInfo n of     GlobalName _ og-      | TopModule m <- ogModule og, not (ogFromModParam og) ->+      | TopModule m <- ogModule og, not (ogIsModParam og) ->         Just $ PrimIdent m $ identText $ ogName og      _ -> Nothing@@ -371,6 +382,7 @@                                 , ogModule    = m                                 , ogName      = ident                                 , ogSource    = FromDefinition+                                , ogFromParam = Nothing                                 }               } @@ -410,7 +422,8 @@                               { ogModule    = own                               , ogName      = nameIdent n                               , ogNamespace = nameNamespace n-                              , ogSource    = FromModParam pname+                              , ogSource    = FromModParam+                              , ogFromParam = Just pname                               }               , nFixity = nFixity n               , nLoc    = rng

@@ -6,14 +6,14 @@ -- Stability   :  provisional -- Portability :  portable -{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE BlockArguments #-}-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}-module Cryptol.ModuleSystem.NamingEnv where+module Cryptol.ModuleSystem.NamingEnv+  ( module Cryptol.ModuleSystem.NamingEnv.Types+  , module Cryptol.ModuleSystem.NamingEnv+  ) where  import Data.Maybe (mapMaybe,maybeToList) import           Data.Map.Strict (Map)@@ -22,9 +22,6 @@ import qualified Data.Set as Set import           Data.Foldable(foldl') -import GHC.Generics (Generic)-import Control.DeepSeq(NFData)- import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Ident(allNamespaces)@@ -34,24 +31,7 @@ import Cryptol.ModuleSystem.Names import Cryptol.ModuleSystem.Interface ---- | The 'NamingEnv' is used by the renamer to determine what--- identifiers refer to.-newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names))-  deriving (Show,Generic,NFData)--instance Monoid NamingEnv where-  mempty = NamingEnv Map.empty-  {-# INLINE mempty #-}--instance Semigroup NamingEnv where-  NamingEnv l <> NamingEnv r =-    NamingEnv (Map.unionWith (Map.unionWith (<>)) l r)--instance PP NamingEnv where-  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps-    where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs)))-          ppNm (x,as)  = pp x <+> "->" <+> commaSep (map pp (namesToList as))+import Cryptol.ModuleSystem.NamingEnv.Types   {- | This "joins" two naming environments by matching the text name.@@ -91,14 +71,16 @@     Just (One x) -> Set.singleton x     Just (Ambig as) -> as --- | Get a unqualified naming environment for the given names+-- | Get a naming environment for the given names.  The `PName`s correspond+-- to the definition sites of the corresponding `Name`s, so typically they+-- will be unqualified.  The exception is for names that comre from parameters,+-- which are qualified with the relevant parameter. namingEnvFromNames :: Set Name -> NamingEnv namingEnvFromNames xs = NamingEnv (foldl' add mempty xs)   where   add mp x = let ns = nameNamespace x-                 txt = nameIdent x              in Map.insertWith (Map.unionWith (<>))-                               ns (Map.singleton (mkUnqual txt) (One x))+                               ns (Map.singleton (nameToDefPName x) (One x))                                mp  @@ -191,11 +173,13 @@ -- | Find the ambiguous entries in an environmet. -- A name is ambiguous if it might refer to multiple entities. findAmbig :: NamingEnv -> [ [Name] ]-findAmbig (NamingEnv ns) =+findAmbig env =   [ Set.toList xs   | mp <- Map.elems ns   , Ambig xs <- Map.elems mp   ]+  where+  NamingEnv ns = consToValues env  -- | Get the subset of the first environment that shadows something -- in the second one.@@ -231,8 +215,8 @@  -- | Compute an unqualified naming environment, containing the various module -- parameters.-modParamsNamingEnv :: T.ModParamNames -> NamingEnv-modParamsNamingEnv T.ModParamNames { .. } =+modParamNamesNamingEnv :: T.ModParamNames -> NamingEnv+modParamNamesNamingEnv T.ModParamNames { .. } =   NamingEnv $ Map.fromList     [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns)     , (NSType,  Map.fromList $ map fromTS (Map.elems mpnTySyn) ++@@ -248,12 +232,17 @@    fromTS ts = (toPName (T.tsName ts), One (T.tsName ts)) +-- | Compute a naming environment from a module parameter, qualifying it+-- according to 'mpQual'.+modParamNamingEnv :: T.ModParam -> NamingEnv+modParamNamingEnv mp = maybe id qualify (T.mpQual mp) $+  modParamNamesNamingEnv (T.mpParameters mp)  -- | Generate a naming environment from a declaration interface, where none of -- the names are qualified. unqualifiedEnv :: IfaceDecls -> NamingEnv unqualifiedEnv IfaceDecls { .. } =-  mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs, mods, sigs ]+  mconcat [ exprs, tySyns, ntTypes, ntExprs, mods, sigs ]   where   toPName n = mkUnqual (nameIdent n) @@ -264,19 +253,16 @@                     | n <- Map.keys ifTySyns ]    ntTypes = mconcat [ n-                    | nt <- Map.elems ifNewtypes-                    , let tname = T.ntName nt-                          cname = T.ntConName nt-                    , n  <- [ singletonNS NSType (toPName tname) tname-                            , singletonNS NSValue (toPName cname) cname+                    | nt <- Map.elems ifNominalTypes+                    , let tname  = T.ntName nt+                    , n  <- singletonNS NSType (toPName tname) tname+                          : [ singletonNS NSValue (toPName cname) cname+                            | cname <-map fst (T.nominalTypeConTypes nt)                             ]                     ] -  absTys  = mconcat [ singletonNS NSType (toPName n) n-                    | n <- Map.keys ifAbstractTypes ]-   ntExprs = mconcat [ singletonNS NSValue (toPName n) n-                    | n <- Map.keys ifNewtypes ]+                    | n <- Map.keys ifNominalTypes ]    mods    = mconcat [ singletonNS NSModule (toPName n) n                     | n <- Map.keys ifModules ]

@@ -0,0 +1,43 @@+{-# LANGUAGE DeriveAnyClass    #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE OverloadedStrings #-}++module Cryptol.ModuleSystem.NamingEnv.Types where++import           Data.Map.Strict            (Map)+import qualified Data.Map.Strict            as Map++import           Control.DeepSeq            (NFData)+import           GHC.Generics               (Generic)++import           Cryptol.ModuleSystem.Names+import           Cryptol.Parser.Name+import           Cryptol.Utils.Ident+import           Cryptol.Utils.PP++-- | The 'NamingEnv' is used by the renamer to determine what+-- identifiers refer to.+newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names))+  deriving (Show,Generic,NFData)++instance Monoid NamingEnv where+  mempty = NamingEnv Map.empty+  {-# INLINE mempty #-}++instance Semigroup NamingEnv where+  NamingEnv l <> NamingEnv r =+    NamingEnv (Map.unionWith (Map.unionWith (<>)) l r)++instance PP NamingEnv where+  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps+    where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs)))+          ppNm (x,as)  = pp x <+> "->" <+> commaSep (map pp (namesToList as))++-- | Move names in the constructor namespace to the value namespace.+-- This is handy when checking for ambiguities.+consToValues :: NamingEnv -> NamingEnv+consToValues (NamingEnv mps) =+  NamingEnv $+  case Map.updateLookupWithKey (\_ _ -> Nothing) NSConstructor mps of+    (Nothing, mp1) -> mp1+    (Just conMap, mp1) -> Map.insertWith (Map.unionWith (<>)) NSValue conMap mp1

@@ -118,7 +118,6 @@ data RenamedModule = RenamedModule   { rmModule   :: Module Name     -- ^ The renamed module   , rmDefines  :: NamingEnv       -- ^ What this module defines-  , rmInScope  :: NamingEnv       -- ^ What's in scope in this module   , rmImported :: IfaceDecls     -- ^ Imported declarations.  This provides the types for external     -- names (used by the type-checker).@@ -152,12 +151,11 @@       setResolvedLocals resolvedMods $        setNestedModule pathToName-       do (ifs,(inScope,m1)) <- collectIfaceDeps (renameModule' mname m)+       do (ifs,m1) <- collectIfaceDeps (renameModule' mname m)           env <- rmodDefines <$> lookupResolved mname           pure RenamedModule                  { rmModule = m1                  , rmDefines = env-                 , rmInScope = inScope                  , rmImported = ifs                   -- XXX: maybe we should keep the nested defines too?                  }@@ -220,12 +218,9 @@ renameModule' ::   ImpName Name {- ^ Resolved name for this module -} ->   ModuleG mname PName ->-  RenameM (NamingEnv, ModuleG mname Name)+  RenameM (ModuleG mname Name) renameModule' mname m =-  setCurMod-    case mname of-      ImpTop r    -> TopModule r-      ImpNested r -> Nested (nameModPath r) (nameIdent r)+  setCurMod (impNameModPath mname)    do resolved <- lookupResolved mname      shadowNames' CheckNone (rmodImports resolved)@@ -247,7 +242,7 @@                      let exports = exportedDecls ds1                      mapM_ recordUse (exported NSType exports)                      inScope <- getNamingEnv-                     pure (inScope, m { mDef = NormalModule ds1 })+                     pure m { mDef = NormalModule ds1, mInScope = inScope }           -- The things defined by this module are the *results*          -- of the instantiation, so we should *not* add them@@ -260,30 +255,20 @@               let l = Just (srcRange f')               imap <- mkInstMap l mempty (thing f') mname -              {- Now we need to compute what's "in scope" of the instantiated-              module.  This is used when the module is loaded at the command-              line and users want to evalute things in the context of the-              module -}-              fuEnv <- if isFakeName (thing f')-                          then pure mempty-                          else lookupDefines (thing f')-              let ren x = Map.findWithDefault x x imap--              -- XXX: This is not quite right as it only considers the things-              -- defined in the module to be in scope.  It misses things-              -- that are *imported* by the functor, in particular the Cryptol-              -- library-              -- is missing.  See #1455.-              inScope <- shadowNames' CheckNone (mapNamingEnv ren fuEnv)-                         getNamingEnv+              -- This inScope is incomplete; it only contains names from the+              -- enclosing scope, but we also want the names in scope from the+              -- functor, for ease of testing at the command line. We will fix+              -- this up in doFunctorInst in the typechecker, because right now+              -- we don't have access yet to the inScope of the functor.+              inScope <- getNamingEnv -              pure (inScope, m { mDef = FunctorInstance f' as' imap })+              pure m { mDef = FunctorInstance f' as' imap, mInScope = inScope }           InterfaceModule s ->            shadowNames' CheckNone (rmodDefines resolved)              do d <- InterfaceModule <$> renameIfaceModule mname s                 inScope <- getNamingEnv-                pure (inScope, m { mDef = d })+                pure m { mDef = d, mInScope = inScope }   checkFunctorArgs :: ModuleInstanceArgs Name -> RenameM ()@@ -547,6 +532,7 @@       Decl tl                 -> isValDecl (tlValue tl)       DPrimType {}            -> False       TDNewtype {}            -> False+      TDEnum {}               -> False       DParamDecl {}           -> False       DInterfaceConstraint {} -> False @@ -599,6 +585,9 @@     DPrimType d             -> hasName (thing (primTName (tlValue d)))     TDNewtype d             -> hasName' (thing (nName (tlValue d)))                                         [ nConName (tlValue d) ]+    TDEnum d                -> hasName' (thing (eName (tlValue d)))+                                        (map (thing . ecName . tlValue)+                                             (eCons (tlValue d)))     DModule d               -> hasName (thing (mName m))       where NestedModule m = tlValue d @@ -696,9 +685,10 @@       forM_ repeated \ps ->        case ps of+         [] -> panic "doModParams" ["[]"]          [_]      -> pure ()-         ~(p : _) -> recordError (MultipleModParams (renModParamName p)-                                                    (map renModParamRange ps))+         (p : _) -> recordError (MultipleModParams (renModParamName p)+                                                   (map renModParamRange ps))       pure (mconcat paramEnvs,params) @@ -723,6 +713,7 @@       Decl d            -> Decl      <$> traverse rename d       DPrimType d       -> DPrimType <$> traverse rename d       TDNewtype n       -> TDNewtype <$> traverse rename n+      TDEnum n          -> TDEnum    <$> traverse rename n       Include n         -> return (Include n)       DModule m  -> DModule <$> traverse rename m       DImport li -> DImport <$> renI li@@ -820,10 +811,8 @@            nm             = thing lnm        n   <- resolveName NameBind NSModule nm        depsOf (NamedThing n)-         do -- XXX: we should store in scope somewhere if we want to browse-            -- nested modules properly-            let m' = m { mName = ImpNested <$> mName m }-            (_inScope,m1) <- renameModule' (ImpNested n) m'+         do let m' = m { mName = ImpNested <$> mName m }+            m1 <- renameModule' (ImpNested n) m'             pure (NestedModule m1 { mName = lnm { thing = n } })  @@ -881,7 +870,7 @@   rename n      =     shadowNames (nParams n) $     do nameT <- rnLocated (renameType NameBind) (nName n)-       nameC <- renameVar  NameBind (nConName n)+       nameC <- renameCon NameBind (nConName n)         depsOf (NamedThing nameC) (addDep (thing nameT)) @@ -893,9 +882,28 @@                            , nParams = ps'                            , nBody   = body' } -+instance Rename EnumDecl where+  rename n =+    shadowNames (eParams n) $+    do nameT  <- rnLocated (renameType NameBind) (eName n)+       nameCs <- forM (eCons n) \tlEc ->+                   do let con = tlValue tlEc+                      nameC <- rnLocated (renameCon NameBind) (ecName con)+                      depsOf (NamedThing (thing nameC)) (addDep (thing nameT))+                      pure (nameC,tlEc)+       depsOf (NamedThing (thing nameT)) $+         do ps' <- traverse rename (eParams n)+            cons <- forM nameCs \(c,tlEc) ->+                     do ts' <- traverse rename (ecFields (tlValue tlEc))+                        let con = EnumCon { ecName = c, ecFields = ts' }+                        pure tlEc { tlValue = con }+            pure EnumDecl { eName = nameT+                          , eParams = ps'+                          , eCons = cons+                          } --- | Try to resolve a name+-- | Try to resolve a name.+-- SPECIAL CASE: if we have a NameUse for NSValue, we also look in NSConstructor resolveNameMaybe :: NameType -> Namespace -> PName -> RenameM (Maybe Name) resolveNameMaybe nt expected qn =   do ro <- RenameM ask@@ -903,7 +911,14 @@          use = case expected of                  NSType -> recordUse                  _      -> const (pure ())-     case lkpIn expected of+         checkCon = case (nt,expected) of+                      (NameUse, NSValue) -> lkpIn NSConstructor+                      _ -> Nothing+         found = case (lkpIn expected, checkCon) of+                   (Just a, Just b) -> Just (a <> b)+                   (Nothing, y)     -> y+                   (x, Nothing)     -> x+     case found of        Just xs ->          case xs of           One n ->@@ -948,7 +963,7 @@         Nothing -> False  --- | Resolve a name, and report error on failure+-- | Resolve a name, and report error on failure. resolveName :: NameType -> Namespace -> PName -> RenameM Name resolveName nt expected qn =   do mb <- resolveNameMaybe nt expected qn@@ -960,6 +975,9 @@ renameVar :: NameType -> PName -> RenameM Name renameVar nt = resolveName nt NSValue +renameCon :: NameType -> PName -> RenameM Name+renameCon nt = resolveName nt NSConstructor+ renameType :: NameType -> PName -> RenameM Name renameType nt = resolveName nt NSType @@ -1063,8 +1081,11 @@                           }  instance Rename BindDef where-  rename DPrim     = return DPrim-  rename DForeign  = return DForeign+  rename DPrim        = return DPrim+  rename (DForeign i) = DForeign <$> traverse rename i+  rename (DImpl i)    = DImpl <$> rename i++instance Rename BindImpl where   rename (DExpr e) = DExpr <$> rename e   rename (DPropGuards cases) = DPropGuards <$> traverse rename cases @@ -1072,10 +1093,11 @@   rename g = PropGuardCase <$> traverse (rnLocated rename) (pgcProps g)                            <*> rename (pgcExpr g) --- NOTE: this only renames types within the pattern. instance Rename Pattern where   rename p      = case p of     PVar lv         -> PVar <$> rnLocated (renameVar NameBind) lv+    PCon c ps       -> PCon <$> rnLocated (renameCon NameUse)  c+                            <*> traverse rename ps     PWild           -> pure PWild     PTuple ps       -> PTuple   <$> traverse rename ps     PRecord nps     -> PRecord  <$> traverse (traverse rename) nps@@ -1153,6 +1175,7 @@     EApp f x        -> EApp    <$> rename f  <*> rename x     EAppT f ti      -> EAppT   <$> rename f  <*> traverse rename ti     EIf b t f       -> EIf     <$> rename b  <*> rename t  <*> rename f+    ECase e as      -> ECase   <$> rename e  <*> traverse rename as     EWhere e' ds    -> shadowNames (map (InModule Nothing) ds) $                           EWhere <$> rename e' <*> renameDecls ds     ETyped e' ty    -> ETyped  <$> rename e' <*> rename ty@@ -1326,7 +1349,7 @@     do n <- liftSupply (mkLocal NSValue (getIdent thing) srcRange)        -- XXX: for deps, we should record a use        return (singletonNS NSValue thing n)-+  go (PCon _ ps)      = bindVars ps   go PWild            = return mempty   go (PTuple ps)      = bindVars ps   go (PRecord fs)     = bindVars (fmap snd (recordElements fs))@@ -1389,6 +1412,8 @@          do res <- bindTypes ts             return (env' `mappend` res) +instance Rename CaseAlt where+  rename (CaseAlt p e) = shadowNames p (CaseAlt <$> rename p <*> rename e)  instance Rename Match where   rename m = case m of@@ -1416,8 +1441,6 @@     doc =       vcat [ "// --- Defines -----------------------------"            , pp (rmDefines rn)-           , "// --- In scope ----------------------------"-           , pp (rmInScope rn)            , "// -- Module -------------------------------"            , pp (rmModule rn)            , "// -----------------------------------------"

@@ -119,6 +119,7 @@                     NSValue   -> "Value"                     NSType    -> "Type"                     NSModule  -> "Module"+                    NSConstructor -> "Constructor"      OverlappingSyms qns ->       hang (text "[error]")@@ -134,6 +135,7 @@         where         sayNS ns = case ns of                      NSValue  -> "value"+                     NSConstructor -> "constructor"                      NSType   -> "type"                      NSModule -> "module"         suggestion =@@ -141,6 +143,8 @@              (NSValue,NSType) ->                 ["Did you mean `(" <.> pp (thing lqn) <.> text")?"]+            (NSConstructor,NSValue) ->+                ["Perhaps the constructor got shadowed?"]             _ -> []      FixityError o1 f1 o2 f2 ->@@ -159,13 +163,16 @@       ppLab as = ppNestedSels (thing as) <+> "at" <+> pp (srcRange as)      InvalidDependency ds ->-      hang "[error] Invalid recursive dependency:"+      hang ("[error] Invalid" <+> self <+>"dependency:")          4 (vcat [ "•" <+> pp x <.>                     case depNameLoc x of                       Just r -> ", defined at" <+> ppR r                       Nothing -> mempty                  | x <- ds ])       where ppR r = pp (from r) <.> "--" <.> pp (to r)+            self = case ds of+                     [_] -> "self"+                     _   -> "recursive"      MultipleModParams x rs ->       hang ("[error] Multiple parameters with name" <+> backticks (pp x))@@ -195,6 +202,7 @@           NSModule -> "submodule" <+> pp n           NSType   -> "type" <+> pp n           NSValue  -> pp n+          NSConstructor -> "constructor" <+> pp n       ModParamName _r i -> "module parameter" <+> pp i       ModPath mp ->         case modPathSplit mp of

@@ -67,10 +67,11 @@  import Cryptol.Parser.AST   ( ImportG(..),PName, ModuleInstanceArgs(..), ImpName(..) )-import Cryptol.ModuleSystem.Binds (Mod(..), TopDef(..), modNested, ModKind(..))+import Cryptol.ModuleSystem.Binds+          ( Mod(..), TopDef(..), modNested, ModKind(..), newFunctorInst ) import Cryptol.ModuleSystem.Name-          ( Name, Supply, SupplyT, runSupplyT, liftSupply, freshNameFor-          , asOrigName, nameIdent, nameTopModule )+          ( Name, Supply, SupplyT, runSupplyT, asOrigName, nameIdent+          , nameTopModule ) import Cryptol.ModuleSystem.Names(Names(..)) import Cryptol.ModuleSystem.NamingEnv           ( NamingEnv(..), lookupNS, shadowing, travNamingEnv@@ -511,7 +512,7 @@    instName :: Name -> SupplyT (M.StateT (Set (Name,Name)) M.Id) Name   instName x =-    do y <- liftSupply (freshNameFor mpath x)+    do y <- newFunctorInst mpath x        when (x `Set.member` rmodNested def)             (M.lift (M.sets_ (Set.insert (x,y))))        pure y

@@ -76,6 +76,7 @@    'type'      { Located $$ (Token (KW KW_type   ) _)}   'newtype'   { Located $$ (Token (KW KW_newtype) _)}+  'enum'      { Located $$ (Token (KW KW_enum) _)}   'module'    { Located $$ (Token (KW KW_module ) _)}   'submodule' { Located $$ (Token (KW KW_submodule ) _)}   'where'     { Located $$ (Token (KW KW_where  ) _)}@@ -83,6 +84,8 @@   'if'        { Located $$ (Token (KW KW_if     ) _)}   'then'      { Located $$ (Token (KW KW_then   ) _)}   'else'      { Located $$ (Token (KW KW_else   ) _)}+  'case'      { Located $$ (Token (KW KW_case) _)}+  'of'        { Located $$ (Token (KW KW_of) _)}   'interface' { Located $$ (Token (KW KW_interface) _)}   'x'         { Located $$ (Token (KW KW_x)       _)}   'down'      { Located $$ (Token (KW KW_down)    _)}@@ -280,11 +283,12 @@   : decl                   { [exportDecl Nothing   Public $1]                 }   | doc decl               { [exportDecl (Just $1) Public $2]                 }   | mbDoc 'include' STRLIT {% (return . Include) `fmap` fromStrLit $3         }-  | mbDoc 'property' name apats '=' expr+  | mbDoc 'property' name iapats '=' expr                            { [exportDecl $1 Public (mkProperty $3 $4 $6)]     }   | mbDoc 'property' name       '=' expr                            { [exportDecl $1 Public (mkProperty $3 [] $5)]     }   | mbDoc newtype          { [exportNewtype Public $1 $2]                     }+  | mbDoc enum             { [exportEnum Public $1 $2]                        }   | prim_bind              { $1                                               }   | foreign_bind           { $1                                               }   | private_decls          { $1                                               }@@ -367,18 +371,18 @@   : vars_comma ':' schema  { at (head $1,$3) $ DSignature (reverse $1) $3   }   | ipat '=' expr          { at ($1,$3) $ DPatBind $1 $3                    }   | '(' op ')' '=' expr    { at ($1,$5) $ DPatBind (PVar $2) $5             }-  | var apats_indices propguards_cases+  | var iapats_indices propguards_cases                            {% mkPropGuardsDecl $1 $2 $3 }   | var propguards_cases                            {% mkConstantPropGuardsDecl $1 $2 }-  | var apats_indices '=' expr+  | var iapats_indices '=' expr                            { at ($1,$4) $ mkIndexedDecl $1 $2 $4 } -  | apat pat_op apat '=' expr+  | iapat pat_op iapat '=' expr                            { at ($1,$5) $                              DBind $ Bind { bName      = $2                                           , bParams    = [$1,$3]-                                          , bDef       = at $5 (Located emptyRange (DExpr $5))+                                          , bDef       = at $5 (Located emptyRange (exprDef $5))                                           , bSignature = Nothing                                           , bPragmas   = []                                           , bMono      = False@@ -402,13 +406,13 @@  let_decl                :: { Decl PName }   : 'let' ipat '=' expr               { at ($2,$4) $ DPatBind $2 $4                    }-  | 'let' var apats_indices '=' expr  { at ($2,$5) $ mkIndexedDecl $2 $3 $5 }+  | 'let' var iapats_indices '=' expr  { at ($2,$5) $ mkIndexedDecl $2 $3 $5 }   | 'let' '(' op ')' '=' expr         { at ($2,$6) $ DPatBind (PVar $3) $6             }-  | 'let' apat pat_op apat '=' expr+  | 'let' iapat pat_op iapat '=' expr                            { at ($2,$6) $                              DBind $ Bind { bName      = $3                                           , bParams    = [$2,$4]-                                          , bDef       = at $6 (Located emptyRange (DExpr $6))+                                          , bDef       = at $6 (Located emptyRange (exprDef $6))                                           , bSignature = Nothing                                           , bPragmas   = []                                           , bMono      = False@@ -453,6 +457,19 @@   : '{' '}'                {% mkRecord (rComb $1 $2) (Located emptyRange) [] }   | '{' field_types '}'    {% mkRecord (rComb $1 $3) (Located emptyRange) $2 } ++enum                              :: { EnumDecl PName }+  : 'enum' type '=' enum_body        {% mkEnumDecl $2 $4 }++enum_body                         :: { [TopLevel (EnumCon PName)] }+  :     enum_con                     { [$1] }+  | '|' enum_con                     { [$2] }+  | enum_body '|' enum_con           { $3 : $1 }++enum_con                           :: { TopLevel (EnumCon PName) }+  : app_type                          {% mkConDecl Nothing   Public $1 }+  | doc  app_type                     {% mkConDecl (Just $1) Public $2 }+ vars_comma                 :: { [ LPName ]  }   : var                       { [ $1]      }   | vars_comma ',' var        { $3 : $1    }@@ -461,26 +478,6 @@   : name                      { $1 }   | '(' op ')'                { $2 } -apats                   :: { [Pattern PName] }-  : apat                   { [$1] }-  | apats apat             { $2 : $1 }--indices                 :: { [Pattern PName] }-  : '@' indices1           { $2 }-  | {- empty -}            { [] }--indices1                :: { [Pattern PName] }-  : apat                   { [$1] }-  | indices1 '@' apat      { $3 : $1 }--apats_indices           :: { ([Pattern PName], [Pattern PName]) }-  : apats indices          { ($1, $2) }-  | '@' indices1           { ([], $2) }--opt_apats_indices       :: { ([Pattern PName], [Pattern PName]) }-  : {- empty -}            { ([],[]) }-  | apats_indices          { $1 }- decls                   :: { [Decl PName] }   : decl ';'               { [$1] }   | decls decl ';'         { $2 : $1 }@@ -568,8 +565,11 @@ -- An expression without an obvious end marker longExpr                       :: { Expr PName }   : 'if' ifBranches 'else' exprNoWhere   { at ($1,$4) $ mkIf (reverse $2) $4 }-  | '\\' apats '->' exprNoWhere          { at ($1,$4) $ EFun emptyFunDesc (reverse $2) $4 }+  | '\\' iapats '->' exprNoWhere         { at ($1,$4) $ EFun emptyFunDesc (reverse $2) $4 }+  | 'case' expr 'of' 'v{' vcaseBranches 'v}' {at ($1,$6) (ECase $2 (reverse $5))}+  | 'case' expr 'of' '{' caseBranches '}' { at ($1,$6) (ECase $2 (reverse $5)) } + ifBranches                     :: { [(Expr PName, Expr PName)] }   : ifBranch                      { [$1] }   | ifBranches '|' ifBranch       { $3 : $1 }@@ -577,6 +577,17 @@ ifBranch                       :: { (Expr PName, Expr PName) }   : expr 'then' expr              { ($1, $3) } +vcaseBranches                  :: { [CaseAlt PName] }+  : caseBranch                    { [$1] }+  | vcaseBranches 'v;' caseBranch { $3 : $1 }++caseBranches                   :: { [CaseAlt PName] }+  : caseBranch                    { [$1] }+  | caseBranches ';' caseBranch   { $3 : $1 }++caseBranch                     :: { CaseAlt PName }+  : cpat '->' expr                { CaseAlt $1 $3 }+ simpleRHS                      :: { Expr PName }   : '-' simpleApp                 { at ($1,$2) (EPrefix PrefixNeg $2) }   | '~' simpleApp                 { at ($1,$2) (EPrefix PrefixComplement $2) }@@ -664,8 +675,8 @@   | field_exprs ',' field_expr    { $3 : $1 }  field_expr                     :: { UpdField PName }-  : field_path opt_apats_indices-                field_how expr    { UpdField $3 $1 (mkIndexedExpr $2 $4) }+  : field_path opt_iapats_indices field_how expr+                                  { UpdField $3 $1 (mkIndexedExpr $2 $4) }  field_path                     :: { [Located Selector] }   : aexpr                         {% exprToFieldPath $1 }@@ -713,20 +724,27 @@   | matches ',' match             { $3 : $1 }  match                          :: { Match PName }-  : pat '<-' expr                 { Match $1 $3 }+  : itpat '<-' expr               { Match $1 $3 }   --------------------------------------------------------------------------------+-- Generic patterns+ pat                            :: { Pattern PName }-  : ipat ':' type                 { at ($1,$3) $ PTyped $1 $3 }-  | ipat                          { $1                        }+  : cpat ':' type                 { at ($1,$3) $ PTyped $1 $3 }+  | cpat                          { $1                        } -ipat                           :: { Pattern PName }-  : ipat '#' ipat                 { at ($1,$3) $ PSplit $1 $3 }+cpat                           :: { Pattern PName }+  : cpat '#' cpat                 { at ($1,$3) $ PSplit $1 $3 }+  | qname apats                   { at ($1,$2) $ PCon $1 (reverse $2)   }   | apat                          { $1                        } +apats                          :: { [Pattern PName] }+  : apat                          { [$1] }+  | apats apat                    { $2 : $1 }+ apat                           :: { Pattern PName }-  : name                          { PVar $1                           }+  : qname                         { at $1 (mkPVar $1) }   | '_'                           { at $1       $ PWild               }   | '(' ')'                       { at ($1,$2) $ PTuple []            }   | '(' pat ')'                   { at ($1,$3)   $2                   }@@ -747,6 +765,41 @@ field_pats                     :: { [Named (Pattern PName)] }   : field_pat                     { [$1]    }   | field_pats ',' field_pat      { $3 : $1 }+++-- Irrefutable patterns+itpat                          :: { Pattern PName }+  : ipat ':' type                 { at ($1,$3) $ PTyped $1 $3 }+  | ipat                          { $1                        }++ipat                           :: { Pattern PName }+  : ipat '#' ipat                 { at ($1,$3) $ PSplit $1 $3 }+  | iapat                         { $1                        }++iapat                          :: { Pattern PName }+  : apat                          {% mkIPat $1 }++iapats                         :: { [Pattern PName] }+  : iapat                         { [$1] }+  | iapats iapat                  { $2 : $1 }++indices                 :: { [Pattern PName] }+  : '@' indices1           { $2 }+  | {- empty -}            { [] }++indices1                :: { [Pattern PName] }+  : iapat                  { [$1] }+  | indices1 '@' apat      { $3 : $1 }++iapats_indices          :: { ([Pattern PName], [Pattern PName]) }+  : iapats indices         { ($1, $2) }+  | '@' indices1           { ([], $2) }++opt_iapats_indices      :: { ([Pattern PName], [Pattern PName]) }+  : {- empty -}            { ([],[]) }+  | iapats_indices         { $1 }++  -------------------------------------------------------------------------------- 

@@ -64,11 +64,13 @@   , PropSyn(..)   , Bind(..)   , BindDef(..), LBindDef+  , BindImpl(..), bindImpl, exprDef   , Pragma(..)   , ExportType(..)   , TopLevel(..)-  , Import, ImportG(..), ImportSpec(..), ImpName(..)+  , Import, ImportG(..), ImportSpec(..), ImpName(..), impNameModPath   , Newtype(..)+  , EnumDecl(..), EnumCon(..)   , PrimType(..)   , ParameterType(..)   , ParameterFun(..)@@ -88,6 +90,7 @@   , Match(..)   , Pattern(..)   , Selector(..)+  , CaseAlt(..)   , TypeInst(..)   , UpdField(..)   , UpdHow(..)@@ -106,6 +109,8 @@   , cppKind, ppSelector   ) where +import Cryptol.ModuleSystem.Name (Name, nameModPath, nameIdent)+import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.Parser.Name import Cryptol.Parser.Position import Cryptol.Parser.Selector@@ -158,6 +163,11 @@ data ModuleG mname name = Module   { mName     :: Located mname              -- ^ Name of the module   , mDef      :: ModuleDefinition name+  , mInScope  :: NamingEnv+    -- ^ Names in scope inside this module, filled in by the renamer.+    --   Also, for the 'FunctorInstance' case this is not the final result of+    --   the names in scope. The typechecker adds in the names in scope in the+    --   functor, so this will just contain the names in the enclosing scope.   } deriving (Show, Generic, NFData)  @@ -243,6 +253,7 @@     Decl (TopLevel (Decl name))   | DPrimType (TopLevel (PrimType name))   | TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t+  | TDEnum (TopLevel (EnumDecl name))   -- ^ @enum T as = cons@   | Include (Located FilePath)          -- ^ @include File@ (until NoInclude)    | DParamDecl Range (Signature name)   -- ^ @parameter ...@ (parser only)@@ -304,6 +315,10 @@   | ImpNested name              -- ^ The module in scope with the given name     deriving (Show, Generic, NFData, Eq, Ord) +impNameModPath :: ImpName Name -> ModPath+impNameModPath (ImpTop mn) = TopModule mn+impNameModPath (ImpNested n) = Nested (nameModPath n) (nameIdent n)+ -- | A simple declaration.  Generally these are things that can appear -- both at the top-level of a module and in `where` clauses. data Decl name = DSignature [Located name] (Schema name)@@ -475,11 +490,26 @@ type LBindDef = Located (BindDef PName)  data BindDef name = DPrim-                  | DForeign-                  | DExpr (Expr name)-                  | DPropGuards [PropGuardCase name]+                  -- | Foreign functions can have an optional cryptol+                  -- implementation+                  | DForeign (Maybe (BindImpl name))+                  | DImpl (BindImpl name)                     deriving (Eq, Show, Generic, NFData, Functor) +bindImpl :: Bind name -> Maybe (BindImpl name)+bindImpl bind =+  case thing (bDef bind) of+    DPrim       -> Nothing+    DForeign mi -> mi+    DImpl i     -> Just i++data BindImpl name = DExpr (Expr name)+                   | DPropGuards [PropGuardCase name]+                     deriving (Eq, Show, Generic, NFData, Functor)++exprDef :: Expr name -> BindDef name+exprDef = DImpl . DExpr+ data PropGuardCase name = PropGuardCase   { pgcProps :: [Located (Prop name)]   , pgcExpr  :: Expr name@@ -497,6 +527,17 @@   , nBody     :: Rec (Type name)     -- ^ Body   } deriving (Eq, Show, Generic, NFData) +data EnumDecl name = EnumDecl+  { eName     :: Located name               -- ^ Type name+  , eParams   :: [TParam name]              -- ^ Type params+  , eCons     :: [TopLevel (EnumCon name)]  -- ^ Value constructors+  } deriving (Show, Generic, NFData)++data EnumCon name = EnumCon+  { ecName    :: Located name+  , ecFields  :: [Type name]+  } deriving (Show, Generic, NFData)+ -- | A declaration for a type with no implementation. data PrimType name = PrimType { primTName :: Located name                               , primTKind :: Located Kind@@ -571,6 +612,7 @@               | EApp (Expr n) (Expr n)          -- ^ @ f x @               | EAppT (Expr n) [(TypeInst n)]   -- ^ @ f `{x = 8}, f`{8} @               | EIf (Expr n) (Expr n) (Expr n)  -- ^ @ if ok then e1 else e2 @+              | ECase (Expr n) [CaseAlt n]      -- ^ @ case e of { P -> e }@               | EWhere (Expr n) [Decl n]        -- ^ @ 1 + x where { x = 2 } @               | ETyped (Expr n) (Type n)        -- ^ @ 1 : [8] @               | ETypeVal (Type n)               -- ^ @ `(x + 1)@, @x@ is a type@@ -629,9 +671,13 @@                | PList [ Pattern n ]           -- ^ @ [ x, y, z ] @                | PTyped (Pattern n) (Type n)   -- ^ @ x : [8] @                | PSplit (Pattern n) (Pattern n)-- ^ @ (x # y) @+               | PCon (Located n) [Pattern n]  -- ^ @ Just x @                | PLocated (Pattern n) Range    -- ^ Location information                  deriving (Eq, Show, Generic, NFData, Functor) +data CaseAlt n = CaseAlt (Pattern n) (Expr n)+  deriving (Eq, Show, Generic, NFData, Functor)+ data Named a = Named { name :: Located Ident, value :: a }   deriving (Eq, Show, Foldable, Traversable, Generic, NFData, Functor) @@ -748,6 +794,7 @@       Decl tld    -> getLoc tld       DPrimType pt -> getLoc pt       TDNewtype n -> getLoc n+      TDEnum n -> getLoc n       Include lfp -> getLoc lfp       DModule d -> getLoc d       DImport d -> getLoc d@@ -801,6 +848,22 @@     where     locs = catMaybes ([ getLoc (nName n)] ++ map (Just . fst . snd) (displayFields (nBody n))) +instance HasLoc (EnumDecl name) where+  getLoc n+    | null locs = Nothing+    | otherwise = Just (rCombs locs)+    where+    locs = catMaybes (getLoc (eName n) : map getLoc (eCons n))++instance HasLoc (EnumCon name) where+  getLoc c+    | null locs = Nothing+    | otherwise = Just (rCombs locs)+    where+    locs = catMaybes (getLoc (ecName c) : map getLoc (ecFields c))+++ instance HasLoc (TySyn name) where   getLoc (TySyn x _ _ _) = getLoc x @@ -839,6 +902,7 @@ ppModule :: (Show name, PPName mname, PPName name) =>   Doc -> ModuleG mname name -> Doc ppModule kw m = kw' <+> ppL (mName m) <+> pp (mDef m)+  $$ indent 2 (vcat ["/* In scope:", indent 2 (pp (mInScope m)), " */"])   where   kw' = case mDef m of           InterfaceModule {} -> "interface" <+> kw@@ -890,6 +954,7 @@       Decl    d   -> pp d       DPrimType p -> pp p       TDNewtype n -> pp n+      TDEnum n -> pp n       Include l   -> text "include" <+> text (show (thing l))       DModule d -> pp d       DImport i -> pp (thing i)@@ -989,6 +1054,16 @@     , ppRecord (map (ppNamed' ":") (displayFields (nBody nt)))     ] +instance (Show name, PPName name) => PP (EnumDecl name) where+  ppPrec _ ed = nest 2 $ sep+    [ fsep $ [text "enum", ppL (eName ed)] ++ map pp (eParams ed) ++ [char '=']+    , vcat [ pre <+> pp con | (pre, con) <- pres `zip` eCons ed ]+    ]+    where pres = " " : repeat "|"++instance (Show name, PPName name) => PP (EnumCon name) where+  ppPrec _ c = pp (ecName c) <+> hsep (map (ppPrec 1) (ecFields c))+ instance (PP mname) => PP (ImportG mname) where   ppPrec _ d = vcat [ text "import" <+> sep ([pp (iModule d)] ++ mbInst ++                                                       mbAs ++ mbSpec)@@ -1051,8 +1126,13 @@   instance (Show name, PPName name) => PP (BindDef name) where-  ppPrec _ DPrim     = text "<primitive>"-  ppPrec _ DForeign  = text "<foreign>"+  ppPrec _ DPrim         = text "<primitive>"+  ppPrec p (DForeign mi) = case mi of+                             Just i  -> "(foreign)" <+> ppPrec p i+                             Nothing -> "<foreign>"+  ppPrec p (DImpl i)     = ppPrec p i++instance (Show name, PPName name) => PP (BindImpl name) where   ppPrec p (DExpr e) = ppPrec p e   ppPrec _p (DPropGuards _guards) = text "propguards" @@ -1195,6 +1275,10 @@                                       , text "then" <+> pp e2                                       , text "else" <+> pp e3 ] +      ECase e as    -> wrap n 0 $ vcat [ "case" <+> pp e <+> "of"+                                       , nest 2 (vcat (map pp as))+                                       ]+       ETyped e t    -> wrap n 0 (ppPrec 2 e <+> text ":" <+> pp t)        EWhere  e ds  -> wrap n 0 $ align $ vsep@@ -1230,6 +1314,9 @@    prefixText PrefixNeg        = "-"    prefixText PrefixComplement = "~" +instance (Show name, PPName name) => PP (CaseAlt name) where+  ppPrec _ (CaseAlt p e) = vcat [ pp p <+> "->", nest 2 (pp e) ]+ instance (Show name, PPName name) => PP (UpdField name) where   ppPrec _ (UpdField h xs e) = ppNestedSels (map thing xs) <+> pp h <+> pp e @@ -1242,6 +1329,10 @@   ppPrec n pat =     case pat of       PVar x        -> pp (thing x)+      PCon c ps ->+        case ps of+          [] -> pp c+          _  -> wrap n 1 (pp c <+> hsep (map (ppPrec 1) ps))       PWild         -> char '_'       PTuple ps     -> ppTuple (map pp ps)       PRecord fs    -> ppRecord (map (ppNamed' "=") (displayFields fs))@@ -1352,6 +1443,7 @@ instance NoPos (ModuleG mname name) where   noPos m = Module { mName      = mName m                    , mDef       = noPos (mDef m)+                   , mInScope   = mInScope m                    }  instance NoPos (ModuleDefinition name) where@@ -1381,6 +1473,7 @@       Decl    x   -> Decl     (noPos x)       DPrimType t -> DPrimType (noPos t)       TDNewtype n -> TDNewtype(noPos n)+      TDEnum n -> TDEnum (noPos n)       Include x   -> Include  (noPos x)       DModule d -> DModule (noPos d)       DImport d -> DImport (noPos d)@@ -1451,6 +1544,15 @@                     , nBody     = fmap noPos (nBody n)                     } +instance NoPos (EnumDecl name) where+  noPos n = EnumDecl { eName    = noPos (eName n)+                     , eParams  = eParams n+                     , eCons    = map noPos (eCons n)+                     }++instance NoPos (EnumCon name) where+  noPos c = EnumCon { ecName = noPos (ecName c), ecFields = noPos (ecFields c) }+ instance NoPos (Bind name) where   noPos x = Bind { bName      = noPos (bName      x)                  , bParams    = noPos (bParams    x)@@ -1508,6 +1610,7 @@       EParens e       -> EParens (noPos e)       EInfix x y f z  -> EInfix (noPos x) y f (noPos z)       EPrefix op x    -> EPrefix op (noPos x)+      ECase x y       -> ECase (noPos x) (noPos y)  instance NoPos (UpdField name) where   noPos (UpdField h xs e) = UpdField h xs (noPos e)@@ -1520,6 +1623,9 @@   noPos (Match x y)  = Match (noPos x) (noPos y)   noPos (MatchLet b) = MatchLet (noPos b) +instance NoPos (CaseAlt name) where+  noPos (CaseAlt p e) = CaseAlt (noPos p) (noPos e)+ instance NoPos (Pattern name) where   noPos pat =     case pat of@@ -1531,6 +1637,7 @@       PTyped x y   -> PTyped  (noPos x) (noPos y)       PSplit x y   -> PSplit  (noPos x) (noPos y)       PLocated x _ -> noPos x+      PCon n ps    -> PCon n (noPos ps)  instance NoPos (Schema name) where   noPos (Forall x y z _) = Forall (noPos x) (noPos y) (noPos z) Nothing

@@ -76,42 +76,46 @@ expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName] expandBind bind =   case thing (bDef bind) of-    DPropGuards guards -> do-      Forall params props t rng <--        case bSignature bind of-          Just schema -> pure schema-          Nothing -> Left . NoSignature $ bName bind-      let goGuard ::-            PropGuardCase PName ->-            ExpandPropGuardsM (PropGuardCase PName, Bind PName)-          goGuard (PropGuardCase props' e) = do-            bName' <- newName (bName bind) (thing <$> props')-            -- call to generated function-            tParams <- case bSignature bind of-              Just (Forall tps _ _ _) -> pure tps-              Nothing -> Left $ NoSignature (bName bind)-            typeInsts <--              (\(TParam n _ _) -> Right . PosInst $ TUser n [])-                `traverse` tParams-            let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bParams bind)-            pure-              ( PropGuardCase props' e',-                bind-                  { bName = bName',-                    -- include guarded props in signature-                    bSignature = Just (Forall params-                                         (props <> map thing props')-                                         t rng),-                    -- keeps same location at original bind-                    -- i.e. "on top of" original bind-                    bDef = (bDef bind) {thing = DExpr e}-                  }-              )-      (guards', binds') <- unzip <$> mapM goGuard guards-      pure $-        bind {bDef = DPropGuards guards' <$ bDef bind} :-        binds'+    DImpl (DPropGuards guards) -> expand (DImpl . DPropGuards) guards+    DForeign (Just (DPropGuards guards)) -> expand (DForeign . Just . DPropGuards) guards     _ -> pure [bind]++  where+  expand def guards = do+    Forall params props t rng <-+      case bSignature bind of+        Just schema -> pure schema+        Nothing -> Left . NoSignature $ bName bind+    let goGuard ::+          PropGuardCase PName ->+          ExpandPropGuardsM (PropGuardCase PName, Bind PName)+        goGuard (PropGuardCase props' e) = do+          bName' <- newName (bName bind) (thing <$> props')+          -- call to generated function+          tParams <- case bSignature bind of+            Just (Forall tps _ _ _) -> pure tps+            Nothing -> Left $ NoSignature (bName bind)+          typeInsts <-+            (\(TParam n _ _) -> Right . PosInst $ TUser n [])+              `traverse` tParams+          let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bParams bind)+          pure+            ( PropGuardCase props' e',+              bind+                { bName = bName',+                  -- include guarded props in signature+                  bSignature = Just (Forall params+                                        (props <> map thing props')+                                        t rng),+                  -- keeps same location at original bind+                  -- i.e. "on top of" original bind+                  bDef = (bDef bind) {thing = exprDef e}+                }+            )+    (guards', binds') <- unzip <$> mapM goGuard guards+    pure $+      bind {bDef = def guards' <$ bDef bind} :+      binds'  patternToExpr :: Pattern PName -> Expr PName patternToExpr (PVar locName) = EVar (thing locName)

@@ -197,6 +197,7 @@ startsLayout ty =   case ty of     KW KW_where       -> True+    KW KW_of          -> True     KW KW_private     -> True     KW KW_parameter   -> True     _                 -> False

@@ -99,12 +99,15 @@ -- Please update the docs, if you add new entries. "else"                    { emit $ KW KW_else } "if"                      { emit $ KW KW_if }+"case"                    { emit $ KW KW_case }+"of"                      { emit $ KW KW_of } "private"                 { emit $ KW KW_private } "include"                 { emit $ KW KW_include } "module"                  { emit $ KW KW_module } "submodule"               { emit $ KW KW_submodule } "interface"               { emit $ KW KW_interface } "newtype"                 { emit $ KW KW_newtype }+"enum"                    { emit $ KW KW_enum } "pragma"                  { emit $ KW KW_pragma } "property"                { emit $ KW KW_property } "then"                    { emit $ KW KW_then }

@@ -46,6 +46,17 @@ mkQual :: ModName -> Ident -> PName mkQual  = Qual +-- | Compute a `PName` for the definition site corresponding to the given+-- `OrigName`.   Usually this is an unqualified name, but names that come+-- from module parameters are qualified with the corresponding parameter name.+origNameToDefPName :: OrigName -> PName+origNameToDefPName og = toPName (ogName og)+  where+  toPName =+    case ogFromParam og of+      Nothing -> UnQual+      Just sig -> Qual (identToModName sig)+ getModName :: PName -> Maybe ModName getModName (Qual ns _) = Just ns getModName _           = Nothing

@@ -13,6 +13,7 @@  module Cryptol.Parser.Names   ( tnamesNT+  , tnamesEnum   , tnamesT   , tnamesC @@ -20,7 +21,9 @@   , tnamesD   , namesB   , namesP+  , namesP'   , namesNT+  , namesEnum    , boundNames   , boundNamesSet@@ -39,6 +42,12 @@ namesNT :: Newtype name -> ([Located name], ()) namesNT x = ([ (nName x) { thing = nConName x } ], ()) +tnamesEnum :: EnumDecl name -> ([Located name],())+tnamesEnum n = ([ eName n], ())++namesEnum :: EnumDecl name -> ([Located name], ())+namesEnum n = (map (ecName . tlValue) (eCons n), ())+ -- | The names defined and used by a group of mutually recursive declarations. namesDs :: Ord name => [Decl name] -> ([Located name], Set name) namesDs ds = (defs, boundLNames defs (Set.unions frees))@@ -53,7 +62,7 @@     DBind b       -> namesB b     DRec bs       -> let (xs,ys) = unzip (map namesB bs)                      in (concat xs, Set.unions ys)  -- remove binders?-    DPatBind p e  -> (namesP p, namesE e)+    DPatBind p e  -> (namesP' p, namesE e)     DSignature {} -> ([],Set.empty)     DFixity{}     -> ([],Set.empty)     DPragma {}    -> ([],Set.empty)@@ -64,16 +73,19 @@ -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name) namesB b =-  ([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b))))+  ([bName b], boundLNames (namesPs' (bParams b)) (namesDef (thing (bDef b))))   namesDef :: Ord name => BindDef name -> Set name-namesDef DPrim     = Set.empty-namesDef DForeign  = Set.empty-namesDef (DExpr e) = namesE e-namesDef (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards)+namesDef DPrim         = Set.empty+namesDef (DForeign mi) = foldMap namesImpl mi+namesDef (DImpl i)     = namesImpl i +namesImpl :: Ord name => BindImpl name -> Set name+namesImpl (DExpr e)            = namesE e+namesImpl (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards) + -- | The names used by an expression. namesE :: Ord name => Expr name -> Set name namesE expr =@@ -98,11 +110,12 @@     EApp e1 e2    -> Set.union (namesE e1) (namesE e2)     EAppT e _     -> namesE e     EIf e1 e2 e3  -> Set.union (namesE e1) (Set.union (namesE e2) (namesE e3))+    ECase e as    -> Set.union (namesE e) (Set.unions (map namesCA as))     EWhere  e ds  -> let (bs,xs) = namesDs ds                      in Set.union (boundLNames bs (namesE e)) xs     ETyped e _    -> namesE e     ETypeVal _    -> Set.empty-    EFun _ ps e   -> boundLNames (namesPs ps) (namesE e)+    EFun _ ps e   -> boundLNames (fst (namesPs ps)) (namesE e) -- no free     ELocated e _  -> namesE e      ESplit e      -> namesE e@@ -113,16 +126,31 @@ namesUF :: Ord name => UpdField name -> Set name namesUF (UpdField _ _ e) = namesE e +namesCA :: Ord name => CaseAlt name -> Set name+namesCA (CaseAlt p e) = Set.union free (boundLNames defs (namesE e))+  where+  (defs,free) = namesP p++namesP' :: Ord name => Pattern name -> [Located name]+namesP' = fst . namesP++namesPs' :: Ord name => [Pattern name] -> [Located name]+namesPs' = fst . namesPs+ -- | The names defined by a group of patterns.-namesPs :: [Pattern name] -> [Located name]-namesPs = concatMap namesP+namesPs :: Ord name => [Pattern name] -> ([Located name], Set name)+namesPs ps = (concat defs, Set.unions uses)+  where+  (defs, uses) = unzip (map namesP ps)  -- | The names defined by a pattern.  These will always be unqualified names.-namesP :: Pattern name -> [Located name]+namesP :: Ord name => Pattern name -> ([Located name], Set name) namesP pat =   case pat of-    PVar x        -> [x]-    PWild         -> []+    PVar x        -> ([x], Set.empty)+    PCon c ps     -> (def, Set.insert (thing c) free)+      where (def,free) = namesPs ps+    PWild         -> ([],Set.empty)     PTuple ps     -> namesPs ps     PRecord fs    -> namesPs (map snd (recordElements fs))     PList ps      -> namesPs ps@@ -130,9 +158,11 @@     PSplit p1 p2  -> namesPs [p1,p2]     PLocated p _  -> namesP p ++ -- | The names defined and used by a match. namesM :: Ord name => Match name -> ([Located name], Set name)-namesM (Match p e)  = (namesP p, namesE e)+namesM (Match p e)  = (namesP' p, namesE e) namesM (MatchLet b) = namesB b  -- | The names defined and used by an arm of alist comprehension.@@ -190,11 +220,14 @@     setE = tnamesDef (thing (bDef b))  tnamesDef :: Ord name => BindDef name -> Set name-tnamesDef DPrim     = Set.empty-tnamesDef DForeign  = Set.empty-tnamesDef (DExpr e) = tnamesE e-tnamesDef (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)+tnamesDef DPrim         = Set.empty+tnamesDef (DForeign mi) = foldMap tnamesImpl mi+tnamesDef (DImpl i)     = tnamesImpl i +tnamesImpl :: Ord name => BindImpl name -> Set name+tnamesImpl (DExpr e)            = tnamesE e+tnamesImpl (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)+ tnamesPropGuardCase :: Ord name => PropGuardCase name -> Set name tnamesPropGuardCase c =   Set.unions (tnamesE (pgcExpr c) : map (tnamesC . thing) (pgcProps c))@@ -225,6 +258,7 @@     EApp e1 e2      -> Set.union (tnamesE e1) (tnamesE e2)     EAppT e fs      -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs))     EIf e1 e2 e3    -> Set.union (tnamesE e1) (Set.union (tnamesE e2) (tnamesE e3))+    ECase e as      -> Set.union (tnamesE e) (Set.unions (map tnamesCA as))     EWhere  e ds    -> let (bs,xs) = tnamesDs ds                        in Set.union (boundLNames bs (tnamesE e)) xs     ETyped e t      -> Set.union (tnamesE e) (tnamesT t)@@ -237,6 +271,9 @@     EInfix a _ _ b  -> Set.union (tnamesE a) (tnamesE b)     EPrefix _ e     -> tnamesE e +tnamesCA :: Ord name => CaseAlt name -> Set name+tnamesCA (CaseAlt p e) = Set.union (tnamesP p) (tnamesE e)+ tnamesUF :: Ord name => UpdField name -> Set name tnamesUF (UpdField _ _ e) = tnamesE e @@ -249,6 +286,7 @@ tnamesP pat =   case pat of     PVar _        -> Set.empty+    PCon _ ps     -> Set.unions (map tnamesP ps)     PWild         -> Set.empty     PTuple ps     -> Set.unions (map tnamesP ps)     PRecord fs    -> Set.unions (map (tnamesP . snd) (recordElements fs))

@@ -212,6 +212,7 @@   Decl _     -> pure [td]   DPrimType {} -> pure [td]   TDNewtype _-> pure [td]+  TDEnum _-> pure [td]   DParamDecl {} -> pure [td]   DInterfaceConstraint {} -> pure [td]   Include lf -> resolveInclude lf

@@ -6,10 +6,12 @@ -- Stability   :  provisional -- Portability :  portable ----- The purpose of this module is to convert all patterns to variable+-- The purpose of this module is to convert all irrefutable patterns to variable -- patterns.  It also eliminates pattern bindings by de-sugaring them -- into `Bind`.  Furthermore, here we associate signatures, fixities,--- and pragmas with the names to which they belong.+-- and pragmas with the names to which they belong.  We also merge+-- empty 'DForeign' binds with their cryptol implementations, if they+-- exist.  {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}@@ -22,7 +24,7 @@  import Cryptol.Parser.AST import Cryptol.Parser.Position(Range(..),emptyRange,start,at)-import Cryptol.Parser.Names (namesP)+import Cryptol.Parser.Names (namesP') import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap@@ -57,7 +59,7 @@  simpleBind :: Located PName -> Expr PName -> Bind PName simpleBind x e = Bind { bName = x, bParams = []-                      , bDef = at e (Located emptyRange (DExpr e))+                      , bDef = at e (Located emptyRange (exprDef e))                       , bSignature = Nothing, bPragmas = []                       , bMono = True, bInfix = False, bFixity = Nothing                       , bDoc = Nothing@@ -72,18 +74,29 @@ -- Simple patterns may only contain variables and type annotations.  -- XXX: We can replace the types in the selectors with annotations on the bindings.-noPat :: Pattern PName -> NoPatM (Pattern PName, [Bind PName])-noPat pat =+noPat :: Bool -> Pattern PName -> NoPatM (Pattern PName, [Bind PName])+noPat conOk pat =   case pat of     PVar x -> return (PVar x, []) +    PCon c ps+      | conOk ->+        do (as,dss) <- mapAndUnzipM (noPat False) ps+           pure (PCon c as, concat dss)++      | otherwise ->+        do let r = srcRange c+           recordError (InvalidConstructorPattern r)+           x <- newName+           pure (pVar r x, [])+     PWild ->       do x <- newName          r <- getRange          return (pVar r x, [])      PTuple ps ->-      do (as,dss) <- unzip `fmap` mapM noPat ps+      do (as,dss) <- unzip `fmap` mapM (noPat False) ps          x <- newName          r <- getRange          let len      = length ps@@ -97,7 +110,7 @@          return (pTy r x (TSeq (TNum 0) TWild), [])      PList ps ->-      do (as,dss) <- unzip `fmap` mapM noPat ps+      do (as,dss) <- unzip `fmap` mapM (noPat False) ps          x <- newName          r <- getRange          let len      = length ps@@ -107,7 +120,7 @@      PRecord fs ->       do let (shape, els) = unzip (canonicalFields fs)-         (as,dss) <- unzip `fmap` mapM (noPat . snd) els+         (as,dss) <- unzip `fmap` mapM (noPat False . snd) els          x <- newName          r <- getRange          let ty           = TRecord (fmap (\(rng,_) -> (rng,TWild)) fs)@@ -115,13 +128,13 @@          return (pTy r x ty, zipWith getN as shape ++ concat dss)      PTyped p t ->-      do (a,ds) <- noPat p+      do (a,ds) <- noPat conOk p          return (PTyped a t, ds)      -- XXX: We can do more with type annotations here     PSplit p1 p2 ->-      do (a1,ds1) <- noPat p1-         (a2,ds2) <- noPat p2+      do (a1,ds1) <- noPat False p1+         (a2,ds2) <- noPat False p2          x <- newName          tmp <- newName          r <- getRange@@ -130,11 +143,11 @@              b2   = sel a2 tmp (TupleSel 1 (Just 2))          return (pVar r x, bTmp : b1 : b2 : ds1 ++ ds2) -    PLocated p r1 -> inRange r1 (noPat p)+    PLocated p r1 -> inRange r1 (noPat conOk p)    where   pVar r x   = PVar (Located r x)-  pTy  r x t = PTyped (PVar (Located r x)) t+  pTy  r x   = PTyped (PVar (Located r x))   splitSimpleP :: Pattern PName -> (Located PName, [Type PName])@@ -166,6 +179,7 @@     EApp e1 e2    -> EApp   <$> noPatE e1 <*> noPatE e2     EAppT e ts    -> EAppT  <$> noPatE e <*> return ts     EIf e1 e2 e3  -> EIf    <$> noPatE e1 <*> noPatE e2 <*> noPatE e3+    ECase e as    -> ECase  <$> noPatE e  <*> traverse noPatAlt as     EWhere e ds   -> EWhere <$> noPatE e <*> noPatDs ds     ETyped e t    -> ETyped <$> noPatE e <*> return t     ETypeVal {}   -> return expr@@ -177,6 +191,14 @@     EInfix x y f z-> EInfix  <$> noPatE x <*> pure y <*> pure f <*> noPatE z     EPrefix op e  -> EPrefix op <$> noPatE e +noPatAlt :: CaseAlt PName -> NoPatM (CaseAlt PName)+noPatAlt (CaseAlt p e) =+  do (p1,ds) <- noPat True p+     e1 <- noPatE e+     let e2 = case ds of+                [] -> e1+                _  -> EWhere e1 (map DBind ds)+     pure (CaseAlt p1 e2)  noPatUF :: UpdField PName -> NoPatM (UpdField PName) noPatUF (UpdField h ls e) = UpdField h ls <$> noPatE e@@ -190,7 +212,7 @@ noPatFun :: Maybe PName -> Int -> [Pattern PName] -> Expr PName -> NoPatM (Expr PName) noPatFun _   _      []     e = noPatE e noPatFun mnm offset (p:ps) e =-  do (p',ds) <- noPat p+  do (p',ds) <- noPat False p      e' <- noPatFun mnm (offset+1) ps e      let body = case ds of                   [] -> e'@@ -207,7 +229,7 @@  noPatM :: Match PName -> NoPatM [Match PName] noPatM (Match p e) =-  do (x,bs) <- noPat p+  do (x,bs) <- noPat False p      e1     <- noPatE e      return (Match x e1 : map MatchLet bs) noPatM (MatchLet b) = (return . MatchLet) <$> noMatchB b@@ -220,21 +242,26 @@           | otherwise        -> panic "NoPat" [ "noMatchB: primitive with params"                                               , show b ] -    DForeign+    DForeign Nothing       | null (bParams b) -> return b       | otherwise        -> panic "NoPat" [ "noMatchB: foreign with params"                                           , show b ] -    DExpr e ->-      do e' <- noPatFun (Just (thing (bName b))) 0 (bParams b) e-         return b { bParams = [], bDef = DExpr e' <$ bDef b }+    DForeign (Just i) -> noMatchI (DForeign . Just) i -    DPropGuards guards ->-      do let nm = thing (bName b)-             ps = bParams b-         gs <- mapM (noPatPropGuardCase nm ps) guards-         pure b { bParams = [], bDef = DPropGuards gs <$ bDef b }+    DImpl i -> noMatchI DImpl i +  where+  noMatchI def i =+    do i' <- case i of+               DExpr e ->+                 DExpr <$> noPatFun (Just (thing (bName b))) 0 (bParams b) e+               DPropGuards guards ->+                 let nm = thing (bName b)+                     ps = bParams b+                 in  DPropGuards <$> mapM (noPatPropGuardCase nm ps) guards+       pure b { bParams = [], bDef = def i' <$ bDef b }+ noPatPropGuardCase ::   PName ->   [Pattern PName] ->@@ -254,13 +281,13 @@                           return [DBind b1]     DRec {}         -> panic "noMatchD" [ "DRec" ] -    DPatBind p e    -> do (p',bs) <- noPat p+    DPatBind p e    -> do (p',bs) <- noPat False p                           let (x,ts) = splitSimpleP p'                           e1 <- noPatE e                           let e2 = foldl ETyped e1 ts                           return $ DBind Bind { bName = x                                               , bParams = []-                                              , bDef = at e (Located emptyRange (DExpr e2))+                                              , bDef = at e (Located emptyRange (exprDef e2))                                               , bSignature = Nothing                                               , bPragmas = []                                               , bMono = False@@ -280,11 +307,13 @@   do ds1 <- concat <$> mapM noMatchD ds      let fixes = Map.fromListWith (++) $ concatMap toFixity ds1          amap = AnnotMap-           { annPragmas = Map.fromListWith (++) $ concatMap toPragma ds1-           , annSigs    = Map.fromListWith (++) $ concatMap toSig ds1-           , annValueFs = fixes-           , annTypeFs  = fixes-           , annDocs    = Map.empty+           { annPragmas  = Map.fromListWith (++) $ concatMap toPragma ds1+           , annSigs     = Map.fromListWith (++) $ concatMap toSig ds1+           , annValueFs  = fixes+           , annTypeFs   = fixes+           , annDocs     = Map.empty+             -- There shouldn't be any foreigns at non-top-level+           , annForeigns = Map.empty            }       (ds2, AnnotMap { .. }) <- runStateT amap (annotDs ds1)@@ -314,11 +343,12 @@          fixes     = Map.fromListWith (++) $ concatMap toFixity allDecls       let ann = AnnotMap-           { annPragmas = Map.fromListWith (++) $ concatMap toPragma allDecls-           , annSigs    = Map.fromListWith (++) $ concatMap toSig    allDecls-           , annValueFs = fixes-           , annTypeFs  = fixes-           , annDocs    = Map.fromListWith (++) $ concatMap toDocs $ decls tds+           { annPragmas  = Map.fromListWith (++) $ concatMap toPragma allDecls+           , annSigs     = Map.fromListWith (++) $ concatMap toSig    allDecls+           , annValueFs  = fixes+           , annTypeFs   = fixes+           , annDocs     = Map.fromListWith (++) $ concatMap toDocs $ decls tds+           , annForeigns = Map.fromListWith (<>) $ concatMap toForeigns allDecls           }       (tds', AnnotMap { .. }) <- runStateT ann (annotTopDs desugared)@@ -362,12 +392,25 @@  -------------------------------------------------------------------------------- +-- | For each binding name, does there exist an empty foreign bind, a normal+-- cryptol bind, or both.+data AnnForeign = OnlyForeign | OnlyImpl | BothForeignImpl++instance Semigroup AnnForeign where+  OnlyForeign     <> OnlyImpl        = BothForeignImpl+  OnlyImpl        <> OnlyForeign     = BothForeignImpl+  _               <> BothForeignImpl = BothForeignImpl+  BothForeignImpl <> _               = BothForeignImpl+  OnlyForeign     <> OnlyForeign     = OnlyForeign+  OnlyImpl        <> OnlyImpl        = OnlyImpl+ data AnnotMap = AnnotMap   { annPragmas  :: Map.Map PName [Located  Pragma       ]   , annSigs     :: Map.Map PName [Located (Schema PName)]   , annValueFs  :: Map.Map PName [Located  Fixity       ]   , annTypeFs   :: Map.Map PName [Located  Fixity       ]   , annDocs     :: Map.Map PName [Located  Text         ]+  , annForeigns :: Map.Map PName AnnForeign   }  type Annotates a = a -> StateT AnnotMap NoPatM a@@ -398,8 +441,9 @@         DParamDecl {} -> (d :) <$> annotTopDs ds         DInterfaceConstraint {} -> (d :) <$> annotTopDs ds -        -- XXX: we may want to add pragmas to newtypes?+        -- XXX: we may want to add pragmas to newtypes and enums?         TDNewtype {} -> (d :) <$> annotTopDs ds+        TDEnum {}    -> (d :) <$> annotTopDs ds         Include {}   -> (d :) <$> annotTopDs ds          DModule m ->@@ -428,7 +472,7 @@ annotD :: Decl PName -> ExceptionT () (StateT AnnotMap NoPatM) (Decl PName) annotD decl =   case decl of-    DBind b       -> DBind <$> lift (annotB b)+    DBind b       -> DBind <$> annotB b     DRec {}       -> panic "annotD" [ "DRec" ]     DSignature {} -> raise ()     DFixity{}     -> raise ()@@ -439,7 +483,10 @@     DLocated d r  -> (`DLocated` r) <$> annotD d  -- | Add pragma/signature annotations to a binding.-annotB :: Annotates (Bind PName)+-- Also perform de-duplication of empty 'DForeign' binds generated by the parser+-- if there exists a cryptol implementation.+-- The exception indicates which declarations are no longer needed.+annotB :: Bind PName -> ExceptionT () (StateT AnnotMap NoPatM) (Bind PName) annotB Bind { .. } =   do AnnotMap { .. } <- get      let name       = thing bName@@ -448,9 +495,17 @@          (thisSigs  , ss') = Map.updateLookupWithKey remove name annSigs          (thisFixes , fs') = Map.updateLookupWithKey remove name annValueFs          (thisDocs  , ds') = Map.updateLookupWithKey remove name annDocs-     s <- lift $ checkSigs name $ jn thisSigs-     f <- lift $ checkFixs name $ jn thisFixes-     d <- lift $ checkDocs name $ jn thisDocs+         thisForeign       = Map.lookup name annForeigns+     -- Compute the new def before updating the state, since we don't want to+     -- consume the annotations if we are throwing away an empty foreign def.+     def' <- case thisForeign of+               Just BothForeignImpl+                 | DForeign _ <- thing bDef -> raise ()+                 | DImpl i    <- thing bDef -> pure (DForeign (Just i) <$ bDef)+               _ -> pure bDef+     s <- lift $ lift $ checkSigs name $ jn thisSigs+     f <- lift $ lift $ checkFixs name $ jn thisFixes+     d <- lift $ lift $ checkDocs name $ jn thisDocs      set AnnotMap { annPragmas = ps'                   , annSigs    = ss'                   , annValueFs = fs'@@ -458,6 +513,7 @@                   , ..                   }      return Bind { bSignature = s+                 , bDef = def'                  , bPragmas = map thing (jn thisPs) ++ bPragmas                  , bFixity = f                  , bDoc = d@@ -544,13 +600,20 @@       DBind b         -> [ (thing (bName b), [txt]) ]       DRec {}         -> panic "toDocs" [ "DRec" ]       DLocated d _    -> go txt d-      DPatBind p _    -> [ (thing n, [txt]) | n <- namesP p ]+      DPatBind p _    -> [ (thing n, [txt]) | n <- namesP' p ]        -- XXX revisit these       DPragma _ _     -> []       DType _         -> []       DProp _         -> [] +-- | Is this declaration a foreign or regular bind?+toForeigns :: Decl PName -> [(PName, AnnForeign)]+toForeigns (DLocated d _) = toForeigns d+toForeigns (DBind Bind {..})+  | DForeign Nothing <- thing bDef = [ (thing bName, OnlyForeign) ]+  | DImpl _          <- thing bDef = [ (thing bName, OnlyImpl) ]+toForeigns _ = []  -------------------------------------------------------------------------------- newtype NoPatM a = M { unM :: ReaderT Range (StateT RW Id) a }@@ -563,6 +626,7 @@             | MultipleFixities PName [Range]             | FixityNoBind (Located PName)             | MultipleDocs PName [Range]+            | InvalidConstructorPattern Range               deriving (Show,Generic, NFData)  instance Functor NoPatM where fmap = liftM@@ -605,21 +669,21 @@     case err of       MultipleSignatures x ss ->         text "Multiple type signatures for" <+> quotes (pp x)-        $$ nest 2 (vcat (map pp ss))+        $$ indent 2 (vcat (map pp ss))        SignatureNoBind x s ->         text "At" <+> pp (srcRange x) <.> colon <+>         text "Type signature without a matching binding:"-         $$ nest 2 (pp (thing x) <+> colon <+> pp s)+         $$ indent 2 (pp (thing x) <+> colon <+> pp s)        PragmaNoBind x s ->         text "At" <+> pp (srcRange x) <.> colon <+>         text "Pragma without a matching binding:"-         $$ nest 2 (pp s)+         $$ indent 2 (pp s)        MultipleFixities n locs ->         text "Multiple fixity declarations for" <+> quotes (pp n)-        $$ nest 2 (vcat (map pp locs))+        $$ indent 2 (vcat (map pp locs))        FixityNoBind n ->         text "At" <+> pp (srcRange n) <.> colon <+>@@ -628,4 +692,10 @@        MultipleDocs n locs ->         text "Multiple documentation blocks given for:" <+> pp n-        $$ nest 2 (vcat (map pp locs))+        $$ indent 2 (vcat (map pp locs))++      InvalidConstructorPattern r ->+        "At" <+> pp r <.> colon <+> "Invalid constructor pattern"+         $$ indent 2 "Constructors may appear only at the top level of a case."++

@@ -50,7 +50,7 @@                           , modNameArg, modNameIfaceMod                           , modNameToText, modNameIsNormal                           , modNameToNormalModName-                          , unpackIdent+                          , unpackIdent, isUpperIdent                           ) import Cryptol.Utils.PP import Cryptol.Utils.Panic@@ -512,6 +512,12 @@                                          , tlDoc    = d                                          , tlValue  = n } +exportEnum ::+  ExportType -> Maybe (Located Text) -> EnumDecl PName -> TopDecl PName+exportEnum e d n = TDEnum TopLevel { tlExport = e+                                   , tlDoc = d+                                   , tlValue = n }+ exportModule :: Maybe (Located Text) -> NestedModule PName -> TopDecl PName exportModule mbDoc m = DModule TopLevel { tlExport = Public                                         , tlDoc    = mbDoc@@ -550,6 +556,7 @@       Decl d                  -> Decl      d { tlExport = e }       DPrimType t             -> DPrimType t { tlExport = e }       TDNewtype n             -> TDNewtype n { tlExport = e }+      TDEnum n                -> TDEnum    n { tlExport = e }       DModule m               -> DModule   m { tlExport = e }       DModParam {}            -> decl       Include{}               -> decl@@ -587,6 +594,66 @@   do (nm,params) <- typeToDecl thead      pure (Newtype nm params (thing nm) (thing def)) +mkEnumDecl ::+  Type PName ->+  [ TopLevel (EnumCon PName) ] {- ^ Reversed -} ->+  ParseM (EnumDecl PName)+mkEnumDecl thead def =+  do (nm,params) <- typeToDecl thead+     mapM_ reportRepeated+        (Map.toList (Map.fromListWith (++) [ (thing k,[srcRange k])+                                           | k <- map (ecName . tlValue) def ]))+     pure EnumDecl+            { eName   = nm+            , eParams = params+            , eCons   = reverse def+            }+  where+  reportRepeated (i,xs) =+    case xs of+      l : ls@(_ : _) ->+        errorMessage l+          ( ("Multiple declarations for " ++ show (backticks (pp i)))+          : [ "Other declaration: " ++ show (pp x) | x <- ls ]+          )++      _ -> pure ()++mkConDecl ::+  Maybe (Located Text) -> ExportType ->+  Type PName -> ParseM (TopLevel (EnumCon PName))+mkConDecl mbDoc expT ty =+  do con <- go Nothing ty+     pure TopLevel { tlExport = expT, tlDoc = mbDoc, tlValue = con }+  where+  go mbLoc t =+    case t of+      TLocated t1 r -> go (Just r) t1+      TUser n ts ->+        case n of+          UnQual i+            | isUpperIdent i ->+              pure EnumCon { ecName = Located (getL mbLoc) (UnQual i)+                           , ecFields = ts+                           }+            | otherwise ->+              errorMessage (getL mbLoc)+                 [ "Malformed constructor declaration."+                 , "The constructor name should start with a capital letter."+                 ]++          _ -> errorMessage (getL mbLoc)+                 [ "Malformed constructor declaration."+                 , "The constructor name may not be qualified."+                 ]+      _ -> errorMessage (getL mbLoc) [ "Malformed constructor declaration." ]++  getL mb =+    case mb of+      Just r  -> r+      Nothing -> panic "mkConDecl" ["Missing type location"]++ typeToDecl :: Type PName -> ParseM (Located PName, [TParam PName]) typeToDecl ty0 =   case ty0 of@@ -692,7 +759,7 @@ mkProperty f ps e = at (f,e) $                     DBind Bind { bName       = f                                , bParams     = reverse ps-                               , bDef        = at e (Located emptyRange (DExpr e))+                               , bDef        = at e (Located emptyRange (exprDef e))                                , bSignature  = Nothing                                , bPragmas    = [PragmaProperty]                                , bMono       = False@@ -708,7 +775,7 @@ mkIndexedDecl f (ps, ixs) e =   DBind Bind { bName       = f              , bParams     = reverse ps-             , bDef        = at e (Located emptyRange (DExpr rhs))+             , bDef        = at e (Located emptyRange (exprDef rhs))              , bSignature  = Nothing              , bPragmas    = []              , bMono       = False@@ -735,7 +802,7 @@      pure $        DBind Bind { bName       = f                   , bParams     = reverse ps-                  , bDef        = Located (srcRange f) (DPropGuards gs)+                  , bDef        = Located (srcRange f) (DImpl (DPropGuards gs))                   , bSignature  = Nothing                   , bPragmas    = []                   , bMono       = False@@ -765,6 +832,34 @@     where     addIfThen (cond, doexpr) elseExpr = EIf cond doexpr elseExpr +mkPVar :: Located PName -> Pattern PName+mkPVar p =+  case thing p of+    UnQual i | isInfixIdent i || not (isUpperIdent i) -> PVar p+    _ -> PCon p []++mkIPat :: Pattern PName -> ParseM (Pattern PName)+mkIPat pat =+  case pat of+    PVar {}      -> pure pat+    PWild        -> pure pat+    PTuple ps    -> PTuple <$> traverse mkIPat ps+    PRecord rp   -> PRecord <$> traverseRecordMap upd rp+      where upd _ (x,y) = (,) x <$> mkIPat y+    PList ps     -> PList <$> traverse mkIPat ps+    PTyped p t   -> (`PTyped` t) <$> mkIPat p+    PSplit p1 p2 -> PSplit <$> mkIPat p1 <*> mkIPat p2+    PLocated p r -> (`PLocated` r) <$> mkIPat p+    PCon n ps    ->+      case ps of+        [] | UnQual {} <- thing n -> pure (PVar n)+        _ -> errorMessage (srcRange n)+               [ "Unexpected constructor pattern."+               , "Constructors patterns may be used only in `case` expressions."+               ]+++ mkPrimDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] mkPrimDecl = mkNoImplDecl DPrim @@ -777,7 +872,11 @@             [ "`" ++ txt ++ "` is not a valid foreign name."             , "The name should contain only alpha-numeric characters or '_'."             ])-     pure (mkNoImplDecl DForeign mbDoc nm ty)+     -- We do allow optional cryptol implementations of foreign functions, these+     -- will be merged with this binding in the NoPat pass. In the parser they+     -- are just treated as a completely separate (non-foreign) binding with the+     -- same name.+     pure (mkNoImplDecl (DForeign Nothing) mbDoc nm ty)   where   isOk c = c == '_' || isAlphaNum c @@ -791,7 +890,7 @@ mkNoImplDecl :: BindDef PName   -> Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] mkNoImplDecl def mbDoc ln sig =-  [ exportDecl mbDoc Public+  [ exportDecl Nothing Public     $ DBind Bind { bName      = ln                  , bParams    = []                  , bDef       = at sig (Located emptyRange def)@@ -803,7 +902,7 @@                  , bDoc       = Nothing                  , bExport    = Public                  }-  , exportDecl Nothing Public+  , exportDecl mbDoc Public     $ DSignature [ln] sig   ] @@ -961,6 +1060,7 @@ mkModule :: Located ModName -> [TopDecl PName] -> Module PName mkModule nm ds = Module { mName = nm                         , mDef = NormalModule ds+                        , mInScope = mempty                         }  mkNested :: Module PName -> ParseM (NestedModule PName)@@ -979,8 +1079,9 @@   TopLevel { tlExport = Public            , tlDoc    = doc            , tlValue  = NestedModule-                        Module { mName = nm-                               , mDef  = InterfaceModule sig+                        Module { mName    = nm+                               , mDef     = InterfaceModule sig+                               , mInScope = mempty                                }            } @@ -1055,8 +1156,9 @@                       [TopDecl PName] ->                       Module PName mkModuleInstanceAnon nm fun ds =-  Module { mName  = nm-         , mDef   = FunctorInstance fun (DefaultInstAnonArg ds) mempty+  Module { mName    = nm+         , mDef     = FunctorInstance fun (DefaultInstAnonArg ds) mempty+         , mInScope = mempty          }  mkModuleInstance ::@@ -1065,8 +1167,9 @@   ModuleInstanceArgs PName ->   Module PName mkModuleInstance m f as =-  Module { mName = m-         , mDef  = FunctorInstance f as emptyModuleInstance+  Module { mName    = m+         , mDef     = FunctorInstance f as emptyModuleInstance+         , mInScope = mempty          }  @@ -1188,8 +1291,9 @@  mkTopSig :: Located ModName -> Signature PName -> [Module PName] mkTopSig nm sig =-  [ Module { mName = nm-           , mDef  = InterfaceModule sig+  [ Module { mName    = nm+           , mDef     = InterfaceModule sig+           , mInScope = mempty            }   ] @@ -1233,7 +1337,8 @@          let i      = mkAnon AnonArg (thing (mName mo))              nm     = Located { srcRange = srcRange (mName mo), thing = i }              as'    = DefaultInstArg (ModuleArg . toImpName <$> nm)-         pure [ Module { mName = nm, mDef  = NormalModule lds' }+         pure [ Module+                  { mName = nm, mDef  = NormalModule lds', mInScope = mempty }               , mo { mDef = FunctorInstance f as' mempty }               ] @@ -1283,6 +1388,7 @@           do let nm = mkAnon AnonIfaceMod <$> ownerName              pure ( [ Module { mName = nm                              , mDef = InterfaceModule sig+                             , mInScope = mempty                              }                      ]                   , [ DModParam@@ -1326,9 +1432,10 @@   ParseM [TopDecl PName] desugarInstImport i inst =   do ms <- desugarMod-           Module { mName = i { thing = iname }-                  , mDef  = FunctorInstance-                              (iModule <$> i) inst emptyModuleInstance+           Module { mName    = i { thing = iname }+                  , mDef     = FunctorInstance+                                 (iModule <$> i) inst emptyModuleInstance+                  , mInScope = mempty                   }      pure (DImport (newImp <$> i) : map modTop ms) 

@@ -23,6 +23,8 @@ data TokenKW  = KW_else               | KW_fin               | KW_if+              | KW_case+              | KW_of               | KW_private               | KW_include               | KW_inf@@ -34,6 +36,7 @@               | KW_module               | KW_submodule               | KW_newtype+              | KW_enum               | KW_pragma               | KW_property               | KW_then

@@ -33,7 +33,7 @@     , browseFunctors disp decls     , browseTSyns disp decls     , browsePrimTys disp decls-    , browseNewtypes disp decls+    , browseNominalTypes disp decls     , browseVars disp decls     ] @@ -97,7 +97,7 @@   ppSection disp "Interface Submodules"     ppS (Map.mapWithKey (,) (ifSignatures decls))   where-  ppS (x,s) = pp x+  ppS (x,_s) = pp x   browseTSyns :: DispInfo -> IfaceDecls -> [Doc]@@ -110,13 +110,15 @@  browsePrimTys :: DispInfo -> IfaceDecls -> [Doc] browsePrimTys disp decls =-  ppSection disp "Primitive Types" ppA (ifAbstractTypes decls)+  ppSection disp "Primitive Types" ppA ats   where-  ppA a = nest 2 (sep [pp (T.atName a) <+> ":", pp (T.atKind a)])+  ats = Map.filter T.nominalTypeIsAbstract (ifNominalTypes decls)+  ppA a = nest 2 (sep [pp (T.ntName a) <+> ":", pp (T.kindOf a)]) -browseNewtypes :: DispInfo -> IfaceDecls -> [Doc]-browseNewtypes disp decls =-  ppSection disp "Newtypes" T.ppNewtypeShort (ifNewtypes decls)+browseNominalTypes :: DispInfo -> IfaceDecls -> [Doc]+browseNominalTypes disp decls =+  ppSection disp "Nominal Types" T.ppNominalShort+    (Map.filter (not . T.nominalTypeIsAbstract) (ifNominalTypes decls))  browseVars :: DispInfo -> IfaceDecls -> [Doc] browseVars disp decls =@@ -132,7 +134,7 @@  ppSection :: DispInfo -> String -> (a -> Doc) -> Map Name a -> [Doc] ppSection disp heading ppThing mp =-  ppSectionHeading heading +  ppSectionHeading heading   case dispHow disp of     BrowseExported | [(_,xs)] <- grouped -> ppThings xs     _ -> concatMap ppMod grouped@@ -151,7 +153,7 @@ ppSectionHeading :: String -> [Doc] -> [Doc] ppSectionHeading heading body   | null body = []-  | otherwise = +  | otherwise =      [ text heading      , text (map (const '=') heading)      , "    "

@@ -121,6 +121,7 @@ import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) import Data.List (intercalate, nub, isPrefixOf)+import qualified Data.Map as Map import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess))@@ -404,7 +405,10 @@ printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL () printCounterexample cexTy exprDoc vs =   do ppOpts <- getPPValOpts-     docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs+     -- NB: Use a precedence of 1 here, as `vs` will be pretty-printed as+     -- arguments to the function in `exprDoc`. This ensures that arguments+     -- are parenthesized as needed.+     docs <- mapM (rEval . E.ppValuePrec Concrete ppOpts 1) vs      let cexRes = case cexTy of            SafetyViolation    -> [text "~> ERROR"]            PredicateFalsified -> [text "= False"]@@ -1823,7 +1827,7 @@         depList show               "includes" (Set.toList (M.fiIncludeDeps fi))        depList (show . show . pp) "imports"  (Set.toList (M.fiImportDeps  fi))-       depList show               "foreign"  (Set.toList (M.fiForeignDeps fi))+       depList show               "foreign"  (Map.toList (M.fiForeignDeps fi))         rPutStrLn "}" 

@@ -34,18 +34,20 @@          rnEnv  = M.mctxNames  fe          disp   = M.mctxNameDisp fe -         vNames = M.lookupListNS M.NSValue  qname rnEnv-         tNames = M.lookupListNS M.NSType   qname rnEnv-         mNames = M.lookupListNS M.NSModule qname rnEnv+         vNames = M.lookupListNS M.NSValue       qname rnEnv+         cNames = M.lookupListNS M.NSConstructor qname rnEnv+         tNames = M.lookupListNS M.NSType        qname rnEnv+         mNames = M.lookupListNS M.NSModule      qname rnEnv       let helps = map (showTypeHelp params env disp) tNames ++                  map (showValHelp params env disp qname) vNames +++                 map (showConHelp env disp qname) cNames ++                  map (showModHelp env disp) mNames           separ = rPutStrLn "            ---------"      sequence_ (intersperse separ helps) -     when (null (vNames ++ tNames ++ mNames)) $+     when (null (vNames ++ cNames ++ tNames ++ mNames)) $        rPrint $ "Undefined name:" <+> pp qname  @@ -84,7 +86,7 @@     foldr addName emptySummary (Set.toList (M.ifsPublic info))   where   addName x ns = fromMaybe ns-               $ msum [ addT <$> msum [fromTS, fromNT, fromAT]+               $ msum [ addT <$> msum [fromTS, fromNT ]                       , addV <$> fromD                       , addM <$> msum [ fromM, fromS, fromF ]                       ]@@ -106,12 +108,9 @@     fromTS = do def <- Map.lookup x (M.ifTySyns env)                 pure (T.kindOf def, T.tsDoc def) -    fromNT = do def <- Map.lookup x (M.ifNewtypes env)+    fromNT = do def <- Map.lookup x (M.ifNominalTypes env)                 pure (T.kindOf def, T.ntDoc def) -    fromAT = do def <- Map.lookup x (M.ifAbstractTypes env)-                pure (T.kindOf def, T.atDoc def)-     fromD = do def <- Map.lookup x (M.ifDecls env)                pure (M.ifDeclSig def, M.ifDeclDoc def, M.ifDeclFixity def) @@ -230,7 +229,7 @@   M.ModContextParams -> M.IfaceDecls -> NameDisp -> T.Name -> REPL () showTypeHelp ctxparams env nameEnv name =   fromMaybe (noInfo nameEnv name) $-  msum [ fromTySyn, fromPrimType, fromNewtype, fromTyParam ]+  msum [ fromTySyn, fromNominal, fromTyParam ]    where   fromTySyn =@@ -240,31 +239,40 @@                   ]        return (doShowTyHelp nameEnv (pp ts) (T.tsDoc ts)) -  fromNewtype =-    do nt <- Map.lookup name (M.ifNewtypes env)-       let decl = pp nt $$ (pp name <+> text ":" <+> pp (T.newtypeConType nt))-       return $ doShowTyHelp nameEnv decl (T.ntDoc nt)+  fromNominal =+    do nt <- Map.lookup name (M.ifNominalTypes env)+       let decl kw =+             vcat+               [ kw <+> pp (T.ntName nt) <.> ":" <+> pp (T.kindOf nt)+               , ""+               , "Constructors:" <+>+                                   commaSep+                                   (map (pp . fst) (T.nominalTypeConTypes nt))+               ]+       case T.ntDef nt of+         T.Struct {} -> pure $ doShowTyHelp nameEnv (decl "newtype") (T.ntDoc nt)+         T.Enum {}   -> pure $ doShowTyHelp nameEnv (decl "enum") (T.ntDoc nt)+         T.Abstract  -> pure (primTypeHelp nt) -  fromPrimType =-    do a <- Map.lookup name (M.ifAbstractTypes env)-       pure $ do rPutStrLn ""-                 rPrint $ runDoc nameEnv $ nest 4-                        $ "primitive type" <+> pp (T.atName a)-                                   <+> ":" <+> pp (T.atKind a)+  primTypeHelp nt =+    do rPutStrLn ""+       rPrint $ runDoc nameEnv $ nest 4+              $ "primitive type" <+> pp (T.ntName nt)+                         <+> ":" <+> pp (T.kindOf nt) -                 let (vs,cs) = T.atCtrs a-                 unless (null cs) $-                   do let example = T.TCon (T.abstractTypeTC a)-                                           (map (T.TVar . T.tpVar) vs)-                          ns = T.addTNames vs emptyNameMap-                          rs = [ "•" <+> ppWithNames ns c | c <- cs ]-                      rPutStrLn ""-                      rPrint $ runDoc nameEnv $ indent 4 $-                                  backticks (ppWithNames ns example) <+>-                                  "requires:" $$ indent 2 (vcat rs)+       let vs = T.ntParams nt+       let cs = T.ntConstraints nt+       unless (null cs) $+         do let example = T.TNominal nt (map (T.TVar . T.tpVar) vs)+                ns = T.addTNames vs emptyNameMap+                rs = [ "•" <+> ppWithNames ns c | c <- cs ]+            rPutStrLn ""+            rPrint $ runDoc nameEnv $ indent 4 $+                        backticks (ppWithNames ns example) <+>+                        "requires:" $$ indent 2 (vcat rs) -                 doShowFix (T.atFixitiy a)-                 doShowDocString (T.atDoc a)+       doShowFix (T.ntFixity nt)+       doShowDocString (T.ntDoc nt)    allParamNames =     case ctxparams of@@ -293,14 +301,35 @@      rPrint (runDoc nameEnv (nest 4 decl))      doShowDocString doc +showConHelp :: M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL ()+showConHelp env nameEnv qname name =+  fromMaybe (noInfo nameEnv name) (Map.lookup name allCons)+  where+  allCons = foldr addCons mempty (M.ifNominalTypes env)+    where+    getDocs nt =+      case T.ntDef nt of+        T.Struct {} -> [ Nothing ]+        T.Enum cs   -> map (Just . T.ecDoc) cs+        T.Abstract  -> [] +    addCons nt mp = foldr (addCon nt) mp+                      (zip (T.nominalTypeConTypes nt) (getDocs nt))+    addCon nt ((c,t),d) = Map.insert c $+      do rPutStrLn ""+         rPrint (runDoc nameEnv $ vcat+            [ "Constructor of" <+> pp (T.ntName nt)+            , indent 4 $ hsep [ pp qname, ":", pp t ]+            ])+         maybe (pure ()) doShowDocString d + showValHelp ::   M.ModContextParams -> M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL ()  showValHelp ctxparams env nameEnv qname name =   fromMaybe (noInfo nameEnv name)-            (msum [ fromDecl, fromNewtype, fromParameter ])+            (msum [ fromDecl, fromParameter ])   where   fromDecl =     do M.IfaceDecl { .. } <- Map.lookup name (M.ifDecls env)@@ -320,10 +349,6 @@                         (guard ifDeclInfix >> return P.defaultFixity)              doShowDocString ifDeclDoc--  fromNewtype =-    do _ <- Map.lookup name (M.ifNewtypes env)-       return $ return ()    allParamNames =     case ctxparams of

@@ -126,6 +126,7 @@ import Data.List (intercalate, isPrefixOf, unfoldr, sortBy) import Data.Maybe (catMaybes) import Data.Ord (comparing)+import Data.Tuple (swap) import Data.Typeable (Typeable) import System.Directory (findExecutable) import System.FilePath (splitSearchPath, searchPathSeparator)@@ -979,6 +980,26 @@                EnvBool False -> setIt M.NoCoreLint                _             -> return () +  , OptionDescr "evalForeign" ["eval-foreign"] defaultEvalForeignOpt+    checkEvalForeign+    (unlines+      [ "How to evaluate 'foreign' bindings:"+      , "  * always  Always call the foreign implementation with the FFI and"+      , "            report an error on module load if it is unavailable."+      , "  * prefer  Call the foreign implementation with the FFI by default,"+      , "            and when unavailable, fall back to the cryptol"+      , "            implementation if present and report runtime error"+      , "            otherwise."+      , "  * never   Never use the FFI. Always call the cryptol implementation"+      , "            if present, and report runtime error otherwise."+      , "Note: changes take effect on module reload."+      ]) $+    \case EnvString s+            | Just p <- lookup s evalForeignOptMap -> do+              me <- getModuleEnv+              setModuleEnv me { M.meEvalForeignPolicy = p }+          _ -> pure ()+   , simpleOpt "hashConsing" ["hash-consing"] (EnvBool True) noCheck     "Enable hash-consing in the What4 symbolic backends." @@ -1119,6 +1140,26 @@     _ | Just n <- readMaybe s -> return (SomeSat n)     _                         -> panic "REPL.Monad.getUserSatNum"                                    [ "invalid satNum option" ]++checkEvalForeign :: Checker+checkEvalForeign (EnvString s)+  | Just _ <- lookup s evalForeignOptMap = noWarns Nothing+checkEvalForeign _ = noWarns $ Just $ "evalForeign must be one of: "+  ++ intercalate ", " (map fst evalForeignOptMap)++evalForeignOptMap :: [(String, M.EvalForeignPolicy)]+evalForeignOptMap =+  [ ("always", M.AlwaysEvalForeign)+  , ("prefer", M.PreferEvalForeign)+  , ("never", M.NeverEvalForeign)+  ]++defaultEvalForeignOpt :: EnvVal+defaultEvalForeignOpt =+  case lookup M.defaultEvalForeignPolicy (map swap evalForeignOptMap) of+    Just s -> EnvString s+    Nothing -> panic "defaultEvalForeignOpt"+      ["cannot find option value matching default EvalForeignPolicy"]  checkTimeMeasurementPeriod :: Checker checkTimeMeasurementPeriod (EnvNum n)

@@ -26,6 +26,7 @@  , CounterExampleType(..)    -- * FinType  , FinType(..)+ , FinNominalType(..)  , finType  , unFinType  , predArgTypes@@ -44,9 +45,12 @@   import Control.Monad (foldM)+import qualified Data.IntMap.Strict as IntMap import Data.IORef(IORef) import Data.List (genericReplicate) import Data.Ratio+import Data.Vector(Vector)+import qualified Data.Vector as Vector import qualified LibBF as FP  @@ -59,7 +63,8 @@ import           Cryptol.Eval.Value import           Cryptol.TypeCheck.AST import           Cryptol.TypeCheck.Solver.InfNat-import           Cryptol.Eval.Type (TValue(..), evalType,tValTy,tNumValTy)+import           Cryptol.Eval.Type+  (TValue(..), TNominalTypeValue(..), evalType,tValTy,tNumValTy,ConInfo(..)) import           Cryptol.Utils.Ident (Ident,prelPrim,floatPrim) import           Cryptol.Utils.RecordMap import           Cryptol.Utils.Panic@@ -118,8 +123,6 @@                   | EmptyResult                   | ProverError  String -- predArgTypes :: QueryType -> Schema -> Either String [FinType] predArgTypes qtype schema@(Forall ts ps ty)   | null ts && null ps =@@ -149,8 +152,12 @@     | FTSeq Integer FinType     | FTTuple [FinType]     | FTRecord (RecordMap Ident FinType)-    | FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)+    | FTNominal NominalType [Either Nat' TValue] FinNominalType +data FinNominalType =+    FStruct (RecordMap Ident FinType)+  | FEnum (Vector (ConInfo FinType))+ finType :: TValue -> Maybe FinType finType ty =   case ty of@@ -162,8 +169,12 @@     TVSeq n t           -> FTSeq n <$> finType t     TVTuple ts          -> FTTuple <$> traverse finType ts     TVRec fields        -> FTRecord <$> traverse finType fields-    TVNewtype u ts body -> FTNewtype u ts <$> traverse finType body-    TVAbstract {}       -> Nothing+    TVNominal u ts nv   -> FTNominal u ts <$>+      case nv of+        TVStruct body -> FStruct <$> traverse finType body+        TVEnum cs     -> FEnum   <$> traverse (traverse finType) cs+        TVAbstract    -> Nothing+     TVArray{}           -> Nothing     TVStream{}          -> Nothing     TVFun{}             -> Nothing@@ -179,7 +190,7 @@     FTSeq l ety       -> tSeq (tNum l) (finTypeToType ety)     FTTuple ftys      -> tTuple (finTypeToType <$> ftys)     FTRecord fs       -> tRec (finTypeToType <$> fs)-    FTNewtype u ts _  -> tNewtype u (map unArg ts)+    FTNominal u ts _  -> tNominal u (map unArg ts)  where   unArg (Left Inf)     = tInf   unArg (Left (Nat n)) = tNum n@@ -196,8 +207,12 @@     FTSeq n ety       -> TVSeq n (unFinType ety)     FTTuple ftys      -> TVTuple (unFinType <$> ftys)     FTRecord fs       -> TVRec   (unFinType <$> fs)-    FTNewtype u ts fs -> TVNewtype u ts (unFinType <$> fs) +    FTNominal u ts nv -> TVNominal u ts $+       case nv of+          FStruct fs  -> TVStruct (unFinType <$> fs)+          FEnum cs    -> TVEnum (fmap unFinType <$> cs)+ data VarShape sym   = VarBit (SBit sym)   | VarInteger (SInteger sym)@@ -207,6 +222,7 @@   | VarFinSeq Integer [VarShape sym]   | VarTuple [VarShape sym]   | VarRecord (RecordMap Ident (VarShape sym))+  | VarEnum (SInteger sym) (Vector (ConInfo (VarShape sym)))  ppVarShape :: Backend sym => sym -> VarShape sym -> Doc ppVarShape _sym (VarBit _b) = text "<bit>"@@ -222,6 +238,7 @@   ppRecord (map ppField (displayFields fs))  where   ppField (f,v) = pp f <+> char '=' <+> ppVarShape sym v+ppVarShape _sym (VarEnum {}) = text "<enum>"   -- | Flatten structured shapes (like tuples and sequences), leaving only@@ -241,6 +258,9 @@     VarFinSeq _ vs -> flattenShapes vs tl     VarTuple vs    -> flattenShapes vs tl     VarRecord fs   -> flattenShapes (recordElements fs) tl+    VarEnum _ cs   -> x : flattenShapes allCons tl+      where+      allCons = concatMap (Vector.toList . conFields) (Vector.toList cs)  varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym varShapeToValue sym var =@@ -253,6 +273,10 @@     VarFinSeq n vs -> VSeq n (finiteSeqMap sym (map (pure . varShapeToValue sym) vs))     VarTuple vs  -> VTuple (map (pure . varShapeToValue sym) vs)     VarRecord fs -> VRecord (fmap (pure . varShapeToValue sym) fs)+    VarEnum tag cons ->+      VEnum tag (IntMap.fromList+                   (zip [ 0 .. ] [ pure . varShapeToValue sym <$> c+                                 | c <- Vector.toList cons ]))  data FreshVarFns sym =   FreshVarFns@@ -277,8 +301,16 @@     FTSeq n t     -> VarFinSeq (toInteger n) <$> sequence (genericReplicate n (freshVar fns t))     FTTuple ts    -> VarTuple    <$> mapM (freshVar fns) ts     FTRecord fs   -> VarRecord   <$> traverse (freshVar fns) fs-    FTNewtype _ _ fs -> VarRecord <$> traverse (freshVar fns) fs+    FTNominal _ _ nv ->+      case nv of+        FStruct fs -> VarRecord <$> traverse (freshVar fns) fs+        FEnum conTs ->+          do let maxCon = toInteger (Vector.length conTs - 1)+             tag <- freshIntegerVar fns (Just 0) (Just maxCon)+             cons <- traverse (traverse (freshVar fns)) conTs+             pure (VarEnum tag cons) + computeModel ::   PrimMap ->   [FinType] ->@@ -332,6 +364,17 @@     (VarFinSeq _n vs, VarFinSeq _ xs) -> modelPred sym vs xs     (VarTuple vs, VarTuple xs) -> modelPred sym vs xs     (VarRecord vs, VarRecord xs) -> modelPred sym (recordElements vs) (recordElements xs)+    (VarEnum vi vcons,  VarEnum i cons) ->+      do tag     <- integerLit sym i+         sameTag <- intEq sym tag vi+         let i' = fromInteger i+             flds = Vector.toList . conFields+         sameFs  <- case (vcons Vector.!? i', cons Vector.!? i') of+                      (Just con1, Just con2) ->+                         modelPred sym (flds con1) (flds con2)+                      _ -> panic "varModelPred" ["malformed constructor"]+         bitAnd sym sameTag sameFs+     _ -> panic "varModelPred" ["variable shape mismatch!"]  @@ -344,13 +387,35 @@   go :: FinType -> VarShape Concrete.Concrete -> Expr   go ty val =     case (ty,val) of-      (FTNewtype nt ts tfs, VarRecord vfs) ->+      (FTNominal nt ts (FStruct tfs), VarRecord vfs) ->         let res = zipRecords (\_lbl v t -> go t v) vfs tfs          in case res of               Left _ -> mismatch -- different fields               Right efs ->-                let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts+                let con = case ntDef nt of+                            Struct c -> ntConName c+                            Enum {} -> panic "varToExpr" ["Enum, expected Struct"]+                            Abstract {} -> panic "varToExpr"+                              ["Abstract, expected Struct"]+                    f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar con) ts                  in EApp f (ERec efs)++      (FTNominal nt ts (FEnum cons), VarEnum tag conVs) ->+         foldl EApp conName args+         where+         tag' = fromInteger tag+         args = case (cons Vector.!? tag', conVs Vector.!? tag') of+                 (Just conT, Just conV) ->+                    Vector.toList+                       (Vector.zipWith go (conFields conT) (conFields conV))+                 _ -> panic "varToExpr" ["Malformed constructor"]++         conName =+           case ntDef nt of+             Enum cs | c : _ <- filter ((tag' ==) . ecNumber ) cs ->+                foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ecName c)) ts++             _ -> panic "varToExpr" ["Missing constructor"]        (FTRecord tfs, VarRecord vfs) ->         let res = zipRecords (\_lbl v t -> go t v) vfs tfs

@@ -34,9 +34,11 @@ import Control.Monad.IO.Class import Control.Monad (when, foldM, forM_) import Data.Maybe (fromMaybe)+import Data.Traversable(mapAccumL) import qualified Data.Map as Map import qualified Control.Exception as X import System.Exit (ExitCode(ExitSuccess))+import qualified Data.Vector as Vector  import LibBF(bfNaN) @@ -57,6 +59,7 @@ import qualified Cryptol.Eval as Eval import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Value as Eval+import           Cryptol.Eval.Type import           Cryptol.Eval.SBV import           Cryptol.Parser.Position (emptyRange) import           Cryptol.Symbolic@@ -316,7 +319,7 @@       getEOpts <- M.getEvalOptsAction -     ntEnv <- M.getNewtypes+     ntEnv <- M.getNominalTypes       -- The `addAsm` function is used to combine assumptions that      -- arise from the types of symbolic variables (e.g. Z n values@@ -351,7 +354,7 @@                  -- we apply it to the symbolic inputs.                  (safety,b) <- doSBVEval $                      do env <- Eval.evalDecls sym extDgs =<<-                                 Eval.evalNewtypeDecls sym ntEnv mempty+                                 Eval.evalNominalDecls sym ntEnv mempty                         v <- Eval.evalExpr sym env pcExpr                         appliedVal <- foldM (Eval.fromVFun sym) v args                         case pcQueryType of@@ -535,7 +538,17 @@         fs         = zip ns vs         r'         = recordFromFieldsWithDisplay (displayOrder r) fs -parseValue (FTNewtype _ _ r) cvs = parseValue (FTRecord r) cvs+parseValue (FTNominal _ _ nv) cvs =+  case nv of+    FStruct r -> parseValue (FTRecord r) cvs+    FEnum cons ->+      fromMaybe (panic "Cryptol.Symbolic.parseValue" ["no enum"]) $+      do (tag, cvs') <- SBV.genParse SBV.KUnbounded cvs+         let doCon input con =+               case parseValues (Vector.toList (conFields con)) input of+                 (vs,input') -> (input', con { conFields = Vector.fromList vs })+             (input3, conVs) = mapAccumL doCon cvs' cons+         pure (VarEnum tag conVs, input3)  parseValue (FTFloat e p) cvs =    (VarFloat FH.BF { FH.bfValue = bfNaN

@@ -309,7 +309,7 @@                        ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym)                ) prepareQuery sym ProverCommand { .. } = do-  ntEnv <- M.getNewtypes+  ntEnv <- M.getNominalTypes   case predArgTypes pcQueryType pcSchema of     Left msg -> pure (Left msg)     Right ts ->@@ -362,7 +362,7 @@         doW4Eval (w4 sym)          do env <- Eval.evalDecls sym extDgs =<<-                     Eval.evalNewtypeDecls sym ntEnv mempty+                     Eval.evalNominalDecls sym ntEnv mempty              v   <- Eval.evalExpr  sym env    pcExpr             appliedVal <-@@ -751,3 +751,6 @@       VarTuple <$> mapM (varShapeToConcrete evalFn) vs     VarRecord fs ->       VarRecord <$> traverse (varShapeToConcrete evalFn) fs+    VarEnum tag cons ->+      VarEnum <$> W4.groundEval evalFn tag+              <*> traverse (traverse (varShapeToConcrete evalFn)) cons

@@ -33,8 +33,12 @@ import Control.Monad          (liftM2) import Control.Monad.IO.Class (MonadIO(..)) import Data.Bits-import Data.List              (unfoldr, genericTake, genericIndex, genericReplicate)+import Data.List              (unfoldr, genericTake, genericIndex,+                               genericReplicate, mapAccumL)+import qualified Data.IntMap.Strict as IntMap import qualified Data.Sequence as Seq+import Data.Vector(Vector)+import qualified Data.Vector as Vector  import System.Random.TF.Gen import System.Random.TF.Instances@@ -46,8 +50,10 @@ import Cryptol.Backend.SeqMap (indexSeqMap, finiteSeqMap) import Cryptol.Backend.WordValue (wordVal) -import Cryptol.Eval.Type      (TValue(..))-import Cryptol.Eval.Value     (GenValue(..), ppValue, defaultPPOpts, fromVFun)+import Cryptol.Eval(evalEnumCon)+import Cryptol.Eval.Type      ( TValue(..), TNominalTypeValue(..), ConInfo(..)+                              , isNullaryCon )+import Cryptol.Eval.Value     ( GenValue(..), ppValue, defaultPPOpts, fromVFun) import Cryptol.TypeCheck.Solver.InfNat (widthInteger) import Cryptol.Utils.Ident    (Ident) import Cryptol.Utils.Panic    (panic)@@ -164,12 +170,18 @@     TVRec fs ->          do gs <- traverse (randomValue sym) fs             return (randomRecord gs)-    TVNewtype _ _ fs ->-         do gs <- traverse (randomValue sym) fs-            return (randomRecord gs)++    TVNominal _ _ nval ->+      case nval of+        TVStruct fs ->+          do gs <- traverse (randomValue sym) fs+             return (randomRecord gs)+        TVEnum cons -> randomCon sym <$>+                          traverse (traverse (randomValue sym)) cons+        TVAbstract -> Nothing+     TVArray{} -> Nothing     TVFun{} -> Nothing-    TVAbstract{} -> Nothing  {-# INLINE randomBit #-} @@ -270,6 +282,69 @@       let (v, g') = gen sz g       in seq v (g', v) +-- | Generate a random constructor value belonging to an enum definition.+--+-- For the purposes of random testing, constructors with zero fields (i.e.,+-- nullary constructors) are less interesting than constructors with at least+-- one field (i.e., non-nullary constructors). For example, given+-- @enum Maybe a = Nothing | Just a@, we would like to generate more @Just@+-- values than @Nothing@ values. To ensure this, we employ the following+-- approach:+--+-- 1. If all constructors are nullary, then randomly pick one of these+--    constructors, where each constructor has an equal chance of being picked.+--+-- 2. If all constructors are non-nullary, then randomly pick one of these+--    constructors, where each constructor has an equal chance of being picked.+--    Then pick random values for each field in the constructor.+--+-- 3. Otherwise, pick a random number between 1 and 100. If the number is less+--    than or equal to 25, then randomly pick a nullary constructor. Otherwise,+--    randomly pick a non-nullary constructor. This biases the results so that+--    nullary constructors are only picked ~25% of the time.+randomCon ::+  forall sym g.+  (Backend sym, RandomGen g) =>+  sym ->+  Vector (ConInfo (Gen g sym)) ->+  Gen g sym+randomCon sym cons+    -- (1) from the Haddocks+  | null nonNullaryCons+  = randomCon' nullaryLen nullaryCons++    -- (2) from the Haddocks+  | null nullaryCons+  = randomCon' nonNullaryLen nonNullaryCons++    -- (3) from the Haddocks+  | otherwise+  = \sz g0 ->+      let (x :: Int, g1) = randomR (1, 100) g0 in+      if x <= 25+         then randomCon' nullaryLen nullaryCons sz g1+         else randomCon' nonNullaryLen nonNullaryCons sz g1+  where+    (nullaryLen,nullaryCons, nonNullaryLen, nonNullaryCons) =+       let check (!nullLen,nullary,!nonNullLen,nonNullary) i con+             | isNullaryCon con = ( 1+nullLen,(i,con) : nullary+                                  , nonNullLen, nonNullary)+             | otherwise        = (nullLen, nullary+                                  , 1+nonNullLen, (i,con) : nonNullary)+        in Vector.ifoldl' check (0,[],0,[]) cons++    randomCon' :: Int -> [(Int, ConInfo (Gen g sym))] -> Gen g sym+    randomCon' conLen cons' sz g0 =+      let (idx, g1) = randomR (0, conLen - 1) g0+          (num, con) = cons' !! idx+          (g2, !flds') =+            mapAccumL+              (\g gen ->+                let (v, g') = gen sz g in+                seq v (g', v))+              g1 (conFields con) in+      (($ flds') <$> evalEnumCon sym (conIdent con) num, g2)+ randomFloat ::   (Backend sym, RandomGen g) =>   sym ->@@ -398,8 +473,12 @@   TVTuple els -> product <$> mapM typeSize els   TVRec fs -> product <$> traverse typeSize fs   TVFun{} -> Nothing-  TVAbstract{} -> Nothing-  TVNewtype _ _ tbody -> typeSize (TVRec tbody)+  TVNominal _ _ nv ->+    case nv of+      TVStruct tbody -> typeSize (TVRec tbody)+      TVEnum cons -> sum <$> mapM (conSize . conFields) cons+        where conSize = foldr (\t sz -> liftM2 (*) (typeSize t) sz) (Just 1)+      TVAbstract -> Nothing  {- | Returns all the values in a type.  Returns an empty list of values, for types where 'typeSize' returned 'Nothing'. -}@@ -430,8 +509,16 @@       | xs <- traverse typeValues fs       ]     TVFun{} -> []-    TVAbstract{} -> []-    TVNewtype _ _ tbody -> typeValues (TVRec tbody)+    TVNominal _ _ nv ->+      case nv of+        TVStruct tbody -> typeValues (TVRec tbody)+        TVEnum cons ->+          [ VEnum (toInteger tag) (IntMap.singleton tag con')+          | (tag,con) <- zip [0..] (Vector.toList cons)+          , vs        <- mapM typeValues (conFields con)+          , let con' = con { conFields = pure <$> vs }+          ]+        TVAbstract -> []  -------------------------------------------------------------------------------- -- Driver function

@@ -187,6 +187,8 @@       ESel e s        -> ESel    <$> go e  <*> return s       ESet ty e s v   -> ESet ty <$> go e  <*> return s <*> go v       EIf e1 e2 e3    -> EIf     <$> go e1 <*> go e2 <*> go e3+      ECase e as d    -> ECase   <$> go e  <*> traverse (rewCase rews) as+                                           <*> traverse (rewCase rews) d        EComp len t e mss -> EComp len t <$> go e  <*> mapM (mapM (rewM rews)) mss       EVar _          -> return expr@@ -204,6 +206,9 @@       EPropGuards guards ty -> EPropGuards <$> (\(props, e) -> (,) <$> pure props <*> go e) `traverse` guards <*> pure ty  +rewCase :: RewMap -> CaseAlt -> M CaseAlt+rewCase rew (CaseAlt xs e) = CaseAlt xs <$> rewE rew e+ rewM :: RewMap -> Match -> M Match rewM rews ma =   case ma of@@ -218,9 +223,9 @@                  return d { dDefinition = e }  rewDef :: RewMap -> DeclDef -> M DeclDef-rewDef rews (DExpr e)    = DExpr <$> rewE rews e-rewDef _    DPrim        = return DPrim-rewDef _    (DForeign t) = return $ DForeign t+rewDef rews (DExpr e)       = DExpr <$> rewE rews e+rewDef _    DPrim           = return DPrim+rewDef rews (DForeign t me) = DForeign t <$> traverse (rewE rews) me  rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup rewDeclGroup rews dg =@@ -240,12 +245,17 @@    consider d   =     case dDefinition d of-      DPrim      -> Left d-      DForeign _ -> Left d-      DExpr e    -> let (tps,props,e') = splitTParams e-                    in if not (null tps) && notFun e'-                        then Right (d, tps, props, e')-                        else Left d+      DPrim         -> Left d+      DForeign _ me -> case me of+                         Nothing -> Left d+                         Just e  -> conExpr e+      DExpr e       -> conExpr e+    where+    conExpr e =+      let (tps,props,e') = splitTParams e+      in if not (null tps) && notFun e'+          then Right (d, tps, props, e')+          else Left d    rewSame ds =      do new <- forM (NE.toList ds) $ \(d,_,_,e) ->

@@ -85,6 +85,9 @@     ESel e s      -> ESel <$> specializeExpr e <*> pure s     ESet ty e s v -> ESet ty <$> specializeExpr e <*> pure s <*> specializeExpr v     EIf e1 e2 e3  -> EIf <$> specializeExpr e1 <*> specializeExpr e2 <*> specializeExpr e3+    ECase e as d   -> ECase <$> specializeExpr e+                            <*> traverse specializeCaseAlt as+                            <*> traverse specializeCaseAlt d     EComp len t e mss -> EComp len t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss     -- Bindings within list comprehensions always have monomorphic types.     EVar {}       -> specializeConst expr@@ -117,6 +120,8 @@           pm <- liftSpecT getPrimMap           pure $ eError pm ty "no constraint guard was satisfied" +specializeCaseAlt :: CaseAlt -> SpecM CaseAlt+specializeCaseAlt (CaseAlt xs e) = CaseAlt xs <$> specializeExpr e  specializeMatch :: Match -> SpecM Match specializeMatch (From qn l t e) = From qn l t <$> specializeExpr e@@ -201,11 +206,11 @@                  qname' <- freshName qname ts -- New type instance, record new name                  sig' <- instantiateSchema ts n (dSignature decl)                  modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Nothing))) qname)+                 let spec e = specializeExpr =<< instantiateExpr ts n e                  rhs' <- case dDefinition decl of-                           DExpr e    -> do e' <- specializeExpr =<< instantiateExpr ts n e-                                            return (DExpr e')-                           DPrim      -> return DPrim-                           DForeign t -> return $ DForeign t+                           DExpr e       -> DExpr <$> spec e+                           DPrim         -> return DPrim+                           DForeign t me -> DForeign t <$> traverse spec me                  let decl' = decl { dName = qname', dSignature = sig', dDefinition = rhs' }                  modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Just decl'))) qname)                  return (EVar qname')

@@ -86,7 +86,7 @@                 [ P.Bind                     { P.bName      = P.Located { P.srcRange = loc, P.thing = fresh }                     , P.bParams    = []-                    , P.bDef       = P.Located (inpRange inp) (P.DExpr expr)+                    , P.bDef       = P.Located (inpRange inp) (P.exprDef expr)                     , P.bPragmas   = []                     , P.bSignature = Nothing                     , P.bMono      = False

@@ -36,6 +36,7 @@ import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) import Cryptol.Parser.Position(Located,Range,HasLoc(..)) import Cryptol.ModuleSystem.Name+import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Exports(ExportSpec(..)                                    , isExportedBind, isExportedType, isExported)@@ -106,11 +107,14 @@                        -- These have everything from this module and all submodules                      , mTySyns           :: Map Name TySyn-                     , mNewtypes         :: Map Name Newtype-                     , mPrimTypes        :: Map Name AbstractType+                     , mNominalTypes     :: Map Name NominalType                      , mDecls            :: [DeclGroup]                      , mSubmodules       :: Map Name (IfaceNames Name)                      , mSignatures       :: !(Map Name ModParamNames)++                     , mInScope          :: NamingEnv+                       -- ^ Things in scope at the top level.+                       --   Submodule in-scope information is in 'mSubmodules'.                      } deriving (Show, Generic, NFData)  emptyModule :: mname -> ModuleG mname@@ -128,28 +132,34 @@     , mNested           = mempty      , mTySyns           = mempty-    , mNewtypes         = mempty-    , mPrimTypes        = mempty+    , mNominalTypes     = mempty     , mDecls            = mempty     , mFunctors         = mempty     , mSubmodules       = mempty     , mSignatures       = mempty++    , mInScope          = mempty     }  -- | Find all the foreign declarations in the module and return their names and FFIFunTypes. findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)]-findForeignDecls = mapMaybe getForeign . mDecls-  where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType })-          = Just (dName, ffiType)-        -- Recursive DeclGroups can't have foreign decls-        getForeign _ = Nothing+findForeignDecls = mapMaybe getForeign . concatMap groupDecls . mDecls+  where getForeign d =+          case dDefinition d of+            DForeign ffiType _ -> Just (dName d, ffiType)+            _                  -> Nothing --- | Find all the foreign declarations that are in functors.+-- | Find all the foreign declarations that are in functors, including in the+-- top-level module itself if it is a functor. -- This is used to report an error findForeignDeclsInFunctors :: ModuleG mname -> [Name]-findForeignDeclsInFunctors = concatMap fromM . Map.elems . mFunctors+findForeignDeclsInFunctors mo+  | isParametrizedModule mo = fromM mo+  | otherwise               = findInSubs mo   where-  fromM m = map fst (findForeignDecls m) ++ findForeignDeclsInFunctors m+  findInSubs :: ModuleG mname -> [Name]+  findInSubs = concatMap fromM . Map.elems . mFunctors+  fromM m = map fst (findForeignDecls m) ++ findInSubs m   @@ -172,6 +182,11 @@                                            --   The included type gives the type of the record being updated              | EIf Expr Expr Expr        -- ^ If-then-else+            | ECase Expr (Map Ident CaseAlt) (Maybe CaseAlt)+              -- ^ Case expression. The keys are the name of constructors+              -- `Nothing` for default case, the expresssions are what to+              -- do if the constructor matches.  If the constructor binds+              -- variables, then then the expr should be `EAbs`             | EComp Type Type Expr [[Match]]                                         -- ^ List comprehensions                                         --   The types cache the length of the@@ -211,6 +226,10 @@                deriving (Show, Generic, NFData) +-- | Used for case expressions.  Similar to a lambda, the variables+-- are bound by the value examined in the case.+data CaseAlt = CaseAlt [(Name,Type)] Expr+  deriving (Show, Generic, NFData)  data Match  = From Name Type Type Expr                                   -- ^ Type arguments are the length and element@@ -238,7 +257,9 @@                        } deriving (Generic, NFData, Show)  data DeclDef    = DPrim-                | DForeign FFIFunType+                -- | Foreign functions can have an optional cryptol+                -- implementation+                | DForeign FFIFunType (Maybe Expr)                 | DExpr Expr                   deriving (Show, Generic, NFData) @@ -294,9 +315,17 @@                     $ sep [ text "if"   <+> ppW e1                           , text "then" <+> ppW e2                           , text "else" <+> ppW e3 ]+      ECase e arms dflt ->+        optParens (prec > 0) $+        vcat [ "case" <+> pp e <+> "of"+             , indent 2 (vcat ppArms $$ ppDflt)+             ]+        where+        ppArms  = [ pp i <+> pp c | (i,c) <- reverse (Map.toList arms) ]+        ppDflt  = maybe mempty pp dflt        EComp _ _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms)-                          in brackets $ ppW e <+> (align (vcat (map arm mss)))+                          in brackets $ ppW e <+> align (vcat (map arm mss))        EVar x        -> ppPrefixName x @@ -344,6 +373,10 @@     ppW x   = ppWithNames nm x     ppWP x  = ppWithNamesPrec nm x +instance PP CaseAlt where+  ppPrec _ (CaseAlt xs e) = hsep (map ppV xs) <+> "->" <+> pp e+    where ppV (x,t) = parens (pp x <.> ":" <+> pp t)+ ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc ppLam nm prec [] [] [] e = nest 2 (ppWithNamesPrec nm prec e) ppLam nm prec ts ps xs e =@@ -456,9 +489,12 @@       ++ [ nest 2 (sep [pp dName <+> text "=", ppWithNames nm dDefinition]) ]  instance PP (WithNames DeclDef) where-  ppPrec _ (WithNames DPrim _)        = text "<primitive>"-  ppPrec _ (WithNames (DForeign _) _) = text "<foreign>"-  ppPrec _ (WithNames (DExpr e) nm)   = ppWithNames nm e+  ppPrec _ (WithNames DPrim _) = text "<primitive>"+  ppPrec _ (WithNames (DForeign _ me) nm) =+    case me of+      Just e -> text "(foreign)" <+> ppWithNames nm e+      Nothing -> text "<foreign>"+  ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e  instance PP Decl where   ppPrec = ppWithNamesPrec IntMap.empty

@@ -94,6 +94,13 @@               | TypeMismatch TypeSource Path Type Type                 -- ^ Expected type, inferred type +              | EnumTypeMismatch Type+                -- ^ Expected an enum type, but inferred the supplied 'Type'+                --   instead, which is not an enum. This corresponds to the+                --   \"Matched Expression Must Have a Known Enum Type\"+                --   restriction for @case@ expressions, as described in the+                --   Cryptol Reference Manual.+               | SchemaMismatch Ident Schema Schema                 -- ^ Name of module parameter, expected scehema, actual schema.                 -- This may happen when instantiating modules.@@ -172,6 +179,18 @@               | InvalidConstraintGuard Prop                 -- ^ The given constraint may not be used as a constraint guard +              | InvalidConPat Int Int+                -- ^ Bad constructor pattern.+                -- 1) Number of parameters we have,+                -- 2) Number of parameters we need.++              | UncoveredConPat [Name]+                -- ^ A @case@ expression is non-exhaustive and does not cover+                --   the supplied constructor 'Name's.++              | OverlappingPat (Maybe Ident) [Range]+                -- ^ Overlapping patterns in a case+               | TemporaryError Doc                 -- ^ This is for errors that don't fit other cateogories.                 -- We should not use it much, and is generally to be used@@ -207,7 +226,11 @@     KindMismatch {}                                  -> 10     TyVarWithParams {}                               -> 9     TypeMismatch {}                                  -> 8+    EnumTypeMismatch {}                              -> 7     SchemaMismatch {}                                -> 7+    InvalidConPat {}                                 -> 7+    UncoveredConPat {}                               -> 7+    OverlappingPat {}                                -> 3     RecursiveType {}                                 -> 7     NotForAll {}                                     -> 6     TypeVariableEscaped {}                           -> 5@@ -281,6 +304,10 @@       SchemaMismatch i t1 t2  ->         SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2)       TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)+      EnumTypeMismatch t        -> EnumTypeMismatch !$ apSubst su t+      InvalidConPat {}          -> err+      UncoveredConPat {}        -> err+      OverlappingPat {}         -> err       RecursiveType src pa t1 t2   -> RecursiveType src pa !$ (apSubst su t1) !$ (apSubst su t2)       UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs       UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs@@ -331,6 +358,10 @@       RecursiveTypeDecls {}     -> Set.empty       SchemaMismatch _ t1 t2    -> fvs (t1,t2)       TypeMismatch _ _ t1 t2    -> fvs (t1,t2)+      EnumTypeMismatch t        -> fvs t+      InvalidConPat {}          -> Set.empty+      UncoveredConPat {}        -> Set.empty+      OverlappingPat {}         -> Set.empty       RecursiveType _ _ t1 t2   -> fvs (t1,t2)       UnsolvedGoals gs          -> fvs gs       UnsolvableGoals gs        -> fvs gs@@ -390,7 +421,7 @@                                               <+> ppWithNames names ty        NonExhaustivePropGuards n ->-        text "Could not prove that the constraint guards used in defining" <+> +        text "Could not prove that the constraint guards used in defining" <+>         pp n <+> text "were exhaustive."  instance PP (WithNames Error) where@@ -439,7 +470,7 @@         addTVarsDescsAfter names err $         nested "Malformed type."           ("Type synonym" <+> nm t <+> "was applied to" <+>-            pl extra "extra parameters" <.> text ".")+            pl extra "extra parameter" <.> text ".")        TooFewTyParams t few ->         addTVarsDescsAfter names err $@@ -461,6 +492,19 @@             ++ ppCtxt pa             ++ ["When checking" <+> pp src] +      EnumTypeMismatch t ->+        case tNoUser t of+          TVar {} ->+            nested "Failed to infer the type of cased expression."+              "Try giving the expression an explicit type annotation."+          _ ->+            addTVarsDescsAfter names err $+            nested "Type mismatch in cased expresson:" $+              vcat+                [ "Expected: an `enum` type"+                , "Inferred:" <+> ppWithNames names t+                ]+       SchemaMismatch i t1 t2 ->           addTVarsDescsAfter names err $           nested ("Type mismatch in module parameter" <+> quotes (pp i)) $@@ -469,6 +513,27 @@             , "Actual type:"   <+> ppWithNames names t2             ] +      InvalidConPat have need ->+        addTVarsDescsAfter names err $+        nested "Invalid constructor pattern" $+          vcat+            [ "Expected" <+> int need <+> "parameters,"+            , "but there are" <+> int have <.> "."+            ]++      UncoveredConPat conNames ->+        "Case expression does not cover the following patterns:"+        $$ commaSep (map pp conNames)++      OverlappingPat mbCon rs ->+        addTVarsDescsAfter names err $+        nested ("Overlapping choices for" <+> what <.> ":") $+          vcat [ "Pattern at" <+> pp r | r <- rs ]+        where+        what = case mbCon of+                 Just i  -> "constructor" <+> pp i+                 Nothing -> "default case"+       UnsolvableGoals gs -> explainUnsolvable names gs        UnsolvedGoals gs@@ -574,6 +639,7 @@               NSValue     -> "value"               NSType      -> "type"               NSModule    -> "module"+              NSConstructor -> "constructor"        FunctorInstanceBadBacktick bad ->         case bad of@@ -607,7 +673,7 @@                 [ "Parameter name:" <+> pp x                 , "Parameterized instantiation requires distinct parameter names"                 ]-                +        UnsupportedFFIKind src param k ->         nested "Kind of type variable unsupported for FFI: " $

@@ -10,13 +10,11 @@  {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE PatternGuards #-}-{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE BlockArguments #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}-{-# LANGUAGE LambdaCase #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Redundant <$>" #-} {-# HLINT ignore "Redundant <&>" #-}@@ -43,7 +41,7 @@ import           Cryptol.TypeCheck.Solve import           Cryptol.TypeCheck.SimpType(tMul) import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,-                                        checkPropSyn,checkNewtype,+                                        checkPropSyn,checkNewtype,checkEnum,                                         checkParameterType,                                         checkPrimType,                                         checkParameterConstraints,@@ -79,13 +77,14 @@ inferTopModule m =   case P.mDef m of     P.NormalModule ds ->-      do newModuleScope (thing (P.mName m)) (P.exportedDecls ds)+      do newModuleScope (thing (P.mName m)) (P.exportedDecls ds) (P.mInScope m)          checkTopDecls ds          proveModuleTopLevel          endModule      P.FunctorInstance f as inst ->-      do mb <- doFunctorInst (P.ImpTop <$> P.mName m) f as inst Nothing+      do mb <- doFunctorInst+           (P.ImpTop <$> P.mName m) f as inst (P.mInScope m) Nothing          case mb of            Just mo -> pure mo            Nothing -> panic "inferModule" ["Didnt' get a module"]@@ -202,6 +201,7 @@     P.EFun      {} -> mono     P.ESplit    {} -> mono     P.EPrefix   {} -> mono+    P.ECase {}     -> mono      P.EParens e       -> appTys e ts tGoal     P.EInfix a op _ b -> appTys (P.EVar (thing op) `P.EApp` a `P.EApp` b) ts tGoal@@ -476,9 +476,134 @@            P.PrefixComplement -> "complement"          checkE (P.EApp prim e) tGoal +    P.ECase e as ->+     do et   <- newType CasedExpression KType+        alts <- forM as \a -> checkCaseAlt a et tGoal+        rng  <- curRange+        e1   <- checkE e (WithSource et CasedExpression (Just rng))++        -- Check for overlapping cases that follow default patterns, e.g.,+        --+        --   enum Foo = A | B+        --   f : Foo -> Bit+        --   f l =+        --     case l of+        --       _ -> True+        --       B -> False+        --+        -- In this example, the `B` case overlaps the catch-all `_` case.+        let defltAltAndOthers = dropWhile (\(_,x,_) -> isJust x) alts+        defltAlt <-+          case defltAltAndOthers of+            [] ->+              pure Nothing+            defltAlt@(_,defltPat,_):otherAlts -> do+              unless (null otherAlts) $+                recordError $+                OverlappingPat defltPat [ r | (r,_,_) <- defltAltAndOthers ]+              pure (Just defltAlt)++        -- Check that there are no overlapping patterns among the case+        -- alternatives, e.g.,+        --+        --   enum Foo = A | B+        --   g : Foo -> Bit+        --   g l =+        --     case l of+        --       A -> True+        --       B -> True+        --       B -> False+        --+        -- In this example, the two `B` cases overlap.+        let mp1 = Map.fromListWith (++) [ (x,[(r,y)]) | (r,x,y) <- alts ]+        forM_ (Map.toList mp1) \(mb,cs) ->+          case cs of+            [_] -> pure ()+            _   -> recordError (OverlappingPat mb [ r | (r,_) <- cs ])++        -- Check that the type of the scrutinee is unambiguously an enum.+        et' <- applySubst et+        cons <- case getLoc e of+                 Just r -> inRange r (expectEnum et')+                 Nothing -> expectEnum et'++        -- Check that the case expression covers all possible constructors.+        -- If there is a default case, there is no need to check anything,+        -- since the default case will catch any constructors that weren't+        -- explicitly matched on.+        case defltAlt of+          Just _ -> pure ()+          Nothing ->+            let uncoveredCons =+                  filter+                    (\con -> Map.notMember (Just (nameIdent (ecName con))) mp1)+                    cons in+            unless (null uncoveredCons) $+              recordError $ UncoveredConPat $ map ecName uncoveredCons++        let dflt = fmap (\(_,_,y) -> y) defltAlt+        let arms = Map.fromList [ (i,a) | (_,Just i, a) <- alts ]+        pure (ECase e1 arms dflt)+     P.EParens e -> checkE e tGoal  +checkCaseAlt ::+  P.CaseAlt Name -> Type -> TypeWithSource ->+  InferM (Range, Maybe Ident, CaseAlt)+checkCaseAlt (P.CaseAlt pat e) srcT resT =+  case pat of+    P.PCon c ps ->+      inRange (srcRange c) $+      do (_tArgs,_pArgs,fTs,cresT) <- instantiatePCon (thing c)+         -- XXX: should we store these somewhere?++         let have = length ps+             need = length fTs+         unless (have == need) (recordError (InvalidConPat have need))+         let expect = WithSource+                        { twsType = srcT+                        , twsRange = Just (srcRange c)+                        , twsSource = ConPat+                        }+         newGoals CtExactType =<< unify expect cresT+         xs <- zipWithM checkNested ps fTs+         e1 <- withMonoTypes (Map.fromList xs) (checkE e resT)+         pure (srcRange c, Just (nameIdent (thing c)), mkAlt xs e1)++    P.PVar x ->+      do let xty = (thing x, Located (srcRange x) srcT)+         e1 <- withMonoType xty (checkE e resT)+         pure (srcRange x, Nothing, mkAlt [xty] e1)++    P.PLocated p r -> inRange r (checkCaseAlt (P.CaseAlt p e) srcT resT)++    P.PTyped p t ->+      do t1 <- checkType t (Just KType)+         rng <- curRange+         newGoals CtExactType =<<+           unify (WithSource t1 TypeFromUserAnnotation (Just rng)) srcT+         checkCaseAlt (P.CaseAlt p e) t1 resT++    _ -> panic "checkCaseAlt" ["Unexpected pattern"]+  where+  checkNested p ty =+    case p of+      P.PVar x -> pure (thing x, Located (srcRange x) ty)+      P.PLocated p1 r -> inRange r (checkNested p1 ty)+      P.PTyped p1 t ->+        do t1 <- checkType t (Just KType)+           rng <- curRange+           newGoals CtExactType =<<+             unify (WithSource t1 TypeFromUserAnnotation (Just rng)) ty+           checkNested p1 t1+      _ -> panic "checkNested" ["Unexpected pattern"]++++  mkAlt xs = CaseAlt [ (x, thing t) | (x,t) <- xs ]++ checkRecUpd ::   Maybe (P.Expr Name) -> [ P.UpdField Name ] -> TypeWithSource -> InferM Expr checkRecUpd mb fs tGoal =@@ -610,6 +735,22 @@          return res  +-- | Retrieve the constructors from a type that is expected to be unambiguously+-- an enum, throwing an error if this is not the case.+expectEnum :: Type -> InferM [EnumCon]+expectEnum ty =+  case ty of+    TUser _ _ ty' ->+      expectEnum ty'++    TNominal nt _+      |  Enum ecs <- ntDef nt+      -> pure ecs++    _ -> do+      recordError (EnumTypeMismatch ty)+      pure []+ expectFin :: Int -> TypeWithSource -> InferM () expectFin n tGoal@(WithSource ty src rng) =   case ty of@@ -872,9 +1013,9 @@   -- so no need to look at noSig    hasConstraintGuards b =-    case thing (P.bDef b) of-      P.DPropGuards {} -> True-      _                -> False+    case P.bindImpl b of+      Just (P.DPropGuards {}) -> True+      _                       -> False   @@ -895,10 +1036,11 @@      Just s ->       do let wildOk = case thing bDef of-                        P.DForeign {}    -> NoWildCards-                        P.DPrim          -> NoWildCards-                        P.DExpr {}       -> AllowWildCards-                        P.DPropGuards {} -> NoWildCards+                        P.DForeign {}                   -> NoWildCards+                        P.DPrim                         -> NoWildCards+                        P.DImpl i -> case i of+                                       P.DExpr {}       -> AllowWildCards+                                       P.DPropGuards {} -> NoWildCards          s1 <- checkSchema wildOk s          return ((name, ExtVar (fst s1)), Left (checkSigB b s1)) @@ -993,9 +1135,9 @@           genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs          genB d = d { dDefinition = case dDefinition d of-                                      DExpr e    -> DExpr (genE e)-                                      DPrim      -> DPrim-                                      DForeign t -> DForeign t+                                      DExpr e       -> DExpr (genE e)+                                      DPrim         -> DPrim+                                      DForeign t me -> DForeign t (genE <$> me)                     , dSignature  = Forall asPs qs                                   $ apSubst su $ sType $ dSignature d                     }@@ -1017,31 +1159,33 @@      P.DPrim -> panic "checkMonoB" ["Primitive with no signature?"] -    P.DForeign -> panic "checkMonoB" ["Foreign with no signature?"]+    P.DForeign _ -> panic "checkMonoB" ["Foreign with no signature?"] -    P.DExpr e ->-      do let nm = thing (P.bName b)-         let tGoal = WithSource t (DefinitionOf nm) (getLoc b)-         e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal-         let f = thing (P.bName b)-         return Decl { dName = f-                     , dSignature = Forall [] [] t-                     , dDefinition = DExpr e1-                     , dPragmas = P.bPragmas b-                     , dInfix = P.bInfix b-                     , dFixity = P.bFixity b-                     , dDoc = P.bDoc b-                     }+    P.DImpl i ->+      case i of -    P.DPropGuards _ ->-      tcPanic "checkMonoB"-        [ "Used constraint guards without a signature at "-        , show . pp $ P.bName b ]+        P.DExpr e ->+          do let nm = thing (P.bName b)+             let tGoal = WithSource t (DefinitionOf nm) (getLoc b)+             e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal+             let f = thing (P.bName b)+             return Decl { dName = f+                         , dSignature = Forall [] [] t+                         , dDefinition = DExpr e1+                         , dPragmas = P.bPragmas b+                         , dInfix = P.bInfix b+                         , dFixity = P.bFixity b+                         , dDoc = P.bDoc b+                         } +        P.DPropGuards _ ->+          tcPanic "checkMonoB"+            [ "Used constraint guards without a signature at "+            , show . pp $ P.bName b ]+ -- XXX: Do we really need to do the defaulting business in two different places? checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl checkSigB b (Forall as asmps0 t0, validSchema) =-  let name = thing (P.bName b) in   case thing (P.bDef b) of      -- XXX what should we do with validSchema in this case?@@ -1056,10 +1200,13 @@         , dDoc        = P.bDoc b         } -    P.DForeign -> do+    P.DForeign mi -> do+      (asmps, t, me) <-+        case mi of+          Just i -> fmap Just <$> checkImpl i+          Nothing -> pure (asmps0, t0, Nothing)       let loc = getLoc b-          name' = thing $ P.bName b-          src = DefinitionOf name'+          src = DefinitionOf name       inRangeMb loc do         -- Ensure all type params are of kind #         forM_ as \a ->@@ -1067,10 +1214,10 @@             recordErrorLoc loc $ UnsupportedFFIKind src a $ tpKind a         withTParams as do           ffiFunType <--            case toFFIFunType (Forall as asmps0 t0) of+            case toFFIFunType (Forall as asmps t) of               Right (props, ffiFunType) -> ffiFunType <$ do-                ffiGoals <- traverse (newGoal (CtFFI name')) props-                proveImplication True (Just name') as asmps0 $+                ffiGoals <- traverse (newGoal (CtFFI name)) props+                proveImplication True (Just name) as asmps $                   validSchema ++ ffiGoals               Left err -> do                 recordErrorLoc loc $ UnsupportedFFIType src err@@ -1079,32 +1226,44 @@                   { ffiTParams = as, ffiArgTypes = []                   , ffiRetType = FFITuple [] }           pure Decl { dName       = thing (P.bName b)-                    , dSignature  = Forall as asmps0 t0-                    , dDefinition = DForeign ffiFunType+                    , dSignature  = Forall as asmps t+                    , dDefinition = DForeign ffiFunType me                     , dPragmas    = P.bPragmas b                     , dInfix      = P.bInfix b                     , dFixity     = P.bFixity b                     , dDoc        = P.bDoc b                     } -    P.DExpr e0 ->-      inRangeMb (getLoc b) $-      withTParams as $ do-        (t, asmps, e2) <- checkBindDefExpr [] asmps0 e0+    P.DImpl i -> do+      (asmps, t, expr) <- checkImpl i+      return Decl+        { dName       = name+        , dSignature  = Forall as asmps t+        , dDefinition = DExpr expr+        , dPragmas    = P.bPragmas b+        , dInfix      = P.bInfix b+        , dFixity     = P.bFixity b+        , dDoc        = P.bDoc b+        } -        return Decl-          { dName       = name-          , dSignature  = Forall as asmps t-          , dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)-          , dPragmas    = P.bPragmas b-          , dInfix      = P.bInfix b-          , dFixity     = P.bFixity b-          , dDoc        = P.bDoc b-          }+  where -    P.DPropGuards cases0 ->+    name = thing (P.bName b)++    checkImpl :: P.BindImpl Name -> InferM ([Prop], Type, Expr)+    checkImpl i =       inRangeMb (getLoc b) $-        withTParams as $ do+      withTParams as $+      case i of++        P.DExpr e0 -> do+          (t, asmps, e2) <- checkBindDefExpr [] asmps0 e0+          pure ( asmps+               , t+               , foldr ETAbs (foldr EProofAbs e2 asmps) as+               )++        P.DPropGuards cases0 -> do           asmps1 <- applySubstPreds asmps0           t1     <- applySubst t0           cases1 <- mapM checkPropGuardCase cases0@@ -1115,25 +1274,14 @@               -- necessarily hold               recordWarning (NonExhaustivePropGuards name) -          let schema = Forall as asmps1 t1--          return Decl-            { dName       = name-            , dSignature  = schema-            , dDefinition = DExpr-                              (foldr ETAbs-                                (foldr EProofAbs-                                  (EPropGuards cases1 t1)-                                asmps1)-                              as)-            , dPragmas    = P.bPragmas b-            , dInfix      = P.bInfix b-            , dFixity     = P.bFixity b-            , dDoc        = P.bDoc b-            }---  where+          pure ( asmps1+               , t1+               , foldr ETAbs+                   (foldr EProofAbs+                     (EPropGuards cases1 t1)+                   asmps1)+                 as+               )      checkBindDefExpr ::       [Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)@@ -1183,8 +1331,8 @@  @ f : {...} A-f | (B1, B2) => ... -  | (C1, C2, C2) => ... +f | (B1, B2) => ...+  | (C1, C2, C2) => ... @  we check that it is exhaustive by trying to prove the following@@ -1302,11 +1450,15 @@        P.TDNewtype tl ->         do t <- checkNewtype (P.tlValue tl) (thing <$> P.tlDoc tl)-           addNewtype t+           addNominal t +      P.TDEnum tl ->+        do t <- checkEnum (P.tlValue tl) (thing <$> P.tlDoc tl)+           addNominal t+       P.DPrimType tl ->         do t <- checkPrimType (P.tlValue tl) (thing <$> P.tlDoc tl)-           addPrimType t+           addNominal t         P.DInterfaceConstraint _ cs ->@@ -1322,13 +1474,15 @@              do newSubmoduleScope (thing (P.mName m))                                   (thing <$> P.tlDoc tl)                                   (P.exportedDecls ds)+                                  (P.mInScope m)                 checkTopDecls ds                 proveModuleTopLevel                 endSubmodule             P.FunctorInstance f as inst ->              do let doc = thing <$> P.tlDoc tl-                _ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst doc+                _ <- doFunctorInst+                  (P.ImpNested <$> P.mName m) f as inst (P.mInScope m) doc                 pure ()             P.InterfaceModule sig ->

@@ -11,6 +11,7 @@   , TypeArg(..)   , uncheckedTypeArg   , MaybeCheckedType(..)+  , instantiatePCon   ) where  import Cryptol.ModuleSystem.Name (nameIdent)@@ -60,7 +61,27 @@         where k' = kindOf t     Unchecked t -> checkType t (Just k) -+-- | Instantiate a pattern constructor.  Returns (A,B,C,D) where:+-- A) are the instantiations of the type parameters of the constructor+-- B) is how many proofs we would have if we had dictionaries+-- C) are the types of the fields of the constructor+-- D) is the type of the result of the constructor (i.e., what we are mathcing)+instantiatePCon :: Name -> InferM ([Type],Int,[Type],Type)+instantiatePCon nm =+  do vart <- lookupVar nm+     case vart of+       CurSCC {} -> panic "instantiatePCon" [ "CurSCC"]+       ExtVar s ->+         do (e,t) <- instantiateWith nm (EVar nm) s []+            let (_, tApps, proofApps) = splitExprInst e+                (fs,res) = splitFun t+            pure (tApps, proofApps,fs,res)+  where+  splitFun ty =+    case tIsFun ty of+      Nothing -> ([], ty)+      Just (a,b) -> (a:as,c)+        where (as,c) = splitFun b  instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr,Type) instantiateWith nm e s ts

@@ -40,9 +40,9 @@ genModDefines m =   Set.unions     [ Map.keysSet  (mTySyns m)-    , Map.keysSet  (mNewtypes m)-    , Set.fromList (map ntConName (Map.elems (mNewtypes m)))-    , Map.keysSet  (mPrimTypes m)+    , Map.keysSet  (mNominalTypes m)+    , Set.fromList (concatMap (map fst . nominalTypeConTypes)+                              (Map.elems (mNominalTypes m)))     , Set.fromList (map dName (concatMap groupDecls (mDecls m)))     , Map.keysSet  (mSubmodules m)     , Map.keysSet  (mFunctors m)@@ -65,8 +65,7 @@    , ifDefines = IfaceDecls     { ifTySyns          = mTySyns m-    , ifNewtypes        = mNewtypes m-    , ifAbstractTypes   = mPrimTypes m+    , ifNominalTypes    = mNominalTypes m     , ifDecls           = Map.fromList [ (qn,mkIfaceDecl d)                                        | dg <- mDecls m                                        , d  <- groupDecls dg

@@ -14,6 +14,7 @@   ( checkType   , checkSchema   , checkNewtype+  , checkEnum   , checkPrimType   , checkTySyn   , checkPropSyn@@ -26,12 +27,13 @@ import           Cryptol.Parser.Position import           Cryptol.TypeCheck.AST import           Cryptol.TypeCheck.Error+import           Cryptol.TypeCheck.Subst(listSubst,apSubst) import           Cryptol.TypeCheck.Monad hiding (withTParams) import           Cryptol.TypeCheck.SimpType(tRebuild) import           Cryptol.TypeCheck.SimpleSolver(simplify) import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)-import           Cryptol.TypeCheck.Subst(listSubst,apSubst) import           Cryptol.Utils.Panic (panic)+import           Cryptol.Utils.PP(pp,commaSep) import           Cryptol.Utils.RecordMap  import qualified Data.Map as Map@@ -39,7 +41,7 @@ import           Data.Maybe(fromMaybe) import           Data.Function(on) import           Data.Text (Text)-import           Control.Monad(unless,when,mplus)+import           Control.Monad(unless,mplus,forM,when)  -- | Check a type signature.  Returns validated schema, and any implicit -- constraints that we inferred.@@ -132,37 +134,86 @@                   }  -- | Check a newtype declaration.--- XXX: Do something with constraints.-checkNewtype :: P.Newtype Name -> Maybe Text -> InferM Newtype+checkNewtype :: P.Newtype Name -> Maybe Text -> InferM NominalType checkNewtype (P.Newtype x as con fs) mbD =   do ((as1,fs1),gs) <- collectGoals $        inRange (srcRange x) $-       do r <- withTParams NoWildCards newtypeParam as $+       do r <- withTParams NoWildCards nominalParam as $                flip traverseRecordMap fs $ \_n (rng,f) ->                  kInRange rng $ doCheckType f (Just KType)           simplifyAllConstraints           return r -     return Newtype { ntName   = thing x+     return NominalType+                    { ntName   = thing x+                    , ntKind   = KType                     , ntParams = as1                     , ntConstraints = map goal gs-                    , ntConName = con-                    , ntFields = fs1+                    , ntDef = Struct+                                StructCon { ntConName = con, ntFields = fs1 }+                    , ntFixity = Nothing                     , ntDoc = mbD                     } -checkPrimType :: P.PrimType Name -> Maybe Text -> InferM AbstractType+checkEnum :: P.EnumDecl Name -> Maybe Text -> InferM NominalType+checkEnum ed mbD =+  do let x = P.eName ed+     ((as1,cons1),gs) <- collectGoals $+       inRange (srcRange x) $+       do r <- withTParams NoWildCards nominalParam (P.eParams ed) $+               forM (P.eCons ed `zip` [0..]) \(tlC,nu) ->+                 do let con = P.tlValue tlC+                        cname = P.ecName con+                    ts <- kInRange (srcRange cname)+                            (mapM (`doCheckType` Just KType) (P.ecFields con))+                    pure EnumCon+                          { ecName   = thing cname+                          , ecNumber = nu+                          , ecFields = ts+                          , ecPublic = P.tlExport tlC == P.Public+                          , ecDoc    = thing <$> P.tlDoc tlC+                          }+          simplifyAllConstraints+          pure r+     pure NominalType+                  { ntName = thing x+                  , ntParams = as1+                  , ntKind = KType+                  , ntConstraints = map goal gs+                  , ntDef = Enum cons1+                  , ntFixity = Nothing+                  , ntDoc = mbD+                  }++checkPrimType :: P.PrimType Name -> Maybe Text -> InferM NominalType checkPrimType p mbD =   do let (as,cs) = P.primTCts p-     (as',cs') <- withTParams NoWildCards TPPrimParam as $-                    mapM checkProp cs-     pure AbstractType { atName = thing (P.primTName p)-                       , atKind = cvtK (thing (P.primTKind p))-                       , atFixitiy = P.primTFixity p-                       , atCtrs = (as',cs')-                       , atDoc = mbD-                       }+     (as',cs') <- withTParams NoWildCards TPPrimParam as (mapM checkProp cs)+     let (args,finK) = splitK (cvtK (thing (P.primTKind p)))+         (declared,others) = splitAt (length as') args+     unless (and (zipWith (==) (map kindOf as') args)) $+       panic "checkPrimType"+         [ "Primtive declaration, kind argument prefix mismach:"+         , "Expected: " ++ show (commaSep (map (pp . kindOf) as'))+         , "Actual: " ++ show (commaSep (map pp declared))+         ]+     pure NominalType+            { ntName = thing (P.primTName p)+            , ntParams = as'+            , ntKind = foldr (:->) finK others+            , ntFixity = P.primTFixity p+            , ntConstraints = cs'+            , ntDoc = mbD+            , ntDef = Abstract+            }+  where+  splitK k =+    case k of+      k1 :-> k2 -> (k1:ks,r)+        where (ks,r) = splitK k2+      _ -> ([], k) + checkType :: P.Type Name -> Maybe Kind -> InferM Type checkType t k =   do (_, t1) <- withTParams AllowWildCards schemaParam [] $ doCheckType t k@@ -270,9 +321,8 @@ checkTUser x ts k =   mcase kLookupTyVar      checkBoundVarUse $   mcase kLookupTSyn       checkTySynUse $-  mcase kLookupNewtype    checkNewTypeUse $+  mcase kLookupNominal    checkNominalTypeUse $   mcase kLookupParamType  checkModuleParamUse $-  mcase kLookupAbstractType checkAbstractTypeUse $   checkScopedVarUse -- none of the above, must be a scoped type variable,                     -- if the renamer did its job correctly.   where@@ -286,28 +336,36 @@        t1  <- kInstantiateT (tsDef tysyn) su        checkKind (TUser x ts1 t1) k k1 -  checkNewTypeUse nt =+  checkNominalTypeUse nt+    | Abstract <- ntDef nt =+      do (ts1,k1) <- appTy ts (kindOf nt)+         let as = ntParams nt+             ps = ntConstraints nt+         case as of+           [] -> pure ()+           _ -> do let need = length as+                       have = length ts1+                   when (need > have) $+                     kRecordError (TooFewTyParams (ntName nt) (need - have))+                   let su = listSubst (map tpVar as `zip` ts1)+                   kNewGoals (CtPartialTypeFun (ntName nt)) (apSubst su <$> ps)+         let ty =+               -- We must uphold the invariant that built-in abstract types+               -- are represented with TCon. User-defined abstract types use+               -- TNominal instead.+               case builtInType (ntName nt) of+                 Just tc -> TCon tc ts1+                 Nothing -> TNominal nt ts1+         checkKind ty k k1++    | otherwise =     do (ts1,k1) <- appTy ts (kindOf nt)        let as = ntParams nt        ts2 <- checkParams as ts1        let su = zip as ts2        ps1 <- mapM (`kInstantiateT` su) (ntConstraints nt)        kNewGoals (CtPartialTypeFun (ntName nt)) ps1-       checkKind (TNewtype nt ts2) k k1--  checkAbstractTypeUse absT =-    do let tc   = abstractTypeTC absT-       (ts1,k1) <- appTy ts (kindOf tc)-       let (as,ps) = atCtrs absT-       case ps of-          [] -> pure ()   -- common case-          _ -> do let need = length as-                      have = length ts1-                  when (need > have) $-                     kRecordError (TooFewTyParams (atName absT) (need - have))-                  let su = listSubst (map tpVar as `zip` ts1)-                  kNewGoals (CtPartialTypeFun (atName absT)) (apSubst su <$> ps)-       checkKind (TCon tc ts1) k k1+       checkKind (TNominal nt ts2) k k1    checkParams as ts1     | paramHave == paramNeed = return ts1

@@ -1,20 +1,24 @@ {-# Language BlockArguments, ImplicitParams #-} module Cryptol.TypeCheck.Module (doFunctorInst) where -import Data.List(partition)+import Data.List(partition,unzip4) import Data.Text(Text) import Data.Map(Map) import qualified Data.Map as Map+import qualified Data.Map.Merge.Strict as Map import Data.Set (Set) import qualified Data.Set as Set-import Control.Monad(unless,forM_)+import Control.Monad(unless,forM_,mapAndUnzipM)   import Cryptol.Utils.Panic(panic)-import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent)+import Cryptol.Utils.Ident(Ident,Namespace(..),ModPath,isInfixIdent) import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P+import Cryptol.ModuleSystem.Binds(newFunctorInst) import Cryptol.ModuleSystem.Name(nameIdent)+import Cryptol.ModuleSystem.NamingEnv+          (NamingEnv(..), modParamNamingEnv, shadowing, without) import Cryptol.ModuleSystem.Interface           ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..)           , filterIfaceDecls@@ -36,16 +40,21 @@   {- ^ Instantitation.  These is the renaming for the functor that arises from        generativity (i.e., it is something that will make the names "fresh").   -} ->+  NamingEnv+  {- ^ Names in the enclosing scope of the instantiated module -} ->   Maybe Text                  {- ^ Documentation -} ->   InferM (Maybe TCTopEntity)-doFunctorInst m f as inst doc =+doFunctorInst m f as instMap0 enclosingInScope doc =   inRange (srcRange m)   do mf    <- lookupFunctor (thing f)      argIs <- checkArity (srcRange f) mf as-     m2 <- do as2 <- mapM checkArg argIs-              let (tySus,decls) = unzip [ (su,ds) | DefinedInst su ds <- as2 ]-              let ?tSu = mergeDistinctSubst tySus-                  ?vSu = inst+     m2 <- do let mpath = P.impNameModPath (thing m)+              as2 <- mapM (checkArg mpath) argIs+              let (tySus,paramTySyns,decls,paramInstMaps) =+                    unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ]+              instMap <- addMissingTySyns mpath mf instMap0+              let ?tVarSu = mergeDistinctSubst tySus+                  ?nameSu = instMap <> mconcat paramInstMaps               let m1   = moduleInstance mf                   m2   = m1 { mName             = m                             , mDoc              = Nothing@@ -53,6 +62,7 @@                             , mParamFuns        = mempty                             , mParamConstraints = mempty                             , mParams           = mempty+                            , mTySyns = mconcat paramTySyns <> mTySyns m1                             , mDecls = map NonRecursive (concat decls) ++                                       mDecls m1                             }@@ -73,13 +83,27 @@                                  (Map.unions vps)                                  m2 +     -- An instantiation doesn't really have anything "in scope" per se, but+     -- here we compute what would be in scope as if you hand wrote the+     -- instantiation by copy-pasting the functor then substituting the+     -- parameters. That is, it would be whatever is in scope in the functor,+     -- together with any names in the enclosing scope if this is a nested+     -- module, with the functor's names taking precedence. This is used to+     -- determine what is in scope at the REPL when the instantiation is loaded+     -- and focused.+     --+     -- The exception is when instantiating with _, in which case we must delete+     -- the module parameters from the naming environment.+     let inScope0 = mInScope m2 `without`+           mconcat [ modParamNamingEnv mp | (_, mp, AddDeclParams) <- argIs ]+         inScope = inScope0 `shadowing` enclosingInScope+      case thing m of-       P.ImpTop mn    -> newModuleScope mn (mExports m2)-       P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2)+       P.ImpTop mn    -> newModuleScope mn (mExports m2) inScope+       P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) inScope       mapM_ addTySyn     (Map.elems (mTySyns m2))-     mapM_ addNewtype   (Map.elems (mNewtypes m2))-     mapM_ addPrimType  (Map.elems (mPrimTypes m2))+     mapM_ addNominal   (Map.elems (mNominalTypes m2))      addSignatures      (mSignatures m2)      addSubmodules      (mSubmodules m2)      addFunctors        (mFunctors m2)@@ -100,10 +124,7 @@  {- | Validate a functor application, just checking the argument names. The result associates a module parameter with the concrete way it should-be instantiated, which could be:--  * `Left` instanciate using another parameter that is in scope-  * `Right` instanciate using a module, with the given interface+be instantiated. -} checkArity ::   Range             {- ^ Location for reporting errors -} ->@@ -159,7 +180,16 @@                checkArgs done ps more  -data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params+data ArgInst = -- | Argument that defines the params+               DefinedInst Subst+                 (Map Name TySyn)+                 -- ^ Type synonyms created from the functor's type parameters+                 [Decl]+                 -- ^ Bindings for value parameters+                 (Map Name Name)+                 -- ^ Map from the functor's parameter names to the new names+                 --   created for the instantiation+              | ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type)                -- ^ Argument that add parameters                -- The type parameters are in their module type parameter@@ -179,8 +209,8 @@   * XXX: Extra parameters for instantiation by adding params -} checkArg ::-  (Range, ModParam, ActualArg) -> InferM ArgInst-checkArg (r,expect,actual') =+  ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst+checkArg mpath (r,expect,actual') =   case actual' of     AddDeclParams   -> paramInst     UseParameter {} -> definedInst@@ -197,7 +227,8 @@        pure (ParamInst as cs (Map.mapKeys qual fs))    definedInst =-    do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params))+    do (tRens, tSyns, tInstMaps) <- unzip3 <$>+         mapM (checkParamType mpath r tyMap) (Map.toList (mpnTypes params))        let renSu = listParamSubst (concat tRens)         {- Note: the constraints from the signature are already added to the@@ -205,12 +236,13 @@           doFunctorInst -}  -       vDecls <- concat <$>-                  mapM (checkParamValue r vMap)-                       [ s { mvpType = apSubst renSu (mvpType s) }-                       | s <- Map.elems (mpnFuns params) ]+       (vDecls, vInstMaps) <-+         mapAndUnzipM (checkParamValue mpath r vMap)+           [ s { mvpType = apSubst renSu (mvpType s) }+           | s <- Map.elems (mpnFuns params) ] -       pure (DefinedInst renSu vDecls)+       pure $ DefinedInst renSu (mconcat tSyns)+         (concat vDecls) (mconcat tInstMaps <> mconcat vInstMaps)     params = mpParameters expect@@ -231,8 +263,7 @@        UseModule actual ->         ( Map.unions [ nameMapToIdentMap fromTS      (ifTySyns decls)-                     , nameMapToIdentMap fromNewtype (ifNewtypes decls)-                     , nameMapToIdentMap fromPrimT   (ifAbstractTypes decls)+                     , nameMapToIdentMap fromNominal (ifNominalTypes decls)                      ]          , nameMapToIdentMap fromD (ifDecls decls)@@ -247,8 +278,7 @@          fromD d         = (ifDeclName d, ifDeclSig d)         fromTS ts       = (kindOf ts, tsDef ts)-        fromNewtype nt  = (kindOf nt, TNewtype nt [])-        fromPrimT pt    = (kindOf pt, TCon (abstractTypeTC pt) [])+        fromNominal nt  = (kindOf nt, TNominal nt [])        AddDeclParams -> panic "checkArg" ["AddDeclParams"] @@ -263,51 +293,72 @@  -- | Check a type parameter to a module. checkParamType ::-  Range                 {- ^ Location for error reporting -} ->-  Map Ident (Kind,Type) {- ^ Actual types -} ->-  (Name,ModTParam)      {- ^ Type parameter -} ->-  InferM [(TParam,Type)]  {- ^ Mapping from parameter name to actual type -}-checkParamType r tyMap (name,mp) =+  ModPath                    {- ^ The new module we are creating -} ->+  Range                      {- ^ Location for error reporting -} ->+  Map Ident (Kind,Type)      {- ^ Actual types -} ->+  (Name,ModTParam)           {- ^ Type parameter -} ->+  InferM ([(TParam,Type)], Map Name TySyn, Map Name Name)+    {- ^ Mapping from parameter name to actual type (for type substitution),+         type synonym map from a fresh type name to the actual type+           (only so that the type can be referred to in the REPL;+            type synonyms are fully inlined into types at this point),+         and a map from the old type name to the fresh type name+           (for instantiation) -}+checkParamType mpath r tyMap (name,mp) =   let i       = nameIdent name       expectK = mtpKind mp   in   case Map.lookup i tyMap of     Nothing ->       do recordErrorLoc (Just r) (FunctorInstanceMissingName NSType i)-         pure []+         pure ([], Map.empty, Map.empty)     Just (actualK,actualT) ->       do unless (expectK == actualK)            (recordErrorLoc (Just r)                            (KindMismatch (Just (TVFromModParam name))                                                   expectK actualK))-         pure [(mtpParam mp, actualT)]+         name' <- newFunctorInst mpath name+         let tySyn = TySyn { tsName = name'+                           , tsParams = []+                           , tsConstraints = []+                           , tsDef = actualT+                           , tsDoc = mtpDoc mp }+         pure ( [(mtpParam mp, actualT)]+              , Map.singleton name' tySyn+              , Map.singleton name name'+              )  -- | Check a value parameter to a module. checkParamValue ::+  ModPath                 {- ^ The new module we are creating -} ->   Range                   {- ^ Location for error reporting -} ->   Map Ident (Name,Schema) {- ^ Actual values -} ->   ModVParam               {- ^ The parameter we are checking -} ->-  InferM [Decl]           {- ^ Mapping from parameter name to definition -}-checkParamValue r vMap mp =+  InferM ([Decl], Map Name Name)+  {- ^ Decl mapping a new name to the actual value,+       and a map from the value param name in the functor to the new name+         (for instantiation) -}+checkParamValue mpath r vMap mp =   let name     = mvpName mp       i        = nameIdent name       expectT  = mvpType mp   in case Map.lookup i vMap of        Nothing ->          do recordErrorLoc (Just r) (FunctorInstanceMissingName NSValue i)-            pure []+            pure ([], Map.empty)        Just actual ->          do e <- mkParamDef r (name,expectT) actual-            let d = Decl { dName        = name+            name' <- newFunctorInst mpath name+            let d = Decl { dName        = name'                          , dSignature   = expectT                          , dDefinition  = DExpr e                          , dPragmas     = []-                         , dInfix       = isInfixIdent (nameIdent name)+                         , dInfix       = isInfixIdent (nameIdent name')                          , dFixity      = mvpFixity mp                          , dDoc         = mvpDoc mp                          } -            pure [d]+            pure ([d], Map.singleton name name')   @@ -372,5 +423,21 @@      applySubst res  --+-- | The instMap we get from the renamer will not contain the fresh names for+-- certain things in the functor generated in the typechecking stage, if we are+-- instantiating a functor that is in the same file, since renaming and+-- typechecking happens together with the instantiation. In particular, if the+-- functor's interface has type synonyms, they will only get copied over into+-- the functor in the typechecker, so the renamer will not see them. Here we+-- make the fresh names for those missing type synonyms and add them to the+-- instMap.+addMissingTySyns ::+  ModPath                  {- ^ The new module we are creating -} ->+  ModuleG ()               {- ^ The functor -} ->+  Map Name Name            {- ^ instMap we get from renamer -} ->+  InferM (Map Name Name)   {- ^ the complete instMap -}+addMissingTySyns mpath f = Map.mergeA+  (Map.traverseMissing \name _ -> newFunctorInst mpath name)+  Map.preserveMissing+  (Map.zipWithMatched \_ _ name' -> name')+  (mTySyns f)

@@ -18,15 +18,15 @@ import Data.Maybe(mapMaybe) import qualified Data.Text as Text -import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..)+import Cryptol.Utils.Ident(modPathIsOrContains,Namespace(..)                           , Ident, mkIdent, identText                           , ModName, modNameChunksText ) import Cryptol.Utils.PP(pp) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr)+import Cryptol.Parser.AST(impNameModPath) import Cryptol.Parser.Position-import Cryptol.ModuleSystem.Name(-  nameModPath, nameModPathMaybe, nameIdent, mapNameIdent)+import Cryptol.ModuleSystem.Name(nameModPathMaybe, nameIdent, mapNameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Error import qualified Cryptol.TypeCheck.Monad as TC@@ -56,7 +56,7 @@          , tparams = Set.toList as          , constraints = ps          , vparams = mp-         , newNewtypes = Map.empty+         , newNominalTypes = Map.empty          }      do unless (null bad)@@ -64,12 +64,12 @@         rec          ts <- doAddParams nt mTySyns-         nt <- doAddParams nt mNewtypes+         nt <- doAddParams nt mNominalTypes          ds <- doAddParams nt mDecls         pure m          { mTySyns   = ts-         , mNewtypes = nt+         , mNominalTypes = nt          , mDecls    = ds          } @@ -78,14 +78,14 @@        ++ mkBad mPrimTypes BIAbstractType        ++ mkBad mSignatures BIInterface +    mPrimTypes = Map.filter nominalTypeIsAbstract . mNominalTypes+     mkBad sel a = [ (a,k) | k <- Map.keys (sel m) ] -    ourPath = case thing (mName m) of-                ImpTop mo    -> TopModule mo-                ImpNested mo -> Nested (nameModPath mo) (nameIdent mo)+    ourPath = impNameModPath (thing (mName m))      doAddParams nt sel =-      mapReader (\ro -> ro { newNewtypes = nt }) (addParams (sel m))+      mapReader (\ro -> ro { newNominalTypes = nt }) (addParams (sel m))   type RewM = ReaderT RO TC.InferM@@ -98,7 +98,7 @@   , tparams      :: [MBQual TParam]   , constraints  :: [Prop]   , vparams      :: Map (MBQual Name) Type-  , newNewtypes  :: Map Name Newtype+  , newNominalTypes :: Map Name NominalType   }  @@ -111,17 +111,28 @@ instance AddParams a => AddParams [a] where   addParams = mapM addParams -instance AddParams Newtype where+instance AddParams NominalType where   addParams nt =-    do (tps,cs) <- newTypeParams TPNewtypeParam+    do (tps,cs) <- newTypeParams TPNominalParam        rProps   <- rewTypeM tps (ntConstraints nt)-       rFields  <- rewTypeM tps (ntFields nt)+       def <- case ntDef nt of+                Struct con ->+                   Struct <$>+                   do rFields  <- rewTypeM tps (ntFields con)+                      pure con { ntFields = rFields }+                Enum cons ->+                  Enum <$>+                  forM cons \c ->+                    do rFileds <- rewTypeM tps (ecFields c)+                       pure c { ecFields = rFileds }+                Abstract -> pure Abstract        pure nt-         { ntParams       = pDecl tps ++ ntParams nt-         , ntConstraints  = cs ++ rProps-         , ntFields       = rFields+         { ntParams      = pDecl tps ++ ntParams nt+         , ntConstraints = cs ++ rProps+         , ntDef         = def          } + instance AddParams TySyn where   addParams ts =     do (tps,cs) <- newTypeParams TPTySynParam@@ -251,12 +262,12 @@                  )  liftRew ::-  ((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) ->+  ((?isOurs :: Name -> Bool, ?newNominalTypes :: Map Name NominalType) => a) ->   RewM a liftRew x =   do ro <- ask      let ?isOurs      = isOurs ro-         ?newNewtypes = newNewtypes ro+         ?newNominalTypes = newNominalTypes ro      pure x  rewTypeM :: RewType t => TypeParams -> t -> RewM t@@ -274,7 +285,7 @@ class RewType t where   rewType ::     ( ?isOurs      :: Name -> Bool-    , ?newNewtypes :: Map Name Newtype    -- Lazy+    , ?newNominalTypes :: Map Name NominalType -- Lazy     , ?tparams     :: TypeParams     ) => t -> t @@ -282,10 +293,7 @@   rewType ty =     case ty of -      TCon tc ts-        | TC (TCAbstract (UserTC x _)) <- tc-        , ?isOurs x  -> TCon tc (pUse ?tparams ++ rewType ts)-        | otherwise  -> TCon tc (rewType ts)+      TCon tc ts -> TCon tc (rewType ts)        TVar x ->         case x of@@ -301,12 +309,12 @@        TRec fs -> TRec (rewType fs) -      TNewtype tdef ts-        | ?isOurs nm -> TNewtype tdef' (pUse ?tparams ++ rewType ts)-        | otherwise  -> TNewtype tdef (rewType ts)+      TNominal tdef ts+        | ?isOurs nm -> TNominal tdef' (pUse ?tparams ++ rewType ts)+        | otherwise  -> TNominal tdef (rewType ts)         where         nm    = ntName tdef-        tdef' = case Map.lookup nm ?newNewtypes of+        tdef' = case Map.lookup nm ?newNominalTypes of                   Just yes -> yes                   Nothing  -> panic "rewType" [ "Missing recursive newtype"                                               , show (pp nm) ]@@ -328,7 +336,7 @@ class RewVal t where   rew ::     ( ?isOurs      :: Name -> Bool-    , ?newNewtypes :: Map Name Newtype    -- Lazy+    , ?newNominalTypes :: Map Name NominalType -- Lazy     , ?tparams     :: TypeParams     , ?cparams     :: Int                 -- Number of constraitns     , ?vparams     :: ValParams@@ -352,6 +360,7 @@       ESel e l          -> ESel (rew e) l       ESet t e1 s e2    -> ESet (rewType t) (rew e1) s (rew e2)       EIf e1 e2 e3      -> EIf (rew e1) (rew e2) (rew e3)+      ECase e as d      -> ECase (rew e) (rew <$> as) (rew <$> d)       EComp t1 t2 e mss -> EComp (rewType t1) (rewType t2) (rew e) (rew mss)       EVar x            -> tryVarApp                            case Map.lookup x (pSubst ?vparams) of@@ -379,6 +388,9 @@                evs = foldl EApp eps (pUse ?vparams)            in evs         _ -> orElse++instance RewVal CaseAlt where+  rew (CaseAlt xs e) = CaseAlt xs (rew e)   instance RewVal DeclGroup where

@@ -8,26 +8,29 @@  import Cryptol.Parser.Position(Located) import Cryptol.ModuleSystem.Interface(IfaceNames(..))+import Cryptol.ModuleSystem.NamingEnv(NamingEnv,mapNamingEnv) import Cryptol.IR.TraverseNames(TraverseNames,mapNames) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)  -{- | `?tSu` should be applied to all types.-     `?vSu` shoudl be applied to all values. -}-type Su = (?tSu :: Subst, ?vSu :: Map Name Name)+{- | `?tVarSu` substitutes 'Type's for 'TVar's which are module type parameters.+     `?nameSu` substitutes fresh 'Name's for the functor's 'Name's+       (in all namespaces). -}+type Su = (?tVarSu :: Subst, ?nameSu :: Map Name Name) --- | Has value names but no types.-doVInst :: (Su, TraverseNames a) => a -> a-doVInst = mapNames (\x -> Map.findWithDefault x x ?vSu)+-- | Instantiate something that has 'Name's.+doNameInst :: (Su, TraverseNames a) => a -> a+doNameInst = mapNames (\x -> Map.findWithDefault x x ?nameSu) --- | Has types but not values.-doTInst :: (Su, TVars a) => a -> a-doTInst = apSubst ?tSu+-- | Instantiate something that has 'TVar's.+doTVarInst :: (Su, TVars a) => a -> a+doTVarInst = apSubst ?tVarSu --- | Has both value names and types.-doTVInst :: (Su, TVars a, TraverseNames a) => a -> a-doTVInst = apSubst ?tSu . doVInst+-- | Instantiate something that has both 'TVar's and 'Name's.+-- Order is important here because '?tVarSu' might insert 'Name's.+doInst :: (Su, TVars a, TraverseNames a) => a -> a+doInst = doNameInst . doTVarInst  doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a doMap mp =@@ -49,8 +52,11 @@   moduleInstance l = moduleInstance <$> l  instance ModuleInstance Name where-  moduleInstance = doVInst+  moduleInstance = doNameInst +instance ModuleInstance NamingEnv where+  moduleInstance = mapNamingEnv doNameInst+ instance ModuleInstance name => ModuleInstance (ImpName name) where   moduleInstance x =     case x of@@ -61,7 +67,7 @@   moduleInstance m =     Module { mName             = mName m            , mDoc              = Nothing-           , mExports          = doVInst (mExports m)+           , mExports          = doNameInst (mExports m)            , mParamTypes       = doMap (mParamTypes m)            , mParamFuns        = doMap (mParamFuns m)            , mParamConstraints = moduleInstance (mParamConstraints m)@@ -69,18 +75,18 @@            , mFunctors         = doMap (mFunctors m)            , mNested           = doSet (mNested m)            , mTySyns           = doMap (mTySyns m)-           , mNewtypes         = doMap (mNewtypes m)-           , mPrimTypes        = doMap (mPrimTypes m)+           , mNominalTypes     = doMap (mNominalTypes m)            , mDecls            = moduleInstance (mDecls m)            , mSubmodules       = doMap (mSubmodules m)            , mSignatures       = doMap (mSignatures m)+           , mInScope          = moduleInstance (mInScope m)            }  instance ModuleInstance Type where-  moduleInstance = doTInst+  moduleInstance = doInst  instance ModuleInstance Schema where-  moduleInstance = doTInst+  moduleInstance = doInst  instance ModuleInstance TySyn where   moduleInstance ts =@@ -91,26 +97,42 @@           , tsDoc         = tsDoc ts           } -instance ModuleInstance Newtype where+instance ModuleInstance NominalType where   moduleInstance nt =-    Newtype { ntName        = moduleInstance (ntName nt)+    NominalType+            { ntName        = moduleInstance (ntName nt)             , ntParams      = ntParams nt+            , ntKind        = ntKind nt             , ntConstraints = moduleInstance (ntConstraints nt)-            , ntConName     = moduleInstance (ntConName nt)-            , ntFields      = moduleInstance <$> ntFields nt+            , ntDef         = moduleInstance (ntDef nt)+            , ntFixity      = ntFixity nt             , ntDoc         = ntDoc nt             } -instance ModuleInstance AbstractType where-  moduleInstance at =-    AbstractType { atName     = moduleInstance (atName at)-                 , atKind     = atKind at-                 , atCtrs     = let (ps,cs) = atCtrs at-                                in (ps, moduleInstance cs)-                 , atFixitiy  = atFixitiy at-                 , atDoc      = atDoc at-                 }+instance ModuleInstance NominalTypeDef where+  moduleInstance def =+    case def of+      Struct c -> Struct (moduleInstance c)+      Enum cs  -> Enum   (moduleInstance cs)+      Abstract -> Abstract +instance ModuleInstance StructCon where+  moduleInstance c =+    StructCon+      { ntConName     = moduleInstance (ntConName c)+      , ntFields      = moduleInstance <$> ntFields c+      }++instance ModuleInstance EnumCon where+  moduleInstance c =+    EnumCon+      { ecName        = moduleInstance (ecName c)+      , ecNumber      = ecNumber c+      , ecFields      = moduleInstance (ecFields c)+      , ecPublic      = ecPublic c+      , ecDoc         = ecDoc c+      }+ instance ModuleInstance DeclGroup where   moduleInstance dg =     case dg of@@ -118,7 +140,7 @@       NonRecursive d -> NonRecursive (moduleInstance d)  instance ModuleInstance Decl where-  moduleInstance = doTVInst+  moduleInstance = doInst   instance ModuleInstance name => ModuleInstance (IfaceNames name) where

@@ -40,6 +40,7 @@ import           Cryptol.ModuleSystem.Name                     (FreshM(..),Supply,mkLocal,asLocal                     , nameInfo, NameInfo(..),NameSource(..), nameTopModule)+import           Cryptol.ModuleSystem.NamingEnv.Types import qualified Cryptol.ModuleSystem.Interface as If import           Cryptol.Parser.Position import qualified Cryptol.Parser.AST as P@@ -64,8 +65,7 @@   { inpRange     :: Range             -- ^ Location of program source   , inpVars      :: Map Name Schema   -- ^ Variables that are in scope   , inpTSyns     :: Map Name TySyn    -- ^ Type synonyms that are in scope-  , inpNewtypes  :: Map Name Newtype  -- ^ Newtypes in scope-  , inpAbstractTypes :: Map Name AbstractType   -- ^ Abstract types in scope+  , inpNominalTypes :: Map Name NominalType -- ^ Nominal types in scope   , inpSignatures :: !(Map Name ModParamNames)  -- ^ Signatures in scope    , inpTopModules    :: ModName -> Maybe (ModuleG (), If.IfaceG ())@@ -129,8 +129,9 @@       let env = Map.map ExtVar (inpVars info)             <> Map.fromList-              [ (ntConName nt, ExtVar (newtypeConType nt))-              | nt <- Map.elems (inpNewtypes info)+              [ (c, ExtVar t)+              | nt <- Map.elems (inpNominalTypes info)+              , (c,t) <- nominalTypeConTypes nt               ]             <> Map.map (ExtVar . mvpType) (mpnFuns allPs) @@ -141,8 +142,7 @@                          , iExtScope = (emptyModule ExternalScope)                              { mTySyns           = inpTSyns info <>                                                    mpnTySyn allPs-                             , mNewtypes         = inpNewtypes info-                             , mPrimTypes        = inpAbstractTypes info+                             , mNominalTypes     = inpNominalTypes info                              , mParamTypes       = mpnTypes allPs                              , mParamFuns        = mpnFuns  allPs                              , mParamConstraints = mpnConstraints allPs@@ -611,7 +611,7 @@       TPPropSynParam _ -> starOrHashOrProp       TPTySynParam _   -> starOrHash       TPSchemaParam _  -> starOrHash-      TPNewtypeParam _ -> starOrHash+      TPNominalParam _ -> starOrHash       TPPrimParam _    -> starOrHash       TPUnifyVar       -> starOrHash @@ -629,7 +629,6 @@         KType -> return ()         _ -> recordError (BadParameterKind tp k) - -- | Generate a new free type variable. newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam newTParam nm flav k =@@ -788,12 +787,9 @@ lookupTSyn :: Name -> InferM (Maybe TySyn) lookupTSyn x = Map.lookup x <$> getTSyns --- | Lookup the definition of a newtype-lookupNewtype :: Name -> InferM (Maybe Newtype)-lookupNewtype x = Map.lookup x <$> getNewtypes--lookupAbstractType :: Name -> InferM (Maybe AbstractType)-lookupAbstractType x = Map.lookup x <$> getAbstractTypes+-- | Lookup the definition of a nominal type+lookupNominal :: Name -> InferM (Maybe NominalType)+lookupNominal x = Map.lookup x <$> getNominalTypes  -- | Lookup the kind of a parameter type lookupParamType :: Name -> InferM (Maybe ModTParam)@@ -907,13 +903,9 @@ getTSyns :: InferM (Map Name TySyn) getTSyns = getScope mTySyns --- | Returns the newtype declarations that are in scope.-getNewtypes :: InferM (Map Name Newtype)-getNewtypes = getScope mNewtypes---- | Returns the abstract type declarations that are in scope.-getAbstractTypes :: InferM (Map Name AbstractType)-getAbstractTypes = getScope mPrimTypes+-- | Returns the nominal type declarations that are in scope.+getNominalTypes :: InferM (Map Name NominalType)+getNominalTypes = getScope mNominalTypes  -- | Returns the abstract function declarations getParamTypes :: InferM (Map Name ModTParam)@@ -1006,16 +998,16 @@ to initialize an empty module.  As we type check declarations they are added to this module's scope. -} newSubmoduleScope ::-  Name -> Maybe Text -> ExportSpec Name -> InferM ()-newSubmoduleScope x docs e =+  Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> InferM ()+newSubmoduleScope x docs e inScope =   do updScope \o -> o { mNested = Set.insert x (mNested o) }      newScope (SubModule x)-     updScope \m -> m { mDoc = docs, mExports = e }+     updScope \m -> m { mDoc = docs, mExports = e, mInScope = inScope } -newModuleScope :: P.ModName -> ExportSpec Name -> InferM ()-newModuleScope x e =+newModuleScope :: P.ModName -> ExportSpec Name -> NamingEnv -> InferM ()+newModuleScope x e inScope =   do newScope (MTopModule x)-     updScope \m -> m { mDoc = Nothing, mExports = e }+     updScope \m -> m { mDoc = Nothing, mExports = e, mInScope = inScope }  -- | Update the current scope (first in the list). Assumes there is one. updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()@@ -1057,10 +1049,10 @@                  , mParamConstraints = mParamConstraints y                  , mParams           = mParams y                  , mNested           = mNested y+                 , mInScope          = mInScope y                   , mTySyns      = add mTySyns-                 , mNewtypes    = add mNewtypes-                 , mPrimTypes   = add mPrimTypes+                 , mNominalTypes = add mNominalTypes                  , mDecls       = add mDecls                  , mSignatures  = add mSignatures                  , mSubmodules  = if isFun@@ -1149,12 +1141,13 @@       , mNested           = mempty        , mTySyns           = uni mTySyns-      , mNewtypes         = uni mNewtypes-      , mPrimTypes        = uni mPrimTypes+      , mNominalTypes     = uni mNominalTypes       , mDecls            = uni mDecls       , mSubmodules       = uni mSubmodules       , mFunctors         = uni mFunctors       , mSignatures       = uni mSignatures++      , mInScope          = uni mInScope       }     where     uni f = f m1 <> f m2@@ -1175,18 +1168,12 @@      checkTShadowing "synonym" x      updScope \r -> r { mTySyns = Map.insert x t (mTySyns r) } -addNewtype :: Newtype -> InferM ()-addNewtype t =-  do updScope \r -> r { mNewtypes = Map.insert (ntName t) t (mNewtypes r) }-     IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntConName t)-                                                    (newtypeConType t)-                                                    (iBindTypes rw) }--addPrimType :: AbstractType -> InferM ()-addPrimType t =-  updScope \r ->-    r { mPrimTypes = Map.insert (atName t) t (mPrimTypes r) }-+addNominal :: NominalType -> InferM ()+addNominal t =+  do updScope \r -> r { mNominalTypes = Map.insert (ntName t) t (mNominalTypes r) }+     let cons = nominalTypeConTypes t+         ins  = uncurry Map.insert+     IM $ sets_ \rw -> rw { iBindTypes = foldr ins (iBindTypes rw) cons }  addParamType :: ModTParam -> InferM () addParamType a =@@ -1354,15 +1341,12 @@ kLookupTSyn :: Name -> KindM (Maybe TySyn) kLookupTSyn x = kInInferM $ lookupTSyn x --- | Lookup the definition of a newtype.-kLookupNewtype :: Name -> KindM (Maybe Newtype)-kLookupNewtype x = kInInferM $ lookupNewtype x+-- | Lookup the definition of a nominal type.+kLookupNominal :: Name -> KindM (Maybe NominalType)+kLookupNominal = kInInferM . lookupNominal  kLookupParamType :: Name -> KindM (Maybe ModTParam) kLookupParamType x = kInInferM (lookupParamType x)--kLookupAbstractType :: Name -> KindM (Maybe AbstractType)-kLookupAbstractType x = kInInferM $ lookupAbstractType x  kExistTVar :: Name -> Kind -> KindM Type kExistTVar x k = kInInferM $ existVar x k